Fix PR#6980 and remove unused Ctype.iterative_generalization

5 files changed, 40 insertions, 27 deletions

diff --git a/Changes b/Changes
index 22ab2d1718..962ec7ae16 100644
--- a/Changes
+++ b/Changes
@@ -293,6 +293,7 @@ Bug fixes:
 - PR#6954: Infinite loop in type checker with module aliases
 - PR#6972, GPR#276: 4.02.3 regression on documentation comments in .cmt files
   (Leo White, report by Olivier Andrieu)
+- PR#6980: Assert failure from polymorphic variants and existentials
 - PR#6982: unexpected type error when packing a module alias
 - PR#6985: `module type of struct include Bar end exposes
            %s#row when Bar contains private row types
diff --git a/testsuite/tests/typing-gadts/pr6980.ml b/testsuite/tests/typing-gadts/pr6980.ml
new file mode 100644
index 0000000000..d42002ad33
--- /dev/null
+++ b/testsuite/tests/typing-gadts/pr6980.ml
@@ -0,0 +1,11 @@
+type 'a t = [< `Foo | `Bar] as 'a;;
+type 'a s = [< `Foo | `Bar | `Baz > `Bar] as 'a;;
+
+type 'a first = First : 'a second -> ('b t as 'a) first
+and 'a second = Second : ('b s as 'a) second;;  
+
+type aux = Aux : 'a t second * ('a -> int) -> aux;;
+
+let it : 'a. [< `Bar | `Foo > `Bar ] as 'a = `Bar;;
+
+let g (Aux(Second, f)) = f it;;
diff --git a/testsuite/tests/typing-gadts/pr6980.ml.reference b/testsuite/tests/typing-gadts/pr6980.ml.reference
new file mode 100644
index 0000000000..5fd89921c2
--- /dev/null
+++ b/testsuite/tests/typing-gadts/pr6980.ml.reference
@@ -0,0 +1,14 @@
+
+# type 'a t = 'a constraint 'a = [< `Bar | `Foo ]
+# type 'a s = 'a constraint 'a = [< `Bar | `Baz | `Foo > `Bar ]
+#     type 'a first = First : 'b t second -> ([< `Bar | `Foo ] as 'b) t first
+and 'a second = Second : [< `Bar | `Baz | `Foo > `Bar ] s second
+#   type aux = Aux : ([< `Bar | `Foo ] as 'a) t second * ('a -> int) -> aux
+#   val it : [< `Bar | `Foo > `Bar ] = `Bar
+#   Characters 28-30:
+  let g (Aux(Second, f)) = f it;;
+                             ^^
+Error: This expression has type [< `Bar | `Foo > `Bar ]
+       but an expression was expected of type [< `Bar | `Foo ]
+       Types for tag `Bar are incompatible
+# 
diff --git a/typing/ctype.ml b/typing/ctype.ml
index c1df6c0b5f..d69fba248e 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -593,32 +593,17 @@ let duplicate_class_type ty =
    [expand_abbrev] (via [subst]) requires these expansions to be
    preserved. Does it worth duplicating this code ?
 *)
-let rec iter_generalize tyl ty =
+let rec generalize ty =
   let ty = repr ty in
   if (ty.level > !current_level) && (ty.level <> generic_level) then begin
     set_level ty generic_level;
     begin match ty.desc with
       Tconstr (_, _, abbrev) ->
-        iter_abbrev (iter_generalize tyl) !abbrev
+        iter_abbrev generalize !abbrev
     | _ -> ()
     end;
-    iter_type_expr (iter_generalize tyl) ty
-  end else
-    tyl := ty :: !tyl
-
-let iter_generalize tyl ty =
-  simple_abbrevs := Mnil;
-  iter_generalize tyl ty
-
-let generalize ty =
-  iter_generalize (ref []) ty
-
-(* Efficient repeated generalisation of the same type *)
-let iterative_generalization min_level tyl =
-  let tyl' = ref [] in
-  List.iter (iter_generalize tyl') tyl;
-  List.fold_right (fun ty l -> if ty.level <= min_level then l else ty::l)
-    !tyl' []
+    iter_type_expr generalize ty
+  end
 
 (* Generalize the structure and lower the variables *)
 
@@ -3291,19 +3276,23 @@ and eqtype_row rename type_pairs subst env row1 row2 =
       | _ -> raise (Unify []))
     pairs
 
+(* Must empty univar_pairs first *)
+let eqtype_list rename type_pairs subst env tl1 tl2 =
+  univar_pairs := [];
+  let snap = Btype.snapshot () in
+  try eqtype_list rename type_pairs subst env tl1 tl2; backtrack snap
+  with exn -> backtrack snap; raise exn
+
+let eqtype rename type_pairs subst env t1 t2 =
+  eqtype_list rename type_pairs subst env [t1] [t2]
+
 (* Two modes: with or without renaming of variables *)
 let equal env rename tyl1 tyl2 =
   try
-    univar_pairs := [];
     eqtype_list rename (TypePairs.create 11) (ref []) env tyl1 tyl2; true
   with
     Unify _ -> false
 
-(* Must empty univar_pairs first *)
-let eqtype rename type_pairs subst env t1 t2 =
-  univar_pairs := [];
-  eqtype rename type_pairs subst env t1 t2
-
 
                           (*************************)
                           (*  Class type matching  *)
diff --git a/typing/ctype.mli b/typing/ctype.mli
index 90bfcbe6de..6a0b506e06 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -90,8 +90,6 @@ val filter_row_fields:
 
 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: Env.t -> type_expr -> unit
         (* Generalize the covariant part of a type, making
            contravariant branches non-generalizable *)