Coq: replace n_constraints with equivalent bool variables

Prevents some type variables that came from unpacking existentials
leaking into generated Coq types.

1 files changed, 16 insertions, 0 deletions

diff --git a/test/coq/pass/unbound_ex_tyvars.sail b/test/coq/pass/unbound_ex_tyvars.sail
new file mode 100644
index 00000000..f99b1bd1
--- /dev/null
+++ b/test/coq/pass/unbound_ex_tyvars.sail
@@ -0,0 +1,16 @@
+$include <prelude.sail>
+
+/* We currently produce a rich type for the guard of the if that's
+   visible in the Coq output.  The raw Sail type involves unbound type
+   variables that were existentially bound in x, so in order to print
+   out a useful Coq type we now rewrite it in terms of x. */
+
+val isA : unit -> bool effect {rreg}
+val isB : unit -> bool effect {rreg}
+val isC : unit -> bool effect {rreg}
+val foo : bool -> bool effect {rreg}
+
+function foo(b) = {
+  let x = (b | isA()) & isB();
+  if x | isC() then true else false
+}