"Fatal error: types should not include variables" #6158
Original bug ID: 6158
The following code should be rejected but triggers an internal error:
$ cat vars.ml
type (_, _) eq = Refl : ('a, 'a) eq
let f : (int s, int t) eq -> unit = function
A similar example with well-typed code gives the same error:
$ cat vars2.ml
module M (S : sig
The text was updated successfully, but these errors were encountered:
Comment author: @garrigue
Fixed in trunk and 4.01, revision 14064.
Indeed, the incompatibility check is more clever than before, but as a result it may be called on type definitions containing variables. No need to fail in that case.
Keep this PR open, as there is a minor side-problem, as the non-principal typechecker may leave reified variables in exported types. They are detected and report when using -principal.