Draft: Type-level comparison expands to equality

Addresses #21935

While working on updating existing code to GHC 9.4.1-rc1: https://github.com/clash-lang/ghc-typelits-knownnat/pull/41 I noticed that one of my class instances which had <= in the instance constraints suddenly required -XUndecidableInstances.

Specifically this code:

-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.-'
instance (KnownNat a, KnownNat b, (b <= a)) => KnownNat2 $(nameToSymbol ''(-)) a b where
  natSing2 = SNatKn (natVal (Proxy @a) - natVal (Proxy @b))
  {-# INLINE natSing2 #-}

instance (KnownNat x, KnownNat y, (1 <= y)) => KnownNat2 $(nameToSymbol ''Div) x y where
  natSing2 = SNatKn (quot (natVal (Proxy @x)) (natVal (Proxy @y)))

instance (KnownNat x, KnownNat y, (1 <= y)) => KnownNat2 $(nameToSymbol ''Mod) x y where
  natSing2 = SNatKn (rem (natVal (Proxy @x)) (natVal (Proxy @y)))

gave the following errors:

src-ghc-9.4\GHC\TypeLits\KnownNat.hs:194:10: error:
    * Variables `b, a' occur more often
        in the constraint `b <= a'
        than in the instance head `KnownNat2 "GHC.TypeNats.-" a b'
      (Use UndecidableInstances to permit this)
    * In the instance declaration for
        `KnownNat2 ("GHC.TypeNats.-") a b'
    |
194 | instance (KnownNat a, KnownNat b, (b <= a) ) => KnownNat2 $(nameToSymbol ''(-)) a b where
    |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src-ghc-9.4\GHC\TypeLits\KnownNat.hs:198:10: error:
    * Variable `y' occurs more often
        in the constraint `1 <= y'
        than in the instance head `KnownNat2 "GHC.TypeNats.Div" x y'
      (Use UndecidableInstances to permit this)
    * In the instance declaration for
        `KnownNat2 ("GHC.TypeNats.Div") x y'
    |
198 | instance (KnownNat x, KnownNat y, (1 <= y)) => KnownNat2 $(nameToSymbol ''Div) x y where
    |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src-ghc-9.4\GHC\TypeLits\KnownNat.hs:201:10: error:
    * Variable `y' occurs more often
        in the constraint `1 <= y'
        than in the instance head `KnownNat2 "GHC.TypeNats.Mod" x y'
      (Use UndecidableInstances to permit this)
    * In the instance declaration for
        `KnownNat2 ("GHC.TypeNats.Mod") x y'
    |
201 | instance (KnownNat x, KnownNat y, (1 <= y)) => KnownNat2 $(nameToSymbol ''Mod) x y where
    |     

Currently I'm working around it by rewriting my instances to:

instance (KnownNat a, KnownNat b, (b <= a) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''(-)) a b where
  natSing2 = SNatKn (natVal (Proxy @a) - natVal (Proxy @b))
  {-# INLINE natSing2 #-}

instance (KnownNat x, KnownNat y, (1 <= y) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''Div) x y where
  natSing2 = SNatKn (quot (natVal (Proxy @x)) (natVal (Proxy @y)))

instance (KnownNat x, KnownNat y, (1 <= y) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''Mod) x y where
  natSing2 = SNatKn (rem (natVal (Proxy @x)) (natVal (Proxy @y)))

But it would be much nicer if I didn't have to, and the type synonyms for the comparison operators already expanded to an equality constrait.

I would be nice if this could still make it into GHC 9.4.1

• are either individually buildable or squashed
• have commit messages which describe what they do (referring to [Notes][notes] and tickets using #NNNN syntax when appropriate)
• have added source comments describing your change. For larger changes you likely should add a [Note][notes] and cross-reference it from the relevant places.
• add a testcase to the testsuite.