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 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