diff options
| -rw-r--r-- | typing/ctype.ml | 72 | ||||
| -rw-r--r-- | typing/ctype.mli | 5 | ||||
| -rw-r--r-- | typing/typedecl.ml | 40 |
3 files changed, 83 insertions, 34 deletions
diff --git a/typing/ctype.ml b/typing/ctype.ml index a9d7cace2..756abff91 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -1203,38 +1203,40 @@ let rec occur_rec env visited ty0 ty = Tconstr(p, tl, abbrev) -> begin try if List.memq ty visited then raise Occur; - iter_type_expr (occur_rec env (ty::visited) ty0) ty - with Occur -> try - let ty' = try_expand_head env ty in + if not !Clflags.recursive_types then + iter_type_expr (occur_rec env (ty::visited) ty0) ty + with Occur -> + if not (generic_abbrev env p) then raise Occur else + let ty' = repr (expand_abbrev env ty) in (* Maybe we could simply make a recursive call here, but it seems it could make the occur check loop (see change in rev. 1.58) *) if ty' == ty0 || List.memq ty' visited then raise Occur; match ty'.desc with Tobject _ | Tvariant _ -> () - | _ -> iter_type_expr (occur_rec env (ty'::visited) ty0) ty' - with Cannot_expand -> - raise Occur + | _ -> + if not !Clflags.recursive_types then + iter_type_expr (occur_rec env (ty'::visited) ty0) ty' end | Tobject _ | Tvariant _ -> () | _ -> - iter_type_expr (occur_rec env visited ty0) ty + if not !Clflags.recursive_types then + iter_type_expr (occur_rec env visited ty0) ty let type_changed = ref false (* trace possible changes to the studied type *) let merge r b = if b then r := true let occur env ty0 ty = - if not !Clflags.recursive_types then - let old = !type_changed in - try - while type_changed := false; occur_rec env [] ty0 ty; !type_changed - do () (* prerr_endline "changed" *) done; - merge type_changed old - with exn -> - merge type_changed old; - raise (match exn with Occur -> Unify [] | _ -> exn) + let old = !type_changed in + try + while type_changed := false; occur_rec env [] ty0 ty; !type_changed + do () (* prerr_endline "changed" *) done; + merge type_changed old + with exn -> + merge type_changed old; + raise (match exn with Occur -> Unify [] | _ -> exn) (*****************************) @@ -2063,6 +2065,44 @@ let moregeneral env inst_nongen pat_sch subj_sch = res +(* Alternative approach: "rigidify" a type scheme, + and check validity after unification *) +(* Simpler, no? *) + +let rec rigidify_rec vars ty = + let ty = repr ty in + if ty.level >= lowest_level then begin + ty.level <- pivot_level - ty.level; + begin match ty.desc with + | Tvar -> + if not (List.memq ty !vars) then vars := ty :: !vars + | Tvariant row -> + let row = row_repr row in + let more = repr row.row_more in + if more.desc = Tvar && not row.row_fixed then + let more' = newty2 more.level Tvar in + let row' = {row with row_fixed=true; row_fields=[]; row_more=more'} + in link_type more (newty2 ty.level (Tvariant row')) + | _ -> () + end; + iter_type_expr (rigidify_rec vars) ty + end + +let rigidify ty = + let vars = ref [] in + rigidify_rec vars ty; + unmark_type ty; + !vars + +let all_distinct_vars vars = + let tyl = ref [] in + List.for_all + (fun ty -> + let ty = repr ty in + if List.memq ty !tyl then false else + (tyl := ty :: !tyl; ty.desc = Tvar)) + vars + (*********************************************) (* Equivalence between parameterized types *) (*********************************************) diff --git a/typing/ctype.mli b/typing/ctype.mli index c7c93e109..158dd2498 100644 --- a/typing/ctype.mli +++ b/typing/ctype.mli @@ -150,6 +150,11 @@ val filter_self_method: type_expr -> Ident.t * type_expr val moregeneral: Env.t -> bool -> type_expr -> type_expr -> bool (* Check if the first type scheme is more general than the second. *) +val rigidify: type_expr -> type_expr list + (* "Rigidify" a type and return its type variable *) +val all_distinct_vars: type_expr list -> bool + (* Check those type are all distinct type variables *) + type class_match_failure = CM_Virtual_class | CM_Parameter_arity_mismatch of int * int diff --git a/typing/typedecl.ml b/typing/typedecl.ml index f7278ea4a..4e9081d99 100644 --- a/typing/typedecl.ml +++ b/typing/typedecl.ml @@ -193,32 +193,36 @@ module TypeSet = let compare t1 t2 = t1.id - t2.id end) -let rec check_constraints_rec env newenv loc visited ty = +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; match ty.desc with | Tconstr (path, args, _) -> - Ctype.begin_def (); let args' = List.map (fun _ -> Ctype.newvar ()) args in let ty' = Ctype.newconstr path args' in - begin try Ctype.enforce_constraints newenv ty' + begin try Ctype.enforce_constraints env ty' with Ctype.Unify _ -> assert false | Not_found -> raise (Error(loc, Unavailable_type_constructor path)) end; - Ctype.end_def (); - Ctype.generalize ty'; - if not (List.for_all2 (Ctype.moregeneral env false) args' args) then - raise (Error(loc, Constraint_failed (ty, ty'))); - List.iter (check_constraints_rec env newenv loc visited) args + let snap = Btype.snapshot () in + let vars = Ctype.rigidify ty in + begin try + Ctype.unify env ty ty'; + if not (Ctype.all_distinct_vars vars) then raise (Ctype.Unify[]) + with Ctype.Unify _ -> + raise (Error(loc, Constraint_failed (ty, ty'))) + end; + Btype.backtrack snap; + List.iter (check_constraints_rec env loc visited) args | Tpoly (ty, tl) -> let _, ty = Ctype.instance_poly false tl ty in - check_constraints_rec env newenv loc visited ty + check_constraints_rec env loc visited ty | _ -> - Btype.iter_type_expr (check_constraints_rec env newenv loc visited) ty + Btype.iter_type_expr (check_constraints_rec env loc visited) ty end -let check_constraints env newenv (_, sdecl) (_, decl) = +let check_constraints env (_, sdecl) (_, decl) = let visited = ref TypeSet.empty in let rec check = function | Type_abstract -> () @@ -234,7 +238,7 @@ let check_constraints env newenv (_, sdecl) (_, decl) = let styl = try List.assoc name pl with Not_found -> assert false in List.iter2 (fun sty ty -> - check_constraints_rec env newenv sty.ptyp_loc visited ty) + check_constraints_rec env sty.ptyp_loc visited ty) styl tyl) l | Type_record (l, _) -> @@ -251,7 +255,7 @@ let check_constraints env newenv (_, sdecl) (_, decl) = in List.iter (fun (name, _, ty) -> - check_constraints_rec env newenv (get_loc name pl) visited ty) + check_constraints_rec env (get_loc name pl) visited ty) l | Type_private tkind -> check tkind in check decl.type_kind; @@ -261,7 +265,7 @@ let check_constraints env newenv (_, sdecl) (_, decl) = let sty = match sdecl.ptype_manifest with Some sty -> sty | _ -> assert false in - check_constraints_rec env newenv sty.ptyp_loc visited ty + check_constraints_rec env sty.ptyp_loc visited ty end (* @@ -309,8 +313,8 @@ let check_recursive_abbrev env (name, sdecl) (id, decl) = let rec check_expansion_rec env id args loc id_check_list visited ty = let ty = Ctype.repr ty in if List.memq ty visited then () else - let check_rec = - check_expansion_rec env id args loc id_check_list (ty :: visited) in + let visited = ty :: visited in + let check_rec = check_expansion_rec env id args loc id_check_list visited in match ty.desc with | Tconstr(Path.Pident id' as path, args', _) -> if Ident.same id id' then begin @@ -328,7 +332,7 @@ let rec check_expansion_rec env id args loc id_check_list visited ty = try List.iter2 (Ctype.unify env) params args' with Ctype.Unify _ -> assert false end; - check_rec body + check_expansion_rec env id args loc id_check_list visited body end with Not_found -> () end; @@ -527,7 +531,7 @@ let transl_type_decl env name_sdecl_list = (* Check re-exportation *) List.iter2 (check_abbrev newenv) name_sdecl_list decls; (* Check that constraints are enforced *) - List.iter2 (check_constraints temp_env newenv) name_sdecl_list decls; + List.iter2 (check_constraints newenv) name_sdecl_list decls; (* Check that abbreviations have same parameters *) let id_loc_list = List.map2 |