在模式中输入推论 [英] Type Inference in Patterns

问题描述

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

  { - ＃LANGUAGE GADTs，RankNTypes，ScopedTypeVariables，
 TypeOperators，NoMonomorphismRestriction＃ - } 
 module Foo其中
 
导入Data.Typeable 
 
数据Bar rp rq 
 
 data Foo b = Foo（Foo b）
 
 
 rebar :: forall rp rq rp'rp''。 （可键入rp'，可键入rp''）
 =>代理rp' - >代理rp'' - > Foo rp  - > Foo（Bar rp rq）
 rebar p1 p2（Foo x）= 
  - 应该推断y的签名... 
 let y = rebar p1 p2 x  -  :: Foo （Bar rp rq）
  - 在
的情况下（eqT :: Maybe（rp'：〜：rp''）），case语句与y 
的类型无关Just Refl  - > y 
  

如果 y ，我得到错误：

  Foo.hs：19：20：
无法匹配类型' rq0'与'rq'
'rq0'在约束内（rp'〜rp''）
不可触及
由构造函数
绑定的模式绑定$ b $ Refl :: forall（k :: BOX）（a1 :: k）。 a1：〜：a1，
在一个案例中，
在testsuite / Foo.hs：19：12-15 
'rq'是一个刚性类型变量，由
绑定
 rebar ::（可键入rp'，Typeable rp''）=>的签名
 Proxy rp' - >代理rp'' - > Foo rp  - > Foo（Bar rp rq）
 at testsuite / Foo.hs：12：20 
预期类型：Foo（Bar rp rq）
实际类型：Foo（Bar rp rq0）
相关绑定包括：
y :: Foo（Bar rp rq0）（绑定在testsuite / Foo.hs：16：7）
 rebar :: Proxy rp' - >代理rp'' - > Foo rp  - > Foo（Bar rp rq）
（绑定在testsuite / Foo.hs：14：1）
在表达式中：y 
在另一种情况下：Just Refl  - > y 
失败，模块加载：无。 
  

在多次事件中受到可怕的单态限制的影响后，我开启了 NoMonomorphismRestriction ，但不会改变行为。

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

解决方案

单态限制仅适用于顶级绑定。编译器知道 y 的实际类型，但是没有办法为它推断单形类型;这是类型错误的原因。如果你真的想关闭单形式的绑定，你必须使用正确的扩展名：

  { - ＃LANGUAGE NoMonoLocalBinds＃ - } 
  

使用它，您的代码将被编译。

关于单态let绑定的更多细节，查看ghc wiki 。

I noticed that GHC wanted a type signature which I think should be inferred. I minimized my example down to this, which almost certainly does nothing meaningful (I don't recommend running it on your favorite types):

{-# 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

Without a type signature on the definition of y, I get the error:

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.

Having been caught by the dreaded monomorphism restriction on multiple occassions, I turned on NoMonomorphismRestriction, but that doesn't change the behavior.

Why is the type of y not inferred to be the output type of the function?

解决方案

The monomorphism restriction applies only to top level bindings. The compiler is aware of the real type of y, but there is no way to infer a monomorphic type for it; that is the cause of the type error. If you really would like to turn off monomorphic let bindings, you have to use the correct extension:

{-# LANGUAGE NoMonoLocalBinds #-}

With it, your code compiles.

For much more detail about monomorphic let bindings, see the ghc wiki.

这篇关于在模式中输入推论的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！