fix: Cleanup delayed_check with sort variables

Author: TDiazT

engine/uState.ml

@@ -158,18 +158,18 @@ let set q qv m =
   let q, rigid = match q with ReprVar (q, rigid) -> q, rigid | ReprConstant _ -> assert false in
   let qv = match qv with QVar qv -> repr_node qv m | QConstant qc -> ReprConstant qc in
   let enforce_eq q1 q2 g = QGraph.enforce_eliminates_to q1 q2 (QGraph.enforce_eliminates_to q2 q1 g) in
-  match q, qv with
-  | q, ReprVar (qv, _qvrigd) ->
+  match qv with
+  | ReprVar (qv, _qvrigd) ->
     if QVar.equal q qv then Some m
     else if rigid then None
     else
       let above_prop =
         if is_above_prop m q
         then QSet.add qv (QSet.remove q m.above_prop)
         else m.above_prop in
-      Some { qmap = QMap.add q (Equiv (QVar qv)) m.qmap; above_prop;
-             elims = enforce_eq (QVar qv) (QVar q) m.elims; initial_elims = m.initial_elims }
-  | q, ReprConstant qc ->
+      Some { m with qmap = QMap.add q (Equiv (QVar qv)) m.qmap; above_prop;
+                    elims = enforce_eq (QVar qv) (QVar q) m.elims; }
+  | ReprConstant qc ->
     if qc == QSProp && (is_above_prop m q || eliminates_to_prop m q) then None
     else if rigid then None
     else

kernel/qGraph.ml

@@ -154,11 +154,31 @@ let rec update_dominance g q qv =
     | Some q' -> update_dominant_if_related g qv q' q in
   match QMap.find_opt qv g.delayed_check with
   | None -> g'
-  | Some qs ->
-     let g' = QSet.fold (fun v g -> Option.bind g (fun g -> update_dominance g q v)) qs g' in
-     match g' with
-     | Some graph -> Some { graph with delayed_check = QMap.set qv QSet.empty g.delayed_check }
-     | None -> None
+  | Some delayed_qs ->
+    (* When two sort variables are `set` to each other, e.g. uState, (q1 <-> q2), without being
+       dominated, then both delay the domination check of each other:
+       delayed_check[q1] = {q2}
+       delayed_check[q2] = {q1}
+
+       When one of them becomes dominated, e.g. q1 dominated by Type, then we need to clear up
+       any occurrence of it in the delayed check of the other, e.g. remove q1 from delayed_check[q2].
+       Otherwise, we end up in a loop. *)
+    let remove_qv_from_delayed delayed_q delayed_check =
+      match QMap.find_opt delayed_q delayed_check with
+      | None -> delayed_check
+      | Some dqs ->
+        QMap.set delayed_q (QSet.remove qv dqs) delayed_check
+    in
+    let clearup_cyclic_delay graph =
+      QSet.fold (fun delayed_q acc_graph ->
+        { acc_graph with delayed_check = remove_qv_from_delayed delayed_q acc_graph.delayed_check })
+        delayed_qs graph
+    in
+    let g' = Option.map clearup_cyclic_delay g' in
+    let g' = QSet.fold (fun v g -> Option.bind g (fun g -> update_dominance g q v)) delayed_qs g' in
+    match g' with
+    | Some graph -> Some { graph with delayed_check = QMap.set qv QSet.empty g.delayed_check }
+    | None -> None
 
 let update_dominance_if_valid g (q1,k,q2) =
   match k with
@@ -229,9 +249,8 @@ let enforce_constraint (q1, k, q2) g =
      let e = lazy (G.get_explanation (q1,to_graph_cstr k,q2) g.graph) in
      raise @@ EliminationError (QualityInconsistency (None, (k, q1, q2, Some (Path e))))
   | Some graph ->
-    let g = { g with graph } in
-    if Quality.equal q1 q2 then g
-    else dominance_check g (q1, k, q2)
+    if Quality.equal q1 q2 then graph
+    else dominance_check graph (q1, k, q2)
 
 let merge_constraints csts g = ElimConstraints.fold enforce_constraint csts g
 
@@ -296,10 +315,10 @@ let merge g g' =
              (fun q acc -> try add_quality q acc with _ -> acc) qs g in
   Quality.Set.fold
     (fun q -> Quality.Set.fold
-             (fun q' acc -> if Quality.equal q q' then acc
-                         else if eliminates_to g' q q'
-                         then enforce_eliminates_to q q' acc
-                         else acc) qs) qs g
+      (fun q' acc -> if Quality.equal q q' then acc
+        else if eliminates_to g' q q'
+        then enforce_eliminates_to q q' acc
+        else acc) qs) qs g
 
 let is_empty g = QVar.Set.is_empty (qvar_domain g)