Better error message for when type variable instances are not found for :checking

[rybla]

Addresses #1345

The problem: due to nondeterminism in the SMT solver, using :check on a property with numeric constraints can sometimes find and sometimes not find concrete instances for some numeric type variables. If the instance is not found, then the user is presented with the error message Cannot evaluate polymorphic value. which is misleading because, in fact, another run of :check might find an instance and to testing just fine.

In Cryptol.REPL.Monad, this PR introduces a new constructor to REPLException,

data REPLException =
  ...
  | InstantiationsNotFound Schema
  ...

which is very similar to EvalPolyError, which is the misleading exception raised in #1345. The exception InstantiationsNotFound is only thrown when the user :checks a property, and defaultReplExpr' fails to find a model (assignment of type variables) that satisfies the type constraints (list of Props). This failure mode is now reflected in the type of replEvalCheckedExpr which now returns REPL (Maybe ...), which allows the different call sites of replEvalCheckedExpr to handle the solver failure differently.

Now, the feedback a user gets they try the example in #1345 is:

Main> :check
property NTTandNTT'areInverses 
Cannot find instantiations for some type variables.
Type: {N, k, g, n}
  (prime N, N == 1 + k * n, fin k, g ^^ (N - 1) % N == 1, N > g,
   fin n) =>
  [n](Z N) -> Bit
Main> :check
property NTTandNTT'areInverses Showing a specific instance of polymorphic result:
  * Using '2' for signature variable 'N'
  * Using '1' for signature variable 'k'
  * Using '1' for signature variable 'g'
  * Using '1' for signature variable 'n'
Using exhaustive testing.
Passed 2 tests.
Q.E.D.

However, further work needs to be done to properly support testing for polymorphic properties. This PR merely makes the lacking capability less confusing for the user.

[robdockins]

Overall, looks good to me, with a minor style nitpick.