What are the negative consequences of extending CIC with axioms? Is it true that adding axioms to the CIC might have negative influences in the computational content of definitions and theorems? I understand that, in the theory's normal behavior, any closed term will reduce to its canonical normal form, e.g. if $n : \mathbb{N}$ is true, then $n$ must reduce to a term of the form $(succ ... (succ (0)))$. But when postulating an axiom - say the function extensionality axiom funext - we just add a new constant to the system

$$ funext : \Pi_{x : A} f (x) = g (x) \to f = g$$

that will just "magically" produces a proof of $f = g$ from any proof of $\Pi_{x : A} f (x) = g (x)$, without any computational meaning at all (in the sense that we cannot extract any code from them?)

But why is this "bad"?

For funext, I read in this coq entry and this mathoverflow question that it will cause the system to either loose canonicity or decidable checking. The coq entry seems to present a good example, but I still would like some more references on that - and somehow I can't find any.

How is that adding extra axioms could cause CIC to have a worse behavior? Any practical examples would be great. (For example, the Univalence Axiom?)
I am afraid in this question is too soft, but if anyone could shed some light on those issues or give me some references would be great!



PS: The coq entry mentions that "Thierry Coquand already observed that pattern matching over intensional families is inconsistent with extensionality in the mid 90ies." Does anyone know in which paper or something?
One first reason to reject axioms is that they might be inconsistent. Even for the axioms that are proved consistent, some of them have a computational interpretation (we know how to extend definitional equality with a reduction principle for them) and some do not -- those break canonicity. This is "bad" for different reasons:


In theory, canonicity lets you prove things about the values of your language, without having to go to a specific model. This is a very satisfying property to have thinking about your system; in particular, it supports claims about the real world -- we can think of the nat type as formalized in the system as really "natural numbers" because we can prove that its closed normal inhabitants really are natural numbers. Otherwise it's easy to think that you modelled something correctly in your system, but actually be working with different objects.
In practice, reduction is a major asset of dependent type theories, because it makes proof easy. Proving a propositional equality can be arbitrarily difficult, while proving a definitional equality is (less often possible) but much easier, as the proof term is trivial. More generally, computation is a core aspect of the user experience of a proof assistant, and it is common to define things just so they reduce correctly as you expect. (You don't need axioms to make computation difficult; for example, using the conversion principle on propositional equalities can already block reductions). The entire business of proof by reflection is based on the use of computation to help proofs. This is a major difference in power and convenience with respect to other logics-based proof assistant (eg. HOL-light, which only supports equality reasoning; or see Zombie for a different approach), and using unchecked axioms, or other programming styles, can get you out of this comfort zone.