Coq: be more careful about merging Sail variables and type variables

In particular, spot variable shadowing and handle (n as 'm) patterns.

1 files changed, 10 insertions, 0 deletions

diff --git a/test/coq/pass/rebind.sail b/test/coq/pass/rebind.sail
new file mode 100644
index 00000000..247c1d6d
--- /dev/null
+++ b/test/coq/pass/rebind.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+val foo : forall 'n, 'n >= 0. (int('n),bits('n)) -> bits(5 + 'n)
+
+function foo(n,x) = {
+  let (n as 'm) = 5 in
+  (append((x : bits('n)),sail_ones(n)) : bits('m + 'n))
+}