feat: abstractMVars: do not loop on bad input

[nomeata]

previously abstractMVars would go into a loop on bad input, in
particular if an mvar occurs in its own type. While this should never
happen in practice and is thus not a problem for our users, it can be
quote annoying when one runs into this problem while developing meta
code, as the stack overflow means you don’t get your trace messages
etc.

By keeping track of the mvars whose type we are processing we can break
the loop. The function is pure, so no throwError, but even a panic!
is going to be somewhat helpful.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-4378 has successfully built against this PR. (2024-06-06 18:27:05) View Log

[leodemoura]

@nomeata Let's discuss this PR in our next 1:1. There are many other places in the code that will loop if there are circular assignments at MetavarContext. The assign operation is a low-level one. We should improve its documentation instead, and make it clear that it is the caller responsibility to ensure a circular assignment is not created. We may also point users to higher level functions that perform occurs-check (e.g., isDefEq).

[nomeata]

Right, this is right now a draft so that I can find my bugs. We talked a bit at the tea time about this, and it seems that the isDefEq advice isn't fully correct, as it would not assign mvars of type Prop?

I would find it helpful if the API and it's docs could be improved. In particular a .checkedAssign is something that I often wanted, i.e. like assign (safe, returning Unit not Bool).

Also note that here it's not a circular assignment but a circular type (the mvar is unassigned, but occurs is in its own type) that cause this to fail baldy. Do the safe functions check for that?

[leodemoura]

Right, this is right now a draft so that I can find my bugs. We talked a bit at the tea time about this, and it seems that the isDefEq advice isn't fully correct, as it would not assign mvars of type Prop?

Not true. If we call isDefEq on ?m and a term t, the assignment is performed before we try to use proof irrelevance. Here is an example.

import Lean

open Lean Meta
run_meta do
  let mvar ← mkFreshExprMVar (mkConst ``True)
  let term := mkConst ``True.intro
  IO.println (← ppExpr mvar). -- ?m
  IO.println (← isDefEq mvar term) -- true
  IO.println (← ppExpr mvar) -- True.intro

Here is a bad example using assign which creates a cycle

run_meta do
  let mvar1 ← mkFreshExprMVar (mkConst ``True)
  let mvar2 ← mkFreshExprMVar (mkConst ``True)
  mvar1.mvarId!.assign mvar2
  mvar2.mvarId!.assign mvar1 -- Bad, cycle created
  IO.println (← ppExpr mvar1)
  IO.println (← ppExpr mvar2)

Same example, using isDefEq to avoid the cycle

run_meta do
  let mvar1 ← mkFreshExprMVar (mkConst ``True)
  let mvar2 ← mkFreshExprMVar (mkConst ``True)
  mvar1.mvarId!.assign mvar2
  IO.println (← isDefEq mvar2 mvar1) -- true, and no cycle created
  IO.println (← ppExpr mvar1)
  IO.println (← ppExpr mvar2)

[leodemoura]

I would find it helpful if the API and it's docs could be improved. In particular a .checkedAssign is something that I often wanted, i.e. like assign (safe, returning Unit not Bool).

We can implement .checkedAssign using isDefEq. It performs many checks before assigning ?m := e

• Cyclic assignments
• ?m and e types are definitionally equal.
• Local context compatibility. That is, e does not contain a free variable that is not on ?m's local context.

[nomeata]

Thanks. Does it also check that the type of the mvar doesn't mention the mvar, possibly indirectly? (I am not 100% certain, but I think I ran into the infinite loop using just isDefEq, no assign.)

(Maybe I misunderstood what Sebastian said about proof irrelevance and mvars. Maybe it's mvars nested inside proofs.)

[nomeata]

Thanks. Does it also check that the type of the mvar doesn't mention the mvar, possibly indirectly? (I am not 100% certain, but I think I ran into the infinite loop using just isDefEq, no assign.)

Was able to condense it to a mwe at #4405.

[leodemoura]

Thanks. Does it also check that the type of the mvar doesn't mention the mvar, possibly indirectly? (I am not 100% certain, but I think I ran into the infinite loop using just isDefEq, no assign.)

(Maybe I misunderstood what Sebastian said about proof irrelevance and mvars. Maybe it's mvars nested inside proofs.)

@nomeata This check is not performed. It is a different discussion whether it should be included in isDefEq or not. We need more evidence it is useful instead of just extra unnecessary work. The example in #4405 looks artificial to me, and was constructed programmatically. I don't recall ever seeing in real code a cyclic assignment issue similar to the issue described in #4405. What about the following:

• You start using isDefEq or a wrapper (checkedAssign) on top of it.
• If you still hit a loop, we investigate and understand what is going on. Then, we can decide whether it is needed.

[nomeata]

I was using isDefEq, and I was hitting this in practice, and because it manifested as a stack overflow (so no catching exceptions, no trace messages, although good old IO.eprintln helped to debug it) it took me some time to get to the bottom of it. Of course I was doing something in a way that nobody else did before, it seems, if I stumbled first over this, but at least I didn't feel particularly naughty doing it. It doesn't seem unreasonable to me to hope for a bit more robustness of the Meta API.

(I wonder if I can reproduce it using conv if that makes it more relevant.)

[nomeata]

Of course it's totally fair to say that what I am doing here is a bit too obscure (and now that I know what to look out for I am no longer blocked) and we wait to see if others hit the same issue before acting.

[leodemoura]

I was using isDefEq, and I was hitting this in practice, and because it manifested as a stack overflow (so no catching exceptions, no trace messages, although good old IO.eprintln helped to debug it) it took me some time to get to the bottom of it. Of course I was doing something in a way that nobody else did before, it seems, if I stumbled first over this, but at least I didn't feel particularly naughty doing it. It doesn't seem unreasonable to me to hope for a bit more robustness of the Meta API.

(I wonder if I can reproduce it using conv if that makes it more relevant.)

Let's talk about it next time we meet. I would love to see the code and how it happened.
If this is a recurrent thing for you, we can add Context.extraDefEqChecks that when set to true will perform extra sanity checks.

[nomeata]

You were right to ask for better evidence. I didn’t necessarily expect that to be possible, but it is possible to trigger a stack overflows without using the programmatic interface. Added it to #4405 (comment).

[leodemoura]

You were right to ask for better evidence. I didn’t necessarily expect that to be possible, but it is possible to trigger a stack overflows without using the programmatic interface. Added it to #4405 (comment).

Thanks. I will work on a fix this week for #4405.