ghc accepts non-standard type without language extension

Ghc accepts this

f :: Eq a => Eq b => a -> b -> Bool
f a b = a==a && b==b

The nested contexts should require some language extension.

Trac metadata

Trac field	Value
Version	7.8.4
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

mentioned in issue #5957 (closed)

changed weight to 5

added Tbug Trac import labels

Hmmm, fair enough. Perhaps -XNestedContexts?

Trac metadata

Trac field	Value
Component	Compiler → Compiler (Parser)

If we want to control this with a language extension, then Rank2Types/RankNTypes should be a good choice. After all we already have

Prelude> let f :: a -> Eq a => a; f = undefined

<interactive>:4:10:
    Illegal polymorphic or qualified type: Eq a => a
    Perhaps you intended to use RankNTypes or Rank2Types
    In the type signature for ‘f’: f :: a -> Eq a => a

That being said, it was decided at some point that we should also allow forall independently from RankNTypes with ExplicitForAll. My initial thought was that RankNTypes would imply NestedContexts, just as it does ExplicitForAll.

I'd be happy to see this checked, if someone wants to have a go, but I doubt that it's a very high priority.

mentioned in issue #12087 (closed)

Moreover, the current treatment (allowing nested contexts) is inconsistent with GADTs (#12087 (closed)), which is undesirable.

Nothing hard here; just gotta decide what we want and implement it.

Trac metadata

Trac field	Value
Related	- → #5957 (closed)

added Pnormal label

marked this issue as related to #8346

added RankNTypes label

That being said, it was decided at some point that we should also allow forall independently from RankNTypes with ExplicitForAll.

It's true that ExplicitForAll allows use of the forall syntax independently of RankNTypes. That being said, it's clear that ExplicitForAll is not meant to enable the use of forall everywhere. After all, GHC will reject this program:

λ> :set -XExplicitForAll
λ> f :: forall a. a -> forall b. b -> a; f x _ = x

<interactive>:2:6: error:
    • Illegal polymorphic type: forall b. b -> a
      Perhaps you intended to use RankNTypes
    • In the type signature: f :: forall a. a -> forall b. b -> a

It's a bit tricky trying to figure out where the dividing line between ExplicitForAll and RankNTypes is, however. While the example is above is rejected without RankNTypes, the examples below are just fine without RankNTypes:

λ> :set -XExplicitForAll
λ> f2 :: forall a. forall b. a -> b -> a; f2 x _ = x
λ> f3 :: (forall a. a -> a); f3 x = x

This mirrors the situation with contexts quite closely, as the following is rejected without RankNTypes:

λ> g :: Eq a => a -> Eq b => b -> a; g x _ = x

<interactive>:2:6: error:
    • Illegal qualified type: Eq b => b -> a
      Perhaps you intended to use RankNTypes
    • In the type signature: g :: Eq a => a -> Eq b => b -> a

But the following are accepted without RankNTypes:

λ> g2 :: Eq a => Eq b => a -> b -> a; g2 x _ = x
λ> g3 :: (Eq a => a -> a); g3 x = x

One way to resolve this tension is to require that any non-prenex uses of forall or contexts must be guarded behind RankNTypes. A prenex type would be one that begins with an optional forall (with no surrounding parentheses), followed by an optional context (with no surrounding parentheses), followed by the body of the type. In other words, f2, f3, g2, and g3 above would all fail with the same error as f and g.

A benefit of this approach is that we wouldn't need a special NestedContexts extension just to rule out the original program in the issue description, as it would fall under the general RankNTypes umbrella. One might object that the type Eq a => Eq b => a -> b -> Bool isn't really higher-rank, but then again, GHC already rejects the very similar type Eq a => a -> Eq b => b -> a under the same pretenses, so we should at least be consistent.

One way to resolve this tension is to require that any non-prenex uses of forall or contexts must be guarded behind RankNTypes. A prenex type would be one that begins with an optional forall (with no surrounding parentheses), followed by an optional context (with no surrounding parentheses), followed by the body of the type. In other words, f2, f3, g2, and g3 above would all fail with the same error as f and g.

Go for it. I think this is the right answer. As we've discovered in many ways, a top-level forall is really quite different than other foralls.

Oh, and we should change RankNTypes to be called NestedForAlls. I see far too many people who call forall a. a -> forall b. b -> (a, b) a higher-rank type, and we are the reason why. But that's not really what I'm expecting here.

Oh, and we should change RankNTypes to be called NestedForAlls.

But that's just the thing—RankNTypes gives you more than nested foralls. It gives you nested contexts as well.

Also, do you think that this would meet the bar for requiring a GHC proposal? I expect a fair deal of breaking from this change, as it's surprisingly common for code to do things like forall a. forall b. {...} without enabling RankNTypes. In fact, base itself does this—see throw in GHC.Exception as one example.

Accepting forall a. forall b. without -XRankNTypes is a bug. You're fixing the bug. No proposal.

(Changing the name would require a proposal. Some day, I'll write a big proposal changing the names of lots of extensions. Including this one. -XInstanceSigs, I'm looking at you, too.)

Very well. If you're content with this being a bugfix, then so am I. I don't have a pressing need to implement this right now, but since I have been working on closely related nested-forall issues recently, this issue seemed like another place that would benefit from similar treatment.

Now that I think about it, actually implementing this idea would be slightly annoying. We couldn't implement this in the typechecker, since the following two types are identical in Core:

(Eq a, Eq b) => a -> b -> Bool
Eq a => Eq b => a -> b -> Bool

And yet only the latter must require RankNTypes. This suggests that we would need to implement this check earlier, perhaps in the renamer. Every time we rename a type, we would need to keep track of whether nested foralls or contexts are permitted, and every time we go underneath an arrow, forall, context, or HsParTy, we would need to update the nested-foralls-or-contexts-allowed state. This sounds fairly tedious, but I don't see a better way to do this at present.

I was thinking this would be easy, because of your ongoing refactoring. But that accounts for only the nested foralls, not the nested contexts.

Speaking of nested contexts, and while we're thinking about what our specification is, what do we think of

foo :: forall a. a -> a -> Int -> Eq a => Bool
foo x ((== x) -> result) _ = result

? This uses the Eq instance before it's in scope. (The Int parameter is to prevent any kind of lookahead.) This is accepted today, because of deep skolemisation. I've posted !2600 (comment 278638) to see what will happen without deep skolemisation. It's possible that the new semantics in !2600 (merged) gives privileged access to top-level constraints, which would then suggest that we store top-level constraints separately, like you're trying to do with top-level foralls. That, in turn, would make this easier to implement.

It's possible that the new semantics in !2600 (merged) gives privileged access to top-level constraints, which would then suggest that we store top-level constraints separately, like you're trying to do with top-level foralls. That, in turn, would make this easier to implement.

I'm not quite sure I follow. What about simplified subsumption would give special treatment to top-level constraints?