Confusing error message when universally quantifying unused type variables

[Alexander Berntsen]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

In Set theory sentence construction, if the letter is not used then no
foul. In Haskell, it is not always so.

The following is well-typed and works happily:
f :: Eq a => b -> b
f b = b

However, this does not work:
f :: ∀ a. Eq a => b -> b
f b = b

It will result in the error "Not in scope: type variable ‘b’" being
spat out twice.

Is this error message really desirable? If there is no principled
reason for this result, may I suggest improving it?

I can conceivably see some codebase using RankNTypes exclusively
having a typo like

f :: ∀ a. b -> b
f b = b

Consequently the error message should be more precise.

Furthermore the first code snippet I gave also strikes me as
nonsensical; if someone has code like that, it is probably the result
of a typo. Should we really permit it? Is there a motivating reason
for permitting it? If no, I suggest it be an error. (My understanding
of the 2010 report was that it *isn't* permitted, but perhaps I read
it wrong.)
- -- 
Alexander
alexander at plaimi.net
https://secure.plaimi.net/~alexander
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2

iQIcBAEBCgAGBQJWJiE0AAoJENQqWdRUGk8BVmYP/0yhrfFs8LHLUAhGnza3f6Xx
uFJQdvMmZcSLQQZxFyBvVcNwAK0x1ntnT+jeG/Q0j1oQns6EoWkJ9WzBQIxVQ2+O
9bm45N+gX1K1W1Z0WEX+LCPszntLMvBdp6C3Wp4ff+XvS9e0uHTqftDdD3iUexPA
K5wTB5qs+3IWVFEyyPIuJpOqOLhTy9FMct9Ls4m72Uu3FIWPEgjANuT/WkkLASXP
Av+qn0hTUzmoNf2nWcjvJQIZvgM6xfpJleWlO2CinOuPunZiackja/qTGlvx7Pu6
Yo5Fs2WdfCB1yx3iPnDcSrJ3pQcZkLqVsGRNdEXdQEHMH1icLR15Z7ynpKkI6uBb
JI+vAyq//NbdbRUOPzwN/PA+kGczUTBhTeAnwB5194fdzlfmH9vDsdN8p4CPtsTG
3T3u5EEyn8a/v0nQPssDEfli8Mx4uOswQmTsLgJCJ1H94FbNdGS3R98NmM63A9II
rN53o16m6z4C27YQL4q84LwbnWvOEyE9s3xBZMd8hsbTdb7F2syVoSYZazgP5PGc
uv/pAwKqwkGU53yBBhj+RqfPXk3qf0bOHtsercIAhnmkIAjI5l7bdxmDyhW4aj49
pWRJgOPAAlQ+VriFoodMZ9PD42pvxUlzicDfvpELVpviHdlTrovky9UC+buCFrtG
7k9GmyHqe/B3LyDjxbh+
=jerq
-----END PGP SIGNATURE-----