Have fun with All and HList

AllHList.hs

{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# OPTIONS_GHC -Wall              #-}

module AllHList where

import Data.Constraint
import Data.Void

data HList (as :: [*]) :: * where
  HNil  :: HList '[]
  HCons :: a -> HList as -> HList (a ': as)

type family All (c :: * -> Constraint) (as :: [*]) :: Constraint where
  All c '[]       = ()
  All c (a ': as) = (c a, All c as)

printHList :: All Show as => HList as -> IO ()
printHList = \case
  HNil       -> return ()
  HCons v vs -> print v >> printHList vs

data In (a :: *) (as :: [*]) :: * where
  Here  :: In a (a ': as)
  There :: In a as -> In a (b ': as)

type family (:=:) (x :: *) (y :: *) :: Bool where
  x :=: x = 'True
  x :=: y = 'False

class x :=: y ~ 'False => NotEq x y where

notIn :: All (NotEq x) as => In x as -> Void
notIn (There v) = notIn v