Trying to handle constraints flexibly with existentials

Test.hs

{-# LANGUAGE
    ConstraintKinds
  , ExistentialQuantification
  , FlexibleContexts
  , FlexibleInstances
  , KindSignatures
  , MultiParamTypeClasses
  , Rank2Types
  , ScopedTypeVariables
  , TypeApplications
  , TypeOperators
  , UndecidableInstances
  , UndecidableSuperClasses
#-}
module Test where

import Data.Typeable
import GHC.Exts (Constraint)


-- https://github.com/glaebhoerl/exists/blob/master/Control/Constraint/Combine.hs
-- provides a type class for combining/aliasing two constraints as follows:

class (c a, d a) => (c :&: d) a
instance (c a, d a) => (c :&: d) a
infixl 7 :&:


-- We define an existential datatype that is parameterised over the constraint:
data Ex c = forall a. c a => Ex a

-- This allows us to write, e.g. `Ex (Num :&: Show)` and know that the value
-- contained inside the existential must have both Num and Show instances.


-- exApp allows us to extract a value from its Ex context and apply a function
-- to it, so long as the function satisfies the constraint on the Ex
exApp :: forall c r. (forall a. c a => a -> r) -> Ex c -> r
exApp f (Ex a) = f a


-- The following type class allows use to say whether a particular constraint,
-- which could be a compound constraint of the form `c1 :&: c2 :&: .. cn`,
-- contains a particular single constraint, and cast our existential in terms of
-- it.
--
-- This is inspired by Data.Constraint, but I'm trying to make it work in the
-- context of Ex, which doesn't have a concrete constraint to work with...

class (a :: * -> Constraint) :- (b :: * -> Constraint) where
  castConstraint :: Ex a -> Ex b
instance c :- c where
  castConstraint ex = ex
instance {-# OVERLAPPABLE #-} (c1 :&: c2) :- c2 where
  castConstraint (Ex a) = Ex a
instance {-# OVERLAPS #-} (c1 :- c3) => (c1 :&: c2) :- c3 where
  castConstraint (Ex a) = castConstraint (Ex @c1 a)


-- The combination of exApp and castConstraint allows us to write a Show
-- instance for Ex that works for any (possibly combined) context:

instance (ctx :- Show) => Show (Ex ctx) where
  show ex = "Ex " ++ (exApp @Show show $ castConstraint ex)


-- We can even write some functions that can do type-safe application of binary
-- functions, provided that we can cast the values inside the Ex's:

eq :: (Eq a, Typeable a, Typeable b) => a -> b -> Maybe Bool
eq = f2 (==)

f2 :: (Typeable a, Typeable b) => (a -> a -> r) -> a -> b -> Maybe r
f2 f x y = f x <$> cast y

exApp2 :: forall c1 c2 r. (forall a b. (c1 a, c2 b) => a -> b -> r) -> Ex c1 -> Ex c2 -> r
exApp2 f (Ex a) (Ex b) = f a b

-- This allows us to write:
--
-- > three = Ex 3 :: Ex (Eq :&: Typeable)
-- > four = Ex 4 :: Ex (Eq :&: Typeable)
-- > hello = Ex "hello" :: Ex (Eq :&: Typeable)
-- > exApp2 eq three three
-- Just True
-- > exApp2 eq three four
-- Just False
-- > exApp2 eq three hello
-- Nothing

-- So far, so good. _But_, I can't work out how to define an Eq instance for Ex.
-- The Show instance used the type application of @Show and castConstraint to
-- make sure we could get from Ex (c1 :&: c2 .. cn) where one of the c's was
-- definitely Show to (Ex Show). But I need somehow to make an Ex who's
-- constraint is both Eq and Typeable.

-- It feels like I want to be able to write a subset test somehow, such that I
-- can do casts like:
--   Ex (c1 :&: c2 :&: c3 :&: c4) -> Ex (c2 :&: c4)
-- But I'm struggling with the type classes as it is.

-- Am I going about this in even a remotely sane way?
-- Am I trying to do something that's just impossible?

-- Any help much appreciated!