Support promoting/singling invisible type patterns

[RyanGlScott]

GHC 9.10 introduces the ability to use invisible type patterns. As such, examples like this can now be written:

id :: a -> a
id @t x = x :: t

The question is: can we promote and single these definitions? It seems plausible, given that we can write the following:

type Id :: a -> a
type family Id x where
  Id @t x = x :: t

sId :: (forall (x :: a). Sing x -> Sing (Id x) :: Type)
sId @t (sX :: Sing x) = sX :: Sing (x :: t)

We should see if this is doable. See also #565.

[RyanGlScott]

One wrinkle that I foresee is class method defaults. Consider this example:

class C a where
  m :: forall b. a -> b -> a
  m x _ = x

Currently, we promote this to:

class PC a where
  type M (x :: a) (y :: b) :: a
  type M x y = MDefault x y

type MDefault :: a -> b -> a
type family MDefault x y where
  MDefault x _ = x

So far, so good. Now consider this variation:

class C a where
  m :: forall b. a -> b -> a
  m @b x (_ :: b) = x

A naïve approach would lead to this promoted definition:

class PC a where
  type M (x :: a) (y :: b) :: a
  type M x y = MDefault x y

type MDefault :: a -> b -> a
type family MDefault x y where
  MDefault @b x (_ :: b) = x

But this is wrong: we really want to generate this instead:

type MDefault :: a -> b -> a
type family MDefault x y where
  MDefault @_ @b x (_ :: b) = x

In general, we'd need to insert a number of @_s equal to the number of type variables bound in the class header.

Actually, that's an oversimplification. Inspired by Note [Promoted class methods and kind variable ordering], we can make yet another variation of the example above:

class C b where
  m :: forall a. a -> b -> a
  m x _ = x

Note that b will be quantified before a in the type of m. In the promoted version of m, however, the type variables are quantified in the opposite order:

class PC b where
  type M (x :: a) (y :: b) :: a
  type M x y = MDefault x y

type MDefault :: a -> b -> a
type family MDefault x y where
  MDefault x (_ :: b) = x

This makes it less clear what to do when TypeAbstractions are involved:

class C b where
  m :: forall a. a -> b -> a
  m @a (x :: a) _ = x

Two possible options for promoting this to MDefault are:

1. type MDefault :: a -> b -> a
   type family MDefault x y where
    MDefault @a x (_ :: b) = x

2. type MDefault :: forall b a. a -> b -> a
   type family MDefault x y where
    MDefault @_ @a x (_ :: b) = x

Option (1) might appear simpler at a first glance, but generating that code would require us to ignore our earlier rule about inserting @_s. In fact, the more I think about it, I actually think that option (1) would be harder, since it would require swizzling around the invisible type variable arguments to match whatever order singletons-th happens to pick for MDefault's standalone kind signature.

Option (2), on the other hand, would be more consistent with the example above, since we'd continue to apply the insert-@_s rule. Note that the standalone kind signature that singletons-th generates for MDefault (as well as other "default" type families) doesn't yet have an explicit forall, but we could make it have one.

[RyanGlScott]

591 takes one step towards option (2), as it ensures that type families like MDefault are given explicit foralls. The catch is that the order of the foralls isn't guaranteed to be in the expected order, but after #596 lands, we can guarantee that the order will be preserved for class methods whose parent class has a standalone kind signature. As such, we should land #591 and #596 first before making further progress on this.

[RyanGlScott]

After discovering a regression, I've reverted #596 (in #606). As such, we cannot guarantee the order of kind variables for promoted class methods after all. This means that if we wanted to support invisible type patterns in class method defaults, then we would have no choice but to go with option (1). This means that we would need to swizzle around the invisible type patterns to match whatever type variable order singletons-th happens to pick in the promoted kind.

Is this doable? Perhaps. But it would be somewhat tedious to do so, and I'm not exactly excited about implementing it. As such, I'm inclined to decide that singletons-th doesn't support invisible type patterns in class method defaults at all. If someone asks for this feature later, we could revisit this.

[RyanGlScott]

We also can't reliably guarantee the order of type variables for let- or where-bound functions, as they aren't given standalone kind signatures (see https://github.com/goldfirere/singletons/issues/378#issuecomment-584096320). As such, it would also be challenging to support the use of invisible type patterns in let- or where-bound functions.

Thinking about this more, this issue is really just a new twist on the old problem of not being able to guarantee the order of type variables, first described in #378. The last update on #378 was that we opted not to promote visible type applications because singletons-th cannot guarantee the order of type variables in enough places for it to work reliably. (I continue to be on the fence about this position, but that's where things left off.) For the sake of consistency, we should apply the same position to invisible type patterns as well.