给定以下程序:
{-# 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
中的模式匹配?已经完成?
最佳答案
这很烦人,是的。 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
关于haskell - 在使用类型系列限制 GADT 时摆脱 "non-exhaustive patten matches"警告,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/12438909/