From 6e417aa3d12eae3076a75da3e4465ebdd37002ac Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Mon, 1 Jul 2024 13:04:21 -0400
Subject: [PATCH] Abort early after type-checking malformed constraint guards

Checking ill-typed constraint guards for exhaustivity can cause Cryptol to
panic. If we detect any type errors after type-checking the guards, we now
abort early and report any recorded errors instead of proceeding to check
exhaustivity.

Fixes #1593. Fixes #1693.
---
 CHANGES.md                         |  4 ++++
 src/Cryptol/TypeCheck/Infer.hs     |  5 +++++
 tests/issues/issue1593.cry         |  5 +++++
 tests/issues/issue1593.icry        |  1 +
 tests/issues/issue1593.icry.stdout |  7 +++++++
 tests/issues/issue1693.cry         |  4 ++++
 tests/issues/issue1693.icry        |  1 +
 tests/issues/issue1693.icry.stdout | 12 ++++++++++++
 8 files changed, 39 insertions(+)
 create mode 100644 tests/issues/issue1593.cry
 create mode 100644 tests/issues/issue1593.icry
 create mode 100644 tests/issues/issue1593.icry.stdout
 create mode 100644 tests/issues/issue1693.cry
 create mode 100644 tests/issues/issue1693.icry
 create mode 100644 tests/issues/issue1693.icry.stdout

diff --git a/CHANGES.md b/CHANGES.md
index 833e1c96..dc85a51e 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -10,6 +10,10 @@
 
 * Fix #1685, which caused Cryptol to panic when given a local definition without
   a type signature that uses numeric constraint guards.
+
+* Fix #1593 and #1693, two related bugs that would cause Cryptol to panic when
+  checking ill-typed constraint guards for exhaustivity.
+
 # 3.1.0 -- 2024-02-05
 
 ## Language changes
diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs
index 1853b1b0..62d6c37b 100644
--- a/src/Cryptol/TypeCheck/Infer.hs
+++ b/src/Cryptol/TypeCheck/Infer.hs
@@ -1234,6 +1234,11 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
           asmps1 <- applySubstPreds asmps0
           t1     <- applySubst t0
           cases1 <- mapM (checkPropGuardCase asmps1) cases0
+          -- If we recorded any errors when type-checking the constraint guards,
+          -- then abort early. We don't want to check exhaustivity if there are
+          -- malformed constraints, as these can cause panics elsewhere during
+          -- exhaustivity checking (see the `issue{1593,1693}` test cases).
+          abortIfErrors
 
           exh <- checkExhaustive (P.bName b) as asmps1 (map fst cases1)
           unless exh $
diff --git a/tests/issues/issue1593.cry b/tests/issues/issue1593.cry
new file mode 100644
index 00000000..921701da
--- /dev/null
+++ b/tests/issues/issue1593.cry
@@ -0,0 +1,5 @@
+f : {n, a} [n]a -> [8]
+f x
+  | n == 1 => 0
+  | n != 1 => 1
+  | Eq a   => 2 // Malformed
diff --git a/tests/issues/issue1593.icry b/tests/issues/issue1593.icry
new file mode 100644
index 00000000..b2f871dd
--- /dev/null
+++ b/tests/issues/issue1593.icry
@@ -0,0 +1 @@
+:load issue1593.cry
diff --git a/tests/issues/issue1593.icry.stdout b/tests/issues/issue1593.icry.stdout
new file mode 100644
index 00000000..c317c8df
--- /dev/null
+++ b/tests/issues/issue1593.icry.stdout
@@ -0,0 +1,7 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+
+[error] at issue1593.cry:5:5--5:9:
+  `Eq` may not be used in a constraint guard.
+  Constraint guards support only numeric comparisons and `fin`.
diff --git a/tests/issues/issue1693.cry b/tests/issues/issue1693.cry
new file mode 100644
index 00000000..6d634499
--- /dev/null
+++ b/tests/issues/issue1693.cry
@@ -0,0 +1,4 @@
+f : {n} [n] -> [n+1]
+f x
+  | (fin n) => x # [False]
+  | (inf n) => x
diff --git a/tests/issues/issue1693.icry b/tests/issues/issue1693.icry
new file mode 100644
index 00000000..d174791b
--- /dev/null
+++ b/tests/issues/issue1693.icry
@@ -0,0 +1 @@
+:load issue1693.cry
diff --git a/tests/issues/issue1693.icry.stdout b/tests/issues/issue1693.icry.stdout
new file mode 100644
index 00000000..1f8d37a8
--- /dev/null
+++ b/tests/issues/issue1693.icry.stdout
@@ -0,0 +1,12 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+
+[error] at issue1693.cry:1:5--1:21:
+  Incorrect type form.
+    Expected: a constraint
+    Inferred: a numeric type
+[error] at issue1693.cry:4:5--4:12:
+  Incorrect type form.
+    Expected: a constraint
+    Inferred: a numeric type