GADT类型参数未用于类型类分辨率

Question

请考虑以下代码

data Foo f where
  Foo :: Foo Int

class DynFoo t where
  dynFoo :: Foo f -> Foo t

instance DynFoo Int where
  dynFoo Foo = Foo

obsFoo :: (DynFoo t) => Foo f -> Foo t
obsFoo = dynFoo

useDynFoo :: Foo f -> Int
useDynFoo (obsFoo -> Foo) = 1

模式匹配useDynFoo应限制使用obsFoo类型Foo f -> Foo Int,这应该使它搜索一个实例DynFoo Int.但是,它会搜索DynFoo t未知的实例t,并自然会失败.

  No instance for (DynFoo t0) arising from a use of ‘obsFoo’
    The type variable ‘t0’ is ambiguous

但是,如果我将定义更改useDynFoo为

useDynFoo :: Foo f -> Int
useDynFoo (obsFoo -> (Foo :: Foo Int)) = 1

然后它突然起作用,即使我的类型签名完全是多余的.

那么,为什么会发生这种情况,如何obsFoo在不必提供类型签名的情况下使用？

Answer 1

如果你用明确的方式写出来就更清楚了case（视图模式非常模糊 WRT 类型信息流）：

\n\n

useDynFoo :: Foo f -> Int\nuseDynFoo foof = case obsFoo foof of\n    Foo -> 1\n

\n\n

在这里，信息f ~ Int对于1. 嗯，但这不是我们需要此信息的地方：我们已经需要它了obsFoo foof。并且信息无法到达那里：GADT模式匹配充当完整的\xe2\x80\x9c类型信息二极管\xe2\x80\x9d，即来自外部的任何信息都可以在匹配范围内使用，但不能使用来自内部的信息可以不使用。（显然有充分的理由，因为该信息只能在运行时确认，当你实际上有一个 GADT 构造函数可以从中获取它时。）

\n\n

比较有趣的问题是，为什么加了签名还能起作用呢:: Foo Int？嗯，这尤其是视图模式的奇怪之处。看看下面的不会的：

\n\n

useDynFoo :: Foo f -> Int\nuseDynFoo foof = case obsFoo foof of\n    (Foo :: Foo Int) -> 1\n

\n\n

正如您自己所说，这些信息完全是多余的。

\n\n

然而事实证明，这种视图模式实际上相当于将签名放在案例的另一部分上：

\n\n

useDynFoo :: Foo f -> Int\nuseDynFoo foof = case obsFoo foof :: Foo Int of\n    Foo -> 1\n

\n\n

这是一双完全不同的鞋，因为现在Foo IntGADT里面的图案不匹配。

\n\n

我不知道为什么要像这样查看带有签名脱糖的模式，也许是为了使这种模式成为可能。

\n