haskell - 如何在 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