Why does noconfusion use equality rather than a recursive call?
Question
Conor McBride defined the noconfusion property of Nat
on page 11 of A Polynomial Testing Principle as:


Why was this defined that way, rather than the following way which works without dependencies?


Context
I still had this question quite near the end of my working through A Polynomial Testing Principle, and it didn’t seem to have been answered: I managed to get through most of the paper without serious problems arising from my different definition.
Answer
Conor immediately follows the definition of NoConf
by defining a canonical way to construct a NoConf
:


If you do it my way instead, you end up unable to use this canonical construction to do proofs by noconfusion.
You probably find yourself proving that succ
is injective manually, and then using that directly instead of via the NoConf
; which defeats the entire purpose of packaging up the noconfusion property into a type.
For example:


What should go here?
We need something of type a + c ≡ a + d
, but all we have in scope is the input succ (a + c) ≡ succ (a + d)
.
That is, we need the noconfusion property for succ
; which suggests that NoConf
should somehow contain an equality type, so that we can use it!
Commentary
I think I only had this question because Nat
is such a simple type.
If there were more constructors and more cases in each patternmatch, it would have been obvious straight away that I had deleted the entire point of the NoConf
construction.