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

@@ -5,6 +5,9 @@
 * 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

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 $

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

tests/issues/issue1593.icry

@@ -0,0 +1 @@
+:load issue1593.cry

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`.

tests/issues/issue1693.cry

@@ -0,0 +1,4 @@
+f : {n} [n] -> [n+1]
+f x
+  | (fin n) => x # [False]
+  | (inf n) => x

tests/issues/issue1693.icry

@@ -0,0 +1 @@
+:load issue1693.cry

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