{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
{-# LANGUAGE ConstraintKinds, DataKinds, GADTs, TypeFamilies, TypeOperators #-}

module T9747 where
import Data.List (intercalate)
import Data.Proxy
import Data.Kind (Type, Constraint)

data HList :: [Type] -> Type where
  Nil :: HList '[]
  Cons :: a -> HList as -> HList (a ': as)

type family HListAll (c :: Type -> Constraint)
                     (ts :: [Type]) :: Constraint where
  HListAll c '[] = ()
  HListAll c (t ': ts) = (c t, HListAll c ts)

showHList :: HListAll Show ts => HList ts -> String
showHList = ("[" ++ ) . (++"]") . intercalate ", " . go
  where
    go :: HListAll Show ts => HList ts -> [String]
    go Nil = []
    go (Cons x xs) = show x : go xs

-- Things work okay up to this point
test :: String
test = showHList (Cons (2::Int)
                 (Cons (3.1 :: Float)
                 (Cons 'c' Nil)))

type family ConFun (t :: Type) :: Type -> Constraint
data Tag
type instance ConFun Tag = Group

class (Show a, Eq a, Ord a) => Group a

-- This is notionally similar to showHList
bar :: HListAll (ConFun l) ts => Proxy l -> HList ts -> ()
bar _ _ = ()

baz :: (ConFun l a, ConFun l b) => Proxy l -> HList [a,b] -> ()
baz = bar