Nice way to write an unsatisfiable constraint?

Question

I've found myself writing this:

data T1
data T2

type Unsatisfiable = T1 ~ T2

So I can do something like this:

type family NEq t1 t2 :: Constraint where
  NEq t t = Unsatisfiable
  NEq _ _ = ()

type HasProxyT t = NEq t (ProxyT t)

Then I can use HasProxyT to restrict default methods to not loop if the proxy type is the same as themselves (doesn't stop two instances from looping to each other's default methods, but you'd have to be pretty stupid to do such a thing).

But the definition of Unsatisfiable seems a bit ugly? Is there a nicer way of defining Unsatisfiable or is this just the way it's done?

Answer 1

On recent versions of GHC you can use TypeError:

import GHC.TypeLits 

type Unsatisfiable = TypeError ('Text "oops")

However, I recommend you just use TypeError directly at use sites and give a custom error message:

type family NEq t1 t2 :: Constraint where
  NEq t t = TypeError ('Text "Expected a type distinct from " ':<>: 'ShowType t)
  NEq _ _ = ()