解构成功的GADT记录功能失败

Question

我试图把我的头包裹在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没有存在变量,它只有一个简单的约束,它只是构造函数,但就是这样.

Answer 1

这里发生的是模式匹配

g (T x) = f x

告诉typechecker你已经满足了约束,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’