{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
module M where
import GHC.Tuple (Solo)
import Data.Kind (Type)
import GHC.TypeLits


data Rv v r a

value :: (Rv 0 r Char, Rv v r Bool)
value = undefined

-- type family attempt:

type family TupleN_M m xs = r | r -> m xs where
 TupleN_M m '[x] = (Solo (m x))
 TupleN_M m '[x1, x2] = (m x1, m x2)

-- foo :: TupleN_M (Rv v r) (x:xs) -> ()
-- foo = undefined

-- usage = foo value


-- type class attempt:

class CTupleN_M r where
  type MonadOf r :: Type -> Type
  type XsOf r :: [Type]

instance CTupleN_M (Solo (m (x :: Type))) where
  type MonadOf (Solo (m x)) = m
  type XsOf (Solo (m x)) = '[x]

instance m ~ m' => CTupleN_M (m (x1 :: Type), m' x2) where
  type MonadOf (m x1, m' x2) = m
  type XsOf (m x1, m' x2) = '[x1, x2]

class Failure r where
-- instance TypeError (Text "m is " :<>: ShowType (MonadOf r) :$$:
--                     Text "xs is " :<>: ShowType (XsOf r)) => Failure r

fooC ::
  ( Rv v r ~ m
  , (CTupleN_M (TupleN_M m xs))
  ) =>
  TupleN_M m xs -> ()
fooC = undefined

usageC = fooC value