Figure out how to promote visible type application sensibly

[RyanGlScott]

There's currently this line in Data.Singletons.Promote:

https://github.com/goldfirere/singletons/blob/fb5e0051591f4e30109713e237bc2f0957406a3b/src/Data/Singletons/Promote.hs#L762-L765

Darn, if only we had visible kind applications! But hey, we're getting just that in GHC 8.8! Surely this means that we can rip out this antiquated code and treat visible type applications as a first-class citizen in singletons...

...but not so fast. It turns out that having visible kind applications isn't enough—we also need to figure out how to use it properly. Here's a function to help illustrate some of the challenges that VTA presents:

constBA :: forall b a. a -> b -> a
constBA x _ = x

constBA is exactly the same as the familiar const function, except I've deliberately swapped the conventional order that the type variables are quantified in. One interesting observation, right off the bat, is that when constBA is promoted to a type family:

type family ConstBA (x :: a) (y :: b) :: a where ...

The kind of ConstBA is now forall a b. a -> b -> a, not forall b a. a -> b -> a! What's worse, there is no reliable way of swapping the order that a and b are quantified in until we get top-level kind signatures. Blast.

But that's far from the only sticky thing about this situation. Let's suppose you want to use constBA, like in the following function:

blah :: forall b a. [a] -> [b -> a]
blah x = map (constBA @b) x

How should this promote? This is what currently happens in today's singletons, which simply drops VTAs:

type family Blah (x :: [a]) :: [b ~> a] where
  Blah x = Apply (Apply MapSym0 ConstBASym0) x

Notice that singletons always uses defunctionalization symbols when promoting function application, so if we want to promote constBA @b, this suggests that the output should be something like ConstBASym0 @b. But that presents its own set of challenges, because this is the code that gets generated for ConstBASym0:

data ConstBASym0 :: forall a b. a ~> b ~> a

This happens because during defunctionalization, we take the type a ~> b ~> a and quantify over it by simply gathering the free variables in left-to-right order. Unfortunately, this means that we get forall a b. <...> instead of forall b a. <...>. Double blast.

One could envision tweaking defunctionalization to remember the original order of type variables so that we generate data ConstBASym0 :: forall b a. a ~> b ~> a instead. That would fix blah, but we're not out of the clear yet. There's one more defunctionalization symbol to consider: ConstBASym1, which arises from this generated code:

data ConstSym1 (x :: a) :: forall b. b ~> a

This is even gnarlier than ConstSym0. The kind of ConstSym1 is forall a. a -> forall b. b ~> a, and this time, it's not simple to rearrange the foralls so that b is quantified before a due to the syntax used. One way forward is to declare ConstSym1 like so:

data ConstSym1 :: forall b a. a -> (b ~> a)

This works, although this trick currently won't work for anything that involves visible dependent quantification. (We could carve out a special case when defunctionalizing things without visible dependent quantification, although that would be a bit messy.)

By sheer accident, constBA is singled correctly... at least, some of the time. That is to say, this is generated for sConstBA:

sConstBA :: forall b_1 a_2 (x :: a_2) (y :: b_1). Sing x -> Sing y -> Sing (Apply (Apply ConstBASym0 x) y :: a_2)

This works only because b_1's unique happens to come before a_2's unique, so b_1 comes before a_2 when they're both put into a Set. (If compiled with -dunique-increment=-1, however, then you'd get the opposite order!)

That's not to say that singling VTAs is already a solved problem. Consider what happens when you single blah today:

sBlah :: forall b a (x :: [a]). Sing x -> Sing (Apply BlahSym0 x :: [b ~> a])
sBlah (sX :: Sing x) = (applySing ((applySing ((singFun2 @MapSym0) sMap)) ((singFun2 @ConstBASym0) sConstBA))) sX

Once again, we single function application by leveraging defunctionalization symbols. Therefore, in order to single blah correctly, we'd need to change singFun2 @ConstBASym0 to singFun2 @(ConstBASym0 @b), and moreover, we'd need to ensure that ConstBASym0 :: forall b a. a ~> b ~> a.

[goldfirere]

Even worse: we really should include the visible dependent stuff in the defunctionalization symbols, making something like forall b ~> forall a ~> a ~> b ~> a. Actually, maybe that point is moot, because (->) is to (~>) as forall is to foreach, and kind-level forall already means foreach.

But it looks like this is a no-go at least until with have top-level signatures. I wouldn't even try this before we have that.

[RyanGlScott]

One thing that may not be evident from the wall of text in https://github.com/goldfirere/singletons/issues/378#issue-399023570 is that fixing this issue can be divided into three relatively self-contained chunks:

1. Change singling to produce type signatures with correct type variable orders.
2. Change promotion to produce standalone kind signatures with correct type variable orders.
3. Make promotion/singling preserve visible type applications.

Chunk (2) depends on having standalone kind signatures, and chunk (3) depends on chunk (2). Chunk (1), on the other hand, is quite feasible to implement today. PR #408 knocks out chunk (1).

[RyanGlScott]

PR #432 knocked out chunk (2). Unfortunately, I don't think we're ready to tackle chunk (3) yet for various reasons:

1. Even after #432, there are still three two situations where singletons won't preserve the order of kind variables during promotion:

   • let- or where-bound functions won't be given SAKS. To give a particular example:

     f :: Bool
     f = let x = True
          g :: () -> Bool
          g _ = x
      in g ()

     The TH machinery will give the promoted F type family a SAK, but not the G type family. See Note [No SAKs for let-decs with local variables] in D.S.Promote for an explanation.

   • Promoted class methods cannot be given SAKS. For example, this class:

     class C (b :: Type) where
     m :: forall a. a -> b -> a

     Is promoted like so:

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

     The order of the variables a and b are different between the type of m and the kind of M. See Note [Promoted class methods and kind variable ordering] in D.S.Promote.

   • EDIT: This is no longer the case after #446.

     Fully saturated defunctionalization symbols won't be given SAKS. For example, if you defunctionalize the Id type family, you'll generate two defunctionalization symbols:

     type IdSym0 :: forall a. a ~> a
     data IdSym0 f where ...
     
     type IdSym1 (x :: a) = Id x :: a

     Notice that unlike IdSym0, IdSym1 (the "fully saturated" defunctionalization symbol) does not have a SAK. This is because in general, giving fully saturated defunctionalization symbols SAKS can lead to kind errors. See Note [No SAKs for fully saturated defunctionalization symbols] in D.S.Promote.Defun for the sordid story.

2. EDIT: This is much less of an issue after https://github.com/goldfirere/singletons/pull/573.

   Even if we did generate exactly the right order of kind variables for all promoted declarations, there is an even larger issue: functions that make use of scoped type variables do not reliably promote. See #433. This is rather annoying since scoped type variables and TypeApplications are often used in tandem, such as in the following example (which is affected by #433):

   $(singletons [d|
    f :: forall a. a -> a
    f x = id @a x
    |])

These issues essentially boil down to limitations in the way type families work in GHC, and as a result, they are difficult to work around on singletons end. As a result, I am inclined to park this issue pending further developments on GHC's side. That is not to say that the work spent fixing chunks (1) and (2) was wasted. We can now use TypeApplications in manually written singletons code much more reliably than before, which is a huge win. I'm personally benefitting from this work, at the very least, and I imagine others will too.

[RyanGlScott]

See also #583, which describes the challenges in promoting invisible type patterns. Really, the challenges are the same as what is described above: because singletons-th cannot reliably guarantee the order of type variables in all situations, it is difficult to guarantee that promoting invisible type patterns will work in the general case.