Make ranked and shaped lists newtypes over mixed

1 files changed, 29 insertions, 35 deletions

diff --git a/src/Data/Array/Nested/Shaped/Shape.hs b/src/Data/Array/Nested/Shaped/Shape.hs
index d59f65c..97d1559 100644
--- a/src/Data/Array/Nested/Shaped/Shape.hs
+++ b/src/Data/Array/Nested/Shaped/Shape.hs
@@ -47,14 +47,35 @@ import Data.Array.Nested.Types
 
 type role ListS nominal representational
 type ListS :: [Nat] -> Type -> Type
-data ListS sh i where
-  ZS :: ListS '[] i
-  (::$) :: forall n sh {i}. i -> ListS sh i -> ListS (n : sh) i
-deriving instance Eq i => Eq (ListS sh i)
-deriving instance Ord i => Ord (ListS sh i)
+newtype ListS sh i = ListS (ListX (MapJust sh) i)
+  deriving (Eq, Ord, NFData, Functor, Foldable)
+
+pattern ZS :: forall sh i. () => sh ~ '[] => ListS sh i
+pattern ZS <- ListS (matchZX -> Just Refl)
+  where ZS = ListS ZX
+
+matchZX :: forall sh i. ListX (MapJust sh) i -> Maybe (sh :~: '[])
+matchZX ZX | Refl <- lemMapJustEmpty @sh Refl = Just Refl
+matchZX _ = Nothing
 
+pattern (::$)
+  :: forall {sh1} {i}.
+     forall n sh. (n : sh ~ sh1)
+  => i -> ListS sh i -> ListS sh1 i
+pattern i ::$ sh <- (listsUncons -> Just (UnconsListSRes sh i))
+  where i ::$ ListS sh = ListS (i ::% sh)
 infixr 3 ::$
 
+data UnconsListSRes i sh1 =
+  forall n sh. (n : sh ~ sh1) => UnconsListSRes (ListS sh i) i
+listsUncons :: forall sh1 i. ListS sh1 i -> Maybe (UnconsListSRes i sh1)
+listsUncons (ListS (x ::% sh')) | Refl <- lemMapJustHead (Proxy @sh1)
+                                , Refl <- lemMapJustCons @sh1 Refl =
+  Just (UnconsListSRes (ListS sh') x)
+listsUncons (ListS _) = Nothing
+
+{-# COMPLETE ZS, (::$) #-}
+
 #ifdef OXAR_DEFAULT_SHOW_INSTANCES
 deriving instance Show i => Show (ListS sh i)
 #else
@@ -62,16 +83,6 @@ instance Show i => Show (ListS sh i) where
   showsPrec _ = listsShow shows
 #endif
 
-instance NFData i => NFData (ListS n i) where
-  rnf ZS = ()
-  rnf (x ::$ l) = rnf x `seq` rnf l
-
-data UnconsListSRes i sh1 =
-  forall n sh. (n : sh ~ sh1) => UnconsListSRes (ListS sh i) i
-listsUncons :: ListS sh1 i -> Maybe (UnconsListSRes i sh1)
-listsUncons (x ::$ sh') = Just (UnconsListSRes sh' x)
-listsUncons ZS = Nothing
-
 listsShow :: forall sh i. (i -> ShowS) -> ListS sh i -> ShowS
 listsShow f l = showString "[" . go "" l . showString "]"
   where
@@ -79,22 +90,6 @@ listsShow f l = showString "[" . go "" l . showString "]"
     go _ ZS = id
     go prefix (x ::$ xs) = showString prefix . f x . go "," xs
 
-instance Functor (ListS l) where
-  {-# INLINE fmap #-}
-  fmap _ ZS = ZS
-  fmap f (x ::$ xs) = f x ::$ fmap f xs
-
-instance Foldable (ListS l) where
-  {-# INLINE foldMap #-}
-  foldMap _ ZS = mempty
-  foldMap f (x ::$ xs) = f x <> foldMap f xs
-  {-# INLINE foldr #-}
-  foldr _ z ZS = z
-  foldr f z (x ::$ xs) = f x (foldr f z xs)
-  toList = listsToList
-  null ZS = False
-  null _ = True
-
 listsLength :: ListS sh i -> Int
 listsLength = length
 
@@ -315,8 +310,9 @@ pattern (:$$)
   :: forall {sh1}.
      forall n sh. (n : sh ~ sh1)
   => SNat n -> ShS sh -> ShS sh1
-pattern i :$$ shl <- (shsUncons -> Just (UnconsShSRes i shl))
-  where i :$$ ShS shl = ShS (SKnown i :$% shl)
+pattern i :$$ sh <- (shsUncons -> Just (UnconsShSRes i sh))
+  where i :$$ ShS sh = ShS (SKnown i :$% sh)
+infixr 3 :$$
 
 data UnconsShSRes sh1 =
   forall n sh. (n : sh ~ sh1) => UnconsShSRes (SNat n) (ShS sh)
@@ -326,8 +322,6 @@ shsUncons (ShS (SKnown x :$% sh'))
   = Just (UnconsShSRes x (ShS sh'))
 shsUncons (ShS _) = Nothing
 
-infixr 3 :$$
-
 {-# COMPLETE ZSS, (:$$) #-}
 
 #ifdef OXAR_DEFAULT_SHOW_INSTANCES