Regression: HEAD fails to typecheck uses of (GHC.TypeNats.<=) that 9.0.1 could

Originally observed on a head.hackage build here.

The constraints library fails to compile with HEAD. Here is a minimized example of what goes wrong:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind
import Data.Type.Bool
import GHC.TypeNats

data Dict :: Constraint -> Type where
  Dict :: c => Dict c

type family Min (m::Nat) (n::Nat) :: Nat where
    Min m n = If (n <=? m) n m
type family Max (m::Nat) (n::Nat) :: Nat where
    Max m n = If (n <=? m) m n

eqLe :: (a ~ b) => Dict (a <= b)
eqLe = Dict

minZero :: Dict (Min n 0 ~ 0)
minZero = Dict

maxZero :: Dict (Max n 0 ~ n)
maxZero = Dict

zeroLe :: Dict (0 <= a)
zeroLe = Dict

leId :: Dict (a <= a)
leId = Dict

This compiles with GHC 9.0.1, but with HEAD it errors thusly:

$ ~/Software/ghc-9.1.20210303/bin/ghc Bug.hs              
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:22:9: error:
    • Couldn't match type: Data.Type.Ord.OrdCond
                             (Data.Type.Ord.Compare b0 b0) 'True 'True 'False
                     with: Data.Type.Ord.OrdCond
                             (Data.Type.Ord.Compare b b) 'True 'True 'False
      Expected: Dict (a <= b)
        Actual: Dict (b0 <= b0)
      NB: ‘Data.Type.Ord.OrdCond’ is a non-injective type family
      The type variable ‘b0’ is ambiguous
    • In the ambiguity check for ‘eqLe’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature: eqLe :: (a ~ b) => Dict (a <= b)
   |
22 | eqLe :: (a ~ b) => Dict (a <= b)
   |         ^^^^^^^^^^^^^^^^^^^^^^^^

Bug.hs:25:12: error:
    • Couldn't match type: If
                             (Data.Type.Ord.OrdCond (CmpNat 0 n0) 'True 'True 'False) 0 n0
                     with: If
                             (Data.Type.Ord.OrdCond (CmpNat 0 n) 'True 'True 'False) 0 n
      Expected: Dict (Min n 0 ~ 0)
        Actual: Dict (Min n0 0 ~ 0)
      NB: ‘If’ is a non-injective type family
      The type variable ‘n0’ is ambiguous
    • In the ambiguity check for ‘minZero’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature: minZero :: Dict (Min n 0 ~ 0)
   |
25 | minZero :: Dict (Min n 0 ~ 0)
   |            ^^^^^^^^^^^^^^^^^^

Bug.hs:31:11: error:
    • Couldn't match type: Data.Type.Ord.OrdCond
                             (CmpNat 0 a0) 'True 'True 'False
                     with: Data.Type.Ord.OrdCond (CmpNat 0 a) 'True 'True 'False
      Expected: Dict (0 <= a)
        Actual: Dict (0 <= a0)
      NB: ‘Data.Type.Ord.OrdCond’ is a non-injective type family
      The type variable ‘a0’ is ambiguous
    • In the ambiguity check for ‘zeroLe’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature: zeroLe :: Dict (0 <= a)
   |
31 | zeroLe :: Dict (0 <= a)
   |           ^^^^^^^^^^^^^

Bug.hs:34:9: error:
    • Couldn't match type: Data.Type.Ord.OrdCond
                             (Data.Type.Ord.Compare a0 a0) 'True 'True 'False
                     with: Data.Type.Ord.OrdCond
                             (Data.Type.Ord.Compare a a) 'True 'True 'False
      Expected: Dict (a <= a)
        Actual: Dict (a0 <= a0)
      NB: ‘Data.Type.Ord.OrdCond’ is a non-injective type family
      The type variable ‘a0’ is ambiguous
    • In the ambiguity check for ‘leId’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature: leId :: Dict (a <= a)
   |
34 | leId :: Dict (a <= a)
   |         ^^^^^^^^^^^^^

It looks like commit eea96042 (Add cmpNat, cmpSymbol, and cmpChar) is the culprit. It's unclear to me if this is expected behavior, however. Since the commit lacks a changelog entry, I'm unclear if this was anticipated or not.