Working with structure with implicit T

Stream: general

[DSB]

Friends, I'm trying to use Lean for Functional Programming, and one of the things I was trying to do was to create a list that had multiple-types constrained by a type class, akin to what in Haskell is called an existential type. The colleagues here helped me out with the solution shown in the code below.
I'm now trying to understand how to work with it and one of the issues I'm having is shown in the very end of the code:

class MInterface (a : Type) where
  fm : a -> Int

instance :  MInterface Nat where
  fm x := x + 1

instance :  MInterface String where
  fm x := String.length (x) + 1

structure M where
  {T : Type}
  [inst : MInterface T]
  val : T

def M.fm : M → Int := fun m => m.inst.fm m.val

def foo : List M :=
  [⟨1⟩, ⟨"example"⟩, ⟨3⟩]

def m : M := ⟨1⟩

#eval (fun x : Nat => 2*x) m.val -- Works
#eval 2*m.val -- Does not work

I'm confused why the function with the Nat type works, but the 2* m.val does not.
When I try to check the type under m.val I get m.T instead of Nat.
Any ideas on what might be going on?

[Eric Wieser]

If you make m an abbrev rather than a def it should work

[DSB]

Thanks, @Eric Wieser. Why would that be so? Any "issues" arise from using abbrev besides def?
I'm confused by how the typed function works... It seems like it should not.