Suggest ScopedTypeVariables when type variable not in scope

I recently wrote this:

{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE TypeApplications #-}
module B where
f :: forall a. a -> a
f x = id @a x

And was hornswoggled for the better part of five minutes for why "a" wasn't in scope. Answer: you need ScopedTypeVariables. A suggestion would be nice.

Trac metadata

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

mentioned in issue #9244

changed weight to 5

added Tbug Trac import typechecker labels

Duplicate of #9244 (and #1316 (closed), #3691 (closed), #11438 (closed), #10581 (closed), #11539 (closed), ...).

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedDuplicate

I saw that bug, but it looks completely different (a request for name shadowing warnings at the type variable level), but OK ;)

I would love someone to work on this a bit.

In Edward's example above, it would be relatively easy to put 'a' in the environment with a flag to say "Not really in scope unless you use ScopedTypeVariables.

But there is more thinking to do. What if he'd written

f :: forall a. a -> a
f x = let g :: a -> a
          g _ = x
      in g x

Here the programmer probably intended the inner a -> a to be scoped by the forall; but as it stands, without ScopedTypeVariables it means

  g :: forall a. a->a

which will then be rejected by the type checker.

I suggest that

• ExplicitForAll should imply ScopedTypeVariables. (The reverse is already true!)

• 'RankNTypesshould implyScopedTypeVariables. (RankNTypesalready impliesExplicitForAll`, so the earlier bullet would imply this one.)

  You could always say ExplicitForAll, NoScopedTypeVariables\ if you really wanted.

That still leaves #9244 and friends wanting a better error message/suggestion. Simon

added Pnormal label