GHC何时可以推断约束变量？

Question

我得到类型推断错误，因为GHC不会推断约束变量。一阶统一看起来是不可推论的。在进一步的调查中，我发现插入让绑定改变了类型推断的行为。我想知道GHC在做什么。

这里的代码演示了这个问题。newtypeConstrainedF c代表一个多态函数，其类型参数受c约束。据我所知，GHC不会根据ConstrainedF的值推断c。

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

1. ConstrainedF对于所有c.（对于所有a.c.a.）都有类型=

然而，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]]

但是在foo中引入let绑定会混淆类型推断，并且它不能再将c与Monoid统一起来。

foo_doesn't_work :: [Int]
foo_doesn't_work = let cf = ConstrainedF mconcat
                   in applyConstrainedF cf monoid [[1], [2]]

由于类型推断在这两个函数中的一个函数中得到了正确的答案，这告诉我GHC在某些情况下会统一约束变量，但在其他情况下不会。我不明白发生了什么。




Answer 1

这里的问题是分型。在你的例子中，c也可以是（幺半群b，等式b）。

此外，还可以使用数据。可键入以检查c的实例化内容。

或者，如果您要求将（c，d）（一对约束）与幺半群“统一”呢？

你问题第二部分的答案是-你猜对了！-让我们概括一下。

我知道你猜到了，因为你添加了一个monocalbindspragma。然而，它并没有达到你期望的效果。你看，它只会停止真正的局部绑定的泛化——那些依赖于函数参数或其他局部绑定的绑定。

例如，这种方法有效：

foo_does_work :: () -> [Int]
foo_does_work x =
  let cf = const (ConstrainedF mconcat) x
  in applyConstrainedF cf monoid [[1], [2]]

有关详细信息，请参阅Let generalization:哪些绑定受到影响？