在模式中输入推论 [英] Type Inference in Patterns
问题描述
{ - #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屋!