Specifying constraints on existentials from the outside

Foo.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Data.Kind (Constraint, Type)
import Data.Maybe (fromMaybe)
import GHC.TypeLits (ErrorMessage((:<>:)))
import Prelude
import Type.Reflection (type (:~~:)(HRefl), Typeable, eqTypeRep, typeRep)
import qualified GHC.TypeLits as TypeLits

data Foo :: [Type -> Constraint] -> Type where
  Foo :: (a `HasInstances` cs) => a -> Foo cs

-- This instance compiles fine
instance Eq (Foo '[Eq, Typeable]) where
  (Foo (x :: a)) == (Foo (y :: a')) =
    fromMaybe False do
      HRefl <- eqTypeRep (typeRep @a) $ typeRep @a'
      pure $ x == y

-- This instance does not compile, as GHC cannot deduce Eq/Typeable
--instance
--  ( Eq `Elem` cs
--  , Typeable `Elem` cs
--  ) => Eq (Foo cs) where
--  (Foo (x :: a)) == (Foo (y :: a')) =
--    fromMaybe False do
--      HRefl <- eqTypeRep (typeRep @a) $ typeRep @a'
--      pure $ x == y

type family HasInstances (x :: Type) (cs :: [Type -> Constraint]) :: Constraint where
  HasInstances x '[] = ()
  HasInstances x (c ': cs) = (c x, x `HasInstances` cs)

type Elem a as = ElemGo a as as
type family ElemGo (a :: k) (as :: [k]) (as' :: [k]) :: Constraint where
  ElemGo a (a ': as) as' = ()
  ElemGo y (a ': as) as' = ElemGo y as as'
  ElemGo a '[] as' =
    TypeLits.TypeError
      ( 'TypeLits.ShowType a
          ':<>: 'TypeLits.Text " is not an element of "
          ':<>: 'TypeLits.ShowType as'
      )