From 4b299673151b4762559c53bd36c76c96a2269a86 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Fri, 13 Dec 2019 11:13:03 -0800
Subject: [PATCH] Add regression test for issue #614.

---
 tests/issues/issue614.cry         |  6 ++++++
 tests/issues/issue614.icry        |  1 +
 tests/issues/issue614.icry.stdout | 16 ++++++++++++++++
 3 files changed, 23 insertions(+)
 create mode 100644 tests/issues/issue614.cry
 create mode 100644 tests/issues/issue614.icry
 create mode 100644 tests/issues/issue614.icry.stdout

diff --git a/tests/issues/issue614.cry b/tests/issues/issue614.cry
new file mode 100644
index 000000000..8c870e7c2
--- /dev/null
+++ b/tests/issues/issue614.cry
@@ -0,0 +1,6 @@
+f : {m, n, k} (n == max 2 m k == m + 1) => [m] -> [k][n]
+f x = zero
+
+
+g : {n, k} (fin n, fin k, 0 < n <= k) => [n] -> [k]
+g x = sext x
diff --git a/tests/issues/issue614.icry b/tests/issues/issue614.icry
new file mode 100644
index 000000000..21b6484ab
--- /dev/null
+++ b/tests/issues/issue614.icry
@@ -0,0 +1 @@
+:l issue614.cry
diff --git a/tests/issues/issue614.icry.stdout b/tests/issues/issue614.icry.stdout
new file mode 100644
index 000000000..5c55abeca
--- /dev/null
+++ b/tests/issues/issue614.icry.stdout
@@ -0,0 +1,16 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+
+[error] at issue614.cry:1:18--1:20 and issue614.cry:1:31--1:33
+    The fixities of
+      • (==) (precedence 20, non-associative)
+      • (==) (precedence 20, non-associative)
+    are not compatible.
+    You may use explicit parentheses to disambiguate.
+[error] at issue614.cry:5:29--5:30 and issue614.cry:5:33--5:35
+    The fixities of
+      • (<) (precedence 30, non-associative)
+      • (<=) (precedence 30, non-associative)
+    are not compatible.
+    You may use explicit parentheses to disambiguate.