The Coq mailing list

[Hendrik Boom <hendrik AT topoi.cam.org>]

Deep within the coq reference manual (Section 4.2, Typed Terms),
I find the rule.

Prod: 

        E[G] |- T : Type(i)     E[G::(x:T)] |- U : Type(j)   i <= k   j <= k
       -------------------------------------------------------------------
                          E[G] |- (x:T)U : Type(k)

THe dependency of k on i surprised me.
I had thought that coq would be based on the calculus of constructions
(even the name coq = coc - coquand?) suggests that.
But here I find a constraint that hearkens back to Martin-Lof's
Intuitionistic Theory of Types.

Is this an error in the manual?
Is this a historical accident?
Or, as I fear, is there some deepseated reason why this impredicativity is
forbidden?  Do we encounter inconsistency if we confront impredicativity
with these lovely induction laws?  Or has no one happened to prove 
consistency yet (of the CoC with all the inductions)?

-- hendrik.