Check base case for recursive types

lib/typing/types.ml

@@ -314,46 +314,76 @@ let resolve_alias find_decl typ =
   in
   aux typ
 
+type recurs_state = { recurs : bool; has_base : bool }
+
+let combine a b =
+  (* Something is recursive if one branch is recursive. If both branches are
+     recursive, both must have a base for the whole recursion to have a base. *)
+  match (a, b) with
+  | Ok a, Ok b ->
+      Ok
+        (match (a, b) with
+        | { recurs = true; _ }, { recurs = false; _ } -> a
+        | { recurs = false; _ }, { recurs = true; _ } -> b
+        | { recurs = true; has_base = ab }, { recurs = true; has_base = bb } ->
+            { recurs = true; has_base = ab && bb }
+        | { recurs = false; _ }, { recurs = false; _ } ->
+            { recurs = false; has_base = false })
+  | Error _, _ -> a
+  | _, Error _ -> b
+
 let recursion_allowed ~params name typ =
   let rec aux behind_ptr res = function
     | Ttuple ts ->
-        let res, ts =
+        let nres, ts =
           List.fold_left_map (fun res t -> aux behind_ptr res t) res ts
         in
-        (res, Ttuple ts)
+        (combine nres res, Ttuple ts)
     | Tfun (ps, ret, kind) ->
-        let res, ps =
+        let nres, ps =
           List.fold_left_map
             (fun res p ->
-              let res, pt = aux true res p.pt in
-              (res, { p with pt }))
+              let res =
+                Result.map (fun st -> { st with has_base = true }) res
+              in
+              let nres, pt = aux true res p.pt in
+              (combine nres res, { p with pt }))
             res ps
         in
-        let res, ret = aux true res ret in
-        (res, Tfun (ps, ret, kind))
+        let mres, ret = aux true res ret in
+        (combine nres res |> combine mres, Tfun (ps, ret, kind))
     | (Qvar _ | Tvar { contents = Unbound _ }) as t -> (res, t)
     | Tvar ({ contents = Link t } as rf) as tvr ->
-        let res, t = aux behind_ptr res t in
+        let nres, t = aux behind_ptr res t in
         rf := Link t;
-        (res, tvr)
+        (combine nres res, tvr)
     | Tfixed_array (sz, t) ->
-        let res, t = aux behind_ptr res t in
-        (res, Tfixed_array (sz, t))
-    | Tconstr ((Pid ("array" | "raw_ptr" | "rc") as name), [ t ]) ->
-        let res, t = aux true res t in
-        (res, Tconstr (name, [ t ]))
+        let nres, t = aux behind_ptr res t in
+        (combine nres res, Tfixed_array (sz, t))
+    | Tconstr ((Pid ("array" | "raw_ptr") as name), [ t ]) ->
+        let nres, t =
+          aux true (Result.map (fun st -> { st with has_base = true }) res) t
+        in
+        (combine nres res, Tconstr (name, [ t ]))
+    | Tconstr ((Pid "rc" as name), [ t ]) ->
+        let nres, t = aux true res t in
+        (combine nres res, Tconstr (name, [ t ]))
     | Tconstr (n, ps) as t ->
         if Path.equal n name then
-          if behind_ptr then (Ok true, Tconstr (n, params))
+          if behind_ptr then
+            ( (match res with
+              | Ok { has_base; _ } -> Ok { has_base; recurs = true }
+              | Error _ as err -> err),
+              Tconstr (n, params) )
           else (Error "Infinite type", t)
         else
           let res, ps =
             List.fold_left_map (fun res t -> aux behind_ptr res t) res ps
           in
           (res, Tconstr (n, ps))
   in
-  let res, typ = aux false (Ok false) typ in
+  let res, typ = aux false (Ok { recurs = false; has_base = false }) typ in
   match res with
-  | Ok true -> Ok (Some typ)
-  | Ok false -> Ok None
+  | Ok { recurs = true; has_base } -> Ok (Some (typ, has_base))
+  | Ok { recurs = false; _ } -> Ok None
   | Error _ as err -> err

lib/typing/types.mli

@@ -77,4 +77,7 @@ val typ_of_decl : type_decl -> Path.t -> typ
 val resolve_alias : (Path.t -> (type_decl * Path.t) option) -> typ -> typ
 
 val recursion_allowed :
-  params:typ list -> Path.t -> typ -> (typ option, string) result
+  params:typ list ->
+  Path.t ->
+  typ ->
+  ((typ * bool (* includes base case *)) option, string) result

lib/typing/typing.ml

@@ -356,7 +356,9 @@ let type_record env loc ~in_sgn Ast.{ name = { poly_param; name }; labels } =
           let typ = typeof_annot ~typedef:true temp_env loc type_expr in
           let ftyp =
             match recursion_allowed ~params absolute_path typ with
-            | Ok (Some typ) ->
+            | Ok (Some (typ, has_base)) ->
+                if not has_base then
+                  raise (Error (loc, "Recursive type has no base case"));
                 recurs := true;
                 typ
             | Ok None -> typ
@@ -445,7 +447,8 @@ let type_variant env loc ~in_sgn { Ast.name = { poly_param; name }; ctors } =
             let typ = typeof_annot ~typedef:true temp_env loc annot in
             let typ =
               match recursion_allowed ~params absolute_path typ with
-              | Ok (Some typ) ->
+              | Ok (Some (typ, hasbase)) ->
+                  if hasbase then has_base := true;
                   recurs := true;
                   typ
               | Ok None ->

test/typing.ml

@@ -1310,6 +1310,12 @@ type option('a) = #none | #some('a)
 type data('a) = { cb : 'a }
 type state = { data : container(data(option((state&) -> unit))) }|}
 
+let test_rec_type_record_param_nobase () =
+  test_exn "Recursive type has no base case"
+    {|type container('a) = { a : 'a }
+type data('a) = { cb : 'a }
+type state = { data : container(data(rc(state))) }|}
+
 let case str test = test_case str `Quick test
 
 (* Run it *)
@@ -1781,5 +1787,6 @@ do:
           case "noptr fixed array" test_rec_type_noptr_array;
           case "nobase" test_rec_type_nobase;
           case "record param" test_rec_type_record_param;
+          case "record param nobase" test_rec_type_record_param_nobase;
         ] );
     ]