Agreed and better articulated than what I likely would have said On Thu, Jun 17, 2021 at 8:38 AM Sam Derbyshire wrote:

Hi Christiaan,

As far as I'm concerned that's a worrying regression, and I think you should file a ticket on the GHC tracker about it. I believe GHC already contains logic to avoid expanding type synonyms in error messages in certain situations, but it apparently doesn't apply here. Hopefully someone more knowledgeable about this can chime in.

Sam _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

I imagined solution 1. as: 1. reinstate the magic type family `(<=?) :: Nat -> Nat -> Bool` in GHC.TypeNats ``` module GHC.TypeNats where type family (m :: Nat) <=? (n :: Nat) :: Bool ``` 2. instead of exporting the following type alias from Data.Type.Ord ``` type (<=?) :: k -> k -> Bool type m <=? n = OrdCond (Compare m n) 'True 'True 'False ``` do: ``` import qualified GHC.TypeNats as T type (<=?) :: forall k . k -> k -> Bool type family (<=?) a b where (<=?) (a :: T.Nat) b = (T.<=?) a b (<=?) a b = OrdCond (Compare a b) 'True 'True 'False ``` I realize this is far from ideal On Thu, 17 Jun 2021 at 14:46, Adam Gundry wrote:

Hi Christiaan,

On 17/06/2021 10:43, Christiaan Baaij wrote:

...

[...]

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/eea96042f1e8682605ae68db10f2bcdd...

...

< https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd...

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?

I don't know the context for this change or the immediate feasibility of 1, but regarding the other two points:

GHC does in general try to avoid expanding type aliases if it doesn't need to (but it does expand type families). The difficulty here is that the constraint solver must expand the synonym to see if the constraint can be solved, and it seems hard (though perhaps not impossible) to keep track of the original forms of constraints as they get simplified by the solver.

Presumably it wouldn't be terribly difficult to add some built-in magic to GHC's error message printing machinery that looked through types for occurrences of specific patterns (like OrdCond with concrete arguments) and replaced them with simpler versions. It would be really nice, though, to have a way to specify this as a user, rather than it being limited to built-in magic.

I'm imagining having a pragma to mark type synonyms as "contractible", then when showing a type, GHC would try to match it against the RHSs of contractible synonyms in scope. If there are multiple matches, probably it should pick the most specific; I'm not sure if we should have some other mechanism for prioritization or if we should just accept arbitrary choices where there is overlap.

Does this sound useful to others? I think it could be really helpful for improving type error messages. It won't be in 9.2 though...

Best wishes,

Adam

-- Adam Gundry, Haskell Consultant Well-Typed LLP, https://www.well-typed.com/

Registered in England & Wales, OC335890 118 Wymering Mansions, Wymering Road, London W9 2NF, England

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 wrote:

Christiaan,

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

Thanks

Simon

*From:* ghc-devs *On Behalf Of *Christiaan Baaij *Sent:* 17 June 2021 10:44 *To:* ghc-devs *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/eea96042f1e8682605ae68db10f2bcdd... 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