GADT and OR pattern matching

Hi everyone. I have noticed a very strange behaviour for GADTs when using pattern matching. Consider the following type and function :

type _ t =
  | A : int t
  | B : int t
  | C : char t

let f : type a. a t -> (a -> string) = function
  | A -> string_of_int
  | B -> string_of_int
  | C -> String.make 1

Then the function works and it compiles. However, when combining the match cases of the same type for a syntactic sugar purpose…

let g : type a. a t -> (a -> string) = function
  | A | B -> string_of_int
  | C     -> String.make 1

… I’m getting this error :

Error: This pattern matches values of type int t
       but a pattern was expected which matches values of type a t
       Type int is not compatible with type a 

I’m using OCaml 4.07.0. Is that a known bug for this OCaml version, or is it something normal coming from the GADT type system that is a bit different from the classic one ? Thanks for explanations.

In OCaml 4.07, you can’t use GADTs in or-patterns.

In OCaml 4.08 you can use GADTs in some or-patterns, but you can’t make use of type equations introduced by or-patterns (in your case, the equation a = int), so unfortunately your specific example still won’t compile.