[ refactor ] weaken type of Relation.Nullary.Negation.Core.contradiction-irr

[jamesmckinna]

For justification, see CHANGELOG: this is really a consequence of #2199 and subsequent refactorings of Relation.Nullary.Recomputable{.Properties}. Cf. #2346 which might be worth re-opening?

Very little is affected, except that contradiction now needs to be eta-expanded because there is no subtyping between A → B and .A → B.

For candidate use, see the discussion in #2783 .

[JacquesCarette]

Minor but important change. Well spotted.

[jamesmckinna]

Minor but important change. Well spotted.

Thanks! But mostly I'm annoyed with myself that this kind of downstream consequence of my introduction and refactoring of Recomputable could/should have been done more or less straight after #2199 , but I was too tired/distracted to follow through, or remember to loop back to these things until now. Better late than never though!

[MatthewDaggitt]

Was this changed forced? And if so, is this therefore a breaking change?

[jamesmckinna]

Two good questions, to which my evasive, equivocating answers would be: "yes, but...; no, but..."

• re: the change itself: yes, the eta-expansion was forced because of the (lack of!) subtyping issue between A → B and .A → B, BUT the original definition could have been written in eta-expanded form, with equivalent semantics, so it's really an artefact of the (my!) lazy choice not to have done so originally...;
• re: is it breaking: I would argue no, in terms of the behaviour of the exported definition of contradiction itself, as there is no difference to the type, or uses, or call-sites of contradiction; as to contradiction-irr, yes, indeed so as to enable [ add ] new name for flipped version of Relation.Nullary.Negation.Core.contradiction #2784 [ deprecate ] Data.Fin.Base.lower₁ in favour of Data.Fin.Base.lower #2786 [ refactor ] make i ≢ j argument to Data.Fin.Base.punchOut irrelevant #2790 downstream, BUT I would argue that it is a bug that we didn't follow through on the consequences of ⊥ is Recomputable #2199

As in the CHANGELOG, I regard this as a minor improvement : non-breaking, but arguably better move the commentary to non-backwards compatible (at least for the downstream consequences, because the unfolding behaviour of the proposed revised function definitions changes subtly)?

While the suggestion been punted before, I might still argue that the type of contradiction itself should be changed to .A → .(¬ A) → Whatever, but I thought that would be a step too far here... but perhaps one way out is simply to agree here and now that that is what we will do for v3.0 (and get rid of contradiction-irr completely!), and I'll move the milestone on the downstream PRs, but I don't want to have to relitigate these things for a third time then... ;-)