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)