From 2018dc3476c1a1b723f8c7106d628bd0da8cb49c Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Thu, 2 Oct 2025 14:12:15 +0200
Subject: Tune redundant cases for no-warnings on GHC 9.12

---
 cabal.project                         | 2 +-
 src/Data/Array/Nested/Convert.hs      | 1 -
 src/Data/Array/Nested/Permutation.hs  | 1 +
 src/Data/Array/Nested/Ranked/Shape.hs | 5 +----
 4 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/cabal.project b/cabal.project
index d102ed6..d76d872 100644
--- a/cabal.project
+++ b/cabal.project
@@ -1,2 +1,2 @@
 packages: .
-with-compiler: ghc-9.8.4
+with-compiler: ghc-9.12.2
diff --git a/src/Data/Array/Nested/Convert.hs b/src/Data/Array/Nested/Convert.hs
index a260dc0..8c88d23 100644
--- a/src/Data/Array/Nested/Convert.hs
+++ b/src/Data/Array/Nested/Convert.hs
@@ -80,7 +80,6 @@ shrFromShS (n :$$ sh) = fromSNat' n :$: shrFromShS sh
 ixsFromIxR :: ShS sh -> IxR (Rank sh) i -> IxS sh i
 ixsFromIxR ZSS ZIR = ZIS
 ixsFromIxR (_ :$$ sh) (n :.: idx) = n :.$ ixsFromIxR sh idx
-ixsFromIxR _ _ = error "unreachable"
 
 -- | Performs a runtime check that @n@ matches @Rank sh@. Equivalent to the
 -- following, but more efficient:
diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs
index 1a0fd22..045b18f 100644
--- a/src/Data/Array/Nested/Permutation.hs
+++ b/src/Data/Array/Nested/Permutation.hs
@@ -283,6 +283,7 @@ lemRankDropLen (_ :!% sh) (_ `PCons` is)
   = unsafeCoerceRefl
 #endif
 lemRankDropLen (_ :!% _) PNil = Refl
+lemRankDropLen ZKX (_ `PCons` _) = error "1 <= 0"
 
 lemIndexSucc :: Proxy i -> Proxy a -> Proxy l
              -> Index (i + 1) (a : l) :~: Index i l
diff --git a/src/Data/Array/Nested/Ranked/Shape.hs b/src/Data/Array/Nested/Ranked/Shape.hs
index 88a550c..488b4d8 100644
--- a/src/Data/Array/Nested/Ranked/Shape.hs
+++ b/src/Data/Array/Nested/Ranked/Shape.hs
@@ -115,21 +115,17 @@ listrFromList (x : xs) k = listrFromList xs $ \l -> k (x ::: l)
 
 listrHead :: ListR (n + 1) i -> i
 listrHead (i ::: _) = i
-listrHead ZR = error "unreachable"
 
 listrTail :: ListR (n + 1) i -> ListR n i
 listrTail (_ ::: sh) = sh
-listrTail ZR = error "unreachable"
 
 listrInit :: ListR (n + 1) i -> ListR n i
 listrInit (n ::: sh@(_ ::: _)) = n ::: listrInit sh
 listrInit (_ ::: ZR) = ZR
-listrInit ZR = error "unreachable"
 
 listrLast :: ListR (n + 1) i -> i
 listrLast (_ ::: sh@(_ ::: _)) = listrLast sh
 listrLast (n ::: ZR) = n
-listrLast ZR = error "unreachable"
 
 -- | Performs a runtime check that the lengths are identical.
 listrCast :: SNat n' -> ListR n i -> ListR n' i
@@ -138,6 +134,7 @@ listrCast = listrCastWithName "listrCast"
 listrIndex :: forall k n i. (k + 1 <= n) => SNat k -> ListR n i -> i
 listrIndex SZ (x ::: _) = x
 listrIndex (SS i) (_ ::: xs) | Refl <- lemLeqSuccSucc (Proxy @k) (Proxy @n) = listrIndex i xs
+listrIndex _ ZR = error "k + 1 <= 0"
 
 listrZip :: ListR n i -> ListR n j -> ListR n (i, j)
 listrZip ZR ZR = ZR
-- 
cgit v1.2.3-70-g09d2