Support GADT equations on non-local abstract types

[vicuna]

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]

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]

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]

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?