Use `TypeAbstractions` to quantify kind variables in the correct order for promoted class method type signatures (at least, some of the time)

[RyanGlScott]

As explained in Note [Promoted class methods and kind variable ordering], singletons-th makes no effort to ensure that the kind of a promoted class method quantifies its kind variables in the same order as the type variables in the original class method's type signature. A minimal example of this limitation is this:

type C :: Type -> Constraint
class C b where
  m :: forall a. a -> b -> a

-- C promotes to this...

type PC :: Type -> Constraint
class PC b where
  type M (x :: a) (y :: b) :: a

Note that we have the following type variable orderings:

m :: forall b a. a -> b -> a -- Ignoring the `C b` constraint
M :: forall a b. a -> b -> a

This is rather unfortunate. However, we can do better thanks to the TypeAbstractions extension. Using TypeAbstractions, we can promote m like so:

type PC :: Type -> Constraint
class PC b where
  type M @b @a (x :: a) (y :: b) :: a

And now we have M :: forall b a. a -> b -> a, just as desired!

Unfortunately, this trick isn't always viable. In particular, you can only use TypeAbstractions in an associated type family when the parent class has a standalone kind signature. This means that if the user left off the type C :: Type -> Constraint part in the original example, then GHC would reject the use of TypeAbstractions in the generated definition of PC:

$ ghc-9.10 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
Bug.hs:10:3: error: [GHC-92337]
    • Invalid invisible type variable binder: @a
      Either a standalone kind signature (SAKS)
      or a complete user-supplied kind (CUSK, legacy feature)
      is required to use invisible binders.
    • In the associated type family declaration for ‘M’
    Suggested fix: Add a standalone kind signature for ‘M’
   |
10 |   type M @b @a (x :: a) (y :: b) :: a
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Bug.hs:10:3: error: [GHC-92337]
    • Invalid invisible type variable binder: @b
      Either a standalone kind signature (SAKS)
      or a complete user-supplied kind (CUSK, legacy feature)
      is required to use invisible binders.
    • In the associated type family declaration for ‘M’
    Suggested fix: Add a standalone kind signature for ‘M’
   |
10 |   type M @b @a (x :: a) (y :: b) :: a
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Bummer. But we need not let perfect be the enemy of good. I propose that we use TypeAbstractions whenever it is possible to do so.