Vector type doesn't reduce the natural number

Stream: lean4

[Brandon Brown]

inductive Vector (α : Type u) : Nat → Type u
  | nil : Vector α 0
  | cons : α → Vector α n → Vector α (n+1)

#check Vector.cons 3 (Vector.cons 5 Vector.nil)
-- Vector.cons 3 (Vector.cons 5 Vector.nil) : Vector Nat (0 + 1 + 1)

Why does it stay (0 + 1 + 1) and not get reduced to 2?

[Sébastien Michelland]

When you say that cons outputs a Vector α (n+1), that's syntactic. But types will reduce if you assign, cast, or otherwise compare for equality:

def v: Vector Nat 2 := Vector.cons 3 (Vector.cons 5 Vector.nil)

But also what set of expressions do you expect would simplify? Would n+0 simplify? What about 0+n, which is equal but not definitionally equal?

[Henrik Böving]

Counter question: Why should Lean eagerly reduce the type here without a real need to do so in say a compare operation. As we know reducing a term can be costly if the term is complex enough.