When can GHC infer constraint variables?

I am getting type inference errors because GHC will not infer a constraint variable. It looks inferable by first-order unification. In further investigation, I found that inserting let-bindings changes the behavior of type inference. I'd like to know what GHC is doing.

The code here demonstrates the problem. The newtype ConstrainedF c stands for a polymorphic function whose type parameter is constrained by c . As far as I can tell, GHC won't infer c based on the values given to 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]]

It should be possible to infer types in the application ConstrainedF mconcat :

ConstrainedF has type forall c. (forall a. ca => [a] -> a) -> ConstrainedF c forall c. (forall a. ca => [a] -> a) -> ConstrainedF c .

mconcat has type forall b. Monoid b => [b] -> b forall b. Monoid b => [b] -> b .

forall b. Monoid b => [b] -> b forall b. Monoid b => [b] -> b unifies with forall a. ca => [a] -> a forall a. ca => [a] -> a by the assignment a := b and c := Monoid .

However, GHC complains:

Could not deduce (Monoid a) arising from a use of `mconcat'
from the context (c0 a).

What rules do I have to follow regarding constraint variables so that GHC can infer types?

---

A typical solution for ambiguous type errors is to add proxy values to constrain the ambiguous type. This was finicky when I tried it. If I just add an extra parameter to constrain the type of c , it works:

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]]

But introducing a let binding in foo confuses type inference, and it can no longer unify c with Monoid .

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

Since type inference gets the right answer in one of these two functions, this tells me that GHC will unify constraint variables in some situations but not others. I don't understand what's going on.

---

The problem here is subtyping. In your example, c could as well be (Monoid b, Eq b) .

Furthermore, you could then use Data.Typeable to inspect what c was instantiated with.

Or, what if you asked to "unify" (c, d) (a pair of constraints) with Monoid ?

---

The answer to the second part of your question is — you guessed it! — let generalization.

I know that you guessed it since you've added a MonoLocalBinds pragma. However, it doesn't do what you expect here. You see, it only stops generalization of truly local bindings — ones that depend on function parameters or other local bindings.

Eg this works:

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

For the details see Let generalisation: Which bindings are affected?

链接地址: http://www.djcxy.com/p/43076.html

上一篇: 用fundeps捆绑约束

下一篇: GHC何时可以推断约束变量？