{-# Language GADTSyntax,ExistentialQuantification,TypeOperators,PolyKinds,DataKinds,TypeFamilies,TypeInType ,DatatypeContexts#-}

import GHC.Exts

type family State (x :: * -> * -> *) :: Constraint where
 State Basecase = ()
 State (Nested xs) = ()

data Basecase s a where
 Stream' :: Stream s a -> Basecase s a
 Linear' :: Linear s a -> Basecase s a
 Stack'  :: Stack  s a -> Basecase s a

data Stream s a = Stream (a,s)

data Linear s a = Linear (a,s) | End a

data Stack  s a = Stack  (a,s) | Empty

type family Head (xs :: [a]) :: a where
 Head (x ': xs) = x

type family All (f :: k -> Constraint) (xs :: [k]) :: Constraint where
 All _ '[] = ()
 All f (x ': xs) = (f x,All f xs)
{-
data (All State xs) => Nested (xs :: [* -> * -> *]) (s :: *) (a :: *) where
 Nested :: (State x,Head xs ~ x) => x s a -> Nested xs s a
{-
    No context is allowed on a GADT-style data declaration
    (You can put a context on each constructor, though.)
   |
27 | data (All State xs) => Nested (xs :: [* -> * -> *]) (s :: *) (a :: *) where
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
-}

data (All State xs) => Nested (xs :: [* -> * -> *]) (s :: *) (a :: *) = Nested {unNested :: (State x,Head xs ~ x) => x s a}

{-
   |
27 | data (All State xs) => Nested (xs :: [* -> * -> *]) (s :: *) (a :: *) = Nested {unNested :: (State x,Head xs ~ x) => x s a}
   |                                                                                                                      ^
-}
-}