[Haskell-cafe] RankNTypes + ConstraintKinds to use Either as a "union"

[oleg at okmij.org]

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)