|Anonymous | Login | Signup for a new account||2013-05-24 00:56 CEST|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0005713||OCaml||OCaml typing||public||2012-08-02 14:57||2013-04-23 02:46|
|Target Version||4.00.2+dev||Fixed in Version|
|Summary||0005713: Opening GADTs to get more equations on local abstract types introduced by module unpacking|
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.
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?
|Tags||No tags attached.|
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.
|2012-08-02 14:57||frisch||New Issue|
|2012-08-02 15:32||garrigue||Assigned To||=> garrigue|
|2012-08-02 15:32||garrigue||Status||new => assigned|
|2012-08-02 15:36||garrigue||Note Added: 0007874|
|2012-09-06 19:32||frisch||Target Version||4.00.1+dev => 4.00.2+dev|
|2013-04-23 02:46||garrigue||Relationship added||child of 0005998|
|Copyright © 2000 - 2011 MantisBT Group|