Confusing error message when universally quantifying unused type variables
-----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@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-----
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
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA512 On 20/10/15 13:23, Joachim Breitner wrote:
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: I see. I still think the error message could be more specific though...
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. It is. It just hit me while reading through my email before sending it.
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. Then I understood it correctly. I think we should fix this.
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 :-) If there is a usecase for this, it could be a pragma. GHC should not accept it by default though.
Alexander alexander@plaimi.net https://secure.plaimi.net/~alexander -----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQIcBAEBCgAGBQJWJiUfAAoJENQqWdRUGk8BwE8QALSsg6Tn0Xet7v4uJ6xRj2Hi Ai2D70snCRi3kVrIbtwN3ZiOQfmLPTqQbohfICMac1AwWA8P9QQ+FKvii5UNh9SG 0YdAOp6SFyIrKU9SobfEiDSM4D2KZJ/6JsJFh4nmmDQWneA7YgGM1Gk2zFlMiW1e oYyERM3qTcMKo1g/qwQOEIvGiWhdbxBQ04NbuOf+cSLAb/rKeBEylzG7dbmtCJeN LFUZPwMOUNFSSXvaM5xGzeSppd+dxEd1zk9JR2lm0Q4J8gRfz3Upibi7tWDtJnia IW0znMAPRXdcjxaonXsmUC1rK+Ub9Ey3Bt0lR37BzCUaAmvYgVfvzhRyDSLUrpFA ym2sBGn75dfWJuor9kbeoQ1kRg1wPrZy9B6/4u7DBFWU2HnSreH6x/Izu741QSdZ 9xXT5caU1H/W76CybbBvnH8IUjv76SP9b83rYBFc0r/JhK3+r/nODckTrif1zAh9 2WOq6q1lo30/bURcNcx0qLZoCoOFmQtOpFTOOD84yCWAfrZ2Ybnnh8Eh/7cd5JQo 8/dIW9wFJCSBL9rX9PbuYygTEPaUHNR099QRZ5LBRp39NjFR/t+Z/gnHpnivxsz0 p12aOPbTNxCbctoeLNE2S/sw9ZDEWnTupUqhF8QLvZieVaznnqwNcsGXUd/qYPP8 Y2l0+sojeWyk8XNKNz+m =nxvb -----END PGP SIGNATURE-----
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA512 I opened a ticket[0] for the "accepting tv in ctx not mentioned in t"-bug. [0] https://ghc.haskell.org/trac/ghc/ticket/10991 - -- Alexander alexander@plaimi.net https://secure.plaimi.net/~alexander -----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQIcBAEBCgAGBQJWJimRAAoJENQqWdRUGk8BrxMQALYy+5lMQyyjXC9NOikvsu/1 fMuIPdFcG8pCPuUVcTwSQ3WiqcHf7sfkTMXcFAhDwaEdxBsoOCuMmnLQVD+1lP8I lC6Qht/Ykw1n+Ifdv/F6AEPYsKuZk7DWW1LMAVDimDK+gyDrUmopCwyU/qMNOuwl KvquTHC2MOuIe/RWP6fssF2aeFbY4rnVIOuJezQbGqohgwCsbSLLU5raZCpuiL/R mCvarhl6csZ/uQmY8p/WWosX9r3IXH/z9OF9txAEQLQ//SvHjOVg3KzErKJQcYu8 K8dqmYItbbU5u28yOg7fP+N1fn55WBbA6Z9IaNyJl+WX9wy9lxloS2Sqxor12Nr/ KeWIWncelQ18o5ZX6nccGij/EPIsOidx7Fd92nw+WF07bZBhk8PXZw7F+daNCJKB woTlb1s6bLTsyl8wdheaVajNXMtAsVjQr9fEoB0yxLFpkj8xlh/9JWJ4pjlJonr7 zBGz95myygTQ+y47rRnxwV279v2FommnIF0pzjCuYfuIGaaCshe6pvIJOLdiVh0Y eCRPVUcXGCCg81CQP3vHAiNm2ocpIYT+P6n9wihvjgh5zpcxjkkJO+aYNIRfHbEo CQ8zch+UoF6fcMriJU/B0xrJ+ZZYyFuU/9YgOLJf0uBWUVMvKk/pjrLPRlB8OLWE 8PEOUf+OxyAWcGRwapND =ICmd -----END PGP SIGNATURE-----
participants (2)
-
Alexander Berntsen -
Joachim Breitner