Undocumented 9.4 TypeNats breaking change

Summary

Location of documentation issue: the GHC user's guide / base's changelog

In GHC 9.4, more specifically !6066 (closed), the implementation of (at least) Data.Type.Ord.(<=) changed so the following code no longer compiles

import GHC.TypeNats

newtype A (l :: Nat) (u :: Nat) = Finite ()
class E1 (x :: *) where

instance x <= y => E1 (A x y) where

The error is

Bug.hs:13:10: error:
    • Variables ‘x, y’ occur more often
        in the constraint ‘x <= y’ than in the instance head ‘E1 (A x y)’
      (Use UndecidableInstances to permit this)
    • In the instance declaration for ‘E1 (A x y)’
   |
13 | instance x <= y => E1 (A x y) where

Whilst the suggestion to add UndecidableInstances works,

• This breakage is undocumented afaict
• The error is really confusing, since it is not obvious that <= actually expands into a more complex type synonym

Proposed improvements or changes

We should document this somewhere. I suggest the user's guide, since that is where I went looking for information about the breakage. However, I don't know if this is reasonable, given that 9.6 has now come out.

Background

The need for documentation was briefly mentioned in #21935 (comment 446169), but appears to have slipped through the cracks.

For reference, GHC 9.2 had

type x <= y = (x <=? y) ~ 'True

whereas GHC 9.4 had:

type x <= y = Assert (x <=? y) (LeErrMsg x y)