For me, the drawbacks of using functional extensibility are more or less the same with using any other axiom in Coq: it increases the complexity of the system and how much we need to trust. Although theoretically we well understand the logical consequences of working with these well-known axioms (for example, which combinations of axioms should be avoided to ensure consistency), in practice we are sometimes taken by surprise. For example, it was recently discovered that the axiom of the propositional axiom was incompatible with Coca's theory in version 8.4, although it was widely thought to be consistent. This seemingly natural axiom simply says that equivalent sentences are equal and accepted in many Coq designs:
Axiom propositional_extensionality : forall PQ : Prop, (P <-> Q) -> P = Q.
In the answer given above , Andrei Bauer suggests that this fragility may be related to these axioms, not related to them by the rules of computation, contrary to the rest of Kok’s theory.
Beyond this general remark, I heard people say that default functional extensibility may not be desirable because it equates functions with very different computer behaviors (e.g. bubble sorting and quick sorting) and that we might want to reason about these differences . I personally do not buy this argument, since Coq already equates many values that are calculated very differently, for example 0 and 47^1729 - 47 mod 1729 . I do not know of other reasons why I do not want to assume functional extensibility.