haskell - 解构成功的地方GADT记录功能失败

我正在尝试围绕GADT进行检查，我怀疑有些魔术正在发生，我不理解。

考虑以下：

class C t

data T a where
  T :: (C a) => { getT :: a } -> T a

f :: C a => a -> ()
f = undefined

class D t where
  g :: t a -> ()

instance D T where
  g (T x) = f x

这一切都很好，并且可以成功编译。

现在考虑T的实例定义稍有不同：

instance D T where
  g x = f (getT x)

看起来和上面完全一样，但是有一个编译错误。这里发生了什么事？数据类型T没有存在变量，它确实有一个简单的约束，因为它只是构造函数，仅此而已。

最佳答案

这里发生的是模式匹配

g (T x) = f x

告诉类型检查器您已满足约束C a，因此可以使用f。没有模式匹配，您永远不会引入C a，因此它不能满足约束。

它的工作方式是，值T something :: T a还包含C a的字典，并在T上进行模式匹配时使其可用。但是，使用getT并不能为您提供C a词典的任何方式（从getT :: T a -> a的类型可以看到）。



对于后代，错误是

• No instance for (C a) arising from a use of ‘f’
  Possible fix:
    add (C a) to the context of
      the type signature for:
        g :: T a -> ()
• In the expression: f (getT x)
  In an equation for ‘g’: g x = f (getT x)
  In the instance declaration for ‘D T’