TypeError is fragile

Consider this use of the new TypeError feature,

{-# LANGUAGE TypeInType, TypeFamilies, UndecidableInstances #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind
import GHC.TypeLits (TypeError, ErrorMessage(..))

type family Resolve (t :: Type -> Type) :: Type -> Type where
  Resolve _ = TypeError (Text "ERROR")

The okay case

Given something like,

testOK :: Resolve [] Int
testOK = []

we find that things work as expected,

    • ERROR
    • In the expression: [] :: Resolve [] Int
      In an equation for ‘testOK’: testOK = [] :: Resolve [] Int

The bad case

However, it is very easy to fool GHC into not yielding the desired error message. For instance,

testNOTOK1 :: Resolve [] Int
testNOTOK1 = ()

gives us this a unification error,

  • Couldn't match type ‘()’ with ‘(TypeError ...)’
    Expected type: Resolve [] Int
      Actual type: ()

This clearly isn't what we expected.

The tricky case

Another way we can fool the typechecker is to make it attempt instance resolution on our TypeError,

testNOTOK2 :: Resolve [] Int
testNOTOK2 = 1

Which results in,

  • No instance for (Num (TypeError ...))
      arising from the literal ‘1’
  • In the expression: 1
    In an equation for ‘testNOTOK2’: testNOTOK2 = 1