我收到类型推断错误,因为 GHC 不会推断约束变量。它看起来可以通过一阶统一来推断。在进一步的调查中,我发现插入 let-bindings 会改变类型推断的行为。我想知道GHC在做什么。
这里的代码演示了这个问题。newtypeConstrainedF c
代表类型参数受 约束的多态函数c
。据我所知,GHC 不会c
根据给定的值进行推断ConstrainedF
。
{-# LANGUAGE RankNTypes, ScopedTypeVariables, ConstraintKinds, MonoLocalBinds #-}
import Data.Monoid
import GHC.Prim(Constraint)
newtype ConstrainedF c =
ConstrainedF { runConstrainedF :: forall a. c a => [a] -> a}
applyConstrainedF :: forall c a. c a => ConstrainedF c -> [a] -> a
applyConstrainedF f xs = runConstrainedF f xs
-- GHC cannot infer the type parameter of ConstrainedF
foo :: [Int]
foo = applyConstrainedF (ConstrainedF mconcat) [[1], [2]]
--foo = applyConstrainedF (ConstrainedF mconcat :: ConstrainedF Monoid) [[1], [2]]
应该可以在应用程序中推断类型ConstrainedF mconcat
:
ConstrainedF
有类型forall c. (forall a. c a => [a] -> a) -> ConstrainedF c
。mconcat
有类型forall b. Monoid b => [b] -> b
。forall b. Monoid b => [b] -> b
forall a. c a => [a] -> a
与由赋值a := b
和相结合c := Monoid
。
然而,GHC 抱怨:
Could not deduce (Monoid a) arising from a use of `mconcat'
from the context (c0 a).
关于约束变量,我必须遵循哪些规则才能让 GHC 推断类型?
歧义类型错误的典型解决方案是添加代理值来约束歧义类型。当我尝试时,这很挑剔。如果我只是添加一个额外的参数来约束 的类型c
,它可以工作:
data Cst1 (c :: * -> Constraint) = Cst1
monoid :: Cst1 Monoid
monoid = Cst1
applyConstrainedF :: forall c a. c a => ConstrainedF c -> Cst1 c -> [a] -> a
applyConstrainedF f _ xs = runConstrainedF f xs
foo :: [Int]
foo = applyConstrainedF (ConstrainedF mconcat) monoid [[1], [2]]
但是引入 let 绑定会foo
混淆类型推断,并且不能再c
与Monoid
.
foo_doesn't_work :: [Int]
foo_doesn't_work = let cf = ConstrainedF mconcat
in applyConstrainedF cf monoid [[1], [2]]
由于类型推断在这两个函数之一中得到了正确答案,这告诉我 GHC 在某些情况下会统一约束变量,但在其他情况下不会。我不明白发生了什么事。