β¦probably. To be clear, ECIC^{1} refers to Monnier and Bosβ Erasable CIC^{2}, with erasable in the sense of erasable pure type systems (EPTS)^{3}. Iβll argue that even with erased impredicative fields, Coquandβs paradox of trees^{4} is still typeable.
ECIC
I wonβt go too much into detail on the definition of ECIC, but Iβll touch on some key rules and examples. In short, ECIC is CIC, but:
 Function arguments can be erased or normal;
 Erased arguments may only appear in type annotations that are erased prior to evaluation^{5};
 Inductives may only live in Prop;
 Large arguments of constructors must be erased; and
 There are no restrictions on what inductives may be eliminated into^{6}.
They claim that erasure of large arguments is what permits unrestricted inductive elimination, but I believe that this is still inconsistent.
To establish some syntax, hereβs the typing rule for function types and functions with erased arguments, where $\cdot$ is the erasure of a term, which erases type annotations as well as erased arguments entirely.
$\frac{ \Gamma \vdash \tau_1 : s_1 \qquad \Gamma, x : \tau_1 \vdash \tau_2 : s_2 \qquad (k, s_1, s_2, s_3) \in \mathcal{R} }{ \Gamma \vdash (x :^k \tau_1) \to \tau_2 : s_3 } \qquad \frac{ \Gamma, x : \tau_1 \vdash e : \tau_2 \qquad x \notin \mathsf{fv}( e ) }{ \Gamma \vdash \lambda x :^{\mathbf{\mathsf{e}}} \tau_1. e : (x :^{\mathbf{\mathsf{e}}} \tau_1) \to \tau_2 }$The PTS rules $\mathcal{R}$ are $(k, \mathsf{\textcolor{#069}{Prop}}, s, s)$, $(k, \mathsf{\textcolor{#069}{Type}}_{\ell_1}, \mathsf{\textcolor{#069}{Type}}_{\ell_2}, \mathsf{\textcolor{#069}{Type}}_{\ell_1 \sqcup \ell_2})$, and most importantly, $(\mathsf{e}, \mathsf{\textcolor{#069}{Type}}_\ell, \mathsf{\textcolor{#069}{Prop}}, \mathsf{\textcolor{#069}{Prop}})$. The last rule says that if you want to use something large for a proposition, it must be erasable, and therefore only used in type annotations. A key theorem states that if a term is typeable is CIC, then itβs typeable in ECIC with additional erasure annotations, meaning that CIC inherently never uses impredicativity in computationally relevant ways.
The typing rules for inductives and especially their case expressions, as usual, are rather involved, and I wonβt repeat them here. Instead, to establish its syntax, hereβs an example defining propositional equality as an inductive, and a proof that itβs symmetric. From here onwards Iβll use square brackets to indicate erased arguments, omitting annotations entirely, as well as $\cdot \to \cdot$ as a shorthand for nondependent function types.
$\begin{align*} \mathsf{\textcolor{#bf616a}{Eq}} &: [A : \mathsf{\textcolor{#069}{Type}}] \to [A] \to [A] \to \mathsf{\textcolor{#069}{Prop}} \\ &\coloneqq \lambda [A : \mathsf{\textcolor{#069}{Type}}]. \lambda [x : A]. \mathsf{\textcolor{#069}{Ind}}(\textit{Eq} : [A] \to \mathsf{\textcolor{#069}{Prop}})\langle 0: \textit{Eq} \; [x] \rangle \\ \mathsf{\textcolor{#bf616a}{Refl}} &: [A : \mathsf{\textcolor{#069}{Type}}] \to [x : A] \to \mathsf{\textcolor{#bf616a}{Eq}} \; [A] \; [x] \; [x] \\ &\coloneqq \lambda [A : \mathsf{\textcolor{#069}{Type}}]. \lambda [x : A]. \mathsf{\textcolor{#069}{Con}}(0, \mathsf{\textcolor{#bf616a}{Eq}} \; [A] \; [x]) \\ \mathsf{\textcolor{#bf616a}{sym}} &: [A : \mathsf{\textcolor{#069}{Type}}] \to [x : A] \to [y : A] \to (p : \mathsf{\textcolor{#bf616a}{Eq}} \; [A] \; [x] \; [y]) \to \mathsf{\textcolor{#bf616a}{Eq}} \; [A] \; [y] \; [x] \\ &\coloneqq \lambda [A : \mathsf{\textcolor{#069}{Type}}]. \lambda [x : A]. \lambda [y : A]. \lambda p : \mathsf{\textcolor{#bf616a}{Eq}} \; [A] \; [x] \; [y]. \\ &\phantom{\coloneqq} \mathsf{\textcolor{#069}{Case}} \; p \; \mathsf{\textcolor{#069}{return}} \; \lambda [z : A]. \lambda p : \mathsf{\textcolor{#bf616a}{Eq}} \; [A] \; [x] \; [z]. \mathsf{\textcolor{#bf616a}{Eq}} \; [A] \; [z] \; [x] \; \mathsf{\textcolor{#069}{of}} \; \langle 0: \mathsf{\textcolor{#bf616a}{Refl}} \; [A] \; [x] \rangle \end{align*}$This equality is over large terms to be able to talk about both equal propositions and equal proofs^{7}, so basically all arguments except for equality itself must be erased. However, it still doesnβt qualify as a large inductive, since none of the constructor arguments are large, i.g. have types in sort $\mathsf{\textcolor{#069}{Type}}$. Contrariwise, the following inductive is large, requiring its first constructor argument to be erased to justify unrestricted elimination.
$\mathsf{\textcolor{#bf616a}{U}} : \mathsf{\textcolor{#069}{Prop}} \coloneqq \mathsf{\textcolor{#069}{Ind}}(\textit{U} : \mathsf{\textcolor{#069}{Prop}})\langle [X : \mathsf{\textcolor{#069}{Prop}}] \to (X \to \textit{U}) \to \textit{U} \rangle$Digression: Rocqβs $\mathsf{\textcolor{#069}{Prop}}$ and $\mathsf{\textcolor{#069}{Set}}$
ECICβs $\mathsf{\textcolor{#069}{Prop}}$ is neither like Rocqβs $\mathsf{\textcolor{#069}{Prop}}$ nor like its impredicative $\mathsf{\textcolor{#069}{Set}}$, which Iβll call $\mathsf{\textcolor{#069}{rProp}}$ and $\mathsf{\textcolor{#069}{rSet}}$ to avoid confusion. Large inductives in either $\mathsf{\textcolor{#069}{rProp}}$ and $\mathsf{\textcolor{#069}{rSet}}$ are not allowed to be strongly eliminated, because this would be inconsistent. Furthermore, as members of types of sort $\mathsf{\textcolor{#069}{rProp}}$ are intended to be erased during extraction, inductives in $\mathsf{\textcolor{#069}{rProp}}$ with multiple constructors canβt be strongly eliminated either, so that case expressions only have a single branch to which they erase. This makes eCICβs $\mathsf{\textcolor{#069}{Prop}}$, confusingly, exactly Rocqβs impredicative $\mathsf{\textcolor{#069}{Set}}$.
The paradox of trees
Coquandβs paradox of trees develops an inconsistency out of the inductive $\mathsf{\textcolor{#bf616a}{U}}$ above by showing that simultaneously all $\mathsf{\textcolor{#bf616a}{U}}$ are well founded and there exists a $\mathsf{\textcolor{#bf616a}{U}}$ that is not well founded, in particular $\mathsf{\textcolor{#bf616a}{loop}}$ below.
$\begin{align*} \mathsf{\textcolor{#bf616a}{loop}} : \mathsf{\textcolor{#bf616a}{U}} \coloneqq \mathsf{\textcolor{#069}{Con}}(0, \mathsf{\textcolor{#bf616a}{U}}) \; [U] \; (\lambda x : U. x) \end{align*}$$\mathsf{\textcolor{#bf616a}{U}}$ is injective
Before we continue, we need an injectivity lemma saying that if two $\mathsf{\textcolor{#bf616a}{U}}$s are equal, then their components are equal too. I omit the $\mathsf{\textcolor{#069}{return}}$ expression in the body because itβs already in the type. Importantly, when matching on the $\mathsf{\textcolor{#bf616a}{U}}$s, the large, erased first argument of the constructor is only used in erased positions.
$\begin{align*} \mathsf{\textcolor{#bf616a}{injU}} &: (u_1 : \mathsf{\textcolor{#bf616a}{U}}) \to (u_2 : \mathsf{\textcolor{#bf616a}{U}}) \to (p : \mathsf{\textcolor{#bf616a}{Eq}} \; [\mathsf{\textcolor{#bf616a}{U}}] \; [u_1] \; [u_2]) \to \\ &\phantom{:} \mathsf{\textcolor{#069}{Case}} \; u_1 \; \mathsf{\textcolor{#069}{return}} \; \lambda u : \mathsf{\textcolor{#bf616a}{U}}. \mathsf{\textcolor{#069}{Prop}} \; \mathsf{\textcolor{#069}{of}} \; \langle \lambda [X_1 : \mathsf{\textcolor{#069}{Prop}}]. \lambda f_1 : X_1 \to \mathsf{\textcolor{#bf616a}{U}}. \\ &\phantom{:} \mathsf{\textcolor{#069}{Case}} \; u_2 \; \mathsf{\textcolor{#069}{return}} \; \lambda u : \mathsf{\textcolor{#bf616a}{U}}. \mathsf{\textcolor{#069}{Prop}} \; \mathsf{\textcolor{#069}{of}} \; \langle \lambda [X_2 : \mathsf{\textcolor{#069}{Prop}}]. \lambda f_2 : X_2 \to \mathsf{\textcolor{#bf616a}{U}}. \\ &\phantom{:} \exists q : \mathsf{\textcolor{#bf616a}{Eq}} \; [\mathsf{\textcolor{#069}{Prop}}] \; [X_1] \; [X_2]. \\ &\phantom{: \exists q :} \mathsf{\textcolor{#bf616a}{Eq}} \; [X_2 \to \mathsf{\textcolor{#bf616a}{U}}] \; \\ &\phantom{: \exists q : \mathsf{\textcolor{#bf616a}{Eq}}} \; [\mathsf{\textcolor{#069}{Case}} \; q \; \mathsf{\textcolor{#069}{return}} \; \lambda [Z : \mathsf{\textcolor{#069}{Prop}}]. \lambda q : \mathsf{\textcolor{#bf616a}{Eq}} \; [\mathsf{\textcolor{#069}{Prop}}] \; [X_1] \; [Z]. Z \to U \; \mathsf{\textcolor{#069}{of}} \; \langle f_1 \rangle] \; \\ &\phantom{: \exists q : \mathsf{\textcolor{#bf616a}{Eq}}} \; [f_2] \rangle \rangle \\ &\coloneqq \lambda u_1 : \mathsf{\textcolor{#bf616a}{U}}. \lambda u_2 : \mathsf{\textcolor{#bf616a}{U}}. \lambda p : \mathsf{\textcolor{#bf616a}{Eq}} \; [\mathsf{\textcolor{#bf616a}{U}}] \; [u_1] \; [u_2]. \\ &\phantom{\coloneqq} \mathsf{\textcolor{#069}{Case}} \; p \; \mathsf{\textcolor{#069}{of}} \; \langle \mathsf{\textcolor{#069}{Case}} \; u_1 \; \mathsf{\textcolor{#069}{of}} \; \langle \lambda [X : \mathsf{\textcolor{#069}{Prop}}]. \lambda f : X \to \mathsf{\textcolor{#bf616a}{U}}. (\mathsf{\textcolor{#bf616a}{Refl}} \; [\mathsf{\textcolor{#069}{Prop}}] \; [X] , \mathsf{\textcolor{#bf616a}{Refl}} \; [X \to \mathsf{\textcolor{#bf616a}{U}}] \; [f]) \rangle \rangle \end{align*}$The equalities make its statement a bit convoluted,
but the proof is ultimately a pair of reflexivities.
It would perhaps be clearer to see the equivalent Rocq proof,
which uses rew
notations to make it cleaner.
Here, I need to turn off universe checking when defining the inductive
to prevent Rocq from disallowing its strong elimination.
Notably, this is the only place where turning off universe checking is required,
and the type of $\mathsf{\textcolor{#bf616a}{injU}}$ is the only place where strong elimination occurs.
Import EqNotations.
Unset Universe Checking.
Inductive U : Prop := u (X : Prop) (f : X > U) : U.
Set Universe Checking.
Definition loop : U := u U (fun x => x).
Definition injU [u1 u2 : U] (p : u1 = u2) :
match u1, u2 with
 u X1 f1, u X2 f2 =>
exists (q : X1 = X2),
rew [fun Z => Z > U] q in f1 = f2
end :=
rew dependent p in
match u1 with
 u _ _ => ex_intro _ eq_refl eq_refl
end.
$\mathsf{\textcolor{#bf616a}{U}}$s are well founded
The wellfoundedness predicate is another inductive stating that a $\mathsf{\textcolor{#bf616a}{U}}$ is well founded if all of its children are. Wellfoundedness for all $\mathsf{\textcolor{#bf616a}{U}}$ is easily proven by induction.
$\begin{align*} \mathsf{\textcolor{#bf616a}{WF}} &: \mathsf{\textcolor{#bf616a}{U}} \to \mathsf{\textcolor{#069}{Prop}} \\ &\coloneqq \mathsf{\textcolor{#069}{Ind}}(\textit{WF} : \mathsf{\textcolor{#bf616a}{U}} \to \mathsf{\textcolor{#069}{Prop}}) \langle 0: [X : \mathsf{\textcolor{#069}{Prop}}] \to (f : X \to U) \to ((x : X) \to \textit{WF} \; (f \; x)) \to \textit{WF} \; (\mathsf{\textcolor{#069}{Con}}(0, \mathsf{\textcolor{#bf616a}{U}}) \; [X] \; f) \rangle \\ \mathsf{\textcolor{#bf616a}{wfU}} &: (u : \mathsf{\textcolor{#bf616a}{U}}) \to \mathsf{\textcolor{#bf616a}{WF}} \; u \\ &\coloneqq \mathsf{\textcolor{#069}{Fix}}_0 \; \textit{wfU} : (u : \mathsf{\textcolor{#bf616a}{U}}) \to \mathsf{\textcolor{#bf616a}{WF}} \; u \; \mathsf{\textcolor{#069}{in}} \; \lambda u : \mathsf{\textcolor{#bf616a}{U}}. \\ &\phantom{\coloneqq} \mathsf{\textcolor{#069}{Case}} \; u \; \mathsf{\textcolor{#069}{return}} \; \lambda u : \mathsf{\textcolor{#bf616a}{U}}. \mathsf{\textcolor{#bf616a}{WF}} \; u \; \mathsf{\textcolor{#069}{of}} \; \langle 0: \lambda [X : \mathsf{\textcolor{#069}{Prop}}]. \lambda f : X \to \mathsf{\textcolor{#bf616a}{U}}. \mathsf{\textcolor{#069}{Con}}(0, \mathsf{\textcolor{#bf616a}{WF}}) \; [X] \; f \; (\lambda x : X. \textit{wfU} \; (f \; x)) \rangle \end{align*}$Again, hereβs the equivalent definitions in Rocq. Thereβs no need to turn off universe checking this time since we wonβt be strongly eliminating $\mathsf{\textcolor{#bf616a}{WF}}$.
Inductive WF : U > Prop :=
 wf : forall X f, (forall x, WF (f x)) > WF (u X f).
Fixpoint wfU (u : U) : WF u :=
match u with
 u X f => wf X f (fun x => wfU (f x))
end.
$\mathsf{\textcolor{#bf616a}{loop}}$ is not well founded
Showing nonwellfoundedness of $\mathsf{\textcolor{#bf616a}{loop}}$ is more complicated, not because itβs an inherently difficult proof, but because it requires manually unifying indices. In fact, the whole proof in Agda is quite simple.
{# NO_UNIVERSE_CHECK #}
data U : Set where
u : (X : Set) β (X β U) β U
data WF : U β Setβ where
wf : β (X : Set) (f : X β U) β (β x β WF (f x)) β WF (u X f)
loop = u U (Ξ» x β x)
nwf : WF loop β β₯
nwf (wf X f h) = nwf (h loop)
Destructing $\mathsf{\textcolor{#bf616a}{WF}} \; \mathsf{\textcolor{#bf616a}{loop}}$ as $\mathsf{\textcolor{#bf616a}{WF}} \; [X] \; f \; h$, we know that $X$ is $\mathsf{\textcolor{#bf616a}{U}}$ and $f$ is $\lambda x : \mathsf{\textcolor{#bf616a}{U}}. x$. In Rocq, we have the help of tactics and dependent induction, as well as $\mathsf{\textcolor{#bf616a}{injU}}$ proven earlier to explicitly unify indices.
Require Import Coq.Program.Equality.
Lemma nwf (u : U) (p : u = loop) (wfl : WF u) : False.
Proof.
dependent induction wfl.
apply injU in p as [q r].
simpl in q. subst.
simpl in r. subst.
eapply H0. reflexivity.
Qed.
But writing the same proof in plain ECIC is a challenge,
especially as the proof term generated for nwf
is disgusting.
Iβve simplified it to the following to the best of my ability,
still using copious amounts of rew
.
Fixpoint nwf (wfl : WF loop) : False :=
match wfl in WF u' return loop = u' > False with
 wf _ f h => fun p => let (q , r) := injU p in
(rew dependent [fun _ q => forall f,
rew [fun Z => Z > U] q in (fun x => x) = f
> (forall x, WF (f x))
> False] q
in fun _ r =>
rew [fun f => (forall x, WF (f x)) > False] r
in fun h => nwf (h loop)) f r h
end eq_refl.
I wonβt bother trying to typeset that in ECIC, but I hope itβs convincing enough as an argument that the corresponding definition would still type check and that erasure isnβt violated, i.e. that the $\mathsf{\textcolor{#069}{Prop}}$ argument from the $\mathsf{\textcolor{#bf616a}{WF}}$ isnβt used in the body of the proof. This proof doesnβt even use strong elimination, either: the return type of every case expression lives in $\mathsf{\textcolor{#069}{Prop}}$.
Why isnβt ECIC consistent?
The proof sketch above tells us how ECIC isnβt consistent, but we still need to understand why it isnβt consistent. ECICβs original argument was that
forcing impredicative fields to be erasable also avoids this source of inconsistency usually avoided with the $\Gamma \vdash e \; \mathsf{small}$ constraint.
Said source refers to the ability for large impredicative inductives with strong elimination to hide a larger type within a smaller construction thatβs then used later. The idea is that if the impredicative field is erased, then surely it canβt be meaningfully used later as usual to construct an inconsistency. Here, Iβve shown that it can be meaningfully used even if it canβt be used relevantly, because all we need is to be able to refer to them in propositions and proofs. It doesnβt really make sense anyway that the computational relevance of a term should have any influence on propositions, which arguably exist independently of whether they can be computed.
Then why is strong elimination inconsistent with impredicativity, if computational relevance isnβt the reason? I believe that the real connection is between impredicativity and proof irrelevance, from which computational irrelevance arises. After all, $\mathsf{\textcolor{#069}{Prop}}$ is often modelled proofirrelevantly as a twoelement set $\{ \top , \bot \}$, collapsing all of its types to truthhood or falsehood and disregarding those typesβ inhabitants. Other times, $\mathsf{\textcolor{#069}{Prop}}$ is defined as the universe of mere propositions, or the universe of types such that their inhabitants (if any) are all propositionally equal.
Under this view, impredicativity is permitted, although not necessary, because referring to larger information ought to be safe so long as thereβs no way to use that information to violate proof irrelevance. Strong elimination commits this violation because, as seen in $\mathsf{\textcolor{#bf616a}{injU}}$, it allows us to talk about the identity (or nonidentity) of larger terms, even if the way we talk about it is proofirrelevantly. Concretely, the contrapositive of $\mathsf{\textcolor{#bf616a}{injU}}$ lets us distinguish two $\mathsf{\textcolor{#bf616a}{U}}$s as soon as we have two provably unequal types, such as $\top$ and $\bot$, from which we can provably distinguish $\mathsf{\textcolor{#069}{Con}}(0, \mathsf{\textcolor{#bf616a}{U}}) \; [\top] \; (\lambda \_. \mathsf{\textcolor{#bf616a}{loop}})$ and $\mathsf{\textcolor{#069}{Con}}(0, \mathsf{\textcolor{#bf616a}{U}}) \; [\bot] \; (\lambda b. \mathsf{\textcolor{#069}{Case}} \; b \; \mathsf{\textcolor{#069}{of}} \; \langle \rangle)$.
Interestingly, even without strong elimination of large inductives, proof irrelevance can still be violated by strong elimination of a small inductive with two constructors, since that would enable proving the two constructors unequal. The only way an inconsistency arises is if proof irrelevance is explicitly internalized. This is why the axiom of excluded middle is inconsistent in the presence of strong elimination in this setting: Berardiβs paradox^{8} says that EM implies proof irrelevance. I think thereβs something profound in this paradox that I havenβt yet grasped, because connects two different views of a proposition: as something that is definitively either true or false, or as something that carries no other information than whether it is true or false.

Not to be confused with their eCIC, the erasable CIC.Β ↩

Stefan Monnier; Nathaniel Bos. Is Impredicativity Implicitly Implicit? TYPES 2019. doi:10.4230/LIPIcs.TYPES.2019.9.Β ↩

Nathan MishraLinger; Tim Sheard. Erasure and polymorphism in pure type systems. FOSSACS 2008. doi:10.5555/1792803.1792828.Β ↩

Thierry Coquand. The paradox of trees in type theory. BIT 32 (1992). doi:10.1007/BF01995104.Β ↩

Also called runtime erasure, runtime irrelevance, computational irrelevance, or external erasure.Β ↩

Also called the noSELIT (strong elimination of large inductive types) rule.Β ↩

ECIC doesnβt formally have cumulativity, but we can use our imaginations.Β ↩

Barbanera, Franco; Berardi, Stefano. JFP 1996. Proofirrelevance out of excluded middle and choice in the calculus of constructions. doi:10.1017/S0956796800001829.Β ↩