Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
Assertion failure in Env.add_gadt_instances #7214
Original bug ID: 7214
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) =
Tested on recent trunk and 4.03+beta1.
Comment author: @stedolan
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) =
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.