You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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)
The text was updated successfully, but these errors were encountered:
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)
The text was updated successfully, but these errors were encountered: