Add regression test for #723.

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

tests/issues/issue723.icry

@@ -0,0 +1 @@
+:l issue723.cry

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