Coq: add missing effectful existential unpacking case

1 files changed, 5 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