Locally Abstract Types in an Or-pattern with a GADT Scrutinee: Clash during Refinement?

[YueLiPicasso]

Perhaps the rule-of-thumb for a casual GADT user is just to avoid using or-patterns.

I had a look at the discussions on GitHub (link below) regarding this issue, and could see that there are indeed implementation-related intricacies yet to be resolved.

It is surprising that such a seemingly / intuitively simple problem could have such challenging technical implications.

GADT and OR pattern matching

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.