我认为加利纳语言的每个有效术语都有一个与之相关的类型。 但是，有没有被Coq接受而没有被输入的术语？
这主要是关于一些翻译的东西，但(我认为(也是一件有趣的事情。
正如Yves和gallais所说，除了系统中的错误之外，Coq接受的每个Gallina术语都有一个类型。 这几乎是按照定义;说Coq接受t术语就是说Check t不会失败，我们可以观察到Check t总是会打印一种t。 现在，可能是Check t打印的类型输入不正确，但这又是系统中的错误，我从未见过它发生(只要符号不妨碍打印的可逆性(。
但是，有几件事与您提出的问题很接近，您可能会感兴趣。
宇宙
在Coq中，我们可以写
Universe i.
Check Type@{i}.
然而，尽管i是一个有效的宇宙，但Check i失败了，i没有加利纳术语具有类型的类型。
请注意，在阿格达语中，我们可以写
postulate foo : (i : Level) → Set i
阿格达检查器接受这一点，但如果我们写
bar = (i : Level) → Set i
我们收到错误消息Setω is not a valid type。 Coq没有这个问题，因为Coq中的宇宙不是项，Coq中的宇宙多态性是prenex。
受试者减少损失
Coq有一些极端情况(可能也称为bug(，其中主题减少丢失。 也就是说，有一些类型良好的术语在减少它们时会变得类型错误。 例如，请参阅错误 #6768，它给出了代码
CoInductive I := C : I -> I.
CoFixpoint infty := C infty.
Definition unfold : infty = C infty :=
match infty as x return match x with C n => x = C n end with
| C n => eq_refl (C n)
end.
Fail Definition nf_unfold : infty = C infty := Eval lazy in unfold.
请注意，即使没有类型注释，我们也会收到这样的错误，例如
Axiom id : forall {T}, T -> T.
Definition nf_unfold := Eval lazy in id unfold.
(*Error: Illegal application:
The term "@id" of type "forall T : Type, T -> T"
cannot be applied to the terms
"(cofix infty : I := C infty) = C (cofix infty : I := C infty)" : "Prop"
"eq_refl"
: "C (cofix infty : I := C infty) = C (cofix infty : I := C infty)"
The 2nd term has type
"C (cofix infty : I := C infty) = C (cofix infty : I := C infty)"
which should be coercible to
"(cofix infty : I := C infty) = C (cofix infty : I := C infty)".
*)
这不完全是你要问的，但它似乎是相关的。
自引用类型
所有术语都有类型，但并非所有术语都具有您希望它们的类型。 例如，给定A : Type和B : A -> Type，您可能希望写下具有类型的术语f
forall b : bool, if b then A else B (f true)
当然，Coq不接受这一点，但我们可以定义具有这种类型的术语。 例如，给定A、B和x : @sigT A B，Coq接受
Definition f := fun b : bool => if b return if b then _ else _
then projT1 x else projT2 x.
Check f : forall b : bool, if b then A else B (f true).
无法陈述的定理的证明
早在Coq有明确的宇宙变量之前，我想证明函数外延性是向下闭合的。 也就是说，我想证明定理
Set Universe Polymorphism.
Definition funext_at@{i} := forall (A B : Type@{i}) (f g : A -> B),
(forall x, f x = g x) -> f = g.
Universes i j.
Constraint j <= i.
Theorem funext_downward_closed : funext_at@{i} -> funext_at@{j}.
但是，没有办法陈述这个定理。 我只能写
Theorem funext_downward_closed : funext -> funext.
不过，我仍然设法证明了这个定理(参见HoTT/HoTT库中的这个提交和这个提交以及这个问题(，通过写下证明项，然后检查定理以查看宇宙约束是否正确。 我开玩笑地说，我已经证明了一个不可言说的定理。
不，微积分的每个术语都必须正确键入。