GADTs and modules

Learning
1

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?

2

It seems that renaming the constructor for b so it doesn’t collide with
the one for a works around the issue

Gaëtan Gilbert

3

Thanks you very much for your quick answer, Gaëtan! Since the constructors were there only for injectivity, I didn’t even try to change their names. It solves my immediate problem, thanks again.

Anyway, it seems a bit inconsistent that these definitions are accepted as I wrote them initially when they are made in the same module and rejected if they are in distinct modules. If somebody can confirm me that it is probably a bug, I would be happy to report it.

4

This is known difference of behaviour. The problem is that the typechecker cannot distinguish your example from the following case:

module A: sig
  type a = A
  type b = A
  type _ t =
    | X : a t
    | Y : b t
   val magic: a t
end  
= struct
  type a = A
  type b = a = A
  type _ t =
    | X : a t
    | Y : b t
  let magic = Y
end

let check : type s . s A.t -> s A.t -> bool = fun u v ->
  match u, v with
  | X, X -> true
  | Y, Y -> false
  | _ -> assert false
 let fail =  check (A.magic) X

Here, we defined a value Y: a t which is impossible to build outside of A, and makes check fails.
To be able to discard this possibility the type checker needs to be able to prove that A.a and A.b are distinct. Renaming the constructor of A.b is one way to make it clear that A.b ≠ A.a and avoid the issue, as suggested by @SkySkimmer .

At some point, it was discussed if this discrepancy should be removed. However, the straightforwad way to do so would be to remove the special casing for types defined in the same modules and make the module-less code fails in the same way that your code example.

2 Likes
5

Thank you very much for your explanation! I didn’t think about this possibility of hiding an aliasing: thanks for having made it clear.

6

May I ask what is the . in _ -> . for?

7

This is a refutation case, which is essentially an assertion to the compiler that the unspecified pattern-matching cases are impossible. The compiler then checks exhaustivity, sometimes trying harder than without the refutation case.

1 Like