revert to try_expand_head in Ctype.occur_rec (bug report by skaller)

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

testlabl/poly.exp

@@ -1,4 +1,4 @@
-        Objective Caml version 3.06+37 (2003-06-30)
+        Objective Caml version 3.07+beta 1
 
 #   * * *       #   type 'a t = { t : 'a; }
 # type 'a fold = { fold : 'b. f:('b -> 'a -> 'b) -> init:'b -> 'b; }
@@ -118,7 +118,7 @@
 val p1 : point = <obj>
 val cp : color_point = <obj>
 val c : circle = <obj>
-val d : float = 11.45362404707371
+val d : float = 11.4536240470737098
 #   val f : < m : 'a. 'a -> 'a > -> < m : 'a. 'a -> 'a > = <fun>
 #   Characters 41-42:
 This expression has type < m : 'a. 'a -> 'a list > but is here used with type
@@ -251,4 +251,7 @@ type 'a v = 'a u t constraint 'a = int
 In the definition of v, type 'a list u should be 'a u
 #       type 'a t = 'a
 type 'a u = A of 'a t
+#     type 'a t = < a : 'a >
+# - : ('a t as 'a) -> 'a t = <fun>
+# type u = 'a t as 'a
 # 

testlabl/poly.exp2

@@ -1,4 +1,4 @@
-        Objective Caml version 3.06+37 (2003-06-30)
+        Objective Caml version 3.07+beta 1
 
 #   * * *       #   type 'a t = { t : 'a; }
 # type 'a fold = { fold : 'b. f:('b -> 'a -> 'b) -> init:'b -> 'b; }
@@ -118,7 +118,7 @@
 val p1 : point = <obj>
 val cp : color_point = <obj>
 val c : circle = <obj>
-val d : float = 11.45362404707371
+val d : float = 11.4536240470737098
 #   val f : < m : 'a. 'a -> 'a > -> < m : 'b. 'b -> 'b > = <fun>
 #   Characters 41-42:
 This expression has type < m : 'a. 'a -> 'a list > but is here used with type
@@ -258,4 +258,7 @@ type 'a v = 'a u t constraint 'a = int
 In the definition of v, type 'a list u should be 'a u
 #       type 'a t = 'a
 type 'a u = A of 'a t
+#     type 'a t = < a : 'a >
+# - : ('a t as 'a) -> ('b t as 'b) t = <fun>
+# type u = 'a t as 'a
 # 

testlabl/poly.ml

@@ -413,3 +413,8 @@ type 'a u = < m : 'a v > and 'a v = 'a list u;;
 (* PR#1744: Ctype.matches *)
 type 'a t = 'a
 type 'a u = A of 'a t;;
+
+(* Unification of cyclic terms *)
+type 'a t = < a : 'a >;;
+fun (x : 'a t as 'a) -> (x : 'b t);;
+type u = 'a t as 'a;;

typing/btype.ml

@@ -328,6 +328,20 @@ let rec forget_abbrev_rec mem path =
 let forget_abbrev mem path =
   try mem := forget_abbrev_rec !mem path with Exit -> ()
 
+let rec check_abbrev_rec path = function
+    Mnil -> true
+  | Mcons (path', _, ty, rem) ->
+      if Path.same path path' && 
+        match repr ty with
+          {desc = Tconstr(path',_,_)} -> Path.same path path'
+        | _ -> false
+      then false
+      else check_abbrev_rec path rem
+  | Mlink mem' ->
+      check_abbrev_rec path !mem'
+
+let check_memorized_abbrevs path =
+  List.for_all (fun mem -> check_abbrev_rec path !mem) !memo
 
                   (**********************************)
                   (*  Utilities for labels          *)
@@ -392,6 +406,10 @@ let log_change ch =
 let log_type ty =
   if ty.id <= !last_snapshot then log_change (Ctype (ty, ty.desc))
 let link_type ty ty' = log_type ty; ty.desc <- Tlink ty'
+(*match repr ty' with
+    {desc=Tconstr(path,_,_)} -> assert (check_memorized_abbrevs path)
+  | _ -> ()
+*)
 let set_level ty level =
   if ty.id <= !last_snapshot then log_change (Clevel (ty, ty.level));
   ty.level <- level

typing/ctype.ml

@@ -1204,8 +1204,8 @@ let rec occur_rec env visited ty0 ty =
         if List.memq ty visited then raise Occur;
         if not !Clflags.recursive_types then
           iter_type_expr (occur_rec env (ty::visited) ty0) ty
-      with Occur when generic_abbrev env p ->
-        let ty' = repr (expand_abbrev env ty) in
+      with Occur -> try
+        let ty' = try_expand_head env ty in
         (* Maybe we could simply make a recursive call here,
            but it seems it could make the occur check loop
            (see change in rev. 1.58) *)
@@ -1215,6 +1215,7 @@ let rec occur_rec env visited ty0 ty =
         | _ ->
             if not !Clflags.recursive_types then
               iter_type_expr (occur_rec env (ty'::visited) ty0) ty'
+      with Cannot_expand -> raise Occur
       end
   | Tobject _ | Tvariant _ ->
       ()
@@ -2071,19 +2072,22 @@ let rec rigidify_rec vars ty =
   let ty = repr ty in
   if ty.level >= lowest_level then begin
     ty.level <- pivot_level - ty.level;
-    begin match ty.desc with
+    match ty.desc with
     | Tvar ->
         if not (List.memq ty !vars) then vars := ty :: !vars
     | Tvariant row ->
         let row = row_repr row in
         let more = repr row.row_more in
-        if more.desc = Tvar && not row.row_fixed then
+        if more.desc = Tvar && not row.row_fixed then begin
           let more' = newty2 more.level Tvar in
           let row' = {row with row_fixed=true; row_fields=[]; row_more=more'}
           in link_type more (newty2 ty.level (Tvariant row'))
-    | _ -> ()
-    end;
-    iter_type_expr (rigidify_rec vars) ty
+        end;
+        iter_row (rigidify_rec vars) row;
+        (* only consider the row variable if the variant is not static *)
+        if not (static_row row) then rigidify_rec vars (row_more row)
+    | _ ->
+        iter_type_expr (rigidify_rec vars) ty
   end
 
 let rigidify ty =