<div dir="ltr"><div>I imagined solution 1. as:</div><div><br></div><div>1. reinstate the magic type family `(<=?) :: Nat -> Nat -> Bool` in GHC.TypeNats</div><div>```</div><div>module GHC.TypeNats where</div><div><br></div><div>type family (m :: Nat) <=? (n :: Nat) :: Bool<br>```</div><div><br></div><div>2. instead of exporting the following type alias from Data.Type.Ord<br>```</div><div>type (<=?) :: k -> k -> Bool<br>type m <=? n = OrdCond (Compare m n) 'True 'True 'False<br>```</div><div><br></div><div>do:<br><br>```</div><div>import qualified GHC.TypeNats as T</div><div><br></div><div>type (<=?) :: forall k . k -> k -> Bool<br>type family (<=?) a b where<br>  (<=?) (a :: T.Nat) b = (T.<=?) a b<br>  (<=?) a b            = OrdCond (Compare a b) 'True 'True 'False<br>```</div><div><br></div><div>I realize this is far from ideal<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, 17 Jun 2021 at 14:46, Adam Gundry <<a href="mailto:adam@well-typed.com">adam@well-typed.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Christiaan,<br>
<br>
<br>
On 17/06/2021 10:43, Christiaan Baaij wrote:<br>
> [...]<br>
> <br>
> Errors messages involving type-level naturals and their operations<br>
> already weren't the poster-child of comprehensable GHC error messages,<br>
> but this change has made the situation worse in my opinion.<br>
> <br>
> This change in error message is due to:<br>
> <a href="https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e" rel="noreferrer" target="_blank">https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e</a><br>
> <<a href="https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e" rel="noreferrer" target="_blank">https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e</a>><br>
> <br>
> Is there a way we can get the nicer pre-9.2.0.2021 error message again<br>
> before the proper 9.2.1 release?<br>
> e.g. by doing one of the following:<br>
> 1. Reinstate `(<=? :: Nat -> Nat -> Bool)` as a builtin type family<br>
> 2. Somehow add a custom type-error to `Data.Type.Ord.OrdCond`<br>
> 3. Don't expand type aliases in type errors<br>
> <br>
> What do you think? should this be fixed? should this be fixed before the<br>
> 9.2.1 release?<br>
<br>
I don't know the context for this change or the immediate feasibility of<br>
1, but regarding the other two points:<br>
<br>
GHC does in general try to avoid expanding type aliases if it doesn't<br>
need to (but it does expand type families). The difficulty here is that<br>
the constraint solver must expand the synonym to see if the constraint<br>
can be solved, and it seems hard (though perhaps not impossible) to keep<br>
track of the original forms of constraints as they get simplified by the<br>
solver.<br>
<br>
Presumably it wouldn't be terribly difficult to add some built-in magic<br>
to GHC's error message printing machinery that looked through types for<br>
occurrences of specific patterns (like OrdCond with concrete arguments)<br>
and replaced them with simpler versions. It would be really nice,<br>
though, to have a way to specify this as a user, rather than it being<br>
limited to built-in magic.<br>
<br>
I'm imagining having a pragma to mark type synonyms as "contractible",<br>
then when showing a type, GHC would try to match it against the RHSs of<br>
contractible synonyms in scope. If there are multiple matches, probably<br>
it should pick the most specific; I'm not sure if we should have some<br>
other mechanism for prioritization or if we should just accept arbitrary<br>
choices where there is overlap.<br>
<br>
Does this sound useful to others? I think it could be really helpful for<br>
improving type error messages. It won't be in 9.2 though...<br>
<br>
Best wishes,<br>
<br>
Adam<br>
<br>
<br>
-- <br>
Adam Gundry, Haskell Consultant<br>
Well-Typed LLP, <a href="https://www.well-typed.com/" rel="noreferrer" target="_blank">https://www.well-typed.com/</a><br>
<br>
Registered in England & Wales, OC335890<br>
118 Wymering Mansions, Wymering Road, London W9 2NF, England<br>
</blockquote></div>