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

[Adam Gundry]

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