<div dir="ltr"><div>Hi Ghc-Devs,</div><div><br></div><div>When upgrading one of our tc plugins 
<a href="https://hackage.haskell.org/package/ghc-typelits-natnormalise" target="_blank">https://hackage.haskell.org/package/ghc-typelits-natnormalise</a> to GHC 9.2, one of our tests, repeated here:<br><br>```</div><div>{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}<br>module TestInEq where<br><br>import Data.Proxy<br>import GHC.TypeLits<br><br>proxyInEq :: (a <= b) => Proxy a -> Proxy b -> ()<br>proxyInEq _ _ = ()<br><br>proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()<br>proxyInEq1 = proxyInEq<br>```</div><div><br></div><div>degraded quite badly in terms of the error message. <br></div><div>Where in GHC 9.0.1 we get:</div><div><br></div><div>```</div><div>TestInEq.hs:11:14: error:<br>    • Couldn't match type ‘a <=? (a + 1)’ with ‘'True’<br>        arising from a use of ‘proxyInEq’<br>    • In the expression: proxyInEq<br>      In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq<br>    • Relevant bindings include<br>        proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()<br>          (bound at TestInEq.hs:11:1)<br>   |<br>11 | proxyInEq1 = proxyInEq<br>   |      <br></div><div>```</div><div><br></div><div>with GHC 9.2.0.20210422 we get:</div><div><br></div><div>```</div><div>TestInEq.hs:11:14: error:<br>    • Couldn't match type ‘Data.Type.Ord.OrdCond<br>                             (CmpNat a (a + 1)) 'True 'True 'False’<br>                     with ‘'True’<br>        arising from a use of ‘proxyInEq’<br>    • In the expression: proxyInEq<br>      In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq<br>    • Relevant bindings include<br>        proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()<br>          (bound at TestInEq.hs:11:1)<br>   |<br>11 | proxyInEq1 = proxyInEq<br>   |<br>```</div><div><br></div><div>
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.

</div><div><br></div><div>This change in error message is due to: <a href="https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e">https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e</a></div><div><br></div><div>Is there a way we can get the nicer pre-9.2.0.2021 error message again before the proper 9.2.1 release?</div><div>e.g. by doing one of the following:</div><div>1. Reinstate `(<=? :: Nat -> Nat -> Bool)` as a builtin type family<br></div><div>2. Somehow add a custom type-error to `Data.Type.Ord.OrdCond`</div><div>3. Don't expand type aliases in type errors</div><div><br>

</div><div>What do you think? should this be fixed? should this be fixed before the 9.2.1 release?</div><div><br></div><div>-- Christiaan<br></div><div><br></div></div>