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

[Christiaan Baaij]

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 <adam at well-typed.com> 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/eea96042f1e8682605ae68db10f2bcdd7dab923e
> > <
> 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?
>
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210617/e7a4b27f/attachment.html>