At Wed, 02 Jan 2013 12:32:53 +0100,
Francesco Mazzoli wrote:
>
> Hi list,
>
> I am a bit puzzled by the behaviour exemplified by this code:
>
> {-# LANGUAGE RankNTypes #-}
>
> one :: (forall a. a -> a) -> b -> b
> one f = f
>
> two = let f = flip one in f 'x' id
> three = (flip one :: b -> (forall a. a -> a) -> b) 'x' id
> four = flip one 'x' id
>
> Try to guess if this code typechecks, and if not what’s the error.
>
> While `two' and `three' are fine, GHC (7.4.1 and 7.6.1) complains about
> `four':
>
> Line 8: 1 error(s), 0 warning(s)
>
> Couldn't match expected type `forall a. a -> a'
> with actual type `a0 -> a0'
> In the third argument of `flip', namely `id'
> In the expression: flip one 'x' id
> In an equation for `four': four = flip one 'x' id
>
> So for some reason the quantified variable in `id' gets instantiated before it
> should, and I have no idea why.
>
> Any ideas?
>
> Francesco
OK, I should have looked at the manual first. From
<http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#id623016>:
“For a lambda-bound or case-bound variable, x, either the programmer provides an
explicit polymorphic type for x, or GHC's type inference will assume that x's
type has no foralls in it.”. So there is a difference between let-bound things
and the rest.
I still don’t get exactly what’s going on there. What’s the inferred type for
`flip one', and why is it causing that error? Since there really isn’t much to
infer here.
Francesco
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
