Handle type variables generated while inferring applications in monomorphisation

Also handle any type variables from assignments and degrade gracefully
during constant propagation when unification is not possible.

2 files changed, 33 insertions, 0 deletions

diff --git a/test/mono/assign_range.sail b/test/mono/assign_range.sail
new file mode 100644
index 00000000..baf3ed43
--- /dev/null
+++ b/test/mono/assign_range.sail
@@ -0,0 +1,32 @@
+default Order dec
+$include <prelude.sail>
+
+val use : forall 'n, 'n >= 8. int('n) -> int
+
+function use(n) = {
+  let x : bits('n) = sail_sign_extend(0x12, n);
+  unsigned(x)
+}
+
+val test1 : forall 'n, 'n in {2,4}. int('n) -> int
+
+function test1(n) = {
+  size : {'m, 'm >= 8. int('m)} = n * 8;
+  use(size)
+}
+
+val test2 : forall 'n, 'n in {2,4}. int('n) -> int
+
+function test2(n) = {
+  size : range(8,32) = n * 8;
+  use(size)
+}
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+  assert(test1(2) == 18);
+  assert(test1(4) == 18);
+  assert(test2(2) == 18);
+  assert(test2(4) == 18);
+}
diff --git a/test/mono/pass/assign_range b/test/mono/pass/assign_range
new file mode 100644
index 00000000..13642ef2
--- /dev/null
+++ b/test/mono/pass/assign_range
@@ -0,0 +1 @@
+assign_range.sail -auto_mono