|Anonymous | Login | Signup for a new account||2019-02-24 02:12 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0007233||OCaml||typing||public||2016-04-19 18:29||2017-09-24 17:33|
|Target Version||Fixed in Version||4.04.0 +dev / +beta1 / +beta2|
|Summary||0007233: Support GADT equations on non-local abstract types|
|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
val eql : (t, int) eq
module F (M : S) = struct
let zero : M.t =
let Refl = M.eql in
Currently, the above is an error:
Error: This expression has type int but an expression was expected of type
Mostly such cases can be worked around by introducing a locally abstract type, but it is an unnecessary chore and can require code duplication.
|Tags||No tags attached.|
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?
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.
Actually, the (rather simple) changes in GPR 0000578 have made this almost trivial.
See GPR #579 for a seemingly working implementation.
Anybody willing to torture it?
|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|