这种涉及反射的神秘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) -> ()

我觉得这很好奇.乍一看,这是无效的,因为在第二个例子中,skolem s将逃避其范围.然而,这实际上并不正确 - 错误消息从未提及skolem逃逸,与此略有不同的程序形成对比:

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

的范围a和s显然是不同的,所以它似乎很有道理是GHC不会让他们统一.然而,似乎关于函数依赖引入的局部等式约束Reifies会引起某种奇怪的行为.有趣的是,这对功能强大了:

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` ())

...但是删除类型签名中的等式约束foo会使它们无法进行类型检查,从而产生一个skolem转义错误:

• 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` ())’

在这一点上,我感到困惑.我有几个(高度相关的)问题.

1. 为什么reifyBad首先没有进行类型检查？

2. 更具体地说,为什么它会产生缺少的实例错误？

此外,这种行为是期望的还是定义明确的,还是仅仅是类型检测器的一个奇怪的边缘情况恰好产生了这个特定的结果？

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,这里没有逃避问题.

然而,p @t根据类型p需要Reifies t t.既然reify会选择t ~ s,约束就是一样的Reifies s s.相反,reify只提供Reifies s a其中a的类型undefined.

这里的细微之处在于,虽然undefined可以生成任何类型a,但类型检查器无法统一s和a.这是因为具有相同类型的函数reify有权仅接收固定(刚性)类型的一个值a,然后s根据需要选择多个类型.s用一个单独统一所有这样的s a是错误的,有效地限制了sby 的选择reify.

相反,在变体中

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错误.