fix: bug at `typeOccursCheck`

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.74k stars 427 forks source link

fix: bug at `typeOccursCheck` #6104

Closed leodemoura closed 5 days ago

leodemoura commented 1 week ago

This PR fixes bug at typeOccursCheck that allowed cycles in the metavariable assignments.

closes #6013

leanprover-community-bot commented 1 week ago

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-6104 build failed against this PR. (2024-11-17 00:39:54) View Log
🟡 Mathlib branch lean-pr-testing-6104 build against this PR was cancelled. (2024-11-19 06:01:44) View Log
✅ Mathlib branch lean-pr-testing-6104 has successfully built against this PR. (2024-11-19 06:42:32) View Log

kim-em commented 6 days ago

This needed one extra type ascription in Plausible, but otherwise Mathlib was unharmed.

kim-em commented 6 days ago

Oh! The change required in Plausible is exactly what is now failing in the test typeOccursCheckIssue.lean.

JovanGerb commented 6 days ago

At #6128, I made a change to not create unused let binders in metavariable types when eliminating dependencies. This, together with a proper type occurs check, closes #6013 and causes no breakages.