added recursive check for local constraint

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

typing/ctype.ml

@@ -95,6 +95,8 @@ exception Cannot_apply
 
 exception Recursive_abbrev
 
+exception Unification_recursive_abbrev of (type_expr * type_expr) list
+
 (**** Type level management ****)
 
 let current_level = ref 0
@@ -1939,6 +1941,7 @@ and unify3 mode env t1 t1' t2 t2' =
         unify_list mode env tl1 tl2
     | (Tconstr ((Path.Pident p) as path,[],_)),_  when is_abstract_newtype !env path && mode = Pattern -> 
 	reify env t2 ;
+	correct_abbrev !env (Path.Pident p) [] t2;
 	begin_def ();
 	let t2 = duplicate_type t2 in
 	end_def ();
@@ -1947,10 +1950,12 @@ and unify3 mode env t1 t1' t2 t2' =
         env := Env.add_type p decl !env 
     | _,(Tconstr ((Path.Pident p) as path,[],_)) when is_abstract_newtype !env path && mode = Pattern -> 
 	reify env t1 ;
+	correct_abbrev !env (Path.Pident p) [] t2;
 	begin_def ();
 	let t1 = duplicate_type t1 in
 	end_def ();
 	generalize t1 ;
+
 	let decl = new_declaration true (Some t1) in
         env := Env.add_type p decl !env 
     | Tconstr (p1,_,_), Tconstr (p2,_,_) when mode = Pattern ->
@@ -2217,8 +2222,11 @@ let unify mode env ty1 ty2 =
   try
     TypePairs.clear unify_eq_set;
     unify mode env ty1 ty2
-  with Unify trace ->
-    raise (Unify (expand_trace !env trace))
+  with 
+  | Unify trace ->
+      raise (Unify (expand_trace !env trace))
+  | Recursive_abbrev ->
+      raise (Unification_recursive_abbrev (expand_trace !env [(ty1,ty2)]))
 
 
 let unify_gadt plev (env:Env.t ref) ty1 ty2 =
@@ -3559,6 +3567,7 @@ let cyclic_abbrev env id ty =
     let ty = repr ty in
     match ty.desc with
       Tconstr (p, tl, abbrev) ->
+	print_endline (Path.name p);
         p = Path.Pident id || List.memq ty seen ||
         begin try
           check_cycle (ty :: seen) (expand_abbrev_opt env ty)
@@ -3567,8 +3576,11 @@ let cyclic_abbrev env id ty =
         | Unify _ -> true
         end
     | _ ->
+	print_endline "false";
         false
-  in check_cycle [] ty
+  in
+  print_endline "calling cyclic_abbrev";
+  check_cycle [] ty
 
 (* Normalize a type before printing, saving... *)
 (* Cannot use mark_type because deep_occur uses it too *)

typing/ctype.mli

@@ -24,6 +24,7 @@ exception Subtype of
 exception Cannot_expand
 exception Cannot_apply
 exception Recursive_abbrev
+exception Unification_recursive_abbrev of (type_expr * type_expr) list
 
 val init_def: int -> unit
         (* Set the initial variable level *)

typing/typeclass.ml

@@ -1608,3 +1608,4 @@ let report_error ppf = function
         "instance variable"
   | No_overriding (kind, name) ->
       fprintf ppf "@[The %s `%s'@ has no previous definition@]" kind name
+	

typing/typecore.ml

@@ -57,6 +57,7 @@ type error =
   | Not_a_variant_type of Longident.t
   | Incoherent_label_order
   | Less_general of string * (type_expr * type_expr) list
+  | Recursive_local_constraint of (type_expr * type_expr) list
 
 exception Error of Location.t * error
 
@@ -177,6 +178,8 @@ let unify_pat_types_gadt loc env ty ty' =
       raise(Error(loc, Pattern_type_clash(trace)))
   | Tags(l1,l2) ->
       raise(Typetexp.Error(loc, Typetexp.Variant_tags (l1, l2)))
+  | Unification_recursive_abbrev trace ->
+      raise(Error(loc, Recursive_local_constraint trace))
 
 
 (* Creating new conjunctive types is not allowed when typing patterns *)
@@ -2625,3 +2628,9 @@ let report_error ppf = function
       report_unification_error ppf trace
         (fun ppf -> fprintf ppf "This %s has type" kind)
         (fun ppf -> fprintf ppf "which is less general than")
+  | Recursive_local_constraint trace ->
+      report_unification_error ppf trace
+        (function ppf ->
+           fprintf ppf "Recursive local constraint when unifying")
+        (function ppf ->
+           fprintf ppf "with")      

typing/typecore.mli

@@ -96,7 +96,7 @@ type error =
   | Not_a_variant_type of Longident.t
   | Incoherent_label_order
   | Less_general of string * (type_expr * type_expr) list
-
+  | Recursive_local_constraint of (type_expr * type_expr) list
 exception Error of Location.t * error
 
 val report_error: formatter -> error -> unit