Typing of substitution in a bidirectional type system In most typed lambda calculi, we have the following lemma:


If $\Gamma \vdash t_1 : \tau_1$ and $\Gamma, x : \tau_1, \Delta \vdash t_2 : \tau_2$ then $\Gamma,\Delta[t_1/x] \vdash t_2[t_1/x] : \tau_2[t_1/x]$


However, I'm wondering how we'd phrase such a lemma in a bidirectional typing system, with synthesis $\Rightarrow$ and checking $\Leftarrow$ judgements.

The main problem is that substitution does not preserve synthesis. For example, in most systems, $\Gamma \vdash x \Rightarrow T$ if $x : T \in \Gamma$, but  $[(\lambda y \ldotp t)/x]x$ won't synthesize any type if there are only checking rules for $\lambda$.

Potential solutions I can think of:


Restrict to substituting with synthesizing expressions. This seems like it would give us the induction hypothesis we need (since, in most systems, all synthesizing expressions also check), but is very restrictive.
Only show that substitution preserves checking. This is a weaker result, and I'm unsure of whether it gives us a strong enough inductive hypothesis, since it would be difficult to rebuild typing derivations with synthesis judgements in the premises.


This seems like a pretty basic metatheoretic property, so I'm sure I'm not the first one to have encountered this. Does anyone have a reference to a bidirectional system that cleanly solves these issues? Is there an obvious solution I am missing?
One solution is indeed to restrict to substituting with synthesizing expressions. You can only hope to replace variables with terms of the same mode (i.e. inferrable terms), anything else just won't fit. It is not that restrictive in the sense that usually a checkable term together with a type annotation gives you an inferrable term. This embedding is typically called cut because well... this is what it is. This restriction is described (and deployed) in I Got Plenty o’ Nuttin’.

Alternatively (which is also mentioned in IGPoN) you can define hereditary substitution (a formalised account for STLC) whereby if you are about to form a redex because of the checkable you just plugged in, you fire it. And again. And again. And again. Until your substitution is not creating any new redexes.