What is a clean algorithm to recover a CC term from an untyped one and its CC type?

Suppose I have an untyped term, such as:

data Term = Lam Term | App Term Term | Var Int

-- λ succ . λ zero . succ zero
c1 = (Lam (Lam (App (Var 1) (Var 0)))

-- λ succ . λ zero . succ (succ zero)
c2 = (Lam (Lam (App (Var 1) (App (Var 1) (Var 0))))

-- λ succ . λ zero . succ (succ (succ zero))
c3 = (Lam (Lam (App (Var 1) (App (Var 1) (App (Var 1) (Var 0)))))

-- λ cons . λ nil . cons 1 (cons 2 (cons 3 nil))
term_untyped = (Lam (Lam (App (App (Var 1) c1) (App (App (Var 1) c2 (App (App (Var 1) c3) Nil)

And its CC type:

data Type = Set | All Type Type | Var Int

-- ∀ (P : *) -> ∀ (Succ : P -> P) -> ∀ (Zero : P) -> P
nat = All(Set, All(All(Var(0), Var(1)), All(Var(0), Var(1))))

-- ∀ (P : *) -> ∀ (Cons : x -> P -> P) -> ∀ (Nil : P) -> P
list x = All(Set, All(All(x, All(Var(0), Var(1))), All(Var(0), Var(0))))

-- term_type
term_type = list nat

Is there a clean algorithm that will recover the CC term corresponding to the untyped one? I.e.,

data CCTerm 
   = Lam CCTerm CCTerm 
   | All CCTerm CCTerm 
   | App CCTerm CCTerm 
   | Set 
   | Var Int

term_typed :: Term -> CCTerm
term_typed = from_untyped term_type term_untyped

-- As the result, typed_term would be:
-- λ (P : *) ->
-- λ (Cons : ∀ (x : (∀ (Q : *) -> (Q -> Q) -> Q -> Q)) -> P -> P) ->
-- λ (Nil : P) ->
-- ( Cons (λ (Q : *) -> λ (Succ : Q -> Q) -> (Zero : Q) -> Succ Zero)
-- ( Cons (λ (Q : *) -> λ (Succ : Q -> Q) -> (Zero : Q) -> Succ (Succ Zero))
-- ( Cons (λ (Q : *) -> λ (Succ : Q -> Q) -> (Zero : Q) -> Succ (Succ (Succ Zero)))
--   Nil)))

I tried some things, but soon noticed it is not obvious how to pass the type around. Specifically, the Lam case seems to require a forall type and append it to context, the function of the App case seems to produce a forall type which is used by the argument, and the Var case seems to query a type on context. That asymmetry made my code a little messy, so I wonder if there is an obvious way to implement this.

Solution

You can't have beta redexes in the input, because you can't principally infer types for lambdas, but otherwise it's just standard bidirectional type checking. If it's known that the input is well-typed with the type, then you can skip conversion checking. Pseudocode:

check : Term → Type → Cxt → CCTerm
check (λ x. t) ((x : A) → B) Γ = λ (x : A). check t B (Γ, x : A)
check t        A             Γ = fst (infer t Γ) -- no conv check

infer : Term → Cxt → (CCTerm, Type)
infer (λ x.t) Γ = undefined
infer x       Γ = (x, lookup x Γ)
infer (t u)   Γ = (t' u', B[x ↦ u'])
  where (t', ((x : A) → B)) = infer t Γ
        u' = check u A Γ

(Convert this to de Bruijn indices and possiby faster All substitution). I find it a bit weird that Star and All are not in Term, but those could be trivially included in infer as well.