How to trigger a type family pattern match error in Haskell?

Question

Is Haskell able to indicate a type family match error? For example, using a closed type family:

type family Testf a where
  Testf Char   = IO ()
  Testf String = IO ()

The type of Testf Int is just Testf Int. The compiler does not generate any kind of error. Is it possible to get it to generate one if there are no matches?

Answer 1

Not possible. Well-kinded type family applications never trigger errors by themselves. Instead, we only get type errors when we try to use unreduced type family expressions for something.

We can use custom types holding error messages, in order to make errors a bit clearer:

import GHC.TypeLits

data Error (msg :: Symbol) -- a type-level error message

type family Testf a where
  Testf Char   = IO ()
  Testf String = IO ()
  Testf x      = Error "No match for Testf"

Now, GHC throws an error and consequently prints our message whenever we try to use Error msg to type a non-undefined value.

From GHC 8.0, we can use TypeError to print our message in a nicer way:

{-# language DataKinds #-}
import GHC.TypeLits

type family Testf a where
  Testf Char   = IO ()
  Testf String = IO ()
  Testf x      = TypeError (Text "No matching case for Testf")

This would print:

Notes.hs:18:5: error: …
    • No matching case for Testf
    • In the expression: ...

However, this still only throws the error on use:

type T = Testf Int -- this typechecks

x :: T
x = () -- we throw error only here

Answer 2

This is impossible in GHCs before 8.0, but the (as of this writing) just-released GHC 8.0.1 adds support for custom type errors.

The idea is that, just like the function error :: String -> a inhabits any type with an error at the term level, we now have, in GHC.TypeLits, the type family

type family TypeError (msg :: ErrorMessage) :: k

that inhabits any type with a type error. The ErrorMessage type is very simple:

data ErrorMessage = Text     Symbol
                  | ShowType t
                  | ErrorMessage :<>: ErrorMessage
                  | ErrorMessage :$$: ErrorMessage

The (:<>:) constructor concatenates two error messages horizontally; the (:$$:) constructor concatenates them vertically. The other two constructors do what they say.

Thus, in your example, you can fill in the last case with a TypeError; for instance,

type family Testf a where
  Testf Char   = IO ()
  Testf String = IO ()
  Testf a      = TypeError (    Text "‘Testf’ didn't match"
                           :$$: Text "when applied to the type ‘"
                                :<>: ShowType a :<>: Text "’")

Then, trying to use pure () at type Testf Int will fail with the error

....hs:19:12: error: …
    • ‘Testf’ didn't match
      when applied to the type ‘Int’
    • In the expression: pure ()
      In an equation for ‘testfInt’: testfInt = pure ()
Compilation failed.

Note that while defining

testfInt :: Testf Int
testfInt = pure ()

correctly broke, defining

testfInt :: Testf Int
testfInt = undefined

(or similarly with testfInt = testfInt) worked fine.

---

Here's a full example source file:

{-# LANGUAGE UndecidableInstances, TypeFamilies, DataKinds, TypeOperators #-}

import GHC.TypeLits

type family Testf a where
  Testf Char   = IO ()
  Testf String = IO ()
  Testf a      = TypeError (    Text "‘Testf’ didn't match"
                           :$$: Text "when applied to the type ‘"
                                :<>: ShowType a :<>: Text "’")

testfChar :: Testf Char
testfChar = putStrLn "Testf Char"

testfString :: Testf Char
testfString = putStrLn "Testf String"

-- Error here!
testfInt :: Testf Int
testfInt = putStrLn "Int"