Generate better error messages to report mixed mut rec groups

src/interp/Interpreter.ml

@@ -11,6 +11,7 @@ open LlbcAst
 open Contexts
 open SynthesizeSymbolic
 open Errors
+open Meta
 module SA = SymbolicAst
 
 (** The local logger *)
@@ -23,8 +24,85 @@ let compute_contexts (m : crate) : decls_ctx =
   let global_decls = m.global_decls in
   let trait_decls = m.trait_decls in
   let trait_impls = m.trait_impls in
-  let type_decls_groups, _, _, _, _ =
-    split_declarations_to_group_maps m.declarations
+  let fmt_env : Print.fmt_env =
+    {
+      type_decls;
+      fun_decls;
+      global_decls;
+      trait_decls;
+      trait_impls;
+      regions = [];
+      generics = empty_generic_params;
+      locals = [];
+    }
+  in
+  let type_decls_groups =
+    match split_declarations_to_group_maps m.declarations with
+    | Ok (type_decls_groups, _, _, _, _) -> type_decls_groups
+    | Error mixed_groups ->
+        let any_decl_id_to_string (id : any_decl_id) : string =
+          let get_meta :
+                'a. ('a -> item_meta) -> 'a option -> (span * name) option =
+           fun get x ->
+            match x with
+            | None -> None
+            | Some d ->
+                let meta = get d in
+                Some (meta.span, meta.name)
+          in
+          let kind, info =
+            match id with
+            | IdType id ->
+                ( "type decl",
+                  get_meta
+                    (fun (d : type_decl) -> d.item_meta)
+                    (TypeDeclId.Map.find_opt id type_decls) )
+            | IdFun id ->
+                ( "fun decl",
+                  get_meta
+                    (fun (d : fun_decl) -> d.item_meta)
+                    (FunDeclId.Map.find_opt id fun_decls) )
+            | IdGlobal id ->
+                ( "global decl",
+                  get_meta
+                    (fun (d : global_decl) -> d.item_meta)
+                    (GlobalDeclId.Map.find_opt id global_decls) )
+            | IdTraitDecl id ->
+                ( "trait decl",
+                  get_meta
+                    (fun (d : trait_decl) -> d.item_meta)
+                    (TraitDeclId.Map.find_opt id trait_decls) )
+            | IdTraitImpl id ->
+                ( "trait impl",
+                  get_meta
+                    (fun (d : trait_impl) -> d.item_meta)
+                    (TraitImplId.Map.find_opt id trait_impls) )
+          in
+          let s =
+            match info with
+            | None -> show_any_decl_id id
+            | Some (span, name) ->
+                kind ^ "(" ^ span_to_string span ^ "): "
+                ^ Print.name_to_string fmt_env name
+          in
+          "- " ^ s
+        in
+        let msgs =
+          List.map
+            (fun (g : mixed_declaration_group) ->
+              let decls =
+                List.map any_decl_id_to_string (g_declaration_group_to_list g)
+              in
+              String.concat "\n" decls)
+            mixed_groups
+        in
+        let msgs =
+          String.concat "\n\n" (List.map (fun s -> "Group:\n" ^ s) msgs)
+        in
+        craise_opt_span __FILE__ __LINE__ None
+          ("Detected groups of mixed mutually recursive definitions (such as a \
+            type mutually recursive with a function, or a function mutually \
+            recursive with a trait implementation):\n\n" ^ msgs)
   in
   let type_infos =
     TypesAnalysis.analyze_type_declarations type_decls type_decls_list