Confusing error with computed field

Stream: lean4

[François G. Dorais]

This snippet

inductive RankedList (α : Type _) where
  | nil : RankedList α
  | cons : α → RankedList α → RankedList α
with
  @[computed_field] rank : RankedList α → Nat
  | .nil => 0
  | .cons _ l => l.rank + 1

gives me this error (v4.8.0-rc2)

application type mismatch
  RankedList.rank α
argument
  α
has type
  Type u_1 : Type (u_1 + 1)
but is expected to have type
  RankedList ?α : Type ?u.1293

Apparently computed fields don't work for inductives with parameters or indices? If that's the case, the error message could be more useful.

[Number Eighteen]

I don'tknow what a computed feld is; can you lnk to any documentation?

[François G. Dorais]

It's in core: Lean.Elab.ComputedFields, documentation is there.

[Kyle Miller]

It looks like you can get it to work:

inductive RankedList (α : Type _) where
  | nil : RankedList α
  | cons : α → RankedList α → RankedList α
with
  @[computed_field] rank : (α : Type _) → RankedList α → Nat
  | _, .nil => 0
  | _, .cons _ l => l.rank + 1

[Eric Wieser]

Does this mean that the computed field can be specialized to certain types?

[François G. Dorais]

I didn't think about that variation. Thanks! Sadly, this fails:

inductive RankedList (α : Type _) where
  | nil : RankedList α
  | cons : α → RankedList α → RankedList α
with
  @[computed_field] rank : {α : Type _} → RankedList α → Nat
  | _, .nil => 0
  | _, .cons _ l => l.rank + 1

I think we're homing in on the core issue!