do not use univars in fixed instances

git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10685 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

typing/btype.ml

@@ -529,6 +529,5 @@ let backtrack (changes, old) =
 (**** Sets, maps and hashtables of types ****)
 
 module TypeSet = Set.Make(TypeOps)
-module TypeSetPair = Set.Make(struct type t = TypeOps.t * TypeOps.t let compare (x1,x2) (y1,y2) = let r = TypeOps.compare x1 y1 in if r == 0 then TypeOps.compare x2 y2 else r end)
 module TypeMap = Map.Make (TypeOps)
 module TypeHash = Hashtbl.Make(TypeOps)

typing/btype.mli

@@ -153,12 +153,10 @@ val set_commu: commutable ref -> commutable -> unit
         (* Set references, logging the old value *)
 val log_type: type_expr -> unit
         (* Log the old value of a type, before modifying it by hand *)
-
     
 
 (**** Sets, maps and hashtables of types ****)
 
 module TypeSet  : Set.S with type elt = type_expr
-module TypeSetPair  : Set.S with type elt = type_expr * type_expr
 module TypeMap  : Map.S with type key = type_expr
 module TypeHash : Hashtbl.S with type key = type_expr

typing/ctype.ml

@@ -990,7 +990,7 @@ let rec copy_sep fixed free bound visited ty =
           (* We shall really check the level on the row variable *)
           let keep = more.desc = Tvar && more.level <> generic_level in
           let more' = copy_rec more in
-          let fixed' = fixed && (repr more').desc = Tunivar in
+          let fixed' = fixed && (repr more').desc = Tvar in
           let row = copy_row copy_rec fixed' row keep more' in
           Tvariant row
       | Tpoly (t1, tl) ->
@@ -1006,8 +1006,7 @@ let rec copy_sep fixed free bound visited ty =
   end
 
 let instance_poly fixed univars sch =
-  let mkvar = if fixed then (fun () -> newty Tunivar) else newvar in
-  let vars = List.map (fun _ -> mkvar ()) univars in
+  let vars = List.map (fun _ -> newvar ()) univars in
   let pairs = List.map2 (fun u v -> repr u, (v, [])) univars vars in
   delayed_copy := [];
   let ty = copy_sep fixed (compute_univars sch) [] pairs sch in
@@ -1369,14 +1368,6 @@ let rec unify_univar t1 t2 = function
       end
   | [] -> raise (Unify [])
 
-(* Free univars. One can unify them with variables. *)
-let free_univars = ref TypeSet.empty
-let add_free_univars tl =
-  let old = !free_univars in
-  free_univars := List.fold_right TypeSet.add tl old;
-  old
-
-let set_free_univars tl = free_univars := tl
 
 (* Test the occurence of free univars in a type *)
 (* that's way too expansive. Must do some kind of cacheing *)
@@ -1399,8 +1390,7 @@ let occur_univar env ty =
     then
       match ty.desc with
         Tunivar ->
-          if not (TypeSet.mem ty bound) && not (TypeSet.mem ty !free_univars)
-          then raise (Unify [ty, newgenvar()])
+          if not (TypeSet.mem ty bound) then raise (Unify [ty, newgenvar()])
       | Tpoly (ty, tyl) ->
           let bound = List.fold_right TypeSet.add (List.map repr tyl) bound in
           occur_rec bound  ty

typing/ctype.mli

@@ -29,11 +29,10 @@ val init_def: int -> unit
         (* Set the initial variable level *)
 val begin_def: unit -> unit
         (* Raise the variable level by one at the beginning of a definition. *)
-val begin_class_def: unit -> unit
-        (* Same as begin_def, but do not raise nongen_level *)
-val raise_nongen_level: unit -> unit
 val end_def: unit -> unit
-        (* Return to the previous variable levels *)
+        (* Lower the variable level by one at the end of a definition *)
+val begin_class_def: unit -> unit
+val raise_nongen_level: unit -> unit
 val reset_global_level: unit -> unit
         (* Reset the global level before typing an expression *)
 val increase_global_level: unit -> int
@@ -140,12 +139,6 @@ val full_expand: Env.t -> type_expr -> type_expr
 
 val enforce_constraints: Env.t -> type_expr -> unit
 
-val add_free_univars: type_expr list -> Btype.TypeSet.t
-        (* add some free univars (allows unifying them with variables),
-           returning the original set *)
-val set_free_univars: Btype.TypeSet.t -> unit
-        (* return to a previous set of free univars *)
-
 val unify: Env.t -> type_expr -> type_expr -> unit
         (* Unify the two types given. Raise [Unify] if not possible. *)
 val unify_gadt: Env.t ref -> type_expr -> type_expr -> unit

typing/printtyp.ml

@@ -919,11 +919,8 @@ let print_tags ppf fields =
 
 let has_explanation unif t3 t4 =
   match t3.desc, t4.desc with
-    Tunivar, Tunivar ->
-      let free_univars = add_free_univars [] in
-      TypeSet.mem t3 free_univars || TypeSet.mem t4 free_univars
-  | Tfield _, _ | _, Tfield _
-  | Tunivar, _ | _, Tunivar
+    Tfield _, _ | _, Tfield _
+  | Tunivar, Tvar | Tvar, Tunivar
   | Tvariant _, Tvariant _ -> true
   | Tconstr (p, _, _), Tvar | Tvar, Tconstr (p, _, _) ->
       unif && min t3.level t4.level < Path.binding_time p
@@ -953,15 +950,9 @@ let explanation unif t3 t4 ppf =
       fprintf ppf
         "@,@[The type constructor@;<1 2>%a@ would escape its scope@]"
         path p
-  | Tunivar, Tunivar ->
-      fprintf ppf "@,Universal variables %a and %a are incompatible"
-        type_expr t3 type_expr t4
   | Tvar, Tunivar | Tunivar, Tvar ->
       fprintf ppf "@,The universal variable %a would escape its scope"
         type_expr (if t3.desc = Tunivar then t3 else t4)
-  | _, Tunivar | Tunivar, _ ->
-      fprintf ppf "@,The universal variable %a cannot be instantiated"
-        type_expr (if t3.desc = Tunivar then t3 else t4)
   | Tfield (lab, _, _, _), _
   | _, Tfield (lab, _, _, _) when lab = dummy_method ->
       fprintf ppf

typing/typecore.ml

@@ -496,7 +496,7 @@ let rec type_pat (env:Env.t ref) sp expected_ty  =
       let constr = Typetexp.find_constructor !env loc lid in
       let _ = (* GAH : there must be an easier way to do this, ask garrigue *)
 	let (_, ty_res) = instance_constructor constr in
-	match ty_res.desc with
+	match (repr ty_res).desc with
 	| Tconstr(p,args,m) ->
 	    ty_res.desc <- Tconstr(p,List.map (fun _ -> newvar ()) args,m);
 	    unify_pat_types loc !env expected_ty ty_res
@@ -707,9 +707,7 @@ let type_self_pattern cl_num privty val_env met_env par_env spat  =
   (pat, meths, vars, val_env, met_env, par_env)
 
 let delayed_checks = ref []
-let reset_delayed_checks () =
-  delayed_checks := [];
-  set_free_univars TypeSet.empty (* Hook this here. Better name? *)
+let reset_delayed_checks () = delayed_checks := []
 let add_delayed_check f  =  delayed_checks := f :: !delayed_checks
 let force_delayed_checks () =
   (* checks may change type levels *)
@@ -1038,7 +1036,9 @@ let check_univars env expans kind exp ty_expected vars  =
       (fun t ->
         let t = repr t in
         generalize t;
-        t.level = generic_level)
+        if t.desc = Tvar && t.level = generic_level then
+          (log_type t; t.desc <- Tunivar; true)
+        else false)
       vars in
   if List.length vars = List.length vars' then () else
   let ty = newgenty (Tpoly(repr exp.exp_type, vars'))
@@ -1731,12 +1731,10 @@ and type_label_exp create env loc ty (lid, sarg)  =
     raise(Error(loc, if create then Private_type ty else Private_label (lid, ty)));
   let arg =
     let snap = if vars = [] then None else Some (Btype.snapshot ()) in
-    let old = add_free_univars vars in
     let arg = type_argument env sarg ty_arg in
     end_def ();
     try
       check_univars env (vars <> []) "field value" arg label.lbl_arg vars;
-      set_free_univars old;
       arg
     with exn when not (is_nonexpansive arg) -> try
       (* Try to retype without propagating ty_arg, cf PR#4862 *)
@@ -1747,7 +1745,6 @@ and type_label_exp create env loc ty (lid, sarg)  =
       generalize_expansive env arg.exp_type;
       unify_exp env arg ty_arg;
       check_univars env false "field value" arg label.lbl_arg vars;
-      set_free_univars old;
       arg
     with Error (_, Less_general _) as e -> raise e
     | _ -> raise exn    (* In case of failure return the first error *)
@@ -2178,11 +2175,9 @@ and type_expect ?in_function env sexp ty_expected =
             (* One more level to generalize locally *)
             begin_def ();
             let vars, ty'' = instance_poly true tl ty' in
-            let old = add_free_univars vars in
             let exp = type_expect env sbody ty'' in
             end_def ();
             check_univars env false "method" exp ty_expected vars;
-            set_free_univars old;
             re { exp with exp_type = ty }
         | _ -> assert false
       end
@@ -2341,11 +2336,9 @@ and type_let env rec_flag spat_sexp_list scope   =
         | Tpoly (ty, tl) ->
             begin_def ();
             let vars, ty' = instance_poly true tl ty in
-            let old = add_free_univars vars in
             let exp = type_expect exp_env sexp ty' in
             end_def ();
             check_univars env true "definition" exp pat.pat_type vars;
-            set_free_univars old;
             {exp with exp_type = instance exp.exp_type}
         | _ -> type_expect exp_env sexp pat.pat_type)
       spat_sexp_list pat_list in