A substitution to add variables in the context

Question

I'm doing type-inference in a dependently typed language, using (as is commonly done) a λ-calculus with explicit substitutions like that of Abadi (with a representation based on debruijn indices) in order to handle the issues of scoping when performing (higher-order) unification.

The "shift" operation of those explicit substitutions (denoted ↑) allows one to move a term to a larger context (i.e. applying weakening). I.e. we can start from

Γ ⊢ e : τ

and then move this term e to a larger context:

Γ,x₁…xₙ ⊢ e[↑ⁿ] : τ

where e[↑ⁿ] is the result of n applications of ↑ to e. So far so good.

This also works with metavariables: if a metavariable u appears within e (where it should appear as u[σ] where σ is a "pending" substitution that should be applied to u when it gets instantiated), then in e[↑ⁿ] u will get a new explicit substitution which is a combination of σ and ↑ⁿ to make sure that after instantiating u the result is properly adjusted for the context Γ,x₁…xₙ.

Now here's my problem: The metavariables in e[↑ⁿ] will never be able to refer to any of the x₁…xₙ variables. In general, this is indeed desirable and necessary. But in my case I know that all my metavariables's original context is Γ or some extension thereof, and I'd like to compute something like e[↑ⁿ] but where the metavariables are modified such that they can refer to the new x₁…xₙ variables.

For example: let's say we have a declaration f : List u → u, and during type inference I want to generalize this to f : ∀t. List t → t, like Twelf does. The original term List u → u was declared within a context Γ so it looked like Γ ⊢ List u[id] → u[id] : *. Now this term needs to be moved to the new context Γ,t but if I do it by applying ↑ I get Γ,t ⊢ List u[↑] → u[↑] : *. But u[↑] cannot refer to t since t is at debruijn index 0 and the ↑ substitution adds 1 to the index of any variable reference, so I cannot get from List u[↑] → u[↑] to List t → t by instantiating the metavariable u (currently, I do it by manually traversing the term instead of reusing the existing metavariable instantiation infrastructure: it works but it's unsatisfactory). Note that this is no accident: u exists (is created?) in context Γ and the explicit substitutions are designed to make it possible to use it in different contexts, not to change its own context.

My question is if it rings a bell and someone has seen a similar problem somewhere, which might help me better understand the underlying problem and maybe find a different approach.