diff --git a/tests/issues/issue723.cry b/tests/issues/issue723.cry
new file mode 100644
index 000000000..0ce7dc7f3
--- /dev/null
+++ b/tests/issues/issue723.cry
@@ -0,0 +1,7 @@
+f : {n} (fin n) => [n] -> [n]
+f x = g x
+  where
+    m1 = zero # x
+
+    g : {k} (fin k) => [k] -> [k]
+    g m0 = m0 ^ m1
diff --git a/tests/issues/issue723.icry b/tests/issues/issue723.icry
new file mode 100644
index 000000000..ed91f861c
--- /dev/null
+++ b/tests/issues/issue723.icry
@@ -0,0 +1 @@
+:l issue723.cry
diff --git a/tests/issues/issue723.icry.stdout b/tests/issues/issue723.icry.stdout
new file mode 100644
index 000000000..763b8421a
--- /dev/null
+++ b/tests/issues/issue723.icry.stdout
@@ -0,0 +1,20 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+[warning] at issue723.cry:4:10--4:18:
+  Defaulting type argument 'front' of '(#)' to 0
+
+[error] at issue723.cry:7:5--7:19:
+  Failed to validate user-specified signature.
+    in the definition of 'Main::g', at issue723.cry:7:5--7:6,
+    we need to show that
+      for any type k
+      assuming
+        • fin k
+      the following constraints hold:
+        • k >= n`908
+            arising from
+            matching types
+            at issue723.cry:7:17--7:19
+  where
+  n`908 is signature variable 'n' at issue723.cry:1:6--1:7