Type substitution does not shift term variables when going under term binders

[mbovel]

I have mutually inductive types and terms where types can both contain terms (e.g., refinement predicates) and bind term variables (e.g., dependent function types).

In this setting, type substitution .[U/] does not shift U's term variables when going under a term binder in the outer type.

Require Import Autosubst.Autosubst.

Inductive Ty : Type :=
  | TVar : var -> Ty
  | TFun : Ty -> {bind Term in Ty} -> Ty
  | TRefine : Ty -> {bind Term} -> Ty
with Term : Type :=
  | tvar : var -> Term.

Global Instance Ids_Ty : Ids Ty. derive. Defined.
Global Instance Rename_Ty : Rename Ty. derive. Defined.
Global Instance Subst_Ty : Subst Ty. derive. Defined.
Global Instance SubstLemmas_Ty : SubstLemmas Ty. derive. Defined.

Global Instance Ids_Term : Ids Term. derive. Defined.
Global Instance Rename_Term : Rename Term. derive. Defined.
Global Instance Subst_Term : Subst Term. derive. Defined.
Global Instance SubstLemmas_Term : SubstLemmas Term. derive. Defined.

Global Instance HSubst_Term_Ty : HSubst Term Ty. derive. Defined.

Example ty_subst_does_not_shift :
  (TFun (TVar 0) (TVar 0)).[(TRefine (TVar 1) (tvar 1))/] =
  TFun (TRefine (TVar 1) (tvar 1)) (TRefine (TVar 1) (tvar 1)).
  (*                                                  ^^^^^^ should be tvar 2 *)
Proof. reflexivity. Qed.

Both copies of the substituted type are identical. The second one is under TFun's term binder ({bind Term in Ty}), so its free term variable tvar 1 should have been shifted to tvar 2.

It seems type substitution .[sigma] only tracks type-variable binders (applying up when going under {bind Ty ...}) but does not track term-variable binders ({bind Term in Ty}), so the substituted type is inserted verbatim regardless of how many term binders have been crossed.

Is this a known limitation?

• All existing Autosubst 1 examples have types that never contain terms, so this issue does not arise there.
• Why is Ids_outer necessary for HSubstLemmas? #4 discusses related limitations with heterogeneous substitution, but it seems to predate support for mutually inductive types.
• I read Autosubst 2 uses vector substitutions that track all sorts simultaneously, which should in principle handle this correctly. However, I'd prefer to stay on Autosubst 1 if possible.