Safe casting type over several potential types

I currently have a pattern similar to the following happening in my code (this is simplified from the actual code, which is a large GADT that handles 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:

• Is there a better way to specify a constraint that always fails instead ('True ~ 'False)
  
  ?
• mkT1
  
  looks a little hacky, but it looks like it works. Is there a better way to do this?
• Is there a better way to structure the whole thing (I realize this is a tricky question as I cannot include all the details of what I am trying to achieve in a long enough post, but I am basically generating a parse tree).