[ refactor ] Make Data.Irrelevant.Irrelevant a proper Monad

[jamesmckinna]

This is prompted by this comment and @gallais 's introduction of the λ∙ operator which shifts irrelevant application to ordinary application. In some sense, this PR offers the converse operation, provided the codomain is Irrelevant.

Rationale:

• type of Data.Irrelevant._>>=_ now has that of a 'proper' monadic bind operator, which increases the range of its applicability wrt its type, but also permits the use of do-notation etc. downstream

Details:

• irrelevant-recompute moves (as recompute) to Data.Irrelevant
• is (currently) re-exported with its old name from Relation.Nullary.Recomputable
• but could be deprecated, although to do so might introduce awkward dependency mangling

Badged as v2.4, because AFAICT this is a backwards-compatible (if fiddly) change.

Potential consequences: downstream, we can reconsider all (?) uses of the . modality in favour of the Irrelevant modality, and otherwise leave it encapsulated in Data.Irrelevant?

[Taneb]

This looks very useful!

[JacquesCarette]

Up to naming, I think this is a great change.

[gallais]

I did not like the original names but could not think of any fix.
The new ones make a lot of sense!

[jamesmckinna]

Thanks everyone!