haskell - 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 写出来会更清楚。 ( View 模式非常模糊 WRT 类型信息流):

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

在这里，信息 f ~ Int 1 完全可以访问.好吧，但这不是我们需要这些信息的地方:我们已经在 obsFoo foof 需要它了。 .并且信息无法到达那里:GADT模式匹配充当完整的“类型信息二极管”，即任何来自外部的信息都可以在匹配范围内使用，但没有来自内部的信息不能使用。 (显然有充分的理由，因为该信息只能在运行时确认，当您实际上有一个 GADT 构造函数可以从中获取它时。)

更有趣的问题是，为什么添加 :: Foo Int 会起作用？签名？好吧，这尤其是 View 模式的怪异之处。看，以下方法不起作用:

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

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

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

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

这是完全不同的一双鞋，因为现在 Foo Int不在 GADT 模式匹配内。

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