1 files changed, 13 insertions, 4 deletions
diff --git a/src/Data/Array/Mixed/Shape.hs b/src/Data/Array/Mixed/Shape.hs
index 363b772..a13a176 100644
--- a/src/Data/Array/Mixed/Shape.hs
+++ b/src/Data/Array/Mixed/Shape.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImportQualifiedPost #-}
 {-# LANGUAGE NoStarIsType #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
@@ -22,7 +23,9 @@
 module Data.Array.Mixed.Shape where
 
 import Control.DeepSeq (NFData(..))
-import qualified Data.Foldable as Foldable
+import Data.Bifunctor (first)
+import Data.Coerce
+import Data.Foldable qualified as Foldable
 import Data.Functor.Const
 import Data.Kind (Type, Constraint)
 import Data.Monoid (Sum(..))
@@ -30,12 +33,10 @@ import Data.Proxy
 import Data.Type.Equality
 import GHC.Generics (Generic)
 import GHC.IsList (IsList)
-import qualified GHC.IsList as IsList
+import GHC.IsList qualified as IsList
 import GHC.TypeLits
 
 import Data.Array.Mixed.Types
-import Data.Coerce
-import Data.Bifunctor (first)
 
 
 -- | The length of a type-level list. If the argument is a shape, then the
@@ -307,6 +308,10 @@ shxEnum = \sh -> go sh id []
     go ZSX f = (f ZIX :)
     go (n :$% sh) f = foldr (.) id [go sh (f . (i :.%)) | i <- [0 .. fromSMayNat' n - 1]]
 
+shxRank :: ShX sh f -> SNat (Rank sh)
+shxRank ZSX = SNat
+shxRank (_ :$% sh) | SNat <- shxRank sh = SNat
+
 
 -- * Static mixed shapes
 
@@ -377,6 +382,10 @@ ssxFromShape :: IShX sh -> StaticShX sh
 ssxFromShape ZSX = ZKX
 ssxFromShape (n :$% sh) = fromSMayNat (\_ -> SUnknown ()) SKnown n :!% ssxFromShape sh
 
+ssxFromSNat :: SNat n -> StaticShX (Replicate n Nothing)
+ssxFromSNat SZ = ZKX
+ssxFromSNat (SS (n :: SNat nm1)) | Refl <- lemReplicateSucc @(Nothing @Nat) @nm1 = SUnknown () :!% ssxFromSNat n
+
 
 -- | Evidence for the static part of a shape. This pops up only when you are
 -- polymorphic in the element type of an array.