Thiago Negri wrote:

Why type inference can't resolve this code?

{-# LANGUAGE RankNTypes, ConstraintKinds #-}

bar :: (Num a, Num b) => (forall c. Num c => c -> c) ->Either a b ->Either a b bar f (Left a) = Left (f a) bar f (Right b) = Right (f b)

bar' = bar (+ 2) -- This compiles ok

foo :: (tc a, tc b) => (forall c. tc c => c -> c) -> Either a b -> Either a b foo f (Left a) = Left (f a) foo f (Right b) = Right (f b)

foo' = foo (+ 2) -- This doesn't compile because foo' does not typecheck

The type inference of the constraint fails because it is ambiguous. Observe that not only bar (+2) compiles OK, but also bar id. The function id :: c -> c has no constraints attached, but still fits for (forall c. Num c => c -> c). Let's look at the problematic foo'. What constraint would you think GHC should infer for tc? Num? Why not the composition of Num and Read, or Num and Show, or Num and any other set of constraints? Or perhaps Fractional (because Fractional implies Num)? For constraints, we get the implicit subtyping (a term well-typed with constraints C is also well-typed with any bigger constraint set C', or any constraint set C'' which implies C). Synonyms and superclass constraints break the principal types. So, inference is hopeless. We got to help the type inference and tell which constraint we want. For example,

newtype C ctx = C (forall c. ctx c => c -> c)

foo :: (ctx a, ctx b) => C ctx -> (forall c. ctx c => c -> c) -> Either a b -> Either a b foo _ f (Left a) = Left (f a) foo _ f (Right b) = Right (f b)

foo' = foo (undefined :: C Num) (+2)

Or, better

xyz :: (ctx a, ctx b) => C ctx -> Either a b -> Either a b xyz (C f) (Left a) = Left (f a) xyz (C f) (Right b) = Right (f b)

xyz' = xyz ((C (+2)) :: C Num) xyz'' = xyz ((C (+2)) :: C Fractional)