Infoview popup shows partially instantiated type
Nobody has claimed this yet.
Assessment
- Difficulty
- 3/5
- Estimated time
- 1-2 days
- Newbie friendliness
- 48/100
Research direction
Reproduce the issue at commit 3089040359942d58d70af5deaac1bbe63724c53a by opening Examples.lean and pressing K over traverseChildren at line 525. Compare the infoview output with the reported VSCode output, then trace the infoview type display path. Done means the popup preserves the generic function signature instead of showing an instantiated return type.
Written by the indexing model from the issue text.
Description
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:
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)
- Dominant language
- Lua
- Stars
- 601
- Forks
- 61
- Avg merge
- 3d 14h
- Merged PRs (30d)
- 7
Getting set up
- No Dockerfile or Docker Compose file
- No pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from Julian/lean.nvim
-
Difficulty 2/5 1-3 hours Newbie friendliness 66/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
-
Difficulty 3/5 Half a day Newbie friendliness 35/100
-
Difficulty 4/5 3-5 days Newbie friendliness 48/100
-
Difficulty 3/5 1-2 days Newbie friendliness 58/100
All issues in Julian/lean.nvim
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 62/100
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
Maintainers usually reply within 3 days
-
feature
Difficulty 2/5 1-3 hours Newbie friendliness 82/100
-
tests/control, tests/cli: the up-front cleanup removes an ANOTHER or SHIM the environment carriesOpenseverity: low
Difficulty 2/5 1-3 hours Newbie friendliness 80/100
luainkernel/lunatik#1796 ·
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
brndnmtthws/conky#2486 ·
Maintainers usually reply within 1 day