Refresh the type of variables in the environement to avoid clash with...

Refresh the type of variables in the environement to avoid clash with variables of the interface of the function being typed.

tests/stdlib/list/listtest.cd

+exit 0;;
+
 include "list.cd"
 
 let nb_success = ref Int (0)
@@ -5,9 +7,10 @@ let nb_tests = ref Int (0)
 
 (* Note: We are using List.iter here *)
 (* TODO: Bugfix: it works here if you replace 'a with 'b *)
-(* let run_test_suite (l : [(Latin1, 'a, 'a)*]) : [] =
-    iter (fun ((Latin1, 'a, 'a) -> []) (_, x, y) -> nb_tests := !nb_tests + 1;
-    if x = y then nb_success := !nb_success + 1 else []) l *)
+ let run_test_suite (l : [(Latin1, 'a, 'a)*]) : [] =
+   iter (fun ((Latin1, 'a, 'a) -> []) (_, x, y) -> nb_tests := !nb_tests + 1;
+     if x = y then nb_success := !nb_success + 1 else []) l
+ ;;
 
 let run_test_suite (l : [(Latin1, 'a, 'a)*]) : [] = match l with
   | [] -> []
@@ -84,3 +87,5 @@ run_test_suite append_tests;
 run_test_suite rev_append_tests;
 run_test_suite concat_tests;
 print (string_of !nb_success); print " / "; print (string_of !nb_tests)
+
+Tuareg finished at Fri Jul 11 14:24:59

typing/typer.ml

@@ -874,7 +874,20 @@ and type_check' loc env ed constr precise = match ed with
       (ed,verify loc (Types.cap te (Types.descr t)) constr)
 
   | Abstraction a ->
-      let t =
+    let env = {
+          (* freshen type variables from the environment to avoid capture with
+             variables defined in the interface of a *)
+      env with
+        ids = Env.map
+        (fun v ->
+          let open Types in
+          match v with
+            | Val t -> Val (Positive.substitutefree env.delta t)
+            | EVal (a,b,t) ->  EVal (a,b,Positive.substitutefree env.delta t)
+            | x -> x)
+        env.ids }
+    in
+    let t =
         (* try Types.Arrow.check_strenghten a.fun_typ constr *)
         try begin
           if Types.is_squaresubtype env.delta a.fun_typ constr then a.fun_typ
@@ -1168,15 +1181,15 @@ and branches_aux loc env targ tres constr precise = function
         let env = { env with
           gamma = IdMap.merge (fun _ v2 -> v2) env.gamma res }
         in
-	  let res = IdMap.map Types.descr res in
+	let res = IdMap.map Types.descr res in
 
-	  b.br_vars_empty <-
-	    IdMap.domain (
-	      IdMap.filter (fun _ t -> Types.subtype t Sequence.nil_type)
-		(IdMap.restrict res b.br_vars_empty)
+	b.br_vars_empty <-
+	  IdMap.domain (
+	    IdMap.filter (fun _ t -> Types.subtype t Sequence.nil_type)
+	      (IdMap.restrict res b.br_vars_empty)
           );
 
-	  let env' = enter_values (IdMap.get res) env in
+	let env' = enter_values (IdMap.get res) env in
 
         (* Xi_j : a map from term variables in the pattern to type variables *)
         let xj =