haskell - 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

尽管 fun 是一个详尽的匹配项，但在使用 -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 添加更多案例，如果你有很多应用这种模式的功能，那可能会很有趣(虽然简单和机械)。