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
If you do allow this eventually, you'll have to be very careful to avoid the same sort of issues as #7215 arising via "module rec" instead of "let rec".
Here's an erroneous program which used to trigger the assert, and is now correctly rejected. Any patch that allows toplevel refinement will have to ensure this program is still rejected:
type (,) eq = Refl : ('a, 'a) eq
let bad (type a) =
let module N = struct
module rec M : sig
val e : (int, a) eq
end = struct
let (Refl : (int, a) eq) = M.e
let e : (int, a) eq = Refl
end
end in N.M.e
I do not think that the current check for "recursive module cannot be safely evaluated" will catch this case, for the same reasons as #7215.
Original bug ID: 7214
Reporter: @stedolan
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-09-24T15:32:14Z)
Resolution: fixed
Priority: normal
Severity: minor
Target version: 4.03.0+dev / +beta1
Fixed in version: 4.03.0+dev / +beta1
Category: typing
Monitored by: braibant @gasche @yallop @hcarty
Bug description
The following program causes an assertion in Env.add_gadt_instance to fail:
type _ t = I : int t
let f (type a) (x : a t) =
let module M = struct
let (I : a t) = x
let x = (I : a t)
end in
()
Tested on recent trunk and 4.03+beta1.
The text was updated successfully, but these errors were encountered: