How can I produce a Tag type for any datatype for use with DSum, without Template Haskell?

background

I want to write some library code, which internally uses DSum to manipulate a user's datatype. DSum requires a 'tag' type that has a single type argument. However I want my code to work with just any old concrete type. So, I'd like to just take the user's type and automatically produce the tag type. I've asked a very similar question here How can I programatically produce this datatype from the other?, and gotten a great answer. That answer relies on TH, mainly so that it can create top-level declarations. However, I actually don't care about the top-level declaration, and I'd prefer to avoid the TH if possible.

question

[How] can I write, with some generic programming technique, a datatype

data Magic t a ...

where given some arbitrary sum type, e.g.

data SomeUserType = Foo Int | Bar Char | Baz Bool String

Magic SomeUserType is equivalent to this 'tag' type that can be used with DSum?

data TagSomeUserType a where
  TagFoo :: TagSomeUserType Int
  TagBar :: TagSomeUserType Char
  TagBaz :: TagSomeUserType (Bool, String)

Solution

Unlike some here have claimed, it is perfectly sensible (and in fact quite straightforward, with the correct library - generics-sop) to define such a type. Essentially all the machinery is provided by this library already:

{-# LANGUAGE PatternSynonyms, PolyKinds, DeriveGeneric #-} 

import Generics.SOP 
import qualified GHC.Generics as GHC 
import Data.Dependent.Sum

data Tup2List :: * -> [*] -> * where 
  Tup0 :: Tup2List () '[] 
  Tup1 :: Tup2List x '[ x ] 
  TupS :: Tup2List r (x ': xs) -> Tup2List (a, r) (a ': x ': xs) 

newtype GTag t i = GTag { unTag :: NS (Tup2List i) (Code t) }

The type GTag is what you call Magic. The actual 'magic' happens in the Code type family, which compute the generic representation of a type, as a list of lists of types. The type NS (Tup2List i) xs means that for precisely one of xs, Tup2List i holds - this is simply a proof that a list of arguments is isomorphic to some tuple.

All the classes you need can be derived:

data SomeUserType = Foo Int | Bar Char | Baz Bool String 
  deriving (GHC.Generic, Show) 
instance Generic SomeUserType

You can define some pattern synonyms for the tags valid for this type:

pattern TagFoo :: () => (x ~ Int) => GTag SomeUserType x 
pattern TagFoo = GTag (Z Tup1) 

pattern TagBar :: () => (x ~ Char) => GTag SomeUserType x 
pattern TagBar = GTag (S (Z Tup1)) 

pattern TagBaz :: () => (x ~ (Bool, String)) => GTag SomeUserType x 
pattern TagBaz = GTag (S (S (Z (TupS Tup1))))

and a simple test:

fun0 :: GTag SomeUserType i -> i -> String 
fun0 TagFoo i = replicate i 'a' 
fun0 TagBar c = c : [] 
fun0 TagBaz (b,s) = (if b then show else id) s 

fun0' = \(t :& v) -> fun0 t v 

main = mapM_ (putStrLn . fun0' . toTagVal) 
          [ Foo 10, Bar 'q', Baz True "hello", Baz False "world" ]

Since this is expressed in terms of a generic type function, you can write generic operations over tags. For example, exists x . (GTag t x, x) is isomorphic to t for any Generic t:

type GTagVal t = DSum (GTag t) I 

pattern (:&) :: forall (t :: * -> *). () => forall a. t a -> a -> DSum t I
pattern t :& a = t :=> I a     

toTagValG_Con :: NP I xs -> (forall i . Tup2List i xs -> i -> r) -> r 
toTagValG_Con Nil k = k Tup0 () 
toTagValG_Con (I x :* Nil) k = k Tup1 x
toTagValG_Con (I x :* y :* ys) k = toTagValG_Con (y :* ys) (\tp vl -> k (TupS tp) (x, vl))

toTagValG :: NS (NP I) xss -> (forall i . NS (Tup2List i) xss -> i -> r) -> r 
toTagValG (Z x) k = toTagValG_Con x (k . Z)
toTagValG (S q) k = toTagValG q (k . S)

fromTagValG_Con :: i -> Tup2List i xs -> NP I xs 
fromTagValG_Con i Tup0 = case i of { () -> Nil } 
fromTagValG_Con x Tup1 = I x :* Nil 
fromTagValG_Con xs (TupS tg) = I (fst xs) :* fromTagValG_Con (snd xs) tg 

toTagVal :: Generic a => a -> GTagVal a 
toTagVal a = toTagValG (unSOP $ from a) ((:&) . GTag)

fromTagVal :: Generic a => GTagVal a -> a 
fromTagVal (GTag tg :& vl) = to $ SOP $ hmap (fromTagValG_Con vl) tg

As for the need for Tup2List, it is needed for the simply reason that you represent a constructor of two arguments (Baz Bool String) as a tag over a tuple of (Bool, String) in your example.

You could also implement it as

type HList = NP I -- from generics-sop 

data Tup2List i xs where Tup2List :: Tup2List (HList xs) xs

which represents the arguments as a heterogeneous list, or even more simply

newtype GTag t i = GTag { unTag :: NS ((:~:) i) (Code t) }
type GTagVal t = DSum (GTag t) HList  

fun0 :: GTag SomeUserType i -> HList i -> String 
fun0 TagFoo (I i :* Nil) = replicate i 'a' 
fun0 ...

However, the tuple representation does have the advantage that unary tuples are 'projected' to the single value which is in the tuple (i.e., instead of (x, ())). If you represent arguements in the obvious way, functions such as fun0 must pattern match to retrieve the single value stored in a constructor.