switched to abstract types, still needs work on exhaustion type. the code needs to be cleaned up. printfs need to be removed

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

21 files changed, 671 insertions, 280 deletions

diff --git a/parsing/parser.mly b/parsing/parser.mly
index 87cb9ddec..888938d40 100644
--- a/parsing/parser.mly
+++ b/parsing/parser.mly
@@ -1300,7 +1300,9 @@ constructor_arguments:
 
 generalized_constructor_arguments:
   | COLON core_type_list MINUSGREATER simple_core_type                      
-                                                { (List.rev $2,$4) } 
+                                                { (List.rev $2, $4) } 
+  | COLON simple_core_type                       
+                                                { ([],$2) } 
 ;
 
 
diff --git a/parsing/printast.ml b/parsing/printast.ml
index e173dcb50..ee52f7d9d 100644
--- a/parsing/printast.ml
+++ b/parsing/printast.ml
@@ -747,3 +747,5 @@ let print_expression = expression 0 ;;
 
 let print_pattern = pattern 0 ;;
 
+let print_core_type = core_type 0 ;;
+
diff --git a/parsing/printast.mli b/parsing/printast.mli
index 4bf4635cc..307b5a208 100644
--- a/parsing/printast.mli
+++ b/parsing/printast.mli
@@ -20,3 +20,4 @@ val implementation : formatter -> structure_item list -> unit;;
 val top_phrase : formatter -> toplevel_phrase -> unit;;
 val print_expression : formatter -> expression -> unit;;
 val print_pattern : formatter -> pattern -> unit;;
+val print_core_type : formatter -> core_type -> unit;;
diff --git a/typing/btype.ml b/typing/btype.ml
index 759ed50f5..edfc4bee4 100644
--- a/typing/btype.ml
+++ b/typing/btype.ml
@@ -23,7 +23,7 @@ let generic_level = 100000000
 (* Used to mark a type during a traversal. *)
 let lowest_level = 0
 let pivot_level = 2 * lowest_level - 1
-    (* pivot_level - lowest_level < lowest_level *)
+    (* pivot_level - lowest_level < lowest_level *) 
 
 (**** Some type creators ****)
 
@@ -197,6 +197,11 @@ let iter_type_expr f ty =
   | Tpoly (ty, tyl)     -> f ty; List.iter f tyl
   | Tpackage (_, _, l)  -> List.iter f l
 
+
+
+
+
+
 let rec iter_abbrev f = function
     Mnil                   -> ()
   | Mcons(_, _, ty, ty', rem) -> f ty; f ty'; iter_abbrev f rem
@@ -286,7 +291,7 @@ let cleanup_types () =
 
 (* Mark a type. *)
 let rec mark_type ty =
-  let ty = repr ty in
+  let ty = repr ty in (* GAH : why do we call repr? *)
   if ty.level >= lowest_level then begin
     ty.level <- pivot_level - ty.level;
     iter_type_expr mark_type ty
@@ -520,6 +525,7 @@ let backtrack (changes, old) =
       last_snapshot := old;
       Weak.set trail 0 (Some changes)
 
+
 (**** Sets, maps and hashtables of types ****)
 
 module TypeSet = Set.Make(TypeOps)
diff --git a/typing/btype.mli b/typing/btype.mli
index f230b2f2d..bdf70a53a 100644
--- a/typing/btype.mli
+++ b/typing/btype.mli
@@ -154,6 +154,8 @@ val set_commu: commutable ref -> commutable -> unit
 val log_type: type_expr -> unit
         (* Log the old value of a type, before modifying it by hand *)
 
+    
+
 (**** Sets, maps and hashtables of types ****)
 
 module TypeSet  : Set.S with type elt = type_expr
diff --git a/typing/ctype.ml b/typing/ctype.ml
index bfc9b1243..84408fe8e 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -80,6 +80,11 @@ open Btype
      [unify].
 *)
 
+
+
+
+
+
 (**** Errors ****)
 
 exception Unify of (type_expr * type_expr) list
@@ -102,6 +107,8 @@ 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;
@@ -150,6 +157,7 @@ let newty desc         = newty2 !current_level desc
 let new_global_ty desc = newty2 !global_level desc
 
 let newvar ()          = newty2 !current_level Tvar
+let newtunivar ()      = newty2 !current_level Tunivar
 let newvar2 level      = newty2 level Tvar
 let new_global_var ()  = newty2 !global_level Tvar
 
@@ -435,7 +443,7 @@ let free_vars ?env ty =
 
 let free_variables ?env ty =
   let tl = List.map fst (free_vars ?env ty) in
-  unmark_type ty;
+  unmark_type ty; (* GAH : ask garrigue, unmark_type ??? *)
   tl
 
 let rec closed_type ty =
@@ -1353,7 +1361,7 @@ let rec unify_univar t1 t2 = function
         Some {contents=Some t'2}, Some _ when t2 == repr t'2 ->
           ()
       | Some({contents=None} as r1), Some({contents=None} as r2) ->
-          set_univar r1 t2; set_univar r2 t1
+          set_univar r1 t2; set_univar r2 t1 (* GAH : ask garrigue, setting univars?? *)
       | None, None ->
           unify_univar t1 t2 rem
       | _ ->
@@ -1367,6 +1375,7 @@ let add_free_univars tl =
   let old = !free_univars in
   free_univars := List.fold_right TypeSet.add tl old;
   old
+
 let set_free_univars tl = free_univars := tl
 
 (* Test the occurence of free univars in a type *)
@@ -1391,7 +1400,7 @@ let occur_univar env ty =
       match ty.desc with
         Tunivar ->
           if not (TypeSet.mem ty bound) && not (TypeSet.mem ty !free_univars)
-          then raise (Unify [ty, newgenvar()])
+          then (print_endline "raising occur_univar";raise (Unify [ty, newgenvar()]))
       | Tpoly (ty, tyl) ->
           let bound = List.fold_right TypeSet.add (List.map repr tyl) bound in
           occur_rec bound  ty
@@ -1552,8 +1561,10 @@ let deep_occur t0 ty =
 *)
 
 let pattern_unification = ref false
-let local_unifier = ref []
+let pattern_level = ref 0
 
+let set_gadt_pattern_level i = pattern_level := !current_level
+let get_gadt_pattern_level () = !pattern_level
 
 let set_unification_type x = 
   match x with
@@ -1567,74 +1578,132 @@ let get_unification_type () =
   | true -> `Pattern
   | false -> `Expression
 
-let reset_local_unifier () = 
-  local_unifier := []
+let reified_var_counter = ref 0
+    
+let get_new_abstract_name () = 
+  let ret = Printf.sprintf "&x%d" !reified_var_counter in
+  incr reified_var_counter;
+  ret
+
+let reify env t =  (* GAH: ask garrigue; is this right? *)
+  let rec iterator ty = 
+
+    match (repr ty).desc with 
+    | Tvar -> 
+      let decl = {
+        type_params = [];
+        type_arity = 0;
+        type_kind = Type_abstract;
+        type_private = Public;
+        type_manifest = None;
+        type_variance = [];
+      }
+      in
+      if ty.level < get_gadt_pattern_level () then
+	raise (Unify [])
+      else
+	let ty = newvar () in
+	Ident.set_current_time ty.level;
+	let (id, new_env) = Env.enter_type (get_new_abstract_name ()) decl !env in
+	let to_unify = newty2 (get_gadt_pattern_level ()) (Tconstr (Path.Pident id,[],ref Mnil)) in (* GAH : ask garrigue, what in the world is an abbrev_memo ?? *)
+	env := new_env;
+	link_type ty to_unify
+    | _ ->
+	iter_type_expr iterator ty
+  in
+  iter_type_expr iterator (full_expand !env t)
+
+
+let print_path_names t1 t2 = 
+  match t1.desc,t2.desc with 
+  | Tconstr (p1,[],_),Tconstr (p2,[],_)    -> 
+      begin match p1,p2 with
+      | Path.Pident q1,Path.Pident q2 ->
+	  Printf.printf "different paths but %s %s\n%!" (Ident.name q1) (Ident.name q2)
+      | _ -> print_endline "not idents"
+      end
+  | _ -> print_endline "not constructors"
+
+let unify_eq_set = Btype.TypeHash.create 10 
+
+let add_type_equality t1 t2 = 
+  try
+    let set = TypeHash.find unify_eq_set t1  in 
+    set := Btype.TypeSet.add t2 !set
+  with
+  | Not_found ->
+      TypeHash.add unify_eq_set t1 (ref (TypeSet.add t2 TypeSet.empty))
+
+
 
-let get_local_unifier () = !local_unifier
-let uni_equalities = ref TypeSetPair.empty
-let uni_eq t1 t2 = t1 == t2 || TypeSetPair.mem   (t1,t2) !uni_equalities   || TypeSetPair.mem   (t2,t1)  !uni_equalities
-let add_equality t1 t2 = 
-  uni_equalities := TypeSetPair.add  (t1, t2) !uni_equalities
 
+let unify_eq t1 t2 =
+  let test t1 t2 =
+    try
+      Btype.TypeSet.mem t2 !(TypeHash.find unify_eq_set t1) ;
+    with
+    | Not_found -> false
+  in	
+  t1 == t2 || test t1 t2 || test t2 t1
 
-let rec unify env t1 t2 =
+
+let rec unify (env:Env.t ref) t1 t2 =
   (* First step: special cases (optimizations) *)
-  if uni_eq t1 t2 then () else
+
+
+
+  if unify_eq t1 t2 then () else
   let t1 = repr t1 in
   let t2 = repr t2 in
-  if uni_eq t1 t2 then () else
+  if unify_eq t1 t2 then () else
+  
   try
     type_changed := true;
     match (t1.desc, t2.desc) with
-    | (Tvar, Tconstr _) when deep_occur t1 t2  -> 
+      (Tvar, Tconstr _) when deep_occur t1 t2 ->
         unify2 env t1 t2
-    | (Tconstr _, Tvar) when deep_occur t2 t1  -> 
+    | (Tconstr _, Tvar) when deep_occur t2 t1 ->
         unify2 env t1 t2
-    | (Tvar, _)  -> 
-        occur env t1 t2; occur_univar env t2;
-        update_level env t1.level t2;
+    | (Tvar, _) ->
+        occur !env t1 t2; occur_univar !env t2;
+        update_level !env t1.level t2;
         link_type t1 t2
-    | (_, Tvar)  -> 
-        occur env t2 t1; occur_univar env t1;
-        update_level env t2.level t1;
+    | (_, Tvar) ->
+        occur !env t2 t1; occur_univar !env t1;
+        update_level !env t2.level t1;
         link_type t2 t1
-    | (Tunivar, Tunivar)  ->  (* GAH : ask garrigue: when do we unify univars? *)
+    | (Tunivar, Tunivar) ->
         unify_univar t1 t2 !univar_pairs;
-        update_level env t1.level t2;
+        update_level !env t1.level t2;
         link_type t1 t2
-
     | (Tconstr (p1, [], a1), Tconstr (p2, [], a2))
           when Path.same p1 p2
             (* This optimization assumes that t1 does not expand to t2
                (and conversely), so we fall back to the general case
                when any of the types has a cached expansion. *)
             && not (has_cached_expansion p1 !a1
-                 || has_cached_expansion p2 !a2)  -> 
-        update_level env t1.level t2;
+                 || has_cached_expansion p2 !a2) ->
+        update_level !env t1.level t2;
         link_type t1 t2
-
-
-    | _  -> 
+    | _ ->
         unify2 env t1 t2
   with Unify trace ->
     raise (Unify ((t1, t2)::trace))
 
 and unify2 env t1 t2 =
-
-
-
   (* Second step: expansion of abbreviations *)
   let rec expand_both t1'' t2'' =
-    let t1' = expand_head_unif env t1 in
-    let t2' = expand_head_unif env t2 in
+    let t1' = expand_head_unif !env t1 in
+    let t2' = expand_head_unif !env t2 in
     (* Expansion may have changed the representative of the types... *)
-    if uni_eq t1' t1'' && uni_eq t2' t2'' then (t1',t2') else
+    if unify_eq t1' t1'' && unify_eq t2' t2'' then (t1',t2') else
     expand_both t1' t2'
   in
   let t1', t2' = expand_both t1 t2 in
-  if uni_eq t1' t2' then () else
+  if unify_eq t1' t2' then () else
+
   let t1 = repr t1 and t2 = repr t2 in
-  if (uni_eq t1 t1') || (not (uni_eq t2 t2')) then (* GAH: ask garrigue why this code seems so strange *)
+  if unify_eq t1 t1' || not (unify_eq t2 t2') then
     unify3 env t1 t1' t2 t2'
   else
     try unify3 env t2 t2' t1 t1' with Unify trace ->
@@ -1646,48 +1715,100 @@ and unify3 env t1 t1' 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_equality t1' t2;
-
-
-  
+  occur !env t1' t2;
+  update_level !env t1'.level t2;
+  add_type_equality t1' t2;
   try
     begin match (d1, d2) with
       (Tvar, _) ->
 	link_type t1' t2;
-        occur_univar env t2
+        occur_univar !env t2
     | (_, Tvar) ->
 	link_type t2' t1;
-        occur_univar env t1;
-(*        let td1 = newgenty d1 in
-        occur env t2' td1;
-
+        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;
+          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;
+          update_level !env t2'.level t1;
           link_type t2' t1
-        end*)
+        end
     | (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  env t1 t2; unify env  u1 u2;
         begin match commu_repr c1, commu_repr c2 with
           Clink r, c2 -> set_commu r c2
         | c1, Clink r -> set_commu r c1
         | _ -> ()
         end
     | (Ttuple tl1, Ttuple tl2) ->
+
         unify_list env tl1 tl2
     | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 ->
+
         unify_list env tl1 tl2
+
+    | _,(Tconstr (Path.Pident p,[],_))  when not !pattern_unification -> (* GAH : must be abstract or else it would have been expanded, ask garrigue *)
+	raise (Unify [])
+
+(*	let _,td =  Env.lookup_type (Longident.parse (Ident.name p)) !env in*)
+(*	let td = Env.lookup_type  (Ident.name "t") !env in	
+	(match td.type_manifest with
+	| None ->
+	    print_endline "no manifest 1"
+	| Some ty ->
+	    print_endline (string_of_bool (ty == t1));
+	    print_endline "have a manifest 1");
+*)
+
+(*	ignore(Env.find_type_expansion  (Path.Pident p) !env);*)
+
+	
+
+    | Tconstr (p1,[],_),Tconstr (p2,[],_)  when Path.same p1 p2  -> 
+	print_endline "same path yo";
+
+
+(* GAH : must be abstract or else it would have been expanded, ask garrigue *)
+
+    | (Tconstr (Path.Pident p,[],_)),_  when !pattern_unification -> (* GAH : must be abstract or else it would have been expanded, ask garrigue *)
+	let t2 = copy t2 in
+
+	reify env t2 ;
+
+	let decl = {
+          type_params = [];
+          type_arity = 0;
+          type_kind = Type_abstract;
+          type_private = Public;
+          type_manifest = Some t2;
+          type_variance = [];
+	}
+	in
+	let new_env = Env.add_type  p decl !env in
+	env := new_env
+    | _,(Tconstr (Path.Pident p,[],_)) when !pattern_unification -> 
+	let t1 = copy t1 in
+	reify env t1 ;
+	let decl = {
+          type_params = [];
+          type_arity = 0;
+          type_kind = Type_abstract;
+          type_private = Public;
+          type_manifest = Some t1;
+          type_variance = [];
+	}
+	in
+	let new_env = Env.add_type p decl !env in
+	env := new_env 
     | (Tobject (fi1, nm1), Tobject (fi2, _)) ->
+	link_type t1' t2;
         unify_fields env fi1 fi2;
         (* Type [t2'] may have been instantiated by [unify_fields] *)
         (* XXX One should do some kind of unification... *)
@@ -1701,10 +1822,13 @@ and unify3 env t1 t1' t2 t2' =
             ()
         end
     | (Tvariant row1, Tvariant row2) ->
+	link_type t1' t2;
         unify_row env row1 row2
     | (Tfield _, Tfield _) ->           (* Actually unused *)
+	link_type t1' t2;
         unify_fields env t1' t2'
     | (Tfield(f,kind,_,rem), Tnil) | (Tnil, Tfield(f,kind,_,rem)) ->
+	link_type t1' t2;
         begin match field_kind_repr kind with
           Fvar r when f <> dummy_method -> set_kind r Fabsent
         | _      -> raise (Unify [])
@@ -1712,23 +1836,14 @@ and unify3 env t1 t1' t2 t2' =
     | (Tnil, Tnil) ->
         ()
     | (Tpoly (t1, []), Tpoly (t2, [])) ->
-        unify env t1 t2
+	link_type t1' t2;
+        unify env  t1 t2
     | (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
-        enter_poly env univar_pairs t1 tl1 t2 tl2 (unify env)
+	link_type t1' t2;
+        enter_poly !env univar_pairs t1 tl1 t2 tl2 (unify env)
     | (Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2)) when Path.same p1 p2 && n1 = n2 ->
+	link_type t1' t2;
         unify_list env tl1 tl2
-    | (Tunivar,_)  -> 
-	
-	if !pattern_unification then 
-	  local_unifier:= (t1,t2) :: !local_unifier
-	else
-          raise (Unify [])
-    | (_,Tunivar)  -> 
-	
-	if !pattern_unification then 
-	  local_unifier:= (t2,t1) :: !local_unifier
-	else
-          ( raise (Unify []) )
     | (_, _) ->
         raise (Unify [])
     end;
@@ -1738,7 +1853,7 @@ and unify3 env t1 t1' t2 t2' =
       match t2.desc with
         Tconstr (p, tl, abbrev) ->
           forget_abbrev abbrev p;
-          let t2'' = expand_head_unif env t2 in
+          let t2'' = expand_head_unif !env t2 in
           if not (closed_parameterized_type tl t2'') then
             link_type (repr t2) (repr t2')
       | _ ->
@@ -1835,7 +1950,7 @@ and unify_row env row1 row2 =
     if row1.row_fixed then rm1 else
     if row2.row_fixed then rm2 else
     newgenvar ()
-  in update_level env (min rm1.level rm2.level) more;
+  in update_level !env (min rm1.level rm2.level) more;
   let fixed = row1.row_fixed || row2.row_fixed
   and closed = row1.row_closed || row2.row_closed in
   let keep switch =
@@ -1882,7 +1997,7 @@ and unify_row env row1 row2 =
       unify env rm row0.row_more
     else
       let ty = newty2 generic_level (Tvariant {row0 with row_fields = rest}) in
-      update_level env rm.level ty;
+      update_level !env rm.level ty;
       link_type rm ty
   in
   let md1 = rm1.desc and md2 = rm2.desc in
@@ -1904,7 +2019,7 @@ and unify_row_field env fixed1 fixed2 more l f1 f2 =
   let f1 = row_field_repr f1 and f2 = row_field_repr f2 in
   if f1 == f2 then () else
   match f1, f2 with
-    Rpresent(Some t1), Rpresent(Some t2) -> unify env t1 t2
+    Rpresent(Some t1), Rpresent(Some t2) -> unify  env t1 t2
   | Rpresent None, Rpresent None -> ()
   | Reither(c1, tl1, m1, e1), Reither(c2, tl2, m2, e2) ->
       if e1 == e2 then () else
@@ -1925,7 +2040,7 @@ and unify_row_field env fixed1 fixed2 more l f1 f2 =
       in
       let tl2' = remq tl2 tl1 and tl1' = remq tl1 tl2 in
       (* Is this handling of levels really principal? *)
-      List.iter (update_level env (repr more).level) (tl1' @ tl2');
+      List.iter (update_level !env (repr more).level) (tl1' @ tl2');
       let e = ref None in
       let f1' = Reither(c1 || c2, tl1', m1 || m2, e)
       and f2' = Reither(c1 || c2, tl2', m1 || m2, e) in
@@ -1950,14 +2065,31 @@ and unify_row_field env fixed1 fixed2 more l f1 f2 =
 ;;
 
 
+let bare_tunivar x = (* GAH: ask garrigue about this. is it correct *)
+    match (repr x).desc with
+    | Tunivar -> true
+    | _ -> false
+
+let bare_tvar x = (* GAH: ask garrigue about this. is it correct *)
+    match (repr x).desc with
+    | Tvar -> true
+    | _ -> false
+
+      
+
 let unify env ty1 ty2 =
   try
-    uni_equalities := TypeSetPair.empty;
+    unify env ty1 ty2
+  with Unify trace ->
+    raise (Unify (expand_trace !env trace))
+
+let unify_gadt (env:Env.t ref) ty1 ty2 =
+  try
+    pattern_unification:=true;
     unify env ty1 ty2;
-    uni_equalities := TypeSetPair.empty;
+    pattern_unification:=false;
   with Unify trace ->
-    uni_equalities := TypeSetPair.empty;
-    raise (Unify (expand_trace env trace))
+    raise (Unify (expand_trace !env trace))
 
 
 let unify_var env t1 t2 =
@@ -1973,7 +2105,7 @@ let unify_var env t1 t2 =
         raise (Unify (expand_trace env ((t1,t2)::trace)))
       end
   | _ ->
-      unify env t1 t2
+      unify (ref env) t1 t2
 
 let _ = unify' := unify_var
 
@@ -1983,7 +2115,11 @@ let unify_pairs env ty1 ty2 pairs =
 
 let unify env ty1 ty2 =
   univar_pairs := [];
-  unify env ty1 ty2
+  unify (ref env) ty1 ty2
+
+let unify_gadt env ty1 ty2 = 
+  univar_pairs := [];
+  unify_gadt env ty1 ty2
 
 
 (**** Special cases of unification ****)
@@ -3205,7 +3341,7 @@ let subtype env ty1 ty2 =
   function () ->
     List.iter
       (function (trace0, t1, t2, pairs) ->
-         try unify_pairs env t1 t2 pairs with Unify trace ->
+         try unify_pairs (ref env) t1 t2 pairs with Unify trace ->
            raise (Subtype (expand_trace env (List.rev trace0),
                            List.tl (List.tl trace))))
       (List.rev cstrs)
diff --git a/typing/ctype.mli b/typing/ctype.mli
index 108b251a1..1213dc25f 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -148,6 +148,8 @@ val set_free_univars: Btype.TypeSet.t -> 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
+        (* 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
            is a variable. *)
@@ -250,7 +252,11 @@ val arity: type_expr -> int
 
 val collapse_conj_params: Env.t -> type_expr list -> unit
         (* Collapse conjunctive types in class parameters *)
-val reset_local_unifier: unit -> unit
-val get_local_unifier: unit -> (type_expr * type_expr) list
 val set_unification_type : [`Pattern | `Expression] -> unit
 val get_unification_type : unit -> [`Pattern | `Expression] 
+val bare_tunivar : type_expr -> bool
+val bare_tvar : type_expr -> bool
+
+val set_gadt_pattern_level : unit -> unit
+val get_gadt_pattern_level : unit -> int
+
diff --git a/typing/datarepr.ml b/typing/datarepr.ml
index 2482059c5..1f4f05230 100644
--- a/typing/datarepr.ml
+++ b/typing/datarepr.ml
@@ -19,18 +19,53 @@ open Misc
 open Asttypes
 open Types
 
+module Duplicated_code = (* GAH: causes a stack overflow when encountering recursive type *) 
+struct
+  let rec free_vars ty =
+    let ret = ref [] in
+    let rec loop ty = 
+      let ty = Btype.repr ty in
+      if ty.level >= Btype.lowest_level then begin
+	ty.level <- Btype.pivot_level - ty.level;
+	match ty.desc with
+	| Tvar ->
+            ret := ty :: !ret
+	| _ ->
+	    Btype.iter_type_expr loop ty
+      end
+    in
+    loop ty;
+    Btype.unmark_type ty;
+    !ret
+end
+
+
+let constructor_descrs_called = ref 0
+
 let constructor_descrs ty_res cstrs priv =
   let num_consts = ref 0 and num_nonconsts = ref 0 in
   List.iter
     (function (name, [],_) -> incr num_consts
             | (name, _,_)  -> incr num_nonconsts)
     cstrs;
+  let all_ty_res = 
+    List.map
+      (fun (_, _,x) ->  x)
+      cstrs
+  in
   let rec describe_constructors idx_const idx_nonconst = function
       [] -> []
     | (name, ty_args, ty_res_opt) :: rem ->
 	let ty_res = 
 	  match ty_res_opt with
-	  | Some ty_res -> ty_res
+	  | Some ty_res' -> 
+	      (match ty_res.desc, ty_res'.desc with
+	      | Tconstr (p,_,_), Tconstr(p',_,_) ->
+		  if not (Path.same p p') then 
+		    failwith "the return type of a generalized constructor has incorrect type" 
+		  else
+		    ty_res'
+	      | _ -> fatal_error "return type must be a Tconstr")
 	  | None -> ty_res
 	in
         let (tag, descr_rem) =
@@ -39,25 +74,34 @@ let constructor_descrs ty_res cstrs priv =
                    describe_constructors (idx_const+1) idx_nonconst rem)
           | _  -> (Cstr_block idx_nonconst,
                    describe_constructors idx_const (idx_nonconst+1) rem) in
-(*	let existentials = 
+	let existentials = 
 	    match ty_res_opt with
 	    | None -> []
 	    | Some type_ret ->
-		let res_vars = List.fold_right Btype.TypeSet.add (free_vars type_ret) Btype.TypeSet.empty in
-		let other_types
-*)
-
+		let res_vars = List.fold_right Btype.TypeSet.add (Duplicated_code.free_vars type_ret) Btype.TypeSet.empty in
+		let arg_vars = 
+		  List.fold_left 
+		    (fun s list -> List.fold_right Btype.TypeSet.add list s)
+		    Btype.TypeSet.empty 
+		    (List.map Duplicated_code.free_vars ty_args)
+		in
+		Btype.TypeSet.elements (Btype.TypeSet.diff arg_vars res_vars)
+	in
+	incr constructor_descrs_called;
         let cstr =
           { cstr_res = ty_res;    
-	    cstr_existentials = [] ; (* GAH: HOW DO I GET THE EXISTENTIALS OF A TYPE?? *)
+	    cstr_existentials = existentials ; (* GAH: HOW DO I GET THE EXISTENTIALS OF A TYPE?? *)
             cstr_args = ty_args;
             cstr_arity = List.length ty_args;
             cstr_tag = tag;
             cstr_consts = !num_consts;
             cstr_nonconsts = !num_nonconsts;
+	    cstr_all_ty_res = all_ty_res;
             cstr_private = priv } in
         (name, cstr) :: descr_rem in
-  describe_constructors 0 0 cstrs
+  describe_constructors 0 0 cstrs 
+
+
 
 let exception_descr path_exc decl =
   { cstr_res = Predef.type_exn;
@@ -67,6 +111,7 @@ let exception_descr path_exc decl =
     cstr_tag = Cstr_exception path_exc;
     cstr_consts = -1;
     cstr_nonconsts = -1;
+    cstr_all_ty_res = [];
     cstr_private = Public }
 
 let none = {desc = Ttuple []; level = -1; id = -1}
diff --git a/typing/env.ml b/typing/env.ml
index 391a363f4..ef898cbea 100644
--- a/typing/env.ml
+++ b/typing/env.ml
@@ -21,6 +21,7 @@ open Longident
 open Path
 open Types
 
+let store_type_called = ref 0
 
 type error =
     Not_an_interface of string
@@ -451,12 +452,13 @@ let rec scrape_modtype mty env =
   | _ -> mty
 
 (* Compute constructor descriptions *)
-
 let constructors_of_type ty_path decl =
   let handle_variants cstrs = 
-      Datarepr.constructor_descrs
+      let ret = Datarepr.constructor_descrs
         (Btype.newgenty (Tconstr(ty_path, decl.type_params, ref Mnil)))
         cstrs decl.type_private
+      in
+      ret
   in
   match decl.type_kind with
   | Type_variant cstrs -> 
diff --git a/typing/parmatch.ml b/typing/parmatch.ml
index 266d42795..9cafac4a4 100644
--- a/typing/parmatch.ml
+++ b/typing/parmatch.ml
@@ -259,6 +259,10 @@ and pretty_lvals lbls ppf = function
 let top_pretty ppf v =
   fprintf ppf "@[%a@]@?" pretty_val v
 
+let pretty_pat_now p =
+  top_pretty Format.str_formatter p ;
+  prerr_endline (Format.flush_str_formatter ())
+
 
 let prerr_pat v =
   top_pretty str_formatter v ;
@@ -618,11 +622,33 @@ let row_of_pat pat =
   not.
 *)
 
+let initial_env = ref Env.empty
+
+let unifiable t t' = 
+  let snap = Btype.snapshot () in
+  try
+    Ctype.unify_gadt (ref !initial_env) t t'; (* GAH: ask garrigue: unify in which environment??? *)
+    Btype.backtrack snap;
+    true
+  with
+    _ -> 
+      Btype.backtrack snap;
+      false
+
 let full_match closing env =  match env with
 | ({pat_desc = Tpat_construct ({cstr_tag=Cstr_exception _},_)},_)::_ ->
     false
-| ({pat_desc = Tpat_construct(c,_)},_) :: _ ->
-    List.length env = c.cstr_consts + c.cstr_nonconsts
+| ({pat_desc = Tpat_construct(c,_);pat_type=typ},_) :: _ -> 
+
+    let all_ty_res = c.cstr_all_ty_res in 
+    let possibles = ref 0 in
+    List.iter
+      (function 
+	| None -> incr possibles
+	| Some t ->
+	    if unifiable typ t then incr possibles)
+      all_ty_res;
+    List.length env = !possibles (*c.cstr_consts + c.cstr_nonconsts*)
 | ({pat_desc = Tpat_variant _} as p,_) :: _ ->
     let fields =
       List.map
@@ -711,12 +737,16 @@ let rec pat_of_constrs ex_pat = function
         (pat_of_constr ex_pat cstr,
          pat_of_constrs ex_pat rem, None)}
 
+
+
 (* Sends back a pattern that complements constructor tags all_tag *)
-let complete_constrs p all_tags = match p.pat_desc with
+let complete_constrs p all_tags  = 
+  let ty = p.pat_type in 
+  match p.pat_desc with
 | Tpat_construct (c,_) ->
     begin try
       let not_tags = complete_tags  c.cstr_consts c.cstr_nonconsts all_tags in
-      List.map
+      map_filter
         (fun tag ->
           let _,targs,ret_type_opt = get_constr tag p.pat_type p.pat_env in (* GAH: is this correct? don't forget the existentials! *)
 	  let ret_type = 
@@ -724,18 +754,22 @@ let complete_constrs p all_tags = match p.pat_desc with
 	    | None -> c.cstr_res
 	    | Some ret_type -> ret_type
 	  in
-          {c with
-	   cstr_res = ret_type ;
-	   cstr_tag = tag ;
-	   cstr_args = targs ;
-	     cstr_arity = List.length targs})
+	  if not (unifiable ty ret_type) then 
+	    None
+	  else
+	    Some
+              {c with
+	       cstr_res = ret_type ;
+	       cstr_tag = tag ;
+	       cstr_args = targs ;
+	       cstr_arity = List.length targs})
         not_tags
     with
-| Datarepr.Constr_not_found ->
-    fatal_error "Parmatch.complete_constr: constr_not_found"
+    | Datarepr.Constr_not_found ->
+	fatal_error "Parmatch.complete_constr: constr_not_found"
     end
 | _ -> fatal_error "Parmatch.complete_constr"
-
+      
 
 (* Auxiliary for build_other *)
 
@@ -752,7 +786,8 @@ let build_other_constant proj make first next p env =
   in the first column of env
 *)
 
-let build_other ext env =  match env with
+let build_other ext env =  
+match env with
 | ({pat_desc = Tpat_construct ({cstr_tag=Cstr_exception _} as c,_)},_)
   ::_ ->
     make_pat
@@ -771,7 +806,9 @@ let build_other ext env =  match env with
           | {pat_desc = Tpat_construct (c,_)} -> c.cstr_tag
           | _ -> fatal_error "Parmatch.get_tag" in
         let all_tags =  List.map (fun (p,_) -> get_tag p) env in
-        pat_of_constrs p (complete_constrs p all_tags)
+	let cnstrs  = complete_constrs p all_tags in
+        let ret = pat_of_constrs p cnstrs in 
+	ret
     end
 | ({pat_desc = Tpat_variant (_,_,r)} as p,_) :: _ ->
     let tags =
@@ -951,29 +988,53 @@ let rec try_many f = function
       | r -> r
       end
 
-let rec exhaust ext pss n = match pss with
+(*let pretty_pss pss = 
+  let print_lst ppf lst = 
+    fprintf ppf "{";
+    List.iter
+      (top_pretty ppf)
+      lst;
+    fprintf ppf "}";
+  in
+  let print_lstlst ppf lstlst = 
+    fprintf ppf "[";
+    List.iter
+      (print_lst ppf)
+      lstlst;
+    fprintf ppf "]"
+  in
+  Format.fprintf Format.str_formatter "[%a]%!"
+    print_lstlst pss;
+  print_endline (Format.flush_str_formatter ())*)
+
+
+
+let rec exhaust ext pss n  = 
+  match pss with
 | []    ->  Rsome (omegas n)
 | []::_ ->  Rnone
-| pss   ->
-    let q0 = discr_pat omega pss in
+| pss   -> 
+    let q0  = discr_pat omega pss in
     begin match filter_all q0 pss with
           (* first column of pss is made of variables only *)
-    | [] ->
+    | [] -> 
         begin match exhaust ext (filter_extra pss) (n-1) with
         | Rsome r -> Rsome (q0::r)
         | r -> r
       end
-    | constrs ->
+    | constrs -> 
         let try_non_omega (p,pss) =
           if is_absent_pat p then
             Rnone
           else
-            match
-              exhaust
-                ext pss (List.length (simple_match_args p omega) + n - 1)
-            with
-            | Rsome r -> Rsome (set_args p r)
-            | r       -> r in
+	    begin
+              match
+		exhaust
+                  ext pss (List.length (simple_match_args p omega) + n - 1)
+              with
+              | Rsome r -> Rsome (set_args p r)
+              | r       -> r end in
+	    
         if
           full_match false constrs && not (should_extend ext constrs)
         then
@@ -987,6 +1048,7 @@ let rec exhaust ext pss n = match pss with
              * D exhaustive => pss exhaustive
              * D non-exhaustive => we have a non-filtered value
           *)
+	  
           let r =  exhaust ext (filter_extra pss) (n-1) in
           match r with
           | Rnone -> Rnone
@@ -1064,6 +1126,9 @@ let pretty_pat p =
   top_pretty Format.str_formatter p ;
   prerr_string (Format.flush_str_formatter ())
 
+
+
+
 type matrix = pattern list list
 
 let pretty_line ps =
@@ -1316,6 +1381,7 @@ and every_both pss qs q1 q2 =
 
 
 (* le_pat p q  means, forall V,  V matches q implies V matches p *)
+(* GAH: ask garrigue: does le mean "less than or equal" ? *)
 let rec le_pat p q =
   match (p.pat_desc, q.pat_desc) with
   | (Tpat_var _|Tpat_any),_ -> true
@@ -1450,7 +1516,7 @@ let rec initial_matrix = function
   | (pat, act) :: rem ->
       if has_guard act
       then
-        initial_matrix rem
+        initial_matrix rem 
       else
         [pat] :: initial_matrix rem
 
@@ -1535,6 +1601,7 @@ let do_check_partial loc casel pss = match pss with
           Then match MUST be considered non-exhaustive,
           otherwise compilation of PM is broken.
           *)
+    (* GAH: ask garrigue: what's PM? *)
     begin match casel with
     | [] -> ()
     | _  -> Location.prerr_warning loc Warnings.All_clauses_guarded
@@ -1646,7 +1713,8 @@ let do_check_fragile loc casel pss =
    on exhaustive matches only.
 *)
 
-let check_partial loc casel =
+let check_partial  loc casel env  =
+  initial_env := env; (* GAH : make this more functional *)
   if Warnings.is_active (Warnings.Partial_match "") then begin
     let pss = initial_matrix casel in
     let pss = get_mins le_pats pss in
diff --git a/typing/parmatch.mli b/typing/parmatch.mli
index 7ef6a8308..5bae2fa37 100644
--- a/typing/parmatch.mli
+++ b/typing/parmatch.mli
@@ -51,7 +51,7 @@ val complete_constrs :
     pattern -> constructor_tag list -> constructor_description  list
 
 val pressure_variants: Env.t -> pattern list -> unit
-val check_partial: Location.t -> (pattern * expression) list -> partial
+val check_partial: Location.t -> (pattern * expression) list -> Env.t -> partial
 val check_unused: Env.t -> (pattern * expression) list -> unit
 
 (* Irrefutability tests *)
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index de093cfc5..d7c12fe93 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -809,12 +809,14 @@ and class_expr cl_num val_env met_env scl =
         | _ -> true
       in
       let partial =
-        Parmatch.check_partial pat.pat_loc
+        Parmatch.check_partial pat.pat_loc 
           [pat, (* Dummy expression *)
            {exp_desc = Texp_constant (Asttypes.Const_int 1);
             exp_loc = Location.none;
             exp_type = Ctype.none;
-            exp_env = Env.empty }] in
+            exp_env = Env.empty }] 
+	  val_env (* GAH : whoa, I don't know what val_env is, and quite frankly I'm scared. Ask garrigue *)
+      in
       Ctype.raise_nongen_level ();
       let cl = class_expr cl_num val_env' met_env scl' in
       Ctype.end_def ();
diff --git a/typing/typecore.ml b/typing/typecore.ml
index a5452661e..942d50231 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -25,6 +25,8 @@ open Ctype
 type error =
     Polymorphic_label of Longident.t
   | Constructor_arity_mismatch of Longident.t * int * int
+  | Constructor_inhabit_tunivar of type_expr * Longident.t
+  | Constant_inhabit_tunivar of type_expr
   | Label_mismatch of Longident.t * (type_expr * type_expr) list
   | Pattern_type_clash of (type_expr * type_expr) list
   | Multiply_bound_variable of string
@@ -70,12 +72,7 @@ let type_module =
 let type_open =
   ref (fun _ -> assert false)
 
-(*let print_local_unifier ?(s="") () = 
-  Format.fprintf Format.std_formatter "%s local_unifier:\n[%a]\n%!" s
-    (fun ppf lst -> List.iter  (fun (t,t') -> Format.fprintf ppf "%a = %a;" Printtyp.raw_type_expr  t Printtyp.raw_type_expr t') lst)
-    (get_local_unifier ())
-;;
-*)
+
 
 (* Forward declaration, to be filled in by Typeclass.class_structure *)
 let type_object =
@@ -147,15 +144,41 @@ let rec extract_label_names sexp env ty  =
 
 (* Typing of patterns *)
 
+
+let unify_pat_types loc env ty ty' = 
+  try
+    unify env ty ty'
+  with
+    Unify trace ->
+      raise(Error(loc, Pattern_type_clash(trace)))
+  | Tags(l1,l2) ->
+      raise(Typetexp.Error(loc, Typetexp.Variant_tags (l1, l2)))
+
+
+let unify_pat_types_gadt loc env ty ty' = 
+  try
+    unify_gadt env ty ty'
+  with
+    Unify trace ->
+      raise(Error(loc, Pattern_type_clash(trace)))
+  | Tags(l1,l2) ->
+      raise(Typetexp.Error(loc, Typetexp.Variant_tags (l1, l2)))
+
+
 (* Creating new conjunctive types is not allowed when typing patterns *)
 let unify_pat env pat expected_ty  = 
-  try
+  unify_pat_types pat.pat_loc env pat.pat_type expected_ty
+
+(*  try
     unify env pat.pat_type expected_ty
   with
     Unify trace ->
       raise(Error(pat.pat_loc, Pattern_type_clash(trace)))
   | Tags(l1,l2) ->
-      raise(Typetexp.Error(pat.pat_loc, Typetexp.Variant_tags (l1, l2)))
+      raise(Typetexp.Error(pat.pat_loc, Typetexp.Variant_tags (l1, l2)))*)
+
+
+
 
 (* make all Reither present in open variants *)
 let finalize_variant pat  = 
@@ -397,7 +420,7 @@ let check_recordpat_labels loc lbl_pat_list closed  =
 
 (* Typing of patterns *)
 
-let rec type_pat env sp expected_ty  = 
+let rec type_pat (env:Env.t ref) sp expected_ty  = 
   let loc = sp.ppat_loc in
   match sp.ppat_desc with
   |Ppat_any -> 
@@ -405,20 +428,20 @@ let rec type_pat env sp expected_ty  =
         pat_desc = Tpat_any;
         pat_loc = loc;
         pat_type = expected_ty;
-        pat_env = env }
-  |Ppat_var name -> 
+        pat_env = !env }
+  | Ppat_var name -> 
       let ty = newvar() in
       let id = enter_variable loc name ty in (* GAH : what does this do? *)
-      unify env ty expected_ty;
+      unify_pat_types loc !env expected_ty ty;
       rp {
         pat_desc = Tpat_var id;
         pat_loc = loc;
         pat_type = ty;
-        pat_env = env }
+        pat_env = !env }
   | Ppat_constraint({ppat_desc=Ppat_var name; ppat_loc=loc},
                     ({ptyp_desc=Ptyp_poly _} as sty)) ->
       (* explicitly polymorphic type *)
-      let ty, force = Typetexp.transl_simple_type_delayed env sty in
+      let ty, force = Typetexp.transl_simple_type_delayed !env sty in
       pattern_force := force :: !pattern_force;
       begin match ty.desc with
       |Tpoly (body, tyl) -> 
@@ -430,13 +453,13 @@ let rec type_pat env sp expected_ty  =
           rp { pat_desc = Tpat_var id;
                pat_loc = loc;
                pat_type = ty;
-               pat_env = env }
+               pat_env = !env }
       | _ -> assert false
       end
   |Ppat_alias(sq, name) -> 
       let q = type_pat env sq expected_ty in (* GAH: no idea *)
       begin_def ();
-      let ty_var = build_as_type env q in
+      let ty_var = build_as_type !env q in
       end_def ();
       generalize ty_var;
       let id = enter_variable loc name ty_var in
@@ -444,26 +467,34 @@ let rec type_pat env sp expected_ty  =
         pat_desc = Tpat_alias(q, id);
         pat_loc = loc;
         pat_type = q.pat_type;
-        pat_env = env }
+        pat_env = !env }
   |Ppat_constant cst -> 
-      (* GAH: dunno what to do here *)
-      unify env expected_ty (type_constant cst);
+      if bare_tunivar expected_ty then 	
+	raise (Error(loc,Constant_inhabit_tunivar(expected_ty)));
+      unify_pat_types loc !env expected_ty (type_constant cst);
       rp {
         pat_desc = Tpat_constant cst;
         pat_loc = loc;
         pat_type = expected_ty; (*type_constant cst;*)
-        pat_env = env }
+        pat_env = !env }
   |Ppat_tuple spl -> 
       let spl_ann = List.map (fun p -> (p,newvar ())) spl in 
       let pl = List.map (fun (p,t) -> type_pat env p t) spl_ann in
-      unify env expected_ty (newty (Ttuple(List.map snd spl_ann)));
+      unify_pat_types loc !env expected_ty (newty (Ttuple(List.map snd spl_ann)));
       rp {
         pat_desc = Tpat_tuple pl;
         pat_loc = loc;
         pat_type = expected_ty;
-        pat_env = env }
+        pat_env = !env }
   |Ppat_construct(lid, sarg, explicit_arity) -> 
-      let constr = Typetexp.find_constructor env loc lid in
+
+      
+      
+      
+      
+      if bare_tunivar expected_ty then 	
+	raise (Error(loc,Constructor_inhabit_tunivar(expected_ty,lid )));
+      let constr = Typetexp.find_constructor !env loc lid in
       let sargs =
         match sarg with
           None -> []
@@ -479,13 +510,13 @@ let rec type_pat env sp expected_ty  =
         raise(Error(loc, Constructor_arity_mismatch(lid,
                                      constr.cstr_arity, List.length sargs)));
       let (ty_args, ty_res) = instance_constructor constr in
-      unify env expected_ty ty_res;
+      unify_pat_types_gadt loc env expected_ty ty_res;
       let args: Typedtree.pattern list = List.map2 (fun p t -> type_pat env p t) sargs ty_args in (* GAH : might be wrong *)
       rp {
         pat_desc = Tpat_construct(constr, args);
         pat_loc = loc;
-        pat_type = ty_res;
-        pat_env = env }
+        pat_type = expected_ty;
+        pat_env = !env }
   |Ppat_variant(l, sarg) -> 
       let arg = may_map (fun p -> type_pat env p (newvar())) sarg in (* GAH: this is certainly false *)
       let arg_type = match arg with None -> [] | Some arg -> [arg.pat_type]  in
@@ -499,17 +530,17 @@ let rec type_pat env sp expected_ty  =
       rp {
         pat_desc = Tpat_variant(l, arg, ref {row with row_more = newvar()});
         pat_loc = loc;
-        pat_type = newty (Tvariant row);
-        pat_env = env }
+        pat_type = newty (Tvariant row); (* GAH : should probably expected_ty *)
+        pat_env = !env }
   |Ppat_record(lid_sp_list, closed) -> 
       let ty = expected_ty in
       let type_label_pat (lid, sarg) =
-        let label = Typetexp.find_label env loc lid in
+        let label = Typetexp.find_label !env loc lid in
         begin_def ();
         let (vars, ty_arg, ty_res) = instance_label false label in
         if vars = [] then end_def ();
         begin try
-          unify env ty_res ty
+          unify_pat_types loc !env ty ty_res 
         with Unify trace ->
           raise(Error(loc, Label_mismatch(lid, trace)))
         end;
@@ -519,7 +550,7 @@ let rec type_pat env sp expected_ty  =
           generalize ty_arg;
           List.iter generalize vars;
           let instantiated tv  = 
-            let tv = expand_head env tv in
+            let tv = expand_head !env tv in
             tv.desc <> Tvar || tv.level <> generic_level in
           if List.exists instantiated vars then
             raise (Error(loc, Polymorphic_label lid))
@@ -532,52 +563,49 @@ let rec type_pat env sp expected_ty  =
         pat_desc = Tpat_record lbl_pat_list;
         pat_loc = loc;
         pat_type = ty;
-        pat_env = env }
+        pat_env = !env }
   |Ppat_array spl -> 
       let ty_elt = newvar() in
-      unify env expected_ty (instance (Predef.type_array ty_elt));
+      unify_pat_types loc !env expected_ty (instance (Predef.type_array ty_elt));
       let spl_ann = List.map (fun p -> (p,newvar())) spl in 
       let pl = List.map (fun (p,t) -> type_pat env p ty_elt) spl_ann in
       rp {
         pat_desc = Tpat_array pl;
         pat_loc = loc;
         pat_type = expected_ty;
-        pat_env = env }
-  |Ppat_or(sp1, sp2) -> 
+        pat_env = !env }
+  |Ppat_or(sp1, sp2) ->  (* GAH: what do we do for or patterns? ask garrigue if this is ok *)
       let initial_pattern_variables = !pattern_variables in
-      let nv = newvar() in 
-      let p1 = type_pat env sp1 nv in (* GAH: so wrong *)
+      let p1 = type_pat env sp1 expected_ty in 
       let p1_variables = !pattern_variables in
       pattern_variables := initial_pattern_variables ;
-      let p2 = type_pat env sp2 nv in (* GAH: again, so wrong *)
+      let p2 = type_pat env sp2 expected_ty in 
       let p2_variables = !pattern_variables in
-      unify_pat env p2 p1.pat_type;
       let alpha_env =
-        enter_orpat_variables loc env p1_variables p2_variables in
+        enter_orpat_variables loc !env p1_variables p2_variables in
       pattern_variables := p1_variables ;
       rp {
         pat_desc = Tpat_or(p1, alpha_pat alpha_env p2, None);
         pat_loc = loc;
-        pat_type = p1.pat_type;
-        pat_env = env }
+        pat_type = expected_ty;
+        pat_env = !env }
   |Ppat_lazy sp1 -> 
       let nv = newvar () in 
-      unify env expected_ty (instance (Predef.type_lazy_t nv));
+      unify_pat_types loc !env expected_ty (instance (Predef.type_lazy_t nv));
       let p1 = type_pat env sp1 nv in
       rp {
         pat_desc = Tpat_lazy p1;
         pat_loc = loc;
         pat_type = expected_ty;
-        pat_env = env }
+        pat_env = !env }
   |Ppat_constraint(sp, sty) -> 
-      let nv = newvar () in 
-      let p = type_pat env sp nv in (* GAH: so wrong *)
-      let ty, force = Typetexp.transl_simple_type_delayed env sty in
-      unify_pat env p ty;
+      let ty, force = Typetexp.transl_simple_type_delayed !env sty in
+      unify_pat_types loc !env expected_ty ty;
+      let p = type_pat env sp expected_ty in (* GAH: so wrong *)
       pattern_force := force :: !pattern_force;
-      p
+      p (* GAH: this pattern will have the wrong location! *)
   |Ppat_type lid -> 
-      build_or_pat env loc lid
+      build_or_pat !env loc lid
 
 let get_ref r  = 
   let v = !r in r := []; v
@@ -594,34 +622,32 @@ let add_pattern_variables env  =
 
 let type_pattern env spat scope expected_ty  = 
   reset_pattern scope;
-      
-  let pat = type_pat env spat expected_ty in
-      
-  let new_env = add_pattern_variables env in
-      
+  set_gadt_pattern_level ();
+  let new_env = ref env in 
+  let pat = type_pat new_env spat expected_ty in
+  let new_env = add_pattern_variables !new_env in
   (pat, new_env, get_ref pattern_force)
 
 
 let type_pattern_list env spatl scope expected_tys  = 
-  
-  reset_local_unifier ();
-  set_unification_type `Pattern;
-  try_finally
-    (fun () -> 
-      reset_pattern scope;
-
-      let patl = List.map2 (fun p t -> type_pat env p t) spatl expected_tys in
-      let new_env = add_pattern_variables env in
-      
-      (patl, new_env, get_ref pattern_force))
-    (fun () -> 
-      set_unification_type `Expression)  
+  reset_pattern scope;
+  set_gadt_pattern_level ();
+  let new_env = ref env in 
+  let patl = 
+    List.map2 
+      (fun p t -> 
+	type_pat new_env p t)
+      spatl expected_tys 
+  in
+  let new_env = add_pattern_variables !new_env in
+  (patl, new_env, get_ref pattern_force)
+
+
 
 let type_class_arg_pattern cl_num val_env met_env l spat  = 
-  
   reset_pattern None;
   let nv = newvar () in 
-  let pat = type_pat val_env spat nv in
+  let pat = type_pat (ref val_env) spat nv in
   
   if has_variants pat then begin
     Parmatch.pressure_variants val_env [pat];
@@ -652,13 +678,13 @@ let type_self_pattern cl_num privty val_env met_env par_env spat  =
   in
   reset_pattern None;
   let nv = newvar() in 
-  let pat = type_pat val_env spat nv in (* GAH: so wrong *)
+  let pat = type_pat (ref val_env) spat nv in (* GAH: so wrong *)
   List.iter (fun f -> f()) (get_ref pattern_force);
   let meths = ref Meths.empty in
   let vars = ref Vars.empty in
   let pv = !pattern_variables in
   pattern_variables := [];
-  let (val_env, met_env, par_env) =
+  let ((val_env:Env.t), met_env, par_env) =
     List.fold_right
       (fun (id, ty, _loc) (val_env, met_env, par_env) ->
          (Env.add_value id {val_type = ty; val_kind = Val_unbound} val_env,
@@ -1154,9 +1180,8 @@ let rec type_exp env sexp  =
       let arg = type_exp env sarg in
       let ty_res = newvar() in
       let cases, partial =
-        type_cases_gadt env arg.exp_type ty_res (Some loc) caselist
+        type_cases env arg.exp_type ty_res (Some loc) caselist
       in
-      Format.fprintf Format.std_formatter " match type : %a\n%! " Printtyp.raw_type_expr  ty_res ;
       re {
         exp_desc = Texp_match(arg, cases, partial);
         exp_loc = loc;
@@ -2098,7 +2123,7 @@ and type_expect ?in_function env sexp ty_expected =
         else ty_arg
       in
       let cases, partial =
-        type_cases_gadt ~in_function:(loc_fun,ty_fun) env ty_arg ty_res
+        type_cases ~in_function:(loc_fun,ty_fun) env ty_arg ty_res
           (Some loc) caselist in
       let not_function ty  = 
         let ls, tvar = list_labels env ty in
@@ -2155,7 +2180,7 @@ and type_expect ?in_function env sexp ty_expected =
   | Pexp_match(sarg, caselist) -> (* GAH : check with garrigue that this is ok *)
       let arg = type_exp env sarg in
       let cases, partial =
-        type_cases_gadt env arg.exp_type ty_expected (Some loc) caselist
+        type_cases env arg.exp_type ty_expected (Some loc) caselist
       in
       re {
         exp_desc = Texp_match(arg, cases, partial);
@@ -2197,14 +2222,9 @@ and type_statement env sexp  =
 
 (* Typing of match cases *)
 
-and type_pattern_gadt env spat scope ty_arg  =  
-  reset_local_unifier ();
-  set_unification_type `Pattern;
-  try_finally
-    (fun () -> type_pattern env spat scope ty_arg )
-    (fun () -> set_unification_type `Expression)  
 
-and type_cases ?in_function ?(gadt=false) env ty_arg ty_res partial_loc caselist =
+
+and type_cases ?in_function env ty_arg ty_res partial_loc caselist =
 (*  let ty_arg' = newvar () in *) (* GAH : must ask garrigue about this *)
   let pattern_force = ref [] in
   let pat_env_list = 
@@ -2215,13 +2235,10 @@ and type_cases ?in_function ?(gadt=false) env ty_arg ty_res partial_loc caselist
         let scope = Some (Annot.Idef loc) in
 	
         let (pat, ext_env, force) = 
-	  if gadt then 
-	    type_pattern_gadt env spat scope ty_arg
-	  else
-	    type_pattern env spat scope ty_arg
+	  type_pattern env spat scope ty_arg
 	in
-	let local_unifier = get_local_unifier () in
-        pattern_force := force @ !pattern_force;
+
+
         let pat =
           if !Clflags.principal then begin
             end_def ();
@@ -2231,12 +2248,12 @@ and type_cases ?in_function ?(gadt=false) env ty_arg ty_res partial_loc caselist
         in
 	
 (*        unify_pat env pat ty_arg'; (* GAH: probably wrong. what in the blazes does ty_arg' do?? *)*)
-        (pat, ext_env,local_unifier))
+        (pat, ext_env))
       caselist in
   (* Check for polymorphic variants to close *)
 
-  let fst3 (a,b,c) = a in 
-  let patl = List.map fst3 pat_env_list in
+
+  let patl = List.map fst pat_env_list in
   
   if List.exists has_variants patl then begin
     Parmatch.pressure_variants env patl;
@@ -2244,37 +2261,35 @@ and type_cases ?in_function ?(gadt=false) env ty_arg ty_res partial_loc caselist
   end;
   (* `Contaminating' unifications start here *)
   List.iter (fun f -> f()) !pattern_force;
-  
+
 (*  begin match pat_env_list with [] -> ()
   | (pat, _) :: _ -> unify_pat env pat ty_arg (* GAH: probably incorrect; check with garrigue. if we readd this code then it doesn't work *)
   end;*)
   let in_function = if List.length caselist = 1 then in_function else None in
   let cases =
     List.map2
-      (fun (pat, ext_env,local_unifier) (spat, sexp) ->
-	List.iter (fun (t,t') -> t.desc <- Tlink t') local_unifier;
-	try_finally
-	  (fun () ->
-            let exp = type_expect ?in_function ext_env sexp ty_res in
-            (pat, exp))
-	  (fun () -> List.iter (fun (t,_) -> t.desc <- Tunivar) local_unifier))
+      (fun (pat, ext_env) (spat, sexp) ->
+	let ty_res = expand_head ext_env ty_res in
+        let exp = type_expect ?in_function ext_env sexp ty_res in
+	(pat, exp))
       pat_env_list caselist
   in
   let partial =
     match partial_loc with
     | None -> Partial
-    | Some partial_loc -> Parmatch.check_partial partial_loc cases
+    | Some partial_loc ->  
+	let r = Parmatch.check_partial partial_loc cases env in 
+	r
   in
   add_delayed_check (fun () -> Parmatch.check_unused env cases);
   cases, partial
 
-and type_cases_gadt ?in_function env ty_arg ty_res partial_loc caselist =
-	type_cases ?in_function ~gadt:true env ty_arg ty_res partial_loc caselist
+(*and type_cases_gadt ?in_function env ty_arg ty_res partial_loc caselist =
+	type_cases ?in_function env ty_arg ty_res partial_loc caselist*)
   
 (* Typing of let bindings *)
 
 and type_let env rec_flag spat_sexp_list scope   = 
-  
   begin_def();
   if !Clflags.principal then begin_def ();
   let spatl = List.map (fun (spat, sexp) -> spat) spat_sexp_list in
@@ -2328,7 +2343,7 @@ and type_let env rec_flag spat_sexp_list scope   =
         | _ -> type_expect exp_env sexp pat.pat_type)
       spat_sexp_list pat_list in
   List.iter2
-    (fun pat exp -> ignore(Parmatch.check_partial pat.pat_loc [pat, exp]))
+    (fun pat exp -> ignore(Parmatch.check_partial pat.pat_loc [pat, exp] env))
     pat_list exp_list;
   end_def();
   List.iter2
@@ -2371,7 +2386,15 @@ let report_error ppf  =  function
       fprintf ppf
        "@[The constructor %a@ expects %i argument(s),@ \
         but is applied here to %i argument(s)@]"
-       longident lid expected provided
+       longident lid expected provided 
+  | Constructor_inhabit_tunivar(t,lid) ->
+      fprintf ppf
+       "The constructor %a does not inhabit the univarsal type %a"
+       longident lid type_scheme t
+  | Constant_inhabit_tunivar t ->
+      fprintf ppf
+       "This constant does not inhabit the type universal type %a"
+       type_scheme t
   | Label_mismatch(lid, trace) ->
       report_unification_error ppf trace
         (function ppf ->
diff --git a/typing/typecore.mli b/typing/typecore.mli
index 3fb90ff34..5114d3429 100644
--- a/typing/typecore.mli
+++ b/typing/typecore.mli
@@ -65,6 +65,8 @@ val self_coercion : (Path.t * Location.t list ref) list ref
 type error =
     Polymorphic_label of Longident.t
   | Constructor_arity_mismatch of Longident.t * int * int
+  | Constructor_inhabit_tunivar of type_expr * Longident.t
+  | Constant_inhabit_tunivar of type_expr
   | Label_mismatch of Longident.t * (type_expr * type_expr) list
   | Pattern_type_clash of (type_expr * type_expr) list
   | Multiply_bound_variable of string
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index 5c8ed6f58..6aa8932f8 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -121,6 +121,9 @@ module StringSet =
     let compare = compare
   end)
 
+
+
+
 let transl_declaration env (name, sdecl) id =
   (* Bind type parameters *)
   reset_type_variables();
@@ -150,21 +153,32 @@ let transl_declaration env (name, sdecl) id =
                   raise(Error(sdecl.ptype_loc, Duplicate_constructor name));
                 all_constrs := StringSet.add name !all_constrs)
               cstrs;
+
             if List.length (List.filter (fun (_, args, _, _) -> args <> []) cstrs) (* GAH: MIGHT BE WRONG *)
                > (Config.max_tag + 1) then
               raise(Error(sdecl.ptype_loc, Too_many_constructors));
-	    if List.for_all (fun (_,_,x,_) -> match x with Some _ -> false | None -> true) cstrs then
+(*	    if List.for_all (fun (_,_,x,_) -> match x with Some _ -> false | None -> true) cstrs then
             Type_variant
               (List.map
                  (fun (name, args,_, loc) ->
                     (name, List.map (transl_simple_type env true) args))
               cstrs)
-	    else
+	    else*)
+
+	    let ret = 
 	      Type_generalized_variant
 		(List.map
                    (fun (name, args,ret_type_opt, loc) ->
-                     (name, List.map (transl_simple_type env false) args,may_map (transl_simple_type env false) ret_type_opt)) (* GAH: calling transl_simple_type with fixed=false, ask garrigue if this is ok *)
+		     let gadt = 
+		       match ret_type_opt with
+		       | None -> None
+		       | Some _ -> Some (ref [])
+		     in
+                     (name, List.map (transl_simple_type ~gadt env false) args,may_map (transl_simple_type ~gadt env false) ret_type_opt)) (* GAH: calling transl_simple_type with fixed=false, ask garrigue if this is ok *)
 		   cstrs)
+	    in
+	    ret
+	    
         | Ptype_record lbls ->
             let all_labels = ref StringSet.empty in
             List.iter
@@ -196,6 +210,9 @@ let transl_declaration env (name, sdecl) id =
       type_variance = List.map (fun _ -> true, true, true) params;
     } in
 
+
+
+
   (* Check constraints *)
   List.iter
     (fun (ty, ty', loc) ->
@@ -247,6 +264,7 @@ module TypeSet =
     end)
 
 let rec check_constraints_rec env loc visited ty =
+
   let ty = Ctype.repr ty in
   if TypeSet.mem ty !visited then () else begin
   visited := TypeSet.add ty !visited;
@@ -279,17 +297,19 @@ let check_constraints env (_, sdecl) (_, decl) =
       List.iter
         (fun (name, tyl,ret_type_opt) -> (* GAH: again, no idea *)
           let styl,sret_type_opt =
-            try let (_,sty,ret_type_opt (* added by me *) ,_) = List.find (fun (n,_,_,_) -> n = name)  pl in sty,ret_type_opt (* GAH: lord, I have no idea what this is about *)
+            try let (_,sty,sret_type_opt (* added by me *) ,_) = List.find (fun (n,_,_,_) -> n = name)  pl in sty,sret_type_opt (* GAH: lord, I have no idea what this is about *)
             with Not_found -> assert false in
           List.iter2
             (fun sty ty ->
               check_constraints_rec env sty.ptyp_loc visited ty)
             styl tyl;
+
+	  (* GAH : ask garrigue how to do the following: *)
 	  match sret_type_opt,ret_type_opt with
 	  | Some sr,Some r ->
 	      check_constraints_rec env sr.ptyp_loc visited r
 	  | _ ->
-	      ())
+	      () )
 	l
   in
   begin match decl.type_kind with
@@ -526,7 +546,23 @@ let compute_variance_decl env check decl (required, loc) =
   let tvl1 = List.map make_variance fvl in
   let tvl2 = List.map make_variance fvl in
   let tvl = tvl0 @ tvl1 in
-  begin match decl.type_kind with
+  let is_gadt = 
+    match decl.type_kind with
+    | Type_generalized_variant tll -> (* GAH: what in the blazes *)
+	let ret = ref false in 
+	List.iter
+          (function 
+	    | (_,_,Some _) ->
+		ret:=true;
+	    | _ -> ())
+	  tll;
+	!ret
+    | _ -> false
+  in
+  if is_gadt then
+    List.map (fun _ -> (true,true,true)) params
+  else
+  begin begin match decl.type_kind with
   | Type_abstract ->
       begin match decl.type_manifest with
         None -> assert false
@@ -544,8 +580,8 @@ let compute_variance_decl env check decl (required, loc) =
 	  | None ->
               List.iter (compute_variance env tvl true false false) tl
 	  | Some ret_type ->
-	      List.iter (compute_variance env tvl true true true) tl) (* GAH: variance calculation, is this right *)
-        tll
+	      fatal_error "gadt not properly handled")
+        tll;
   | Type_record (ftl, _) ->
       List.iter
         (fun (_, mut, ty) ->
@@ -566,7 +602,7 @@ let compute_variance_decl env check decl (required, loc) =
     tvl0 required;
   List.iter2
     (fun (ty, c1, n1, t1) (_, c2, n2, t2) ->
-      if !c1 && not !c2 || !n1 && not !n2
+      if !c1 && not !c2 || !n1 && not !n2  
       (* || !t1 && not !t2 && decl.type_kind = Type_abstract *)
       then raise (Error(loc,
                         if not (!c2 || !n2) then Unbound_type_var (ty, decl)
@@ -582,6 +618,7 @@ let compute_variance_decl env check decl (required, loc) =
       let ct = if decl.type_kind = Type_abstract then ct else cn in
       (!co, !cn, !ct))
     tvl0 required
+  end
 
 let is_sharp id =
   let s = Ident.name id in
@@ -613,6 +650,7 @@ let rec compute_variance_fixpoint env decls required variances =
       (fun (id, decl) req -> if not (is_sharp id) then
         ignore (compute_variance_decl new_env true decl req))
       new_decls required;
+
     new_decls, new_env
   end
 
@@ -680,6 +718,8 @@ let name_recursion sdecl id decl =
     else decl
   | _ -> decl
 
+
+
 (* Translate a set of mutually recursive type declarations *)
 let transl_type_decl env name_sdecl_list =
   (* Add dummy types for fixed rows *)
@@ -753,6 +793,7 @@ let transl_type_decl env name_sdecl_list =
     List.map (fun (_, sdecl) -> sdecl.ptype_variance, sdecl.ptype_loc)
       name_sdecl_list
   in
+
   let final_decls, final_env =
     compute_variance_fixpoint env decls required (List.map init_variance decls)
   in
@@ -818,7 +859,7 @@ let transl_with_constraint env id row_path sdecl =
          Ctype.unify env (transl_simple_type env false ty)
                          (transl_simple_type env false ty')
        with Ctype.Unify tr ->
-         raise(Error(loc, Unconsistent_constraint tr)))
+         raise(Error(loc, Unconsistent_constraint tr))) (* GAH : Unconsistent is not a word *)
     sdecl.ptype_cstrs;
   let no_row = not (is_fixed_type sdecl) in
   let decl =
diff --git a/typing/types.ml b/typing/types.ml
index d1ef644a3..f9f011092 100644
--- a/typing/types.ml
+++ b/typing/types.ml
@@ -105,14 +105,15 @@ and value_kind =
 (* Constructor descriptions *)
 
 type constructor_description =
-  { cstr_res: type_expr;                (* Type of the result *)
-    cstr_existentials: type_expr list;  (* list of existentials *)
-    cstr_args: type_expr list;          (* Type of the arguments *)
-    cstr_arity: int;                    (* Number of arguments *)
-    cstr_tag: constructor_tag;          (* Tag for heap blocks *)
-    cstr_consts: int;                   (* Number of constant constructors *)
-    cstr_nonconsts: int;                (* Number of non-const constructors *)
-    cstr_private: private_flag }        (* Read-only constructor? *)
+  { cstr_res: type_expr;                       (* Type of the result *)
+    cstr_existentials: type_expr list;         (* list of existentials *)
+    cstr_args: type_expr list;                 (* Type of the arguments *)
+    cstr_arity: int;                           (* Number of arguments *)
+    cstr_tag: constructor_tag;                 (* Tag for heap blocks *)
+    cstr_consts: int;                          (* Number of constant constructors *) (* GAH: ask garrigue: why is this field here?? is it the same for each constructor?*)
+    cstr_nonconsts: int;                       (* Number of non-const constructors *)
+    cstr_all_ty_res: type_expr option list;    (* The return type of all the constructors of the type *)
+    cstr_private: private_flag }               (* Read-only constructor? *)
 
 and constructor_tag =
     Cstr_constant of int                (* Constant constructor (an int) *)
diff --git a/typing/types.mli b/typing/types.mli
index 962dfd02e..ef0b3460e 100644
--- a/typing/types.mli
+++ b/typing/types.mli
@@ -102,14 +102,15 @@ and value_kind =
 (* Constructor descriptions *)
 
 type constructor_description =
-  { cstr_res: type_expr;                (* Type of the result *)
-    cstr_existentials: type_expr list;  (* list of existentials *)
-    cstr_args: type_expr list;          (* Type of the arguments *)
-    cstr_arity: int;                    (* Number of arguments *)
-    cstr_tag: constructor_tag;          (* Tag for heap blocks *)
-    cstr_consts: int;                   (* Number of constant constructors *)
-    cstr_nonconsts: int;                (* Number of non-const constructors *)
-    cstr_private: private_flag }        (* Read-only constructor? *)
+  { cstr_res: type_expr;                       (* Type of the result *)
+    cstr_existentials: type_expr list;         (* list of existentials *)
+    cstr_args: type_expr list;                 (* Type of the arguments *)
+    cstr_arity: int;                           (* Number of arguments *)
+    cstr_tag: constructor_tag;                 (* Tag for heap blocks *)
+    cstr_consts: int;                          (* Number of constant constructors *) (* GAH: ask garrigue: why is this field here?? is it the same for each constructor?*)
+    cstr_nonconsts: int;                       (* Number of non-const constructors *)
+    cstr_all_ty_res: type_expr option list;    (* The return type of all the constructors of the type *)
+    cstr_private: private_flag }               (* Read-only constructor? *)
 
 and constructor_tag =
     Cstr_constant of int                (* Constant constructor (an int) *)
diff --git a/typing/typetexp.ml b/typing/typetexp.ml
index 838719b7c..d395a793e 100644
--- a/typing/typetexp.ml
+++ b/typing/typetexp.ml
@@ -158,6 +158,7 @@ let type_variable loc name =
   try
     Tbl.find name !type_variables
   with Not_found ->
+    print_endline "raising type_variable";
     raise(Error(loc, Unbound_type_variable ("'" ^ name)))
 
 let wrap_method ty =
@@ -174,9 +175,11 @@ let rec swap_list = function
 
 type policy = Fixed | Extensible | Univars
 
+let gadt_map = ref None
+
 let rec transl_type env policy styp =
   match styp.ptyp_desc with
-    Ptyp_any ->
+  | Ptyp_any ->
       if policy = Univars then new_pre_univar () else
       if policy = Fixed then
         raise (Error (styp.ptyp_loc, Unbound_type_variable "_"))
@@ -184,15 +187,25 @@ let rec transl_type env policy styp =
   | Ptyp_var name ->
       if name <> "" && name.[0] = '_' then
         raise (Error (styp.ptyp_loc, Invalid_variable_name ("'" ^ name)));
-      begin try
-        instance (List.assoc name !univars)
-      with Not_found -> try
-        instance (fst(Tbl.find name !used_variables))
-      with Not_found ->
-        let v =
-          if policy = Univars then new_pre_univar () else newvar () in
-        used_variables := Tbl.add name (v, styp.ptyp_loc) !used_variables;
-        v
+      begin 
+	match !gadt_map with
+	| Some lst ->
+	    begin try
+	      List.assoc name !lst
+	    with Not_found ->
+	      let ret = newvar () in 
+	      lst := (name,ret) :: !lst;
+	      ret end
+	| None ->
+	    try
+              instance (List.assoc name !univars)
+	    with Not_found -> try
+              instance (fst(Tbl.find name !used_variables))
+	    with Not_found ->
+              let v =
+		if policy = Univars then new_pre_univar () else newvar () in
+              used_variables := Tbl.add name (v, styp.ptyp_loc) !used_variables;
+              v
       end
   | Ptyp_arrow(l, st1, st2) ->
       let ty1 = transl_type env policy st1 in
@@ -215,14 +228,15 @@ let rec transl_type env policy styp =
       in
       List.iter2
         (fun (sty, ty) ty' ->
+	  Format.fprintf Format.std_formatter " ty: %a \n ty': %a \n\n%! " Printtyp.raw_type_expr ty Printtyp.raw_type_expr ty' ;
            try unify_param env ty' ty with Unify trace ->
-             raise (Error(sty.ptyp_loc, Type_mismatch (swap_list trace))))
+             (print_endline "mismatch from trans_type ";raise (Error(sty.ptyp_loc, Type_mismatch (swap_list trace)))))
         (List.combine stl args) params;
       let constr = newconstr path args in
       begin try
         Ctype.enforce_constraints env constr
       with Unify trace ->
-        raise (Error(styp.ptyp_loc, Type_mismatch trace))
+        (print_endline "another mismatch from trans_type"; raise (Error(styp.ptyp_loc, Type_mismatch trace)))
       end;
       constr
   | Ptyp_object fields ->
@@ -264,7 +278,7 @@ let rec transl_type env policy styp =
       List.iter2
         (fun (sty, ty) ty' ->
            try unify_var env ty' ty with Unify trace ->
-             raise (Error(sty.ptyp_loc, Type_mismatch (swap_list trace))))
+             (print_endline "yet another";raise (Error(sty.ptyp_loc, Type_mismatch (swap_list trace)))))
         (List.combine stl args) params;
       let ty =
         try Ctype.expand_head env (newconstr path args)
@@ -310,9 +324,18 @@ let rec transl_type env policy styp =
       begin
         try
           let t =
-            try List.assoc alias !univars
-            with Not_found ->
-              instance (fst(Tbl.find alias !used_variables))
+	    try List.assoc alias !univars 
+	    with Not_found ->		
+	      match !gadt_map with
+	      | Some lst ->
+		  begin try
+		    List.assoc alias !lst
+		  with Not_found ->
+		    let ret = newvar () in 
+		    lst := (alias,ret) :: !lst;
+		    ret end
+	      | None ->
+		  instance (fst(Tbl.find alias !used_variables))
           in
           let ty = transl_type env policy st in
           begin try unify_var env t ty with Unify trace ->
@@ -475,6 +498,10 @@ and transl_fields env policy seen =
         newty (Tfield (s, Fpresent, ty1, ty2))
 
 
+
+
+    
+
 (* Make the rows "fixed" in this type, to make universal check easier *)
 let rec make_fixed_univars ty =
   let ty = repr ty in
@@ -503,6 +530,7 @@ let make_fixed_univars ty =
 let create_package_mty = create_package_mty false
 
 let globalize_used_variables env fixed =
+  Printf.printf "globalize_used_variables, fixed: %B\n%!" fixed;
   let r = ref [] in
   Tbl.iter
     (fun name (ty, loc) ->
@@ -513,7 +541,10 @@ let globalize_used_variables env fixed =
         r := (loc, v,  Tbl.find name !type_variables) :: !r
       with Not_found ->
         if fixed && (repr ty).desc = Tvar then
-          raise(Error(loc, Unbound_type_variable ("'"^name)));
+	  begin
+	    print_endline "raising";
+            raise(Error(loc, Unbound_type_variable ("'"^name)))
+	  end;
         let v2 = new_global_var () in
         r := (loc, v, v2) :: !r;
         type_variables := Tbl.add name v2 !type_variables)
@@ -526,15 +557,21 @@ let globalize_used_variables env fixed =
           raise (Error(loc, Type_mismatch trace)))
       !r
 
-let transl_simple_type env fixed styp =
-  univars := []; used_variables := Tbl.empty;
+let transl_simple_type env fixed ?(gadt=None) styp = (* GAH : ask garrigue about this *)
+  (match gadt with
+  | Some _ -> print_endline "doing gadt thing"
+  | None ->
+      print_endline "not doing gadt thing");
+  univars := []; used_variables := Tbl.empty;gadt_map:=gadt;
+  Format.fprintf Format.std_formatter " styp = %a\n%! " Printast.print_core_type styp ;
   let typ = transl_type env (if fixed then Fixed else Extensible) styp in
+  Format.fprintf Format.std_formatter " typ: %a \n\n%! " Printtyp.raw_type_expr typ;
   globalize_used_variables env fixed ();
   make_fixed_univars typ;
   typ
 
 let transl_simple_type_univars env styp =
-  univars := []; used_variables := Tbl.empty; pre_univars := [];
+  univars := []; used_variables := Tbl.empty; pre_univars := [];gadt_map:=None;
   begin_def ();
   let typ = transl_type env Univars styp in
   (* Only keep already global variables in used_variables *)
@@ -560,13 +597,13 @@ let transl_simple_type_univars env styp =
   instance (Btype.newgenty (Tpoly (typ, univs)))
 
 let transl_simple_type_delayed env styp =
-  univars := []; used_variables := Tbl.empty;
+  univars := []; used_variables := Tbl.empty;gadt_map:=None;
   let typ = transl_type env Extensible styp in
   make_fixed_univars typ;
   (typ, globalize_used_variables env false)
 
 let transl_type_scheme env styp =
-  reset_type_variables();
+  reset_type_variables();gadt_map:=None;
   begin_def();
   let typ = transl_simple_type env false styp in
   end_def();
diff --git a/typing/typetexp.mli b/typing/typetexp.mli
index ec9042ce8..e83f42453 100644
--- a/typing/typetexp.mli
+++ b/typing/typetexp.mli
@@ -17,7 +17,7 @@
 open Format;;
 
 val transl_simple_type:
-        Env.t -> bool -> Parsetree.core_type -> Types.type_expr
+        Env.t -> bool -> ?gadt:(string*Types.type_expr) list ref option -> Parsetree.core_type -> Types.type_expr
 val transl_simple_type_univars:
         Env.t -> Parsetree.core_type -> Types.type_expr
 val transl_simple_type_delayed:
diff --git a/utils/misc.ml b/utils/misc.ml
index 68ca8e3da..784c92985 100644
--- a/utils/misc.ml
+++ b/utils/misc.ml
@@ -195,3 +195,15 @@ let rev_split_words s =
       | _ -> split2 res i (j+1)
     end
   in split1 [] 0
+
+let map_filter f  = 
+  let rec loop = 
+    function 
+      | [] -> []
+      | x :: xs ->
+	  match f x with
+	  | None -> loop xs
+	  | Some y -> 
+	      y :: loop xs
+  in
+  loop
diff --git a/utils/misc.mli b/utils/misc.mli
index 87f74e257..da0a36c5e 100644
--- a/utils/misc.mli
+++ b/utils/misc.mli
@@ -23,6 +23,8 @@ val map_end: ('a -> 'b) -> 'a list -> 'b list -> 'b list
         (* [map_end f l t] is [map f l @ t], just more efficient. *)
 val map_left_right: ('a -> 'b) -> 'a list -> 'b list
         (* Like [List.map], with guaranteed left-to-right evaluation order *)
+val map_filter: ('a -> 'b option) -> 'a list -> 'b list
+        (* Mapping and filtering at the same time *)
 val for_all2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
         (* Same as [List.for_all] but for a binary predicate.
            In addition, this [for_all2] never fails: given two lists