propagate type information to patterns, even when there are polymorphic variants

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

2 files changed, 81 insertions, 14 deletions

diff --git a/typing/ctype.ml b/typing/ctype.ml
index 4a43582e7f..7dbbb94c7f 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -981,6 +981,25 @@ let rec copy ?env ?partial ?keep_names ty =
                     if keep then more else newty more.desc
                 |  _ -> assert false
               in
+              (* Open row if partial for pattern and contains Reither *)
+              let more', row =
+                match partial with
+                  Some (free_univars, false) when row.row_closed
+                  && not row.row_fixed && TypeSet.is_empty (free_univars ty) ->
+                    let not_reither (_, f) =
+                      match row_field_repr f with
+                        Reither _ -> false
+                      | _ -> true
+                    in
+                    if List.for_all not_reither row.row_fields
+                    then (more', row) else
+                    (newty2 (if keep then more.level else !current_level)
+                       (Tvar None),
+                     {row_fields = List.filter not_reither row.row_fields;
+                      row_more = more; row_bound = ();
+                      row_closed = false; row_fixed = false; row_name = None})
+                | _ -> (more', row)
+              in
               (* Register new type first for recursion *)
               more.desc <- Tsubst(newgenty(Ttuple[more';t]));
               (* Return a new copy *)
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 34b7b9784a..69089e38c2 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -326,7 +326,7 @@ let finalize_variant pat =
         | _ -> assert false
       in
       begin match row_field tag row with
-      | Rabsent -> assert false
+      | Rabsent -> () (* assert false *)
       | Reither (true, [], _, e) when not row.row_closed ->
           set_row_field e (Rpresent None)
       | Reither (false, ty::tl, _, e) when not row.row_closed ->
@@ -1658,6 +1658,28 @@ let create_package_type loc env (p, l) =
     sexp unpacks
 
 (* Helpers for type_cases *)
+
+let contains_variant_either ty =
+  let rec loop ty = 
+    let ty = repr ty in
+    if ty.level >= lowest_level then begin
+      mark_type_node ty;
+      match ty.desc with
+        Tvariant row ->
+          let row = row_repr row in
+          if not row.row_fixed then
+            List.iter
+              (fun (_,f) ->
+                match row_field_repr f with Reither _ -> raise Exit | _ -> ())
+              row.row_fields;
+          iter_row loop row
+      | _ ->
+          iter_type_expr loop ty
+    end
+  in
+  try loop ty; unmark_type ty; false
+  with Exit -> unmark_type ty; true
+
 let iter_ppat f p =
   match p.ppat_desc with
   | Ppat_any | Ppat_var _ | Ppat_constant _
@@ -1691,6 +1713,24 @@ let contains_gadt env p =
   in
   try loop p; false with Exit -> true
 
+let check_absent_variant env =
+  iter_pattern
+    (function {pat_desc = Tpat_variant (s, arg, row)} as pat ->
+      let row = row_repr !row in
+      if List.exists (fun (s',fi) -> s = s' && row_field_repr fi <> Rabsent)
+          row.row_fields
+      then () else
+      let ty_arg =
+        match arg with None -> [] | Some p -> [correct_levels p.pat_type] in
+      let row' = {row_fields = [s, Reither(arg=None,ty_arg,true,ref None)];
+                  row_more = newvar (); row_bound = ();
+                  row_closed = false; row_fixed = false; row_name = None} in
+      (* Should fail *)
+      unify_pat env {pat with pat_type = newty (Tvariant row')}
+                    (correct_levels pat.pat_type)
+      | _ -> ())
+      
+
 let dummy_expr = {pexp_desc = Pexp_tuple []; pexp_loc = Location.none}
 
 (* Duplicate types of values in the environment *)
@@ -3040,16 +3080,20 @@ and type_statement env sexp =
 
 and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
   (* ty_arg is _fully_ generalized *)
-  let dont_propagate, has_gadts =
-    let patterns = List.map fst caselist in
-    List.exists contains_polymorphic_variant patterns,
-    List.exists (contains_gadt env) patterns in
+  let patterns = List.map fst caselist in
+  let erase_either =
+    List.exists contains_polymorphic_variant patterns
+    && contains_variant_either ty_arg
+  and has_gadts = List.exists (contains_gadt env) patterns in
 (*  prerr_endline ( if has_gadts then "contains gadt" else "no gadt"); *)
-  let ty_arg, ty_res, env =
+  let ty_arg =
+    if (has_gadts || erase_either) && not !Clflags.principal
+    then correct_levels ty_arg else ty_arg
+  and ty_res, env =
     if has_gadts && not !Clflags.principal then
-      correct_levels ty_arg, correct_levels ty_res,
-      duplicate_ident_types loc caselist env
-    else ty_arg, ty_res, env in
+      correct_levels ty_res, duplicate_ident_types loc caselist env
+    else ty_res, env
+  in
   let lev, env =
     if has_gadts then begin
       (* raise level for existentials *)
@@ -3075,10 +3119,10 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
         let scope = Some (Annot.Idef loc) in
         let (pat, ext_env, force, unpacks) =
           let partial =
-            if !Clflags.principal then Some false else None in
-          let ty_arg =
-            if dont_propagate then newvar () else instance ?partial env ty_arg
-          in type_pattern ~lev env spat scope ty_arg
+            if !Clflags.principal || erase_either
+            then Some false else None in
+          let ty_arg = instance ?partial env ty_arg in
+          type_pattern ~lev env spat scope ty_arg
         in
         pattern_force := force @ !pattern_force;
         let pat =
@@ -3137,7 +3181,11 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
     else
       Partial
   in
-  add_delayed_check (fun () -> Parmatch.check_unused env cases);
+  add_delayed_check
+    (fun () ->
+      List.iter (fun (pat, (env, _)) -> check_absent_variant env pat)
+        pat_env_list;
+      Parmatch.check_unused env cases);
   if has_gadts then begin
     end_def ();
     (* Ensure that existential types do not escape *)