Add annotations to rewrite rules and simpsets

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

@@ -1611,9 +1611,9 @@ scCryptolType sc t =
 scCryptolEq :: SharedContext -> Term -> Term -> IO Term
 scCryptolEq sc x y =
   do rules <- concat <$> traverse defRewrites defs
-     let ss = addConvs natConversions (addRules rules emptySimpset)
-     tx <- scTypeOf sc x >>= rewriteSharedTerm sc ss >>= scCryptolType sc
-     ty <- scTypeOf sc y >>= rewriteSharedTerm sc ss >>= scCryptolType sc
+     let ss = addConvs natConversions (addRules rules emptySimpset :: Simpset ())
+     tx <- scTypeOf sc x >>= rewriteSharedTerm sc ss >>= scCryptolType sc . snd
+     ty <- scTypeOf sc y >>= rewriteSharedTerm sc ss >>= scCryptolType sc . snd
      unless (tx == ty) $
        panic "scCryptolEq"
                  [ "scCryptolEq: type mismatch between"

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

@@ -18,7 +18,7 @@ import Verifier.SAW.Rewriter
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.Term.Functor
 
-mkCryptolSimpset :: SharedContext -> IO Simpset
+mkCryptolSimpset :: SharedContext -> IO (Simpset a)
 mkCryptolSimpset sc =
   do m <- scFindModule sc cryptolModuleName
      scSimpset sc (cryptolDefs m) [] []

saw-core/src/Verifier/SAW/Constant.hs

@@ -15,5 +15,5 @@ import Verifier.SAW.Conversion
 scConst :: SharedContext -> String -> Term -> IO Term
 scConst sc name t = do
   ty <- scTypeOf sc t
-  ty' <- rewriteSharedTerm sc (addConvs natConversions emptySimpset) ty
+  (_,ty') <- rewriteSharedTerm sc (addConvs natConversions emptySimpset :: Simpset ()) ty
   scConstant sc name t ty'