So I have been learning about both type theory and GADT lately and I thought I could try to encode a constructive proof on my own with GADT. I decided to encode a proof of a version of law of excluded middle for natural integer (two integers are either equal or not equal). During the process, I got puzzled by the interaction between locally abstract types and the displayed function signature. I tried a bit to reduce the problem but I am not yet very confortable and I don’t fully understand the problem, so I give you the entire code (which is not that long anyway). Here is what I came up with :

```
type void = |
type 'a neg = 'a -> void
type ('a, 'b) either = Left of 'a | Right of 'b
type (_, _) eq = Refl: ('a, 'a) eq
type zero
type _ s = S: 'n -> 'n s
type _ nat = Z: zero nat | S: 'n nat -> 'n s nat
type ('n1, 'n2) nat_lem = (('n1 nat, 'n2 nat) eq, ('n1 nat, 'n2 nat) eq neg) either
let z_not_s: (zero nat, 'n s nat) eq -> void = function _ -> .
let s_not_z: ('n s nat, zero nat) eq -> void = function _ -> .
let prop_eq: type n1 n2. (n1 nat, n2 nat) eq -> (n1 s nat, n2 s nat) eq =
function Refl -> Refl
let backprop_eq: type n1 n2. (n1 s nat, n2 s nat) eq -> (n1 nat, n2 nat) eq =
function Refl -> Refl
let prop_neq: type n1 n2.(n1 nat, n2 nat) eq neg -> (n1 s nat, n2 s nat) eq neg
= fun n1_n2_neq n1s_n2s_eq -> n1_n2_neq (backprop_eq n1s_n2s_eq)
let propagate: type n1 n2. (n1, n2) nat_lem -> (n1 s, n2 s) nat_lem = function
| Left peq -> Left (prop_eq peq)
| Right pneq -> Right (prop_neq pneq)
let rec are_equal: type n1 n2. n1 nat -> n2 nat -> (n1, n2) nat_lem =
fun n1 n2 -> match n1, n2 with
| Z, Z -> Left Refl
| Z, S _ -> Right z_not_s
| S _, Z -> Right s_not_z
| S n1, S n2 -> propagate (are_equal n1 n2)
let () = match are_equal (S (S Z)) (S (S Z)) with
| Left _ -> print_endline "true !"
| Right _ -> print_endline "false !"
```

It works : in this case, the code prints true, and if you change the first (S (S Z)) to Z or S Z, it will print false. So I am happy with that. My first question would be : is there anything in this code that I could improve or that you would have done differently.

I have a second, more specific question : when I type the function prop_eq in utop, the type it displays is simply :

```
val prop_eq : ('n1 nat, 'n2 nat) eq -> ('n1 s nat, 'n2 s nat) eq
```

Instead of the more specific type I wrote, which is :

```
type n1 n2. (n1 nat, n2 nat) eq -> (n1 s nat, n2 s nat) eq
```

So I would tend to think that in this specific case, the typechecker has deduced that these types are equivalent. But if I change my type annotation in prop_eq with the type above (the one given by utop with more standard polymorphism), then the function propagate does not compile anymore :

```
let prop_eq: ('n1 nat, 'n2 nat) eq -> ('n1 s nat, 'n2 s nat) eq =
function Refl -> Refl
...
let propagate: type n1 n2. (n1, n2) nat_lem -> (n1 s, n2 s) nat_lem = function
| Left peq -> Left (prop_eq peq)
| Right pneq -> Right (prop_neq pneq)
```

Line 2, characters 30-33:

Error: This expression has type (n1 nat, n2 nat) eq

but an expression was expected of type (n1 nat, n1 nat) eq

Type n2 is not compatible with type n1

The error does not help me much. So it seems that these two types are indeed different, even in my specific case. My question is then : why are they printed the same way in toplevel ? Is it the intended behaviour or just some small mistake waiting to be fixed ? I also know that you can’t specify explicit polymorphism or locally abstract types in module signatures, is this related ? If I do the same thing with prop_neq or backprop_eq, the same error arises.

If you could also take this occasion to re-explain the subtleties between locally abstract types, explicit polymorphism and the combination of both, that could also help me. For example, why do I need to use locally abstract type in my example. By doing the exercises on gadt I finally got a kind of instinct of which one to use in which case but it is still not clear for me, and I have yet to find a case where I should use the form with only locally abstract type - this one :

```
let f = fun (type t) (foo : t list) -> …
```

Instead of this one (with explicit polymorphism):

```
let f : type t. t list -> ... = fun foo -> …
```

Thank you in advance !