这个涉及反射的神秘的Haskell类型错误的原因是什么？

Question

我在使用Haskell反射包时，遇到了一个我不完全理解的类型错误。首先，我尝试编写以下函数，它可以轻松地打字：

{-# LANGUAGE TypeApplications #-}

reifyGood :: (forall s. Reifies s a => Proxy a) -> ()
reifyGood p = reify undefined (\(_ :: Proxy t) -> p @t `seq` ())

reifyBad :: (forall s. Reifies s s => Proxy s) -> ()
reifyBad p = reify undefined (\(_ :: Proxy t) -> p @t `seq` ())

• Could not deduce (Reifies s s) arising from a use of ‘p’
  from the context: Reifies s a0
    bound by a type expected by the context:
               Reifies s a0 => Proxy s -> ()
• In the first argument of ‘seq’, namely ‘p @t’
  In the expression: p @t `seq` ()
  In the second argument of ‘reify’, namely
    ‘(\ (_ :: Proxy t) -> p @t `seq` ())’

reifyGood :: (forall s. Reifies s a => Proxy a) -> ()
reifyBad  :: (forall s. Reifies s s => Proxy s) -> ()

我觉得这很奇怪。乍一看，这是无效的，因为在第二个示例中，skolems将会逃避它的作用域。然而，这实际上不是真的--错误消息从未提到skolem escape，与这个略有不同的程序形成对比：

reifyBad' :: (forall s. Reifies s s => Proxy s) -> ()
reifyBad' p = reify undefined (\(_ :: Proxy t) -> p @t) `seq` ()

• Couldn't match expected type ‘t0’ with actual type ‘Proxy s’
    because type variable ‘s’ would escape its scope
  This (rigid, skolem) type variable is bound by
    a type expected by the context:
      Reifies s a0 => Proxy s -> t0
• In the expression: p @t
  In the second argument of ‘reify’, namely
    ‘(\ (_ :: Proxy t) -> p @t)’
  In the first argument of ‘seq’, namely
    ‘reify undefined (\ (_ :: Proxy t) -> p @t)’

所以也许还有别的东西在起作用。

检查Reify的类型，可以稍微清楚地看出有些问题：

reify :: forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r

foo :: forall a r. Proxy a -> (forall s. (s ~ a) => Proxy s -> r) -> r
foo _ f = f Proxy

bar :: (forall a. Proxy a) -> ()
bar p = let p' = p in foo p' (\(_ :: Proxy s) -> (p' :: Proxy s) `seq` ())

• Couldn't match type ‘a0’ with ‘s’
    because type variable ‘s’ would escape its scope
  This (rigid, skolem) type variable is bound by
    a type expected by the context:
      Proxy s -> ()
  Expected type: Proxy s
    Actual type: Proxy a0
• In the first argument of ‘seq’, namely ‘(p' :: Proxy s)’
  In the expression: (p' :: Proxy s) `seq` ()
  In the second argument of ‘foo’, namely
    ‘(\ (_ :: Proxy s) -> (p' :: Proxy s) `seq` ())’

更具体地说，为什么会产生缺少实例的错误？

此外，这种行为是预期的、定义良好的，还是仅仅是typechecker的一个奇怪的边缘情况，碰巧产生了这种特定的结果？

Answer 1

reify :: forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r

skolem需求本质上声明，上面类型中的R不能依赖于第二个参数中量化的S。否则，由于reify返回r，它实际上会“转义”其作用域。

在

reifyBad :: (forall s. Reifies s s => Proxy s) -> ()
reifyBad p = reify undefined (\(_ :: Proxy t) -> p @t `seq` ())

我们看到Reify的第二个参数是\(_::Proxy t)->p@t`seq`()，因此R类型将是该函数的返回类型，即()。由于R~()不依赖于S，所以这里没有逃避的问题。

相反，在变体中

reifyBad' :: (forall s. Reifies s s => Proxy s) -> ()
reifyBad' p = reify undefined (\(_ :: Proxy t) -> p @t) `seq` ()

这里R被推断为\(_::Proxy t)->p@t的返回类型，它是Proxy t，其中t~s。因为R~Proxy s确实依赖于s，所以我们触发一个skolem错误。