Original bug ID: 5713
Reporter: @alainfrisch
Assigned to: @garrigue
Status: resolved (set by @Octachron on 2016-12-07T20:00:43Z)
Resolution: fixed
Priority: normal
Severity: feature
Fixed in version: 4.04.0
Category: typing
Child of: #5998
Monitored by: mbarbin @glondu @hcarty @alainfrisch

Bug description

Consider:

type 'a gadt = A: int gadt

let f (type s) =
  let _foo (x : s gadt) : s =
    match x with
    | A -> 5 (* here s == int *)
  in
  ()

This type-checks because in the context of the branch, one can use the equation s == int. Here, s is a fresh locally abstract type introduced by the (type s) syntax.

Now, consider:

module type S = sig type s end

let f (module X : S) =
  let _foo (x : X.s gadt) : X.s =
    match x with
    | A -> 5 (* here X.s == int *)
  in
  ()

Here, we have a local abstract type X.s, but it cannot be refined by opening the GADT.

We have faced this situation in real code, where we were forced to create a local polymorphic function (with explicit local abstract types) and use it immediately on a fixed type obtained by unpacking a first-class module.

Would it be possible to allow GADTs to add equations to such local abstract types introduced by module unpacking?