如何在Haskell中触发类型族模式匹配错误？

Question

Haskell是否能够指示类型系列匹配错误？例如,使用封闭类型系列:

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

这种类型Testf Int就是Testf Int.编译器不会生成任何类型的错误.如果没有匹配,是否可以让它生成一个？

Answer 1

不可能.良好的家庭类型应用程序从不会自行触发错误.相反,当我们尝试使用未减少的类型族表达式时,我们只会遇到类型错误.

我们可以使用包含错误消息的自定义类型,以使错误更清晰:

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"

现在,GHC抛出一个错误,因此每当我们尝试Error msg用来键入一个非未定义的值时就打印出我们的消息.

从GHC 8.0开始,我们可以用TypeError更好的方式打印我们的消息:

{-# 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")

这将打印:

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

但是,这仍然只会在使用时抛出错误:

type T = Testf Int -- this typechecks

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