Equation compiler uses unbounded recursion for matches in tactic blocks

[gebner]

Consider the following lemma:

lemma main : false :=
begin
have helper : true → false := λ ⟨⟩, _fun_match _x,  --<--
exact helper ⟨⟩
end

Currently, the equation compiler thinks that the match expression inside the have tactic is meta, and hence solves it using unbounded recursion. This is clearly not the intended behavior inside a lemma.

The reason is that we store the information whether a match is meta or not inside the equation header, and we set the meta flag when parsing begin-end blocks. This flag is not reset when parsing expression arguments to tactics, so the equation macro in the example has the meta flag set.

Conceptually, I think this information (whether an equation is meta/ncnomputable/etc.) should not be stored in the equations macro, but determined during elaboration (however I don't think the elaborator knows about meta/noncomputable at the moment). @Kha Any ideas? Should we just postpone this to the parser refactoring?

I already fixed the immediate unsoundness by rejecting rec_fn_macro in non-meta declarations when type-checking, so there is no hurry.

[Kha]

should not be stored in the equations macro, but determined during elaboration

Sounds good to me. I think parsing and elaboration always happens inside the same declaration_info_scope, so the elaborator should mostly see the same information as the parser. The only complication should be nested names from matches, for which it may suffice to move the match_scopes into the elaborator...? That may interfere with backtracking in the elaborator though since it updates global state.

If we want to solve this in the elaborator, there is no need to wait for the parser refactoring.

[leodemoura]

Remark: at trust level 0, the lemma is rejected.

../../bin/lean -t0 bug.lean
bug.lean:1:6: error: failed to expand macro
bug.lean:1:0: error: kernel failed to type check declaration 'main' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  false
elaborated value:
  (λ (_x : true), (λ (_x _a : true), true.dcases_on _a ([main._match_1] _x _x)) _x _x) true.intro
nested exception message:
declaration contains macro with trust-level higher than the one allowed (possible solution: unfold macro, or increase trust-level)

[gebner]

@leodemoura Note that with the last commit, the lemma is rejected at every trust level. This issue is about the equation compiler using the wrong strategy.

[leodemoura]

@leodemoura Note that with the last commit, the lemma is rejected at every trust level. This issue is about the equation compiler using the wrong strategy.

I know, I just wanted to make it clear to readers that this kind of issue was being detected at trust level 0.