Infoview popup shows partially instantiated type

I am on https://github.com/Julian/lean.nvim/commit/3089040359942d58d70af5deaac1bbe63724c53a -- the latest revision available.

This is the project: https://github.com/AeneasVerif/kraken/tree/fd2b8f6b0761f51623c0fe62b83e85d36db8155a

Opening Examples.lean then hitting K over `traverseChildren` at line 525 shows the following infoview:

```lean4
Lean.Meta.traverseChildren.{u_1} {M : Type → Type u_1} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M]
(visit : Expr → M Expr) (e : Expr) : StateRefT' IO.RealWorld Bool SymM Expr

Maps `visit` on each child of the given expression.

Applications, foralls, lambdas and let binders are bundled (as they are bundled in `Expr.traverseApp`, `traverseForall`, ...).
So `traverseChildren f e` where ``e = `(fn a₁ ... aₙ)`` will return
``(← f `(fn)) (← f `(a₁)) ... (← f `(aₙ))`` rather than ``(← f `(fn a₁ ... aₙ₋₁)) (← f `(aₙ))``

See also `Lean.Core.traverseChildren`.
```

Note how the type that is shown starts as the type of the *definition* (with proper type classes), but the return type of the function shows an *instantiated* type where M has been replaced with a concrete instance. The type should be the generic type of the function signature.

This does not happen on VSCode (@kha sent a screenshot of VSCode's output)