haskell - 在使用类型系列限制 GADT 时摆脱 "non-exhaustive patten matches"警告

Question

给定以下程序:

{-# LANGUAGE DataKinds, GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Foo = A | B
type family IsA (foo :: Foo) :: Bool

type instance IsA A = True
type instance IsA B = False

data Bar (foo :: Foo) where
    BarA :: (IsA foo ~ True) => Int -> Bar foo
    BarB :: (IsA foo ~ False) => String -> Bar foo

f :: Bar A -> Int
f bar = case bar of
    BarA x -> x

使用 -fwarn-incomplete-patterns 时，我从 GHC 7.4.2 收到此警告对于总函数 f上面定义:

Warning: Pattern match(es) are non-exhaustive
         In a case alternative: Patterns not matched: BarB _

当然，即使尝试为 BarB 添加匹配项也是没有意义的。 :

Couldn't match type `'False' with `'True'
Inaccessible code in
  a pattern with constructor
    BarB :: forall (foo :: Foo). IsA foo ~ 'False => String -> Bar foo,
  in a case alternative
In the pattern: BarB _
In a case alternative: BarB _ -> undefined
In the expression:
  case bar of {
    BarA x -> x
    BarB _ -> undefined }

有没有办法让 GHC 相信 f是总数吗？另外，这是 GHC 的一个错误，还是只是一个已知的限制？或者实际上有一个很好的理由为什么无法看到 f 中的模式匹配？已经完成？

Answer 1

这很烦人，是的。 GHC 假设类型族(和类)在其算法中是开放的。但是，您正在编写由封闭类型参数化的类型族。这种紧张关系解释了你和 GHC 之间的误解。我认为已经有一些关于如何处理封闭类型类(class)和家庭的想法，但这是一个棘手的领域。

同时，您可以避免类型族的开放性以说服整体检查器。

{-# LANGUAGE DataKinds, GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Foo = A | B

data Bar (foo :: Foo) where
    BarA :: Int    -> Bar A -- or BarA :: foo ~ A => Int    -> Bar foo
    BarB :: String -> Bar B -- or BarB :: foo ~ B => String -> Bar foo

f :: Bar A -> Int
f bar = case bar of
    BarA x -> x
-- or f (BarA x) = x