I would like to define a GADT in one module, and deconstruct values of it in another module. For instance:

```
module A = struct
type a = A
type b = A
type _ t =
| X : a t
| Y : b t
end
module B = struct
let check : type s . s A.t -> s A.t -> bool = fun u v ->
match u, v with
| X, X -> true
| Y, Y -> false
| _ -> .
end
```

I obtain the following error message:

```
Error: This match case could not be refuted.
Here is an example of a value that would reach it: (X, Y)
```

Obviously, I don’t get this error message when `check`

is defined in the same module than `'a t`

. I still get the error when I give an explicit signature to `A`

(with exactly the same definitions than in the module structure).

Should I put more annotations to make `B.check`

type-check?