{-# 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 BooleanOf r

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

class c (TensorOf n r) => CTensorOf c n r where
instance c (TensorOf n r) => CTensorOf c n r where

class (BooleanOf (TensorOf n (Primal a)) ~ BooleanOf (IntOf a)) => B n a where
instance (BooleanOf (TensorOf n (Primal a)) ~ BooleanOf (IntOf a)) => B n a where

type BundleOfConstraints :: Type -> Constraint
type BundleOfConstraints r = (Num r, forall n. KnownNat n => CTensorOf Num n r)

foo :: BundleOfConstraints r => TensorOf n r -> TensorOf n r
foo x = x

foo2 :: (p ~ Primal r, forall n. CTensorOf Num n p) => TensorOf n r -> TensorOf n (Primal r) -> TensorOf n (Primal r)
foo2 _ x = x

foo3 :: (forall n. B n a) => TensorOf n a -> TensorOf n a
foo3 x = x

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