diff --git a/typing/ctype.ml b/typing/ctype.ml index 939dd05fe..0198d5631 100644 --- a/typing/ctype.ml +++ b/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; diff --git a/typing/ctype.mli b/typing/ctype.mli index 9af75aca0..2af650a01 100644 --- a/typing/ctype.mli +++ b/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 diff --git a/typing/parmatch.ml b/typing/parmatch.ml index e2423c8b2..227d640b5 100644 --- a/typing/parmatch.ml +++ b/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 diff --git a/typing/typecore.ml b/typing/typecore.ml index 3010c627a..364eaea35 100644 --- a/typing/typecore.ml +++ b/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;*)