Unexpected field notation completion

[Kha]

import Lean

example (range : String.Range) : String.Pos :=
  ⟨range.stop.b⟩

example (p : String.Pos) : String.Pos :=
  ⟨p.b⟩

Both bs complete to very different lists, but neither contains the desired byteIdx.