Panic when trying to evaluate or prove expressions in a parameterized module

[brianhuffman]

module issue where

parameter
  type foo : #
  type constraint (fin foo)

bad : [foo] -> Bit
property bad x = True

nope : [foo]
nope = 0

Now running either :prove bad or nope at the REPL causes a panic:

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

%< ---------------------------------------------------
  Revision:  607a55c76a26e549f31e9687dcb16381659c4b65
  Branch:    master (uncommited files present)
  Location:  [Eval] evalType
  Message:   type variable not bound

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

%< ---------------------------------------------------
  Revision:  607a55c76a26e549f31e9687dcb16381659c4b65
  Branch:    master (uncommited files present)
  Location:  [Eval] evalExpr
  Message:   var `issue::nope` is not defined

[brianhuffman]

Turns out it's worse than I thought: The expression doesn't even need to depend on the module type parameter. In the following module, either :prove yes, yes, or :check yes causes a panic that exits the REPL.

module issue where

parameter
  type foo : #

yes : Bit
yes = True

[yav]

Yep, proving in the context of parameterized modules is not implemented at all.

The main issue is that we can't currently represent symbolic types (i.e., all evaluation is expected to result in a concrete type). There's probably a fair bit of work to get this to work.

In the mean time, we should probably issue some more useful message (e.g. "prove is not supported for parameterized modules"), rather than panicking.

I don't think it is worth the effort to make things work in parameterized modules, that do not actually depend on the parameters work, though.

I'll have a go at fixing this.