Stack overflow with empty local context

Stream: lean4

[Wojciech Nawrocki]

The following code appears to cause a stack overflow:

import Lean
open Lean Elab Term Meta

elab "wat" stx:term : term => do
  withLCtx {} {} do
    elabTerm stx none

#check wat AAA -- unknown identifier 'AAA'
/-
libc++abi: terminating due to uncaught exception of type lean::throwable: deep recursion was detected at 'interpreter' (potential solution: increase stack space in your system)
interpreter stacktrace:
#1 _aux_Lingo_ToMathlib_Franken___elabRules_termWat__1._closed_1
#2 _aux_Lingo_ToMathlib_Franken___elabRules_termWat__1._closed_2
#3 _aux_Lingo_ToMathlib_Franken___elabRules_termWat__1._closed_3
#4 _aux_Lingo_ToMathlib_Franken___elabRules_termWat__1._closed_7
#5 _aux_Lingo_ToMathlib_Franken___elabRules_termWat__1
#6 _aux_Lingo_ToMathlib_Franken___elabRules_termWat__1._boxed
-/
variable (z : wat AAA)

Is this a bug in Lean or ought one not use an empty local context?

[Leonardo de Moura]

It might be a nasty interaction with the autoImplicit feature. Did not explore yet.

[Leonardo de Moura]

Loop goes away when using set_option autoImplicit false

[Gabriel Ebner]

Yes, what happens is that elabTerm (←`(AAA)) throws an exception when the variable name cannot be resolved. Normally, the definition elaborator would then add AAA to the local context and try again, and the next time the name can be resolved successfully. However resetting the local context means that the exception is thrown again every time.

[Wojciech Nawrocki]

Ah, I guess that explains that then!

[Mario Carneiro]

Isn't there a flag to locally block autoImplicit generation (e.g. when not in the signature of a declaration)? I guess the main issue here is that it is not enabled in the above code, and/or that the default setting doesn't use it. I think the default behavior should be to block autoImplicits

[Kyle Miller]

@Mario Carneiro Yeah, there's a flag (docs#Lean.Elab.Term.withoutAutoBoundImplicit), and it's set in the #check wat AAA example due to #check using docs#Lean.Elab.Command.runTermElabM, but variable can't set this flag, so variable (z : wat AAA) fails

[Kyle Miller]

I wonder if when resolveName wants to throw the autoBoundImplicitException it should check that all the names in the TermElabM's autoBoundImplicits array are actually in the current local context (and if not, then don't throw the exception and instead report an unknown identifier). This at least seems like the invariant the autoImplicit feature is meant to keep for it to work.

If the local context has some extra piece of data, like an id that's unique to the given set of auto implicits (generated by withAutoBoundImplicit?), then this check could be done quickly.

[Wojciech Nawrocki]

Kyle Miller said:

Mario Carneiro Yeah, there's a flag (docs#Lean.Elab.Term.withoutAutoBoundImplicit), and it's set in the #check wat AAA example due to #check using docs#Lean.Elab.Command.runTermElabM, but variable can't set this flag, so variable (z : wat AAA) fails

Why can variable not set the flag? Is it just that we do want auto-bound implicits in variable declarations?

[Kyle Miller]

Yes, exactly, binders in variable declarations are one of the places auto-bound implicits are meant to be used.