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.