TypeError reporting is too aggressive

Summary: we are reporting TypeError calls too aggressively. This is blocking !6066 (closed). An easy fix is available.

Consider this, derived from an ongoing MR.

type Assert :: Bool -> Constraint -> Constraint
type family Assert check errMsg where
  Assert 'True _      = ()
  Assert _     errMsg = errMsg

foo_sym :: Assert 'True (TypeError (Text "Boom")) => Proxy a -> ()
foo_sym Proxy = ()

We get

T6066.hs:14:12: error:
    • Boom
    • In the type signature:
        foo_sym :: Assert 'True (TypeError (Text "Boom")) => Proxy a -> ()
   |
14 | foo_sym :: Assert 'True (TypeError (Text "Boom")) => Proxy a -> ()
   |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

But this is silly: the Assert call is going to discard that TypeError. And not only is it silly, it actually prevents some useful applications of TypeError. Here is a less contrived signature:

foo_sym :: forall a. (Assert (IsInt a) ErrSyn) => Proxy a -> ()

We want to blow up on calls of foo_sym where IsInt a turns out to be False.

You can hide the TypeError inside a nullary type family like this:

type family HiddenTypeError where
  HiddenTypeError = TypeError (Text "Boom")

foo_sym :: Assert 'True HiddenTypeError => Proxy a -> ()

but that is obviously grotesque.

Proposed solution

When checking the validity of a user-written type signature (in GHC.Tc.Validity.checkValidType), we currently complain if TypeError occurs anywhere. Proposed solution:

• checkValidType complains of TypeError, ignoring occurrences in the argument of a type family

So it would not look at the arguments of Assert above.

Any views? This is closely related to #20180 (closed) and #20181 (closed).