Do not generate equations for monomorphic variables, during the generation of...

Do not generate equations for monomorphic variables, during the generation of type equation from constraints.

types/types.ml

@@ -3398,7 +3398,7 @@ module Tallying = struct
 
   (* Add constraints of the form { alpha = ( s v fresh ) ^ t } *)
 
-  let solve s =
+  let solve delta s =
 
     let aux alpha (s,t) acc =
         (* we cannot solve twice the same variable *)
@@ -3417,9 +3417,11 @@ module Tallying = struct
                * means that the constraint is of the form (alpha,beta). *)
           if is_var t then begin
             let (beta,_) = extract_variable t in
-            let acc1 = aux beta (empty,any) acc in
-                (* alpha <= beta --> { empty <= alpha <= beta ; empty <= beta <= any } *)
-            aux alpha (s,t) acc1
+            if Var.Set.mem beta delta then aux alpha (s, t) acc
+            else
+              let acc1 = aux beta (empty,any) acc in
+            (* alpha <= beta --> { empty <= alpha <= beta ; empty <= beta <= any } *)
+              aux alpha (s,t) acc1
           end else
             (* alpha = ( s v fresh) ^ t *)
             aux alpha (s,t) acc;
@@ -3471,21 +3473,13 @@ module Tallying = struct
     if Pervasives.(n = CS.unsat) then raise Step1Fail else
     let m =
       CS.S.fold (fun c acc ->
-        try CS.ES.union (solve (merge delta c)) acc
+        try CS.ES.union (solve delta (merge delta c)) acc
         with UnSatConstr _ -> acc
       ) n CS.ES.empty
     in
     if CS.ES.is_empty m then raise Step2Fail else
     let el =
-      let dom e = CS.E.fold (fun v _ acc -> Var.Set.add v acc) e Var.Set.empty in
-      CS.ES.fold (fun e acc ->
-        let si = unify e in
-        (* XXX maybe we can eliminate solution earlier. Is it safe to do it here ? *)
-        (* it is a solution only if (dom(si) /\ delta = emptyset) *)
-        if Var.Set.is_empty (Var.Set.inter (dom(si)) delta) then
-          CS.ES.add si acc
-        else acc
-      ) m CS.ES.empty
+      CS.ES.fold (fun e acc -> CS.ES.add (unify e) acc ) m CS.ES.empty
     in
     (CS.ES.elements el)
 

types/types.mli

@@ -427,7 +427,7 @@ module Tallying : sig
 
   val norm : Var.Set.t -> t -> CS.s
   val merge : Var.Set.t -> CS.m -> CS.s
-  val solve : CS.s -> CS.es
+  val solve : Var.Set.t -> CS.s -> CS.es
   val unify : CS.sigma -> CS.sigma
 
   (* [s1 ... sn] . si is a solution for tallying problem