Mantis Bug Tracker
Main | My View | View Issues | Change Log | Roadmap
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005713OCamlOCaml typingpublic2012-08-02 14:572013-04-23 02:46
Reporterfrisch 
Assigned Togarrigue 
PrioritynormalSeverityfeatureReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version 
Target Version4.00.2+devFixed in Version 
Summary0005713: Opening GADTs to get more equations on local abstract types introduced by module unpacking
DescriptionConsider:

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?
TagsNo tags attached.
Attached Files

- Relationships
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 

-  Notes
(0007874)
garrigue (manager)
2012-08-02 15:36

 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.

- Issue History
Date Modified Username Field Change
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
Powered by Mantis Bugtracker