**tl;dr:** Abstract types already give you the guarantee that you wonâ€™t accidentally unify the two types.

To encode negation, the trick is to use the formulation `forall X, something_wrong -> X`

which translates to â€śif you can construct a wrong term, then it implies I can deduce anything from itâ€ť (including more wrong stuff since I can choose what `X`

stands for)

For example, to prove that the type `int`

and `string`

are incompatible, we can write:

```
type ('s, 't) eq = Refl : ('a, 'a) eq (* type 's and 't are equal, since 's='a and 't='a *)
let impossible : type x. (int, string) eq -> x
= function
_ (* Any _ constructor representing the equality int=string *)
-> . (* should be rejected statically by the typechecker as impossible *)
```

(The dot `.`

is special notation to indicate an impossible pattern matching)

The fact that we can define `impossible`

this way is a proof that `int <> string`

. If you try the same code with unifiable types, the typechecker will complain:

```
let possible : type x. (int, Int.t) eq -> x = function _ -> .
(* Error: This match case could not be refuted.
Here is an example of a value that would reach it: Refl *)
```

But this approach will not work if your types are abstract! (as mentionned by @sim642) Itâ€™s possible for types to be equal behind the scene, and for that equality to still be accessible indirectly:

```
module Test : sig
module A : sig type t end
module B : sig type t end
val eq_ab : (A.t, B.t) eq
end = struct
module A = struct type t = string end
module B = struct type t = A.t end
let eq_ab = Refl (* at this point, we still have knowledge of the defintion of [A.t] and [B.t] *)
end
open Test
let not_eq_ab : type x. (A.t, B.t) eq -> x = function _ -> .
(* Error: This match case could not be refuted.
Here is an example of a value that would reach it: Refl *)
```

If the typechecker accepted the definition of `not_eq_ab`

, then we would run into problems since `not_eq_ab eq_ab`

is actually possible! Sure, the types `A.t`

and `B.t`

are abstracted and hence not unifiable directly anymoreâ€¦ but we can locally reveal their equality by using `eq_ab`

:

```
let b_of_a : A.t -> B.t = fun a -> a (* error! *)
let b_of_a : A.t -> B.t = fun a -> match eq_ab with Refl -> a (* ok! *)
```

In any case, abstract types are actually the way to go to ensure that you wonâ€™t confuse similar types in your function calls: they do give you the guarantee that the types will not unify out of the box (since you would have to work hard to un-erase the abstraction!) â€¦ and so in practice we donâ€™t need to spend time trying to double-check what the typechecker will accept to unify