Temporarily revert ListS as a newtype over ListX

until a GHC workaround is found. Please revert this commit ASAP
so that horde-ad can coerce shaped to mixed things for free
(unless the cost of the new WrapJust type turns out to overweight
the benefit, which is unlikely, and/or unless unsafeCoerce works
without WrapJust somehow).

1 files changed, 9 insertions, 31 deletions

diff --git a/src/Data/Array/Nested/Shaped/Shape.hs b/src/Data/Array/Nested/Shaped/Shape.hs
index f3e2c1e..bfc6ad2 100644
--- a/src/Data/Array/Nested/Shaped/Shape.hs
+++ b/src/Data/Array/Nested/Shaped/Shape.hs
@@ -52,34 +52,14 @@ import Data.Array.Nested.Types
 
 -- * Shaped lists
 
-type role ListS nominal nominal
-newtype ListS sh f = ListS (ListX (MapJust sh) (WrapJust f))
+type role ListS nominal representational
+type ListS :: [Nat] -> (Nat -> Type) -> Type
+data ListS sh f where
+  ZS :: ListS '[] f
+  (::$) :: forall n sh {f}. f n -> ListS sh f -> ListS (n : sh) f
 deriving instance (forall n. Eq (f n)) => Eq (ListS sh f)
 deriving instance (forall n. Ord (f n)) => Ord (ListS sh f)
 
-type role WrapJust nominal nominal
-data WrapJust f n where
-  WrapJust :: f n -> WrapJust f (Just n)
-deriving instance (forall m. Eq (f m)) => Eq (WrapJust f n)
-deriving instance (forall m. Ord (f m)) => Ord (WrapJust f n)
-
-pattern ZS :: () => sh ~ '[] => ListS sh f
-pattern ZS <- ListS (matchZS -> Just Refl)
-  where ZS = ListS ZX
-
-matchZS :: forall sh f. ListX (MapJust sh) f -> Maybe (sh :~: '[])
-matchZS ZX | Refl <- lemMapJustEmpty @sh Refl = Just Refl
-matchZS _ = Nothing
-
-pattern (::$)
-  :: forall {sh1} {f}.
-     forall n sh. (n : sh ~ sh1)
-  => f n -> ListS sh f -> ListS sh1 f
-pattern n ::$ sh <- (listsUncons -> Just (UnconsListSRes sh n))
-  where n ::$ ListS sh = ListS (WrapJust n ::% sh)
-
-{-# COMPLETE ZS, (::$) #-}
-
 infixr 3 ::$
 
 #ifdef OXAR_DEFAULT_SHOW_INSTANCES
@@ -95,11 +75,9 @@ instance (forall m. NFData (f m)) => NFData (ListS n f) where
 
 data UnconsListSRes f sh1 =
   forall n sh. (n : sh ~ sh1) => UnconsListSRes (ListS sh f) (f n)
-listsUncons :: forall sh1 f. ListS sh1 f -> Maybe (UnconsListSRes f sh1)
-listsUncons (ListS (WrapJust x ::% sh'))
-  | Refl <- lemMapJustCons @sh1 Refl
-  = Just (UnconsListSRes (ListS sh') x)
-listsUncons (ListS ZX) = Nothing
+listsUncons :: ListS sh1 f -> Maybe (UnconsListSRes f sh1)
+listsUncons (x ::$ sh') = Just (UnconsListSRes sh' x)
+listsUncons ZS = Nothing
 
 -- | This checks only whether the types are equal; if the elements of the list
 -- are not singletons, their values may still differ. This corresponds to
@@ -224,7 +202,7 @@ listsPermutePrefix perm sh = listsAppend (listsPermute perm (listsTakeLenPerm pe
 -- * Shaped indices
 
 -- | An index into a shape-typed array.
-type role IxS nominal nominal
+type role IxS nominal representational
 type IxS :: [Nat] -> Type -> Type
 newtype IxS sh i = IxS (ListS sh (Const i))
   deriving (Eq, Ord, Generic)