Use `TypeAbstractions` in singled data type definitions

[RyanGlScott]

GHC recently landed !9480, an implementation of GHC proposal #425. This introduces invisible @k-binders for type-level declarations, guarded behind the TypeAbstractions extension. For example:

data D @k @j (a :: k) (b :: j) = ...
       ^^ ^^

With this, we can finally address singletons-th limitations that are described in Note [Preserve the order of type variables during singling]:

• https://github.com/goldfirere/singletons/blob/2c91ce4ad7e80518f08ea7cf962c48820e83b309/singletons-th/src/Data/Singletons/TH/Single/Type.hs#L249-L253
• https://github.com/goldfirere/singletons/blob/2c91ce4ad7e80518f08ea7cf962c48820e83b309/singletons-th/src/Data/Singletons/TH/Single/Type.hs#L320-L328

(Historical note: https://github.com/ghc-proposals/ghc-proposals/pull/326 was an earlier iteration of what eventually became GHC proposal #425.)

It's possible that there are other use cases for TypeAbstractions within singletons, but this is the one that first comes to mind.

[RyanGlScott]

Looking at this a bit more, I think that we would first need to resolve https://github.com/goldfirere/th-desugar/issues/199 before we could address this issue. This sounds doable, but I think it would take some time to get right. Moreover, I'd like to release a new version of singletons soon that is compatible with GHC 9.8, and I don't want to hold up the release on this issue. For that reason, I'll defer this to later.

[RyanGlScott]

See also #583.

[RyanGlScott]

https://github.com/goldfirere/th-desugar/issues/199 has been fixed, which means that we can revisit this. At minimum, wrinkle 2 in Note [Preserve the order of type variables during singling] is completely moot, so we can remove that entirely. I'm still not sure about wrinkle 3, however. When I first wrote that, I imagined that if we had a data constructor C :: forall a. D a, then instead of singling it to this:

SC :: forall a. SD (C :: D a)

We could instead single it to this:

SC :: forall a. SD (C @a)

But what if the user had written C :: forall {a}. D a instead? Then it wouldn't be possible to write C @a because a isn't eligible for visible type application. The only way to resolve the ambiguity would be to single C to SC :: forall a. SD (C :: D a), which is exactly what we do today.

One might wonder if there are any situations where visible kind applications would be necessary in situations where explicit return kinds don't suffice. For example, what if the user had declared this data type?

data D where
  C :: forall a. D

Then it wouldn't suffice to write SD (C :: D), since the a kind variable would be ambiguous. On the other hand, it you tried promoting and singling C, then you'd encounter many more problems besides the definition of SC itself. For example, singletons-th would generate the following defunctionalization symbol for C:

type CSym0 :: forall a. D
type family CSym0 @a :: D where
  CSym0 = C

But GHC will reject this:

error: [GHC-16220]
    • Uninferrable type variables k0, (a0 :: k0) in
      the type family equation right-hand side: C @{k0} @a0
    • In the type family declaration for ‘CSym0’

I imagine that there would be various other issues of this sort in the code that singletons-th generates. It's conceivable that we could fix these issues, but it potentially require a lot of work for relatively little gain (definitions like C are rather rare in practice).

As such, I'm inclined to leave wrinkle 3 of the Note in place, but with some expanded commentary on why we use explicit return kinds instead of visible kind applications.