diff options
| -rw-r--r-- | typing/ctype.ml | 4 | ||||
| -rw-r--r-- | typing/ctype.mli | 2 | ||||
| -rw-r--r-- | typing/mtype.ml | 24 | ||||
| -rw-r--r-- | typing/mtype.mli | 1 | ||||
| -rw-r--r-- | typing/path.ml | 6 | ||||
| -rw-r--r-- | typing/path.mli | 1 | ||||
| -rw-r--r-- | typing/typedecl.ml | 82 | ||||
| -rw-r--r-- | typing/typedecl.mli | 4 | ||||
| -rw-r--r-- | typing/typemod.ml | 15 |
9 files changed, 127 insertions, 12 deletions
diff --git a/typing/ctype.ml b/typing/ctype.ml index 9b7c4927d..afed7a70a 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -1181,11 +1181,11 @@ let rec non_recursive_abbrev env ty0 ty = iter_type_expr (non_recursive_abbrev env ty0) ty end -let correct_abbrev env ident params ty = +let correct_abbrev env path params ty = check_abbrev_env env; let ty0 = newgenvar () in visited := []; - let abbrev = Mcons (Path.Pident ident, ty0, ty0, Mnil) in + let abbrev = Mcons (path, ty0, ty0, Mnil) in simple_abbrevs := abbrev; try non_recursive_abbrev env ty0 diff --git a/typing/ctype.mli b/typing/ctype.mli index 899e7015d..766476d44 100644 --- a/typing/ctype.mli +++ b/typing/ctype.mli @@ -209,7 +209,7 @@ val nondep_class_declaration: val nondep_cltype_declaration: Env.t -> Ident.t -> cltype_declaration -> cltype_declaration (* Same for class type declarations. *) -val correct_abbrev: Env.t -> Ident.t -> type_expr list -> type_expr -> unit +val correct_abbrev: Env.t -> Path.t -> type_expr list -> type_expr -> unit val cyclic_abbrev: Env.t -> Ident.t -> type_expr -> bool val normalize_type: Env.t -> type_expr -> unit diff --git a/typing/mtype.ml b/typing/mtype.ml index 193799345..0b4805c14 100644 --- a/typing/mtype.ml +++ b/typing/mtype.ml @@ -153,3 +153,27 @@ and enrich_item env p = function | Tsig_module(id, mty) -> Tsig_module(id, enrich_modtype env (Pdot(p, Ident.name id, nopos)) mty) | item -> item + +let rec type_paths env p mty = + match scrape env mty with + Tmty_ident p -> [] + | Tmty_signature sg -> type_paths_sig env p 0 sg + | Tmty_functor(param, arg, res) -> [] + +and type_paths_sig env p pos sg = + match sg with + [] -> [] + | Tsig_value(id, decl) :: rem -> + let pos' = match decl.val_kind with Val_prim _ -> pos | _ -> pos + 1 in + type_paths_sig env p pos' rem + | Tsig_type(id, decl) :: rem -> + Pdot(p, Ident.name id, nopos) :: type_paths_sig env p pos rem + | Tsig_module(id, mty) :: rem -> + type_paths env (Pdot(p, Ident.name id, pos)) mty @ + type_paths_sig (Env.add_module id mty env) p (pos+1) rem + | Tsig_modtype(id, decl) :: rem -> + type_paths_sig (Env.add_modtype id decl env) p pos rem + | (Tsig_exception _ | Tsig_class _) :: rem -> + type_paths_sig env p (pos+1) rem + | (Tsig_cltype _) :: rem -> + type_paths_sig env p pos rem diff --git a/typing/mtype.mli b/typing/mtype.mli index 5bc63c5f5..ee720be28 100644 --- a/typing/mtype.mli +++ b/typing/mtype.mli @@ -29,3 +29,4 @@ val nondep_supertype: Env.t -> Ident.t -> module_type -> module_type Raise [Not_found] if no such type exists. *) val enrich_modtype: Env.t -> Path.t -> module_type -> module_type val enrich_typedecl: Env.t -> Path.t -> type_declaration -> type_declaration +val type_paths: Env.t -> Path.t -> module_type -> Path.t list diff --git a/typing/path.ml b/typing/path.ml index efe4a2617..88f9aa574 100644 --- a/typing/path.ml +++ b/typing/path.ml @@ -41,3 +41,9 @@ let rec name = function Pident id -> Ident.name id | Pdot(p, s, pos) -> name p ^ "." ^ s | Papply(p1, p2) -> name p1 ^ "(" ^ name p2 ^ ")" + +let rec head = function + Pident id -> id + | Pdot(p, s, pos) -> head p + | Papply(p1, p2) -> assert false + diff --git a/typing/path.mli b/typing/path.mli index 78bef3f98..96f3e9836 100644 --- a/typing/path.mli +++ b/typing/path.mli @@ -26,3 +26,4 @@ val binding_time: t -> int val nopos: int val name: t -> string +val head: t -> Ident.t diff --git a/typing/typedecl.ml b/typing/typedecl.ml index 5f79b906c..21846f450 100644 --- a/typing/typedecl.ml +++ b/typing/typedecl.ml @@ -32,7 +32,7 @@ type error = | Constraint_failed of type_expr * type_expr | Unconsistent_constraint of (type_expr * type_expr) list | Type_clash of (type_expr * type_expr) list - | Parameters_differ of type_expr * type_expr + | Parameters_differ of Path.t * type_expr * type_expr | Null_arity_external | Missing_native_external | Unbound_type_var @@ -294,9 +294,10 @@ let check_abbrev env (_, sdecl) (id, decl) = let check_recursive_abbrev env (name, sdecl) (id, decl) = match decl.type_manifest with Some ty -> - begin try Ctype.correct_abbrev env id decl.type_params ty with - Ctype.Recursive_abbrev -> - raise(Error(sdecl.ptype_loc, Recursive_abbrev name)) + begin try + Ctype.correct_abbrev env (Path.Pident id) decl.type_params ty + with Ctype.Recursive_abbrev -> + raise(Error(sdecl.ptype_loc, Recursive_abbrev name)) end | _ -> () @@ -312,7 +313,8 @@ let rec check_expansion_rec env id args loc id_check_list visited ty = | Tconstr(Path.Pident id' as path, args', _) -> if Ident.same id id' then begin if not (Ctype.equal env false args args') then - raise (Error(loc, Parameters_differ(ty, Ctype.newconstr path args))) + raise (Error(loc, + Parameters_differ(path, ty, Ctype.newconstr path args))) end else begin try let (loc, checked) = List.assoc id' id_check_list in if List.exists (Ctype.equal env false args') !checked then () else @@ -647,6 +649,70 @@ let approx_type_decl env name_sdecl_list = abstract_type_decl (List.length sdecl.ptype_params))) name_sdecl_list +(* These are variants of [check_recursive_abbrev] and [check_expansion] + above that check the well-formedness conditions on type abbreviations + defined within recursive modules. *) + +let check_recmod_typedecl env loc recmod_ids path decl = + (* recmod_ids is the list of recursively-defined module idents. + (path, decl) is the type declaration to be checked. *) + let visited = ref [] in + + let rec check_regular path args prev_exp ty = + let ty = Ctype.repr ty in + if not (List.memq ty !visited) then begin + visited := ty :: !visited; + match ty.desc with + | Tconstr(path', args', _) -> + if Path.same path path' then begin + if not (Ctype.equal env false args args') then + raise (Error(loc, + Parameters_differ(path, ty, Ctype.newconstr path args))) + end + (* Attempt to expand a type abbreviation if: + 1- it belongs to one of the recursively-defined modules + (otherwise its expansion cannot involve [path]); + 2- we haven't expanded this type constructor before + (otherwise we could loop if [path'] is itself + a non-regular abbreviation). *) + else if List.mem (Path.head path') recmod_ids + && not (List.mem path' prev_exp) then begin + try + (* Attempt expansion *) + let (params, body) = Env.find_type_expansion path' env in + let (params, body) = + Ctype.instance_parameterized_type params body in + begin + try List.iter2 (Ctype.unify env) params args' + with Ctype.Unify _ -> assert false + end; + check_regular path args (path' :: prev_exp) body + with Not_found -> () + end; + List.iter (check_regular path args prev_exp) args' + | Tpoly (ty, tl) -> + let (_, ty) = Ctype.instance_poly false tl ty in + check_regular path args prev_exp ty + | _ -> + Btype.iter_type_expr (check_regular path args prev_exp) ty + end in + + match decl.type_manifest with + None -> () + | Some body -> + (* Check that recursion is well-founded *) + begin try + Ctype.correct_abbrev env path decl.type_params body + with Ctype.Recursive_abbrev -> + raise(Error(loc, Recursive_abbrev (Path.name path))) + end; + (* Check that recursion is regular *) + if decl.type_params <> [] then begin + let (args, body) = + Ctype.instance_parameterized_type decl.type_params body in + check_regular path args [] body + end + (**** Error report ****) open Format @@ -675,12 +741,12 @@ let report_error ppf = function Printtyp.mark_loops ty'; fprintf ppf "@[<hv>Type@ %a@ should be an instance of@ %a@]" Printtyp.type_expr ty Printtyp.type_expr ty' - | Parameters_differ (ty, ty') -> + | Parameters_differ (path, ty, ty') -> Printtyp.reset_and_mark_loops ty; Printtyp.mark_loops ty'; fprintf ppf - "@[<hv>In this definition, type@ %a@ should be@ %a@]" - Printtyp.type_expr ty Printtyp.type_expr ty' + "@[<hv>In the definition of %s, type@ %a@ should be@ %a@]" + (Path.name path) Printtyp.type_expr ty Printtyp.type_expr ty' | Unconsistent_constraint trace -> fprintf ppf "The type constraints are not consistent.@."; Printtyp.report_unification_error ppf trace diff --git a/typing/typedecl.mli b/typing/typedecl.mli index b109c4854..e5e723b76 100644 --- a/typing/typedecl.mli +++ b/typing/typedecl.mli @@ -36,6 +36,8 @@ val abstract_type_decl: int -> type_declaration val approx_type_decl: Env.t -> (string * Parsetree.type_declaration) list -> (Ident.t * type_declaration) list +val check_recmod_typedecl: + Env.t -> Location.t -> Ident.t list -> Path.t -> type_declaration -> unit (* for typeclass.ml *) val compute_variance_decls: @@ -53,7 +55,7 @@ type error = | Constraint_failed of type_expr * type_expr | Unconsistent_constraint of (type_expr * type_expr) list | Type_clash of (type_expr * type_expr) list - | Parameters_differ of type_expr * type_expr + | Parameters_differ of Path.t * type_expr * type_expr | Null_arity_external | Missing_native_external | Unbound_type_var diff --git a/typing/typemod.ml b/typing/typemod.ml index 01de20a9a..7c3387951 100644 --- a/typing/typemod.ml +++ b/typing/typemod.ml @@ -179,6 +179,20 @@ let approx_modtype transl_mty init_env smty = in approx_mty init_env smty +(* Additional validity checks on type definitions arising from + recursive modules *) + +let check_recmod_typedecls env sdecls decls = + let recmod_ids = List.map fst decls in + List.iter2 + (fun (_, smty) (id, mty) -> + List.iter + (fun path -> + Typedecl.check_recmod_typedecl env smty.pmty_loc recmod_ids + path (Env.find_type path env)) + (Mtype.type_paths env (Pident id) mty)) + sdecls decls + (* Auxiliaries for checking uniqueness of names in signatures and structures *) module StringSet = Set.Make(struct type t = string let compare = compare end) @@ -341,6 +355,7 @@ and transl_recmodule_modtypes loc env sdecls = let first = transition (make_env init) init in let final_env = make_env first in let final_decl = transition final_env init in + check_recmod_typedecls final_env sdecls final_decl; (final_decl, final_env) (* Try to convert a module expression to a module path. *) |