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]:

• singletons/singletons-th/src/Data/Singletons/TH/Single/Type.hs

  Lines 249 to 253 in 2c91ce4

  	At present, Template Haskell does not have a way to distinguish among the
  	specificities bound by a data type header. Without this knowledge, it is
  	unclear how one could work around this issue. Thankfully, this issue is
  	only likely to surface in very limited circumstances, so the damage is somewhat
  	minimal.

• singletons/singletons-th/src/Data/Singletons/TH/Single/Type.hs

  Lines 320 to 328 in 2c91ce4

  	This will not kind-check because MkProxy only accepts /one/ visible kind argument,
  	whereas this supplies it with two. To avoid this issue, we instead use the type
  	`forall k (a :: k). SProxy (MkProxy :: Proxy a)`. Granted, this type is /still/
  	technically wrong due to the fact that it explicitly quantifies `k`, but at the
  	very least it typechecks. If Template Haskell gained the ability to distinguish
  	among the specificities of type variables bound by a data type header
  	(perhaps by way of a language feature akin to
  	https://github.com/ghc-proposals/ghc-proposals/pull/326), then we could revisit
  	this design choice.

(Historical note: ghc-proposals/ghc-proposals#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 goldfirere/th-desugar#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]

goldfirere/th-desugar#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.