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

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 开始，可以编写:

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}

import GHC.TypeLits

type family Foo a where
    Foo Bool = Int
    Foo Int  = Bool
    Foo a    = TypeError (Text "Invalid Foo " :<>: ShowType a)

data T a = MkT deriving Show

x :: T (Foo String)
x = MkT

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

*Main> :r
[1 of 1] Compiling Main             ( te.hs, interpreted )
Ok, modules loaded: Main.
*Main> x

<interactive>:18:1: error:
    • Invalid Foo [Char]
    • When checking the inferred type
        it :: T (TypeError ...)

如果添加，没有类型签名

y = id x

GHC(i) 在类型检查期间提示:

te.hs:15:1: error:
    • Invalid Foo [Char]
    • When checking the inferred type
        y :: T (TypeError ...)

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

我不确定这是错误还是功能。类型族，即使是封闭的，也不能任意减少，尤其是在存在 UndecidableInstances 的情况下，需要使用哪个 TypeError首先。如果类型族减少到 Maybe (TypeError ...)，甚至像 whnf 这样的东西可能还不够。 .