A generic way to use existential quantification to generalize data over type variables.

ghostbuster.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}

import GHC.Exts (Constraint)

data SuchThat (c :: [k -> Constraint]) (p :: k -> *) = forall s. Constrain c s => SuchThat (p s)

type family Constrain (c :: [k -> Constraint]) (x :: k) :: Constraint where
  Constrain (c ': '[]) x = c x
  Constrain (c ': cs) x = (c x,Constrain cs x)
  Constrain '[] x = x ~ x

-- An unconstrained SuchThat. Only useful for Ghost Busting (removing phantom types) and reading structure
--data ForAny (p :: k -> *) = forall s. ForAny (p s)
type ForAny = SuchThat '[]

-- "Inject" a value into a SuchThat. It becomes more ambiguous because it throws out the exact type of s
ambiguate :: Constrain c s => p s -> SuchThat c p
ambiguate = SuchThat

-- Escape from a SuchThat by running a continuation with the context
onFA :: SuchThat c p -> (forall s. Constrain c s => p s -> r) -> r
onFA (SuchThat ps) f = f ps

-- Example usage of ForAny
-- Reads the structure of the Maybe, but not the contents

testForAny :: Bool
testForAny = onFA exampleValue isJust -- == True

isJust :: Maybe a -> Bool
isJust (Just _) = True
isJust Nothing = False

exampleValue :: ForAny Maybe
exampleValue = ambiguate $ Just 5

exampleNot :: ForAny Maybe
exampleNot = ambiguate Nothing