Error message degradation for (<= :: Nat -> Nat -> Constraint) in GHC 9.2+

[Christiaan Baaij]

I have reported the issue here:
https://gitlab.haskell.org/ghc/ghc/-/issues/20009

On Thu, 17 Jun 2021 at 18:44, Simon Peyton Jones <simonpj at microsoft.com>
wrote:

> 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 at haskell.org> *On Behalf Of *Christiaan
> Baaij
> *Sent:* 17 June 2021 10:44
> *To:* ghc-devs <ghc-devs at 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
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fhackage.haskell.org%2Fpackage%2Fghc-typelits-natnormalise&data=04%7C01%7Csimonpj%40microsoft.com%7C42380a30e7f54d6ad06708d931747622%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637595199077626853%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000&sdata=MDuOq05JaifjtEkq7JrdjmmwgCWEtIyZ%2BYqIFNv7FhY%3D&reserved=0>
> 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
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2F-%2Fcommit%2Feea96042f1e8682605ae68db10f2bcdd7dab923e&data=04%7C01%7Csimonpj%40microsoft.com%7C42380a30e7f54d6ad06708d931747622%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637595199077636846%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000&sdata=FfAQaEksSYEWNjOzuOmwhPXz6lI%2F5o5LT%2Ftwbh42wFM%3D&reserved=0>
>
>
>
> 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
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210617/b0fa11f0/attachment.html>