Skip to content

Commit

Permalink
Check for type recursion without boxing
Browse files Browse the repository at this point in the history
  • Loading branch information
rtjoa committed Dec 25, 2024
1 parent 2358e09 commit 2247db3
Show file tree
Hide file tree
Showing 11 changed files with 401 additions and 160 deletions.
13 changes: 8 additions & 5 deletions testsuite/tests/letrec-check/unboxed.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
13 changes: 7 additions & 6 deletions testsuite/tests/typing-layouts-unboxed-records/basics_alpha.ml
Original file line number Diff line number Diff line change
Expand Up @@ -25,19 +25,20 @@ 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}
[%%expect{|
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"
|}]

(******************************************************************************)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 = <fun>
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 *)
Expand Down
13 changes: 8 additions & 5 deletions testsuite/tests/typing-layouts-unboxed-records/letrec.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand Down
Loading

0 comments on commit 2247db3

Please sign in to comment.