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?