Functions with class arguments

Stream: lean4

[Paul Chisholm]

I want to write a function that takes a class as an argument, as opposed to a type. For example, I might have

class Nat2 (α : Type) where
  first  : α → Nat
  second : α → Nat

structure AB where
  a : Nat
  b : Nat

instance : Nat2 AB where
  first ab  := ab.a
  second ab := ab.b

Given any instance of Nat2 implements a first and a second function, say I want to write a function on Nat2 that sums the two values. Since any instance of Nat2 must implement these functions, any instance would inherit the sum function (i.e. it would not need to be implemented in each instance). Something like

def sum (n : Nat2 α) : Nat :=
  --n.first + n.second
  --first n + second n
  --Nat2.first n + Nat2.second n
  sorry

Each of the three commented out lines throws a different error, and I can't think of anything else to try. Is this or something similar possible in Lean 4?
This is trying to do what you might do with abstract supertypes in OO languages or a language that has a feature similar to Java's interfaces or Scala's traits.

[Scott Morrison]

def sum {α : Type} [Nat2 α] (n : α) : Nat :=
  Nat2.first n + Nat2.second n