Skip to content

Commit

Permalink
Add example of conservatively rejected recursion
Browse files Browse the repository at this point in the history
  • Loading branch information
rtjoa committed Dec 27, 2024
1 parent b7d41f8 commit f2fba07
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 0 deletions.
13 changes: 13 additions & 0 deletions testsuite/tests/typing-layouts-unboxed-records/recursive.ml
Original file line number Diff line number Diff line change
Expand Up @@ -247,6 +247,19 @@ Error: Unboxed record element types must have a representable layout.
(***************************************)
(* Singleton recursive unboxed records *)

(* CR layouts v7.2: allow the below. *)
type 'a safe = #{ a : 'a }
type x = int safe safe
[%%expect{|
type 'a safe = #{ a : 'a; }
Line 2, characters 0-22:
2 | type x = int safe safe
^^^^^^^^^^^^^^^^^^^^^^
Error: The definition of "x" is recursive without boxing:
"x" = "int safe safe",
"int safe safe" contains "int safe"
|}]

(* We could allow these, as although they have unguarded recursion,
they are finite size (thanks to the fact that we represent single-field
records as the layout of the field rather than as a singleton product).
Expand Down
5 changes: 5 additions & 0 deletions typing/typedecl.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2077,6 +2077,11 @@ let check_well_founded_decl ~abs_env env loc path decl to_check =
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.
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."
*)
let check_unboxed_recursion ~abs_env env loc path0 ty0 to_check =
let check_visited parents trace ty =
Expand Down

0 comments on commit f2fba07

Please sign in to comment.