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)

_______________________________________________

Haskell-Cafe mailing list

[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe