GADT and OR pattern matching

Learning
1

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.

2

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.

3

I find a similar problem with or-pattern and GADT …

4

Is there a way to workaround it?

5

Maybe someone has a PPX to expand OR branches in match with? IIRC there is an optimization step to merge case branches with the same code, so this is only affecting the power and time of type inference.