在限制带有类型族的GADT时,摆脱"非详尽的模式匹配"警告

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之间的误解.我认为已经考虑过如何处理封闭式类和家庭,但这是一个棘手的领域.

与此同时,您可以避免类型族的开放性来说服整体检查者.

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