Handle TError in constrant guard translator (#1935)

When using constraint guards in instantiations of parameterized modules,
Cryptol may replace impossible constraints with `TError`. To support
this behavior, this change adds a case to
`importNumericConstraintAsBool` that translates those `TError` constraints
to `False`. This is consistent with
[`checkProp` in Cryptol](https://github.com/GaloisInc/cryptol/blob/3973b15236ace5c11fdfabbf811d97daee7885ed/src/Cryptol/Eval.hs#L247),
which is the Cryptol function that handles evaluation of constraint
guard constraints.

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -356,6 +356,7 @@ importNumericConstraintAsBool sc env prop =
       rhs' <- importType sc env rhs
       scAnd sc lhs' rhs'
     C.TCon (C.PC C.PTrue) [] -> scBool sc True
+    C.TCon (C.TError _) _ -> scBool sc False
     C.TUser _ _ t -> importNumericConstraintAsBool sc env t
     _ -> panic
       "importNumericConstraintAsBool"

intTests/test_constraint_guards/Parameterized.cry

@@ -6,4 +6,8 @@ parameter
 
 // Constraint guard with type dependent on module parameter value
 v : [gamma]
-v | () => 0
+v | (gamma == 3) => 0
+  // Cryptol replaces this next constraint with `TError 3 == 2` when
+  // instantiating `Instantiated.cry`
+  | (gamma == 2) => 1
+  | () => 2