Make irrelevant-recompute unsafe

[jespercockx]

This is the less invasive alternative to #2998, which instead just makes the definitions that are no longer supported unsafe by putting them in a separate Unsafe module that has the --irrelevant-projections flag.

Currently this is based on the experimental branch, which seems to lag a bit behind on master. I tried to bring it up to date but got a bunch of merge conflicts that I didn't know how to solve immediately. If someone else could bring the experimental branch up to date, I'd be glad to rebase this PR on it.

TODO:

• Merge master into this branch
• Add changelog entry

[jamesmckinna]

I guess we'll only bring experimental up-to-date with master once v2.4 has finally been officially released, but in the meantime, I think that a version of this, even less invasive, can be written directly for merging into master? Specifically, is it not safe to refactor this as

⊥-recompute : Recomputable ⊥
⊥-recompute ()

and hence its corollary ¬-recompute is also safe?

[jespercockx]

D'oh, you're absolutely right. I've restored these two functions to safe status.

[jamesmckinna]

Similarly:

• do you want to mirror the current re-import structure, and push the definition of irrelevant-recompute to Data.Irrelevant.Unsafe.recompute (along with the current version of _>>=_ cf. [ refactor ] Make Data.Irrelevant.Irrelevant a proper Monad #2977 ; but I'm not quite sure if we can/should be bothered to reinstate the old version, of type Irrelevant A → (.A → Irrelevant B) → Irrelevant B, except perhaps for backwards compatibility...? Shoutouts to @MatthewDaggitt @JacquesCarette and @gallais for their opinions...)
• also: does this need to be on experimental, or could it simply be pushed to master?

Happy also to myself contribute to this branch, if you are OK with that!

[jespercockx]

I have no strong opinions on the import structure, we should do whatever makes most sense with the design intent behind the rest of the standard library. Feel free to push any changes to this branch if you want!

[JacquesCarette]

I'm fine with just deprecating this entirely (rather than try to reinstate). Data.Irrelevant.Unsafe makes sense. This PR also needs deprecation warnings.

[gallais]

We should get this sorted by the next Agda stdlib meeting

[jamesmckinna]

We should get this sorted by the next Agda stdlib meeting

OK, then I'll ask again whether this needs to be merged into experimental, or whether simply making a change on master would suffice?

[jamesmckinna]

Pro: changes on master

• already have --without-K
• we're fixing a bug, and the upstream fixes to Agda still won't make irrelevant-recompute, join etc. safe

Pro: changes on experimental

• anticipates fix to the bug which introduced all this in the first place
• BUT: contra, see pro above!

I have commits which are fine on master, but on experimental, without the rebase on master, the whole thing is a mess...