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@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0xF0FBF51F Debian Developer: nomeata@debian.org