Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Opening GADTs to get more equations on local abstract types introduced by module unpacking #5713

Closed
vicuna opened this issue Aug 2, 2012 · 2 comments
Assignees
Labels
feature-wish typing typing-GADTS GADT typing and exhaustiveness bugs

Comments

@vicuna
Copy link

vicuna commented Aug 2, 2012

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?

@vicuna
Copy link
Author

vicuna commented Aug 2, 2012

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented Dec 7, 2016

Comment author: @Octachron

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.

@vicuna vicuna closed this as completed Dec 7, 2016
@vicuna vicuna added the typing label Mar 14, 2019
@Octachron Octachron added the typing-GADTS GADT typing and exhaustiveness bugs label May 18, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature-wish typing typing-GADTS GADT typing and exhaustiveness bugs
Projects
None yet
Development

No branches or pull requests

3 participants