diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,10 @@
 # Revision history for agda2lagda
 
+## 0.2025.9.5
+
+* Fix `incomplete-patterns` warnings.
+* Tested with GHC 8.0.2 - 9.14 alpha1.
+
 ## 0.2023.6.9
 
 _West Pride revision._
diff --git a/agda2lagda.cabal b/agda2lagda.cabal
--- a/agda2lagda.cabal
+++ b/agda2lagda.cabal
@@ -1,7 +1,7 @@
 cabal-version:       1.24
 
 name:                agda2lagda
-version:             0.2023.6.9
+version:             0.2025.9.5
 synopsis:            Translate .agda files into .lagda.tex files.
 
 description:         Simple command line tool to convert plain Agda
@@ -15,7 +15,7 @@
 
 author:              Andreas Abel
 maintainer:          Andreas Abel <andreas.abel@cse.gu.se>
-copyright:           Andreas Abel, 2020-2023
+copyright:           Andreas Abel, 2020-2025
 category:            Dependent types, Development
 
 build-type:          Simple
@@ -32,8 +32,12 @@
   test/golden/*.lagda.tex
 
 tested-with:
-  GHC == 9.6.2
-  GHC == 9.4.5
+  GHC == 9.14.1
+  GHC == 9.12.2
+  GHC == 9.10.2
+  GHC == 9.8.4
+  GHC == 9.6.7
+  GHC == 9.4.8
   GHC == 9.2.8
   GHC == 9.0.2
   GHC == 8.10.7
@@ -87,7 +91,7 @@
   main-is:            Tests.hs
   default-language:   Haskell2010
   ghc-options:        -threaded
-  build-depends:      base >= 4.11
+  build-depends:      base >= 4.11 && < 5
                         -- goldplate requires ghc >= 8.4
                       , process
   build-tool-depends: goldplate:goldplate
diff --git a/src/LexicalStructure.hs b/src/LexicalStructure.hs
--- a/src/LexicalStructure.hs
+++ b/src/LexicalStructure.hs
@@ -56,6 +56,8 @@
 -- | Commented out code from block comments.
 pattern CommItem a = Item Comment a
 
+{-# COMPLETE CodeItem, TextItem, CommItem #-}
+
 -- | Entry point for the parser of the lexical structure.
 
 parseItems
diff --git a/src/Markup.hs b/src/Markup.hs
--- a/src/Markup.hs
+++ b/src/Markup.hs
@@ -8,6 +8,8 @@
   , gobbleTrailingBlockCommentClosers
   ) where
 
+import qualified Data.List.NonEmpty as List1
+
 import Util
 import qualified LexicalStructure as L
 
@@ -40,33 +42,33 @@
       $ paragraphs s
 
 -- | A paragraph is a non-empty list of non-empty lines.
-type Paragraph = [String]
+type Paragraph = List1 String
 
 groupBullets :: [TextItem] -> [TextItem]
-groupBullets = map joinItems . groupBy (\ a b -> all (isJust . isItemize) [a,b])
+groupBullets = map joinItems . List1.groupBy (\ a b -> all (isJust . isItemize) [a,b])
   where
   isItemize = \case
     Itemize ps -> Just ps
     _ -> Nothing
-  joinItems :: [TextItem] -> TextItem
+  joinItems :: List1 TextItem -> TextItem
   joinItems is =
     -- In each group...
-    case mapMaybe isItemize is of
+    case mapMaybe isItemize $ List1.toList is of
       -- ...either it is not Itemize
-      []  -> head is
+      []  -> List1.head is
       -- or all are Itemize.
       pps -> Itemize $ concat pps
 
 -- | If the last line of a paragraph is just dashes or equal signs, we are a heading.
 
 detectMarkup :: Paragraph -> TextItem
-detectMarkup ls@(l1:ls1)
-  | Just s <- bulleted l1 = Itemize [s:ls1]
+detectMarkup ls@(l1 :| ls1)
+  | Just s <- bulleted l1 = Itemize [s :| ls1]
   | all (== '=') l0 = Heading 1 $ unwords $ map trimLeft ls0
   | all (== '-') l0 = Heading 2 $ unwords $ map trimLeft ls0
   | otherwise       = Paragraph ls
   where
-  (ls0, l) = initLast ls  -- safe!
+  (ls0, l) = initLast ls
   l0 = trimLeft l
 
 -- | If the line starts with @*@, return the rest.
@@ -81,7 +83,7 @@
 --   Preserves indentation.
 
 paragraphs :: String -> [Paragraph]
-paragraphs = mapMaybe filterBlank . groupBy emptyOrNot . lines
+paragraphs = mapMaybe filterBlank . List1.groupBy emptyOrNot . lines
   where
   emptyLine  = null . trimLeft
   emptyOrNot = (==) `on` emptyLine
@@ -92,7 +94,7 @@
 -- | Text lines at the end of file consisting solely of words "-}" are
 -- discarded, to accommodate for a hack that makes it easy to comment
 -- out everything to the end of the file.
--- https://github.com/agda/agda/issues/4953#issuecomment-702720296
+-- <https://github.com/agda/agda/issues/4953#issuecomment-702720296>
 
 gobbleTrailingBlockCommentClosers :: [L.Item] -> [L.Item]
 gobbleTrailingBlockCommentClosers = updateLast $ \case
diff --git a/src/Render.hs b/src/Render.hs
--- a/src/Render.hs
+++ b/src/Render.hs
@@ -8,6 +8,8 @@
   , lagdaMd
   ) where
 
+import qualified Data.List.NonEmpty as List1
+
 import qualified LexicalStructure as L
 import Options (Language, languageToHighlighter)
 import Markup
@@ -35,12 +37,13 @@
 
 renderTex :: TextItem -> String
 renderTex = \case
-  Paragraph p -> unlines p
+  Paragraph p -> unlines $ List1.toList p
   Heading 1 s -> "\\heading{" ++ s ++ "}\n"
   Heading 2 s -> "\\subheading{" ++ s ++ "}\n"
+  Heading _ _ -> error "Render.renderTex: headings are only supported of level 1 or 2"
   Itemize ps  -> unlines $ concat $
     [ [ "\\begin{itemize}\n" ]
-    , map (unlines . ("\\item" :)) ps
+    , map (unlines . ("\\item" :) . List1.toList) ps
     , [ "\\end{itemize}" ]
     ]
 
diff --git a/src/Util.hs b/src/Util.hs
--- a/src/Util.hs
+++ b/src/Util.hs
@@ -8,7 +8,11 @@
 import Data.List      as X (dropWhileEnd, groupBy)
 import Data.Maybe     as X
 import Data.Semigroup as X
+import Data.List.NonEmpty as X (pattern (:|))
+import qualified Data.List.NonEmpty as List1
 
+type List1 = List1.NonEmpty
+
 (<&>) :: Functor f => f a -> (a -> b) -> f b
 (<&>) = flip (<$>)
 
@@ -25,8 +29,8 @@
 
 -- | Precondition: list non-empty.
 
-initLast :: [a] -> ([a], a)
-initLast as = (init as, last as)
+initLast :: List1 a -> ([a], a)
+initLast as = (List1.init as, List1.last as)
 
 -- * String manipulation
 
diff --git a/test/golden/ClosingCommentInString.lagda.md b/test/golden/ClosingCommentInString.lagda.md
--- a/test/golden/ClosingCommentInString.lagda.md
+++ b/test/golden/ClosingCommentInString.lagda.md
@@ -1,4 +1,4 @@
-<!-- This file was automatically generated by agda2lagda 0.2023.6.9. -->
+<!-- This file was automatically generated by agda2lagda 0.2025.9.5. -->
 
 This demonstrates a known issue:
 The parser is not aware of strings, thus,
diff --git a/test/golden/ClosingCommentInString.lagda.tex b/test/golden/ClosingCommentInString.lagda.tex
--- a/test/golden/ClosingCommentInString.lagda.tex
+++ b/test/golden/ClosingCommentInString.lagda.tex
@@ -1,4 +1,4 @@
-%% This file was automatically generated by agda2lagda 0.2023.6.9.
+%% This file was automatically generated by agda2lagda 0.2025.9.5.
 
 This demonstrates a known issue:
 The parser is not aware of strings, thus,
diff --git a/test/golden/Foo.lagda.md b/test/golden/Foo.lagda.md
--- a/test/golden/Foo.lagda.md
+++ b/test/golden/Foo.lagda.md
@@ -1,4 +1,4 @@
-<!-- This file was automatically generated by agda2lagda 0.2023.6.9. -->
+<!-- This file was automatically generated by agda2lagda 0.2025.9.5. -->
 
 Sample non-literate Agda program
 ================================
diff --git a/test/golden/Foo.lagda.tex b/test/golden/Foo.lagda.tex
--- a/test/golden/Foo.lagda.tex
+++ b/test/golden/Foo.lagda.tex
@@ -1,4 +1,4 @@
-%% This file was automatically generated by agda2lagda 0.2023.6.9.
+%% This file was automatically generated by agda2lagda 0.2025.9.5.
 
 \heading{Sample non-literate Agda program}