{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
module M where

import GHC.Tuple (Solo)

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

data Rv v r a

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

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

usage = foo value