Failed to synthesize despite abbrev

Stream: new members

[Francisco Giordano]

What is the reason the second #synth fails below? I expected abbrev to solve this typeclass issue.

import Mathlib.LinearAlgebra.Basic

variable [Field F] [Fintype F]
variable (n : ℕ)

#synth AddCommMonoid (Fin n → F) -- ok

abbrev Vec := Fin n → F

#synth AddCommMonoid (Vec n) -- failed to synthesize

[Eric Wieser]

Lean doesn't know what F you want to use

[Eric Wieser]

#synth AddCommMonoid (Vec (F := F) n) works