fixed small bug for levels of reified types in patterns and cleaned up ctype

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

typing/ctype.ml

@@ -102,6 +102,7 @@ let nongen_level = ref 0
 let global_level = ref 1
 let saved_level = ref []
 
+let get_current_level () = !current_level
 let init_def level = current_level := level; nongen_level := level
 let begin_def () =
   saved_level := (!current_level, !nongen_level) :: !saved_level;
@@ -1571,7 +1572,14 @@ let deep_occur t0 ty =
 
 let pattern_unification = ref false
 
+let pattern_level = ref None
+
 let reify env t =  
+  let pattern_level = 
+    match !pattern_level with
+    | None -> assert false
+    | Some x -> x
+  in
   let rec iterator ty = 
     match (repr ty).desc with 
     | Tvar -> 
@@ -1585,7 +1593,7 @@ let reify env t =
       }
       in
       let (id, new_env) = Env.enter_type (get_new_abstract_name ()) decl !env in
-      let to_unify = newty (Tconstr (Path.Pident id,[],ref Mnil)) in
+      let to_unify = newty2 pattern_level (Tconstr (Path.Pident id,[],ref Mnil)) in
       env := new_env;
       link_type ty to_unify
     | _ ->
@@ -1679,47 +1687,19 @@ and unify3 env t1 t1' t2 t2' =
   (* Third step: truly unification *)
   (* Assumes either [t1 == t1'] or [t2 != t2'] *)
   let d1 = t1'.desc and d2 = t2'.desc in
-
   let create_recursion = (t2 != t2') && (deep_occur t1' t2) in
-  occur !env t1' t2;
-  update_level !env t1'.level t2;
-  add_type_equality t1' t2;
+  occur !env t1' t2';
+  add_type_equality t1' t2';
   try
     begin match (d1, d2) with
       (Tvar, _) ->
-(*	link_type t1' t2;
-        occur_univar !env t2*)
+	update_level !env t1'.level t2;
 	link_type t1' t2;
-        let td2 = newgenty d2 in
-        occur !env t1' td2;
-        occur_univar !env td2;
-        if t2 == t2' then begin
-          (* The variable must be instantiated... *)
-          let ty = newty2 t2'.level d2 in
-          update_level !env t1'.level ty;
-          link_type t1' ty
-        end else begin
-          log_type t2';
-          t2'.desc <- d2;
-          update_level !env t1'.level t2;
-          link_type t1' t2
-        end
+        occur_univar !env t2
     | (_, Tvar) ->
+	update_level !env t2'.level t1;
 	link_type t2' t1;
-        let td1 = newgenty d1 in
-        occur !env t2' td1;
-        occur_univar !env td1;
-        if t1 == t1' then begin
-          (* The variable must be instantiated... *)
-          let ty = newty2 t1'.level d1 in
-          update_level !env t2'.level ty;
-          link_type t2' ty
-        end else begin
-          log_type t1';
-          t1'.desc <- d1;
-          update_level !env t2'.level t1;
-          link_type t2' t1
-        end
+        occur_univar !env t1
     | (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;
@@ -2023,7 +2003,7 @@ let unify env ty1 ty2 =
   with Unify trace ->
     raise (Unify (expand_trace !env trace))
 
-let unify_gadt (env:Env.t ref) ty1 ty2 =
+let unify_gadt pattern_level (env:Env.t ref) ty1 ty2 =
   try
     pattern_unification:=true;
     unify env ty1 ty2;

typing/ctype.mli

@@ -141,7 +141,7 @@ val enforce_constraints: Env.t -> type_expr -> unit
 
 val unify: Env.t -> type_expr -> type_expr -> unit
         (* Unify the two types given. Raise [Unify] if not possible. *)
-val unify_gadt: Env.t ref -> type_expr -> type_expr -> unit
+val unify_gadt: int -> Env.t ref -> type_expr -> type_expr -> unit
         (* Unify the two types given and update the environment with the local constraints. Raise [Unify] if not possible. *)
 val unify_var: Env.t -> type_expr -> type_expr -> unit
         (* Same as [unify], but allow free univars when first type
@@ -245,3 +245,5 @@ val arity: type_expr -> int
 
 val collapse_conj_params: Env.t -> type_expr list -> unit
         (* Collapse conjunctive types in class parameters *)
+
+val get_current_level: unit -> int

typing/parmatch.ml

@@ -623,7 +623,7 @@ let initial_env = ref Env.empty
 let unifiable t t' = 
   let snap = Btype.snapshot () in
   try
-    Ctype.unify_gadt (ref !initial_env) t t';
+    Ctype.unify_gadt 0 (ref !initial_env) t t'; (* GAH: we need separate algorithm for GADTs *)
     Btype.backtrack snap;
     true
   with

typing/typecore.ml

@@ -149,9 +149,16 @@ let unify_pat_types loc env ty ty' =
   | Tags(l1,l2) ->
       raise(Typetexp.Error(loc, Typetexp.Variant_tags (l1, l2)))
 
+let pattern_level = ref None
+
 let unify_pat_types_gadt loc env ty ty' = 
+  let pattern_level = 
+    match !pattern_level with
+    | None -> assert false
+    | Some x -> x
+  in
   try
-    unify_gadt env ty ty'
+    unify_gadt pattern_level env ty ty'
   with
     Unify trace ->
       raise(Error(loc, Pattern_type_clash(trace)))
@@ -604,6 +611,18 @@ let rec type_pat (env:Env.t ref) sp expected_ty  =
       unify_pat_types loc !env ty expected_ty;
       r
 
+let type_pat env sp expected_ty = 
+  pattern_level := Some (get_current_level ());
+  try
+    let r = type_pat env sp expected_ty in
+    pattern_level := None;
+    r
+  with
+    e -> 
+      pattern_level := None;
+      raise e
+  
+
 let get_ref r =
   let v = !r in r := []; v
 
@@ -2208,9 +2227,7 @@ and type_cases ?in_function env ty_arg ty_res partial_loc caselist =
 (*  let closed = free_variables ~env ty_arg = [] in*)
 (*  let ty_arg' = newvar () in *) 
   begin_def ();
-  let ty = newvar () in
-  Ident.set_current_time ty.level;
-  Ctype.init_def(Ident.current_time());
+  Ident.set_current_time (get_current_level ());
   let pattern_force = ref [] in
   let pat_env_list =
     List.map
@@ -2240,7 +2257,7 @@ and type_cases ?in_function env ty_arg ty_res partial_loc caselist =
   end;
   (* `Contaminating' unifications start here *)
   List.iter (fun f -> f()) !pattern_force;
-
+  Ctype.init_def(Ident.current_time());
 (*  begin match pat_env_list with [] -> ()
   | (pat, _) :: _ -> unify_pat env pat ty_arg (* GAH: ask garrigue, contamination *) 
   end;*)