{-# LANGUAGE ImpredicativeTypes, TypeFamilies, DataKinds, OverloadedLists, QuantifiedConstraints,
             UndecidableInstances #-}

import Data.Kind (Constraint, Type)
import GHC.TypeLits (KnownNat, Nat)

type family IntOf (f :: Type -> k -> Type) r :: Type

type family BooleanOf t

data Array :: Nat -> Type -> Type

fromList :: forall r n. KnownNat n => [Int] -> [r] -> Array n r
fromList = undefined

assertEqualUpToEpsilon'
    :: (v ~ Array m r, g ~ Array n r)
    => Array n r
    -> (v, g)
    -> ()
assertEqualUpToEpsilon' = undefined

rev' :: forall r m n v g.
        (v ~ Array m r, g ~ Array n r)
     => (forall f x. ADReady22 f x => f x n -> f x m)
     -> (v, g)
rev' = undefined

testReluSimpler :: ()
testReluSimpler =
  assertEqualUpToEpsilon'
    (fromList [] [])  -- (fromList @Double @2 [] []) -- compiles fine
    (rev' @Double @2 (relu @2))

relu
  :: forall n r f. ADReady22 f r
  => f r n -> f r n
relu v = undefined

class ( BooleanOf (IntOf f r) ~ BooleanOf (f r n)
      , BooleanOf (f r n) ~ BooleanOf (IntOf f r) )
      => BooleanOfMatches f r n where
instance
      ( BooleanOf (IntOf f r) ~ BooleanOf (f r n)
      , BooleanOf (f r n) ~ BooleanOf (IntOf f r) )
      => BooleanOfMatches f r n where

class (forall yf. c f r yf) => CRankedF f r c where
instance (forall yf. c f r yf) => CRankedF f r c where

type ADReady22 f r =
  (
-- uncommenting the line below make the example compile fine:
    CRankedF f r BooleanOfMatches
  ) :: Constraint