[ refactor ] make contradiction and friends entirely definitionally proof-irrelevant
#2802
Conversation
| length zs ≤⟨ ℕ.n≤1+n (length zs) ⟩ | ||
| length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩ | ||
| length ys₁ ∎) $ ℕ.<-irrefl ≡.refl | ||
| length ys₁ ∎) (ℕ.<-irrefl ≡.refl) |
There was a problem hiding this comment.
perhaps don't roll in such pure, non-breaking style changes in to something breaking and make a separate (if tiny) PR?
There was a problem hiding this comment.
Not a style change; it's yet another 'feature' of irrelevant function spaces: _$_ is no longer well-typed!
There was a problem hiding this comment.
So do we need a new variant for _$_ that would be?
|
Thanks @JacquesCarette for the speedy feedback (on a For most of your queries, eta-expansion is needed because there's no (contravariant) subtyping between As for the ones which seemingly contradict #2653 , see #2803 : don't use |
jamesmckinna
added
the
status: blocked-by-issue
|
Reconsidering whether this is even worthwhile: logically it makes sense, but ergonomically, it's such a pain. |
|
Reading this code, I get the same impression: ergonomically, agda's proof irrelevance leaves much to be desired. Is there any conclusion from here that can be up-streamed? |
2 participants
The inevitable
breakingconsequence of #2785 , designed as a 'cleaning of the stables'.Cf. #2346 whose intention it follows.
Currently duplicates functionality from #2803 ; will tidy up once that is merged.
Downstream consequence:
contradictioninternally need eta-expansion (and this may be regarded as a UX failure...?)stdlibthat I can find)TODO:
contradiction-irrintroduced as consequences of [ refactor ] weaken type ofRelation.Nullary.Negation.Core.contradiction-irr#2785Consider also:
Relation.Nullary.Reflectsto make its various arguments definitionally proof-irrelevantRelation.Nullary.Negation.Core._¬-⊎_in favour ofcontradiction₂, or else change its type as well; its one use instdlibis inReflects, so could be refactored in any case via¬-recomputeand inlining...