Weird Error with Custom Nat Lits

Stream: lean4

[Mac]

So I was defining a Sort-polymorphic instead of Type-polymorphic nat lit and ran into the following weird error:

class OfNatLit (A : Sort u) (n : Nat) :=
  ofNatLit : A

@[defaultInstance low]
instance {A : Type u} {n : Nat} [K : OfNat A n] : OfNatLit A n
  := {ofNatLit := K.ofNat}

instance {A : Type u} {n : Nat} [K : OfNatLit A n] : OfNat A n
  := {ofNat := K.ofNatLit}

abbrev Zero (A : Sort u) := OfNatLit A (natLit! 0)

-- Before Syntax ovveride: Works as expected on Type
def fooT {A : Type u} [Zero A] (f : A -> Prop) := f 0

-- Before Syntax ovveride: Errors as expected on Sort
def fooS {A : Sort u} [Zero A] (f : A -> Prop) := f 0
/-
  invalid universe level, ?u.136 is not greater than 0
-/

syntax (name := sortNumLit) (priority := default + 1) num : term
macro_rules [sortNumLit]
  | `( $n:numLit) => `(OfNatLit.ofNatLit (natLit! $n))

-- After syntax override: Errors unexpectedly w/o type scription
def fooS' {A : Sort u} [Zero A] (f : A -> Prop) := f 0
/-
  invalid universe level, ?u.525 is not greater than 0
-/

-- After syntax override: But works as expected w/ type ascription
def fooS'' {A : Sort u} [Zero A] (f : A -> Prop) := f (0 : A)

Why does 0 with a type ascription work, but 0 without one error? This seems like a bug in Lean.

[Mario Carneiro]

btw natLit! has been renamed to nat_lit

[Mario Carneiro]

It seems like the updated syntax macro is not triggering. I tried this:

#eval show TermElabM Syntax from do
  liftMacroM <| expandMacros (← `(term| f 0)) -- unknown parser term
#eval show TermElabM Syntax from do
  liftMacroM <| expandMacros (← `(f 0)) -- (Term.app `f._@._hyg.1 [(numLit "0")])

which seems like there isn't any macro expansion happening, but I think I'm not doing it right. @Sebastian Ullrich help!

[Sebastian Ullrich]

So as you see in Mario's output (or, even better in general, using pp.raw and trace.Elab options), there is no sortNumLit syntax node to begin with, i.e. the problem is the parser and not the macro. So why would 0 be parsed differently in f 0 and in f (0 : A)? The only sensible answer is precedences: syntax will default to a precedence of lead (which is lower than the "acceptable as an argument" precedence arg) unless the syntax is "atomic-like", which is necessarily an incomplete heuristic.

[Sebastian Ullrich]

We could add all *Lit kinds to that heuristic, sure. On the other hand, there isn't really a point in introducing a syntax that is equivalent to an existing one, instead we can add a new macro for the existing syntax. Now, not sure if you already tried that, but it does turn out that there are some limitations with macro_rules that currently make that harder than it should be.

-- fails
macro_rules [numLit]
  | `($n:numLit) => `(OfNatLit.ofNatLit (nat_lit $n))

-- succeeds, but registers macro for the wrong syntax kind
macro_rules
  | `($n:numLit) => `(OfNatLit.ofNatLit (nat_lit $n))

-- the hard way, then
@[macro numLit] def expandNumLit' : Lean.Macro
  | `($n:numLit) => `(OfNatLit.ofNatLit (nat_lit $n))
  | _            => Lean.Macro.throwUnsupported

[Mario Carneiro]

Do you know why the `(term| ...) syntax doesn't work @Sebastian Ullrich ?

[Mario Carneiro]

What syntax category is f 0 in if not term?

[Sebastian Ullrich]

The named quotations are currently hard-coded. There isn't one for term since it would be redundant.

[Sebastian Ullrich]

Generalizing the syntax yields some "interesting" implementation issues with cyclically dependent subsystems

[Mac]

Sebastian Ullrich said:

On the other hand, there isn't really a point in introducing a syntax that is equivalent to an existing one, instead we can add a new macro for the existing syntax.

Unfortunately, I did not know you could add macros to existing syntax kinds like that. However, looking at it now, there was a reason why I made it a separate syntax. Namely, as far as I am aware, you can't scope macro rules. I really wanted the following (I just eliminated the namespaces in my original example to make a #mwe):

namespace Test
scoped syntax (name := sortNumLit) (priority := default + 1) num : term
macro_rules [sortNumLit]
  | `( $n:numLit) => `(OfNatLit.ofNatLit (nat_lit $n))
end Test

open Test

However, the following does also work:

namespace Test
@[scoped macro numLit] def expandNumLit : Lean.Macro
  | `($n:numLit) => `(OfNatLit.ofNatLit (nat_lit $n))
  | _            => Lean.Macro.throwUnsupported
end Test

-- Does not work as expected
def fooS {A : Sort u} [Zero A] (f : A -> Prop) := f 0

open Test

-- Works as expected
def fooS' {A : Sort u} [Zero A] (f : A -> Prop) := f 0

So, thanks!

[Sebastian Ullrich]

Yes, if we want to go that way, we should add local/scoped macro(_rules)

[Mac]

Sebastian Ullrich said:

On the other hand, there isn't really a point in introducing a syntax that is equivalent to an existing one, instead we can add a new macro for the existing syntax.

I have discovered another good reason to make it new syntax. Overriding numLit breaks the syntax command:

syntax:max (name := newNumLit) num : term
@[macro newNumLit]
def expandNewNumLit : Lean.Macro
  | n => `(OfNat.ofNat (nat_lit $n))

-- Works fine
syntax "foo" : term

@[macro numLit]
def expandNumLit : Lean.Macro
  | n => `(OfNat.ofNat (nat_lit $n))

-- Now breaks
syntax "bar" : term
/-
maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)
-/

[Mac]

Though I suspect this may be a bug that needs fixing.

[Leonardo de Moura]

The macro

@[macro numLit]
def expandNumLit : Lean.Macro
  | n => `(OfNat.ofNat (nat_lit $n))

triggers nontermination in any term containing a numeral. The elaborator interrupts the "infinite loop" using the maximum recursion depth threshold.
For example, suppose Lean tries to elaborate the numeral 2. Your macro expands it to

(OfNat.ofNat (nat_lit 2))

but 2 is a subterm of this term, and your macro is applied again, and so on.

[Sebastian Ullrich]

#check 2 works for me, which makes sense because 2 is not a term in nat_lit 2. The issue seems to be the attribute argument @[termParser 1024], because we eagerly unfold attribute arguments using expandMacros.

[Sebastian Ullrich]

Thus a simple workaround would be to make the macro an elaborator... but then Lean has to be imported

[Leonardo de Moura]

Yes, the macro only causes non-termination if another elaborator or macro invokes expandMacros
For example, the match-elaborator uses expandMacros on patterns

@[macro numLit] def expandNumLit : Lean.Macro
  | n => `(OfNat.ofNat (nat_lit $n))

def f (x : Nat) : Bool :=
  match x with   -- non-termination
  | 0 => true
  | _ => false

Here is a minimal example that triggers.

macro "tst" x:num : term => Lean.expandMacros x

@[macro numLit] def expandNumLit : Lean.Macro
  | n => `(OfNat.ofNat (nat_lit $n))

#check tst 2  -- non-termination

That being said, the problem is the expandNumLit macro that produces a term containing the input term.

[Leonardo de Moura]

#check 2 works for me, which makes sense because 2 is not a term in nat_lit 2

@Sebastian Ullrich 2 is a subterm of nat_lit 2. #check 2 doesn't loop because the nat_lit elaborator does not invoke elabTerm or expandMacros on the subterm 2.

The nat_lit elaborator is

@[builtinTermElab rawNatLit] def elabRawNatLit : TermElab :=  fun stx expectedType? => do
  match stx[1].isNatLit? with
  | some val => return mkNatLit val
  | none     => throwIllFormedSyntax

[Mario Carneiro]

Sebastian Ullrich said:

Thus a simple workaround would be to make the macro an elaborator... but then Lean has to be imported

What is the reason that import Lean should be avoided? Back in lean 3 days this would basically always be true, and I've just been doing that whenever it is needed. Is there some hidden performance cost of this?

[Sebastian Ullrich]

There is no hidden cost, but Lean is simply very big compared to Init, so we are at least concerned about importing performance (and maybe performance of other declaration search parts like completion). Right now import Lean increases import time from 38ms to 380ms for me, which is insignificant for a single file... though keep in mind that all downstream modules will inherit that overhead. All of that would be resolved with https://github.com/leanprover/lean4/issues/416... if we can in fact pull it off.

[Mario Carneiro]

I assume that in files where you actually care about the cost to downstream file imports, you can use a more selective import like import Lean.Elab or what have you? Or is everything mutually dependent enough that this has little advantage?

[Mario Carneiro]

(Coming from lean 3 where import times of 5-10 seconds are not unusual, I'm not particularly put off by a 380ms import time :P )

[Mac]

In my experience, there is significant noticeable lag when adding a Lean import when editing in VS Code. I also feel like the response time of the editor decreases somewhat (though not significantly). Though I suspect if most complex metaprogramming requires the whole of Lean to be imported, I imagine most libraries will end up doing so. Thus, I doubt we can really get away from it unless some form of noncumulative/selective importing is introduced (such as the aforementioned module system).

[Sebastian Ullrich]

If you register your complex tactics as built-in tactics and compile them down to shared libraries (which you might want to do anyway), you can load them as plugins without actually importing their code, or their dependencies. This is the one way we imagined for "escaping" from import Lean without the module system.

[Sebastian Ullrich]

Mario Carneiro said:

I assume that in files where you actually care about the cost to downstream file imports, you can use a more selective import like import Lean.Elab or what have you? Or is everything mutually dependent enough that this has little advantage?

There aren't too many mutual dependencies between subsystems, but at least with Lean.Elab you do get almost everything (but the language server implementation).

[Sebastian Ullrich]

IOW, import Lean.Elab is ~310ms

[Mario Carneiro]

Sebastian Ullrich said:

If you register your complex tactics as built-in tactics and compile them down to shared libraries (which you might want to do anyway), you can load them as plugins without actually importing their code, or their dependencies. This is the one way we imagined for "escaping" from import Lean without the module system.

I guess that mathlib will not be able to escape import Lean then, because even with the mathlib prelude handling the majority of tactics we will still want to write small interactive tactics (that we don't mind being interpreted) inside mathlib itself. What about some kind of "header only" way to import files? I guess you could say that lean 3 did that since most substantial tactics were written in C++ and exposed as constant to lean.

[Mario Carneiro]

I see now that the linked module system issue is also trying to solve this problem, although I want to point out that the requirements of improving import BigDependency inside the server mode, say for proof authoring, are slightly different from separate compilation, and perhaps some problems that arise in the pursuit of separate compilation aren't as big of a deal when simply making it possible to write interpreted tactics calling lean builtins.

[Sebastian Ullrich]

builtinTactic is such a header system in absence of a true module system. It allows you to use builtin tactics in macros without importing them. If you need a procedural tactic, you have to import at least Lean.Elab.Tactic.Basic anyway (which currently clocks in at ~170ms), in which case you can use evalTactic together with a syntax quotation of the builtin tactic to call it, still without actually importing it.

[Sebastian Ullrich]

Mario Carneiro said:

although I want to point out that the requirements of improving import BigDependency inside the server mode

I should probably clarify that I don't see improving server mode as a concern for the module system, since imports are fast enough for that anyway as we said above. In fact, I could imagine that we would want to lift some import restriction in server mode so that we can still #eval arbitrary things and e.g. show completion items that would automatically insert necessary additional imports (though ideally in a way that code outside from #eval would still only be accepted if it was also accepted in batch mode; that part might be a bit tricky). If libraries like mathlib want to embrace the module system, the main benefit would still be separate compilation: rebuilding as few files of it as possible on (most) changes.