Rpc Error when hovering variable
Closed this issue · 3 comments
hargoniX commented
Prerequisites
- Put an X between the brackets on this line if you have done all of the following:
- Check that your issue is not already filed.
- Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.
Description
In the following code:
import Lean.Data.HashMap
open Lean
inductive Decl (α : Type) where
| atom (idx : α)
deriving BEq, Hashable
def Cache (α : Type) := Unit
structure CacheHit (decl : Decl α) where
idx : Nat
def Cache.find (cache : Cache α) (decl : Decl α) : (CacheHit decl) :=
sorry
theorem denote_mkAtom_cached {cache : Cache α} {hit} (h : cache.find (.atom v) = hit) :
hit = hit := by
sorry
Hovering hit
at {hit}
yields
Error updating: Error fetching goals: Rpc error: InternalError: unknown metavariable '?_uniq.927'. Try again.
In the infoview. Furthermore the hover itself prints:
hit : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
However hovering on hit
in the theorem statement hit = hit
does reveal a proper hover.
Steps to Reproduce
- Copy code into editor
- Hover over
{hit}
- 💥
Expected behavior: The hover should be the same at the binder and the equation
Actual behavior: A broken hover and seemingly something wrong with the LSP as well.
Versions
4.8.0-rc1
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
JovanGerb commented
Here is a more minimal example that I ran into:
def oops (i : ∀ α, List α) : List β := i β
When hovering over the α
, this error appears:
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
when the cursor is on α
, this error appears with red letters in the infoview:
Error updating: Error fetching goals: Rpc error: InternalError: unknown metavariable '?_uniq.160'. Try again.
nomeata commented
More data points:
Doens’t work
def foo1 (i : ∀ α, List α) : List β := i β
def foo2 (i : (α : _) → List α) : List β := i β
works
def foo3 (i : (α : Type _) → List α) : List β := i β
def foo4 (i : (α : Type 0) → List α) : List β := i β