Opened 22 months ago

Last modified 8 months ago

#8346 new bug

Rank 1 type signature still requires RankNTypes

Reported by: tinctorius Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.6.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #2605 Differential Revisions:

Description

When trying to figure out which type variable names are *actually* bound in ScopedTypeVariables, I tried floating foralls into the covariant argument of the function type. Essentially, I ran into the problem that programs like the following are rejected:

{-# LANGUAGE ExplicitForAll #-}
tuple :: forall a. a -> (forall b. b -> (a, b))
tuple = (,)

The message is as follows:

Main.hs:2:10:
    Illegal polymorphic or qualified type: forall b. b -> (a, b)
    Perhaps you intended to use -XRankNTypes or -XRank2Types
    In the type signature for `tuple':
      tuple :: forall a. a -> (forall b. b -> (a, b))

As far as I know, the rank of a type is defined by how deep quantifiers are nested in contravariant parts of that type. Or something like that. Also, as far as I know, forall a. a -> (forall b. b -> (a, b)) is equivalent to forall a b. a -> b -> (a, b), and more importantly, both are rank-1 polymorphic. There should be no need to use extensions that allow higher-ranked polymorphism.

Change History (3)

comment:1 Changed 22 months ago by tinctorius

Now, about a fix for this. It can be done quickly, and it can be done elegantly.

  • The quick fix: when you see A -> (forall B. C), think forall B. (A -> C).

This specific bug should vanish. However, the problem is bigger:

{-# LANGUAGE ExplicitForAll #-}
newtype Wrap a r = Wrap (a -> r)
tuple :: forall a. Wrap a (forall b. b -> (a, b))
tuple = Wrap $ \x y -> (x, y)
  • The elegant fix: when you see C T1 T2 .. (forall X. TK .. TN), and C is covariant in its K-th parameter, think forall X. C T1 T2 .. TK .. TN.

This is of course a lot harder. Perhaps the new roles feature can be leveraged to carry this information around.

comment:2 Changed 22 months ago by simonpj

I know it's technically not right but I'm disinclined to do much about it (myself anyway). In fact I rather regret having Rank2Types as well as RankNTypes. (I think that was originally because Hugs had the former but not the latter.) I'd rather have just a flag to say "all the foralls at the top, like Haskell 98" and "foralls anywhere". Having lots of flags to enforce fine distinctions doesn't seem all that useful to me.

If anyone wants to make a patch to more faithfully implement the current flags, by all means do so. I remember that it was tiresomely fiddly, which is why I compromised on the current behaviour.

Simon

Last edited 22 months ago by simonpj (previous) (diff)

comment:3 Changed 8 months ago by thomie

  • Component changed from Compiler to Compiler (Type checker)
Note: See TracTickets for help on using tickets.