HEAD (7.5.20120421) requires RankNTypes for a rank-2 type

[dreixel]

While building syb with HEAD, Ian reported that he needed to use RankNTypes instead of Rank2Types. I minimized the problem to:

{-# LANGUAGE Rank2Types #-}

module Rank2 where

f :: (forall a. a -> (forall b. b)) -> c
f = undefined

g :: (forall a b. a -> b) -> c
g = undefined

7.4 accepts both f and g. HEAD complains on the signature of f:

    Illegal polymorphic or qualified type: forall b. b
    Perhaps you intended to use -XRankNTypes or -XRank2Types
    In the type signature for `f':
      f :: (forall a. a -> (forall b. b)) -> c

It doesn't complain about g, but I think the signatures are equivalent. Ian further reports that the change in behavior seems to have occurred after 7.5.20120401.

[simonpj]

The difficulty is this

• The argument of a rank-2 arrow type should have rank 1
• A vanilla H98 type sig has rank 1
• But technically (Int -> forall a. a->a) is rank 1, although it is not H98.

GHC currently has the (somewhat ad-hoc) restriction that a rank-1 type must have all its foralls at the front, which is why this program is rejected. And yes that's a change in behaviour. (A different bug report said that (Int -> forall a. a->a) was accepted despite no higher-rank flags being on.

Perhaps it'd be better to always accept foralls to the right of an arrow. After all, you need at least -XForAllTypes to be able to write them.

[dreixel]

I don't feel strongly about it either way. We can change syb to use the rank-n flag. Is there even a good reason to distinguish rank-2 from rank-n?

[simonpj]

I don't think so. I'd be happy to see -XRank2Types deprecated. One less thing to deal with.

[tibbe]

Deprecating Rank2Types would require fixing 775 modules on Hackage. That's a lot of busy work. Could we have Rank2Types just be an alias for RankNTypes?

[simonpj]

Well it'd be odd to have "2" as a permanent alias for "arbitrary" wouldn't it? Isn't this precisely what deprecation is for: everything works but you get a nudge saying "please change when it's convenient". In fact it *is* an alias for RankNTypes plus a deprecation message.

We can keep supporting Rank2Types (as an alias for RankNTypes), with deprecation, for multiple releases.

Or what?

Simon

[illissius]

Might the reason for the separation have been that type inference is in theory decidable for rank-2 types, but not higher? I'm not a type theorist but I found this for example:  http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.144.1202 (WRT the deprecation/aliasing proposal itself I don't have an opinion)

[simonpj@…]

commit 984676d51291ea900cec289599e647de38645405

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Fri Oct 19 00:54:59 2012 +0100

    Deprecate Rank2Types and PolymorphicComponents, in favour of RankNTypes
    
    We agreed that it's not worth the bother of trying to maintain all
    these distinct flags; RankNTypes will do the job fine.  Trac #6032.

 compiler/main/DynFlags.hs        |   11 ++++-------
 compiler/prelude/PrelRules.lhs   |    2 +-
 compiler/simplCore/OccurAnal.lhs |    2 +-
 compiler/typecheck/TcMType.lhs   |   13 +++----------
 4 files changed, 9 insertions(+), 19 deletions(-)