{-# language ImpredicativeTypes, TypeFamilies, DataKinds, UndecidableSuperClasses, UndecidableInstances, TypeFamilyDependencies, QuantifiedConstraints #-}
module M where
import GHC.TypeLits
import Data.Type.Equality
import Data.Kind

data FArray (n :: Nat)
instance KnownNat n => Num (FArray n)

class Tensor r where
  type TensorOf (n :: Nat) r = t | t -> n r
  type Primal r
  type IntOf r
  
type family BooleanOf r

instance Tensor Float where
  type TensorOf n Float = FArray n
  type Primal Float = Float
  type IntOf Float = Int

type instance BooleanOf Float = Bool
type instance BooleanOf Int = Bool
type instance BooleanOf (FArray n) = Bool

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

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

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

type BundleOfConstraints :: Type -> Constraint
type BundleOfConstraints r = 
  (Num r, CRanked (BooleanOfMatches (BooleanOf (IntOf r))) (Primal r))

foo :: (BundleOfConstraints r, Eq (BooleanOf (IntOf r)))
   => BooleanOf (IntOf r) -> BooleanOf (TensorOf n (Primal r)) -> TensorOf n r -> TensorOf n r
foo b1 b2 r = if b1 == b2 then r else r

bar :: FArray n -> FArray n
bar x = foo undefined undefined x