You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
An instance of unification in a Check ends in a stack overflow.
This may be a duplicate of another bug, but for this instance at least, I traced the issue to a call trying to unify ?A with id ?B@{A := ?A} where the occurrence checker doesn't catch the recursive occurrence.
Small Coq file to reproduce the bug
Check (fun (A := ?[A]) (f : A -> id ?[B]) => tt) (fun t => t).
Version of Coq where this bug occurs
8.19.1, master (88a27ca809)
Last version of Coq where the bug did not occur
No response
The text was updated successfully, but these errors were encountered:
Description of the problem
An instance of unification in a
Check
ends in a stack overflow.This may be a duplicate of another bug, but for this instance at least, I traced the issue to a call trying to unify
?A
withid ?B@{A := ?A}
where the occurrence checker doesn't catch the recursive occurrence.Small Coq file to reproduce the bug
Version of Coq where this bug occurs
8.19.1, master (
88a27ca809
)Last version of Coq where the bug did not occur
No response
The text was updated successfully, but these errors were encountered: