Kernel: spurious 'non valid occurrence' in inductive type

Description

The only difference betweenAll₁ and All₂ is whether hts is before or after the colon.
I expected both versions to work.

inductive Tele.{u} (T : Nat → Type u) (a : Nat) : Nat → Type u
  | nil : Tele T a a
  | snoc {b} : Tele T a b → T b → Tele T a (b + 1)

inductive Tele.All₁.{u}
   {T : Nat → Type u}
   (p : ∀ {n}, T n → Prop)
   {a : Nat} :
   {b : Nat} →
   Tele T a b →
   Prop
  | nil : Tele.All₁ p (@Tele.nil T a)
  | snoc {b : Nat} {ts : Tele T a b} {t : T b} :
    (hts : @Tele.All₁ T p a b ts) → -- hts after colon
    p t →
    @Tele.All₁ T p a (b + 1) (@Tele.snoc T a b ts t)

/-- error:
(kernel) arg #7 of 'Tele.All₂.snoc' contains a non valid occurrence of the datatypes being declared
-/
#guard_msgs in
inductive Tele.All₂.{u}
   {T : Nat → Type u}      -- param
   (p : ∀ {n}, T n → Prop) -- param
   {a : Nat} :             -- param
   {b : Nat} →             -- index
   Tele T a b →            -- index
   Prop
  | nil : Tele.All₂ p (@Tele.nil T a)
  | snoc {b : Nat} {ts : Tele T a b} {t : T b}
    (hts : @Tele.All₂ T p a b ts) : -- hts before colon, complaint here
    p t →
    @Tele.All₂ T p a (b + 1) (@Tele.snoc T a b ts t)

Versions

tested on nightly 4.29 today

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Kernel.3A.20spurious.20'non.20valid.20occurrence'/with/573955904

Reproduce the kernel diagnostic with the provided Tele.All₁ and Tele.All₂ inductive declarations, then compare why moving hts changes occurrence validation. Start with the kernel's inductive-declaration validation and confirm that the equivalent declarations are both accepted without the spurious non-valid-occurrence error.