Christiaan,

Do please submit a bug report on GHC’s issue tracker, with a way to reproduce it.

Thanks

Simon

From: ghc-devs <ghc-devs-bounces@haskell.org> On Behalf Of Christiaan Baaij
Sent: 17 June 2021 10:44
To: ghc-devs <ghc-devs@haskell.org>
Subject: Error message degradation for (<= :: Nat -> Nat -> Constraint) in GHC 9.2+

Hi Ghc-Devs,

When upgrading one of our tc plugins https://hackage.haskell.org/package/ghc-typelits-natnormalise to GHC 9.2, one of our tests, repeated here:

```

{-# 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
```

degraded quite badly in terms of the error message.

Where in GHC 9.0.1 we get:

```

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
   |     

```

with GHC 9.2.0.20210422 we get:

```

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
   |
```

Errors messages involving type-level naturals and their operations already weren't the poster-child of comprehensable GHC error messages, but this change has made the situation worse in my opinion.

This change in error message is due to: https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e

Is there a way we can get the nicer pre-9.2.0.2021 error message again before the proper 9.2.1 release?

e.g. by doing one of the following:

1. Reinstate `(<=? :: 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

What do you think? should this be fixed? should this be fixed before the 9.2.1 release?

-- Christiaan