Crash in `sup`/`inf` / `max`/`min` delaborators

Stream: mathlib4

[Bhavik Mehta]

These new delaborators seem to be giving me PANIC errors; or at least deleting them makes the PANICs go away. Here's the example:

import Mathlib.Order.Notation

universe u

class LinearOrder (α : Type u) extends LE α, Min α, Max α, Ord α where

variable {α : Type u}

theorem inf_eq_left [LE α] [Min α] {a b : α} : min a b = a ↔ a ≤ b := sorry

def foo {α : Type} (S : α → Prop) : Nat := sorry

def bar {α : Type} (A : α → Prop) (n : Nat) : α → Prop := sorry

theorem extracted_1 {α : Type} {A : α → Prop} (n : Nat)
    (ih : min (foo A) n = foo (bar A n))
    (h : ∀ y, A y → bar A n y) :
    min (foo A) (n + 1) = foo (bar A n) := by
  replace h : bar A n = A := sorry
  rw [h] at ih
  rw [inf_eq_left]

Putting the cursor in the final rw gives me

PANIC at Lean.MetavarContext.getLevelDepth Lean.MetavarContext:874:14: unknown metavariable
backtrace:

on local VSCode (it seems fine on the web editor)

[Bhavik Mehta]

(deleted)

[Eric Wieser]

Can you make it fall in the command line with trace_state?

[Jovan Gerbscheid]

I'm looking at this trace:

PANIC at Lean.MetavarContext.getLevelDepth Lean.MetavarContext:874:14: unknown metavariable
backtrace:
(lean_panic+0xf5) [0x7ff5d8b77155]
(lean_panic_fn+0x15) [0x7ff5d8b77335]
(l_Lean_Meta_SynthInstance_MkTableKey_normLevel+0x352) [0x7ff5d56ec992]
(l_List_mapM_loop___at_Lean_Meta_SynthInstance_MkTableKey_normExpr___spec__2+0x13b) [0x7ff5d56ee6fb]
(l_Lean_Meta_SynthInstance_MkTableKey_normExpr+0x1a3) [0x7ff5d56eea33]
(l_Lean_Meta_SynthInstance_MkTableKey_normExpr+0x752) [0x7ff5d56eefe2]
(l_Lean_Meta_SynthInstance_mkTableKey___at_Lean_Meta_SynthInstance_main___spec__1+0xe4) [0x7ff5d5743464]
(l_Lean_Meta_SynthInstance_main___lambda__2+0x9c) [0x7ff5d5743ffc]
(lean_apply_3+0xbac) [0x7ff5d8b87afc]
(l_Lean_Core_withCurrHeartbeats___at_Lean_Meta_SynthInstance_main___spec__3+0x24) [0x7ff5d5743bd4]
(l_Lean_Meta_synthInstance_x3f___lambda__2+0x260) [0x7ff5d5756cf0]
(lean_apply_5+0x8cc) [0x7ff5d8b8be2c]
(l___private_Lean_Meta_Basic_0__Lean_Meta_withNewMCtxDepthImp___rarg+0x447) [0x7ff5d5684827]
(l_Lean_Meta_withNewMCtxDepth___at_Lean_Meta_matchesInstance___spec__1___rarg+0x1f) [0x7ff5d51c7cff]
(l_Lean_Meta_synthInstance_x3f___lambda__4+0x12f2) [0x7ff5d57582d2]
(lean_apply_5+0x8cc) [0x7ff5d8b8be2c]
(l_Lean_withTraceNode___at_Lean_Meta_synthInstance_x3f___spec__4+0x2eb) [0x7ff5d57562eb]
(l_Lean_Meta_synthInstance_x3f___lambda__5+0x1f4) [0x7ff5d57611f4]
(lean_apply_1+0xe2f) [0x7ff5d8b834bf]
(l_Lean_profileitIOUnsafe___rarg___lambda__1+0xe) [0x7ff5d50230ce]
(l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed+0x9) [0x7ff5d5023359]
(lean_apply_1+0xb5f) [0x7ff5d8b831ef]
(lean_profileit+0x83) [0x7ff5d886ffd3]
(l_Lean_profileitIOUnsafe___rarg+0x64) [0x7ff5d5023234]
(l_Lean_Meta_synthInstance_x3f+0x162) [0x7ff5d57614e2]
(l___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthPendingImp___lambda__1+0xa0) [0x7ff5d57636b0]
(l___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthPendingImp___lambda__3+0x12c0) [0x7ff5d57657b0]
(lean_apply_5+0xa70) [0x7ff5d8b8bfd0]
(l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___rarg+0x203) [0x7ff5d5688393]
(l_Lean_MVarId_withContext___at___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthPendingImp___spec__2___rarg+0x17) [0x7ff5d57633a7]
(lean_synth_pending+0x4c2) [0x7ff5d57670a2]
(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqOnFailure___spec__1___lambda__2+0xb1) [0x7ff5d53201e1]
(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqOnFailure___spec__1+0x754) [0x7ff5d53218f4]
(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqOnFailure___spec__2+0x5a9) [0x7ff5d5324329]
(lean_apply_5+0x8cc) [0x7ff5d8b8be2c]
(l_Lean_withTraceNodeBefore___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_checkTypesAndAssign___spec__1+0x2e4) [0x7ff5d525edd4]
(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqOnFailure+0x1ef) [0x7ff5d532533f]
(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isExprDefEqExpensive___lambda__1+0xe8c) [0x7ff5d53426fc]
(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isExprDefEqExpensive___lambda__2+0x2256) [0x7ff5d5345606]
(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isExprDefEqExpensive+0xb6a) [0x7ff5d534708a]
(l_Lean_Meta_isExprDefEqAuxImpl___lambda__3+0x295b) [0x7ff5d534f86b]
(lean_apply_5+0x5e6) [0x7ff5d8b8bb46]
(l_Lean_withTraceNodeBefore___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_checkTypesAndAssign___spec__1+0x2e4) [0x7ff5d525edd4]
(lean_is_expr_def_eq+0x621) [0x7ff5d523cca1]
(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqLeft___lambda__1+0x26) [0x7ff5d52ef926]
(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqRight+0x1cb) [0x7ff5d52f009b]
(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqDelta+0xc72) [0x7ff5d53012a2]
(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isExprDefEqExpensive___lambda__2+0x129e) [0x7ff5d534464e]
(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isExprDefEqExpensive+0xb6a) [0x7ff5d534708a]
(l_Lean_Meta_isExprDefEqAuxImpl___lambda__3+0x295b) [0x7ff5d534f86b]
(lean_apply_5+0x5e6) [0x7ff5d8b8bb46]
(l_Lean_withTraceNodeBefore___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_checkTypesAndAssign___spec__1+0x2e4) [0x7ff5d525edd4]
(lean_is_expr_def_eq+0x621) [0x7ff5d523cca1]
(l_Lean_Meta_checkpointDefEq___at_Lean_Meta_isExprDefEq___spec__1+0xe20) [0x7ff5d56c17c0]
(l_Lean_Meta_isExprDefEq+0xd2e) [0x7ff5d56c4e8e]
(_ZN4lean5curryEPvjPP11lean_object+0x1c9) [0x7ff5d8b825a9]
(+0x7ece68a) [0x7ff5d891368a]
(+0x7ecc9a7) [0x7ff5d89119a7]
(+0x7ed02a4) [0x7ff5d89152a4]
(+0x7ecff07) [0x7ff5d8914f07]
(+0x7ecfcdd) [0x7ff5d8914cdd]
(lean_apply_5+0xbe7) [0x7ff5d8b8c147]
(l___private_Lean_Meta_Basic_0__Lean_Meta_withNewMCtxDepthImp___rarg+0x447) [0x7ff5d5684827]
(l_Lean_Meta_withNewMCtxDepth___at_Lean_Meta_matchesInstance___spec__1___rarg+0x1f) [0x7ff5d51c7cff]
(_ZN4lean5curryEPvjPP11lean_object+0x1c9) [0x7ff5d8b825a9]
(+0x7ece68a) [0x7ff5d891368a]
(+0x7ecc9a7) [0x7ff5d89119a7]
(+0x7ece93c) [0x7ff5d891393c]
(+0x7ecc9a7) [0x7ff5d89119a7]
(+0x7ece93c) [0x7ff5d891393c]
(+0x7ecc9a7) [0x7ff5d89119a7]
(+0x7ed02a4) [0x7ff5d89152a4]
(+0x7ecff07) [0x7ff5d8914f07]
(+0x7ecfd4a) [0x7ff5d8914d4a]
(lean_apply_10+0x987) [0x7ff5d8b94177]
(lean_apply_n+0x291) [0x7ff5d8b86e71]
(+0x7ecdf0d) [0x7ff5d8912f0d]
(+0x7ecc9a7) [0x7ff5d89119a7]
(+0x7ed02a4) [0x7ff5d89152a4]
(+0x7ecff07) [0x7ff5d8914f07]
(+0x7ecfc8a) [0x7ff5d8914c8a]
(lean_apply_8+0xc86) [0x7ff5d8b91a96]
(l_ReaderT_bind___at_Lean_PrettyPrinter_Delaborator_delabMVarAux___spec__1___rarg+0x286) [0x7ff5d7a7d146]
(lean_apply_7+0xde5) [0x7ff5d8b901e5]
(l_Lean_PrettyPrinter_Delaborator_whenPPOption+0x295) [0x7ff5d7a4d995]
(lean_apply_7+0xde5) [0x7ff5d8b901e5]
(l_Lean_PrettyPrinter_Delaborator_whenNotPPOption+0x3aa) [0x7ff5d7a4e16a]
(_ZN4lean5curryEPvjPP11lean_object+0x25c) [0x7ff5d8b8263c]
(+0x7ece68a) [0x7ff5d891368a]
(+0x7ecc9a7) [0x7ff5d89119a7]
(+0x7ed02a4) [0x7ff5d89152a4]
(+0x7ec82a9) [0x7ff5d890d2a9]
(+0x7ecff07) [0x7ff5d8914f07]
(+0x7ecfc2d) [0x7ff5d8914c2d]
(lean_apply_7+0xe2b) [0x7ff5d8b9022b]
(l_List_firstM___at_Lean_PrettyPrinter_Delaborator_delabFor___spec__1+0x160) [0x7ff5d7a5e8a0]
(l_Lean_PrettyPrinter_Delaborator_delabFor+0x1b7) [0x7ff5d7a5f467]
(lean_apply_7+0x9a8) [0x7ff5d8b8fda8]
(l_Lean_PrettyPrinter_Delaborator_orElse___rarg+0xce) [0x7ff5d7a4596e]
(lean_apply_7+0x7f2) [0x7ff5d8b8fbf2]
PANIC at Lean.MetavarContext.getLevelDepth Lean.MetavarContext:874:14: unknown metavariable

[Jovan Gerbscheid]

The panic is coming from an unknown universe metavariable, inside the isDefEq call in hasLinearOrder in delabInf.

[Jovan Gerbscheid]

The panic comes from the "Expected type" of inf_eq_left, so it's also triggered by

example : False := by
  rw [inf_eq_left]

The expected type is:

⊢ ∀ {α : Type ?u.8957} [inst : LE α] [inst_1 : Min α] {a b : α}, min a b = a ↔ a ≤ b

[Aaron Liu]

I get

⊢ ∀ {α : Type ?u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b = a ↔ a ≤ b

[Jovan Gerbscheid]

I was using the inf_eq_left from @Bhavik Mehta's example

[Bhavik Mehta]

And the one in my example is modified from mathlib's version to make a more minimal example. You could just do

import Mathlib

example : False := by
  rw [inf_eq_left]

and put your cursor over the inf_eq_left to get the same panic

[Aaron Liu]

oh, it panicked! yay!

[Aaron Liu]

time to bisect this

[Jovan Gerbscheid]

I already did :)

[Aaron Liu]

what'd you get

[Jovan Gerbscheid]

The problem is that this universe metavariable is not in the metavariable context during delaboration. But I don't understand why.

[Jovan Gerbscheid]

(I'm not sure in which way you mean the word bissect, but I meant it as "figure out where the error comes from")

[Bhavik Mehta]

Aaron Liu said:

time to bisect this

Yeah what happened here is I found the panic from import Mathlib, reduced it to something from Order.Notation, and Jovan found the line in that file which produces it! So we understand where it's coming from, but not why

[Aaron Liu]

the infoview now refuses to update for the one file that I'm investigating (it works fine for all the other files)

[Aaron Liu]

apparently it's bad to have IO operations on delaborators

[Aaron Liu]

It seems like this problem is specific to rw?

[Aaron Liu]

Maybe we should be looking at the code for rw instead

[Jovan Gerbscheid]

No, the problem is caused whenever it elaborates (and delaborates the expected type of) inf_eq_left without at expected type

[Aaron Liu]

I didn't get the panic on simp though, so what's the difference?

[Jovan Gerbscheid]

I do seem to get a panic with simp, for example when hovering over inf_eq_left

[Aaron Liu]

I'll try again then.

[Aaron Liu]

panic on rw

[Aaron Liu]

panic on rewrite

[Aaron Liu]

no panic on simp

[Jovan Gerbscheid]

Hmm, I was probably wrong

[Aaron Liu]

rw [(inf_eq_left)] also doesn't panic

[Aaron Liu]

So it's something about how rw handles constants differently than expressions

[Aaron Liu]

The culprit is probably docs#Lean.Elab.Tactic.withRWRulesSeq

[Jovan Gerbscheid]

You're right, thank you! Here is a minimization:

import Mathlib.Order.Notation

universe u

class LinearOrder (α : Type u) extends LE α, Min α, Max α, Ord α where

theorem inf_eq_left  {α : Type u} [LE α] [Min α] {a b : α} : min a b = a ↔ a ≤ b := sorry

open Lean Meta Elab Tactic in
elab "test" term:term : tactic => do
  let _ ← optional <| getFVarId term -- comment out this line to avoid the panic!
  let _ ← elabTerm term none

example : False := by
  test inf_eq_left

Apparently Lean gets confused when the same syntax gets elaborated multiple times.

[Aaron Liu]

Now all that's left to do is to fix it

[Aaron Liu]

How does simp do it?

[Thomas Murrills]

The issue seems to be that optional/orElse for TacticM does not restore the info state. If we instead use something like

def Tactic.observing? {α} (x : TacticM α) (restoreInfo := false) : TacticM (Option α) := do
  let s ← Tactic.saveState
  try
    x
  catch _ =>
    s.restore restoreInfo
    return none

with restoreInfo := true (and this def might already exist somewhere?) I think it should be fine. :)

[Thomas Murrills]

Aaron Liu said:

How does simp do it?

Interestingly, simp uses Term.isLocalIdent?, which is a completely different approach!

getFVarId tries to elaborate the term, then fails if the expression is not an .fvar (and if it is, returns the FVarId). For idents, it uses Term.resolveId?, which resolves any identifier, and adds info to the infotree. In contrast, Term.isLocalIdent? seems to just traverse the local context (etc.) to try to match the actual identifier, without touching the info state.

[Notification Bot]

36 messages were moved here from #mathlib4 > sup/inf or max/min for set interval lemmas? by Eric Wieser.

[Jovan Gerbscheid]

Confusingly, the problem is the other way around. We get a panic if we do restore the state. Here it is further minimized:

import Mathlib.Order.Notation

universe u

class LinearOrder (α : Type u) extends LE α, Min α, Max α, Ord α where

theorem inf_eq_left  {α : Type u} [LE α] [Min α] {a b : α} : min a b = a ↔ a ≤ b := sorry

open Lean Meta Elab Tactic
elab "test" term:term : tactic => do
  let s ← saveState
  let _ ← Term.resolveId? term (withInfo := true) -- comment out `(withInfo := true)` to avoid the panic!
  restoreState s -- comment out this line to avoid the panic!
  let _ ← elabTerm term none

example : False := by
  test inf_eq_left

[Aaron Liu]

Now I'm just confused

[Jovan Gerbscheid]

Somehow, when hovering to see the type, you see the expression from the first time elaborating (with (withInfo := true)), but with the metavariable context from the second time elaborating. restoreState s doesn't affect the InfoTree, but it does affect the metavariable context, thus erasing any universe metavariable that was introduced during the first time elaborating.

[Aaron Liu]

I see

[Thomas Murrills]

@Jovan Gerbscheid what do you mean by the problem being the other way around? We seem to be in agreement that not restoring the info state is the issue.

[Jovan Gerbscheid]

No, my observation is that restoring the state causes the panic

[Jovan Gerbscheid]

In particular restoring the metavariable state removes the universe metavariable from the metavariable context. And that universe metavariable is causing the panic.

[Jovan Gerbscheid]

The best fix in this case would be to avoid (withInfo := true).

[Jovan Gerbscheid]

But there is also an underlying problem of delaboration not using the correct metavariable context.

[Thomas Murrills]

To be clear, the info state I’m talking about refers to the info trees (etc.)! As you observed, when you use restoreState, you’re not restoring the info state. But if you use s.restore (restoreInfo := true), as I mentioned, then the info state is restored as well.

[Jovan Gerbscheid]

You can also see this bug in an arbitrary rw:

import Mathlib
set_option pp.mvars.withType true
example : False := by
  rw [add_comm]

The universe level is different in the "Expected type" and the "tactic 'rewrite' failed".

[Jovan Gerbscheid]

I made a PR to fix this: lean4#8232

[Eric Wieser]

The issue here is that docs#getFVarId causes elaboration?

[Eric Wieser]

Should the docs be updated to suggest using docs#Term.isLocalIdent? when possible instead?

[Jovan Gerbscheid]

I looked at the other uses of getFVarId, and it seems to mostly be used in situations where it is expected that the term is a free variable. So it seems to be used correctly usually.

[Jovan Gerbscheid]

The problem in rw is that the error from getFVarId was being caught

[Bhavik Mehta]

Thanks for figuring this out, everybody!

[Jovan Gerbscheid]

There is a mathlib failure on the PR. Apparently my approach with Term.isLocalIdent doesn't work?

[Aaron Liu]

You need to do it withMainContext

[Aaron Liu]

(this was the product of an hour of debugging)

[Aaron Liu]

By a series of coincidences, not using withMainContext only causes problems when you want to rewrite with a local hypothesis that wasn't present at the beginning of the by block and that has the same name as a (non-ambiguous) global constant, which explains why it didn't cause problems in core.

[Notification Bot]

Jon Eugster has marked this topic as resolved.

[Notification Bot]

Bhavik Mehta has marked this topic as unresolved.

[Bhavik Mehta]

I'm still getting this panic, here's my example:

import Mathlib

example : True := by
  rw [add_max] at *

[Jovan Gerbscheid]

Is it reproducible on Lean web?

[Aaron Liu]

yes

[Aaron Liu]

I reproduced it

[Aaron Liu]

unfortunately, Lean web doesn't report the panics in the backend, so it just shows up as not pretty printing

[Jovan Gerbscheid]

What is not being printed?

[Aaron Liu]

oh that's not what I expected

[Aaron Liu]

maybe nothing's not being printed

[Jovan Gerbscheid]

Ok, I've done some investigation, and it seems that the problem is in tryTactic. It has a try catch block, and the MonadExcept TacticM instance calls Lean.Elab.Term.SavedState.restore, which has a default argument (restoreInfo : Bool := false), and if we set this to true instead of false, then the panic disappears.

The original problem was fixed by making sure the expression is only delaborated once. But for rw at *, the expression needs to be able to be delaborated multiple times.

[Jovan Gerbscheid]

Similarly to before, the problem is that the "expected type" part of the infoview contains some universe level metavaraibles which have been reverted by a try-catch block. But in this case we do want to keep this hover information. (Note that rw adds hover info to the info tree for each place where it tries to rewrite)

[Eric Wieser]

Shouldn't the infoview contain the snapshot before it was reverted, as context?

[Jovan Gerbscheid]

There is this combinator withTacticInfoContext which is called inside withRWRulesSeq. It stores the before & after versions of the MetavarContext into the info tree.

The issue is that the metavariable context is reset before withTacticInfoContext can store it.

[Jovan Gerbscheid]

This version of the bug actually is much more general than just the sup/inf delaborator. Here's a Mathlib-free version:

example : True := by
  rw [Nat.add_comm _] at *

If you put your cursor on the _, then the infoview says

Error updating: Error fetching goals: Rpc error: InternalError: unknown metavariable '?_uniq.4'. Try again.

[Eric Wieser]

Nice minimization!

[Jovan Gerbscheid]

This infoview-breaking bug can also show up in a tactic that succeeds

example (h : 1 + 2 = 3) : True := by
  rw [Nat.add_comm _] at *

[Jovan Gerbscheid]

This example seems to suggest that it would be better to reset the info tree for the locations where the tactic fails. But on the other hand, if the tactic fails everywhere, you'd still want to have some hover information available. But I guess in the case that the tactic fails everywhere, the hover info can be added separately.

[Eric Wieser]

Is this at the point where it's worth filing a bug or moving to #lean4? I think contined conversation in this thread about our unusual delaborators is likely to end up overlooked.

[Bhavik Mehta]

Jovan, would you mind making the bug for this? I think you understand this quite a bit better than me now!

[Jovan Gerbscheid]

lean#10898