What is the role of the Bicolored Calculus of Constructions?

Question

So, I'm reading a bit about elaboration, particularly, algorithms based on the Bicolored Calculus of Construction, and I'm a bit confused. I don't understand what exactly the purpose of the $CC^{bi}$ is. It seems to be identical to $CC$ except there is a distinction between implicit and explicit arguments for functions. In particular, I don't see how it allows you to write $(id\; 0)$ instead of $(id\; \mathbb{N}\; 0)$. If we assume a system for global definitions, then,

$id : (\Pi A\; |\; \mathsf{Type}\; . (\Pi x : A\; . A))$

and

$id = (\lambda A\; |\; \mathsf{Type}\; . (\lambda x : A . x))$.

Do the rules really allow for $(id\; 0)$? Of course the syntax does, but I don't see it in the typing relation. Am I missing something? Am I understanding the role of $CC^{bi}$ incorrectly?

Also, isn't the property of confluence lost? I guess my problem is that I'm reading about elaboration without having read much about $CC^{bi}$ before this. What's a good paper that introduces it and it alone?

Edit: To be more specific, I am asking how $(id\; 0)$ is accepted in place of $(id\; \mathbb{N}\; 0)$ when the rules for both explicit and implicit $\Pi$ application are identical modulo sytnax. I see no difference between $:$ and $|$ the rules for both seem the same.

Edit: I am not talking about the Implicit Calculus of Constructions, which is a different theory and has different rules for explicit $\Pi$'s (application vs. generation.)

Edit: Okay, I think I'm starting to understand this but I won't answer this question until I'm sure. Basically $(id\; 0)$ does not type check and in fact it is just elaborated to $(id\; \mathbb{N}\; 0)$ right before type checking or done as a secondary responsbility of the type checking algorithm. Essentially these implicit calculi are intended to be interface (user-end) languages which are elaborated into the usual (explicit) calculi or at least the explicit fragment of the implicit calculi before the terms are type checked. If that is the case, then I think I see the big picture. Can someone please confirm this?

Answer 1

In The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping, Alexandre Miquel introduces the basic concepts for the Implicit Calculus of Constructions, which I believe is synonymous with the Bicolored Calculus of Constructions.

The point is (among other things) to have a calculus without the clutter of explicit type annotations everywhere. Type inference is (very likely to be) undecidable though.

In this calculus, if we take $id=\lambda x. x$, then you can derive $$ \vdash id\colon \forall X\colon Type. X\rightarrow X$$ by simply using the explicit product and the implicit product rules in succession. Then the instantiation rule for the implicit product allows $$ \vdash id\colon Nat\rightarrow Nat $$ and so $$ \vdash id\ 0 \colon Nat$$ The system admits subject reduction and confluence, even on untyped terms (which in fact fails for calculi with abstraction annotations). All this can be found in Alexandre's thesis, which is sadly in French. Not sure I have a better reference for these results though I'm afraid.