UIP (and equivalents like axiom K) must be added axiomatically in Coq if it is desired:
uip : ∀ A (x y: A) (p q: x = y), p = q
This is surprising, since it appears obvious from the definition of equality, which only has one constructor. (This of course rests on the interpretation that an inductive definition in Coq captures all elements of its type).
When one tries to prove UIP, one gets stuck on the reflexive subcase:
uip_refl : ∀ A (x: A) (h: x = x), h = eq_refl x
We might hope the following term would be an appropriate proof term:
fun A (x: A) (h: x = x) =>
match h as h0 in (_ = a) return (h0 = eq_refl x) with
| eq_refl _ => eq_refl (eq_refl x)
end
This fails because it is ill-typed. We know that h: x = x, but when we match on the term, we lose the reflexivity information and it is generalized to h0: x = a. As a result, our return type h0 = eq_refl x is ill-typed.
Why is it that the match construct generalizes our type here? Would a non-generalizing alternative be tractable?
Would a non-generalizing alternative be tractable?
There is precedent for such a match. It is provided in readily available extensions of Coq (in Program; it's also an option in the Equations plugin). Agda also typechecks pattern-matches in a similar manner (if --with-K is enabled, which is the default).
As you've shown, you can define UIP with it, so all the reasons for not adopting UIP carry over to not adopting that match. Conversely that match can be compiled to a term using UIP, as is done by Program and Equations.
I can't really explain why "generalization" makes a difference though. I would bet the answer is in Conor McBride's thesis.