Unexpeceted numeric constraint panic with malformed constraint guards

[RyanGlScott]

While torturing stress-testing Cryptol recently, I discovered that I can make it panic if I use malformed constraint guards:

f : {n, a} [n]a -> [8]
f x
  | n == 1 => 0
  | n != 1 => 1
  | Eq a   => 2 // Malformed

$ cabal run exe:cryptol -- Bug.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.0.0.99 (d602858, modified)
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Main
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  d602858ea498360126633209d98367654d461995
  Branch:    master (uncommited files present)
  Location:  pNegNumeric
  Message:   Unexpeceted numeric constraint:
             Eq a`909
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.0.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/TypeCheck/Type.hs:951:9 in cryptol-3.0.0.99-inplace:Cryptol.TypeCheck.Type
%< ---------------------------------------------------

I imagine that constraint guards were never meant to contain constraints like Eq a, but nevertheless, we should reject them if encountered. Interestingly, Cryptol does give a proper error message if I move the malformed guard to the top:

f : {n, a} [n]a -> [8]
f x
  | Eq a   => 2 // Malformed
  | n == 1 => 0
  | n != 1 => 1

$ cabal run exe:cryptol -- Bug.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.0.0.99 (d602858, modified)
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Main
[error] at Bug.cry:3:5--3:9:
  `Eq` may not be used in a constraint guard.
  Constraint guards support only numeric comparisons and `fin`.

[RyanGlScott]

The culprit is the code for typechecking numeric constraint guards:

cryptol/src/Cryptol/TypeCheck/Infer.hs

Lines 1266 to 1271 in 6c5bca3

	P.DPropGuards cases0 -> do
	asmps1 <- applySubstPreds asmps0
	t1 <- applySubst t0
	cases1 <- mapM checkPropGuardCase cases0
	exh <- checkExhaustive (P.bName b) as asmps1 (map fst cases1)

Here, checkPropGuardCase ensures that the guards only consist of numeric constraints, and it is ultimately what throws the `Eq` may not be used in a constraint guard. error message. checkExhaustive checks if the guards are exhaustive, and it transitively invokes pNegNumeric, which will panic if it encounters a constraint like Eq a.

At first glance, it seems like calling checkPropGuardCase before checkExhaustive would cause Cryptol to throw a proper error message on invalid numeric guard constraints like Eq a before it ever has a chance to call pNegNumeric. However, this isn't the case, since checkPropGuardCase merely calls recordError:

cryptol/src/Cryptol/TypeCheck/Kind.hs

Line 89 in 6c5bca3

_ -> recordError (InvalidConstraintGuard ps)

recordError doesn't outright abort execution, and it will cause Cryptol to proceed in case there are other errors that may need to be reported at the same time. This ends up biting us, since Cryptol proceeds to invoke pNegNumeric and panic before it ever has a chance to report the earlier error due to Eq a.

One possible solution is to abort earlier when checkPropGuardCase encounters an error. That is, do something like this:

diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs
index 4d142697..acda9938 100644
--- a/src/Cryptol/TypeCheck/Infer.hs
+++ b/src/Cryptol/TypeCheck/Infer.hs
@@ -1267,6 +1267,7 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
           asmps1 <- applySubstPreds asmps0
           t1     <- applySubst t0
           cases1 <- mapM checkPropGuardCase cases0
+          abortIfErrors
 
           exh <- checkExhaustive (P.bName b) as asmps1 (map fst cases1)
           unless exh $

This suffices to fix the panic. I'm unclear if this is the best place to call abortIfErrors, or if this is even a recommended way to abort early.

[WeeknightMVP]

Just encountered a similar panic with an inf constraint guard:

module Towel where

towel : {w} [inf]
towel
  | fin w => zero
  | inf w => zero

~/workspace/scratch$ cryptol
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.1.0.99 (5bbc3dc, modified)
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol> :m Towel
Loading module Cryptol
Loading module Towel
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< ---------------------------------------------------
  Revision:  697d6a7f9745f4e23db2983bc634d3eb5f26c3f0
  Branch:    master (uncommited files present)
  Location:  pNegNumeric
  Message:   Unexpeceted numeric constraint:
             ?err
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.1.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/TypeCheck/Type.hs:967:9 in cryptol-3.1.0.99-inplace:Cryptol.TypeCheck.Type

Swapping the order of constraint guards to lead with the offending inf gives an unclear error:

~/workspace/scratch$ cryptol
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.1.0.99 (5bbc3dc, modified)
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol> :m Towel
Loading module Cryptol
Loading module Towel

[error] at ~/workspace/scratch/Towel.cry:3:9--3:18:
  Incorrect type form.
    Expected: a constraint
    Inferred: a numeric type
[error] at ~/workspace/scratch/Towel.cry:5:5--5:10:
  Incorrect type form.
    Expected: a constraint
    Inferred: a numeric type

[RyanGlScott]

An example very similar to towel (in #1593 (comment)) was reported in #1693.