Support literals 0 and 1 at type Bit (#913).

This adds the instance rule `(1 >= n) => Literal n Bit` to the
type checker.

src/Cryptol/Eval/Generic.hs

@@ -49,6 +49,7 @@ import Cryptol.Utils.RecordMap
 mkLit :: Backend sym => sym -> TValue -> Integer -> SEval sym (GenValue sym)
 mkLit sym ty i =
   case ty of
+    TVBit                        -> pure $ VBit (bitLit sym (i > 0))
     TVInteger                    -> VInteger <$> integerLit sym i
     TVIntMod m
       | m == 0                   -> evalPanic "mkLit" ["0 modulus not allowed"]

src/Cryptol/TypeCheck/Solver/Class.hs

@@ -531,6 +531,9 @@ solveLiteralInst val ty
       -- Literal n Error -> fails
       TCon (TError _ e) _ -> Unsolvable e
 
+      -- (1 >= val) => Literal val Bit
+      TCon (TC TCBit) [] -> SolvedIf [ tOne >== val ]
+
       -- (fin val) => Literal val Integer
       TCon (TC TCInteger) [] -> SolvedIf [ pFin val ]