Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007233OCamltypingpublic2016-04-19 18:292017-09-24 17:33
Reporterlpw25 
Assigned Togarrigue 
PrioritynormalSeverityfeatureReproducibilityN/A
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.04.0 +dev / +beta1 / +beta2 
Summary0007233: Support GADT equations on non-local abstract types
DescriptionCurrently 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.
TagsNo tags attached.
Attached Files

- Relationships
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 

-  Notes
(0015817)
lpw25 (developer)
2016-04-19 18:32

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?
(0015885)
garrigue (manager)
2016-04-29 01:27

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.
(0015920)
garrigue (manager)
2016-05-12 10:13

Actually, the (rather simple) changes in GPR 0000578 have made this almost trivial.
See GPR #579 for a seemingly working implementation.
  https://github.com/ocaml/ocaml/pull/579 [^]

Anybody willing to torture it?

- Issue History
Date Modified Username Field Change
2016-04-19 18:29 lpw25 New Issue
2016-04-19 18:32 lpw25 Note Added: 0015817
2016-04-29 01:27 garrigue Note Added: 0015885
2016-05-12 10:13 garrigue Note Added: 0015920
2016-05-12 10:13 garrigue Assigned To => garrigue
2016-05-12 10:13 garrigue Status new => assigned
2016-06-03 09:59 garrigue Relationship added child of 0005998
2016-08-04 14:47 frisch Status assigned => resolved
2016-08-04 14:47 frisch Fixed in Version => 4.04.0 +dev / +beta1 / +beta2
2016-08-04 14:47 frisch Resolution open => fixed
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-09-24 17:33 xleroy Status resolved => closed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker