What is the downside of using functional extensionality in COQ

Question

Adding Axioms to COQ often makes proofs easier but also introduces some side effects. For instance, by using the classical axiom one leaves the intuitionistic realm and proofs are no longer computable. My question is, what is the downside of using the functional extensionality axiom?

Answer 1

For me, the drawbacks of using functional extensionality are more or less the same as using any other axiom in Coq: it increases the complexity of the system and how much we need to trust. Although in theory we understand fairly well the logical consequences of working with these well-known axioms (e.g., what combinations of axioms must be avoided to ensure consistency), in practice we are sometimes caught off guard. For instance, it was recently found out that the propositional extensionality axiom was inconsistent with Coq's theory in version 8.4, even though it was widely believed to be consistent. This seemingly natural axiom simply says that equivalent propositions are equal, and is adopted in many Coq developments:

Axiom propositional_extensionality :
  forall P Q : Prop, (P <-> Q) -> P = Q.  

In the answer linked above, Andrej Bauer suggests that this fragility could be related to these axioms not having computation rules associated with them, contrary to the rest of Coq's theory.

Besides this general remark, I've heard people say that having functional extensionality by default could be undesirable because it equates functions with very different computational behaviors (e.g., bubble sort and quick sort), and that we might want to reason about these differences. I personally don't buy this argument, since Coq already equates many values that are computed very differently, such as 0 and 47^1729 - 47 mod 1729. I am not aware of other reasons for not wanting to assume functional extensionality.