5 files changed, 51 insertions, 0 deletions

diff --git a/test/typecheck/pass/Replicate.sail b/test/typecheck/pass/Replicate.sail
new file mode 100644
index 00000000..03954a9f
--- /dev/null
+++ b/test/typecheck/pass/Replicate.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <smt.sail>
+$include <prelude.sail>
+
+val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
+  (implicit('N), bits('M)) -> bits('N) effect {escape}
+
+function Replicate (N, x) = {
+    assert('N % 'M == 0);
+    replicate_bits(x, 'N / 'M)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect
new file mode 100644
index 00000000..92c6d7cd
--- /dev/null
+++ b/test/typecheck/pass/Replicate/v1.expect
@@ -0,0 +1,8 @@
+Type error:
+[Replicate/v1.sail]:11:4-30
+11 |    replicate_bits(x, 'N / 'M)
+   |    ^------------------------^
+   | Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, div(__id(N), bitvector_length(x)))
+   | Coercion failed because:
+   | Mismatched argument types in subtype check
+   | 
diff --git a/test/typecheck/pass/Replicate/v1.sail b/test/typecheck/pass/Replicate/v1.sail
new file mode 100644
index 00000000..69f2bb6f
--- /dev/null
+++ b/test/typecheck/pass/Replicate/v1.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <smt.sail>
+$include <prelude.sail>
+
+val Replicate : forall ('M : Int) ('N : Int), 'M >= 0.
+  (implicit('N), bits('M)) -> bits('N) effect {escape}
+
+function Replicate (N, x) = {
+    assert('N % 'M == 0);
+    replicate_bits(x, 'N / 'M)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect
new file mode 100644
index 00000000..0dec309f
--- /dev/null
+++ b/test/typecheck/pass/Replicate/v2.expect
@@ -0,0 +1,8 @@
+Type error:
+[Replicate/v2.sail]:10:4-30
+10 |    replicate_bits(x, 'N / 'M)
+   |    ^------------------------^
+   | Tried performing type coercion from {('ex42# : Int), true. vector(('M * 'ex42#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x)))
+   | Coercion failed because:
+   | Mismatched argument types in subtype check
+   | 
diff --git a/test/typecheck/pass/Replicate/v2.sail b/test/typecheck/pass/Replicate/v2.sail
new file mode 100644
index 00000000..e54b0af4
--- /dev/null
+++ b/test/typecheck/pass/Replicate/v2.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
+  (implicit('N), bits('M)) -> bits('N) effect {escape}
+
+function Replicate (N, x) = {
+    assert('N % 'M == 0);
+    replicate_bits(x, 'N / 'M)
+}
\ No newline at end of file