GADT的失败全面性检查

Question

考虑下面的代码：

data (:+:) f g a = Inl (f a) | Inr (g a)

data A
data B

data Foo l where
  Foo :: Foo A

data Bar l where
  Bar :: Bar B

type Sig = Foo :+: Bar

fun :: Sig B -> Int
fun (Inr Bar) = 1

虽然好玩的是一个详尽的比赛，与-Wall编译时，GHC抱怨缺少的情况。但是，如果我添加另一个构造函数：

data (:+:) f g a = Inl (f a) | Inr (g a)

data A
data B

data Foo l where
  Foo :: Foo A
  Baz :: Foo B

data Bar l where
  Bar :: Bar B

type Sig = Foo :+: Bar

fun :: Sig B -> Int
fun (Inr Bar) = 1
fun (Inl Baz) = 2

然后，GHC正确地检测到的乐趣是总。

我使用类似下面的代码在我的工作，并希望GHC提出警告，如果我有遗漏的情况下，并没有提高警告，如果我不知道。为什么GHC抱怨的第一个程序，我怎么能得到第一个样品没有出现警告编译无需添加虚假构造或案例？

Answer 1

实际报告的问题是：

Warning: Pattern match(es) are non-exhaustive
         In an equation for `fun': Patterns not matched: Inl _

这是真的。您提供的Inr构造的情况下，但不是Inl构造。

什么你希望的是，因为没有办法提供一个使用Sig B构造类型Inl的值（它需要类型Foo B的说法，但对于Foo唯一的构造函数的类型Foo A的），即GHC会发现，你不需要处理Inl构造。

麻烦的是，由于底部每一种类型的有人居住。有迹象表明，使用Sig B构造类型Inl的值;甚至还有一些非谷值。它们必须包含底部，但它们本身并不是底部。因此，它是可能的方案是评估呼叫fun失败匹配;这就是GHC警告有关。

因此，要解决这个问题，你需要fun更改为这样的事情：

fun :: Sig B -> Int
fun (Inr Bar) = 1
fun (Inl foo) = error "whoops"

但现在，当然，如果你在以后添加Baz :: Foo B此功能是一个定时炸弹等待发生。这是很好的GHC警告有关，但要做到这一点的唯一方法是模式匹配foo针对当前详尽的一套模式。不幸的是，你可以把有没有有效的模式！ foo是已知的类型Foo B，其仅由底部无人居住，并且也可以不写为底的图案。

但是你可以把它传递给接受多态型Foo a的参数的函数。然后，该功能可以匹配对所有当前存在的Foo构造函数，这样你会得到一个警告，如果你以后再添加。事情是这样的：

fun :: Sig B -> Int
fun (Inr Bar) = 1
fun (Inl foo) = errorFoo foo
    where 
        errorFoo :: Foo a -> b
        errorFoo Foo = error "whoops"

现在，您已经妥善处理:+:的所有构造函数中fun，“不可能”的情况下简单的错误了，如果曾经实际发生它，如果你曾经添加Baz :: Foo B你得到一个关于非详尽的格局errorFoo，这至少是警告指导你看fun因为它是一个附加的where定义。

不利的一面，当你添加无关的构造函数来Foo（说更多类型Foo A的），你就必须添加更多的情况下errorFoo，这可能是unfun（虽然简单，机械的），如果你有很多的应用此功能图案。

Answer 2

我很遗憾地告诉你，但你的第一个例子是不是很详尽，你认为它是：

∀x. x ⊢ fun (Inl (undefined :: Foo B))
*** Exception: Test.hs:48:1-17: Non-exhaustive patterns in function fun

恼人的，是的，但他们的休息时间。 ⊥就是为什么我们不能有好东西。 ：[

Answer 3

前面已经提到。你是不是办案是Inl _|_，这本身不是_|_，因而必须进行处理。

幸运的是完全很好的处理是这样的：

data (:+:) f g a = Inl (f a) | Inr (g a)

data A
data B

data Foo l where
  Foo :: Foo A
  Baz :: Foo B

data Bar l where
  Bar :: Bar B

type Sig = Foo :+: Bar

fun :: Sig B -> Int
fun (Inr Bar) = 1
fun (Inl x) = case x of {}

现在，如果你在Baz :: Foo B构造函数添加，你会得到适当的：

    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: Baz
   |
21 | fun (Inl x) = case x of {}
   |               ^^^^

因此，你可以在适当的代码更改为类似你的第二个例子，妥善处理已创建的新情况。