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?