Skip to content

Commit

Permalink
Move code
Browse files Browse the repository at this point in the history
  • Loading branch information
rtjoa committed Dec 25, 2024
1 parent 099d3b5 commit 83ae0ff
Showing 1 changed file with 54 additions and 54 deletions.
108 changes: 54 additions & 54 deletions typing/typedecl.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1948,60 +1948,6 @@ let update_decls_jkind env decls =
- if -rectypes is not used, we only allow cycles in the type graph
if they go through an object or polymorphic variant type *)

(* We only allow recursion in unboxed product types to occur through boxes,
otherwise the type is uninhabitable and usually also infinite-size.
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.
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.
*)
let check_unboxed_recursion ~abs_env env loc path0 ty0 to_check =
let check_visited parents trace 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.path_and_expansion env ty with
| Some (path, ty') ->
expand (Path.Set.add path parents) (Expands_to (ty, ty') :: trace) ty'
| None ->
parents, trace, ty
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, _, _) ->
(* If we get a Tconstr, we only need to visit if it's part of this group
of mutually recursive typedecls. *)
if not (to_check path) then () else
check_visited parents trace ty;
visit_subtypes (Path.Set.add path parents) trace ty
| _ ->
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)
in
Ctype.wrap_trace_gadt_instances env (visit Path.Set.empty []) ty0

let check_well_founded ~abs_env env loc path to_check visited ty0 =
let rec check parents trace ty =
if TypeSet.mem ty parents then begin
Expand Down Expand Up @@ -2116,6 +2062,60 @@ let check_well_founded_decl ~abs_env env loc path decl to_check =
end)} in
it.it_type_declaration it (Ctype.generic_instance_declaration decl)

(* We only allow recursion in unboxed product types to occur through boxes,
otherwise the type is uninhabitable and usually also infinite-size.
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.
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.
*)
let check_unboxed_recursion ~abs_env env loc path0 ty0 to_check =
let check_visited parents trace 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.path_and_expansion env ty with
| Some (path, ty') ->
expand (Path.Set.add path parents) (Expands_to (ty, ty') :: trace) ty'
| None ->
parents, trace, ty
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, _, _) ->
(* If we get a Tconstr, we only need to visit if it's part of this group
of mutually recursive typedecls. *)
if not (to_check path) then () else
check_visited parents trace ty;
visit_subtypes (Path.Set.add path parents) trace ty
| _ ->
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)
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
Expand Down

0 comments on commit 83ae0ff

Please sign in to comment.