Degradation in error message clarity for ` GHC.TypeNats.<=?`

Summary

With the introduction of eea96042 the clarity of error messages involving GHC.TypeNats.<=? has degraded compared to GHC 9.0.1 or earlier.

Steps to reproduce

Given this code TestInEq.hs:

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
module TestInEq where

import Data.Proxy
import GHC.TypeLits

proxyInEq :: (a <= b) => Proxy a -> Proxy b -> ()
proxyInEq _ _ = ()

proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()
proxyInEq1 = proxyInEq

Expected behavior

On GHC 9.0.1 and prior, one would get the error message:

$ ghci TestInEq.hs 
GHCi, version 9.0.1: https://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling TestInEq         ( TestInEq.hs, interpreted )

TestInEq.hs:11:14: error:
    • Couldn't match type ‘a <=? (a + 1)’ with ‘'True’
        arising from a use of ‘proxyInEq’
    • In the expression: proxyInEq
      In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
    • Relevant bindings include
        proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
          (bound at TestInEq.hs:11:1)
   |
11 | proxyInEq1 = proxyInEq
   |              ^^^^^^^^^
Failed, no modules loaded.
ghci>

But on GHC 9.2.0.20210422, which includes eea96042, one gets the following error message

$ ghci TestInEq.hs 
GHCi, version 9.2.0.20210422: https://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling TestInEq         ( TestInEq.hs, interpreted )

TestInEq.hs:11:14: error:
    • Couldn't match type ‘Data.Type.Ord.OrdCond
                             (CmpNat a (a + 1)) 'True 'True 'False’
                     with ‘'True’
        arising from a use of ‘proxyInEq’
    • In the expression: proxyInEq
      In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
    • Relevant bindings include
        proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
          (bound at TestInEq.hs:11:1)
   |
11 | proxyInEq1 = proxyInEq
   |              ^^^^^^^^^
Failed, no modules loaded.
ghci> 

which I feel is far less clear.

At the least, I hope we can recover the error message of GHC 9.0.1 or earlier. And it would be even nicer if this could be fixed before the GHC 9.2.1 release. I can envision at least three possible solutions:

1. Reinstate (GHC.TypeNats.<=?) :: Nat -> Nat -> Bool as a builtin type family
2. Somehow add a custom type-error to Data.Type.Ord.OrdCond
3. Don't expand type aliases in type errors

Following up on 3, it would be even nicer if we could actually get an error along the lines of:

TestInEq.hs:11:14: error:
    • Couldn't satisfy ‘a <= (a + 1)’
        arising from a use of ‘proxyInEq’
    • In the expression: proxyInEq
      In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
    • Relevant bindings include
        proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
          (bound at TestInEq.hs:11:1)
   |
11 | proxyInEq1 = proxyInEq
   |              ^^^^^^^^^

where the type synonym (GHC.TypeNats.<=) :: Nat -> Nat -> Constraint isn't expanded either.

This issue was/is also discussed at: https://mail.haskell.org/pipermail/ghc-devs/2021-June/019992.html

Environment

• GHC version used: 9.2.0.20210422