From eaab5e9f4077b560d947f7836aba78ebef8aeab3 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 22 Sep 2020 23:17:39 -0700
Subject: [PATCH] Add regression test for #894.

---
 tests/issues/issue894.cry         | 4 ++++
 tests/issues/issue894.icry        | 2 ++
 tests/issues/issue894.icry.stdout | 7 +++++++
 3 files changed, 13 insertions(+)
 create mode 100644 tests/issues/issue894.cry
 create mode 100644 tests/issues/issue894.icry
 create mode 100644 tests/issues/issue894.icry.stdout

diff --git a/tests/issues/issue894.cry b/tests/issues/issue894.cry
new file mode 100644
index 000000000..42fcc9b85
--- /dev/null
+++ b/tests/issues/issue894.cry
@@ -0,0 +1,4 @@
+type Int n = Integer
+
+foo : {n} (fin n) => [n] -> Int n
+foo x = `n
diff --git a/tests/issues/issue894.icry b/tests/issues/issue894.icry
new file mode 100644
index 000000000..9f63ece9d
--- /dev/null
+++ b/tests/issues/issue894.icry
@@ -0,0 +1,2 @@
+:l issue894.cry
+:t foo 0x1
diff --git a/tests/issues/issue894.icry.stdout b/tests/issues/issue894.icry.stdout
new file mode 100644
index 000000000..8d8cae5de
--- /dev/null
+++ b/tests/issues/issue894.icry.stdout
@@ -0,0 +1,7 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+[warning] at issue894.cry:1:10--1:11 Unused name: n
+[warning] at issue894.cry:1:6--1:9:
+  Assuming  n to have a numeric type
+foo 0x1 : Int 4