Fix issue 429

src/lib/jib_compile.ml

@@ -679,7 +679,13 @@ module Make (C : CONFIG) = struct
               | 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)
+              | None -> begin
+                  match List.find_opt (fun (id, _) -> Id.compare id ctor = 0) ctors with
+                  | Some (_, ctor_ctyp) -> (unifiers, ctor_ctyp)
+                  | None ->
+                      Reporting.unreachable l __POS__
+                        ("Expected constructor " ^ string_of_id ctor ^ " for " ^ full_string_of_ctyp ctyp)
+                end
             in
             let pre, instrs, cleanup, ctx =
               compile_match ctx apat (V_ctor_unwrap (cval, (ctor, unifiers), ctor_ctyp)) case_label

src/lib/jib_util.mli

@@ -137,6 +137,8 @@ val string_of_cval : cval -> string
 val string_of_clexp : clexp -> string
 val string_of_instr : instr -> string
 
+val full_string_of_ctyp : ctyp -> string
+
 (** {1. Functions and modules for working with ctyps} *)
 
 val map_ctyp : (ctyp -> ctyp) -> ctyp -> ctyp

test/c/issue429.expect

@@ -0,0 +1 @@
+ok

test/c/issue429.sail

@@ -0,0 +1,35 @@
+default Order dec
+
+$include <prelude.sail>
+
+union two_bitvectors('n : Int) = {
+    BV1 : bits('n),
+    BV2 : bits('n),
+}
+
+val get_value32 : two_bitvectors(32) -> bits(32)
+
+function get_value32(tbv) = {
+    match tbv {
+        BV1(bs) => bs,
+        BV2(bs) => bs,
+    }
+}
+
+register R : bits(32)
+
+val test : forall 'n. bits('n) -> unit
+
+function test(bv) = {
+    let x : two_bitvectors('n) = BV2(bv);
+    if length(bv) == 32 then {
+        R = get_value32(x);
+    }
+}
+
+val main : unit -> unit
+
+function main() = {
+    test(0xABCD_0000);
+    print_endline("ok")
+}