From 134b2d801390d5e94cd19c6210db1c0408c225fa Mon Sep 17 00:00:00 2001
From: Alasdair <alasdair.armstrong@cl.cam.ac.uk>
Date: Fri, 15 Dec 2023 14:10:31 +0000
Subject: [PATCH] Jib: Avoid ctyp_suprema on monomorphic parts of polymorphic
 constructors

Fixes #401
---
 src/lib/jib_compile.ml | 12 ++++++------
 test/c/issue401.expect |  1 +
 test/c/issue401.sail   | 20 ++++++++++++++++++++
 3 files changed, 27 insertions(+), 6 deletions(-)
 create mode 100644 test/c/issue401.expect
 create mode 100644 test/c/issue401.sail

diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml
index c391af3d4..543df70ea 100644
--- a/src/lib/jib_compile.ml
+++ b/src/lib/jib_compile.ml
@@ -669,17 +669,17 @@ module Make (C : CONFIG) = struct
                       (string_of_ctyp (cval_ctyp cval))
                       (string_of_ctyp (ctyp_of_typ ctx variant_typ))
                    )
-                )
-            else ();
+                );
             let unifiers, ctor_ctyp =
               let generic_ctors = Bindings.find var_id ctx.variants |> snd |> Bindings.bindings in
               let unifiers =
                 ctyp_unify l (CT_variant (var_id, generic_ctors)) (cval_ctyp cval) |> KBindings.bindings |> List.map snd
               in
-              let is_poly_ctor =
-                List.exists (fun (id, ctyp) -> Id.compare id ctor = 0 && is_polymorphic ctyp) generic_ctors
-              in
-              (unifiers, if is_poly_ctor then ctyp_suprema pat_ctyp else pat_ctyp)
+              match List.find_opt (fun (id, ctyp) -> Id.compare id ctor = 0 && is_polymorphic ctyp) generic_ctors with
+              | Some (_, poly_ctor_ctyp) ->
+                  let instantiated_parts = KBindings.map ctyp_suprema (ctyp_unify l poly_ctor_ctyp pat_ctyp) in
+                  (unifiers, subst_poly instantiated_parts poly_ctor_ctyp)
+              | None -> (unifiers, pat_ctyp)
             in
             let pre, instrs, cleanup, ctx =
               compile_match ctx apat (V_ctor_unwrap (cval, (ctor, unifiers), ctor_ctyp)) case_label
diff --git a/test/c/issue401.expect b/test/c/issue401.expect
new file mode 100644
index 000000000..9766475a4
--- /dev/null
+++ b/test/c/issue401.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/issue401.sail b/test/c/issue401.sail
new file mode 100644
index 000000000..b806d7be9
--- /dev/null
+++ b/test/c/issue401.sail
@@ -0,0 +1,20 @@
+default Order dec
+$include <prelude.sail>
+
+union U('t :  Type) = {
+  A : ('t, bits(1))
+}
+
+val f : U(unit) -> bits(1)
+function f(u) = {
+  match u {
+     A(_, bs) => bs
+  }
+}
+
+val main : unit -> unit
+function main () = {
+  let u : U(unit) = A((), 0b1) in
+  let res = f(u) in
+  print_endline("ok");
+}