Pattern match checker should treat TypeError as unsatisfiable

Consider this code from !6066 (closed)

  type (<=?) :: Int -> Int -> Bool

  type (<=) x y = Assert (x <=? y) (TypeError blah-blah)
  type family Assert (check :: Bool) (errMsg :: Constraint) :: Constraint where
    Assert 'True  _errMsg = ()
    Assert _check errMsg  = errMsg

and this use:

data List n t where
     Nil  :: List 0 t
     (:-) :: t -> List n t -> List (n+1) t

head' :: (1 <= n) => List n t -> t
head' (x :- _) = x  -- No need for a Nil case!

The pattern match checker will want to check that the Nil case is unreachable. In the Nil case, the (1 <= n) constraint becomes 1 <= 0, which simplifies (via Assert) to TypeError blah-blah.

And that TypeError @Constraint blahblah should be treated as unsatisfiable by the pattern match checker!

NB: there is some discussion here about having an explicit Unsatisfiable constraint, a more principled cousin of TypeError.

Actually this all came up in #11503 (closed), five years ago. Let's nail it!