Comparing extensible variant type witnesses

Learning
1

With a GADT of type witnesses, it is possible to write a function that tests for type equality:

type (_, _) eq = Refl : ('a, 'a) eq

type _ ty = Int : int ty | String : string ty

let teq : type a b. a ty -> b ty -> (a, b) eq option =
 fun x y -> match (x, y) with
 | Int, Int -> Some Refl
 | String, String -> Some Refl
 | _, _ -> None

Is it possible to do something similar if ty is an extensible variant, so that a user of the library can define their own types that can then be compared for equality? Of course there are limits on what sort of constructors a user could add and expect things to still work, e.g. if the user says

type _ ty += Any : 'a ty

then I don’t expect there’s going to be any way to extend teq to deal with those. But if the user restricts themselves to simple constructors like Int and String, or perhaps parametrized ones for type formers like

type _ ty +=
  | List : 'a ty -> 'a list ty
  | Prod: 'a ty * 'b ty -> ('a * 'b) ty

can anything be done?

I can think of two possibilities so far. One is to maintain a function like teq, or a list of them, in a mutable global variable, so that when users add constructors to ty they can “add clauses” to the match statement by adding new functions to this variable. This would be extra boilerplate for the user, but it would also exclude mistakes like Any since it wouldn’t be possible to write the corresponding clause. (Although it might require some cleverness to make this “extensible function” recursive enough to deal with List and Prod.)

The other possibility I wonder about is

type wrap = Wrap : 'a -> wrap

let teq : type a b. a ty -> b ty -> (a, b) eq option =
 fun x y -> if Wrap x = Wrap y then Some (Obj.magic Refl) else None

On a previous question I learned that comparing elements of wrap for “structural equality” doesn’t see the types. But according to my current understanding, it seems that this comparison would still do the right thing on constructors such as Int, String, List, and Prod, since the type is reified in the constructors. Of course it would be wrong in the presence of a constructor like Any, in which case the Obj.magic would be actually ill-typed and cause all sorts of mayhem, so this is probably a Bad Idea in general. But in the interests of improving my understanding of OCaml, I’m curious whether this would at least work in the case when all constructors of ty are “good” ones.

2

Types are never reified in constructors.

Structural equality only compares blocks and immediate values, which for simple types is a sufficient notion of equality.

Your Obj.magic version misbehaves as soon as two types may contain a block with the same tag or in presence of unboxed type. For instance Wrap [1] = Wrap (1,0).

In other words, Obj.magic is not part of the OCaml language: it should be seen as a tool for using OCaml as a compilation target from a more strongly typed language.

3

What I meant by “types are reified in constructors” is that the type int in int ty is represented by the constructor Int, and so on – the reification happens not at the language level, but by the user in the definition of the particular constructors. I don’t see how Wrap [1] = Wrap (1,0) is relevant, since I’m not applying Wrap to lists or pairs, only to elements of 'a ty for different values of 'a. Is there an example where it misbehaves using only the constructors Int, String, List, and Prod?

4

Sorry I read too fast. So yes, polymorphic comparison works fine within the same type because each constructor needs to be distinguishable from all others. With Int, String, List a,nd Prod, Obj.safe should be safe since each value maps to a single type with no type variables.