Mysterious LSP panic on hover

Stream: mathlib4

[Joris Roos]

Consider the following (tested using current Mathlib, right now at b40a064 and most recent VSCode extension):

import Mathlib.Order.Defs.LinearOrder
import Mathlib.Order.Notation

universe u

theorem nonsense {α : Type u} [Min α] {a b : α} : min a b = a := by sorry

example : min 1 2 = 1 := by rw [nonsense]

The code compiles without problems (except for the sorry of course, ignore the mathematically nonsensical statement).

But: Hovering over nonsense in rw [nonsense] causes a server error message
PANIC at Lean.MetavarContext.getLevelDepth Lean.MetavarContext:874:14: unknown metavariable
(There is no error when hovering over nonsense in its declaration.)

Now this doesn't seem like a big deal and this error doesn't really bother me too much, but I'm trying to use this as an excuse to learn something about Lean internals and the surrounding infrastructure. I'd be happy if someone could give me some hints about what might be going on here, or hints on how to figure it out. So far my methods are pretty much limited to inserting dbg_trace at various places..

Here is what I found so far:

• The metavariable at fault is a universe metavariable (an LMVarId; this is consistent with the error disappearing when we remove u from the "theorem").

• The error seems to be related to the delaborator delabInf in Mathlib.Order.Notation. There might not be anything wrong with this code, but the error message does disappear if we just call failure in that method when u on line 129 is a .mvar and that it doesn't have a Nat assigned to it in the hash table. What is the intended behavior in this scenario? Another thing that confused me was thatdelabInf seems to be called twice here when hovering (is it supposed to be called twice and why is that?). Only one of the two calls results in panic. Where is the Lean server code that performs these calls?

• If we remove either of the two imports (or both), the code still compiles (of course, because Min of Nats is in prelude), but the error message disappears. This doesn't surprise me for removing the second import, because that's where delabInf lives, but I can't figure out why it disappears if we remove the first import (I have also tried to minimize these imports).

My apologies if this isn't the right channel (and feel free to move this thread).