diff --git a/crucible-go/src/Lang/Crucible/Go/Types.hs b/crucible-go/src/Lang/Crucible/Go/Types.hs
index 5ef0e061c..9db1d878a 100644
--- a/crucible-go/src/Lang/Crucible/Go/Types.hs
+++ b/crucible-go/src/Lang/Crucible/Go/Types.hs
@@ -24,6 +24,7 @@ import           Control.Monad.State
 
 import           Data.Default.Class
 import           Data.HashMap.Strict as HM
+import qualified Data.Kind as Kind
 import           Data.Maybe (fromJust)
 import           Data.Text (Text)
 
@@ -223,7 +224,7 @@ goExprType :: GoExpr a tp -> TypeRepr tp
 goExprType (GoExpr _loc e) = exprType e
 
 -- | Pair of things with the same type index.
-data PairIx (f :: * -> CrucibleType -> *) s tp where
+data PairIx (f :: Kind.Type -> CrucibleType -> Kind.Type) s tp where
   PairIx :: forall f s tp. f s tp -> f s tp -> PairIx f s tp
 
 -- | Pair of things with the same type index.
diff --git a/crucible-jvm/src/Lang/Crucible/JVM/Overrides.hs b/crucible-jvm/src/Lang/Crucible/JVM/Overrides.hs
index dd3af64e5..d997f6cd7 100644
--- a/crucible-jvm/src/Lang/Crucible/JVM/Overrides.hs
+++ b/crucible-jvm/src/Lang/Crucible/JVM/Overrides.hs
@@ -636,7 +636,13 @@ printStream name showNewline descr t =
                   { C.typedOverrideHandler=
                     \args -> do
                       let reg = C.unRV (Ctx.last args)
-                      str <- showReg @sym (head (J.methodKeyParameterTypes mk)) t reg
+                      let paramTy =
+                            case J.methodKeyParameterTypes mk of
+                              ty:_ -> ty
+                              []   -> panic
+                                        "printStream"
+                                        ["Expected a parameter type, but none found"]
+                      str <- showReg @sym paramTy t reg
                       h   <- C.printHandle <$> C.getContext
                       liftIO $ (if showNewline then hPutStrLn else hPutStr) h str
                       liftIO $ hFlush h
diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Printf.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Printf.hs
index d6869da6a..971cf481b 100644
--- a/crucible-llvm/src/Lang/Crucible/LLVM/Printf.hs
+++ b/crucible-llvm/src/Lang/Crucible/LLVM/Printf.hs
@@ -47,6 +47,8 @@ import qualified Data.Set as Set
 import           Data.Word
 import qualified GHC.Stack as GHC
 
+import           Lang.Crucible.Panic (panic)
+
 data PrintfFlag
   = PrintfAlternateForm   -- #
   | PrintfZeroPadding     -- 0
@@ -234,7 +236,13 @@ formatOctal
 formatOctal i minwidth prec flags = do
   let digits = N.showOct (abs i) []
   let precdigits = addLeadingZeros prec digits
-  let altdigits = if Set.member PrintfAlternateForm flags && head precdigits /= '0' then
+  let leadingPrecDigit =
+        case precdigits of
+          d:_ -> d
+          [] -> panic
+                  "formatOctal"
+                  ["Octal-formatted number with no digits"]
+  let altdigits = if Set.member PrintfAlternateForm flags && leadingPrecDigit /= '0' then
                      '0':precdigits
                   else
                      precdigits
diff --git a/crucible-mir/src/Mir/Generator.hs b/crucible-mir/src/Mir/Generator.hs
index 6fb25f626..d1fe2ff66 100644
--- a/crucible-mir/src/Mir/Generator.hs
+++ b/crucible-mir/src/Mir/Generator.hs
@@ -100,6 +100,7 @@ import qualified Lang.Crucible.CFG.Generator as G
 import qualified Lang.Crucible.CFG.Reg as R
 import qualified Lang.Crucible.CFG.Expr as E
 import qualified Lang.Crucible.CFG.Core as Core
+import qualified Lang.Crucible.Panic as P
 import qualified Lang.Crucible.Syntax as S
 
 
@@ -589,8 +590,15 @@ resolveCustom instDefId = do
 
 freshVarName :: Text -> Map Text a -> Text
 freshVarName base vm =
-    head $ filter (\n -> not $ n `Map.member` vm) $
-        base : [base <> "_" <> Text.pack (show i) | i <- [0 :: Integer ..]]
+  case varNamesInfList of
+    varName:_ -> varName
+    [] -> P.panic
+            "freshVarName"
+            ["Expected infinite list, but list was empty"]
+  where
+    varNamesInfList =
+      filter (\n -> not $ n `Map.member` vm) $
+      base : [base <> "_" <> Text.pack (show i) | i <- [0 :: Integer ..]]
 
 -- Generate a fresh name of the form `_temp123`
 freshTempName :: Map Text a -> Text
diff --git a/crucible-mir/src/Mir/Pass/AllocateEnum.hs b/crucible-mir/src/Mir/Pass/AllocateEnum.hs
index 4a154d409..240c347c9 100644
--- a/crucible-mir/src/Mir/Pass/AllocateEnum.hs
+++ b/crucible-mir/src/Mir/Pass/AllocateEnum.hs
@@ -99,6 +99,6 @@ pcr :: HasCallStack => (?col :: Collection) => BasicBlock -> BasicBlock
 pcr (BasicBlock inf (BasicBlockData stmts term)) = BasicBlock inf (BasicBlockData (go stmts) term) where
    go :: [Statement] -> [Statement]
    go [] = []
-   go s  | Just (s', ss) <- findAllocEnum s = s' : go ss
-         | otherwise = head s : go (tail s)
-
+   go stmtss@(stmt:stmts)
+     | Just (stmt', stmts') <- findAllocEnum stmtss = stmt' : go stmts'
+     | otherwise = stmt : go stmts
diff --git a/crucible-mir/src/Mir/Trans.hs b/crucible-mir/src/Mir/Trans.hs
index 092a2bf63..8ae306d8e 100644
--- a/crucible-mir/src/Mir/Trans.hs
+++ b/crucible-mir/src/Mir/Trans.hs
@@ -1893,7 +1893,9 @@ transVtableShim colState vtableName (VtableItem fnName defName)
         $ \implFn ->
     withMethodHandle fnName (die ["failed to look up implementation", show fnName])
         $ \implFH ->
-    let implMirArg0 = head $ implFn ^. M.fsig . M.fsarg_tys in
+    let implMirArg0 = case implFn ^. M.fsig . M.fsarg_tys of
+                        arg_ty:_ -> arg_ty
+                        [] -> die ["shim has no argument types"] in
     let implArgs = FH.handleArgTypes implFH in
     let implRet = FH.handleReturnType implFH in
 
diff --git a/crux-llvm/src/Crux/LLVM/Compile.hs b/crux-llvm/src/Crux/LLVM/Compile.hs
index 5448da5d5..3aa6704f6 100644
--- a/crux-llvm/src/Crux/LLVM/Compile.hs
+++ b/crux-llvm/src/Crux/LLVM/Compile.hs
@@ -30,6 +30,7 @@ import           System.Process ( readProcessWithExitCode )
 import           What4.Interface
 import           What4.ProgramLoc
 
+import           Lang.Crucible.Panic ( panic )
 import           Lang.Crucible.Simulator.SimError
 
 import           Crux
@@ -124,13 +125,20 @@ genBitCode ::
   Log.SupportsCruxLLVMLogMessage msgs =>
   CruxOptions -> LLVMOptions -> IO FilePath
 genBitCode cruxOpts llvmOpts =
-  -- n.b. use of head here is OK because inputFiles should not be
-  -- empty (and was previously verified as such in CruxLLVMMain).
   if noCompile llvmOpts
-  then return (head (Crux.inputFiles cruxOpts))
+  then return headInputFile
   else do
-    let ofn = "crux~" <> (takeFileName $ head $ Crux.inputFiles cruxOpts) -<.> ".bc"
+    let ofn = "crux~" <> takeFileName headInputFile -<.> ".bc"
     genBitCodeToFile ofn (Crux.inputFiles cruxOpts) cruxOpts llvmOpts False
+  where
+    -- n.b. the use of partiality here is OK because inputFiles should not be
+    -- empty (and was previously verified as such in CruxLLVMMain).
+    headInputFile =
+      case Crux.inputFiles cruxOpts of
+        inputFile:_ -> inputFile
+        [] -> panic
+                "genBitCode"
+                ["Unexpected empty list of files"]
 
 -- | Given the target filename and a list of input files, along with
 -- the crux and llvm options, bitcode-compile each input .c file and
diff --git a/crux-llvm/test/Test.hs b/crux-llvm/test/Test.hs
index 9f4b56ee2..408605463 100644
--- a/crux-llvm/test/Test.hs
+++ b/crux-llvm/test/Test.hs
@@ -12,7 +12,7 @@ import           Data.Bifunctor ( first )
 import qualified Data.ByteString.Lazy as BSIO
 import qualified Data.ByteString.Lazy.Char8 as BSC
 import           Data.Char ( isLetter, isSpace )
-import           Data.List.Extra ( isInfixOf, isPrefixOf )
+import           Data.List.Extra ( isInfixOf )
 import           Data.Maybe ( catMaybes, fromMaybe )
 import qualified Data.Text as T
 import           Data.Versions ( Versioning, versioning, prettyV, major )
@@ -32,6 +32,8 @@ import qualified Test.Tasty as TT
 import           Test.Tasty.HUnit ( testCase, assertFailure )
 import qualified Test.Tasty.Sugar as TS
 
+import qualified Lang.Crucible.Panic as P
+
 import qualified CruxLLVMMain as C
 
 
@@ -103,7 +105,7 @@ getClangVersion :: IO VersionCheck
 getClangVersion = do
   -- Determine which version of clang will be used for these tests.
   -- An exception (E.g. in the readProcess if clang is not found) will
-  -- result in termination (test failure).  Uses partial 'head' but
+  -- result in termination (test failure).  Uses partiality, but
   -- this is just tests, and failure is captured.
   clangBin <- fromMaybe "clang" <$> lookupEnv "CLANG"
   let isVerLine = isInfixOf "clang version"
@@ -112,10 +114,27 @@ getClangVersion = do
       -- as tildes (cf. https://github.com/fosskers/versions/issues/62).
       -- These have been observed in the wild (e.g., 12.0.0-3ubuntu1~20.04.5).
       scrubProblemChars = filter (/= '~')
+
+      headVersionLine :: [String] -> String
+      headVersionLine ls =
+        case ls of
+          l:_ -> l
+          [] -> P.panic
+                  "getClangVersion"
+                  ["`clang --version` output does not contain line with version"]
+
+      headVersionWord :: [String] -> String
+      headVersionWord ws =
+        case ws of
+          w:_ -> w
+          [] -> P.panic
+                  "getClangVersion"
+                  ["`clang --version` output does not contain numeric version"]
+
       getVer (Right inp) =
         -- example inp: "clang version 10.0.1"
-        scrubProblemChars $ head $ dropLetter $ words $
-        head $ filter isVerLine $ lines inp
+        scrubProblemChars $ headVersionWord $ dropLetter $ words $
+        headVersionLine $ filter isVerLine $ lines inp
       getVer (Left full) = full
   mkVC "clang" . getVer <$> readProcessVersion clangBin
 
@@ -124,8 +143,10 @@ getZ3Version =
   let getVer (Right inp) =
         -- example inp: "Z3 version 4.8.7 - 64 bit"
         let w = words inp
-        in if and [ length w > 2, head w == "Z3" ]
-           then w !! 2 else "?"
+        in if |  ("Z3":_:verNum:_) <- w
+              -> verNum
+              |  otherwise
+              -> "?"
       getVer (Left full) = full
   in mkVC "z3" . getVer <$> readProcessVersion "z3"
 
@@ -134,8 +155,10 @@ getYicesVersion =
   let getVer (Right inp) =
         -- example inp: "Yices 2.6.1\nCopyright ..."
         let w = words inp
-        in if and [ length w > 1, head w == "Yices" ]
-           then w !! 1 else "?"
+        in if |  ("Yices":verNum:_) <- w
+              -> verNum
+              |  otherwise
+              -> "?"
       getVer (Left full) = full
   in mkVC "yices" . getVer <$> readProcessVersion "yices"
 
@@ -144,10 +167,10 @@ getSTPVersion =
   let getVer (Right inp) =
         -- example inp: "STP version 2.3.3\n..."
         let w = words inp
-        in if and [ length w > 2
-                  , head w == "STP"
-                  , w !! 1 == "version" ]
-           then w !! 2 else "?"
+        in if |  ("STP":"version":verNum:_) <- w
+              -> verNum
+              |  otherwise
+              -> "?"
       getVer (Left full) = full
   in mkVC "stp" . getVer <$> readProcessVersion "stp"
 
@@ -156,10 +179,10 @@ getCVC4Version =
   let getVer (Right inp) =
         -- example inp: "This is CVC4 version 1.8\ncompiled ..."
         let w = words inp
-        in if and [ length w > 4
-                  , "This is CVC4 version" `isPrefixOf` inp
-                  ]
-           then w !! 4 else "?"
+        in if |  ("This":"is":"CVC4":"version":verNum:_) <- w
+              -> verNum
+              |  otherwise
+              -> "?"
       getVer (Left full) = full
   in mkVC "cvc4" . getVer <$> readProcessVersion "cvc4"
 
@@ -168,10 +191,10 @@ getCVC5Version =
   let getVer (Right inp) =
         -- example inp: "This is cvc5 version 1.0.2\ncompiled ..."
         let w = words inp
-        in if and [ length w > 4
-                  , "This is cvc5 version" `isPrefixOf` inp
-                  ]
-           then w !! 4 else "?"
+        in if |  ("This":"is":"cvc5":"version":verNum:_) <- w
+              -> verNum
+              |  otherwise
+              -> "?"
       getVer (Left full) = full
   in mkVC "cvc5" . getVer <$> readProcessVersion "cvc5"
 
@@ -180,7 +203,9 @@ getBoolectorVersion =
   let getVer (Right inp) =
         -- example inp: "3.2.1"
         let w = words inp
-        in if not (null w) then head w else "?"
+        in case w of
+             verNum:_ -> verNum
+             [] -> "?"
       getVer (Left full) = full
   in mkVC "boolector" . getVer <$> readProcessVersion "boolector"
 
diff --git a/uc-crux-llvm/test/VersionCheck.hs b/uc-crux-llvm/test/VersionCheck.hs
index 40049ad51..f173c40fe 100644
--- a/uc-crux-llvm/test/VersionCheck.hs
+++ b/uc-crux-llvm/test/VersionCheck.hs
@@ -32,6 +32,8 @@ import           Data.Versions (Versioning, versioning, prettyV, major)
 import qualified GHC.IO.Exception as GE
 import           System.Process (readProcess)
 
+import           UCCrux.LLVM.Errors.Panic (panic)
+
 -- lack of decipherable version is not fatal to running the tests
 data VersionCheck = VC String (Either Text Versioning)
 
@@ -59,7 +61,7 @@ getClangVersion :: FilePath -> IO VersionCheck
 getClangVersion clangBin = do
   -- Determine which version of clang will be used for these tests.
   -- An exception (E.g. in the readProcess if clang is not found) will
-  -- result in termination (test failure).  Uses partial 'head' but
+  -- result in termination (test failure).  Uses partiality, but
   -- this is just tests, and failure is captured.
   let isVerLine = isInfixOf "clang version"
       dropLetter = dropWhile (all isLetter)
@@ -67,10 +69,27 @@ getClangVersion clangBin = do
       -- as tildes (cf. https://github.com/fosskers/versions/issues/62).
       -- These have been observed in the wild (e.g., 12.0.0-3ubuntu1~20.04.5).
       scrubProblemChars = filter (/= '~')
+
+      headVersionLine :: [String] -> String
+      headVersionLine ls =
+        case ls of
+          l:_ -> l
+          [] -> panic
+                  "getClangVersion"
+                  ["`clang --version` output does not contain line with version"]
+
+      headVersionWord :: [String] -> String
+      headVersionWord ws =
+        case ws of
+          w:_ -> w
+          [] -> panic
+                  "getClangVersion"
+                  ["`clang --version` output does not contain numeric version"]
+
       getVer (Right inp) =
         -- example inp: "clang version 10.0.1"
-        scrubProblemChars $ head $ dropLetter $ words $
-        head $ filter isVerLine $ lines inp
+        scrubProblemChars $ headVersionWord $ dropLetter $ words $
+        headVersionLine $ filter isVerLine $ lines inp
       getVer (Left full) = full
   mkVC "clang" . getVer <$> readProcessVersion clangBin