2 Jan 2013 12:32

## Inference for RankNTypes

```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?

```

2 Jan 2013 13:04

### Re: Inference for RankNTypes

```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.
```

2 Jan 2013 13:49

### Re: Inference for RankNTypes

```* 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
```

2 Jan 2013 14:21

### Re: Inference for RankNTypes

```At Wed, 2 Jan 2013 14:49:51 +0200,
Roman Cheplyaka wrote:
> I don't see how this is relevant.

Well, moving `flip one' in a let solves the problem, and The fact that let-bound
variables are treated differently probably has a play here.  I originally
thought that this was because the quantifications will be all to the left in the
let-bound variable while without a let-bound variable the types are used
directly.  However this doesn’t explain the behaviour I’m seeing.

> 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.

Right.  The weirdest thing is that annotating `flip one' (as in `three' in my
code) or indeed `flip one 'x'' with the type that shows up in ghci makes
things work:

five = (flip one 'x' :: (forall a. a -> a) -> Char) id

Francesco

_______________________________________________
```

2 Jan 2013 17:20

### Re: Inference for RankNTypes

Your example doesn't work for the same reason the following doesn't work:

id runST (<some st code>)

It requires the inferencer to instantiate certain variables of id's type to polymorphic types based on runST (or flip's based on one), and then use that information to check <some st code> (id in your example) as a polymorphic type. At various times, GHC has had ad-hoc left-to-right behavior that made this work, but it no longer does. Right now, I believe it only has an ad-hoc check to make sure that:

runST \$ <some st code>

works, and not much else. Note that even left-to-right behavior covers all cases, as you might have:

f x y

such that y requires x to be checked polymorphically in the same way. There are algorithms that can get this right in general, but it's a little tricky, and they're rather different than GHC's algorithm, so I don't know whether it's possible to make GHC behave correctly.

The reason it works when you factor out or annotate "flip one 'x'" is that that is the eventual inferred type of the expression, and then it knows to expect the id to be polymorphic. But when it's all at once, we just have a chain of unifications relating things like: (forall a. a -> a) ~ beta ~ (alpha -> alpha), where beta is part of type checking flip, and alpha -> alpha is the instantiation of id's type with unification variables, because we didn't know that it was supposed to be a fully polymorphic use. And that unification fails.

On Wed, Jan 2, 2013 at 8:21 AM, Francesco Mazzoli wrote:
At Wed, 2 Jan 2013 14:49:51 +0200,
Roman Cheplyaka wrote:
> I don't see how this is relevant.

Well, moving `flip one' in a let solves the problem, and The fact that let-bound
variables are treated differently probably has a play here.  I originally
thought that this was because the quantifications will be all to the left in the
let-bound variable while without a let-bound variable the types are used
directly.  However this doesn’t explain the behaviour I’m seeing.

> 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.

Right.  The weirdest thing is that annotating `flip one' (as in `three' in my
code) or indeed `flip one 'x'' with the type that shows up in ghci makes
things work:

five = (flip one 'x' :: (forall a. a -> a) -> Char) id

Francesco

_______________________________________________

```_______________________________________________
```
2 Jan 2013 17:39

### Re: Inference for RankNTypes

On Wed, Jan 2, 2013 at 11:20 AM, Dan Doel wrote:
Note that even left-to-right behavior covers all cases, as you might have:

f x y

such that y requires x to be checked polymorphically in the same way. There are algorithms that can get this right in general, but it's a little tricky, and they're rather different than GHC's algorithm, so I don't know whether it's possible to make GHC behave correctly.

Oops, that should have been, "note that not even left-to-right behavior covers all cases."

Also, I don't mean to imply that GHC is behaving wrongly. Situations like these are usually the result of necessary trade-offs in the algorithms. GHC does a lot of things that algorithms that successfully check this type of examples don't have to deal with at all. You have to pick your poison.

-- Dan
```_______________________________________________
```
2 Jan 2013 17:47

### Re: Inference for RankNTypes

```At Wed, 2 Jan 2013 11:20:46 -0500,
Dan Doel wrote:
> Your example doesn't work for the same reason the following doesn't work:
>
>     id runST (<some st code>)
>
> It requires the inferencer to instantiate certain variables of id's type to
> polymorphic types based on runST (or flip's based on one), and then use
> that information to check <some st code> (id in your example) as a
> behavior that made this work, but it no longer does. Right now, I believe
> it only has an ad-hoc check to make sure that:
>
>     runST \$ <some st code>
>
> works, and not much else. Note that even left-to-right behavior covers all
> cases, as you might have:
>
>     f x y
>
> such that y requires x to be checked polymorphically in the same way. There
> are algorithms that can get this right in general, but it's a little
> tricky, and they're rather different than GHC's algorithm, so I don't know
> whether it's possible to make GHC behave correctly.
>
> The reason it works when you factor out or annotate "flip one 'x'" is that
> that is the eventual inferred type of the expression, and then it knows to
> expect the id to be polymorphic. But when it's all at once, we just have a
> chain of unifications relating things like: (forall a. a -> a) ~ beta ~
> (alpha -> alpha), where beta is part of type checking flip, and alpha ->
> alpha is the instantiation of id's type with unification variables, because
> we didn't know that it was supposed to be a fully polymorphic use. And that
> unification fails.

Hi Dan,

Thanks a lot for the answer, one forgets that with HM you always replace the
quantified variables immediately.

However I am still confused on how GHC makes it work when I annotate or put
things in separate variables.  In other words, can you provide links or clarify
how this procedure works:

The reason it works when you factor out or annotate "flip one 'x'" is that
that is the eventual inferred type of the expression, and then it knows to
expect the id to be polymorphic.

Thanks,
Francesco
```
2 Jan 2013 19:35

### Re: Inference for RankNTypes

If you want to know the inner workings, you probably need to read the OutsideIn(X) paper.*

I'm not that familiar with the algorithm. But what happens is something like this.... When GHC goes to infer the type of 'f x' where it knows that f's argument is expected to be polymorphic, this triggers a different code path that will check that x can be given a type that is at least as general as is necessary for the argument.

However, "flip one 'x' id" gives flip a type like (alpha -> beta -> gamma) -> beta -> alpha -> gamma. Then, we probably get some constraints collected up like:

alpha ~ (forall a. a -> a)
alpha ~ (delta -> delta)

That is, it does not compute the higher-rank type of "flip one 'x'" and then decide how the application of that to id should be checked; it decides how all the arguments should be checked based only on flip's type, and flip does not have a higher-rank type on its own. And solving the above constraints cannot trigger the alternate path.

However, when you factor out or annotate "flip one 'x'", it knows that it's applying something with a higher-rank type (whether because it inferred it separately, or you gave it), and that does trigger the alternate code path.

If that's still too vague, you'll have to refer to the paper.

-- Dan

On Wed, Jan 2, 2013 at 11:47 AM, Francesco Mazzoli wrote:
At Wed, 2 Jan 2013 11:20:46 -0500,
Dan Doel wrote:
> Your example doesn't work for the same reason the following doesn't work:
>
>     id runST (<some st code>)
>
> It requires the inferencer to instantiate certain variables of id's type to
> polymorphic types based on runST (or flip's based on one), and then use
> that information to check <some st code> (id in your example) as a
> behavior that made this work, but it no longer does. Right now, I believe
> it only has an ad-hoc check to make sure that:
>
>     runST \$ <some st code>
>
> works, and not much else. Note that even left-to-right behavior covers all
> cases, as you might have:
>
>     f x y
>
> such that y requires x to be checked polymorphically in the same way. There
> are algorithms that can get this right in general, but it's a little
> tricky, and they're rather different than GHC's algorithm, so I don't know
> whether it's possible to make GHC behave correctly.
>
> The reason it works when you factor out or annotate "flip one 'x'" is that
> that is the eventual inferred type of the expression, and then it knows to
> expect the id to be polymorphic. But when it's all at once, we just have a
> chain of unifications relating things like: (forall a. a -> a) ~ beta ~
> (alpha -> alpha), where beta is part of type checking flip, and alpha ->
> alpha is the instantiation of id's type with unification variables, because
> we didn't know that it was supposed to be a fully polymorphic use. And that
> unification fails.

Hi Dan,

Thanks a lot for the answer, one forgets that with HM you always replace the
quantified variables immediately.

However I am still confused on how GHC makes it work when I annotate or put
things in separate variables.  In other words, can you provide links or clarify
how this procedure works:

The reason it works when you factor out or annotate "flip one 'x'" is that
that is the eventual inferred type of the expression, and then it knows to
expect the id to be polymorphic.

Thanks,
Francesco

```_______________________________________________
```
2 Jan 2013 21:02

### Re: Inference for RankNTypes

```At Wed, 2 Jan 2013 13:35:24 -0500,
Dan Doel wrote:
> If you want to know the inner workings, you probably need to read the
> OutsideIn(X) paper.*
>
> I'm not that familiar with the algorithm. But what happens is something
> like this.... When GHC goes to infer the type of 'f x' where it knows that
> f's argument is expected to be polymorphic, this triggers a different code
> path that will check that x can be given a type that is at least as general
> as is necessary for the argument.
>
> However, "flip one 'x' id" gives flip a type like (alpha -> beta -> gamma)
> -> beta -> alpha -> gamma. Then, we probably get some constraints collected
> up like:
>
>     alpha ~ (forall a. a -> a)
>     alpha ~ (delta -> delta)
>
> That is, it does not compute the higher-rank type of "flip one 'x'" and
> then decide how the application of that to id should be checked; it decides
> how all the arguments should be checked based only on flip's type, and flip
> does not have a higher-rank type on its own. And solving the above
> constraints cannot trigger the alternate path.
>
> However, when you factor out or annotate "flip one 'x'", it knows that it's
> applying something with a higher-rank type (whether because it inferred it
> separately, or you gave it), and that does trigger the alternate code path.
>
> If that's still too vague, you'll have to refer to the paper.
>
> -- Dan
>
> *
> http://research.microsoft.com/en-us/um/people/simonpj/papers/constraints/jfp-outsidein.pdf

Thanks again for the answer.  I understood more or less what was going on with
the constraints - what I was wondering is how that alternate code path you cite
works.  I guess I’ll have to attack that epic paper sooner or later :).

Francesco

_______________________________________________