From bcf3bcf63626e75af9ab316d988e146f9a60c81d Mon Sep 17 00:00:00 2001
From: Mikolaj Konarski <mikolaj.konarski@funktory.com>
Date: Thu, 9 Apr 2026 18:04:58 +0200
Subject: Follow up the equal-rank-coercibility introduction

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

(limited to 'src/Data/Array/Nested/Shaped')

diff --git a/src/Data/Array/Nested/Shaped/Shape.hs b/src/Data/Array/Nested/Shaped/Shape.hs
index 3d4bf31..d1a72ea 100644
--- a/src/Data/Array/Nested/Shaped/Shape.hs
+++ b/src/Data/Array/Nested/Shaped/Shape.hs
@@ -314,10 +314,12 @@ shsLength :: ShS sh -> Int
 shsLength (ShS shx) = shxLength shx
 
 shsRank :: forall sh. ShS sh -> SNat (Rank sh)
-shsRank (ShS shx) =
-  gcastWith (unsafeCoerceRefl :: Rank (MapJust sh) :~: Rank sh) $
+shsRank (ShS shx) | Refl <- lemRankMapJust (Proxy @sh) =
   shxRank shx
 
+lemRankMapJust :: proxy sh -> Rank (MapJust sh) :~: Rank sh
+lemRankMapJust _ = unsafeCoerceRefl
+
 shsSize :: ShS sh -> Int
 shsSize (ShS sh) = shxSize sh
 
-- 
cgit v1.3