Maybe avoid introducing almost undefined arguments?

[mechvel]

The master branch of July 15, 2025 has

module Algebra.Properties.Semiring.Primality  {a ℓ} (R : Semiring a ℓ) where
...
private  variable    x p : A
...
Irreducible⇒≉0 : 0# ≉ 1# → Irreducible p → p ≉ 0#
...

The old version of Irreducible⇒≉0 : 0# ≉ 1# → (∀ {p } → Irreducible p → p ≉ 0#) -- (I)
looks easier to read and understand, to my mind.
Because it looks like a mathematical statement.
(and the change is backwards incompatible. Is it in CHANGELOG ? ).

I had under lib-2.2 a≉0 = Irreducible⇒≉0 0≉1 {a} irred-a
Now Agda-2.8.0+master report "implicit instead of explicit".
I remove curly braces. And it reports "unequal terms".
Then I remove a. Now it is type-checked.
Then I look into Standard library ...

It is frightening to see a variable name which has come somehow from nowhere.
I recall there are many such places in Standard library.
?

[MatthewDaggitt]

So yes, we shouldn't have introduced the breaking change via the variable. I have fixed this in #2774 and will merge it in time for the release.

However, I do not agree about your general point about the use of variables. Variables have greatly reduced the amount of code we need to write in the library. We have strict rules in the style guide to prevent from being overused.

https://github.com/agda/agda-stdlib/blob/master/doc/style-guide.md#variables