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.