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.

[RyanGlScott]

This is not quite as straightforward as it appears at a first glance. Consider this example:

type C :: k -> Constraint
class C a where
  m :: Proxy a

A naïve attempt at promoting C using the TypeAbstractions–based approach would be:

type PC :: k -> Constraint
class PC a where
  type M @a :: Proxy a

However, this is not quite right. This is because k is specified in the type of m:

λ> :type m
m :: forall k (a :: k). C a => Proxy a

But k is inferred in the kind of M!

λ> :kind M
M :: forall {k} (a :: k). Proxy a

The reason this happens is because GHC determines the visibilities of kind variables for associated type families independently of the parent class's standalone kind signature. That is, it only considers type M @a :: Proxy a in isolation, and since we didn't write out k explicitly in this declaration, GHC considers k to be inferred.

In order to make k specified in M's kind, we need to instead promote C to something that looks closer to this:

type PC :: k -> Constraint
class PC @k (a :: k) where
  type M @k @(a :: k) :: Proxy a

Note that we now have class PC @k (a :: k) instead of simply class PC a. This is a slight departure from what the user originally wrote (without any @ binders), but it is a necessary departure, as k would not be in scope over the definition of M otherwise. The tricky part will be figuring out how to automate the process of going from class PC a to class PC @k (a :: k) in general. I imagine that we will need to do something that resembles the following algorithm:

1. Decompose the parent class's standalone kind signature into DFunArgs.
2. Zip the DFunArgs with the class header's type variable binders, filling in any @ binders that are missing from the type variable binders with the appropriate entry in the DFunArgs.

This algorithm bears some similarities to GHC's matchUpSigWithDecl, which we already take inspiration from when singling data type declaration (see this code).