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/Convert.hs | |
| parent | 2e29470184d9b64b91d2709b7ac1f97f6c797886 (diff) | |
Follow up the equal-rank-coercibility introduction
Diffstat (limited to 'src/Data/Array/Nested/Convert.hs')
| -rw-r--r-- | src/Data/Array/Nested/Convert.hs | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/src/Data/Array/Nested/Convert.hs b/src/Data/Array/Nested/Convert.hs index c27c4c2..6be0f74 100644 --- a/src/Data/Array/Nested/Convert.hs +++ b/src/Data/Array/Nested/Convert.hs @@ -67,9 +67,12 @@ ixrFromIxS Prelude.. coerce ixrFromIxS' :: forall sh i. SNat (Rank sh) -> IxS sh i -> IxR (Rank sh) i -ixrFromIxS' _ = coerce - Prelude.. (unsafeCoerce :: IxX (MapJust sh) i -> IxX (Replicate (Rank sh) Nothing) i) - Prelude.. coerce +ixrFromIxS' _ + | Refl <- lemRankReplicate (Proxy @(Rank sh)) + , Refl <- lemRankMapJust (Proxy @sh) + = coerce + Prelude.. (coerceEqualRankListX :: ListX (MapJust sh) i -> ListX (Replicate (Rank sh) Nothing) i) + Prelude.. coerce -- ixrFromIxX re-exported @@ -99,9 +102,12 @@ ixsFromIxR Prelude.. coerce ixsFromIxR' :: forall sh i. ShS sh -> IxR (Rank sh) i -> IxS sh i -ixsFromIxR' _ = coerce - Prelude.. (unsafeCoerce :: IxX (Replicate (Rank sh) Nothing) i -> IxX (MapJust sh) i) - Prelude.. coerce +ixsFromIxR' _ + | Refl <- lemRankReplicate (Proxy @(Rank sh)) + , Refl <- lemRankMapJust (Proxy @sh) + = coerce + Prelude.. (coerceEqualRankListX :: ListX (Replicate (Rank sh) Nothing) i -> ListX (MapJust sh) i) + Prelude.. coerce -- ixsFromIxX re-exported |