TF.hs

type family KnownBools (bs :: [Bool]) :: Constraint where
  KnownBools '[] = ()
  KnownBools (b ': bs) = (KnownBool b, KnownBools bs)

type family KnownBools (bs :: [Bool]) :: Constraint where
  KnownBools '[] = ()
  KnownBools '[b1] = (KnownBool b1)
  KnownBools '[b1, b2] = (KnownBool b1, KnownBool b2)
  KnownBools '[b1, b2, b3] = (KnownBool b1, KnownBool b2, KnownBool b3)
  KnownBools (b1 ': b2 ': b3 ': b4 ': bs) = (KnownBool b1, KnownBool b2, KnownBool b3, KnownBool b4, KnownBools bs)

How does divide and conquer compare?

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.Types

class KnownBool b

type family BothCons a b c where
	BothCons x y '(xs,ys) = '(x:xs, y:ys)

type family BothKnownBool a where
	BothKnownBool '(as, bs) = (KnownBools as, KnownBools bs)

type family Split xs where
	Split (x : y : rest) = BothCons x y (Split rest)
	Split xs = '(xs, '[])

type family KnownBools bs :: Constraint where
	KnownBools '[] = ()
	KnownBools '[b] = KnownBool b
	KnownBools bs = BothKnownBool (Split bs)

Simpler, but still divide and conquer:

type family Evens xs where
	Evens (x : xs) = x : Odds xs
	Evens '[] = '[]

type family Odds xs where
	Odds (x : xs) = Evens xs
	Odds '[] = '[]

type family KnownBools bs :: Constraint where
	KnownBools '[] = ()
	KnownBools '[b] = KnownBool b
	KnownBools xs = (KnownBools (Evens xs), KnownBools (Odds xs))