Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005713OCamltypingpublic2012-08-02 14:572016-12-07 21:00
Assigned Togarrigue 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.04.0 
Summary0005713: 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 *)

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 *)

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
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.
octachron (developer)
2016-12-07 20:59

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 [^]

- 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
2013-06-12 17:32 frisch Target Version 4.00.2+dev => 4.02.0+dev
2013-07-12 18:15 doligez Target Version 4.02.0+dev => 4.01.1+dev
2014-05-25 20:24 doligez Target Version 4.01.1+dev => 4.02.0+dev
2014-08-21 11:51 doligez Target Version 4.02.0+dev =>
2016-12-07 20:59 octachron Note Added: 0016809
2016-12-07 21:00 octachron Status assigned => resolved
2016-12-07 21:00 octachron Fixed in Version => 4.04.0
2016-12-07 21:00 octachron Resolution open => fixed
2017-02-23 16:45 doligez Category OCaml typing => typing

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker