Insoluble constraints arising from an ambiguity check are reported poorly

The way GHC reports insoluble constraints arising from an ambiguity check seems rather poor, as I discovered in #21149 (closed).

Example 1: an insoluble equality constraint.

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind ( Type )

class C (a :: Type)
instance ( Maybe w ~ Bool ) => C ()

error:
    * Couldn't match type `Maybe w0' with `Bool'
      Expected: forall w. ((Maybe w :: *) ~ (Bool :: *)) => C ()
        Actual: forall w. ((Maybe w :: *) ~ (Bool :: *)) => C ()
    * In the ambiguity check for an instance declaration
      In the instance declaration for `C ()'
  |
8 | instance ( Maybe w ~ Bool ) => C ()
  |          ^^^^^^^^^^^^^^^^^^^^^^^^^^

Note the strange Expected/Actual message which makes no sense.

---

By the way: this program is accepted if one doesn't enable -XUndecidableInstances, as the ambiguity check appears to be skipped altogether in that case. This seems to be due to the following code in checkValidInstance:

        -- Note that the Termination Condition is *more conservative* than
        -- the checkAmbiguity test we do on other type signatures
        --   e.g.  Bar a => Bar Int is ambiguous, but it also fails
        --   the termination condition, because 'a' appears more often
        --   in the constraint than in the head
        ; undecidable_ok <- xoptM LangExt.UndecidableInstances
        ; if undecidable_ok
          then checkAmbiguity ctxt ty
          else checkInstTermination theta tau

This seems to be an example where checkInstTermination is not stricter than checkAmbiguity.

---

Example 2: an insoluble custom type error.

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind    ( Type )
import GHC.TypeLits ( TypeError, ErrorMessage(..) )

class C (a :: Type)
instance TypeError ( ShowType w ) => C ()

error:
    * w0
    * In the ambiguity check for an instance declaration
      In the instance declaration for `C ()'
  |
9 | instance TypeError ( ShowType w ) => C ()
  |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I think these error messages are quite confusing. I think it would be better to adjust the way we report unsolved constraints arising from an ambiguity check to make it a bit clearer.

(The issue with TypeError was introduced in 9.3, as we used to not consider a type error to be insoluble and thus would allow it to go unsolved in an ambiguity check with -XAllowAmbiguousTypes.)