RFC: support structural recursion with non-variable indices

Proposal

Recursive definitions on inductive families should support structural recursion even when the indices to the inductive family are not variables.

For a concrete use case, consider the following fragment of a simple type theory:

inductive Ty
  | nat
  | arr (A B : Ty)

inductive Tm : List Ty → Ty → Type
  | lam : Tm (A :: Γ) B → Tm Γ (A.arr B)
  | zero : Tm Γ .nat
  | succ : Tm Γ .nat → Tm Γ .nat

def Tm.val : Tm [] .nat → Nat
  | .zero => .zero
  | .succ e => e.val.succ

While the definition of Tm.val is accepted, it uses well-founded recursion instead of structural recursion.
The lack of structural recursion means that the defining equations like e.succ.val = e.val.succ are not definitional, which can make working with Tm.val more cumbersome.

Trying to force structural recursion by adding termination_by structural e => e results in this error:

cannot use specified measure for structural recursion:
  its type Tm is an inductive family and indices are not variables
    Tm [] Ty.nat

By manually generalizing the indices, we can create a definition that uses structural recursion and has the desired definitional equations:

def Tm.valAux : ∀ {Γ A}, Γ = [] → A = .nat → Tm Γ A → Nat
  | _, _, rfl, rfl, .zero => .zero
  | _, _, rfl, rfl, .succ e => (e.valAux rfl rfl).succ

def Tm.val : Tm [] .nat → Nat :=
  Tm.valAux rfl rfl

@[simp] theorem Tm.val_zero : Tm.zero.val = .zero := rfl
@[simp] theorem Tm.val_succ (e : Tm [] .nat) : e.succ.val = e.val.succ := rfl

Writing this out is quite tedious and the result is harder to read than the original definition. Furthermore, the transformation is entirely automatable. Thus, I propose that the structural recursion compiler be modified to automatically generalize the indices that are not variables, removing the need for this verbose workaround.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

No source file or test is named. Start by reproducing the Tm.val example and reading the structural recursion compiler; compare the current well-founded result with the valAux workaround. Done means non-variable indices are generalized automatically and the resulting recursive definitions have the stated definitional equations.