Merge pull request #1695 from GaloisInc/issue1593-issue1693

Abort early after type-checking malformed constraint guards

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

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 $
@@ -1434,7 +1439,7 @@ checkPropGuardCase asmps (P.PropGuardCase guards e0) =
   getT ti =
     case ti of
       P.PosInst t    -> t
-      P.NamedInst {} -> bad "Unexpeceted NamedInst"
+      P.NamedInst {} -> bad "Unexpected NamedInst"
 
   bad msg = panic "checkPropGuardCase" [msg]
 

src/Cryptol/TypeCheck/Type.hs

@@ -965,7 +965,7 @@ pNegNumeric prop =
 
   where
   bad = panic "pNegNumeric"
-          [ "Unexpeceted numeric constraint:"
+          [ "Unexpected numeric constraint:"
           , pretty prop
           ]
 

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