Panic while typing eval'd `fun`

Stream: lean4

[Thomas Murrills]

I have a temporary convenience command local_linter which allows me to declare a linter locally via e.g. local_linter foo := fun stx => do ... which will run on the file. However, in the middle of typing, at local_linter foo := fun, Lean panics. Here's why:

Although we have a parse error at this location, lean still attempts to elaborate fun, and this yields a sorry in the resulting nomatch from this MVarId.admit during match elaboration (despite withoutErrToSorry being present, since the elaboration happens in MetaM). Then, my subsequent evalExpr panics on the sorry when trying evaluate it.

I think there are three things to examine here:

1. Should elaboration proceed even though we have a parse error here? In general it makes sense to elaborate as much as possible, but I'm not sure about elaborating a lone fun in these circumstances specifically.
2. Should match elaboration insert a sorry here? I would have maybe expected an error, and a sorry up in TermElabM when errToSorry is true; though perhaps that would mean throwing an error for the entire match (which we don't want)?
3. Should evalExpr (or something it calls) be robustified against sorry? It's easy enough to collectAxioms myself and check for sorry like #eval does, but I wonder if evalExpr should do this too.

All in all this is not so much a "how do I work around this" thread, but a "should we change these behaviors that it brought to light" thread. :)

And here's an #mwe:

module
public import Lean
open Lean Meta Elab Term Command
public section

elab "#huh " t:term : command => liftTermElabM do
  let e ← withoutErrToSorry <| withSynthesize <| elabTerm t (Expr.const ``Bool [])
  let axioms ← (e.getUsedConstants).mapM collectAxioms
  let hasSorry := axioms.any (·.contains ``sorryAx)
  -- note: logInfo's message is obliterated in this circumstance, so trace instead
  trace[debug] "{e} has sorry := {hasSorry}"

set_option trace.debug true
/-- trace: [debug] nomatch has sorry := true -/
#guard_msgs in
#huh fun -- unexpected end of input; expected '[', '{', '|' or '⦃'

[Kyle Miller]

1. If you don't want to do anything when there is partial syntax, you can abort elaboration if you see that t has a missing node. You can assume missing means a parse error was emitted.
2. The #eval command uses collectAxioms for the stronger check that there is no sorry at all. To detect elaborator errors, it suffices to check for a synthetic sorry in the term. I'm not sure why withoutErrToSorry doesn't suffice here. Possibly it's not hitting an elaboration error, despite the sorry inside the term. Or possibly there's some interaction with missing I'm not sure about. Or there's something about match that's not respecting it.
3. This collectAxioms check is making sure you're not getting away with using sorry for empty terms (e.g. false propositions). There's nothing inherently wrong with having sorry in a term. If you try #eval! (sorry : Nat) you can see there's an error despite turning off the the sorry check, not a panic.

[Thomas Murrills]

Thanks! :)

1. Good to know; though I was wondering more about whether the current behavior makes sense, than about what I could do! I.e. I'm skeptical it makes sense for elaboration of a lone fun itself to proceed when those .missing nodes are present.
2. a. re: synthetic sorry checking: makes sense; though, do you happen to know if there's API for that? Note that this sorry is hidden in the value of an autogenerated match_n decl, so hasSyntheticSorry returns false. (collectAxioms therefore seems more convenient than e.g. ImportGraph's transitivelyUsedConstants.)
3. b. Does something during term elaboration check for synthetic sorries, and error if it finds them? I thought that because no error is logged (by mkLabeledSorry, MVarId.admit, or match when admitting), withoutErrToSorry is not relevant in the first place—the sorry is directly constructed. (Perhaps one of these should log an error; mkLabeledSorry says it's the caller's responsibility.)
4. Ah, right, thanks for pointing that out. The "unreachable code" panic (which now that I look at it closely, might not be a panic! per se?) doesn't come from evalExpr; it seems like it comes from actually trying to run the resulting CommandElab on syntax (whether in the elabimmediately or through the lintersRef as intended).

[Thomas Murrills]

(Here’s an updated panicking mwe for completeness!)

module
public import Lean
public import Qq
open Lean Meta Elab Term Command Qq
public section

abbrev BoolToBool := Bool → Bool

elab "#huh " t:term : command => unsafe liftTermElabM do
  let e ← withoutErrToSorry <| withSynthesize <| elabTerm t q(Bool → Bool)
  let axioms ← (e.getUsedConstants).mapM collectAxioms
  let hasSorry := axioms.any (·.contains ``sorryAx)
  -- note: logInfo's message is obliterated in this circumstance, so trace instead
  trace[debug] "{e} has sorry := {hasSorry}"
  let e ← evalExpr (Bool → Bool) q(Bool → Bool) e
  logInfo m!"{e true}"

set_option trace.debug true
/-- trace: [debug] nomatch has sorry := true -/
#guard_msgs in
#huh fun -- panic; unexpected end of input; expected '[', '{', '|' or '⦃'

[Kyle Miller]

1. I don't mean this as a workaround, but rather it's intended that elaboration proceed even if there are missing nodes. This is how term info (hovers) for partial terms works.
2. a. Yes, Expr.hasSyntheticSorry. However, if there's already been a parse error, it's unclear to me whether you can rely on the presence of a synthetic sorry. b. There's already a parse error logged, so further errors aren't shown. Log messages also have some interface for reporting whether they contain an expression containing synthetic sorries, which is used somehow for further error suppression.
3. It might be worth trying to figure out where the panic is coming from more precisely. Maybe try set_option showPartialSyntaxErrors true (to disable the .missing elaboration error suppression) or otherwise create the partial Syntax yourself.

[Thomas Murrills]

1. Thanks for clarifying; that makes sense, but perhaps we are trying to make different points :) For my part, I believe that the core elaboration for fun or match specifically could be polished a little when .missing nodes are present; the hover for fun becomes nomatch in this case, which is unhelpful. Perhaps a more deliberate sorry of function type might be ideal—but this is polishing. :)
2. a. As I mentioned, though, hasSyntheticSorry is insufficient here; though there is indeed a sorry (and it is synthetic), it's locked behind an autogenerated match decl, and hasSyntheticSorry does not unfold constants like collectAxioms does (and thus misses that sorry). The hypothetical API I'm asking about would therefore unfold constants; I suspect it doesn't exist.
3. b. Hmm, interesting!
4. I don't believe the panic has to do with syntax directly (though is of course downstream of the sorry produced by the missing syntax); rather, a declaration shaped like the autogenerated match (with sorry : False in the given position) is sufficient. eval! errors with "'unreachable' code was reached" but does not panic; let _ := r true in the elab does not panic; but IO.println <| r true panics. So perhaps this is a clue as to what is actually reaching the unreachable code—the language server? But I'm not sufficiently familiar with the structure there to diagnose it precisely.

syntax-free mwe

module
public import Lean
public import Qq
open Lean Meta Elab Term Command Qq

private def match_foo.{u_1} : (motive : Sort u_1) → motive :=
fun motive => (sorry : False).elim

/-- error: 'unreachable' code was reached -/
#guard_msgs in
#eval! match_foo (Bool → Bool) true

set_option showPartialSyntaxErrors true
elab "#panic" : command => unsafe liftTermElabM do
  let r ← evalExpr (Bool → Bool) q(Bool → Bool) <|
    mkAppN (Expr.const ``match_foo [1]) #[q(Bool → Bool)]
  IO.println <| r true

-- #panic