How do I get a type error with GHC.TypeLits.TypeError at compile time and not at run time?
So far, I've assumed that GHC performs a type-level (family-type) function at compile time. Therefore, an error message raised by a type of type TypeError must be issued at compile time.
In the following example, I am getting a runtime type error.
{-# 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 a function, test3
evaluating a type-level function Lookup
must give a type error because baz is not a key in TList
.
GHCi loads code without error like:
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.
As a result of requesting the types of functions test1
, test2
the results are shown:
*Main> :t test1
test1 :: Int
*Main> :t test2
test2 :: [Char]
The request for the type of function test3 gives a type error and the TypeError function is only executed when trying to evaluate the function test3
:
*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 need to do to get a compile time error?
source to share
The reason for this does not cause an error when compiling your module - laziness. This is basically the same reason it print (if True then 1 else error "Mearg")
doesn't cause any problems: since the branch is else
never used, there is (provably!) So that the error expression cannot influence the result. If you do this, the error will only occur in the alternate universe.
Likewise, you will never use type information that you test3
might (well, not!) Supply. That is, you never evaluate the result Lookup "baz" TList
, not at compile time or runtime. So there is no error!
In any real program that uses such a type family, however, you would be interested in specific type information and do things like
show0 :: (Show q, Num q) => q -> String
show0 q = show $ 0`asTypeOf`q
main :: IO ()
main = putStrLn $ show0 test3
And that results in a compile-time error (for some reason, essentially twice):
sagemuej@sagemuej-X302LA:~$ ghc /tmp/wtmpf-file2798.hs
[1 of 1] Compiling Main ( /tmp/wtmpf-file2798.hs, /tmp/wtmpf-file2798.o )
/tmp/wtmpf-file2798.hs:35:19: error:
• Key not found: baz
• In the second argument of ‘($)’, namely ‘show0 test3’
In the expression: putStrLn $ show0 test3
In an equation for ‘main’: main = putStrLn $ show0 test3
|
35 | main = putStrLn $ show0 test3
| ^^^^^^^^^^^
/tmp/wtmpf-file2798.hs:35:19: error:
• Key not found: baz
• In the second argument of ‘($)’, namely ‘show0 test3’
In the expression: putStrLn $ show0 test3
In an equation for ‘main’: main = putStrLn $ show0 test3
|
35 | main = putStrLn $ show0 test3
| ^^^^^^^^^^^
source to share