Warning for redundant constraints: interaction with pattern matching

Herbert gives this example:

{-# LANGUAGE GADTs, DataKinds, TypeOperators, UnicodeSyntax #-}
   
import GHC.TypeLits
   
data List l t where
     Nil  ∷ List 0 t
     (:-) ∷ t → List l t → List (l+1) t
   
head' ∷ (1<=l) ⇒ List l t → t
head' (x :- _) = x

We get the warning

  typelits1.hs:9:9: Warning:
      Redundant constraint: 1 <= l
      In the type signature for: head' ∷ (1 <= l) ⇒ List l t → t

But of course the warning is not redundant if we want to exclude the (head' Nil) case.

Here's an example that only depends on GADTs:

{-# LANGUAGE GADTs #-}
data T a where
  TT :: T Bool
  TF :: T Int

f :: T Bool -> Bool
f TT = True

g :: (a ~ Bool) => T a -> Bool
g TT = True

Here f compiles fine, but g warns about a redundant constraint, even though the two types are isomorphic! And indeed the evidence for (a~Bool) is not used in the code for g. But that evidence is used to prove that the un-matched pattern (g TF) is unreachable.

I'm not sure how to fix this. Bother.