Add an `Exists` type

[harpocrates]

Seems like this is a recurring request on StackOverflow and Reddit, and constraints looks to me like the place where it might belong:

data Exists c where
  Exists :: c a => a -> Exists c

This supports at least one interesting operator: foggy :: forall c1 c2. (forall a. c1 a :- c2 a) -> Exists c1 -> Exists c2. You also have the trivial elimination form and some useful instances¹:

withExists :: (forall a. c a => a -> r) -> Exists c -> r
withExists f (Exists x) = f x

instance Show (Exists Show) { show = withExists show }
deriving instance Typeable (Exists Typeable)
-- instance Hashable (Exists Hashable) ...
-- instance NFData (Exists NFData) ...

And, going out on a limb, you can observe one side (or both sides, if you are on a recent version of GHC) of the isomorphism between Exists Typeable and Dynamic

exists2Dyn :: Exists Typeable -> Dynamic
exists2Dyn = withExists toDyn

-- Possible only with `Type.Reflection` since `base-4.10.0.0`
dyn2Exists :: Exists Typeable -> Dynamic
dyn2Exists (Dynamic tr x) = withTypeable tr (Exists x)

If this sounds good, I'll open a PR. In any case, thanks for such an awesome package!

---

¹ You can have more interesting instances like instance Ord (Exists (Ord `And` Typeable)) if you also define a type-level conjunction And :: (* -> Constraint) -> (* -> Constraint) -> * -> Constraint - but that rabbit hole journeys away from constraints.

[lierdakil]

@harpocrates hi. It's been a while, but since lpaste is dead, could you perhaps post your foggy implementation here if possible? Thanks.

[harpocrates]

I think credit for the original foggy code and suggestion goes to @glguy. I don't have the original code anywhere, but I was able to recreate the following:

{-# LANGUAGE RankNTypes, TypeApplications, ScopedTypeVariables, TypeOperators, GADTs, ConstraintKinds #-}
import Data.Constraint

data Exists c where
  Exists :: c a => a -> Exists c

foggy :: forall c1 c2. (forall a. c1 a :- c2 a) -> Exists c1 -> Exists c2
foggy ev (Exists (x :: b)) = withDict (ev @b) (Exists x)

I don't recall ScopedTypeVariables being so helpful for binding existential type variables, so this code might be benefiting from recent GHC features (and may not be portable to older versions).

[lierdakil]

@harpocrates thanks again. It didn't even occur to me to use ScopedTypeVariables for binding the existential type variable here, that's nice to know it works this way!

FWIW, a version that eschews TypeApplications but is otherwise identical apparently works at least since GHC 7.10:

foggy ev (Exists (x :: b)) = withDict (ev :: c1 b :- c2 b) (Exists x)