fix: stack overflow at mkBinding if type occurs check fails

[JovanGerb]

This PR fixes a stackoverflow bug in mkBinding caused by metavariables appearing in their own type.

Closes #6013
Closes #3150 edit: this has been closed

[leanprover-community-bot]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-6079 build this PR didn't complete normally. (2024-11-14 15:32:10) View Log
• ✅ Mathlib branch lean-pr-testing-6079 has successfully built against this PR. (2024-11-14 16:35:19) View Log
• 🟡 Mathlib branch lean-pr-testing-6079 build against this PR was cancelled. (2024-11-15 14:28:32) View Log
• ✅ Mathlib branch lean-pr-testing-6079 has successfully built against this PR. (2024-11-15 15:06:05) View Log

[kim-em]

@JovanGerb could you confirm that #6105 has resolved this?

[JovanGerb]

It is only partially resolved. #6105 closes #3150 by avoiding the type occurs check failure in elaborating structure instances.

#6013 is unaffected.

[leodemoura]

@JovanGerb I am concerned about this PR. We want to avoid cyclic dependencies in the metavariable assignment. This PR goes in a different direction: let's tolerate cycles. For example, in #3150, we were adding an assignment without performing the occurs check. This PR would "mask" the real problem.

[JovanGerb]

That makes sense.

In the PR that introduced the type occurs check, commit 72e5528 defines skipAtMostNumBinders, which somewhat allows cyclic dependencies. (Although I didn't understand where in mathlib or the test file this was happening). Should this be modified to avoid cyclic dependencies?

[leodemoura]

@JovanGerb

Should this be modified to avoid cyclic dependencies?

#6104 does that, but unfortunately it breaks a test. The test comes from a real repo: Plausible.
They would have to add an extra annotation (i.e., (β := β)) here:

      let nextStep := minimizeAux cfg var candidate (n + 1)

I will discuss with the author whether the change is reasonable or not.

[JovanGerb]

Looking at that breaking test, I think this may be fixed with the change I suggested in the last comment on #6013. The particular cyclic metavariables occurrence is in the value of a let-expression where the bound variable doesn't appear in the body. So modifying

lean4/src/Lean/MetavarContext.lean

Lines 1074 to 1084 in 9f42368

	| LocalDecl.ldecl _ _ n type value nonDep _ =>
	let type := type.headBeta
	let type ← abstractRangeAux xs i type
	let value ← abstractRangeAux xs i value
	let e := mkLet n type value e nonDep
	match kind with
	| MetavarKind.syntheticOpaque =>
	-- See "Gruesome details" section in the beginning of the file
	let e := e.liftLooseBVars 0 1
	return mkForall n BinderInfo.default type e
	| _ => pure e

so that it only creates the let if there is a bound variable may help.

[JovanGerb]

Closing, with an alternative solution at #6128.