Right, my bad, I just noticed the ConstraintKinds.

One way of getting round this is:

> type F tc a b =  (tc a, tc b) => (forall c. tc c => c -> c) -> Either a b -> Either a b

> foo' = (foo :: F Num a b) (2+)

As to why the type inference isn't powerful enough, you might want to ask on cafe. It's really tricky to get it right. Too much power and it'll loop. Too little and you end up with cases like this. And that's not even considering bugs!