Kernel: spurious 'non valid occurrence'

Stream: lean4

[IntGrah]

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 : All₁ p (@Tele.nil T a)
  | snoc {b : Nat} {ts : Tele T a b} {t : T b} :
    @All₁ T p a b ts →
    p t →
    @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 : All₂ p (@Tele.nil T a)
  | snoc {b : Nat} {ts : Tele T a b} {t : T b}
    (hts : @All₂ T p a b ts) : -- complaint is here
    p t →
    @All₂ T p a (b + 1) (@Tele.snoc T a b ts t)

The only difference between All₁ and All₂ is whether hts and ht are named or not. This seems like a bug? As far as I can tell, the parameters are all consistent, and there's no rogue inductive occurrences

[IntGrah]

Actually, I misspoke, the difference is not whether hts is named, but whether it appears before or after the colon

[IntGrah]

https://github.com/leanprover/lean4/issues/12491

[Joachim Breitner]

It's the implicit lambda feature changing the parameter type. Parameters have to be syntactically equals. This works:

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) :
    p t →
    @Tele.All₂ T p a (b + 1) (@Tele.snoc T a b ts t)

(Note the @)

[IntGrah]

Why is the @ required only when hts is before the colon? I would have thought that plicity does not matter, since the kernel has no idea about plicity. So p is syntactically equal to p

[IntGrah]

By plicity I mean whether n is {ex,im}plicit

[Joachim Breitner]

Don't know why it's behaving differently, but it seems that in one case it's applying the implicit parameter to p and in the other one it doesn't.