I think what you *probably* want is the below. Does that satisfy your needs?

N.B. you really will need `Typeable`

otherwise you’re never really going to be able to do anything with the constraints you have. There are very few `phi`

s that satisfy `forall x. psi (A x)`

but many interesting ones that satisfy `forall x. Typeable x => psi (A x)`

!

```
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoStarIsType #-}
{-# OPTIONS_GHC -Wall #-}
-- requires packages: singletons, constraints
import Data.Constraint (Dict (Dict))
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (Proxy))
import Data.Singletons (Sing, SingI, sing)
import Data.Typeable (Typeable)
import Type.Reflection (someTypeRep)
type Cases :: Type -> Type
data Cases x = A x | B x | C x
-- {
-- This singletons stuff is mechanical, and can (in theory) be
-- autogenerated. Perhaps singletons-th does it?
type SCases :: forall (x :: Type) -> Cases x -> Type
data SCases x c where
SA :: (Typeable t) => SCases x (A t)
SB :: (Typeable t) => SCases x (B t)
SC :: (Typeable t) => SCases x (C t)
type instance Sing @(Cases x) = SCases x
instance (Typeable x) => SingI (A x) where
sing = SA
instance (Typeable x) => SingI (B x) where
sing = SB
instance (Typeable x) => SingI (C x) where
sing = SC
-- }
caseAnalysis ::
forall (x :: Type) (psi :: Cases x -> Constraint) (y :: Cases x).
( forall x'. (Typeable x') => psi (A x'),
forall x'. (Typeable x') => psi (B x'),
forall x'. (Typeable x') => psi (C x'),
SingI y
) =>
Dict (psi y)
caseAnalysis = case sing @y of
SA -> Dict
SB -> Dict
SC -> Dict
class CC (t :: Cases x) where
showCImpl :: Proxy t -> String
showC :: forall t. (CC t) => String
showC = showCImpl (Proxy @t)
showTypeable :: forall t. (Typeable t) => String
showTypeable = show (someTypeRep (Proxy @t))
instance (Typeable x) => CC (A x) where
showCImpl _ = "A " ++ showTypeable @x
instance (Typeable x) => CC (B x) where
showCImpl _ = "B " ++ showTypeable @x
instance (Typeable x) => CC (C x) where
showCImpl _ = "C " ++ showTypeable @x
usage :: (SingI y) => Dict (CC y)
usage = caseAnalysis
-- > example
-- "A 5"
example :: String
example = case usage @(A 5) of Dict -> showC @(A 5)
```