Commits

Anonymous committed c837ab4

Fix constraint checking regression; one stack overflow remains in typing-misc/constraints.ml

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

Comments (0)

Files changed (4)

testsuite/tests/typing-misc/Makefile

+BASEDIR=../..
+include $(BASEDIR)/makefiles/Makefile.toplevel
+include $(BASEDIR)/makefiles/Makefile.common
+

testsuite/tests/typing-misc/constraints.ml

+type 'a t = [`A of 'a t t] as 'a;; (* fails *)
+
+type 'a t = [`A of 'a t t];; (* fails *)
+
+type 'a t = [`A of 'a t t] constraint 'a = 'a t;;
+
+type 'a t = [`A of 'a t] constraint 'a = 'a t;;
+
+type 'a t = [`A of 'a] as 'a;;
+
+(* XXX Todo : Fix stack overflow *)
+(*
+type 'a v = [`A of u v] constraint 'a = t and t = u and u = t;;
+*)
+
+type 'a t = 'a;;
+let f (x : 'a t as 'a) = ();; (* fails *)
+
+let f (x : 'a t) (y : 'a) = x = y;;

testsuite/tests/typing-misc/constraints.ml.reference

+
+# Characters 12-32:
+  type 'a t = [`A of 'a t t] as 'a;; (* fails *)
+              ^^^^^^^^^^^^^^^^^^^^
+Error: Constraints are not satisfied in this type.
+       Type
+       [ `A of 'a ] t t as 'a
+       should be an instance of
+       ([ `A of 'b t t ] as 'b) t
+#   Characters 5-27:
+  type 'a t = [`A of 'a t t];; (* fails *)
+      ^^^^^^^^^^^^^^^^^^^^^^
+Error: In the definition of t, type 'a t t should be 'a t
+#   type 'a t = [ `A of 'a t t ] constraint 'a = 'a t
+#   type 'a t = [ `A of 'a t ] constraint 'a = 'a t
+#   type 'a t = 'a constraint 'a = [ `A of 'a ]
+#     * *     type 'a t = 'a
+# Characters 11-21:
+  let f (x : 'a t as 'a) = ();; (* fails *)
+             ^^^^^^^^^^
+Error: This alias is bound to type 'a t = 'a
+       but is used as an instance of type 'a
+       The type variable 'a occurs inside 'a
+#   val f : 'a t -> 'a -> bool = <fun>
+# 
   | (Tfield _, Tfield _) -> (* special case for GADTs *)
       unify_fields env t1' t2'
   | _ ->
-      begin match !umode with
-      | Expression ->
-          occur !env t1' t2';
-          link_type t1' t2
-      | Pattern ->
-          add_type_equality t1' t2'
-      end;
-      try match (d1, d2) with
+    begin match !umode with
+    | Expression ->
+        occur !env t1' t2';
+        link_type t1' t2
+    | Pattern ->
+        add_type_equality t1' t2'
+    end;
+    try
+      begin match (d1, d2) with
         (Tarrow (l1, t1, u1, c1), Tarrow (l2, t2, u2, c2)) when l1 = l2 ||
         !Clflags.classic && not (is_optional l1 || is_optional l2) ->
           unify  env t1 t2; unify env  u1 u2;
           unify_list env tl1 tl2
       | (_, _) ->
           raise (Unify [])
-      with Unify trace ->
-        t1'.desc <- d1;
-        raise (Unify trace)
-  end;
-  (* XXX Commentaires + changer "create_recursion" *)
-  if create_recursion then begin
-    match t2.desc with
-      Tconstr (p, tl, abbrev) ->
-        forget_abbrev abbrev p;
-        let t2'' = expand_head_unif !env t2 in
-        if not (closed_parameterized_type tl t2'') then
-          link_type (repr t2) (repr t2')
-    | _ ->
-        () (* t2 has already been expanded by update_level *)
+      end;
+      (* XXX Commentaires + changer "create_recursion" *)
+      if create_recursion then
+        match t2.desc with
+          Tconstr (p, tl, abbrev) ->
+            forget_abbrev abbrev p;
+            let t2'' = expand_head_unif !env t2 in
+            if not (closed_parameterized_type tl t2'') then
+              link_type (repr t2) (repr t2')
+        | _ ->
+            () (* t2 has already been expanded by update_level *)
+    with Unify trace ->
+      t1'.desc <- d1;
+      raise (Unify trace)
   end
 
 and unify_list env tl1 tl2 =