Patterning matching with *or-pattern*, *locally abstract types* and *GADT* has some curious semantics.

Consider the code below , which is a standard implementation of type witness and equality witness, with an additional problematic implementation that simply tries to merge two similar branches of pattern matching into a single branch using an or-pattern. The two parts of the or-pattern: `(Int, Int)`

and `(Char, Char)`

make incompatible refinements for the locally abstract types `a`

and `b`

. The former refines them both to `int`

, whilst the latter â€” `char`

. The machine inferred type, as shown by the error message, for `Refl`

is `(a, a) equal`

,which is not compatible with the annotated return type `(a, b) equal`

, therefore the definition is rejected.

The question:

How exactly the type `(a, a) equal`

is inferred for `Refl`

?

My own answer to question 1: Start with the result `('c, 'c) `

of anti-unification of the tuples `(int, int)`

and `(char, char)`

, followed by a conversion from free type variable to abstract type: `('c, 'c) -->> (a, a)`

. But why `a`

? Why not `b`

nor a fresh locally abstract type? Why the unnecessary conversion `('c, 'c) -->> (a, a)`

?

I am also wondering where can I find from the ocaml source, about code that implements pattern matching and locally abstract types?

```
module Ty : sig
type _ t = Int : int t | Char : char t
type (_, _) equal = Refl : ('a, 'a) equal
val ty_equal : 'a t -> 'b t -> ('a, 'b) equal option
end = struct
type _ t = | Int : int t
| Char : char t
type (_, _) equal = Refl : ('a, 'a) equal
let ty_equal (type a b) (a : a t) (b : b t) : (a, b) equal option
= match a , b with
| Int , Int -> Some Refl
| Char, Char -> Some Refl
| _, _ -> None
module Problem = struct
let ty_equal (type a b) (a : a t) (b : b t) : (a, b) equal option
= match a , b with
| (Int , Int) | (Char, Char) -> Some Refl
| _, _ -> None
end
end
```