Make sure we scan every type for variants during Jib monomorphisation

This might be quite a bit more expensive than what we were doing previously but is needed to avoid missing any type that is used within a function but never appears in any external type signature or is never constructed
rems-project · Oct 31, 2023 · 11845f7 · 11845f7
1 parent 4437a67
commit 11845f7
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 26 deletions.
diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml
@@ -1768,6 +1768,23 @@ module Make (C : CONFIG) = struct
         | _ -> DoChildren
     end
 
+  class scan_variant_visitor instantiations ctx var_id =
+    object
+      inherit empty_jib_visitor
+
+      method vctyp =
+        function
+        | CT_variant (var_id', ctors) when Id.compare var_id var_id' = 0 ->
+            let generic_ctors = Bindings.find var_id ctx.variants |> snd |> Bindings.bindings in
+            let unifiers =
+              ctyp_unify (id_loc var_id') (CT_variant (var_id, generic_ctors)) (CT_variant (var_id, ctors))
+              |> KBindings.bindings |> List.map snd
+            in
+            instantiations := CTListSet.add unifiers !instantiations;
+            DoChildren
+        | _ -> DoChildren
+    end
+
   let rec specialize_variants ctx prior =
     let instantiations = ref CTListSet.empty in
     let fix_variants ctx var_id = visit_ctyp (new fix_variants_visitor ctx var_id) in
@@ -1787,32 +1804,7 @@ module Make (C : CONFIG) = struct
     | CDEF_type (CTD_variant (var_id, ctors)) :: cdefs when List.exists (fun (_, ctyp) -> is_polymorphic ctyp) ctors ->
         let typ_params = List.fold_left (fun set (_, ctyp) -> KidSet.union (ctyp_vars ctyp) set) KidSet.empty ctors in
 
-        List.iter
-          (function
-            | CDEF_val (id, _, ctyps, ctyp) ->
-                let _ =
-                  List.map
-                    (map_ctyp (fun ctyp ->
-                         match ctyp with
-                         | CT_variant (var_id', ctors) when Id.compare var_id var_id' = 0 ->
-                             let generic_ctors = Bindings.find var_id ctx.variants |> snd |> Bindings.bindings in
-                             let unifiers =
-                               ctyp_unify (id_loc var_id')
-                                 (CT_variant (var_id, generic_ctors))
-                                 (CT_variant (var_id, ctors))
-                               |> KBindings.bindings |> List.map snd
-                             in
-                             instantiations := CTListSet.add unifiers !instantiations;
-                             ctyp
-                         | ctyp -> ctyp
-                     )
-                    )
-                    (ctyp :: ctyps)
-                in
-                ()
-            | _ -> ()
-            )
-          cdefs;
+        let _ = visit_cdefs (new scan_variant_visitor instantiations ctx var_id) cdefs in
 
         let cdefs =
           List.fold_left (fun cdefs (ctor_id, ctyp) -> specialize_constructor ctx ctor_id cdefs) cdefs ctors

diff --git a/test/c/unconstructed_type_mono.expect b/test/c/unconstructed_type_mono.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/unconstructed_type_mono.sail b/test/c/unconstructed_type_mono.sail
@@ -0,0 +1,9 @@
+$include <result.sail>
+$include <string.sail>
+
+union U ('a: Type) = { U1 : 'a }
+
+type V = U(unit)
+
+val main : unit -> unit
+function main () = let r : result(V, unit) = Err(()) in print_endline("ok")