模式中的类型推断

Question

我注意到 GHC 想要一个我认为应该推断的类型签名。我将我的示例最小化到此，这几乎肯定没有任何意义（我不建议在您最喜欢的类型上运行它）：

{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables,
             TypeOperators, NoMonomorphismRestriction #-}
module Foo where

import Data.Typeable

data Bar rp rq

data Foo b = Foo (Foo b)


rebar :: forall rp rq rp' rp'' . (Typeable rp', Typeable rp'') 
     => Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq)
rebar p1 p2 (Foo x) =
  -- The signature for y should be inferred...
  let y = rebar p1 p2 x -- :: Foo (Bar rp rq)
  -- The case statement has nothing to do with the type of y
  in case (eqT :: Maybe (rp' :~: rp'')) of
    Just Refl -> y

y 的定义上没有类型签名，我得到错误：

Foo.hs:19:20:
    Couldn't match type ‘rq0’ with ‘rq’
      ‘rq0’ is untouchable
        inside the constraints (rp' ~ rp'')
        bound by a pattern with constructor
                   Refl :: forall (k :: BOX) (a1 :: k). a1 :~: a1,
                 in a case alternative
        at testsuite/Foo.hs:19:12-15
      ‘rq’ is a rigid type variable bound by
           the type signature for
             rebar :: (Typeable rp', Typeable rp'') =>
                      Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq)
           at testsuite/Foo.hs:12:20
    Expected type: Foo (Bar rp rq)
      Actual type: Foo (Bar rp rq0)
    Relevant bindings include
      y :: Foo (Bar rp rq0) (bound at testsuite/Foo.hs:16:7)
      rebar :: Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq)
        (bound at testsuite/Foo.hs:14:1)
    In the expression: y
    In a case alternative: Just Refl -> y
Failed, modules loaded: none.

由于在多种情况下受到可怕的单态限制，我打开了NoMonomorphismRestriction，但这并没有改变行为。

为什么y的类型没有被推断为函数的输出类型？

Answer 1

单态限制仅适用于顶级绑定。编译器知道y 的真实类型，但无法为其推断出单态类型；这就是类型错误的原因。如果你真的想关闭单态 let 绑定，你必须使用正确的扩展：

{-# LANGUAGE NoMonoLocalBinds #-}

有了它，你的代码就可以编译了。

有关单态 let 绑定的更多详细信息，see the ghc wiki。

Answer 2

我不熟悉 GHC 的类型算法。不过，这是我对编译器为什么无法弄清楚的猜测。

考虑这段代码：

rebar :: forall rp rq rp' rp'' . (Typeable rp', Typeable rp'') 
     => Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq)
rebar p1 p2 (Foo x) =
  let y = ... :: Foo (Bar rp Char)
  in case (eqT :: Maybe (Char :~: rq)) of
     Just Refl -> y

这应该可以编译，因为匹配Refl 证明Char ~ rq，因此最后的y 具有正确的返回类型Foo (Bar rp rq)。程序通过类型检查。

但是，假设我们有

  let y = ... :: Foo (Bar rp rq)

在这种情况下，y 已经有了正确的类型，Refl 没有用处。同样，程序通过了类型检查。

现在，假设我们有 no 类型注释。编译如何确定哪个是 let y = ... 绑定的正确类型？毕竟，他们（至少）有两个领先 正确输入整个rebar。

这也可以解释为什么如果添加_ -> y 它确实有效：在这种情况下，编译器知道不需要Refl。相反，如果您添加y -> error ""，则无法推断出有关y 的信息。

实际的完整故事可能比上面更复杂：这里我很方便地忽略了来自y 定义的信息，即rebar p1 p2 x。换句话说，我只考虑上下文对y 定义的约束，而不是其他方向的约束。

在您的示例中，类型方程实际上是 rp' ~ rp''，这似乎与 w.r.t 无关。最后是y 的类型。也许编译器不够聪明，无法弄清楚。