ajout de -principal

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

12 files changed, 161 insertions, 31 deletions

diff --git a/driver/main.ml b/driver/main.ml
index d91d48aa48..47192c69eb 100644
--- a/driver/main.ml
+++ b/driver/main.ml
@@ -94,6 +94,7 @@ module Options = Main_args.Make_options (struct
   let _output_obj () = output_c_object := true; custom_runtime := true
   let _pack = set make_package
   let _pp s = preprocessor := Some s
+  let _principal = set principal
   let _rectypes = set recursive_types
   let _thread = set thread_safe
   let _unsafe = set fast
diff --git a/driver/main_args.ml b/driver/main_args.ml
index 33391e3d05..aeb9483185 100644
--- a/driver/main_args.ml
+++ b/driver/main_args.ml
@@ -98,6 +98,8 @@ struct
            " Package the given .cmo files into one .cmo";
     "-pp", Arg.String F._pp,
            "<command>  Pipe sources through preprocessor <command>";
+    "-principal", Arg.Unit F._principal,
+           " Check principality of type inference";
     "-rectypes", Arg.Unit F._rectypes, " Allow arbitrary recursive types";
     "-thread", Arg.Unit F._thread, " Use thread-safe standard library";
     "-unsafe", Arg.Unit F._unsafe,
diff --git a/driver/optmain.ml b/driver/optmain.ml
index b73a42350c..0cdaa0946c 100644
--- a/driver/optmain.ml
+++ b/driver/optmain.ml
@@ -108,6 +108,8 @@ let main () =
               " Package the given .cmo files into one .cmo";
        "-pp", Arg.String(fun s -> preprocessor := Some s),
              "<command>  Pipe sources through preprocessor <command>";
+       "-principal", Arg.set principal,
+             " Check principality of type inference";
        "-rectypes", Arg.Set recursive_types,
              " Allow arbitrary recursive types";
        "-S", Arg.Set keep_asm_file, " Keep intermediate assembly file";
diff --git a/toplevel/topmain.ml b/toplevel/topmain.ml
index 4875f253cd..555fadde6f 100644
--- a/toplevel/topmain.ml
+++ b/toplevel/topmain.ml
@@ -43,6 +43,7 @@ let main () =
      "-labels", Arg.Clear classic, " Labels commute (default)";
      "-noassert", Arg.Set noassert, " Do not compile assertion checks";
      "-nolabels", Arg.Set classic, " Ignore labels and do not commute";
+     "-principal", Arg.Set principal, " Check principality of type inference";
      "-rectypes", Arg.Set recursive_types, " Allow arbitrary recursive types";
      "-unsafe", Arg.Set fast, " No bound checking on array and string access";
      "-w", Arg.String (Warnings.parse_options false),
diff --git a/typing/btype.ml b/typing/btype.ml
index d0fea6c20a..83d767d031 100644
--- a/typing/btype.ml
+++ b/typing/btype.ml
@@ -143,6 +143,11 @@ let iter_type_expr f ty =
   | Tunivar             -> ()
   | Tpoly (ty, tyl)     -> f ty; List.iter f tyl
 
+let rec iter_abbrev f = function
+    Mnil                   -> ()
+  | Mcons(_, ty, ty', rem) -> f ty; f ty'; iter_abbrev f rem
+  | Mlink rem              -> iter_abbrev f !rem
+
 let copy_row f fixed row keep more =
   let fields = List.map
       (fun (l, fi) -> l,
diff --git a/typing/btype.mli b/typing/btype.mli
index 13e06e7607..f0609d844e 100644
--- a/typing/btype.mli
+++ b/typing/btype.mli
@@ -60,6 +60,8 @@ val iter_type_expr: (type_expr -> unit) -> type_expr -> unit
         (* Iteration on types *)
 val iter_row: (type_expr -> unit) -> row_desc -> unit
         (* Iteration on types in a row *)
+val iter_abbrev: (type_expr -> unit) -> abbrev_memo -> unit
+        (* Iteration on types in an abbreviation list *)
 
 val copy_type_desc: (type_expr -> type_expr) -> type_desc -> type_desc
         (* Copy on types *)
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 96e1129a0f..8101eb33e2 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -496,21 +496,13 @@ let rec iter_generalize tyl ty =
     ty.level <- generic_level;
     begin match ty.desc with
       Tconstr (_, _, abbrev) ->
-        generalize_expans tyl !abbrev
+        iter_abbrev (iter_generalize tyl) !abbrev
     | _ -> ()
     end;
     iter_type_expr (iter_generalize tyl) ty
   end else
     tyl := ty :: !tyl
 
-and generalize_expans tyl =
-  function
-    Mnil                   -> ()
-  | Mcons(_, ty, ty', rem) -> iter_generalize tyl ty;
-                              iter_generalize tyl ty';
-                              generalize_expans tyl rem
-  | Mlink rem              -> generalize_expans tyl !rem
-
 let rec generalize ty =
   iter_generalize (ref []) ty
 
@@ -521,6 +513,38 @@ let iterative_generalization min_level tyl =
   List.fold_right (fun ty l -> if ty.level <= min_level then l else ty::l)
     !tyl' []
 
+(* Generalize the structure and lower the variables *)
+
+let rec generalize_structure var_level ty =
+  let ty = repr ty in
+  if ty.level <> generic_level then begin
+    if ty.desc = Tvar && ty.level > var_level then
+      ty.level <- var_level
+    else if ty.level > !current_level then begin
+      ty.level <- generic_level;
+      begin match ty.desc with
+	Tconstr (_, _, abbrev) ->
+          iter_abbrev (generalize_structure var_level) !abbrev
+      | _ -> ()
+      end;
+      iter_type_expr (generalize_structure var_level) ty
+    end
+  end
+
+let generalize_expansive ty = generalize_structure !nongen_level ty
+let generalize_structure ty = generalize_structure !current_level ty
+
+(* Generalize the spine of a function, if the level >= !current_level *)
+
+let rec generalize_spine ty =
+  let ty = repr ty in
+  if ty.level < !current_level || ty.level = generic_level then () else
+  match ty.desc with
+    Tarrow (_, _, ty', _) | Tpoly (ty', _) ->
+      ty.level <- generic_level;
+      generalize_spine ty'
+  | _ -> ()
+
 let try_expand_head' = (* Forward declaration *)
   ref (fun env ty -> raise Cannot_expand)
 
diff --git a/typing/ctype.mli b/typing/ctype.mli
index a1804ca12c..a50e64f66d 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -83,6 +83,13 @@ val generalize: type_expr -> unit
         (* Generalize in-place the given type *)
 val iterative_generalization: int -> type_expr list -> type_expr list
         (* Efficient repeated generalization of a type *)
+val generalize_expansive: type_expr -> unit
+        (* Generalize the structure of a type, making variables
+           non-generalizable *)
+val generalize_structure: type_expr -> unit
+        (* Same, but variables are only lowered to !current_level *)
+val generalize_spine: type_expr -> unit
+        (* Special function to generalize a method during inference *)
 val make_nongen: type_expr -> unit
         (* Make non-generalizable the given type *)
 val correct_levels: type_expr -> type_expr
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index 8f19c1cf21..d707bc6f21 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -412,10 +412,15 @@ let rec class_field cl_num self_type meths vars
   | Pcf_val (lab, mut, sexp, loc) ->
       if StringSet.mem lab inh_vals then
         Location.prerr_warning loc (Warnings.Hide_instance_variable lab);
+      if !Clflags.principal then Ctype.begin_def ();
       let exp =
         try type_exp val_env sexp with Ctype.Unify [(ty, _)] ->
           raise(Error(loc, Make_nongen_seltype ty))
       in
+      if !Clflags.principal then begin
+        Ctype.end_def ();
+        Ctype.generalize_structure exp.exp_type
+      end;
       let (id, val_env, met_env, par_env) =
         enter_val cl_num vars lab mut exp.exp_type val_env met_env par_env
       in
@@ -453,11 +458,12 @@ let rec class_field cl_num self_type meths vars
 	raise(Error(loc, Method_type_mismatch (lab, trace)))
       end;
       let meth_expr = make_method cl_num expr in
-      let meth_type = Ctype.newty (Tarrow("", self_type, ty, Cok)) in
       let vars_local = !vars in
 
       let field =
         lazy begin
+          let meth_type =
+            Ctype.newty (Tarrow("", self_type, Ctype.instance ty, Cok)) in
           Ctype.raise_nongen_level ();
           vars := vars_local;
           let texp = type_expect met_env meth_expr meth_type in
@@ -545,9 +551,15 @@ and class_structure cl_num val_env met_env (spat, str) =
       str
   in
   Ctype.unify val_env self_type (Ctype.newvar ());
+  let methods =
+    if !Clflags.principal then
+      fst (Ctype.flatten_fields (Ctype.object_fields self_type))
+    else [] in
+  List.iter (fun (_,_,ty) -> Ctype.generalize_spine ty) methods;
   let vars_final = !vars in
   let fields = List.map Lazy.force (List.rev fields) in
   vars := vars_final;
+  List.iter (fun (_,_,ty) -> Ctype.unify val_env ty (Ctype.newvar ())) methods;
 
   {cl_field = fields;
    cl_meths = Meths.map (function (id, ty) -> id) !meths},
@@ -619,10 +631,15 @@ and class_expr cl_num val_env met_env scl =
                   Pcl_let(Default, [spat, smatch], sbody)})}
       in
       class_expr cl_num val_env met_env sfun
-  | Pcl_fun (l, _, spat, scl') ->
+  | Pcl_fun (l, None, spat, scl') ->
+      if !Clflags.principal then Ctype.begin_def ();
       let (pat, pv, val_env, met_env) =
         Typecore.type_class_arg_pattern cl_num val_env met_env l spat
       in
+      if !Clflags.principal then begin
+        Ctype.end_def ();
+        iter_pattern (fun {pat_type=ty} -> Ctype.generalize_structure ty) pat
+      end;
       let pv =
         List.map
           (function (id, id', ty) ->
@@ -652,7 +669,7 @@ and class_expr cl_num val_env met_env scl =
           (Warnings.Other "This optional argument cannot be erased");
       {cl_desc = Tclass_fun (pat, pv, cl, partial);
        cl_loc = scl.pcl_loc;
-       cl_type = Tcty_fun (l, pat.pat_type, cl.cl_type)}
+       cl_type = Tcty_fun (l, Ctype.instance pat.pat_type, cl.cl_type)}
   | Pcl_apply (scl', sargs) ->
       let cl = class_expr cl_num val_env met_env scl' in
       let rec nonopt_labels ls ty_fun =
diff --git a/typing/typecore.ml b/typing/typecore.ml
index a5fc31aa01..e86c95306e 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -751,8 +751,14 @@ let rec type_exp env sexp =
   | Pexp_function _ ->     (* defined in type_expect *)
       type_expect env sexp (newvar())
   | Pexp_apply(sfunct, sargs) ->
+      if !Clflags.principal then begin_def ();
       let funct = type_exp env sfunct in
+      if !Clflags.principal then begin
+        end_def ();
+        generalize_structure funct.exp_type
+      end;
       let (args, ty_res) = type_application env funct sargs in
+      let funct = {funct with exp_type = instance funct.exp_type} in
       { exp_desc = Texp_apply(funct, args);
         exp_loc = sexp.pexp_loc;
         exp_type = ty_res;
@@ -948,8 +954,15 @@ let rec type_exp env sexp =
             let arg = type_exp env sarg in
             (arg, arg.exp_type)
         | (Some sty, None) ->
+            if !Clflags.principal then begin_def ();
             let ty = Typetexp.transl_simple_type env false sty in
-            (type_expect env sarg ty, ty)
+            if !Clflags.principal then begin
+              end_def ();
+              generalize_structure ty;
+              let ty1 = instance ty and ty2 = instance ty in
+              (type_expect env sarg ty1, ty2)
+            end else
+              (type_expect env sarg ty, ty)
         | (None, Some sty') ->
             let (ty', force) =
               Typetexp.transl_simple_type_delayed env sty'
@@ -995,6 +1008,7 @@ let rec type_exp env sexp =
         exp_type = body.exp_type;
         exp_env = env }
   | Pexp_send (e, met) ->
+      if !Clflags.principal then begin_def ();
       let obj = type_exp env e in
       begin try
         let (exp, typ) =
@@ -1022,7 +1036,7 @@ let rec type_exp env sexp =
                   let method_type = newvar () in
                   let (obj_ty, res_ty) = filter_arrow env method_type "" in
                   unify env obj_ty desc.val_type;
-                  unify env res_ty typ;
+                  unify env res_ty (instance typ);
                   (Texp_apply({exp_desc = Texp_ident(Path.Pident method_id,
                                                      {val_type = method_type;
                                                        val_kind = Val_reg});
@@ -1042,17 +1056,25 @@ let rec type_exp env sexp =
               (Texp_send(obj, Tmeth_name met),
                filter_method env met Public obj.exp_type)
         in
+        if !Clflags.principal then begin
+          end_def ();
+          generalize_structure typ;
+        end;
         let typ =
           match repr typ with
             {desc = Tpoly (ty, [])} ->
-              ty
-          | {desc = Tpoly (ty, tl)} ->
+              instance ty
+          | {desc = Tpoly (ty, tl); level = l} ->
+              if !Clflags.principal && l <> generic_level then
+                Location.prerr_warning sexp.pexp_loc
+                  (Warnings.Other
+                     "This use of a polymorphic method is not principal");
               snd (instance_poly false tl ty)
           | {desc = Tvar} as ty ->
               let ty' = newvar () in
-              unify env ty (newty(Tpoly(ty',[])));
+              unify env (instance ty) (newty(Tpoly(ty',[])));
               (* if not !Clflags.nolabels then
-                 Location.print_warning loc (Warnings.Unknown_method met); *)
+                 Location.prerr_warning loc (Warnings.Unknown_method met); *)
               ty'
           | _ ->
               assert false
@@ -1083,7 +1105,7 @@ let rec type_exp env sexp =
         let (path, desc) = Env.lookup_value (Longident.Lident lab) env in
         match desc.val_kind with
           Val_ivar (Mutable, cl_num) ->
-            let newval = type_expect env snewval desc.val_type in
+            let newval = type_expect env snewval (instance desc.val_type) in
             let (path_self, _) =
               Env.lookup_value (Longident.Lident ("self-" ^ cl_num)) env
             in
@@ -1121,7 +1143,7 @@ let rec type_exp env sexp =
           let type_override (lab, snewval) =
             begin try
               let (id, _, ty) = Vars.find lab !vars in
-              (Path.Pident id, type_expect env snewval ty)
+              (Path.Pident id, type_expect env snewval (instance ty))
             with
               Not_found ->
                 raise(Error(sexp.pexp_loc, Unbound_instance_variable lab))
@@ -1302,7 +1324,11 @@ and type_application env funct sargs =
   let rec type_args args omitted ty_fun ty_old sargs more_sargs =
     match expand_head env ty_fun with
       {desc=Tarrow (l, ty, ty_fun, com); level=lv} as ty_fun'
-      when (sargs <> [] || more_sargs <> []) && commu_repr com = Cok ->
+      when (sargs <> [] || more_sargs <> []) ->
+        let warn =
+          (commu_repr com = Cunknown) ||
+          (!Clflags.principal && lv <> generic_level) in
+        let ty = instance ty in
         let name = label_name l
         and optional = if is_optional l then Optional else Required in
         let sargs, more_sargs, arg =
@@ -1321,28 +1347,47 @@ and type_application env funct sargs =
           end else try
             let (l', sarg0, sargs, more_sargs) =
               try
-                let (l', sarg0, sargs1, sargs2) = extract_label name sargs
-                in (l', sarg0, sargs1 @ sargs2, more_sargs)
+                let (l', sarg0, sargs1, sargs2) = extract_label name sargs in
+                if warn && sargs1 <> [] then
+                  Location.prerr_warning sarg0.pexp_loc
+                  (Warnings.Other "Commuting this argument is not principal");
+                (l', sarg0, sargs1 @ sargs2, more_sargs)
               with Not_found ->
-                let (l', sarg0, sargs1, sargs2) = extract_label name more_sargs
-                in (l', sarg0, sargs @ sargs1, sargs2)
+                let (l', sarg0, sargs1, sargs2) =
+                  extract_label name more_sargs in
+                if warn && (sargs1 <> [] || sargs <> []) then
+                  Location.prerr_warning sarg0.pexp_loc
+                  (Warnings.Other "Commuting this argument is not principal");
+                (l', sarg0, sargs @ sargs1, sargs2)
             in
             sargs, more_sargs,
             if optional = Required || is_optional l' then
               Some (fun () -> type_argument env sarg0 ty)
-            else
+            else begin
+              if warn then Location.prerr_warning sarg0.pexp_loc
+                (Warnings.Other
+                   "Using an optional argument here is not principal");
               Some (fun () -> option_some (type_argument env sarg0 
                                              (extract_option_type env ty)))
+            end
           with Not_found ->
             sargs, more_sargs,
             if optional = Optional &&
               (List.mem_assoc "" sargs || List.mem_assoc "" more_sargs)
             then begin
+              if warn then Location.prerr_warning funct.exp_loc
+                  (Warnings.Other
+                     "Eliminated an optional argument without principality");
               ignored := (l,ty,lv) :: !ignored;
               Some (fun () -> option_none ty Location.none)
-            end else None
+            end else begin
+              if warn then Location.prerr_warning funct.exp_loc
+                  (Warnings.Other "Commuted an argument without principality");
+              None
+            end
         in
-        let omitted = if arg = None then (l,ty,lv) :: omitted else omitted in
+        let omitted =
+          if arg = None then (l,ty,min lv ty.level) :: omitted else omitted in
         let ty_old = if sargs = [] then ty_fun else ty_old in
         type_args ((arg,optional)::args) omitted ty_fun ty_old sargs more_sargs
     | _ ->
@@ -1350,13 +1395,14 @@ and type_application env funct sargs =
           (l, sarg0) :: _ when ignore_labels ->
             raise(Error(sarg0.pexp_loc, Apply_wrong_label(l, ty_old)));
         | _ ->
-            type_unknown_args args omitted ty_fun (sargs @ more_sargs)
+            type_unknown_args args omitted (instance ty_fun)
+              (sargs @ more_sargs)
   in
   match funct.exp_desc, sargs with
     (* Special case for ignore: avoid discarding warning *)
     Texp_ident (_, {val_kind=Val_prim{Primitive.prim_name="%ignore"}}),
     ["", sarg] ->
-      let ty_arg, ty_res = filter_arrow env funct.exp_type "" in
+      let ty_arg, ty_res = filter_arrow env (instance funct.exp_type) "" in
       let exp = type_expect env sarg ty_arg in
       begin match expand_head env exp.exp_type with
       | {desc = Tarrow _} ->
@@ -1541,7 +1587,15 @@ and type_cases ?in_function env ty_arg ty_res partial_loc caselist =
   let pat_env_list =
     List.map
       (fun (spat, sexp) ->
+        if !Clflags.principal then begin_def ();
         let (pat, ext_env) = type_pattern env spat in
+        let pat =
+          if !Clflags.principal then begin
+            end_def ();
+            iter_pattern (fun {pat_type=t} -> generalize_structure t) pat;
+            { pat with pat_type = instance pat.pat_type }
+          end else pat
+        in
         unify_pat env pat ty_arg';
         (pat, ext_env))
       caselist in
@@ -1580,6 +1634,7 @@ and type_cases ?in_function env ty_arg ty_res partial_loc caselist =
 
 and type_let env rec_flag spat_sexp_list =
   begin_def();
+  if !Clflags.principal then begin_def ();
   let (pat_list, new_env) =
     type_pattern_list env (List.map (fun (spat, sexp) -> spat) spat_sexp_list)
   in
@@ -1587,6 +1642,15 @@ and type_let env rec_flag spat_sexp_list =
     List.iter2
       (fun pat (_, sexp) -> unify_pat env pat (type_approx env sexp))
       pat_list spat_sexp_list;
+  let pat_list =
+    if !Clflags.principal then begin
+      end_def ();
+      List.map
+        (fun pat ->
+          iter_pattern (fun pat -> generalize_structure pat.pat_type) pat;
+          {pat with pat_type = instance pat.pat_type})
+        pat_list
+    end else pat_list in
   let exp_env =
     match rec_flag with Nonrecursive | Default -> env | Recursive -> new_env in
   let exp_list =
@@ -1600,7 +1664,9 @@ and type_let env rec_flag spat_sexp_list =
   List.iter2
     (fun pat exp ->
        if not (is_nonexpansive exp) then
-         iter_pattern (fun pat -> make_nongen pat.pat_type) pat)
+         let f =
+           if !Clflags.principal then generalize_expansive else make_nongen in
+         iter_pattern (fun pat -> f pat.pat_type) pat)
     pat_list exp_list;
   List.iter
     (fun pat -> iter_pattern (fun pat -> generalize pat.pat_type) pat)
@@ -1621,6 +1687,7 @@ let type_expression env sexp =
   let exp = type_exp env sexp in
   end_def();
   if is_nonexpansive exp then generalize exp.exp_type
+  else if !Clflags.principal then generalize_expansive exp.exp_type
   else make_nongen exp.exp_type;
   exp
 
diff --git a/typing/typecore.mli b/typing/typecore.mli
index 20e73edceb..78a8c77995 100644
--- a/typing/typecore.mli
+++ b/typing/typecore.mli
@@ -53,6 +53,7 @@ val type_argument:
 val option_some: Typedtree.expression -> Typedtree.expression
 val option_none: type_expr -> Location.t -> Typedtree.expression
 val extract_option_type: Env.t -> type_expr -> type_expr
+val iter_pattern: (Typedtree.pattern -> unit) -> Typedtree.pattern -> unit
 
 val self_coercion : (Path.t * Location.t list ref) list ref
 
diff --git a/utils/clflags.ml b/utils/clflags.ml
index ee2b545259..1bcbbec884 100644
--- a/utils/clflags.ml
+++ b/utils/clflags.ml
@@ -40,6 +40,7 @@ and verbose = ref false                 (* -verbose *)
 and use_prims = ref ""                  (* -use_prims ... *)
 and use_runtime = ref ""                (* -use_runtime ... *)
 and recursive_types = ref false         (* -rectypes *)
+and principal = ref false               (* -principal *)
 and make_runtime = ref false            (* -make_runtime *)
 and gprofile = ref false                (* -p *)
 and c_compiler = ref Config.bytecomp_c_compiler (* -cc *)