Haskell lets you express that types unify: `a ~ b` says that `a` unifies with `b`, and similarly `Int ~ b` or `Bool ~ Char` (though the last one is clearly fals

Haskell lets you express that types unify: `a ~ b` says that `a` unifies with `b`, and similarly `Int ~ b` or `Bool ~ Char` (though the last one is clearly false). But there's no equivalent for non-unification - `a /~ b`. You can sort of hack it by asking the compiler "do these types unify right now", and then negating the response you get, but that doesn't work for types which eventually unify, but just fail to at the moment. A good example is with non-injective type functions. To show `Maybe a ~ Maybe b`, you can exploit the fact that `Maybe` is an injective type constructor to simplify the problem to deciding if `a ~ b`. But if you have an ad-hoc type function which is not injective, say `Foo`, then it's possible that `Foo a ~ Foo b` even if `a /~ b`. It's worse if you have two different type functions - `Foo a ~ Bar b`. Those types fail to unify immediately because `Foo` is definitely different to `Bar` - but depending on the final values of `a` and `b`, the types they result in may unify.