如果没有匹配的封闭类型族实例,有没有办法获得编译时错误？

Question

我有一个封闭式的家庭,没有抓住所有情况:

{-# LANGUAGE TypeFamilies #-}

type family Foo a where
    Foo Bool = Int
    Foo Int = Bool

有没有办法强制类型检查器拒绝以下程序:

data T a = MkT deriving Show

x :: T (Foo String)
x = MkT

由于没有Foo String类型的事实？

Answer 1

从 GHC 8.0.1 开始，可以这样写：

\n\n

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}\n\nimport GHC.TypeLits\n\ntype family Foo a where\n    Foo Bool = Int\n    Foo Int  = Bool\n    Foo a    = TypeError (Text "Invalid Foo " :<>: ShowType a)\n\ndata T a = MkT deriving Show\n\nx :: T (Foo String)\nx = MkT\n

\n\n

模块可以加载，但不能使用x：

\n\n

*Main> :r\n[1 of 1] Compiling Main             ( te.hs, interpreted )\nOk, modules loaded: Main.\n*Main> x\n\n<interactive>:18:1: error:\n    \xe2\x80\xa2 Invalid Foo [Char]\n    \xe2\x80\xa2 When checking the inferred type\n        it :: T (TypeError ...)\n

\n\n

如果添加，没有类型签名

\n\n

y = id x\n

\n\n

GHC(i) 在型式检查期间抱怨时：

\n\n

te.hs:15:1: error:\n    \xe2\x80\xa2 Invalid Foo [Char]\n    \xe2\x80\xa2 When checking the inferred type\n        y :: T (TypeError ...)\n

\n\n

然而，如果你给出y一个类型：y :: T (Foo String) ; 那么 GHC 也会接受这一点。

\n\n

我不确定这是否是一个错误或功能。类型族，即使是封闭的类型族，也不能任意减少，尤其是在存在 的情况下，首先UndecidableInstances需要使用哪一个。TypeError如果类型族减少为Maybe (TypeError ...)。

\n