Coq: add missing effectful existential unpacking case

2 files changed, 21 insertions, 1 deletions

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index cce3c2d3..90484598 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1729,7 +1729,11 @@ let doc_exp, doc_let =
             if effectful eff
             then "autocast_m", "projT1_m"
             else "autocast",   "projT1" in
-          let epp = if unpack && not (effectful eff) then string proj_id ^/^ parens epp else epp in
+          (* We need to unpack an existential if it's generated by a pure
+             computation, or if the monadic binding isn't expecting one. *)
+          let epp = if unpack && not (effectful eff && packeff)
+                    then string proj_id ^/^ parens epp
+                    else epp in
           let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in
           let epp =
             if effectful eff && packeff && not unpack
diff --git a/test/coq/pass/unpacking.sail b/test/coq/pass/unpacking.sail
new file mode 100644
index 00000000..d0143f40
--- /dev/null
+++ b/test/coq/pass/unpacking.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+val f : int -> {'n, 'n >= 0. int('n)} effect {rreg}
+val g : int -> {'n, 'n >= 0. int('n)}
+
+val test : unit -> int effect {rreg}
+
+function test() = {
+  let x1 : {'n, 'n >= 0. int('n)} = f(5);
+  let x2 : int = f(6);
+  let y1 : {'n, 'n >= 0. int('n)} = g(7);
+  let y2 : int = g(8);
+  x1 + x2 + y1 + y2
+}