Why do I have to give match patterns which don't type check?

[MSoegtrop]

@Lyxia

Program Definition match_typechecktest (n m : nat) : nat :=

Neat! A very nice example of using Program. And it does not use axioms (I checked with Print Assumptions on your definition).Thanks for pointing this out - I would say this is good enough.

@Lyxia

and the reward is meager (it’s merely an implementation detail, most users can just pretend that axiom is not there)

well there is the issue that e.g. axiom K is incompatible with univalence. See the post by @Zimmi48:

What do you think of axioms?

The most famous example of incompatible axioms is (I think) axiom K and univalence. Axiom K makes it easier to pattern match (à la Agda) and univalence is getting more popular as it is supposed to make formal proofs closer to usual mathematics. Equations https://github.com/mattam82/Coq-Equations is an example of plugin that used to rely heavily on axiom K and has been changed to be configurable (and thus usable in a HoTT / UniMath context). A famous of axiom-free library is the math-comp librar…