Dynamically pattern matching nested GADT back out of a wrapper

I recently asked how to make a homogenous list of GADT instances: Function returning result of any constructor of a GADT

tl;dr

{-#LANGUAGE GADTs, EmptyDataDecls #-}
module Main where

-- Define a contrived GADT
data TFoo
data TBar
data Thing a where
  Foo :: Int -> Thing TFoo
  Bar :: String -> Thing TBar

data SomeThing = forall a. SomeThing (Thing a)

combine :: [SomeThing]
combine = [Something $ Foo 1, SomeThing $ Bar "abc"]

Now, I'm having some trouble dynamically "unwrapping" them. Let's say we have this (still contrived, but closer to my real use case) code:

{-#LANGUAGE GADTs, EmptyDataDecls #-}
module Main where

-- Define a contrived GADT
data Thing a where
  Thing :: TKind a -> Thing a

data TFoo
data TBar
data TKind a where
  Foo :: TKind TFoo
  Bar :: TKind TBar

data SomeThing = forall a. SomeThing (Thing a)

example :: SomeThing
example = SomeThing $ Thing Foo

extractThingWithTKind :: TKind a -> SomeThing -> Either String (Thing a)
extractThingWithTKind k st = case st of
                               SomeThing t@(Thing k) -> Right t
                               _                     -> Left "nope"

The above doesn't work because the t in Right t doesn't have the type Thing a. Intrinsically, I understand why this doesn't work. Pattern matching on the k doesn't do what I want (only match if the k is the same as the one passed in). But this is my best stab at approximating what I want. I tried instanceing Eq on TKind a, but because (==) :: a -> a -> Bool, this won't work (the equality depends on potentially disparate types at runtime). I could wrap TKind like I did Thing, but then I'd just be pushing the problem lower.

Removing the dynamism, I tried just pattern matching out a Thing TFoo explicitly:

extractThingWithFoo :: SomeThing -> Either String (Thing TFoo)
extractThingWithFoo st = case st of
                            SomeThing t@(Thing Foo) -> Right t
                            _                       -> Left "nope"

And that works! But does this mean that I can't do the dynamic matching? It would be a real pain to have to duplicate the above method for each kind TKind (in the non-contrived version, there are many). The only other solution I see is changing SomeThing to be a sum type that has one wrapper for each TKind, but then you're just moving the duplicated code to a different place (and forcing all uses of SomeThing to pattern match each).

Solution

In order to implement a function with the signature extractThingWithTKind :: TKind a -> SomeThing -> Either String (Thing a), we need to be able to decide that what's inside SomeThing is a TKind a or not. GADT constructors are witnesses of such type equalities, but they need to be explicitly pattern-matched on to "unwrap" these assumptions in the function's local scope.

extractThingWithTKind :: TKind a -> SomeThing -> Either String (Thing a)
extractThingWithTKind Foo (SomeThing t@(Thing Foo)) = Right t
extractThingWithTKind Bar (SomeThing t@(Thing Bar)) = Right t
extractThingWithTKind _ _ = Left "nope"

Pattern matching on the first argument gives rise to the assumption that a ~ TFoo (in the first case), and further pattern matching on the second argument proves that the thing inside SomeThing is also a TFoo. Crucially, the individual cases have to be spelled out one by one, as it's the constructors themselves that provide the evidence.