Unexpected GADT behavior when wrapping a type into a module

Learning
1

Hi everyone,
I was playing with GADTs and encountered a pretty surprising behavior. Here is a minimal working example.

The code below compiles without any warning or error (as expected).

type unary
type binary

type ('n, 'a) tuple =
  | Unary: 'a -> (unary, 'a) tuple
  | Binary: 'a * 'a -> (binary, 'a) tuple

type 'sz op =
  | Neg: unary op
  | Plus: binary op

let eval_op: type sz. sz op -> (sz, int) tuple -> int =
  fun op args ->
  match op, args with
    | Neg, Unary x -> -x
    | Plus, Binary (x, y) -> x + y

However, if I put the tuple type in its own module, leaving all the rest unchanged:

module Tuple = struct
  type unary
  type binary
  type ('n, 'a) t =
    | Unary: 'a -> (unary, 'a) t
    | Binary: 'a * 'a -> (binary, 'a) t
end

type 'sz op =
  | Neg: Tuple.unary op
  | Plus: Tuple.binary op

let eval_op: type sz. sz op -> (sz, int) Tuple.t -> int =
  fun op args ->
  match op, args with
    | Neg, Tuple.Unary x -> -x
    | Plus, Tuple.Binary (x, y) -> x + y

Then I get the following warning:

File "snippets/gadts_bug.ml", lines 15-17, characters 2-40:
15 | ..match op, args with
16 |     | Neg, Tuple.Unary x -> -x
17 |     | Plus, Tuple.Binary (x, y) -> x + y
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
(Plus, Unary _)

This is pretty surprising to me as I think the two code snippets above should be equivalent.
Am I missing something?

Edit: I am using Ocaml 4.10+flambda.

Best,
Jonathan

2

type foo (no declaration) in an implementation creates a type that is assumed distinct from all others. In an interface it just means that the type is abstract (its definition is hidden), so it may be equal to other types; in particular, unary and binary are not known to be distinct anymore.

Use

type unary = Unary
type binary = Binary
2 Likes
3

It is surprising, and there’s a proposal to change it:

3 Likes
4

Part of what’s surprising, I think, is that Tuple has an implicit interface.