Elab doesn't match infoview?

Stream: lean4

[nrs]

update: explanation found at #metaprogramming / tactics > Simulating the scope of an inductive declaration in MetaM

Was having a hard time debugging a piece of code, and only managed to fix it when I relied on trace.Elab.step instead of the infoview. Now the more likely thing that's going on is that I don't actually understand how the internals work precisely, so I might be wrong in thinking these two things usually match. In case they do have to usually match: consider the following piece of code. The reported expected type of the (project _) term in infoview says it is W sig, but tracing elaboration shows that at elaboration time the expected type is W ?mvar. Changing the instance implicit to an index makes infoview match the Elab report that the target type is W ?mvar

Is this expected behaviour or am I missing something? Am on nvim and Lean version 4.15.0-rc1

import Mathlib
namespace myNamespace

structure Signature where
  symbols : Type
  arity : symbols -> Nat

inductive Ext (sig : Signature) (α : Type _)
| mk : (s : sig.symbols) -> (Fin2 (sig.arity s) -> α) -> Ext sig α

def Ext.map (f : α -> β) : Ext sig α -> Ext sig β
| ⟨s, g⟩ => ⟨s, f ∘ g⟩

def Alg (sig : Signature) (α : Type _) : Type _ := Ext sig α -> α

inductive W (sig : Signature)
| sup : Ext sig (W sig) -> W sig

class SubSig (siga sigb : Signature) where
  inj : Ext siga α -> Ext sigb α

def inject {siga sigb : Signature}  (ext : Ext siga (W sigb)) [SubSig siga sigb] : W sigb :=
  ⟨SubSig.inj ext⟩

inductive NatTySh | nat
def NatTyE : Signature := ⟨NatTySh, fun _ => 0⟩

#guard_msgs in
set_option trace.Elab.step true in
inductive IArithExprSymbols {sig : Signature} [inst : SubSig NatTyE sig] : W sig -> Type _
| val : Nat -> IArithExprSymbols (inject _)

Along with a stuck metavariables error, this is what the state reports when cursor is over left parenthesis of (inject _):

▶ expected type (35:34-35:44)
sig : Signature
inst : SubSig NatTyE sig
⊢ W sig

This is what infoview reports when cursor is over hole:

▶ expected type (35:42-35:43)
sig : Signature
inst : SubSig NatTyE sig
⊢ Ext ?m.1941 (W sig)

by contrast, the trace.Elab.step reports that the target type for the term is W ?mvar (output curated)

info: [Elab.step] expected type: Sort ?u.1933, term
    Nat -> IArithExprSymbols (inject _)
  [Elab.step] expected type: Type, term
      Nat
  [Elab.step] expected type: Type ?u.1928, term
      IArithExprSymbols (inject _)
    [Elab.step] expected type: W ?m.1942, term
        (inject _)