Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Type checker can loop infinitly and consumes all computer memory #7747

Closed
vicuna opened this Issue Feb 28, 2018 · 2 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link
Collaborator

vicuna commented Feb 28, 2018

Original bug ID: 7747
Reporter: kantian
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2018-03-01T07:10:00Z)
Resolution: fixed
Priority: normal
Severity: minor
Fixed in version: 4.07.0+dev/beta2/rc1/rc2
Category: typing
Related to: #7739
Monitored by: @gasche @hcarty

Bug description

I allready mentioned the problem in the discussion about MPR #7739 issue, but I think it deserves its own independant report.

Normally cycles in types defintion are disallowed by the type checker, as in this example:

module rec M : sig type t = N.t end = struct type t end
and N : sig type t = M.t end = struct type t = M.t end;;
Error: The definition of M.t contains a cycle:
N.t

But with GADT we can hide this cycle and reveal it only when inspecting an equality witness value. In some cases this can put the type checker in an infinite loop and memory consumption increases drastically (around 1 GB per 10 seconds on my computer).

The reproduction case (below) is pretty pathological and a corner case, but I don't know if such situation can appear in a more realistic code wich combines GADT and private types.

Steps to reproduce

type (,) eq = Refl : ('a,'a) eq

module M = struct type t end
module N : sig type t = private M.t val eq : (t, M.t) eq end =
struct type t = M.t let eq = Refl end

(*
as long as we are casting between M.t and N.t
there is no problem, this will type check.
*)

let f x = match N.eq with Refl -> (x : N.t :> M.t)

let f x = match N.eq with Refl -> (x : M.t :> N.t)

(*
but as soon we're trying to cast to another type,
the type checker will never return and memory
consumption will increase drastically.
*)

let f x = match N.eq with Refl -> (x : N.t :> int)

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Mar 1, 2018

Comment author: @garrigue

Well-spotted.
We should certainly expand private abbreviations when checking for recursion.
Trivial fix at: #1641

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Mar 1, 2018

Comment author: @garrigue

Merged #1641 as commit a84c11e.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.