When can GHC infer constraint variables?

Question

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:

1. ConstrainedF has type forall c. (forall a. c a => [a] -> a) -> ConstrainedF c.
2. mconcat has type forall b. Monoid b => [b] -> b.
3. forall b. Monoid b => [b] -> b unifies with forall a. c a => [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.

Answer 1

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.

E.g. 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?