You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
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
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.
The text was updated successfully, but these errors were encountered: