Elimination by `TypeError` constraint

Question

I'd like to use a TypeError constraint to make a "non-instance" produce a more meaningful type error:

{-# LANGUAGE DataKinds, KindSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

import GHC.TypeLits
import Data.Proxy

class Compat (x :: Bool) (y :: Bool) where
    combine :: Proxy x -> Proxy y -> Int

instance Compat False pre2 where
    combine _ _ = 42

instance Compat True False where
    combine _ _ = 1

instance (TypeError (Text "Meaningful error message goes here")) => Compat True True where
    combine = _

At the hole, I'd like to fill it using elimination by the TypeError constraint, i.e. use the fact that I have a TypeError constraint in scope to avoid having to write undefined or error or similar.

Is that possible?

Answer 1

I don't think this is possible with the standard TypeError, but you can define your own variant (TE below) so to provide the eliminator you need.

{-# LANGUAGE 
   DataKinds, UndecidableInstances,
   MultiParamTypeClasses, KindSignatures, TypeFamilies #-}

import GHC.TypeLits
import Data.Kind

class Impossible where
    impossible :: a

type family TE (t :: ErrorMessage) :: Constraint where
  TE t = (TypeError t, Impossible)

class C t where
   foo :: t -> Bool
   
instance (TE (Text "impossible")) => C Bool where
   foo _ = impossible