{-# Language GADTs,TypeOperators,PolyKinds,DataKinds,TypeFamilies,TypeInType #-}
data State s a where
 Basecase' :: Basecase s a -> State s a
 Nested'   :: Nested s a xs   -> State s a

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

data Nested (s :: *) (a :: *) (xs :: [* -> * -> *]) where
 Nested :: (Head xs ~ x) => x s a -> Nested s a xs