From 2d837a1b4ef2914ac4bc8e012b31ff7abd4d2246 Mon Sep 17 00:00:00 2001
From: Mikolaj Konarski <mikolaj.konarski@funktory.com>
Date: Fri, 12 Dec 2025 23:28:02 +0100
Subject: Fix a few KnownNat in ShS-related TODOs and reword the rest

---
 src/Data/Array/Nested/Shaped/Shape.hs | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'src/Data/Array/Nested/Shaped/Shape.hs')

diff --git a/src/Data/Array/Nested/Shaped/Shape.hs b/src/Data/Array/Nested/Shaped/Shape.hs
index bfc6ad2..18bd2e9 100644
--- a/src/Data/Array/Nested/Shaped/Shape.hs
+++ b/src/Data/Array/Nested/Shaped/Shape.hs
@@ -188,7 +188,7 @@ listsPermute (i `PCons` (is :: Perm is')) (sh :: ListS sh f) =
   case listsIndex (Proxy @is') (Proxy @sh) i sh of
     item -> item ::$ listsPermute is sh
 
--- TODO: remove this SNat when the KnownNat constaint in ListS is removed
+-- TODO: try to remove this SNat now that the KnownNat constraint in ListS is removed
 listsIndex :: forall f i is sh shT. Proxy is -> Proxy shT -> SNat i -> ListS sh f -> f (Index i sh)
 listsIndex _ _ SZ (n ::$ _) = n
 listsIndex p pT (SS (i :: SNat i')) ((_ :: f n) ::$ (sh :: ListS sh' f))
@@ -278,11 +278,9 @@ ixsInit (IxS list) = IxS (listsInit list)
 ixsLast :: IxS (n : sh) i -> i
 ixsLast (IxS list) = getConst (listsLast list)
 
--- TODO: this takes a ShS because there are KnownNats inside IxS.
-ixsCast :: ShS sh' -> IxS sh i -> IxS sh' i
-ixsCast ZSS ZIS = ZIS
-ixsCast (_ :$$ sh) (i :.$ idx) = i :.$ ixsCast sh idx
-ixsCast _ _ = error "ixsCast: ranks don't match"
+ixsCast :: IxS sh i -> IxS sh i
+ixsCast ZIS = ZIS
+ixsCast (i :.$ idx) = i :.$ ixsCast idx
 
 ixsAppend :: forall sh sh' i. IxS sh i -> IxS sh' i -> IxS (sh ++ sh') i
 ixsAppend = coerce (listsAppend @_ @(Const i))
-- 
cgit v1.2.3-70-g09d2