Replace irrelevance with Prop

[jespercockx]

As discussed in agda/agda#8557, I made an attempt at replacing the use of irrelevance for the definition of the empty type with Prop. It seems to work rather nicely, with the main disadvantage being that --prop needs to be enabled in basically every file (I haven't yet checked which ones exactly, just enabled it globally for now). On the other hand, this would allow the standard library to adopt the --no-irrelevance flag once agda/agda#8575 is merged.

I'm curious to hear what the standard library developers think of this potential change, in particular @MatthewDaggitt @jamesmckinna @fredrikNordvallForsberg

[jespercockx]

One annoyance when implementing this change is that I could not simply use ⊥ = Irrelevant Empty but had to define Empty as a datatype in Prop instead. It is possible to make things work with the old definition but it requires a bunch of auxiliary definitions so I decided to go for the simpler version instead. It would be possible to go back to defining ⊥ = Irrelevant Empty if/when agda/agda#8548 gets merged.

[Taneb]

Thanks for looking into this! It looks like CI is failing because the README files are a separate Agda library, and also will need --prop enabled throughout. The .agda-lib file is at doc/standard-library-doc.agda-lib.

In addition to Data.Empty, we also use irrelevance for types like NonZero and Positive in Data.Nat, Data,Integer, Data.Rational.Rational, especially in instances. How does instance search interact with Prop? It's not something I've ever taken the time to play with.

As a further point of discussion, do we want to mark things that are provably but not necessarily "obviously" propositional, like _<_ in Data.Nat, as Prop? But that doesn't need to (and probably shouldn't) happen in this PR

[shhyou]

@Taneb Make _<_ live in Prop is similar to asking all _<_ uses be marked as irrelevant (but better), regardless of whether it's stdlib code. I'd argue that this is a huge burden on the clients of _<_ because they can't match on _<_ and have to manually match both indices first.

[jespercockx]

So for other uses of irrelevance for NonZero and Positive and such, I didn't touch them yet because they don't break with my proposed fix for agda/agda#8557. But if we want to migrate the standard library from irrelevance to Prop fully then I agree we should also consider them. There are a few options to migrate them:

• The least invasive change would be to simply replace every function type of the form .A -> B (and .{{x : A}} -> B etc) with Irrelevant A -> B (and {{Irrelevant A}} -> B etc.). This should be a drop-in replacement for irrelevant functions as long as you don't mind the extra verbosity.
• Another possible change would be to update the definition of types such as NonZero and Positive to already include the Irrelevant in their definition. It's less syntactic noise on the use site but you lose the flexibility to not use irrelevance for arguments of this type.
• The third possibility is to actually buy into Prop for user-facing code as well and define NonZero and friends to live in Prop themselves. In some way this is the most elegant (no need to bother with Squash and Irrelevant type wrappers) but you have to deal with the fact that Prop is not Set and many existing functions will not work with it and so need to be duplicated. This is why the Rocq people have been working hard to implement sort polymorphism. Since we don't have that (yet) in Agda I would not recommend this course of action, but I'm mentioning it for completeness' sake.

[jespercockx]

Regarding instance search for Prop: it should work exactly the same as instance search for irrelevant arguments, with the same caveats around it possibly discarding the wrong instances when there are multiple overlapping candidates.

[JacquesCarette]

Doesn't Data.Empty.Polymorphic need the same surgery?

[jespercockx]

Doesn't Data.Empty.Polymorphic need the same surgery?

I don't see any direct use of irrelevance in that file, so I don't think so?

[JacquesCarette]

Oh right, I forgot that that one came from before Empty was made irrelevant.

[JacquesCarette]

So the removal of this function seems to be the biggest change, as far as 'breaking changes' go. Though if this is new to v2.4, it is fine, since that is as-yet unreleased.

[JacquesCarette]

And, of course, the build failed because test-stdlib failed. Maybe --prop can't be compiled, so that's the problem?