{-# LANGUAGE DataKinds, TypeFamilies, AllowAmbiguousTypes, UndecidableInstances, TypeFamilyDependencies #-}
{-# OPTIONS -dsuppress-all -O0 #-}
import Data.Kind
import Data.Typeable

main :: IO ()
main = do
  print (check @[Bool, Int])
  -- print (check @[Float, Bool, Double, Int])

{-# NOINLINE check #-}
check :: forall xs. Extendss Proxy xs => ()
check = ()

-- New
type ReportUnsolved :: () -> Constraint -> Constraint
type family ReportUnsolved a b where
  ReportUnsolved '() x = x

type Extendss :: ([Type] -> Type) -> [Type] -> Constraint 
type family Extendss p xs where
  Extendss p '[] = ()
  Extendss p (x : xs) = (ExtendsWith p x `ReportUnsolved` Extendss p xs)
  
type Extends p x = ExtendsWith p x ~ '()

type ExtendsWith :: ([Type] -> Type) -> Type -> ()
type family ExtendsWith p x where
  ExtendsWith Proxy Bool = '()
  ExtendsWith Proxy Int = '()

-- Old

-- type Extendss :: ([Type] -> Type) -> [Type] -> Constraint 
-- type family Extendss p xs where
--   Extendss p '[] = ()
--   Extendss p (x : xs) = (Extends p x, Extendss p xs)
  

-- type Extends :: ([Type] -> Type) -> Type -> Constraint
-- type family Extends p x where
--   Extends Proxy Bool = ()
--   Extends Proxy Int = ()