Confusing error message when universally quantifying unused type variables

[Joachim Breitner]

Hi,


Am Dienstag, den 20.10.2015, 13:10 +0200 schrieb Alexander Berntsen:
> 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.

This is expected. If there is any ∀ in the type, then GHC wants all
variables to be properly bound. This is not related to whether a is
used or not:

Prelude> let f :: a -> b ; f = undefined
Prelude> let f :: forall a. a -> b ; f = undefined
<interactive>:5:25: Not in scope: type variable ‘b’
Prelude> let f :: forall a b. a -> b ; f = undefined


> 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.)

You mean type constraints involving an otherwise unused type variable?
This seems to be unrelated to the question of foralls.

But indeed the 2010 report writes
“The context cx must only contain type variables referenced in t.”
https://www.haskell.org/report/node/2010/haskellch4.html#x10-660004.1.3
and even with -XHaskell2010, this is accepted. Might be worth a ticket,
although I would not be surprised if some of the type class hackers
around here finds a use case for this :-)

Greetings,
Joachim


-- 
Joachim “nomeata” Breitner
  mail at joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  • GPG-Key: 0xF0FBF51F
  Debian Developer: nomeata at debian.org

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20151020/15f649d2/attachment.sig>