3 files changed, 66 insertions, 0 deletions

diff --git a/test/typecheck/pass/poly_vector.sail b/test/typecheck/pass/poly_vector.sail
new file mode 100644
index 00000000..93676a1b
--- /dev/null
+++ b/test/typecheck/pass/poly_vector.sail
@@ -0,0 +1,24 @@
+default Order dec
+
+$include <prelude.sail>
+
+$ifndef FEATURE_BITVECTOR_TYPE
+type bitvector('n, 'ord) = vector('n, 'ord, bit)
+$endif
+
+val "to_generic" : forall 'n. bitvector('n, dec) -> vector('n, dec, bit)
+
+val "print_endline" : string -> unit
+
+function my_length forall 'n ('a : Type). (xs: vector('n, dec, 'a)) -> int('n) = {
+  length(xs)
+}
+
+function main() -> unit = {
+  let xs : bits(32) = 0xFFFF_FFFF;
+  if my_length(to_generic(xs)) == 32 then {
+    print_endline("ok")
+  } else {
+    print_endline("false")
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/poly_vector/v1.expect b/test/typecheck/pass/poly_vector/v1.expect
new file mode 100644
index 00000000..9c4da56f
--- /dev/null
+++ b/test/typecheck/pass/poly_vector/v1.expect
@@ -0,0 +1,18 @@
+Type error:
+[poly_vector/v1.sail]:19:5-24
+19 |  if my_length(xs) == 32 then {
+   |     ^-----------------^
+   | No overloading for (operator ==), tried:
+   | * eq_int
+   |    No valid casts resulted in unification
+   | * eq_bit
+   |    No valid casts resulted in unification
+   | * eq_bool
+   |    No valid casts resulted in unification
+   | * eq_unit
+   |    No valid casts resulted in unification
+   | * eq_bit
+   |    No valid casts resulted in unification
+   | * eq_bits
+   |    No valid casts resulted in unification
+   | 
diff --git a/test/typecheck/pass/poly_vector/v1.sail b/test/typecheck/pass/poly_vector/v1.sail
new file mode 100644
index 00000000..cad74ddc
--- /dev/null
+++ b/test/typecheck/pass/poly_vector/v1.sail
@@ -0,0 +1,24 @@
+default Order dec
+
+$include <prelude.sail>
+
+$ifndef FEATURE_BITVECTOR_TYPE
+type bitvector('n, 'ord) = vector('n, 'ord, bit)
+$endif
+
+val "to_generic" : forall 'n. bitvector('n, dec) -> vector('n, dec, bit)
+
+val "print_endline" : string -> unit
+
+function my_length forall 'n ('a : Type). (xs: vector('n, dec, 'a)) -> int('n) = {
+  length(xs)
+}
+
+function main() -> unit = {
+  let xs : bits(32) = 0xFFFF_FFFF;
+  if my_length(xs) == 32 then {
+    print_endline("ok")
+  } else {
+    print_endline("false")
+  }
+}
\ No newline at end of file