`pNegNumeric` panic with `prime` numeric constraint guard

[RyanGlScott]

The following program causes the master branch of Cryptol (as of commit 6de5aa8) to panic:

f : {n} [n]
f | prime n => zero
  | fin n => zero
  | n == n => zero

$ cabal -v0 run exe:cryptol -- Bug.cry 
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.5.0.99 (6de5aa8, 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:  6de5aa8cc28e4b5fed8438a41a3549ecbe857002
  Branch:    master (uncommited files present)
  Location:  pNegNumeric
  Message:   Unexpected numeric constraint:
             prime n`901
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.5.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/TypeCheck/Type.hs:1018:9 in cryptol-3.5.0.99-inplace:Cryptol.TypeCheck.Type
%< --------------------------------------------------- 

[RyanGlScott]

Looking at the pNegNumeric function, we have:

cryptol/src/Cryptol/TypeCheck/Type.hs

Lines 982 to 1008 in 6de5aa8

	{-| `pNegNumeric` negates a simple (i.e., not And, not prime, etc) prop
	over numeric type vars. The result is a conjunction of properties. -}
	pNegNumeric :: Prop -> [Prop]
	pNegNumeric prop =
	case tNoUser prop of
	TCon tcon tys ->
	case tcon of
	PC pc ->
	case pc of
	-- not (x == y) <=> x /= y
	PEqual -> [TCon (PC PNeq) tys]
	-- not (x /= y) <=> x == y
	PNeq -> [TCon (PC PEqual) tys]
	-- not (x >= y) <=> x /= y and y >= x
	PGeq -> [TCon (PC PNeq) tys, TCon (PC PGeq) (reverse tys)]
	-- not (fin x) <=> x == Inf
	PFin | [ty] <- tys -> [ty =#= tInf]
	| otherwise -> bad
	-- not True <=> 0 == 1
	PTrue -> [TCon (PC PEqual) [tZero, tOne]]
	_ -> bad

That is, it computes the negation of a numeric constraint. Unfortunately, I don't believe there is any way to express the negation of prime p using the primitive constraints that Cryptol provides...

[yav]

Interesting. Perhaps we should add a not_prime predicate to handle this. We only solve these for concrete values anyway, so I don't foresee complications.

[RyanGlScott]

Fixed in #2091.