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
b. The former refines them both to
int, whilst the latter —
char. The machine inferred type, as shown by the error message, for
(a, a) equal ,which is not compatible with the annotated return type
(a, b) equal, therefore the definition is rejected.
How exactly the type
(a, a) equal is inferred for
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