Changes to avoid irrefutable patterns.

This is to make things build with GHC 8.6, which requires a MonadFail
instance.

Pretty much all of these should end up being `panic`, so perhaps we should
rewrite more of them to call `panic` (instead of using lazy patterns)

src/Cryptol/ModuleSystem/Renamer.hs

@@ -422,7 +422,7 @@ instance Rename Decl where
     DBind b           -> DBind         <$> rename b
 
     -- XXX we probably shouldn't see these at this point...
-    DPatBind pat e    -> do (pe,[pat']) <- renamePats [pat]
+    DPatBind pat e    -> do (pe,pat') <- renamePat pat
                             shadowNames pe (DPatBind pat' <$> rename e)
 
     DType syn         -> DType         <$> rename syn
@@ -842,8 +842,8 @@ renameArm [] =
 renameMatch :: Match PName -> RenameM (NamingEnv,Match Name)
 
 renameMatch (Match p e) =
-  do (pe,[p']) <- renamePats [p]
-     e'        <- rename e
+  do (pe,p') <- renamePat p
+     e'      <- rename e
      return (pe,Match p' e')
 
 renameMatch (MatchLet b) =
@@ -852,6 +852,15 @@ renameMatch (MatchLet b) =
      b' <- shadowNames be (rename b)
      return (be,MatchLet b')
 
+-- | Rename patterns, and collect the new environment that they introduce.
+renamePat :: Pattern PName -> RenameM (NamingEnv, Pattern Name)
+renamePat p =
+  do pe <- patternEnv p
+     p' <- shadowNames pe (rename p)
+     return (pe, p')
+
+
+
 -- | Rename patterns, and collect the new environment that they introduce.
 renamePats :: [Pattern PName] -> RenameM (NamingEnv,[Pattern Name])
 renamePats  = loop

src/Cryptol/Prims/Eval.hs

@@ -926,7 +926,7 @@ ecSplitV =
   lam  $ \ val ->
     case (parts, each) of
        (Nat p, Nat e) | isTBit a -> do
-          VWord _ val' <- val
+          ~(VWord _ val') <- val
           return $ VSeq p $ IndexSeqMap $ \i -> do
             return $ VWord e (extractWordVal e ((p-i-1)*e) <$> val')
        (Inf, Nat e) | isTBit a -> do

src/Cryptol/REPL/Command.hs

@@ -249,9 +249,9 @@ runCommand c = case c of
 -- Get the setting we should use for displaying values.
 getPPValOpts :: REPL E.PPOpts
 getPPValOpts =
-  do EnvNum base      <- getUser "base"
-     EnvBool ascii    <- getUser "ascii"
-     EnvNum infLength <- getUser "infLength"
+  do base      <- getKnownUser "base"
+     ascii     <- getKnownUser "ascii"
+     infLength <- getKnownUser "infLength"
      return E.PPOpts { E.useBase      = base
                      , E.useAscii     = ascii
                      , E.useInfLength = infLength
@@ -315,7 +315,7 @@ qcCmd qcMode "" =
 qcCmd qcMode str =
   do expr <- replParseExpr str
      (val,ty) <- replEvalExpr expr
-     EnvNum testNum <- getUser "tests"
+     testNum <- getKnownUser "tests"
      case testableType ty of
        Just (Just sz,tys,vss) | qcMode == QCExhaust || sz <= toInteger testNum -> do
             rPutStrLn "Using exhaustive testing."
@@ -511,10 +511,10 @@ cmdProveSat isSat "" =
 cmdProveSat isSat str = do
   let cexStr | isSat = "satisfying assignment"
              | otherwise = "counterexample"
-  EnvString proverName <- getUser "prover"
-  EnvString fileName <- getUser "smtfile"
+  proverName <- getKnownUser "prover"
+  fileName   <- getKnownUser "smtfile"
   let mfile = if fileName == "-" then Nothing else Just fileName
-  case proverName of
+  case proverName :: String of
     "offline" -> do
       result <- offlineProveSat isSat str mfile
       case result of
@@ -571,8 +571,8 @@ onlineProveSat :: Bool
                -> String -> Maybe FilePath
                -> REPL (Maybe SBV.Solver,Symbolic.ProverResult,ProverStats)
 onlineProveSat isSat str mfile = do
-  EnvString proverName <- getUser "prover"
-  EnvBool verbose <- getUser "debug"
+  proverName <- getKnownUser "prover"
+  verbose <- getKnownUser "debug"
   satNum <- getUserSatNum
   parseExpr <- replParseExpr str
   (_, expr, schema) <- replCheckExpr parseExpr
@@ -596,7 +596,7 @@ onlineProveSat isSat str mfile = do
 
 offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Either String String)
 offlineProveSat isSat str mfile = do
-  EnvBool verbose <- getUser "debug"
+  verbose <- getKnownUser "debug"
   parseExpr <- replParseExpr str
   (_, expr, schema) <- replCheckExpr parseExpr
   decls <- fmap M.deDecls getDynEnv
@@ -1126,8 +1126,8 @@ liftModuleCmd cmd =
 
 moduleCmdResult :: M.ModuleRes a -> REPL a
 moduleCmdResult (res,ws0) = do
-  EnvBool warnDefaulting <- getUser "warnDefaulting"
-  EnvBool warnShadowing  <- getUser "warnShadowing"
+  warnDefaulting <- getKnownUser "warnDefaulting"
+  warnShadowing  <- getKnownUser "warnShadowing"
   -- XXX: let's generalize this pattern
   let isDefaultWarn (T.DefaultingTo _ _) = True
       isDefaultWarn _ = False
@@ -1213,7 +1213,7 @@ replEvalExpr expr =
     case ts of
       [] -> return ()
       _  ->
-        do EnvBool warnDefaulting <- getUser "warnDefaulting"
+        do warnDefaulting <- getKnownUser "warnDefaulting"
            when warnDefaulting $
              do rPutStrLn "Showing a specific instance of polymorphic result:"
                 mapM_ warnDefault ts

src/Cryptol/REPL/Monad.hs

@@ -13,6 +13,7 @@
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE FlexibleInstances #-}
 
 module Cryptol.REPL.Monad (
     -- * REPL Monad
@@ -56,7 +57,7 @@ module Cryptol.REPL.Monad (
     -- ** Config Options
   , EnvVal(..)
   , OptionDescr(..)
-  , setUser, getUser, tryGetUser
+  , setUser, getUser, getKnownUser, tryGetUser
   , userOptions
   , getUserSatNum
   , getUserShowProverStats
@@ -645,10 +646,38 @@ getUser name = do
     Just ev -> return ev
     Nothing -> panic "[REPL] getUser" ["option `" ++ name ++ "` does not exist"]
 
+getKnownUser :: IsEnvVal a => String -> REPL a
+getKnownUser x = fromEnvVal <$> getUser x
+
+class IsEnvVal a where
+  fromEnvVal :: EnvVal -> a
+
+instance IsEnvVal Bool where
+  fromEnvVal x = case x of
+                   EnvBool b -> b
+                   _         -> badIsEnv "Bool"
+
+instance IsEnvVal Int where
+  fromEnvVal x = case x of
+                   EnvNum b -> b
+                   _         -> badIsEnv "Num"
+
+instance IsEnvVal (String,[String]) where
+  fromEnvVal x = case x of
+                   EnvProg b bs -> (b,bs)
+                   _            -> badIsEnv "Prog"
+
+instance IsEnvVal String where
+  fromEnvVal x = case x of
+                   EnvString b -> b
+                   _           -> badIsEnv "String"
+
+badIsEnv :: String -> a
+badIsEnv x = panic "fromEnvVal" [ "[REPL] Expected a `" ++ x ++ "` value." ]
+
+
 getUserShowProverStats :: REPL Bool
-getUserShowProverStats =
-  do EnvBool yes <- getUser "prover-stats"
-     return yes
+getUserShowProverStats = getKnownUser "prover-stats"
 
 -- Environment Options ---------------------------------------------------------
 
@@ -784,7 +813,7 @@ checkSatNum val = case val of
 
 getUserSatNum :: REPL SatNum
 getUserSatNum = do
-  EnvString s <- getUser "satNum"
+  s <- getKnownUser "satNum"
   case s of
     "all"                     -> return AllSat
     _ | Just n <- readMaybe s -> return (SomeSat n)
@@ -795,7 +824,7 @@ getUserSatNum = do
 
 whenDebug :: REPL () -> REPL ()
 whenDebug m = do
-  EnvBool b <- getUser "debug"
+  b <- getKnownUser "debug"
   when b m
 
 -- Smoke Testing ---------------------------------------------------------------
@@ -825,3 +854,4 @@ z3exists = do
   case mPath of
     Nothing -> return (Just Z3NotFound)
     Just _  -> return Nothing
+

src/Cryptol/Transform/Specialize.hs

@@ -126,7 +126,7 @@ withDeclGroups dgs action = do
   -- Then reassemble the DeclGroups.
   let splitDecl :: Decl -> SpecM [Decl]
       splitDecl d = do
-        Just (_, tm) <- Map.lookup (dName d) <$> getSpecCache
+        ~(Just (_, tm)) <- Map.lookup (dName d) <$> getSpecCache
         return (catMaybes $ map (snd . snd) $ toListTM tm)
   let splitDeclGroup :: DeclGroup -> SpecM [DeclGroup]
       splitDeclGroup (Recursive ds) = do

src/Cryptol/TypeCheck/CheckModuleInstance.hs

@@ -162,7 +162,7 @@ makeValParamDef :: Name   {- ^ Definition of parameter -} ->
                    InferM Expr {- ^ Expression to use for param definition -}
 
 makeValParamDef x sDef pDef =
-  withVar x sDef $ do DExpr e <- dDefinition <$> checkSigB bnd (pDef,[])
+  withVar x sDef $ do ~(DExpr e) <- dDefinition <$> checkSigB bnd (pDef,[])
                       return e
   where
   bnd = P.Bind { P.bName      = loc x

src/Cryptol/TypeCheck/Infer.hs

@@ -928,7 +928,7 @@ inferDs ds continue = checkTyDecls =<< orderTyDecls (mapMaybe toTyDecl ds)
               bs1
 
   checkBinds decls (AcyclicSCC c : more) =
-    do [b] <- inferBinds isTopLevel False [c]
+    do ~[b] <- inferBinds isTopLevel False [c]
        withVar (dName b) (dSignature b) $
          checkBinds (NonRecursive b : decls) more