Type safe casting to multiple potential types

I've currently got a pattern like the following happening in my code (this is simplified from the actual code which is a large GADT dealing with expressions).

data I = A | B | C | D

type family TC1 (a :: I) :: Constraint where
  TC1 'A = ()
  TC1 'C = ()
  TC1 _ = ('True ~ 'False)

type family TC4 (a :: I) :: Constraint where
  TC4 'B = ()
  TC4 'C = ()
  TC4 'D = ()
  TC4 _ = ('True ~ 'False)

data T (t :: I) where
  T1 :: (TC1 t) => T t
  T2 :: T B
  T3 :: T t
  T4 :: (TC4 t) => T t
  etc

castL :: (Typeable t) => [Maybe t] -> Maybe t
castL l = case catMaybes l of
  (x:_) -> Just x
  [] -> Nothing

mkT1 :: Typeable a => Maybe (T a)
mkT1 = castL [cast (T1 :: T 'A), cast (T1 :: T 'C)]

A few questions:

1. Is there a nicer way to specify a constraint that always fails instead of ('True ~ 'False)?
2. mkT1 looks a bit hacky but it does seem to work. Is there a nicer way of doing it?
3. Is there a better way to structure the whole thing (I understand this is a tricky question as I can't include all the detail of what I'm trying to achieve in a reasonably length post, but I'm basically generating a parse tree).