Original bug ID: 7074
Reporter: @garrigue
Assigned to: @garrigue
Status: assigned (set by @garrigue on 2015-12-04T01:38:20Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.02.3
Target version: later
Category: typing
Has duplicate: #5867
Related to: #5780
Child of: #5998
Monitored by: @gasche @diml "Julien Signoles" @yallop @hcarty @alainfrisch

Bug description

When you do pattern-matching on GADTs, new existential variables may be introduced in the environment, either by refining existing locally abstract types, or because the constructor contains some existential variables. One cannot give them a name: they are incompatible with any existing existential variable, and using a normal type variable name causes a scope extrusion.

One often wants to introduce type annotations just for readability, but in some cases they are even required for typing.

There has been already a lengthy discussion in #5780 on what kind of syntax could be used to do that, but no conclusion yet. Let's move the discussion here.

Steps to reproduce

type zero = Zero
type 'a succ = Succ of 'a
type _ nat =
  | NZ : zero nat
  | NS : 'a nat -> 'a succ nat

type (_,_) equal = Eq : ('a,'a) equal

let rec compare : type m n. m nat -> n nat -> (m,n) equal option = fun m n ->
  match m, n with
  | NZ, NZ -> Some Eq
  | NS m', NS n' -> (match compare m' n' with Some Eq -> Some Eq | None -> None)
  | _ -> None

(* There is no way to write a type annotation on m' or n' in the above function *)

Additional information

(* The following workaround does work, but it is verbose, introduces some eta-expansion,
    and forgets some local equalities (i.e., one cannot write (m,n) equal option) *)

let rec compare : type m n. m nat -> n nat -> (m,n) equal option = fun m n ->
  match m, n with
  | NZ, NZ -> Some Eq
  | NS m', NS n' ->
     let cmp : type m' n'. m' nat -> n' nat -> (m' succ,n' succ) equal option = fun m' n' ->
        match compare m' n' with Some Eq -> Some Eq | None -> None
     in cmp m' n'
  | _ -> None