Till now, I assumed, that GHC executes a type level function (type-family) at compile time. Therefore an error message triggered by the TypeError type-family should be issued at compile-time.
In the following example, I get the type error at run time.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeLits
type family If c t e where
If 'True t e = t
If 'False t e = e
type family EqSymbol (a :: Symbol) (b :: Symbol) where
EqSymbol a a = 'True
EqSymbol a b = 'False
type family Lookup (x :: Symbol) (l :: [(Symbol,t)]) :: t where
Lookup k '[] = TypeError (Text "Key not found: " :<>: Text k)
Lookup k ('(x,a) ': ls) = If (EqSymbol k x) a (Lookup k ls)
type TList = '[ '("foo", Int), '("bar", String)]
test1 :: Lookup "foo" TList
test1 = undefined
test2 :: Lookup "bar" TList
test2 = undefined
test3 :: Lookup "baz" TList
test3 = undefined
For the function test3 the evaluation of the type-level function Lookup should give a type error, because baz is not a key in TList.
GHCi loads the code without a type-error:
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Prelude> :l SO.hs
[1 of 1] Compiling Main ( SO.hs, interpreted )
Ok, modules loaded: Main.
Querying the types of the functions test1, test2 gives the exepected results:
*Main> :t test1
test1 :: Int
*Main> :t test2
test2 :: [Char]
Querying the type of the function test3 gives a type error and the TypeError function is only executed when I try to evaluate the test3 function:
*Main> :t test3
test3 :: (TypeError ...)
*Main> test3
<interactive>:5:1: error:
• Key not found: baz
• When checking the inferred type
it :: (TypeError ...)
What do I have to do, to get a compile-time error?