From 277b1d86649d8d5f627bb40323904fb99cd2f595 Mon Sep 17 00:00:00 2001 From: Ryan Tjoa Date: Tue, 31 Dec 2024 15:21:37 -0500 Subject: [PATCH] Future proof for unrepresentable fields and refactor --- .../typing-layouts-products/recursive.ml | 4 +- typing/typedecl.ml | 134 +++++++++++------- 2 files changed, 81 insertions(+), 57 deletions(-) diff --git a/testsuite/tests/typing-layouts-products/recursive.ml b/testsuite/tests/typing-layouts-products/recursive.ml index fce70f09c6..48b586ec09 100644 --- a/testsuite/tests/typing-layouts-products/recursive.ml +++ b/testsuite/tests/typing-layouts-products/recursive.ml @@ -280,9 +280,7 @@ Error: The definition of "Bad_rec1.t" is recursive without boxing: "#(Bad_rec1.s * Bad_rec1.s)" contains "Bad_rec1.s", "Bad_rec1.s" contains "Bad_rec2.u", "Bad_rec2.u" = "Bad_rec1.t Bad_rec2.id", - "Bad_rec1.t Bad_rec2.id" = "Bad_rec1.t", - "Bad_rec1.t" = "#(Bad_rec1.s * Bad_rec1.s)", - "#(Bad_rec1.s * Bad_rec1.s)" contains "Bad_rec1.s" + "Bad_rec1.t Bad_rec2.id" = "Bad_rec1.t" |}] (* When we allow records with elements of unrepresentable layout, this should diff --git a/typing/typedecl.ml b/typing/typedecl.ml index 97f629db63..eef45d7f62 100644 --- a/typing/typedecl.ml +++ b/typing/typedecl.ml @@ -2071,73 +2071,99 @@ let check_well_founded_decl ~abs_env env loc path decl to_check = See [typing-layouts-unboxed-records/recursive.ml]. Because [check_well_founded] already ruled out recursion through structural - types (for this check, we care about unboxed tuples and aliases), we just - look for a cycle in nominal unboxed types ([@@unboxed] types and unboxed - records), tracking the set of seen paths. + types, we just look for a cycle in nominal unboxed types ([@@unboxed] types + and unboxed records), tracking the set of seen paths. - An alternative implementation could have introduced layout variables (for - this check only), finding infinite-size types via the occurs check. Such an - implementation might be more principled, accepting finite-size recursive - types like [type t = #{ t : t }]. The current implementation gives more - informative error traces, and leaves the flexiblity to switch to a less - restrictive check in the future. + For each group of mutually recursive type declarations, we define the + following "type contains" transitive relation on type expressions: + + 1. Unboxed records and variants defined in the group contain their fields. + + If [type 'a t = #{ ...; lbl : u; ... }], + or [type 'a t = { lbl : u } [@@unboxed]], + or [type 'a t = U of u [@@unboxed]] + is in the recursive group, then ['a t] contains [u]. + + 2. Abbreviations defined in the group contain their expansions. + + If [type 'a t = u] is in the recursive group then ['a t] contains [u]. + + 3. Unboxed tuples contain their components. + + [#(u_1 * ...)] contains all [u_i]. + + 4. Types not in the group contain the parameters indicated by their layout. + + ['a t] contains ['a] if [layout_of 'a] or [any] occurs in ['a t]'s layout. + Note: We don't yet have [layout_of], so currently only consider [any]. + + If a path starting from the type expression on the LHS of a declaration + contains two types with the same head type constructor, and that repeated + type is an unboxed record or variant, then the check raises a type error. CR layouts v7.2: accept safe types that expand the same path multiple times, - e.g. [type 'a t = #{ a : 'a } and x = int t t], - either by using layouts variables or the algorithm from - "Unboxed data constructors - or, how cpp decides a halting problem." + e.g. [type 'a t = #{ a : 'a } and x = int t t], either by using layouts + variables or the algorithm from "Unboxed data constructors - or, how cpp + decides a halting problem." + See https://github.com/ocaml-flambda/flambda-backend/pull/3407. *) +type step_result = + | Contained of type_expr list + | Expanded_to of type_expr + | Is_cyclic let check_unboxed_recursion ~abs_env env loc path0 ty0 to_check = - let check_visited parents trace ty = + let contained_parameters tyl layout = + (* A type whose layout has [any] could contain all its parameters. + CR layouts v11: update this function for [layout_of] layouts. *) + let rec has_any : Jkind_types.Layout.Const.t -> bool = function + | Any -> true + | Base _ -> false + | Product l -> List.exists has_any l + in + if has_any layout then tyl else [] + in + let step_once parents ty = match get_desc ty with - | Tconstr (path, _, _) -> - if Path.Set.mem path parents then - let err = Unboxed_recursion(Path.name path0, abs_env, List.rev trace) in - raise (Error(loc, err)) - | _ -> () - in - let rec expand parents trace ty = - match Ctype.try_expand_safe_opt env ty with - | ty' -> - begin match get_desc ty with - | Tconstr (path, _, _) -> - if to_check path then - expand (Path.Set.add path parents) (Expands_to (ty, ty') :: trace) ty' + | Tconstr (path, tyl, _) -> + if to_check path then + if Path.Set.mem path parents then + Is_cyclic, parents else - parents, trace, ty - | _ -> - (* Only [Tconstr]s can be expanded *) - Misc.fatal_error "Typedecl.check_unboxed_recursion" - end - | exception Ctype.Cannot_expand -> - parents, trace, ty + let parents = Path.Set.add path parents in + match Ctype.try_expand_safe_opt env ty with + | ty' -> + Expanded_to ty', parents + | exception Ctype.Cannot_expand -> + Contained (Ctype.contained_without_boxing env ty), parents + else + begin try + (* Determine contained types by layout for decls outside of the + recursive group *) + let jkind = (Env.find_type path env).type_jkind in + let layout = Option.get (Jkind.get_layout jkind) in + Contained (contained_parameters tyl layout), parents + with Not_found | Invalid_argument _ -> + (* Because [to_check path] is false, this decl has already been + typechecked, so it's already in [env] with a constant layout. *) + Misc.fatal_error "Typedecl.check_unboxed_recursion" + end + | _ -> Contained (Ctype.contained_without_boxing env ty), parents in let rec visit parents trace ty = - (* Expand even if this type isn't part of the recursive group, because it - could be instantiated back into the group by a type parameter. *) - let parents, trace, ty = expand parents trace ty in - match get_desc ty with - | Tconstr (path, _, _) -> - (* Only visit [Tconstr]s in this recursive group of typedecls. *) - if to_check path then begin - check_visited parents trace ty; - visit_subtypes (Path.Set.add path parents) trace ty - end - | _ -> - visit_subtypes parents trace ty - and visit_subtypes parents trace ty = - List.iter (fun ty' -> - let trace = Contains (ty, ty') :: trace in - check_visited parents trace ty'; - visit parents trace ty') - (Ctype.contained_without_boxing env ty) + match step_once parents ty with + | Contained tys, parents -> + List.iter (fun ty' -> visit parents (Contains (ty, ty') :: trace) ty') tys + | Expanded_to ty', parents -> + visit parents (Expands_to(ty,ty') :: trace) ty' + | Is_cyclic, _ -> + raise (Error (loc, Unboxed_recursion (path0, abs_env, List.rev trace))) in Ctype.wrap_trace_gadt_instances env (visit Path.Set.empty []) ty0 let check_unboxed_recursion_decl ~abs_env env loc path decl to_check = let decl = Ctype.generic_instance_declaration decl in let ty = Btype.newgenty (Tconstr (path, decl.type_params, ref Mnil)) in - check_unboxed_recursion ~abs_env env loc path ty to_check + check_unboxed_recursion ~abs_env env loc (Path.name path) ty to_check (* Check for non-regular abbreviations; an abbreviation [type 'a t = ...] is non-regular if the expansion of [...] @@ -2425,13 +2451,13 @@ let transl_type_decl env rec_flag sdecl_list = (Path.Pident id) decl to_check) decls; + List.iter (fun (tdecl, _shape) -> + check_abbrev_regularity ~abs_env new_env id_loc_list to_check tdecl) tdecls; List.iter (fun (id, decl) -> check_unboxed_recursion_decl ~abs_env new_env (List.assoc id id_loc_list) (Path.Pident id) decl to_check) decls; - List.iter (fun (tdecl, _shape) -> - check_abbrev_regularity ~abs_env new_env id_loc_list to_check tdecl) tdecls; (* Now that we've ruled out ill-formed types, we can perform the delayed jkind checks *) List.iter (fun (checks,loc) ->