panic with SimpleGraph fun

Stream: mathlib4

[Bhavik Mehta]

import Mathlib.Combinatorics.SimpleGraph.Basic

def SimpleGraph.Sigma {ι : Type u} {V : ι → Type v} (G : (i : ι) → SimpleGraph (V i)) :
  SimpleGraph (Σ i, V i) where
    Adj := fun
    | \
    symm := _
    loopless := _

typing this in gives the error:
"Lean server printed an error: PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:317:22: unreachable code has been reached"
with the output page saying

PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:317:22: unreachable code has been reached
PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:317:22: unreachable code has been reached

This is on 4.0.0-nightly-2023-07-12

[Kevin Buzzard]

I can reproduce. Maybe the attached video is evidence that it's something to do with aesop_graph? But maybe not -- I don't know the first thing about panics.

panic.gif

[Kyle Miller]

From reading the source, this panic means that there is a loose bvar in an expression that's passed to whnf. The whnf code assumes there are no loose bvars. (A bvar can show up if some code looks into the body of a forall or lambda without doing the right sort of binder initialization. I don't have any insight here though.)

[Scott Morrison]

I've run into this error when trying to put fragments of expressions (that had loose bvars) into a DiscrTree. If aesop_graph is involved that could be possibility.

[Jannis Limperg]

Looks like it could be an Aesop issue. I'm investigating.

[Jannis Limperg]

Was indeed a bug in Aesop's intros builtin tactic, which sometimes ran whnf on expressions with loose bvars. Now fixed.

[Jannis Limperg]

And lean4#2338 to turn the panic in whnf into an error, though I'm not 100% sure whether this is a good idea.

[Sebastian Ullrich]

I agree with that assessment :)

[Jannis Limperg]

Why is that?

[Sebastian Ullrich]

Basically all Meta APIs assume that there are no loose bvars, it's the locally-nameless invariant. I understand that Aesop does some novel things with the context, but at least in Lean this would always point to a bug in another place

[Jannis Limperg]

Yes, I also observe this invariant (well, usually...). But when, due to a bug, the invariant is violated, it's easier to find the bug if you have some more info. I guess you're worried that the exception might get caught by some catch-all exception handler?

[Sebastian Ullrich]

Yes, we wouldn't want to bracktrack on it, say

[Sebastian Ullrich]

Knowing the pretty printing of the loose bvar isn't all that much more helpful though, is it?

[Jannis Limperg]

Makes sense. So ideally, we would carry around the whole expression, then panic with an informative error message if there's a loose bvar. But carrying around the expression is probably overkill.

[Kyle Miller]

Rather than unreachable!, it might be more friendly if it were panic! "loose bvar in expression"

[Kyle Miller]

"unreachable code has been reached" is not really accurate, since it's not whnf's fault that the caller broke the invariant

[Jannis Limperg]

Yes, I'll refactor the PR accordingly.