Keep track of registered global name when applying substitutions.

types/types.ml

@@ -2882,6 +2882,9 @@ struct
       end
     )
 
+  let print ppf m =
+    Utils.pp_list (fun ppf (v, t) -> Format.fprintf ppf "%a:%a"
+                      Var.pp v Print.pp_type t) ppf (Map.get m)
 
   let add v t m =
     if is_var t && Var.(equal v (Set.choose (all_vars t))) then m
@@ -2911,7 +2914,10 @@ struct
       MemoSubst.find subst_cache (t, subst)
     with
     Not_found ->
+
       let res =
+        if List.for_all (fun (v, t) -> equiv t (var v)) (Map.get subst) then t
+        else
         let v = decompose t in
         descr (
           Positive.solve_gen ~stop_descr:(fun v ->
@@ -2937,13 +2943,27 @@ struct
           if not (DescrMap.mem nt !Print.named) then begin
             try
               let (cu, name, args) = DescrMap.find t !Print.named in
-              Print.register_global (cu, name, lsubst) nt;
+              if equiv t nt then
+                Print.register_global (cu, name, args) nt
+              else
+                let dom_args = Var.Set.from_list (List.map fst args) in
+                let dom,not_dom = List.fold_left
+                    (fun (acct, accf) (v,t) ->
+                       if Var.Set.mem dom_args v then v :: acct, accf
+                       else acct, t::accf) ([],[]) lsubst
+                in
+                if (Var.Set.equal (Var.Set.from_list dom) dom_args)
+                && (List.for_all no_var not_dom)
+                then
+                  let nargs = List.map (fun (v, _) -> v,Map.assoc v subst) args in
+                  Print.register_global (cu, name, nargs) nt
             with Not_found -> ()
           end;
           let key = (t, subst) in
           if not (MemoSubst.mem subst_cache key) then
             MemoSubst.add subst_cache key nt) !todo;
-      MemoSubst.add subst_cache (t,subst) res; res
+      let res = if equiv t res then t else res in
+      MemoSubst.add subst_cache (t,subst) res;res
 
 
   let full t l =

types/var.ml

@@ -4,9 +4,10 @@ module V = struct
   let function_kind = 1
   let argument_kind = 2
 
-  let dump ppf t = Format.fprintf ppf "{%a(%d)}" Ident.U.print t.id t.fr
+  let dump ppf t = Format.fprintf ppf "{%a(%d_%d)}" Ident.U.print t.id t.fr t.kind
   let compare x y = Pervasives.compare (x.kind,x.id,x.fr) (y.kind,y.id,y.fr)
-  let equal x y = (compare x y) = 0
+  let equal x y =
+    x == y || (x.kind == y.kind && x.fr == y.fr && Ident.U.equal x.id y.id)
   let hash x = Hashtbl.hash (x.id,x.fr,x.kind)
   let check _ = ()