Implementation of GHC.TypeLits.<= is still not quite right
base-4.6
(GHC 7.6) introduced:
module GHC.TypeLits where
class (m :: Nat) <= (n :: Nat)
type family (m :: Nat) <=? (n :: Nat) :: Bool
where both <=
and <=?
had hard-coded resolution rules.
Then in base-4.7
(GHC 7.8) we got:
type x <= y = (x <=? y) ~ True
type family (m :: Nat) <=? (n :: Nat) :: Bool
Where only <=?
had hard-coded resolution rules.
And for a very long time all was right with the world.
Then, in base-4.16
(GHC 9.2) we suddenly got:
type x <= y = (x <=? y) ~ True
type (<=?) :: k -> k -> Bool
type m <=? n = OrdCond (Compare m n) 'True 'True 'False
type OrdCond :: Ordering -> k -> k -> k -> k
type family OrdCond o lt eq gt where
OrdCond 'LT lt eq gt = lt
OrdCond 'EQ lt eq gt = eq
OrdCond 'GT lt eq gt = gt
type Compare :: k -> k -> Ordering
type family Compare a b
type instance Compare (a :: Natural) b = CmpNat a b
type family CmpNat (m :: Natural) (n :: Natural) :: Ordering
Where only CmpNat
has hard-coded resolution rules.
This new implementation of <=
had error messages of much porer quality than previous implementations, which was reported in #20009 (closed).
For the following code:
{-# 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
we went from this error message in GHC 9.0:
$ 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.
to this error message in GHC 9.2:
$ 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>
The quality of the error message was fixed in !6066 (closed), which is currently included to be part of the GHC 9.4.1 release.
In !6066 (closed) the implementation of <=
was changed to:
type x <= y = Assert (x <=? y) (LeErrMsg x y)
type LeErrMsg x y = TypeError ('Text "Cannot satisfy: " ':<>: 'ShowType x ':<>: 'Text " <= " ':<>: 'ShowType y)
type Assert :: Bool -> Constraint -> Constraint
type family Assert check errMsg where
Assert 'True _ = ()
Assert _ errMsg = errMsg
which would create error messages of the following shape instead:
• Cannot satisfy: a <= a + 1
• In the expression: proxyInEq
In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
Remaining issue
The problem with the !6066 (closed) implementation is that the following code:
{-# LANGUAGE DataKinds, TypeFamilies #-}
module KnownNat2 where
import GHC.TypeLits
class KnownNat2 (name :: Symbol) (a :: Nat) (b :: Nat) where {}
instance (b <= a) => KnownNat2 "-" a b
that used to compile without errors, now gives the following error (this is with the GHC 9.4.1-rc1 release):
GHCi, version 9.4.0.20220721: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling KnownNat2 ( KnownNat2.hs, interpreted )
KnownNat2.hs:9:10: error:
* Variables `b, a' occur more often
in the constraint `b <= a'
than in the instance head `KnownNat2 "-" a b'
(Use UndecidableInstances to permit this)
* In the instance declaration for `KnownNat2 "-" a b'
|
9 | instance (KnownNat a, KnownNat b, b <= a) => KnownNat2 "-" a b
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.