Fixed a bugs relating to polymorphic functions :

- Part of the typechecking code was using the monomorphics subtyping function instead of the tallying (when checking the body of a function)
- The function Var.gen that was generating new versions of typed variable names was not properly incrementing its internal counter, thus generating the same name for two distinct variables.

types/type_tallying.ml

@@ -706,12 +706,17 @@ let apply_raw delta s t =
       let t = arrow (cons (get aj j)) cgamma in
       let sl = tallying delta [ (s,t) ] in
       let new_res =
-        Subst.clean_type delta (
+      
           List.fold_left (fun tacc si ->
             cap tacc (Subst.full gamma  si)
           ) any sl
-        )
+        
       in
+      DEBUG apply_raw (Format.eprintf " apply_raw: found raw type @[%a@]@\n"
+				      Print.pp_type new_res);
+      let new_res = Subst.clean_type delta new_res in
+      DEBUG apply_raw (Format.eprintf " apply_raw: found cleaned type @[%a@]@\n"
+				      Print.pp_type new_res);
       raise (FoundApply(new_res,i,j,sl))
     with
       Step1Fail -> (assert (i == 0 &&  j == 0); raise (UnSatConstr "apply_raw step1"))

types/types.ml

@@ -3265,11 +3265,22 @@ struct
       );
       let vars = Var.Set.diff all delta in
       if Var.Set.is_empty vars then t else
+	let i_vars, s_vars =
+	  Var.Set.fold (fun (ia, sa) v -> if Var.is_internal v then
+					 (Var.Set.add v ia, sa)
+				       else (ia, Var.Set.add v sa) ) Var.Set.(empty,empty) vars
+	in
+	let fixed = Var.Set.cup s_vars delta in
         let subst = Map.init
                       (fun v ->
 			let is_pos = Var.Set.mem pos v in
 			let is_neg = Var.Set.mem neg v in
-			if is_pos && is_neg then var (Var.gen delta)
+			if is_pos && is_neg then begin
+			    if Var.is_internal v then
+			      var (Var.gen fixed)
+			    else
+			      var (Var.refresh v)
+			  end
 			else if is_pos then empty else any
 		      ) vars
         in

types/var.ml

@@ -46,7 +46,9 @@ module V = struct
   let is_internal x = x.kind == Internal
 
   let ident x = Ident.U.get_str x.name
-  let print ppf x = Format.fprintf ppf "'%a" Ident.U.print x.name
+  let print ppf x =
+    Format.fprintf ppf "'%a" Ident.U.print x.name;
+    DEBUG var_ident (Format.fprintf ppf "_%i_%a" x.id print_kind x.kind)
 end
 
 
@@ -60,8 +62,9 @@ end
 module Map = Set.Map
 
 include V
-let gen set =
+let gen =
   let idx = ref 0 in
+  fun set ->
   let rec freshvar () =
     let rec pretty i acc =
       let ni,nm = i/26, i mod 26 in

types/var.mli

@@ -4,7 +4,7 @@ val print : Format.formatter -> t -> unit
 val mk : ?internal:bool -> string -> t
 val ident : t -> string
 val refresh : t -> t
-
+val is_internal : t -> bool
 
 module Set : sig
   include SortedList.S with type Elem.t = t

typing/typer.ml

@@ -1260,14 +1260,17 @@ and type_check' loc env ed constr precise = match ed with
 
     let env = {env with delta = delta_intf } in
 
-      (* I check the body with all possible t1 -> t2 types *)
+    (* I check the body with all possible t1 -> t2 types *)
     let sll =
       List.fold_left (fun tacc (t1,t2) ->
         let acc = a.fun_body.br_accept in
         if not (Types.subtype t1 acc) then
           raise_loc loc (NonExhaustive (Types.diff t1 acc));
-        let t = type_check_branches loc env t1 [] a.fun_body t2 true in
+        let t = type_check_branches loc env t1 [] a.fun_body Types.any true in
         try
+	  DEBUG typecheck_arrow (Format.eprintf "Typechecking function %s @[%a@] against expected type @[%a@] delta = @[%a@]@\n%!"
+						(match a.fun_name with None -> "(anonymous)"
+								      | Some s -> Ident.to_string s) Types.Print.pp_type t Types.Print.pp_type t2 Var.Set.print env.delta);
           (Type_tallying.squaresubtype env.delta t t2)::tacc (* H_j *)
         with
           Type_tallying.UnSatConstr _ ->
@@ -1674,12 +1677,15 @@ let type_expr env e =
   report_unused_branches ();
   (e,t)
 
+let refresh l =
+  List.map (fun (x, t) -> x,Types.Subst.freshen Var.Set.empty t) l
+
 let type_let_decl env p e =
   clear_unused_branches ();
   let decl = let_decl env p e in
   let typs = type_let_decl env decl in
   report_unused_branches ();
-  let env = enter_values typs env in
+  let env = enter_values (refresh typs) env in
   (env,decl,typs)
 
 let type_let_funs env funs =
@@ -1696,7 +1702,7 @@ let type_let_funs env funs =
   let funs = List.map (expr env') funs in
   let typs = type_rec_funs env funs in
   report_unused_branches ();
-  let env = enter_values typs env in
+  let env = enter_values (refresh typs) env in
   (env,funs,typs)
 
 (*