{-# language TypeFamilies, DataKinds, UndecidableSuperClasses, UndecidableInstances, TypeFamilyDependencies, QuantifiedConstraints #-}
module M where
import GHC.TypeLits

data FArray (n :: Nat)
instance Num (FArray n)

class Tensor r where
  type TensorOf r = (t :: Nat -> *) | t -> r
  type Primal r

instance Tensor Float where
  type TensorOf Float = FArray
  type Primal Float = Float

foo :: (t ~ TensorOf r, forall n. Num (t n)) => TensorOf r n -> TensorOf r n
foo x = x

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

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

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

foo2 :: (forall n. CTensorOf n a) => a -> a
foo2 x = x