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.