diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-09 18:04:58 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-09 18:39:57 +0200 |
| commit | bcf3bcf63626e75af9ab316d988e146f9a60c81d (patch) | |
| tree | 956c3d5fd9a27974079fb8f3d5267df470656f25 /src/Data/Array/Nested/Shaped | |
| parent | 2e29470184d9b64b91d2709b7ac1f97f6c797886 (diff) | |
Follow up the equal-rank-coercibility introduction
Diffstat (limited to 'src/Data/Array/Nested/Shaped')
| -rw-r--r-- | src/Data/Array/Nested/Shaped/Shape.hs | 6 |
1 files changed, 4 insertions, 2 deletions
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 |