3 files changed, 19 insertions, 2 deletions

diff --git a/test/typecheck/pass/bind_typ_var.sail b/test/typecheck/pass/bind_typ_var.sail
new file mode 100644
index 00000000..c442d6a8
--- /dev/null
+++ b/test/typecheck/pass/bind_typ_var.sail
@@ -0,0 +1,17 @@
+
+val mk_vector : unit -> {'n, 'n in {32, 64}. vector('n, dec, bit)}
+
+val mk_square : unit -> {'n 'm, 'n = 'm. vector('n, dec, vector('m, dec, bit))}
+
+val test : unit -> unit
+
+function test () = {
+  let v as vector('len, _, _) = mk_vector ();
+  // could still be
+  let v2 as 'len2 = mk_vector ();
+  let matrix as vector('width, _, 'height) = mk_square ();
+  _prove(constraint('width = 'height));
+  _prove(constraint('len = 32 | 'len = 64));
+  _prove(constraint('len2 = 32 | 'len2 = 64));
+  ()
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
index 67355f59..62788484 100644
--- a/test/typecheck/pass/global_type_var/v1.expect
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -3,4 +3,4 @@ Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23,
 let _ = test(32)
 
 Tried performing type coercion on 32
-Failed because atom<32> is not a subtype of atom<'size> in context ('size = 32 | 'size = 64)
+Failed because atom<32> is not a subtype of atom<'size> in context 'size = 'ex1#, ('ex1# = 32 | 'ex1# = 64)
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
index fb31fbed..1b9bb23d 100644
--- a/test/typecheck/pass/global_type_var/v2.expect
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -3,4 +3,4 @@ Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23,
 let _ = test(64)
 
 Tried performing type coercion on 64
-Failed because atom<64> is not a subtype of atom<'size> in context ('size = 32 | 'size = 64)
+Failed because atom<64> is not a subtype of atom<'size> in context 'size = 'ex1#, ('ex1# = 32 | 'ex1# = 64)