metavariable loops

Stream: lean4

[Eric Wieser]

I'm a little surprised that this doesn't give an error about a cycle existing:

import Lean

open Lean Elab Meta Tactic

-- (kernel) declaration has metavariables 'foo'
theorem foo : False := by
  run_tac do
    let target ← Tactic.getMainGoal
    -- make a metavariable loop
    let e : Expr ← mkFreshExprMVar (← target.getType)
    target.assign e
    e.mvarId!.assign (.mvar target)
    setGoals []

set_option pp.rawOnError true
#print foo

[Aaron Liu]

docs#Lean.MVarId.assign explicitly says it does not check for cycles.

[Eric Wieser]

If you use docs#Lean.MVarId.assignIfDefeq you get the same problem

[Kyle Miller]

I think docs#Lean.MVarId.checkedAssign is supposed to do an occurs check

[Eric Wieser]

Thanks, that's enough to tell me I'm doing something wrong, but I don't yet know what!

[Kyle Miller]

I think it's likely there are many latent Lean bugs out there due to using MVarId.assign.

At least MVarId.assignIfDefeq does a defeq check on the types first, which sometimes is enough to exclude cycles.

Lean core ought to implement some consistency check functions that can be used to diagnose issues like this. (Some issues that come to mind: valid metacontext state, valid local contexts, that synthetic metavariables have the correct kinds and have consistent associated data, that delayed assignment metavariables have not been assigned directly).

[Kyle Miller]

Feel free to say a bit more about what you're up to.

[Eric Wieser]

I'm trying to bundle a list of interdependent MVarIds (let's say they all have no local context) into one big PSigma goal

[Kyle Miller]

That sounds like it could be tricky. Do you know that there exists some topological sort of the dependencies?

[Eric Wieser]

In a well-formed proof, is the answer always "yes"?