existentials are now treated correctly in patterns

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

3 files changed, 207 insertions, 17 deletions

diff --git a/typing/ctype.ml b/typing/ctype.ml
index 333e350c7..17e084542 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -10,6 +10,180 @@
 (*                                                                     *)
 (***********************************************************************)
 
+
+module Printtyp_ = 
+struct
+
+open Misc
+open Format
+open Longident
+open Path
+open Asttypes
+open Types
+open Btype
+open Outcometree
+
+(* Print a long identifier *)
+
+let rec longident ppf = function
+  | Lident s -> fprintf ppf "%s" s
+  | Ldot(p, s) -> fprintf ppf "%a.%s" longident p s
+  | Lapply(p1, p2) -> fprintf ppf "%a(%a)" longident p1 longident p2
+
+(* Print an identifier *)
+
+let unique_names = ref Ident.empty
+
+let ident_name id =
+  try Ident.find_same id !unique_names with Not_found -> Ident.name id
+
+let add_unique id =
+  try ignore (Ident.find_same id !unique_names)
+  with Not_found ->
+    unique_names := Ident.add id (Ident.unique_toplevel_name id) !unique_names
+
+let ident ppf id = fprintf ppf "%s" (ident_name id)
+
+(* Print a path *)
+
+let ident_pervasive = Ident.create_persistent "Pervasives"
+
+let rec tree_of_path = function
+  | Pident id ->
+      Oide_ident (ident_name id)
+  | Pdot(Pident id, s, pos) when Ident.same id ident_pervasive ->
+      Oide_ident s
+  | Pdot(p, s, pos) ->
+      Oide_dot (tree_of_path p, s)
+  | Papply(p1, p2) ->
+      Oide_apply (tree_of_path p1, tree_of_path p2)
+
+let rec path ppf = function
+  | Pident id ->
+      ident ppf id
+  | Pdot(Pident id, s, pos) when Ident.same id ident_pervasive ->
+      fprintf ppf "%s" s
+  | Pdot(p, s, pos) ->
+      fprintf ppf "%a.%s" path p s
+  | Papply(p1, p2) ->
+      fprintf ppf "%a(%a)" path p1 path p2
+
+(* Print a recursive annotation *)
+
+let tree_of_rec = function
+  | Trec_not -> Orec_not
+  | Trec_first -> Orec_first
+  | Trec_next -> Orec_next
+
+(* Print a raw type expression, with sharing *)
+
+let raw_list pr ppf = function
+    [] -> fprintf ppf "[]"
+  | a :: l ->
+      fprintf ppf "@[<1>[%a%t]@]" pr a
+        (fun ppf -> List.iter (fun x -> fprintf ppf ";@,%a" pr x) l)
+
+let rec safe_kind_repr v = function
+    Fvar {contents=Some k}  ->
+      if List.memq k v then "Fvar loop" else
+      safe_kind_repr (k::v) k
+  | Fvar _ -> "Fvar None"
+  | Fpresent -> "Fpresent"
+  | Fabsent -> "Fabsent"
+
+let rec safe_commu_repr v = function
+    Cok -> "Cok"
+  | Cunknown -> "Cunknown"
+  | Clink r ->
+      if List.memq r v then "Clink loop" else
+      safe_commu_repr (r::v) !r
+
+let rec safe_repr v = function
+    {desc = Tlink t} when not (List.memq t v) ->
+      safe_repr (t::v) t
+  | t -> t
+
+let rec list_of_memo = function
+    Mnil -> []
+  | Mcons (priv, p, t1, t2, rem) -> p :: list_of_memo rem
+  | Mlink rem -> list_of_memo !rem
+
+let visited = ref []
+let rec raw_type ppf ty =
+  let ty = safe_repr [] ty in
+  if List.memq ty !visited then fprintf ppf "{id=%d}" ty.id else begin
+    visited := ty :: !visited;
+    fprintf ppf "@[<1>{id=%d;level=%d;desc=@,%a}@]" ty.id ty.level
+      raw_type_desc ty.desc
+  end
+and raw_type_list tl = raw_list raw_type tl
+and raw_type_desc ppf = function
+    Tvar -> fprintf ppf "Tvar"
+  | Tarrow(l,t1,t2,c) ->
+      fprintf ppf "@[<hov1>Tarrow(%s,@,%a,@,%a,@,%s)@]"
+        l raw_type t1 raw_type t2
+        (safe_commu_repr [] c)
+  | Ttuple tl ->
+      fprintf ppf "@[<1>Ttuple@,%a@]" raw_type_list tl
+  | Tconstr (p, tl, abbrev) ->
+      fprintf ppf "@[<hov1>Tconstr(@,%a,@,%a,@,%a)@]" path p
+        raw_type_list tl
+        (raw_list path) (list_of_memo !abbrev)
+  | Tobject (t, nm) ->
+      fprintf ppf "@[<hov1>Tobject(@,%a,@,@[<1>ref%t@])@]" raw_type t
+        (fun ppf ->
+          match !nm with None -> fprintf ppf " None"
+          | Some(p,tl) ->
+              fprintf ppf "(Some(@,%a,@,%a))" path p raw_type_list tl)
+  | Tfield (f, k, t1, t2) ->
+      fprintf ppf "@[<hov1>Tfield(@,%s,@,%s,@,%a,@;<0 -1>%a)@]" f
+        (safe_kind_repr [] k)
+        raw_type t1 raw_type t2
+  | Tnil -> fprintf ppf "Tnil"
+  | Tlink t -> fprintf ppf "@[<1>Tlink@,%a@]" raw_type t
+  | Tsubst t -> fprintf ppf "@[<1>Tsubst@,%a@]" raw_type t
+  | Tunivar -> fprintf ppf "Tunivar"
+  | Tpoly (t, tl) ->
+      fprintf ppf "@[<hov1>Tpoly(@,%a,@,%a)@]"
+        raw_type t
+        raw_type_list tl
+  | Tvariant row ->
+      fprintf ppf
+        "@[<hov1>{@[%s@,%a;@]@ @[%s@,%a;@]@ %s%b;@ %s%b;@ @[<1>%s%t@]}@]"
+        "row_fields="
+        (raw_list (fun ppf (l, f) ->
+          fprintf ppf "@[%s,@ %a@]" l raw_field f))
+        row.row_fields
+        "row_more=" raw_type row.row_more
+        "row_closed=" row.row_closed
+        "row_fixed=" row.row_fixed
+        "row_name="
+        (fun ppf ->
+          match row.row_name with None -> fprintf ppf "None"
+          | Some(p,tl) ->
+              fprintf ppf "Some(@,%a,@,%a)" path p raw_type_list tl)
+  | Tpackage (p, _, tl) ->
+      fprintf ppf "@[<hov1>Tpackage(@,%a@,%a)@]" path p
+        raw_type_list tl
+
+and raw_field ppf = function
+    Rpresent None -> fprintf ppf "Rpresent None"
+  | Rpresent (Some t) -> fprintf ppf "@[<1>Rpresent(Some@,%a)@]" raw_type t
+  | Reither (c,tl,m,e) ->
+      fprintf ppf "@[<hov1>Reither(%b,@,%a,@,%b,@,@[<1>ref%t@])@]" c
+        raw_type_list tl m
+        (fun ppf ->
+          match !e with None -> fprintf ppf " None"
+          | Some f -> fprintf ppf "@,@[<1>(%a)@]" raw_field f)
+  | Rabsent -> fprintf ppf "Rabsent"
+
+let raw_type_expr ppf t =
+  visited := [];
+  raw_type ppf t;
+  visited := []
+end
+
+
 (* $Id$ *)
 
 (* Operations on core types *)
@@ -866,9 +1040,38 @@ let instance_list schl =
   cleanup_types ();
   tyl
 
-let instance_constructor cstr =
+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 instance_constructor ?(in_pattern=None) cstr = (* GAH : how the blazes does this work?? *)
   let ty_res = copy cstr.cstr_res in
   let ty_args = List.map copy cstr.cstr_args in
+  begin match in_pattern with
+  | None -> ()
+  | Some env ->
+      let existentials = List.map copy cstr.cstr_existentials in
+      let process existential = 
+	let decl = {
+          type_params = [];
+          type_arity = 0;
+          type_kind = Type_abstract;
+          type_private = Public;
+          type_manifest = None;
+          type_variance = [];
+	}
+	in
+	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 generic_level (Tconstr (Path.Pident id,[],ref Mnil)) in (* GAH : ask garrigue, what in the world is an abbrev_memo ?? *)
+	link_type existential to_unify 
+      in
+      List.iter process existentials end;
   cleanup_types ();
   (ty_args, ty_res)
 
@@ -1568,12 +1771,6 @@ let get_unification_type () =
   | true -> `Pattern
   | false -> `Expression
 
-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 = 
diff --git a/typing/ctype.mli b/typing/ctype.mli
index a126c27fa..eef51699a 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -108,7 +108,7 @@ val instance: type_expr -> type_expr
 val instance_list: type_expr list -> type_expr list
         (* Take an instance of a list of type schemes *)
 val instance_constructor:
-        constructor_description -> type_expr list * type_expr
+        ?in_pattern:Env.t ref option -> constructor_description -> type_expr list * type_expr
         (* Same, for a constructor *)
 val instance_parameterized_type:
         type_expr list -> type_expr -> type_expr list * type_expr
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 522da3956..bc2e51a90 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -492,22 +492,15 @@ let rec type_pat (env:Env.t ref) sp expected_ty  =
         pat_type = expected_ty;
         pat_env = !env }
   |Ppat_construct(lid, sarg, explicit_arity) -> 
-
-
-(*      if bare_tunivar expected_ty then 	
-	raise (Error(loc,Constructor_inhabit_tunivar(expected_ty,lid ))); (* GAH : this code is wrong, must change *)*)
       let constr = Typetexp.find_constructor !env loc lid in
       let _ = (* GAH : there must be an easier way to do this, ask garrigue *)
 	let (_, ty_res) = instance_constructor constr in
 	match (repr ty_res).desc with
 	| Tconstr(p,args,m) ->
-	    ty_res.desc <- Tconstr(p,List.map (fun _ -> newvar ()) args,m);
+	    ty_res.desc <- Tconstr(p,List.map (fun _ -> newvar ()) args,m); (* GAH: ask garrigue if this is the best way to only unify the head *)
 	    unify_pat_types loc !env expected_ty ty_res
 	| _ -> fatal_error "constructor type does not have correct description" 
       in
-      
-	
-
       let sargs =
         match sarg with
           None -> []
@@ -522,7 +515,7 @@ let rec type_pat (env:Env.t ref) sp expected_ty  =
       if List.length sargs <> constr.cstr_arity then
         raise(Error(loc, Constructor_arity_mismatch(lid,
                                      constr.cstr_arity, List.length sargs)));
-      let (ty_args, ty_res) = instance_constructor constr in
+      let (ty_args, ty_res) = instance_constructor ~in_pattern:(Some env) constr in
       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 {