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 