# Unexpected GADT behavior when wrapping a type into a module

**URL:** <https://discuss.ocaml.org/t/unexpected-gadt-behavior-when-wrapping-a-type-into-a-module/5707>\
**Category:** Learning\
**Created:** [May 5, 2020, 1:47am UTC](https://discuss.ocaml.org/t/unexpected-gadt-behavior-when-wrapping-a-type-into-a-module/5707 "2020-05-05T01:47:52Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![Jonathan](https://avatars.discourse-cdn.com/v4/letter/j/aeb1de/32.png) [@Jonathan](https://discuss.ocaml.org/u/Jonathan)\
**Post date:** [May 5, 2020, 1:47am UTC](https://discuss.ocaml.org/t/unexpected-gadt-behavior-when-wrapping-a-type-into-a-module/5707/1 "2020-05-05T01:47:52Z")

</div>

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).

```ocaml
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:

```auto
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:

```auto
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

---

<div class="post-metadata">

**Author:** ![gasche](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/gasche/32/4_2.png) [@gasche](https://discuss.ocaml.org/u/gasche)\
**Post date:** [May 5, 2020, 6:08am UTC](https://discuss.ocaml.org/t/unexpected-gadt-behavior-when-wrapping-a-type-into-a-module/5707/2 "2020-05-05T06:08:29Z")

</div>

`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

```ocaml
type unary = Unary
type binary = Binary

```

---

<div class="post-metadata">

**Author:** ![yallop](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/yallop/32/517_2.png) [@yallop](https://discuss.ocaml.org/u/yallop)\
**Post date:** [May 5, 2020, 7:21am UTC](https://discuss.ocaml.org/t/unexpected-gadt-behavior-when-wrapping-a-type-into-a-module/5707/3 "2020-05-05T07:21:53Z")

</div>

> [@Jonathan](#):
>
> I was playing with GADTs and encountered a pretty surprising behavior.

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

> <https://github.com/ocaml/ocaml/pull/8900>
>
> The type-checker treats abstract type definitions in the current specially:
> 
> \`…\`\`ocaml
> \# type (\_, \_) eq = Refl : ('a, 'a) eq;;
>     
> \# module M = struct
> type a
> type b
> let absurd : 'a. (a, b) eq -\> 'a = function \_ -\> .
> end;;
> module M : sig type a type b val absurd : (a, b) eq -\> 'a end
> 
> \# module M = struct
> module N = struct
> type a
> type b
> end
> let absurd : 'a. (N.a, N.b) eq -\> 'a = function \_ -\> .
> end;;
> Line 6, characters 54-55:
> 6 | let absurd : 'a. (N.a, N.b) eq -\> 'a = function \_ -\> .
> ^
> Error: This match case could not be refuted.
> Here is an example of a value that would reach it: Refl
> \`\`\`
> In my experience this special treatment confuses people a lot and is not really useful for anything.
> 
> This PR removes the special treatment. This is not a backwards compatible change so it could probably use some testing on opam.

---

<div class="post-metadata">

**Author:** ![Levi\_Roth](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/levi_roth/32/2268_2.png) [@Levi\_Roth](https://discuss.ocaml.org/u/Levi_Roth)\
**Post date:** [May 11, 2020, 1:49pm UTC](https://discuss.ocaml.org/t/unexpected-gadt-behavior-when-wrapping-a-type-into-a-module/5707/4 "2020-05-11T13:49:08Z")

</div>

> [@gasche](#):
>
> `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.

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