-
Notifications
You must be signed in to change notification settings - Fork 437
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
fix: bug at typeOccursCheck
#6104
Conversation
Mathlib CI status (docs):
|
visitMVar (mvarId' : MVarId) (numArgs : Nat := 0) : Bool := | ||
if let some mvarDecl := mctx.findDecl? mvarId' then | ||
occursCheck (skipAtMostNumBinders mvarDecl.type numArgs) | ||
if let some b := skipAtMostNumBinders? mvarDecl.type numArgs then |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Wouldn't it make more sense to get rid of skipAtMostNumBinders?
altogether? Its only purpose now is to avoid doing the occurs check in some forall binder types. But not doing the type occurs check is exactly the bug we're trying to fix.
This PR fixes bug at `typeOccursCheck` that allowed cycles in the metavariable assignments. closes #6013
840b98e
to
fd193fe
Compare
This needed one extra type ascription in |
Oh! The change required in Plausible is exactly what is now failing in the test |
This PR does the same fix as #6104, but such that it doesn't break the test/the file in `Plausible`. This is done by not creating unused let binders in metavariable types that are made by `elimMVar`. (This is also a positive thing for users looking at metavariable types, for example in error messages) We get rid of `skipAtMostNumBinders`. This function was originally defined for the purpose of making this test work, but it is a hack because it allows cycles in the metavariable context. It would make sense to split these changes into 2 PRs, but I combined them here to show that the combination of them closes #6013 without breaking anything Closes #6013
This PR fixes bug at
typeOccursCheck
that allowed cycles in the metavariable assignments.closes #6013