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: 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.
The text was updated successfully, but these errors were encountered:
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.
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?
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.)
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.
The text was updated successfully, but these errors were encountered: