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

Support GADT equations on non-local abstract types #7233

Closed
vicuna opened this issue Apr 19, 2016 · 3 comments
Closed

Support GADT equations on non-local abstract types #7233

vicuna opened this issue Apr 19, 2016 · 3 comments
Assignees
Labels
feature-wish typing typing-GADTS GADT typing and exhaustiveness bugs

Comments

@vicuna
Copy link

vicuna commented Apr 19, 2016

Original bug ID: 7233
Reporter: @lpw25
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-09-24T15:33:19Z)
Resolution: fixed
Priority: normal
Severity: feature
Fixed in version: 4.04.0 +dev / +beta1 / +beta2
Category: typing
Child of: #5998
Monitored by: runhang @gasche @yallop @hcarty

Bug description

Currently matching on a GADT can only introduce equations on locally abstract types. It would be useful if they could also add equations to other abstract types. For example:

type (_, _) eq = Refl : ('a, 'a) eq

module type S = sig
type t
val eql : (t, int) eq
end

module F (M : S) = struct

  let zero : M.t =
    let Refl = M.eql in
      0

end

Currently, the above is an error:

Error: This expression has type int but an expression was expected of type
M.t

Mostly such cases can be worked around by introducing a locally abstract type, but it is an unnecessary chore and can require code duplication.

@vicuna
Copy link
Author

vicuna commented Apr 19, 2016

Comment author: @lpw25

I remember Jacques mentioning that he would like to add support for this, but I couldn't find an actual Mantis issue for it, so I thought I would create one to track the issue.

I also considered having a go at adding support myself, by I wasn't entirely confident of what was required. Jacques, do you have a clear idea of what needs to be done?

@vicuna
Copy link
Author

vicuna commented Apr 28, 2016

Comment author: @garrigue

One has to update the environment to add equations deeply inside modules.
An extra difficulty is that open can duplicate definitions, without keeping the sharing.
Actually, the work of Frédéric on implicit resolution is related to this, as he ends up modifying the environment.
I would rather do that together or after.

@vicuna
Copy link
Author

vicuna commented May 12, 2016

Comment author: @garrigue

Actually, the (rather simple) changes in GPR #578 have made this almost trivial.
See GPR #579 for a seemingly working implementation.
#579

Anybody willing to torture it?

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