I'd like to pattern match on some GADT constructor and get the associated type in scope and I'd like it to work with wildcard in cases were all the cases are known, but apparently it does not type check.

ReifyGADTWildCard.hs

{-# OPTIONS -Wall #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE GADTs #-}


-- Note that all the @@t@@ in this GADT are explicit
-- So at compile time, there is no ambiguity on this list
data Foo t where
  A :: Foo [Int]
  B :: Foo Ordering
  C :: Foo Float

data AnyFoo where
  AnyFoo :: Foo t -> AnyFoo

-- I want to resolve a constraint (here 'Show') based on the
-- @@t@@ from @@Foo t@@.
-- This implementation is explicit, hence works for all @@t@@ known in @@Foo t@@
reifyImplictShow :: AnyFoo -> String
reifyImplictShow (AnyFoo v) = case v of
  (A :: Foo t) -> show @t undefined
  (B :: Foo t) -> show @t undefined
  (C :: Foo t) -> show @t undefined

{-
-- This one should work, because by construction @@t \in {[Int], Ordering, Float}@@
-- which all have a 'Show' instance.
-- However GHC is unable to find the instance for @@Show t@@.
reifyWildcardShow :: AnyFoo -> String
reifyWildcardShow (AnyFoo v) = case v of
  (_ :: Foo t) -> show @t undefined
-}

-- I'd also interested by non wildcard matching
-- Here I want to use the 'Monoid' instance, which only works for 'A' and 'B', but not 'C'.
-- This works, again, with an exhaustive listing
reifyImplictMonoid :: AnyFoo -> String
reifyImplictMonoid (AnyFoo v) = case v of
  (C :: Foo t) -> error "not possible"
  (A :: Foo t) -> show (mempty @t)
  (B :: Foo t) -> show (mempty @t)

-- This one should work, because by construction @@t \in {[Int],
-- Ordering}@@. The case @@t ~ Float@@ was removed due to the first
-- match. The remaining cases all have a 'Monoid' instance.
-- which all have a 'Monoid' instance.
{-
reifyWildcardMonoid :: AnyFoo -> String
reifyWildcardMonoid (AnyFoo v) = case v of
  C -> error "Not possible"
  (_ :: Foo t) -> show (mempty @t)
-}