Nested GADTs and passing equality tests as arguments

Learning
1

I’ve run into an interesting problem involving GADT equality tests and reached the limits of my understanding.

Say I have a standard simple GADT:

type _ cls = I : int cls | S : string cls

and I declare the standard equality type:

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

I can easily write a function that compares two instances of cls:

let eq_cls : type a b. a cls -> b cls -> (a,b) eq option = fun a b ->
  match a,b with
  | I, I -> Some Eq
  | S, S -> Some Eq
  | _, _ -> None

So far so good. Now I want to declare a new GADT that contains this one:

type _ nested = Cls : 'a cls -> 'a nested
              | Other : float nested

and now I want an equality test for this one:

let eq_nested : type a b. a nested -> b nested -> (a,b) eq option = fun a b ->
  match a,b with
  | Cls a, Cls b -> begin
    match eq_cls a b with
    | Some Eq -> Some Eq
    | None -> None
    end
  | Other, Other -> Some Eq
  | _, _ -> None

This works fine. What I can’t seem to do is to pass in the eq_cls as an argument to this function:

let eq_notworking : type c d. ('a cls -> 'b cls -> ('a,'b) eq option) -> c nested -> d nested -> (c,d) eq option = fun test c d ->
  match c,d with
  | Cls a, Cls b -> begin
    match test a b with
    | Some Eq -> Some Eq
    | None -> None
    end
  | Other, Other -> Some Eq
  | _, _ -> None

This version complains that

Error: This expression has type c cls but an expression was expected of type
         'a cls
       The type constructor c would escape its scope

and if instead I try to keep 'a and 'b abstract:

let eq_also_notworking : type a b c d. (a cls -> b cls -> (a,b) eq option) -> c nested -> d nested -> (c,d) eq option = fun test c d ->

it complains that:

Error: This expression has type c cls but an expression was expected of type
         a cls
       Type c is not compatible with type a

How might I be able to pass in this equality test to this function?

2 Likes
2

The root problem is the type of your function argument in eq_notworking. You probably intended to write
(∀a ∀b. a cls -> b cls->(a,b) eq option) which is not directly possible in OCaml.

There is two possibles fixes. First, since you are only using the test function with type c and d as argument, you can adjust the type of eq_notworking to

let eq_working : type c d. 
 (c cls -> d cls -> (c,d) eq option) -> c nested -> d nested
  -> (c,d) eq option = ..

The second solution, which is probably closer to your intent, is to use a record type with the right polymorphic record field:

type test = 
   { test: 'a 'b. 'a cls -> 'b cls -> ('a,'b) eq option } [@@unboxed]

let eq_working' : type c d. 
  test -> c nested -> d nested -> (c,d) eq option =
  fun {test} c d -> ...
5 Likes
3

As you guessed, the fact that I’m using c and d is just a artefact of my repro here - the second fix is exactly what I was looking for. Thanks!