From 8b38c59832d76c82ba0ef6c918ec1c66c3409cbf Mon Sep 17 00:00:00 2001 From: Ryan Tjoa Date: Mon, 23 Dec 2024 15:45:31 -0500 Subject: [PATCH] Check for type recursion without boxing --- testsuite/tests/letrec-check/unboxed.ml | 13 +- .../basics_alpha.ml | 13 +- .../basics_from_typing_atat_unboxed.ml | 16 +- .../typing-layouts-unboxed-records/letrec.ml | 13 +- .../recursive.ml | 357 +++++++++++------- testsuite/tests/typing-unboxed-types/test.ml | 39 +- testsuite/tests/typing-unboxed/test.ml | 6 +- typing/ctype.ml | 23 ++ typing/ctype.mli | 7 + typing/typedecl.ml | 73 ++++ typing/typedecl.mli | 1 + 11 files changed, 401 insertions(+), 160 deletions(-) diff --git a/testsuite/tests/letrec-check/unboxed.ml b/testsuite/tests/letrec-check/unboxed.ml index 2ebc1c74e69..8e80fa719eb 100644 --- a/testsuite/tests/letrec-check/unboxed.ml +++ b/testsuite/tests/letrec-check/unboxed.ml @@ -23,14 +23,17 @@ Line 2, characters 12-19: Error: This kind of expression is not allowed as right-hand side of "let rec" |}];; +(* This test was made to error by disallowing singleton recursive unboxed types. + We keep it in case these are re-allowed, in which case it should error with: + [This kind of expression is not allowed as right-hand side of "let rec"] *) type r = A of r [@@unboxed] let rec y = A y;; [%%expect{| -type r = A of r [@@unboxed] -Line 2, characters 12-15: -2 | let rec y = A y;; - ^^^ -Error: This kind of expression is not allowed as right-hand side of "let rec" +Line 1, characters 0-27: +1 | type r = A of r [@@unboxed] + ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The definition of "r" is recursive without boxing: + "r" contains "r" |}];; (* This test is not allowed if 'a' is unboxed, but should be accepted diff --git a/testsuite/tests/typing-layouts-unboxed-records/basics_alpha.ml b/testsuite/tests/typing-layouts-unboxed-records/basics_alpha.ml index af39bb18f64..e65ebffd038 100644 --- a/testsuite/tests/typing-layouts-unboxed-records/basics_alpha.ml +++ b/testsuite/tests/typing-layouts-unboxed-records/basics_alpha.ml @@ -25,7 +25,11 @@ type t = { x : t_void; } [@@unboxed] type bad : void = #{ bad : bad } [%%expect{| -type bad = #{ bad : bad; } +Line 1, characters 0-32: +1 | type bad : void = #{ bad : bad } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The definition of "bad" is recursive without boxing: + "bad" contains "bad" |}] type ('a : void) bad = #{ bad : 'a bad ; u : 'a} @@ -33,11 +37,8 @@ type ('a : void) bad = #{ bad : 'a bad ; u : 'a} Line 1, characters 0-49: 1 | type ('a : void) bad = #{ bad : 'a bad ; u : 'a} ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: - The layout of 'a bad is any & any - because it is an unboxed record. - But the layout of 'a bad must be representable - because it is the type of record field bad. +Error: The definition of "bad" is recursive without boxing: + "'a bad" contains "'a bad" |}] (******************************************************************************) diff --git a/testsuite/tests/typing-layouts-unboxed-records/basics_from_typing_atat_unboxed.ml b/testsuite/tests/typing-layouts-unboxed-records/basics_from_typing_atat_unboxed.ml index 34c7c5731d3..662121638b7 100644 --- a/testsuite/tests/typing-layouts-unboxed-records/basics_from_typing_atat_unboxed.ml +++ b/testsuite/tests/typing-layouts-unboxed-records/basics_from_typing_atat_unboxed.ml @@ -80,14 +80,24 @@ in assert (f x = #{ f = 3.14});; - : unit = () |}];; -(* Check for a potential infinite loop in the typing algorithm. *) +(* Check for a potential infinite loop in the typing algorithm. + (This test was made to error upon disallowing singleton recursive unboxed + types. We keep it around in case these are re-allowed.) *) type 'a t12 : value = #{ a : 'a t12 };; [%%expect{| -type 'a t12 = #{ a : 'a t12; } +Line 1, characters 0-37: +1 | type 'a t12 : value = #{ a : 'a t12 };; + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The definition of "t12" is recursive without boxing: + "'a t12" contains "'a t12" |}];; let f (a : int t12 array) = a.(0);; [%%expect{| -val f : int t12 array -> int t12 = +Line 1, characters 15-18: +1 | let f (a : int t12 array) = a.(0);; + ^^^ +Error: Unbound type constructor "t12" +Hint: Did you mean "t11" or "t2"? |}];; (* should work *) diff --git a/testsuite/tests/typing-layouts-unboxed-records/letrec.ml b/testsuite/tests/typing-layouts-unboxed-records/letrec.ml index 847b2fa41a6..8dd8dde255b 100644 --- a/testsuite/tests/typing-layouts-unboxed-records/letrec.ml +++ b/testsuite/tests/typing-layouts-unboxed-records/letrec.ml @@ -7,14 +7,17 @@ } *) +(* This test was made to error by disallowing singleton recursive unboxed types. + We keep it in case these are re-allowed, in which case it should error with: + [This kind of expression is not allowed as right-hand side of "let rec"] *) type t : value = #{ t : t } let rec t = #{ t = t } [%%expect{| -type t = #{ t : t; } -Line 2, characters 12-22: -2 | let rec t = #{ t = t } - ^^^^^^^^^^ -Error: This kind of expression is not allowed as right-hand side of "let rec" +Line 1, characters 0-27: +1 | type t : value = #{ t : t } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The definition of "t" is recursive without boxing: + "t" contains "t" |}] type bx = { bx : ubx } diff --git a/testsuite/tests/typing-layouts-unboxed-records/recursive.ml b/testsuite/tests/typing-layouts-unboxed-records/recursive.ml index a9e00527391..257578fe211 100644 --- a/testsuite/tests/typing-layouts-unboxed-records/recursive.ml +++ b/testsuite/tests/typing-layouts-unboxed-records/recursive.ml @@ -7,59 +7,69 @@ } *) -(* CR layouts v7.2: figure out the story for recursive unboxed products. - Consider that the following is allowed upstream: - type t = { t : t } [@@unboxed] - We should also give good errors for infinite-size unboxed records (see the - test at the bottom of this file with a depth-100 kind). -*) +(* We only allow recursion of unboxed product types through boxing, otherwise + the type is uninhabitable and usually also infinite-size. *) -(************************************) -(* Basic recursive unboxed products *) +(***********************************************) +(* Allowed (guarded) recursive unboxed records *) -type t : value = #{ t : t } +(* Guarded by `list` *) +type t = #{ tl: t list } [%%expect{| -type t = #{ t : t; } +type t = #{ tl : t list; } |}] -type t : float64 = #{ t : t } +(* Guarded by a function *) +type t = #{ f1 : t -> t ; f2 : t -> t } [%%expect{| -type t = #{ t : t; } +type t = #{ f1 : t -> t; f2 : t -> t; } |}] -type t : value = #{ t : t } +(* Guarded by a tuple *) +type a = #{ b : b } +and b = a * a [%%expect{| -type t = #{ t : t; } +type a = #{ b : b; } +and b = a * a |}] -(* CR layouts v7.2: Once we support unboxed records with elements of kind [any], - and detect bad recursive unboxed records with an occurs check, this error - should improve. -*) +(* Guarded by a function *) +type a = #{ b : b } +and b = #{ c1 : c ; c2 : c } +and c = unit -> a +[%%expect{| +type a = #{ b : b; } +and b = #{ c1 : c; c2 : c; } +and c = unit -> a +|}] + +(* Recursion through modules guarded by a function *) +module rec A : sig + type t = #{ b1 : B.t ; b2 : B.t } +end = struct + type t = #{ b1 : B.t ; b2 : B.t } +end +and B : sig + type t = unit -> A.t +end = struct + type t = unit -> A.t +end +[%%expect{| +module rec A : sig type t = #{ b1 : B.t; b2 : B.t; } end +and B : sig type t = unit -> A.t end +|}] + +(**********************************) +(* Infinite-sized unboxed records *) + type bad = #{ bad : bad ; i : int} [%%expect{| Line 1, characters 0-34: 1 | type bad = #{ bad : bad ; i : int} ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: - The layout of bad is any & any - because it is an unboxed record. - But the layout of bad must be representable - because it is the type of record field bad. -|}] - -type bad = #{ bad : bad } -[%%expect{| -Line 1, characters 0-25: -1 | type bad = #{ bad : bad } - ^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: - The layout of bad is any - because a dummy kind of any is used to check mutually recursive datatypes. - Please notify the Jane Street compilers group if you see this output. - But the layout of bad must be representable - because it is the type of record field bad. +Error: The definition of "bad" is recursive without boxing: + "bad" contains "bad" |}] type a_bad = #{ b_bad : b_bad } @@ -68,12 +78,8 @@ and b_bad = #{ a_bad : a_bad } Line 1, characters 0-31: 1 | type a_bad = #{ b_bad : b_bad } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: - The layout of a_bad is any - because a dummy kind of any is used to check mutually recursive datatypes. - Please notify the Jane Street compilers group if you see this output. - But the layout of a_bad must be representable - because it is the type of record field a_bad. +Error: The definition of "a_bad" is recursive without boxing: + "a_bad" contains "a_bad" |}] type bad : any = #{ bad : bad } @@ -81,23 +87,35 @@ type bad : any = #{ bad : bad } Line 1, characters 0-31: 1 | type bad : any = #{ bad : bad } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: - The layout of bad is any - because of the annotation on the declaration of the type bad. - But the layout of bad must be representable - because it is the type of record field bad. +Error: The definition of "bad" is recursive without boxing: + "bad" contains "bad" |}] -type 'a id = #{ a : 'a } -type bad = bad id +type ('a : any) record_id = #{ a : 'a } +type ('a : any) alias_id = 'a [%%expect{| -type 'a id = #{ a : 'a; } -Line 2, characters 0-17: -2 | type bad = bad id - ^^^^^^^^^^^^^^^^^ +type 'a record_id = #{ a : 'a; } +type ('a : any) alias_id = 'a +|}] + +type bad = bad record_id +[%%expect{| +Line 1, characters 0-24: +1 | type bad = bad record_id + ^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The type abbreviation "bad" is cyclic: + "bad" = "bad record_id", + "bad record_id" contains "bad" +|}] + +type bad = bad alias_id +[%%expect{| +Line 1, characters 0-23: +1 | type bad = bad alias_id + ^^^^^^^^^^^^^^^^^^^^^^^ Error: The type abbreviation "bad" is cyclic: - "bad" = "bad id", - "bad id" contains "bad" + "bad" = "bad alias_id", + "bad alias_id" = "bad" |}] @@ -106,11 +124,8 @@ type 'a bad = #{ bad : 'a bad ; u : 'a} Line 1, characters 0-39: 1 | type 'a bad = #{ bad : 'a bad ; u : 'a} ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: - The layout of 'a bad is any & any - because it is an unboxed record. - But the layout of 'a bad must be representable - because it is the type of record field bad. +Error: The definition of "bad" is recursive without boxing: + "'a bad" contains "'a bad" |}] type 'a bad = { bad : 'a bad ; u : 'a} @@ -118,80 +133,160 @@ type 'a bad = { bad : 'a bad ; u : 'a} type 'a bad = { bad : 'a bad; u : 'a; } |}] -(****************************) -(* A particularly bad error *) - type bad : float64 = #{ bad : bad ; i : int} [%%expect{| Line 1, characters 0-44: 1 | type bad : float64 = #{ bad : bad ; i : int} ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The layout of type "bad" is (((((((((((((((((((((((((((((((((((( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - (float64 & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value) & value - because it is an unboxed record. - But the layout of type "bad" must be a sublayout of float64 - because of the annotation on the declaration of the type bad. +Error: The definition of "bad" is recursive without boxing: + "bad" contains "bad" +|}] + +type bad = #{ a : t ; b : t } +[%%expect{| +type bad = #{ a : t; b : t; } +|}] + +type 'a bad = #{ a : 'a bad } +[%%expect{| +Line 1, characters 0-29: +1 | type 'a bad = #{ a : 'a bad } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The definition of "bad" is recursive without boxing: + "'a bad" contains "'a bad" +|}] + +type bad = #( s * s ) +and ('a : any) record_id2 = #{ a : 'a } +and s = #{ u : u } +and u = #(int * bad record_id2) +[%%expect{| +Line 1, characters 0-21: +1 | type bad = #( s * s ) + ^^^^^^^^^^^^^^^^^^^^^ +Error: The definition of "bad" is recursive without boxing: + "bad" = "#(s * s)", + "#(s * s)" contains "u", + "u" = "#(int * bad record_id2)", + "#(int * bad record_id2)" contains "bad" +|}] + +type bad = #( s * s ) +and ('a : any) record_id2 = #{ a : 'a } +and s = #{ u : u } +and u = #(int * bad alias_id record_id2) +[%%expect{| +Line 1, characters 0-21: +1 | type bad = #( s * s ) + ^^^^^^^^^^^^^^^^^^^^^ +Error: The definition of "bad" is recursive without boxing: + "bad" = "#(s * s)", + "#(s * s)" contains "u", + "u" = "#(int * bad alias_id record_id2)", + "#(int * bad alias_id record_id2)" contains "bad alias_id", + "bad alias_id" = "bad", + "bad" = "#(s * s)", + "#(s * s)" contains "s" +|}] + +(* We also check recursive types via modules *) +module rec Bad_rec1 : sig + type t = #( s * s ) + and s = #{ u : Bad_rec2.u } +end = struct + type t = #( s * s ) + and s = #{ u : Bad_rec2.u } +end +and Bad_rec2 : sig + type u = Bad_rec1.t id + and 'a id = 'a +end = struct + type u = Bad_rec1.t id + and 'a id = 'a +end +[%%expect{| +Lines 1-7, characters 0-3: +1 | module rec Bad_rec1 : sig +2 | type t = #( s * s ) +3 | and s = #{ u : Bad_rec2.u } +4 | end = struct +5 | type t = #( s * s ) +6 | and s = #{ u : Bad_rec2.u } +7 | end +Error: The definition of "Bad_rec1.t" is recursive without boxing: + "Bad_rec1.t" = "#(Bad_rec1.s * Bad_rec1.s)", + "#(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" +|}] + +(* When we allow records with elements of unrepresentable layout, this should + still be disallowed. *) +module M : sig + type ('a : any) opaque_id : any +end = struct + type ('a : any) opaque_id = 'a +end +[%%expect{| +module M : sig type ('a : any) opaque_id : any end +|}] +type a = #{ b : b M.opaque_id } +and b = #{ a : a M.opaque_id } +[%%expect{| +Line 1, characters 12-29: +1 | type a = #{ b : b M.opaque_id } + ^^^^^^^^^^^^^^^^^ +Error: Unboxed record element types must have a representable layout. + The layout of b M.opaque_id is any + because of the definition of opaque_id at line 2, characters 2-33. + But the layout of b M.opaque_id must be representable + because it is the type of record field b. +|}] + +(***************************************) +(* Singleton recursive unboxed records *) + +(* 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). + However, allowing them makes checking for recursive types more difficult, + and they are uninhabitable anyway. *) + +type bad : value = #{ bad : bad } +[%%expect{| +Line 1, characters 0-33: +1 | type bad : value = #{ bad : bad } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The definition of "bad" is recursive without boxing: + "bad" contains "bad" +|}] + +type bad : float64 = #{ bad : bad } +[%%expect{| +Line 1, characters 0-35: +1 | type bad : float64 = #{ bad : bad } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The definition of "bad" is recursive without boxing: + "bad" contains "bad" +|}] + + +type bad : value = #{ bad : bad } +[%%expect{| +Line 1, characters 0-33: +1 | type bad : value = #{ bad : bad } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The definition of "bad" is recursive without boxing: + "bad" contains "bad" +|}] + +type bad = #{ bad : bad } +[%%expect{| +Line 1, characters 0-25: +1 | type bad = #{ bad : bad } + ^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The definition of "bad" is recursive without boxing: + "bad" contains "bad" |}] diff --git a/testsuite/tests/typing-unboxed-types/test.ml b/testsuite/tests/typing-unboxed-types/test.ml index 9825f4fdfc3..c14e7bc4503 100644 --- a/testsuite/tests/typing-unboxed-types/test.ml +++ b/testsuite/tests/typing-unboxed-types/test.ml @@ -95,17 +95,24 @@ Error: This type cannot be unboxed because its constructor has more than one field. |}];; -(* let rec must be rejected *) +(* This test was made to error by disallowing singleton recursive unboxed types. + We keep it in case these are re-allowed, in which case it should error with: + [This kind of expression is not allowed as right-hand side of "let rec"] *) type t10 : value = A of t10 [@@ocaml.unboxed];; [%%expect{| -type t10 = A of t10 [@@unboxed] +Line 1, characters 0-45: +1 | type t10 : value = A of t10 [@@ocaml.unboxed];; + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The definition of "t10" is recursive without boxing: + "t10" contains "t10" |}];; let rec x = A x;; [%%expect{| -Line 1, characters 12-15: +Line 1, characters 14-15: 1 | let rec x = A x;; - ^^^ -Error: This kind of expression is not allowed as right-hand side of "let rec" + ^ +Error: This expression has type "t1" but an expression was expected of type + "string" |}];; (* Representation mismatch between module and signature must be rejected *) @@ -284,20 +291,34 @@ in assert (f x = L 3.14);; - : unit = () |}];; -(* Check for a potential infinite loop in the typing algorithm. *) +(* Check for a potential infinite loop in the typing algorithm. + (This test was made to error upon disallowing singleton recursive [@@unboxed] + types. We keep it around in case these are re-allowed.) *) type 'a t12 = M of 'a t12 [@@ocaml.unboxed];; [%%expect{| -type 'a t12 = M of 'a t12 [@@unboxed] +Line 1, characters 0-43: +1 | type 'a t12 = M of 'a t12 [@@ocaml.unboxed];; + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The definition of "t12" is recursive without boxing: + "'a t12" contains "'a t12" |}];; let f (a : int t12 array) = a.(0);; [%%expect{| -val f : int t12 array -> int t12 = +Line 1, characters 15-18: +1 | let f (a : int t12 array) = a.(0);; + ^^^ +Error: Unbound type constructor "t12" +Hint: Did you mean "t1", "t11" or "t2"? |}];; (* Check for another possible loop *) type t13 = A : _ t12 -> t13 [@@ocaml.unboxed];; [%%expect{| -type t13 = A : 'a t12 -> t13 [@@unboxed] +Line 1, characters 17-20: +1 | type t13 = A : _ t12 -> t13 [@@ocaml.unboxed];; + ^^^ +Error: Unbound type constructor "t12" +Hint: Did you mean "t1", "t11", "t13" or "t2"? |}];; diff --git a/testsuite/tests/typing-unboxed/test.ml b/testsuite/tests/typing-unboxed/test.ml index 4c5287e1ab0..ee4da937b43 100644 --- a/testsuite/tests/typing-unboxed/test.ml +++ b/testsuite/tests/typing-unboxed/test.ml @@ -756,7 +756,11 @@ Error: The native code version of the primitive is mandatory (* PR#7424 *) type 'a b = B of 'a b b [@@unboxed];; [%%expect{| -type 'a b = B of 'a b b [@@unboxed] +Line 1, characters 0-35: +1 | type 'a b = B of 'a b b [@@unboxed];; + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The definition of "b" is recursive without boxing: + "'a b" contains "'a b b" |}] diff --git a/typing/ctype.ml b/typing/ctype.ml index 8ac146ae94d..c36922329f0 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -2073,6 +2073,15 @@ let try_expand_safe_opt env ty = with Escape _ -> Btype.backtrack snap; raise Cannot_expand +let path_and_expansion env ty = + match try_expand_safe_opt env ty with + | ty' -> + begin match get_desc ty with + | Tconstr (path, _, _) -> Some (path, ty') + | _ -> Misc.fatal_error "Ctype.path_and_expansion" + end + | exception Cannot_expand -> None + let expand_head_opt env ty = try try_expand_head try_expand_safe_opt env ty with Cannot_expand -> ty @@ -2116,6 +2125,20 @@ let unbox_once env ty = | Tpoly (ty, _) -> Stepped ty | _ -> Final_result +let contained_without_boxing env ty = + match get_desc ty with + | Tconstr _ -> + begin match unbox_once env ty with + | Stepped ty -> [ty] + | Stepped_record_unboxed_product tys -> tys + | Final_result | Missing _ -> [] + end + | Tunboxed_tuple labeled_tys -> + List.map snd labeled_tys + | Tpoly (ty, _) -> [ty] + | Tvar _ | Tarrow _ | Ttuple _ | Tobject _ | Tfield _ | Tnil | Tlink _ + | Tsubst _ | Tvariant _ | Tunivar _ | Tpackage _ -> [] + (* We use ty_prev to track the last type for which we found a definition, allowing us to return a type for which a definition was found even if we eventually bottom out at a missing cmi file, or otherwise. *) diff --git a/typing/ctype.mli b/typing/ctype.mli index 6caadd85790..75951855586 100644 --- a/typing/ctype.mli +++ b/typing/ctype.mli @@ -246,6 +246,9 @@ val apply: val try_expand_once_opt: Env.t -> type_expr -> type_expr val try_expand_safe_opt: Env.t -> type_expr -> type_expr +val path_and_expansion: Env.t -> type_expr -> (Path.t * type_expr) option +(** Return an option instead of raising, and gives the path of the input type *) + val expand_head_once: Env.t -> type_expr -> type_expr val expand_head: Env.t -> type_expr -> type_expr val expand_head_opt: Env.t -> type_expr -> type_expr @@ -581,6 +584,10 @@ val get_unboxed_type_approximation : Env.t -> type_expr -> type_expr [get_unboxed_type_representation], but doesn't indicate whether the type was fully expanded or not. *) +val contained_without_boxing : Env.t -> type_expr -> type_expr list + (* Return all types that are contained without boxing + (or "without indirection" or "flatly") *) + (* Given the row from a variant type, determine if it is immediate. Currently just checks that all constructors have no arguments, doesn't consider void. *) diff --git a/typing/typedecl.ml b/typing/typedecl.ml index 72b12a3d787..80c69b87e02 100644 --- a/typing/typedecl.ml +++ b/typing/typedecl.ml @@ -89,6 +89,7 @@ type error = | Unboxed_mutable_label | Recursive_abbrev of string * Env.t * reaching_type_path | Cycle_in_def of string * Env.t * reaching_type_path + | Unboxed_recursion of string * Env.t * reaching_type_path | Definition_mismatch of type_expr * Env.t * Includecore.type_mismatch option | Constraint_failed of Env.t * Errortrace.unification_error | Inconsistent_constraint of Env.t * Errortrace.unification_error @@ -1947,6 +1948,58 @@ 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 of unboxed product types through boxing, otherwise + the type is uninhabitable and usually also infinite-size. + + Because `check_well_founded` already ruled out recursion without through + structural types (unboxed tuples and aliases), we just look for a cycle in + paths. + + An alternative implementation could have introduced layout variables (for + this check only), and find 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 @@ -2061,6 +2114,12 @@ 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) +let check_unboxed_recursion_decl ~abs_env env loc path decl to_check = + let open Btype in + let decl = Ctype.generic_instance_declaration decl in + let ty = newgenty (Tconstr (path, decl.type_params, ref Mnil)) in + check_unboxed_recursion ~abs_env env loc path ty to_check + (* Check for non-regular abbreviations; an abbreviation [type 'a t = ...] is non-regular if the expansion of [...] contains instances [ty t] where [ty] is not equal to ['a]. @@ -2347,6 +2406,11 @@ let transl_type_decl env rec_flag sdecl_list = (Path.Pident id) decl to_check) decls; + 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 @@ -3434,6 +3498,7 @@ let check_recmod_typedecl env loc recmod_ids path decl = (path, decl) is the type declaration to be checked. *) let to_check path = Path.exists_free recmod_ids path in check_well_founded_decl ~abs_env:env env loc path decl to_check; + check_unboxed_recursion_decl ~abs_env:env env loc path decl to_check; check_regularity ~abs_env:env env loc path decl to_check; (* additional coherence check, as one might build an incoherent signature, and use it to build an incoherent module, cf. #7851 *) @@ -3577,6 +3642,14 @@ let report_error ppf = function fprintf ppf "@[The definition of %a contains a cycle%a@]" Style.inline_code s Reaching_path.pp_colon reaching_path + | Unboxed_recursion (s, env, reaching_path) -> + let reaching_path = Reaching_path.simplify reaching_path in + Printtyp.wrap_printing_env ~error:true env @@ fun () -> + Printtyp.reset (); + Reaching_path.add_to_preparation reaching_path; + fprintf ppf "@[The definition of %a is recursive without boxing%a@]" + Style.inline_code s + Reaching_path.pp_colon reaching_path | Definition_mismatch (ty, _env, None) -> fprintf ppf "@[@[%s@ %s@;<1 2>%a@]@]" "This variant or record definition" "does not match that of type" diff --git a/typing/typedecl.mli b/typing/typedecl.mli index 13693ebd5a7..1a1555a9d1a 100644 --- a/typing/typedecl.mli +++ b/typing/typedecl.mli @@ -125,6 +125,7 @@ type error = | Unboxed_mutable_label | Recursive_abbrev of string * Env.t * reaching_type_path | Cycle_in_def of string * Env.t * reaching_type_path + | Unboxed_recursion of string * Env.t * reaching_type_path | Definition_mismatch of type_expr * Env.t * Includecore.type_mismatch option | Constraint_failed of Env.t * Errortrace.unification_error | Inconsistent_constraint of Env.t * Errortrace.unification_error