Define ix?FromLinear without TH

1 files changed, 10 insertions, 4 deletions

diff --git a/src/Data/Array/Nested/Ranked/Shape.hs b/src/Data/Array/Nested/Ranked/Shape.hs
index 6ce0f4f..59289fb 100644
--- a/src/Data/Array/Nested/Ranked/Shape.hs
+++ b/src/Data/Array/Nested/Ranked/Shape.hs
@@ -39,10 +39,10 @@ import GHC.IsList (IsList)
 import GHC.IsList qualified as IsList
 import GHC.TypeLits
 import GHC.TypeNats qualified as TN
+import Unsafe.Coerce (unsafeCoerce)
 
 import Data.Array.Nested.Lemmas
 import Data.Array.Nested.Mixed.Shape
-import Data.Array.Nested.Mixed.Shape.Internal
 import Data.Array.Nested.Permutation
 import Data.Array.Nested.Types
 
@@ -300,6 +300,15 @@ ixrToLinear = \sh i -> go sh i 0
     go ZSR ZIR a = a
     go (n :$: sh) (i :.: ix) a = go sh ix (fromIntegral n * a + i)
 
+{-# INLINEABLE ixrFromLinear #-}
+ixrFromLinear :: forall i m. Num i => IShR m -> Int -> IxR m i
+ixrFromLinear (ShR sh) i
+  | Refl <- lemRankReplicate (Proxy @m)
+  = ixrFromIxX $ ixxFromLinear sh i
+
+ixrFromIxX :: IxX sh i -> IxR (Rank sh) i
+ixrFromIxX = unsafeCoerce
+
 
 -- * Ranked shapes
 
@@ -505,6 +514,3 @@ listrCastWithName :: String -> SNat n' -> ListR n i -> ListR n' i
 listrCastWithName _ SZ ZR = ZR
 listrCastWithName name (SS n) (i ::: l) = i ::: listrCastWithName name n l
 listrCastWithName name _ _ = error $ name ++ ": ranks don't match"
-
-$(ixFromLinearStub "ixrFromLinear" [t| IShR |] [t| IxR |] [p| ZSR |] (\a b -> [p| $a :$: $b |]) [| ZIR |] [| (:.:) |] [| shrToList |])
-{-# INLINEABLE ixrFromLinear #-}