[Haskell-cafe] Inference for RankNTypes
Roman Cheplyaka
roma at ro-che.info
Wed Jan 2 13:49:51 CET 2013
* Francesco Mazzoli <f at mazzo.li> [2013-01-02 13:04:36+0100]
> 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 don't see how this is relevant.
GHC correctly infers the type of "flip one 'x'":
*Main> :t flip one 'x'
flip one 'x' :: (forall a. a -> a) -> Char
But then somehow it fails to apply this to id. And there are no bound
variables here that we should need to annotate.
Roman
More information about the Haskell-Cafe
mailing list