Doing match on an inductive that should satisfy some defeqs

Stream: new members

[Fernando Chu]

I have the following

import Mathlib

-- Product of sorts
inductive DerivedSorts (Sorts : Type*) where
  | prod {n : ℕ} : (Fin n → Sorts) → DerivedSorts Sorts

-- Functions on strings
structure FunctionSymbols (Sorts : Type*) where
  domain : String → DerivedSorts Sorts
  codomain : String → DerivedSorts Sorts

structure Context (Sorts : Type*) : Type _ where
  length : ℕ
  ctx : Fin length → DerivedSorts Sorts

variable (Sorts : Type*) (S : FunctionSymbols Sorts)

-- Terms of type A in a context Γ
inductive Term : Context Sorts → DerivedSorts Sorts → Type _ where
  | var {Γ : Context Sorts} {A} : {i : Fin Γ.length // Γ.ctx i = A} → Term Γ A
  | func (Γ) (f : String) : Term Γ (S.domain f) → Term Γ (S.codomain f)

-- Substitution of terms. It's missing a context morphism Δ ⟶ Γ to be provable,
-- but this is irrelevant to my current problem.
def Term.subst {Δ Γ : Context Sorts} {A : DerivedSorts Sorts} :
    Term Sorts S Δ A → Term Sorts S Γ A := fun
  | .var _ => _
  | .func Γ f _ => _ -- type mismatch?

I have to say that I'm not sure what Lean is complaining about. I thought that maybe it wasn't figuring out that S.codomain f should be A because of the appearance of A in Term Sorts S Γ A, but this seems to not be the case since it also complains about

def Term.subst {Δ Γ : Context Sorts} {A B : DerivedSorts Sorts} :
    Term Sorts S Δ A → Term Sorts S Γ B := fun
  | .var _ => _
  | .func Γ f _ => _ -- type mismatch?

What's the correct way to match then?

[Yan Yablonovskiy 🇺🇦]

def Term.subst {Δ Γ : Context Sorts} {A : DerivedSorts Sorts} :
    Term Sorts S Δ A → Term Sorts S Γ A := fun
  | .var _ => _
  | _ => sorry

leads to "don't know how to synthesize placeholder" . So there may be an issue there. As opposed to:

def Term.subst {Δ Γ : Context Sorts} {A : DerivedSorts Sorts} :
    Term Sorts S Δ A → Term Sorts S Γ A := fun
  | .var _ => sorry
  | _ => sorry

[Fernando Chu]

I believe this is the same problem as this other post, I'll manage then, thanks!