Hope this helps The brief answer is that GADTs make the type system too expressive to be fully inferred. For instance, in your case, the following functions are both total (aka they handle all possible values of their input

code :

```
let one = (One) => None
let two = (Two) => None
```

```
let one = function
| One -> None
| _ -> .
```

```
let x (type a, (x:t(a))) = switch(x){
| One => None
| Two => None
}
```

```
let x (type a) = fun
| (One:t(a)) => None
| Two => None
```

```
type t(_) =
| Int(int): t(int)
| Equal(t('a),t('a)):t(bool)
let rec eval: type any. t(any) => any = fun
| Int(n) => n
| Equal(x,y) => eval(x) = eval(y)
```

```
let zero (type a, (x:t(a)) = switch (x){
| One => 0
| Two => 0.
}
```

```
let zero (type a, (x:t(a))) = switch (x){
| One => ( 0 : a )
| Two => ( 0. : a )
}
```

```
let zero (type a): t(a) => a = fun
| One => 0
| Two => 0.
```