{-# language TypeFamilies, DataKinds, UndecidableInstances, QuantifiedConstraints #-}
module M where

import GHC.TypeLits
import Data.Kind

data Tagged (n :: Nat) r = MkTagged

type family TensorOf (n :: Nat) (r :: Type)

type family BooleanOf r

class (forall y. c (TensorOf y r)) => CRanked c r where
instance (forall y. c (TensorOf y r)) => CRanked c r where

class (BooleanOf r ~ b) => BooleanOfMatches b r where
instance (BooleanOf r ~ b) => BooleanOfMatches b r where

{-
class (b ~ BooleanOf r) => BooleanOfMatches' b r where
instance (b ~ BooleanOf r) => BooleanOfMatches' b r where
-}

foo :: (CRanked (BooleanOfMatches Bool) r)
   => BooleanOf (TensorOf n r) -> Tagged n r -> Tagged n r
foo b2 r = if b2 then MkTagged else MkTagged

{-
foo' :: (CRanked (BooleanOfMatches' Bool) r)
   => BooleanOf (TensorOf n r) -> Tagged n r -> Tagged n r
foo' b2 r = if b2 then MkTagged else MkTagged
-}