Dependent type; type checker `__do_lift`

Stream: new members

[Curious Joe]

I have the following code:

structure RobotGameState where
  game : EGame
  current : EField game.n game.m
deriving Repr

def make_move (dir : Direction) : StateM RobotGameState Unit := do
  let g := (←get).game
  let f := (←get).current
  let efs := search g f dir

where search as the signature:

def search (g : EGame) (f : EField g.n g.m)
  (dir : Direction) : List (EField g.n g.m) :=

On the line let efs := search g f dir, I get the error:

▶ expected type (120:25-120:28)
dir : Direction
g : EGame := __do_lift✝¹.game
f : EField __do_lift✝.game.n __do_lift✝.game.m := __do_lift✝.current
⊢ Direction

▶ 120:23-120:24: error:
application type mismatch
  search g f
argument
  f
has type
  EField __do_lift✝.game.n __do_lift✝.game.m : Type
but is expected to have type
  EField g.n g.m : Type

I though I was smart by creating a dependent type where the EField depends on EGame such that I can directly access game values.
However, the errors are flying at me since making this change.
Why can the type checker not infer that the EField type of f has the same n and m values as the game field?

[Curious Joe]

Hmm; so extracting the full object using (<-) notation and then accessing the values after does the work:

def make_move (dir : Direction) : StateM RobotGameState Unit := do
  let rgs := (←get)
  let g := rgs.game
  let f := rgs.current
  let efs := search g f dir
  match make_move_helper efs [] with
  | [] => pure ()
  | n :: ns =>
    -- update starting value
    let g := {g with fields := g.fields.update_value f.i_n f.j_m {f with c := '.'}}
    -- update rest
    let g := update_pairs g (n :: ns)
    modify fun s => {s with game := g, current := n}
    pure ()