Panic with local definiton that uses constraint guards without a type signature

[RyanGlScott]

If you give this Cryptol this program:

module Bug where

f : ()
f = g
  where
    g | 0 == 0 => ()

Then Cryptol will panic:

$ ~/Software/cryptol-3.1.0/bin/cryptol Bug.cry 
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.1.0
https://cryptol.net  :? for help

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

%< --------------------------------------------------- 
  Revision:  65397a491bddc3b4e8f41053106ce8859387d662
  Branch:    release-3.1.0 (uncommited files present)
  Location:  [TypeCheck] checkMonoB
  Message:   Used constraint guards without a signature at 
             (at Bug.cry:6:5--6:6, g)
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.1.0-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/TypeCheck/Infer.hs:1622:17 in cryptol-3.1.0-inplace:Cryptol.TypeCheck.Infer
%< ---------------------------------------------------

Note that making slight changes to the program will change the panic to a proper Cryptol error message:

• If you give g a type signature:

  module Bug where
  
  f : ()
  f = g
    where
      g : ()
      g | 0 == 0 => ()
  

  Then Cryptol will error thusly:

  $ ~/Software/cryptol-3.1.0/bin/cryptol Bug.cry 
  ┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
  ┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
  ┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
  version 3.1.0
  https://cryptol.net  :? for help
  
  Loading module Cryptol
  Loading module Bug
  [error] at Bug.cry:7:5--7:6:
    Local declaration `g` may not use constraint guards.
    Constraint guards may only appear at the top-level of a module.
  

• If you use constraint guards at the top level without a type signature, as in this program:

  module Bug where
  
  f | 0 == 0 => ()
  

  Then Cryptol will error thusly:

  $ ~/Software/cryptol-3.1.0/bin/cryptol Bug.cry 
  ┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
  ┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
  ┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
  version 3.1.0
  https://cryptol.net  :? for help
  
  Loading module Cryptol
  Loading module Bug
  At Bug.cry:3:1--3:2: Declarations using constraint guards require an explicit type signature.
  

[RyanGlScott]

This issue involves checkNumericConstraintGuardsOK. This function makes the assumption that by the time it is invoked, all numeric constraint guard expressions have been checked to have a type signature. (See the comment here.) This isn't actually true, however. The code in Cryptol.Parser.ExpandPropGuards does check that top-level numeric constraint guards have type signatures, but it does not check any constraint guards in where expressions.

Two ways we could fix this:

1. Make Cryptol.Parser.ExpandPropGuards recurse into where expressions and reject any nested constraint guards it encounters. (This would make this error message later in the typechecker unreachable, so we could remove it.)
2. Do not assume that by the time checkNumericConstraintGuardsOK is invoked, we have checked all constraint guards to have a type signature.

I am leaning more towards option (1), since this is the sort of thing that we could easily detect (and reject) in the parser, well before we get to the typechecker.

[yav]

Yeah, I also think (1) is the way to go.