Degradation in error message clarity for ` GHC.TypeNats.<=?`
Summary
With the introduction of eea96042 the clarity of error messages involving GHC.TypeNats.<=?
has degraded compared to GHC 9.0.1 or earlier.
Steps to reproduce
Given this code TestInEq.hs
:
{-# 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
Expected behavior
On GHC 9.0.1 and prior, one would get the error message:
$ ghci TestInEq.hs
GHCi, version 9.0.1: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling TestInEq ( TestInEq.hs, interpreted )
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
| ^^^^^^^^^
Failed, no modules loaded.
ghci>
But on GHC 9.2.0.20210422, which includes eea96042, one gets the following error message
$ ghci TestInEq.hs
GHCi, version 9.2.0.20210422: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling TestInEq ( TestInEq.hs, interpreted )
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
| ^^^^^^^^^
Failed, no modules loaded.
ghci>
which I feel is far less clear.
At the least, I hope we can recover the error message of GHC 9.0.1 or earlier. And it would be even nicer if this could be fixed before the GHC 9.2.1 release. I can envision at least three possible solutions:
- Reinstate
(GHC.TypeNats.<=?) :: Nat -> Nat -> Bool
as a builtin type family - Somehow add a custom type-error to
Data.Type.Ord.OrdCond
- Don't expand type aliases in type errors
Following up on 3, it would be even nicer if we could actually get an error along the lines of:
TestInEq.hs:11:14: error:
• Couldn't satisfy ‘a <= (a + 1)’
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
| ^^^^^^^^^
where the type synonym (GHC.TypeNats.<=) :: Nat -> Nat -> Constraint
isn't expanded either.
This issue was/is also discussed at: https://mail.haskell.org/pipermail/ghc-devs/2021-June/019992.html
Environment
- GHC version used: 9.2.0.20210422