The qualified use of Prelude introduced in 2.1.1 breaks Agda

[andreasabel]

Happy 2.1.1 broke Agda:

• Happy-2.1.1 causes Agda build to fail agda/agda#7585

Because our parser has import Prelude hiding (null) another import qualified Prelude has to be omitted by the generator to have Prelude.null in scope.

I think 2.1.1 should be deprecated as it pretends to be a minor bump but breaks user's code.

A new happy should be released including the fix: Emit import qualified Prelude in the generated code.

[sgraf812]

Thanks. Indeed that sounds like a breaking change, but it is pretty much unavoidable. (And even permissible according to the PVP, even if unintended. 2.0->2.1 is a major bump.)

A new happy should be released including the fix: Emit import qualified Prelude in the generated code.

That won't work due to the way the implicit import Prelude is inserted; see #321 (comment). (#321 fixes visq/language-c#99.)
That is, import qualified Prelude would require all users to also import Prelude.

In short, there is no backwards-compatible way for Happy to use any Prelude functions other than the ones it is currently using. If you were to write e.g. import Prelude hiding (otherwise) then you couldn't compile a parser generated by Happy < 2.0 either.

I would be happy to deprecate Happy 2.1.1 and openly announce the breaking change in 2.1.2 if you could help me come up with a better story. For example, we could generate

import qualified Prelude
import Prelude hiding (a,b,c)

where a,b,c are somehow controlled by a flag passed to happy or a directive in the .y file. Then you could still hide null. Would that be preferable? I can't tell.

[sgraf812]

Perhaps we can provide a backwards compatible solution by not relying on Prelude at all.
That is, import qualified Data.Bool, and use Data.Bool.otherwise. (Do note that Data.Bool is not subject to the same treatment by the Haskell report.) Absolutely ugly, but should get the job done.

[andreasabel]

I think not qualifying by Prelude is conceptually better.
Prelude is a (sometimes seemingly random) selection of exports from base, and up to its own fluctuations. Cutting it from the loop entirely would result in a more stable situation.

Concerning the PVP concerns: Agda worked fine with 2.1 but broke with 2.1.1, which is a situation not compatible with the spirit of the PVP. If 2.1.1 were 2.2 that would not be a PVP problem.

Maybe I should have written more clearly:

I think 2.1.1 should be deprecated as it pretends to be a minor bump [over 2.1] but breaks user's code.

But I see now that 2.1 has been deprecated, that makes it no PVP violation over 2.0.2 (non-deprecated).

Would deprecating 2.1.1 be a valid hotfix of the situation?

[sgraf812]

Would deprecating 2.1.1 be a valid hotfix of the situation?

I'm not sure if a deprecated version such as 2.1 is considered a release according to the PVP, but I'm fine with deprecating 2.1.1 for the time being.

[andreasabel]

but I'm fine with deprecating 2.1.1 for the time being.

Thanks, that will save me from revising tons of Agda versions with a bound on happy!

[sgraf812]

I just released 2.1.2. I hope that fixes your issues building Agda.