Unexpected behavior of class fields

Stream: new members

[pandaman]

I'm defining a class PositionRecorder representing a type with a distinguished element (empty) and an operation to update a value (record). My first attempt resulted in empty inheriting an explicit argument of the class, which I'd like to avoid. However, on the second attempt, PositionRecorder.empty is in a weird state where it exists and doesn't exist at the same time.
Does anyone have any idea what's going on (and how to properly define it)?

open String (Pos)

namespace One

class PositionRecorder (s : String) (α : Type) where
  empty : α
  record : α → Nat → Pos s → α

-- For some reason, empty requires (s : String)
-- one.PositionRecorder.empty (s : String) {α : Type} [self : PositionRecorder s α] : α
#check PositionRecorder.empty

end One

namespace Two

-- For some reason, putting `empty` in `PositionRecorder` makes `empty` require `s` as an argument.
class WithEmpty (α : Type) where
  empty : α

class PositionRecorder (s : String) (α : Type) extends WithEmpty α where
  record : α → Nat → Pos s → α

-- empty doesn't exist: "Unknown constant `two.PositionRecorder.empty`"
-- #check PositionRecorder.empty

-- Yet we cannot define it: "invalid declaration name `two.PositionRecorder.empty`, structure `two.PositionRecorder` has field `empty`"
-- def PositionRecorder.empty {s : String} {α : Type} [inst : PositionRecorder s α] := inst.empty

end Two

-- Example implementations
instance historyAccumulatorInst {s : String} : One.PositionRecorder s (Array (Nat × Pos s)) where
  empty := #[]
  record xs idx p := xs.push (idx, p)

instance overwriteInst {s : String} {size : Nat} : One.PositionRecorder s (Vector (Option (Pos s)) size) where
  empty := Vector.replicate size .none
  record ps idx p := ps.setIfInBounds idx p

[Damiano Testa]

Wrt to getting WithEmpty in Two, you can access it via #check PositionRecorder.toWithEmpty. Adding to is what tends to happen.

[pandaman]

Yes, we can access WithEmpty, but I'm more interested in accessing empty directly. In other words, my question is about the differences between these two:

namespace Two

-- For some reason, putting `empty` in `PositionRecorder` makes `empty` require `s` as an argument.
class WithEmpty (α : Type) where
  empty : α

class PositionRecorder (s : String) (α : Type) extends WithEmpty α where
  record : α → Nat → Pos s → α

-- empty doesn't exist: "Unknown constant `two.PositionRecorder.empty`"
-- #check PositionRecorder.empty

-- Yet we cannot define it: "invalid declaration name `two.PositionRecorder.empty`, structure `two.PositionRecorder` has field `empty`"
-- def PositionRecorder.empty {s : String} {α : Type} [inst : PositionRecorder s α] := inst.empty

end Two

namespace Three

-- No dependency on (s : String)
class PositionRecorder (α : Type) where
  empty : α
  record : α → Nat → Nat → α

-- PositionRecorder.empty exists as expected
#check PositionRecorder.empty

end Three

[Aaron Liu]

you can access it through WithEmpty.empty