diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2026-04-09 00:59:15 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-09 18:39:54 +0200 |
| commit | 2e29470184d9b64b91d2709b7ac1f97f6c797886 (patch) | |
| tree | c8ea9b71575022cfc77569857aab7fb4306f20e6 /src/Data/Array/Nested/Convert.hs | |
| parent | 27f5fd474a85bd0c404215a1ce38ed378594e54b (diff) | |
Make equal-rank-coercibility part of the interface of ListX
Diffstat (limited to 'src/Data/Array/Nested/Convert.hs')
| -rw-r--r-- | src/Data/Array/Nested/Convert.hs | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/src/Data/Array/Nested/Convert.hs b/src/Data/Array/Nested/Convert.hs index a6a09f6..c27c4c2 100644 --- a/src/Data/Array/Nested/Convert.hs +++ b/src/Data/Array/Nested/Convert.hs @@ -46,6 +46,7 @@ import Unsafe.Coerce (unsafeCoerce) import Data.Array.Nested.Lemmas import Data.Array.Nested.Mixed +import Data.Array.Nested.Mixed.ListX import Data.Array.Nested.Mixed.Shape import Data.Array.Nested.Ranked.Base import Data.Array.Nested.Ranked.Shape @@ -58,9 +59,12 @@ import Data.Array.Nested.Types -- * To ranked ixrFromIxS :: forall sh i. 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 ixrFromIxS' :: forall sh i. SNat (Rank sh) -> IxS sh i -> IxR (Rank sh) i ixrFromIxS' _ = coerce @@ -87,9 +91,12 @@ shrFromShX = coerce -- * To shaped ixsFromIxR :: forall sh i. 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 ixsFromIxR' :: forall sh i. ShS sh -> IxR (Rank sh) i -> IxS sh i ixsFromIxR' _ = coerce |