diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
index e6b7570b52..d8011aac0f 100644
--- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
@@ -771,16 +771,21 @@ defaultEvalOpts = E.EvalOpts quietLogger E.defaultPPOpts
 
 moduleCmdResult :: M.ModuleRes a -> IO (a, ME.ModuleEnv)
 moduleCmdResult (res, ws) = do
-  mapM_ (print . pp) (map suppressDefaulting ws)
+  mapM_ (print . pp) (concatMap suppressDefaulting ws)
   case res of
     Right (a, me) -> return (a, me)
     Left err      -> fail $ "Cryptol error:\n" ++ show (pp err) -- X.throwIO (ModuleSystemError err)
   where
-    suppressDefaulting :: MM.ModuleWarning -> MM.ModuleWarning
+    -- If all warnings are about type defaults, pretend there are no warnings at
+    -- all to avoid displaying an empty warning container.
+    suppressDefaulting :: MM.ModuleWarning -> [MM.ModuleWarning]
     suppressDefaulting w =
       case w of
-        MM.TypeCheckWarnings nm xs -> MM.TypeCheckWarnings nm (filter (notDefaulting . snd) xs)
-        MM.RenamerWarnings xs -> MM.RenamerWarnings xs
+        MM.RenamerWarnings xs -> [MM.RenamerWarnings xs]
+        MM.TypeCheckWarnings nm xs ->
+          case filter (notDefaulting . snd) xs of
+            [] -> []
+            xs' -> [MM.TypeCheckWarnings nm xs']
 
     notDefaulting :: TE.Warning -> Bool
     notDefaulting (TE.DefaultingTo {}) = False