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。

什么你希望的是，因为没有办法提供一个使用Inl构造Sig B类型的值（它需要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 

恼人的，是的，但他们的休息时间。 ⊥是为什么我们不能拥有美好的事物。 ：[