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

7 files changed, 136 insertions, 37 deletions

diff --git a/Changes b/Changes
index 399d327e16..d8dd33f158 100644
--- a/Changes
+++ b/Changes
@@ -1,11 +1,19 @@
 Next version
 ------------
 
+Type system:
+- Propagate type information towards pattern-matching, even in the presence of
+  polymorphic variants (discarding only information about possibly-present
+  constructors). As a result, matching against absent constructors is no longer
+  allowed. 
+
 Compilers:
-- PR#5861: raise an error when multiple private keywords are used in type declarations
+- PR#5861: raise an error when multiple private keywords are used in type
+  declarations
 - PR#5634: parsetree rewriter (-ppx flag)
 - ocamldep now supports -absname
-- PR#5768: On "unbound identifier" errors, use spell-checking to suggest names present in the environment
+- PR#5768: On "unbound identifier" errors, use spell-checking to suggest names
+  present in the environment
 - ocamlc has a new option -dsource which visualize the parsetree
 - tools/eqparsetree compare two parsetree ignoring location
 Bug fixes:
@@ -37,17 +45,19 @@ Bug fixes:
 - PR#5763: ocamlbuild does not give correct flags when running menhir
 - PR#5784: -dclambda option is ignored
 - PR#5787: Bad behavior of 'Unused ...' warnings in the toplevel
-- PR#5770: Syntax error messages involving unclosed parens are sometimes incorrect
+- PR#5770: Syntax error messages involving unclosed parens are sometimes
+  incorrect
 - PR#5805: Assert failure with warning 34 on pre-processed file
 - PR#5821: Wrong record field is reported as duplicate
 - PR#5824: Generate more efficient code for immediate right shifts.
-- PR#5825: Add a toplevel primitive to use source file wrapped with the coresponding module
+- PR#5825: Add a toplevel primitive to use source file wrapped with the
+  coresponding module
 - PR#5835: nonoptional labeled arguments can be passed with '?'
 - PR#5865: assert failure when reporting undefined field label
 
 Internals:
 - Moved debugger/envaux.ml to typing/envaux.ml to publish env_of_only_summary
-   as part of compilerlibs, to be used on bin-annot files.
+  as part of compilerlibs, to be used on bin-annot files.
 
 Feature wishes:
 - PR#5597: add instruction trace option 't' to OCAMLRUNPARAM
diff --git a/testsuite/tests/typing-gadts/test.ml.principal.reference b/testsuite/tests/typing-gadts/test.ml.principal.reference
index 6efcb4f798..dbad727023 100644
--- a/testsuite/tests/typing-gadts/test.ml.principal.reference
+++ b/testsuite/tests/typing-gadts/test.ml.principal.reference
@@ -62,11 +62,11 @@ Error: Recursive local constraint when unifying (s, s) t with (s, s * s) t
              ^^^^^^^^
 Error: This pattern matches values of type int t
        but a pattern was expected which matches values of type s t
-#                         Characters 224-237:
-          | `A, BoolLit _ -> ()
-            ^^^^^^^^^^^^^
-Error: This pattern matches values of type ([? `A ] as 'a) * bool t
-       but a pattern was expected which matches values of type 'a * int t
+#                         module Polymorphic_variants :
+  sig
+    type _ t = IntLit : int -> int t | BoolLit : bool -> bool t
+    val eval : [ `A ] * 's t -> unit
+  end
 #                                 Characters 299-300:
       | BoolLit b -> b
                      ^
diff --git a/testsuite/tests/typing-gadts/test.ml.reference b/testsuite/tests/typing-gadts/test.ml.reference
index 2a4ccde675..af8047775d 100644
--- a/testsuite/tests/typing-gadts/test.ml.reference
+++ b/testsuite/tests/typing-gadts/test.ml.reference
@@ -62,11 +62,11 @@ Error: Recursive local constraint when unifying (s, s) t with (s, s * s) t
              ^^^^^^^^
 Error: This pattern matches values of type int t
        but a pattern was expected which matches values of type s t
-#                         Characters 224-237:
-          | `A, BoolLit _ -> ()
-            ^^^^^^^^^^^^^
-Error: This pattern matches values of type ([? `A ] as 'a) * bool t
-       but a pattern was expected which matches values of type 'a * int t
+#                         module Polymorphic_variants :
+  sig
+    type _ t = IntLit : int -> int t | BoolLit : bool -> bool t
+    val eval : [ `A ] * 's t -> unit
+  end
 #                                 module Propagation :
   sig
     type _ t = IntLit : int -> int t | BoolLit : bool -> bool t
diff --git a/testsuite/tests/typing-misc/polyvars.ml.principal.reference b/testsuite/tests/typing-misc/polyvars.ml.principal.reference
index c56c3570a3..fabbb9071d 100644
--- a/testsuite/tests/typing-misc/polyvars.ml.principal.reference
+++ b/testsuite/tests/typing-misc/polyvars.ml.principal.reference
@@ -1,10 +1,21 @@
 
 # type ab = [ `A | `B ]
-# val f : [ `A ] -> int = <fun>
-# val f : [ `A ] -> unit = <fun>
+# Characters 32-35:
+  let f (x : [`A]) = match x with #ab -> 1;;
+                                  ^^^
+Error: This pattern matches values of type [? `A | `B ]
+       but a pattern was expected which matches values of type [ `A ]
+       The second variant type does not allow tag(s) `B
+# Characters 31-34:
+  let f x = ignore (match x with #ab -> 1); ignore (x : [`A]);;
+                                 ^^^
+Error: This pattern matches values of type [? `B ]
+       but a pattern was expected which matches values of type [ `A ]
+       Types for tag `B are incompatible
 # Characters 34-36:
   let f x = ignore (match x with `A|`B -> 1); ignore (x : [`A]);;
                                     ^^
-Warning 12: this sub-pattern is unused.
-val f : [ `A ] -> unit = <fun>
+Error: This pattern matches values of type [? `B ]
+       but a pattern was expected which matches values of type [ `A ]
+       Types for tag `B are incompatible
 # 
diff --git a/testsuite/tests/typing-misc/polyvars.ml.reference b/testsuite/tests/typing-misc/polyvars.ml.reference
index c56c3570a3..4117b70fd7 100644
--- a/testsuite/tests/typing-misc/polyvars.ml.reference
+++ b/testsuite/tests/typing-misc/polyvars.ml.reference
@@ -1,10 +1,21 @@
 
 # type ab = [ `A | `B ]
-# val f : [ `A ] -> int = <fun>
-# val f : [ `A ] -> unit = <fun>
+# Characters 32-35:
+  let f (x : [`A]) = match x with #ab -> 1;;
+                                  ^^^
+Error: This pattern matches values of type [? `A | `B ]
+       but a pattern was expected which matches values of type [ `A ]
+       The second variant type does not allow tag(s) `B
+# Characters 31-34:
+  let f x = ignore (match x with #ab -> 1); ignore (x : [`A]);;
+                                 ^^^
+Error: This pattern matches values of type [? `B ]
+       but a pattern was expected which matches values of type [ `A ]
+       The second variant type does not allow tag(s) `B
 # Characters 34-36:
   let f x = ignore (match x with `A|`B -> 1); ignore (x : [`A]);;
                                     ^^
-Warning 12: this sub-pattern is unused.
-val f : [ `A ] -> unit = <fun>
+Error: This pattern matches values of type [? `B ]
+       but a pattern was expected which matches values of type [ `A ]
+       The second variant type does not allow tag(s) `B
 # 
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 *)