A good way to write an unsatisfactory constraint?

Question

I 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 HasProxyTit to restrict the default methods, so as not to loop if the type of proxy server matches itself (does not stop two instances from loops to each other by default, but you should be pretty dumb to do such a thing).

But the definition Unsatisfiableseems a little ugly? Is there a better way to determine Unsatisfiableor is this how it was done?

Answer 1

In the latest versions of GHC you can use TypeError:

import GHC.TypeLits 

type Unsatisfiable = TypeError ('Text "oops")

TypeError :

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