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: 5713 Reporter:@alainfrisch Assigned to:@garrigue Status: resolved (set by @Octachron on 2016-12-07T20:00:43Z) Resolution: fixed Priority: normal Severity: feature Fixed in version: 4.04.0 Category: typing Child of:#5998 Monitored by: mbarbin @glondu@hcarty@alainfrisch
Bug description
Consider:
type 'a gadt = A: int gadt
let f (type s) =
let _foo (x : s gadt) : s =
match x with
| A -> 5 (* here s == int *)
in
()
This type-checks because in the context of the branch, one can use the equation s == int. Here, s is a fresh locally abstract type introduced by the (type s) syntax.
Now, consider:
module type S = sig type s end
let f (module X : S) =
let _foo (x : X.s gadt) : X.s =
match x with
| A -> 5 (* here X.s == int *)
in
()
Here, we have a local abstract type X.s, but it cannot be refined by opening the GADT.
We have faced this situation in real code, where we were forced to create a local polymorphic function (with explicit local abstract types) and use it immediately on a fixed type obtained by unpacking a first-class module.
Would it be possible to allow GADTs to add equations to such local abstract types introduced by module unpacking?
The text was updated successfully, but these errors were encountered:
I have already been thinking about that for a while.
The main problem is that it would require modifying types deep in the environment.
This is clearly an objective for the next version if it can be done simply enough.
In the meantime, eta-expansion is indeed your friend.
As far as I understand, the issue has been incidentally resolved in OCaml 4.04 by
the more generic handling of non-local abstract types introduced in #579.
Original bug ID: 5713
Reporter: @alainfrisch
Assigned to: @garrigue
Status: resolved (set by @Octachron on 2016-12-07T20:00:43Z)
Resolution: fixed
Priority: normal
Severity: feature
Fixed in version: 4.04.0
Category: typing
Child of: #5998
Monitored by: mbarbin @glondu @hcarty @alainfrisch
Bug description
Consider:
This type-checks because in the context of the branch, one can use the equation s == int. Here, s is a fresh locally abstract type introduced by the (type s) syntax.
Now, consider:
Here, we have a local abstract type X.s, but it cannot be refined by opening the GADT.
We have faced this situation in real code, where we were forced to create a local polymorphic function (with explicit local abstract types) and use it immediately on a fixed type obtained by unpacking a first-class module.
Would it be possible to allow GADTs to add equations to such local abstract types introduced by module unpacking?
The text was updated successfully, but these errors were encountered: