Constrained typed extractions with GADTs

Things.hs

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE ViewPatterns              #-}

module Things where

-- Data
data X = X String Bool Char

-- What I get as input
data Ty = STRING | BOOL | INT

-- Representation of things I can pick out of the data.
data Thing :: * -> * where
    TString :: Thing String
    TBool   :: Thing Bool
    TInt    :: Thing Char

-- Existentialized version of Thing, witnesses the constraint that I'll need.
data SomeThing
    = forall k. Show k => SomeThing (Thing k)

-- A polymorphic structure
data Foo a b = Foo a b deriving Show

toSomeThing :: Ty -> SomeThing
toSomeThing BOOL   = SomeThing TBool
toSomeThing INT    = SomeThing TInt
toSomeThing STRING = SomeThing TString

-- dependently-typed extraction
extractThing :: Thing a -> X -> a
extractThing TString (X s b i) = s
extractThing TBool   (X s b i) = b
extractThing TInt    (X s b i) = i

-- Extract various parts of something into a polymorphic structure
extractThings :: Thing a -> Thing b -> X -> Foo a b
extractThings ta tb x = Foo (extractThing ta x) (extractThing tb x)

-- a "dependently typed" operation but returns a simple type
doit :: (Show a, Show b) => Thing a -> Thing b -> X -> String
doit ta tb = show . extractThings ta tb

-- monomorphic signature version
doitSimple :: Ty -> Ty -> X -> String
doitSimple (toSomeThing -> SomeThing ta) (toSomeThing -> SomeThing tb) = doit ta tb

-- But this doesn't work!
--doitBad :: Ty -> Ty -> X -> String
--doitBad a b = doit ta tb
--    where
--        (SomeThing ta) = toSomeThing a
--        (SomeThing tb) = toSomeThing b