haskell - 模式中的类型推断

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

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

{-# LANGUAGE NoMonoLocalBinds #-}

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

有关单态 let 绑定(bind)的更多详细信息， see the ghc wiki .