Rpc Error when hovering variable

hargoniX commented 1 week ago

Prerequisites

[X] 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}
:boom:

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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

JovanGerb commented 1 week ago

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 1 week ago

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 β

nomeata commented 1 week ago

Possible fix at https://github.com/leanprover/lean4/pull/4137

leanprover / lean4