Weird typeclass behavior

Stream: lean4

[Oskar Goldhahn]

Why does the following not work? Is it a bug?

class Cls (f : Type) where
  ITy: Type := Unit
  cst: ITy
  map (_: ITy) : ITy := cst

def Ty: Type := Unit

instance : Cls Ty where -- error here `fields missing: 'map'`
  cst := ()

These all work:

instance : Cls Ty where
  ITy: Type := Nat
  cst := 0

instance : Cls Ty where
  ITy: Type := Unit
  cst := ()

instance : Cls Ty where
  cst := ()
  map _: Unit := ()

instance : Cls Ty where
  ITy: Type := Unit
  cst := ()
  map _: Unit := ()