Add delta to Types.Positive.clean_type

types/types.ml

@@ -2557,7 +2557,7 @@ struct
     in
     aux v subst
 
-  let print ppf v =
+  let pp ppf v =
     let id = ref 0 in
     let memo = MemoHash.create 17 in
     let rec aux ppf v =
@@ -2582,6 +2582,8 @@ struct
     in
     aux v
 
+  let printf = pp Format.std_formatter
+
   (* returns a recursive type where all occurrences of alpha n t
    * are substituted with a recursive variable X *)
   let substituterec t alpha =
@@ -2633,7 +2635,7 @@ struct
     let acc = acc ^ (String.make 1 (OldChar.chr (OldChar.code 'a' + nm))) in
     if ni == 0 then acc else pretty_name ni acc
 
-  let collect_variables v =
+  let collect_variables delta v =
     (* we memoize based on the pair (pos, v), since v can occur both
      * positively and negatively.  and we want to manage the variables
      * differently in both cases *)
@@ -2653,6 +2655,7 @@ struct
         let () = Memo.add memo (pos,v) () in
         match v.def with
         |`Type d -> ()
+        |`Variable d when Var.Set.mem d delta -> ()
         |`Variable d ->
           begin try
             let td = Hashtbl.find vars d in
@@ -2676,11 +2679,11 @@ struct
     aux true v;
     vars
 
-  let clean_variables t =
+  let clean_variables delta t =
     if no_var t then t
     else begin
       let dec = decompose t in
-      let h = collect_variables dec in
+      let h = collect_variables delta dec in
       let new_t =
         substitute_aux dec (fun d ->
           try Hashtbl.find h d
@@ -2690,9 +2693,9 @@ struct
       descr (solve new_t)
     end
 
-  let clean_type t =
+  let clean_type delta t =
     if no_var t then t else
-      let t = clean_variables t in
+      let t = clean_variables delta t in
       let arrow_t, non_arrow_t =
         { empty with arrow = t.arrow },
         { t with arrow = empty.arrow }
@@ -2901,7 +2904,6 @@ module Tallying = struct
             )
               s2 acc1) s1 []
 
-
     end
 
     type s = S.t
@@ -3328,7 +3330,7 @@ let squaresubtype delta s t =
       let s = get ai i in
       let sl = Tallying.tallying ~delta [ (s,t) ] in
       let ss =
-        Positive.clean_type (
+        Positive.clean_type delta (
           List.fold_left (fun acc si ->
               cap acc (Tallying.(s $$ si))
           ) any sl
@@ -3375,7 +3377,7 @@ let apply_raw delta s t =
       let t = arrow (cons (get aj j)) cgamma in
       let sl = Tallying.tallying ~delta [ (s,t) ] in
       let new_res =
-        Positive.clean_type (
+        Positive.clean_type delta (
           List.fold_left (fun tacc si ->
             cap tacc (Tallying.(gamma $$ si))
           ) any sl

typing/typer.ml

@@ -1185,7 +1185,6 @@ and branches_aux loc env targ tres constr precise = function
         b.br_vars_poly <- xj;
 
 	  let t = type_check env' b.br_body constr precise in (* s_i^j *)
-        Format.printf "patt %a // %a" Patterns.Print.pp (Patterns.descr p) Types.Print.pp_type t;
 	  let tres = if precise then Types.cup t tres else tres in
 	  let targ'' = Types.diff targ acc in
 	  if (Types.non_empty targ'') then