模式中的类型推断

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绑定的更多详细信息,请参阅ghc wiki.