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 <a...@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 >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs