Segfault from recursive modules violating exhaustiveness assumptions

[vicuna]

Original bug ID: 6993
Reporter: @stedolan
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-02-16T14:14:49Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.02.3
Fixed in version: 4.03.0+dev / +beta1
Category: typing
Related to: #7016
Monitored by: @gasche @diml @yallop @hcarty

Bug description

Without -rectypes, the exhaustiveness checker "knows" that there is no type t = t list, and so accepts this definition as exhaustive (and optimises away the actual match check):

type (_, _) eqp = Y : ('a, 'a) eqp | N : string -> ('a, 'b) eqp
let f : ('a list, 'a) eqp -> unit = function N s -> print_string s

Using recursive modules, we can construct a type t = t list, even without -rectypes:

module rec A : sig
type t = B.t list
end = struct
type t = B.t list
end and B : sig
type t
val eq : (B.t list, t) eqp
end = struct
type t = A.t
let eq = Y
end

The expression "f B.eq" segfaults.

This example does not segfault with -rectypes, since in that case the exhaustiveness checker does not assume t = t list is impossible.

[vicuna]

Comment author: @garrigue

Fixed in trunk at revision 16426.

Done by allowing recursive types when doing unification on GADT indices (in patterns),
since we want pattern typing to coincide with the exhaustiveness.
Wondering if one could come with a strange example introducing a recursive type this way...
I suppose it wouldn't be bad (we are only talking about types, not parameterized type definitions), but need to think more about it.

[vicuna]

Comment author: @stedolan

If recursive types are assumed to be possible during GADT matching, is there any remaining reason for the restriction on linking -rectypes and non-rectypes code?

[vicuna]

Comment author: @garrigue

Good question. I don't quite remember the reason this was done, but since it seems that the code must be defensive anyway, at least the problem is not soundness anymore.

I still think this is a bad idea to do that, as the behavior of type inference may turn erratic.
Recursive types coming for other modules would be allowed, but one couldn't build one.

If there is a strong demand to remove the restriction, I believe there should still be a warning.
(IIRC, people from Coq were interested in this problem.)