disable progragation in pattern-matchings containing polymorphic variants

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

4 files changed, 111 insertions, 12 deletions

diff --git a/parsing/parsetree.mli b/parsing/parsetree.mli
index 14f9cdb75..e81d9ece1 100644
--- a/parsing/parsetree.mli
+++ b/parsing/parsetree.mli
@@ -73,7 +73,8 @@ and pattern_desc =
   | Ppat_tuple of pattern list
   | Ppat_construct of Longident.t * pattern option * bool * Longident.t option
   | Ppat_variant of label * pattern option
-  | Ppat_record of (Longident.t * pattern) list * closed_flag * Longident.t option
+  | Ppat_record of
+      (Longident.t * pattern) list * closed_flag * Longident.t option
   | Ppat_array of pattern list
   | Ppat_or of pattern * pattern
   | Ppat_constraint of pattern * core_type
@@ -139,7 +140,8 @@ and type_declaration =
 
 and type_kind =
     Ptype_abstract
-  | Ptype_variant of (string * core_type list * core_type option * Location.t) list
+  | Ptype_variant of
+      (string * core_type list * core_type option * Location.t) list
   | Ptype_record of
       (string * mutable_flag * core_type * Location.t) list
 
diff --git a/testsuite/tests/typing-gadts/test.ml.principal.reference b/testsuite/tests/typing-gadts/test.ml.principal.reference
new file mode 100644
index 000000000..0b70c140a
--- /dev/null
+++ b/testsuite/tests/typing-gadts/test.ml.principal.reference
@@ -0,0 +1,74 @@
+
+#                                             module Exp :
+  sig
+    type 'a t =
+        IntLit : int -> int t
+      | BoolLit : bool -> bool t
+      | Pair : 'b t * 'c t -> ('b * 'c) t
+      | App : ('e -> 'd) t * 'e t -> 'd t
+      | Abs : ('f -> 'g) -> ('f -> 'g) t
+    val eval : 'a t -> 'a
+  end
+#                                     module List :
+  sig
+    type zero
+    type 'a t = Nil : zero t | Cons : 'b * 'c t -> ('b * 'c) t
+    val head : ('a * 'b) t -> 'a
+    val tail : ('a * 'b) t -> 'b t
+    val length : 'a t -> int
+  end
+#                                                         Characters 206-227:
+  ......function
+  	| C2 x -> x
+Warning 8: this pattern-matching is not exhaustive.
+Here is an example of a value that is not matched:
+C1 _
+Characters 469-526:
+  ......function
+  	| Foo _ , Foo _ -> true
+  	| Bar _, Bar _ -> true
+Warning 8: this pattern-matching is not exhaustive.
+Here is an example of a value that is not matched:
+(Bar _, Foo _)
+module Nonexhaustive :
+  sig
+    type 'a u = C1 : int -> int u | C2 : bool -> bool u
+    type 'a v = C1 : int -> int v
+    val unexhaustive : 'a u -> 'a
+    module M : sig type t type u end
+    type 'a t = Foo : M.t -> M.t t | Bar : M.u -> M.u t
+    val same_type : 'a t * 'a t -> bool
+  end
+#                             module Exhaustive :
+  sig
+    type t = int
+    type u = bool
+    type 'a v = Foo : t -> t v | Bar : u -> u v
+    val same_type : 'a v * 'a v -> bool
+  end
+#               Characters 119-120:
+      let eval (D x) = x
+                       ^
+Error: This expression has type &x7 t but an expression was expected of type
+         &x7 t
+       The type constructor &x7 would escape its scope
+#                       Characters 157-158:
+  	  C ->
+     ^
+Error: This pattern matches values of type (s, s) t
+       but a pattern was expected which matches values of type (s, s * s) t
+#                         Characters 174-182:
+  	| (IntLit _ | BoolLit _) -> ()
+      ^^^^^^^^
+Error: This pattern matches values of type int t
+       but a pattern was expected which matches values of type s t
+#                         Characters 213-226:
+  	| `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
+#                                     Characters 288-289:
+    | BoolLit b -> b
+                   ^
+Error: This expression has type bool but an expression was expected of type s
+# 
diff --git a/testsuite/tests/typing-gadts/test.ml.reference b/testsuite/tests/typing-gadts/test.ml.reference
index c77292627..177ff66b6 100644
--- a/testsuite/tests/typing-gadts/test.ml.reference
+++ b/testsuite/tests/typing-gadts/test.ml.reference
@@ -61,11 +61,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
-#                         module Polymorphic_variants :
-  sig
-    type 'a t = IntLit : int -> int t | BoolLit : bool -> bool t
-    val eval : [ `A ] * 'a t -> unit
-  end
+#                         Characters 213-226:
+  	| `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 Propagation :
   sig
     type 'a t = IntLit : int -> int t | BoolLit : bool -> bool t
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 1aa7a7578..b3fe2f78e 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -1209,7 +1209,27 @@ let create_package_type loc env (p, l) =
   let s = !Typetexp.transl_modtype_longident loc env p in
   newty (Tpackage (s,
                    List.map fst l,
-                   List.map (Typetexp.transl_simple_type env false) (List.map snd l)))
+                   List.map (Typetexp.transl_simple_type env false)
+                     (List.map snd l)))
+
+let iter_ppat f p = 
+  match p.ppat_desc with
+  | Ppat_any | Ppat_var _ | Ppat_constant _ 
+  | Ppat_type _ | Ppat_unpack _ | Ppat_construct _ -> ()    
+  | Ppat_array pats -> List.iter f pats
+  | Ppat_or (p1,p2) -> f p1; f p2
+  | Ppat_variant (label, arg) -> may f arg
+  | Ppat_tuple lst ->  List.iter f lst
+  | Ppat_alias (p,_) | Ppat_constraint (p,_) | Ppat_lazy p -> f p 
+  | Ppat_record (args, flag, _) -> List.iter (fun (_,p) -> f p) args 
+
+let contains_polymorphic_variant p = 
+  let rec loop p = 
+    match p.ppat_desc with 
+      Ppat_variant _ | Ppat_type _ -> raise Exit
+    | _ -> iter_ppat loop p
+  in
+  try loop p; false with Exit -> true
 
 let wrap_unpacks sexp unpacks =
   List.fold_left
@@ -2446,6 +2466,8 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
   Ctype.init_def lev;
   if !Clflags.principal then begin_def (); (* propagation of the argument *)
   let ty_arg' = newvar () in
+  let dont_propagate =
+    List.exists (fun (p,_) -> contains_polymorphic_variant p) caselist in
   let pattern_force = ref [] in
   let pat_env_list =
     List.map
@@ -2454,8 +2476,10 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
         if !Clflags.principal then begin_def (); (* propagation of pattern *)
         let scope = Some (Annot.Idef loc) in
         let (pat, ext_env, force, unpacks) = 
-	  let ty_arg = instance ~partial:!Clflags.principal ty_arg in 
-	  type_pattern ~lev env spat scope ty_arg 
+	  let ty_arg =
+            if dont_propagate then newvar () else
+            instance ~partial:!Clflags.principal ty_arg
+          in type_pattern ~lev env spat scope ty_arg 
 	in	
         pattern_force := force @ !pattern_force;
         let pat =
@@ -2512,8 +2536,7 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
   unify_exp_types loc env ty_res (newvar ()) ;
   let partial =
     if partial_flag then
-      Parmatch.check_partial_gadt
-	(partial_pred env ty_arg) loc cases
+      Parmatch.check_partial_gadt (partial_pred env ty_arg) loc cases
     else
       Partial
   in