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

import GHC.TypeLits
import Data.Kind

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) => BooleanOfMatchesRev b r where
instance (b ~ BooleanOf r) => BooleanOfMatchesRev b r where

foo :: (CRanked (BooleanOfMatches Bool) r, CRanked (BooleanOfMatchesRev Bool) r)
    => BooleanOf (TensorOf n r) -> BooleanOf (TensorOf k r) -> BooleanOf (TensorOf k r)
foo b1 b2 = if True then b1 else b2