如何在编译时而不是在 运行 时出现 GHC.TypeLits.TypeError 类型错误？
How to get with GHC.TypeLits.TypeError a type error at compile time and not at run-time?
到目前为止，我假设 GHC 在编译时执行类型级函数（类型系列）。因此，应该在编译时发出由 TypeError 类型族触发的错误消息。
在下面的例子中，我在 运行 次得到类型错误。
{-# 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
对于函数 test3 类型级函数 Lookup 的评估应该给出类型错误，因为 baz 不是 TList.
GHCi 加载代码时没有类型错误：
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.
查询函数类型test1，test2得到预期结果：
*Main> :t test1
test1 :: Int
*Main> :t test2
test2 :: [Char]
查询函数 test3 的类型给出了类型错误，TypeError 函数仅在我尝试评估 test3 函数时执行：
*Main> :t test3
test3 :: (TypeError ...)
*Main> test3
<interactive>:5:1: error:
• Key not found: baz
• When checking the inferred type
it :: (TypeError ...)
我必须做什么才能得到编译时错误？
这在编译模块时不会导致错误的原因是懒惰。这与 print (if True then 1 else error "Mearg") 不会导致任何问题的原因基本相同：因为 else 分支实际上从未 使用 ，所以（可证明！）不可能错误的表达可能会影响结果。如果你愿意，错误只会发生在另一个宇宙中。
同样，您永远不会使用 test3 可以（嗯，不是！）提供的类型信息。 IE。您永远不会评估 Lookup "baz" TList 结果，无论是在编译时还是在运行时。所以没有报错！
在任何使用此类类型族的实际程序中，您会但是对具体的类型信息感兴趣，并且会做类似
的事情
show0 :: (Show q, Num q) => q -> String
show0 q = show $ 0`asTypeOf`q
main :: IO ()
main = putStrLn $ show0 test3
这确实会导致编译时错误（实际上是两次，出于某种原因）：
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
| ^^^^^^^^^^^
到目前为止，我假设 GHC 在编译时执行类型级函数（类型系列）。因此，应该在编译时发出由 TypeError 类型族触发的错误消息。
在下面的例子中，我在 运行 次得到类型错误。
{-# 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
对于函数 test3 类型级函数 Lookup 的评估应该给出类型错误，因为 baz 不是 TList.
GHCi 加载代码时没有类型错误：
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.
查询函数类型test1，test2得到预期结果：
*Main> :t test1
test1 :: Int
*Main> :t test2
test2 :: [Char]
查询函数 test3 的类型给出了类型错误，TypeError 函数仅在我尝试评估 test3 函数时执行：
*Main> :t test3
test3 :: (TypeError ...)
*Main> test3
<interactive>:5:1: error:
• Key not found: baz
• When checking the inferred type
it :: (TypeError ...)
我必须做什么才能得到编译时错误？
这在编译模块时不会导致错误的原因是懒惰。这与 print (if True then 1 else error "Mearg") 不会导致任何问题的原因基本相同：因为 else 分支实际上从未 使用 ，所以（可证明！）不可能错误的表达可能会影响结果。如果你愿意，错误只会发生在另一个宇宙中。
同样，您永远不会使用 test3 可以（嗯，不是！）提供的类型信息。 IE。您永远不会评估 Lookup "baz" TList 结果，无论是在编译时还是在运行时。所以没有报错！
在任何使用此类类型族的实际程序中，您会但是对具体的类型信息感兴趣，并且会做类似
的事情show0 :: (Show q, Num q) => q -> String
show0 q = show $ 0`asTypeOf`q
main :: IO ()
main = putStrLn $ show0 test3
这确实会导致编译时错误（实际上是两次，出于某种原因）：
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
| ^^^^^^^^^^^