10 Oct 07:24 2013

## RankNTypes + ConstraintKinds to use Either as a "union"

<oleg <at> okmij.org>

2013-10-10 05:24:41 GMT

2013-10-10 05:24:41 GMT

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).(Continue reading)