Consider allowing promotion and singling of all rank-1 types

[RyanGlScott]

Currently, singletons-th adopts a hard-line stance regarding quantifiers in type signatures. Namely, they must all appear at the top level in this order:

forall tvb_1 ... tvb_m. ctx => arg_1 -> ... arg_n -> res

With the additional stipulations that:

• Only invisible foralls are permitted. A type like forall a -> a (with a visible forall) is not allowed.
• Nested foralls and contexts are not permitted in ctx, the args, the res, or the kinds of the tvbs.

In singletons parlance, this sort of type is referred to as a vanilla type. Vanilla types are a subset of rank-1 types, where quantifiers are allowed to appear contravariantly at a depth of at most 1.¹ singletons-th does not support all rank-1 types, as it will currently reject this one:

const2 :: forall a. a -> forall b. b -> a

In #401, I originally came to the conclusion that we should not support anything more sophisticated than vanilla types. Recently, however, I'm reconsidering that stance. One thing that is making me reconsider my stance is the advent of visible foralls in types, where you can write things like this:

-- Definition:
idv :: forall a -> a -> a
idv (type a) x = x :: a

-- Usage:
n :: Bool
n = idv (type Bool) True

This is an exciting step towards full dependent types. Moreover, it would be interesting to support this feature in singletons. On the surface, it appears simple to support. Here is roughly how the example above would look when promoted:

-- Definition:
type Idv :: forall a -> a -> a
type family Idv a x where
  Idv a x = x :: a

-- Usage:
type N :: Bool
type family N where
  N = Idv Bool True

And singled:

-- Definition:
sIdv :: forall a -> forall (x :: a). Sing x -> Sing (Idv a x)
sIdv (type a) (sX :: Sing x) = sX :: Sing (x :: a)

-- Usage:
sN :: Sing N
sN = sIdv (type Bool) STrue

Note that when promoted (type a) simply becomes a, and (type a) isn't changed at all when singled. The most interesting difference when singled is the need to have a separate, invisible forall (x :: a). after the visible forall a ->. (More on this in a bit.)

As cool as this idea is, it is not possible within singletons-th's current restriction that all types must be vanilla. What if we relaxed this restriction to allow all rank-1 types, however? Although I decided against this in #401, all of the problematic examples that I came up with are actually rank-2 types, not rank-1. As it turns out, each of the issues that I identified in #401 are manageable when the scope is limited to rank-1 types:

Defunctionalization symbols

You definitely can't make defunctionalization symbols for rank-2 or higher of types, as you would need to define Apply instances with polytypes as arguments. This just isn't possible in GHC, even with the advent of Quick Look impredicativity.

With rank-1 types, we can avoid this problem by applying the workaround described in Wrinkle 2: Non-vanilla kinds in Note [Defunctionalization game plan]. The trick is that we can still generate defunctionalization symbols for things with non-vanilla types, but we may have to make some sacrifices:

• For types with nested foralls, the defunctionalization symbols would put all of the foralls up front to avoid the impredicativity issues described above.
• For types with visible foralls, the defunctionalization symbols would turn something like forall a -> a into forall a. Type ~> a.

For many use cases, these sacrifices are acceptable, as you can still profitably use the defunctionalization symbols even with the slightly different treatment of foralls.

In singled definitions

Singling rank-2 or higher definitions would be tricky, as the examples in #401 demonstrate. Singling rank-1 definitions, on the other hand, would be much more tractable. In today's singletons-th, the algorithm works roughly like so: given a (vanilla) type signature of the form:

f :: forall tvb_1 ... tvb_m. arg_1 -> ... arg_n -> res

The singled type signature would become (roughly):

sF :: forall tvb_1 ... tvb_m
            (s_1 :: arg_1) ... (s_n :: arg_n).
      Sing s_1 -> ... -> Sing s_n -> Sing (F s_1 ... s_n :: res)

Where F and sF are the promoted and singled versions of f, respectively. Note that we introduce additional s type variables to instantiate Sing with. For lack of a better name, I'll call these "Sing type variables".

To handle all rank-1 types, this algorithm would need to be generalized slightly to be able to handle nested foralls and visible foralls. Here are two possible algorithms for making this work. (Feel free to skip reading the algorithm descriptions if you don't care about the ugly details.)

Algorithm 1: The nearest telescope algorithm

1. Quantify each Sing type variable in an invisible forall telescope directly after the nearest forall telescope (starting from the ::) in which all of the variables in the Sing type variable's kind have been bound by preceding telescopes.
2. If a Sing type variable telescope appears directly after another invisible forall telescope, combine the two telescopes into one.

Here are some examples of how this would work:

A vanilla type signature

const :: forall a b. a -> b -> a

We need to quantify two Sing type variables, one for each of the arguments preceding a function arrow. The kinds of these Sing type variables are a and b, and the nearest forall telescope that we could pick after which a and b would be bound is forall a b.. As a result, we will quantify the Sing type variables directly after this telescope:

sConst :: forall a b.
          forall (s1 :: a) (s2 :: b).
          Sing s1 -> Sing s2 -> Sing (Const2 s1 s2 :: a)

Then, we would combine the Sing type variable telescope into the preceding one, which also uses invisible foralls:

sConst :: forall a b (s1 :: a) (s2 :: b).
          Sing s1 -> Sing s2 -> Sing (Const2 s1 s2 :: a)

This is exactly the same type signature that sConst would receive in today's singletons-th.

An example with nested, invisible foralls

slurmp :: forall a.
          a ->
          forall b.
          b -> a -> (a, b) -> a

This time, we need to quantify four Sing type variables. The first and third Sing type variables have kind a, and the nearest forall telescope that we could pick after which a would be bound is forall a.. The kind of the second Sing type variable is b, and the kind of the fourth Sing type variable is (a, b). Because both of these kinds mention b, the nearest forall telescope that we could pick after which b would be bound is forall b. These constraints give rise to the following type signature:

sSlurmp :: forall a.
           forall (s1 :: a) (s3 :: a).
           Sing s1 ->
           forall b.
           forall (s2 :: b) (s4 :: (a, b)).
           Sing s2 -> Sing s3 -> Sing s4 -> Sing (Slurmp s1 s2 s3 s4 :: a)

Finally, we combine adjacent invisible forall telescopes to get:

sSlurmp :: forall a (s1 :: a) (s3 :: a).
           Sing s1 ->
           forall b (s2 :: b) (s4 :: (a, b)).
           Sing s2 -> Sing s3 -> Sing s4 -> Sing (Slurmp s1 s2 s3 s4 :: a)

An example with a visible forall

slurmpVis :: forall a.
             a ->
             forall b ->
             b -> a -> (a, b) -> a

The type of slurmpVis is identical to slurmp except that the b is quantified visibly. As a result, the forall b -> and forall (s2 :: b) (s4 :: (a, b)). telescopes would not be combined, resulting in a final singled type signature of:

sSlurmpVis :: forall a (s1 :: a) (s3 :: a).
              Sing s1 ->
              forall b ->
              forall (s2 :: b) (s4 :: (a, b)).
              Sing s2 -> Sing s3 -> Sing s4 -> Sing (SlurmpVis s1 b s2 s3 s4 :: a)

Algorithm 2: The nearest function argument algorithm

Algorithm 1 (the nearest telescope algorithm) is designed to maintain backwards compatibility with singletons-th's existing treatment of foralls in singled type signatures. However, it is not obvious that Algorithm 1 produces the nicest type signatures for things with nested foralls. For instance, in the type of sSlurmp above, we quantified s3 before s2, which feels somewhat awkward.

Algorithm 2 (The nearest function argument algorithm) is an attempt to address this awkwardness. It only has one rule:

1. Quantify each Sing type variable s_i directly before the function argument Sing s_i.

That's it. There's no mention of telescopes in this algorithm, which makes it conceptually simpler. On the other hand, it does not preserve the existing behavior of how singletons-th quantifies type variables.

Here are the same examples from above, but using Algorithm 2:

A vanilla type signature

const :: forall a b. a -> b -> a

would be singled to:

sConst :: forall a b.
          forall (s1 :: a). Sing s1 ->
          forall (s2 :: b). Sing s2 ->
          Sing (Const s1 s2 :: a)

An example with nested, invisible foralls

slurmp :: forall a.
          a ->
          forall b.
          b -> a -> (a, b) -> a

would be singled to:

sSlurmp :: forall a.
           forall (s1 :: a). Sing s1 ->
           forall b.
           forall (s2 :: b). Sing s2 ->
           forall (s3 :: a). Sing s3 ->
           forall (s4 :: (a, b)). Sing s4 ->
           Sing (Slurmp s1 s2 s3 s4 :: a)

An example with a visible forall

slurmpVis :: forall a.
             a ->
             forall b ->
             b -> a -> (a, b) -> a

would be singled to:

sSlurmpVis :: forall a.
              forall (s1 :: a). Sing s1 ->
              forall b ->
              forall (s2 :: b). Sing s2 ->
              forall (s3 :: a). Sing s3 ->
              forall (s4 :: (a, b)). Sing s4 ->
              Sing (SlurmpVis s1 b s2 s3 s4 :: a)

Either algorithm should suffice, but we will have to think carefully about the tradeoffs involved.

---

tl;dr It is quite possible to promote and single all rank-1 type signatures, even those with visible foralls. The downside is that we may have to sacrifice the fidelity of the defunctionalization symbols involved a little. I think this is an acceptable price to pay, but others may feel differently. What are your thoughts?

¹For a more formal definition of what a rank-1 type is, see Section 3.1 of Practical type inference for arbitrary-rank types.

[goldfirere]

I'd like to hear more about your thoughts on promotion and defunctionalization symbols. It doesn't surprise me that singling is possible. But I worry about promotion. In particular, what's our current stance on promoting/singling code with type applications? If we support that, then we're pretty constrained in how to proceed. But if we don't support that today, then we have more freedom.

Of the two singling approaches you propose, I prefer the second. This would be incompatible with current usage if someone uses visible type application to (redundantly) choose singleton arguments. But singletons hasn't, I think, stressed backward compatibility, so I'm not terribly bothered by this.

Regardless of the approach, there is a non-trivial amount of work here. (It's not all that much, but more than an hour!) Is there good motivation for doing this? (Just seeing how far singletons can go is somewhat decent motivation -- especially if it's what actually motivates you!)

[RyanGlScott]

what's our current stance on promoting/singling code with type applications?

Our current stance is that singletons doesn't support type applications, and it will promote code like f @a x to F x. See this section of the README. As a result, we have the freedom to cut corners.

As that section of the README explains, we do try our best to preserve the order of foralls in type signatures whenever possible, but there are certain Haskell constructs for which this is not really possible. Defunctionalization symbols are a notable example of this: there is no sensible way to take const2 :: forall a. a -> forall b. b -> a and give it a defunctionalization symbol Const2Sym0 :: forall a. a ~> (forall b. b ~> a) for the reasons described in #401. This limitation seems pretty fundamental, and I can't think of a way to preserve the order of the foralls in the defunctionalization symbol (short of replacing defunctionalization with some other mechanism entirely).

Of the two singling approaches you propose, I prefer the second. This would be incompatible with current usage if someone uses visible type application to (redundantly) choose singleton arguments. But singletons hasn't, I think, stressed backward compatibility, so I'm not terribly bothered by this.

Indeed, I also prefer the second approach for the same reasons that you list.

Is there good motivation for doing this?

"Good" is subjective, but I am very keen to add support for visible dependent quantification in terms to singletons, for which this issue is a prerequisite. VDQ in terms is a stepping stone for full dependent types, and being able to promote/single types with forall a -> quantifiers would avoid the need for ugly kludges involving Proxy or TypeRep. (See this related issue.)

Additionally, I am definitely curious to see how far singletons can go in this particular direction. The decision to only permit prenex types in #401 has always struck me as a bit too conservative, and I wonder how many of our current assumptions can be relaxed.

[goldfirere]

All sounds good to me. Fire when ready.

[RyanGlScott]

I've been working on this issue for a while, and in the process of doing so, I've gained a better understanding of the code that governs how type variable binders are singled. This new insight has led to a number of simplifications to the code (see #545, #547, #551, and #550, as well as the respective fixes in #548, #549, #552, and #553). In this regard, I consider this issue to have been quite lucrative.

Unfortunately, I think I will have to admit defeat on the end goal of actually implementing the plan described in #542 (comment) — at least for now. The problem is that there is no way to uniformly implement the plan in all forms of type signatures. There are two places where the plan falls apart:

1. GADT constructor types. GHC flat-out disallows nested foralls in the syntax of GADT constructors, so it would be impossible to write something like this:

   $(singletons [d| data Foo a b = MkFoo a b |])
   
   -- ==>
   
   data SFoo z where
     SMkFoo :: forall a b.
               forall (x :: a). Sing x ->
               forall (y :: b). Sing y ->
               SFoo (MkFoo a b)

   Lifting this restriction would require fixing GHC#18389 first.

   If this were the only obstacle, then I wouldn't be too bothered with just having a special case for data constructors, as they are quite special already. However, this isn't the only place where nested foralls cause issues...

2. Class method defaults. This one really surprised me, and it takes some explanation to see what goes wrong. First, consider a type class where the methods have default implementations, such as Eq:

   $(singletons
     [d| class Eq a where
           (==) :: a -> a -> Bool
           x == y = not (x /= y)
           
           (/=) :: a -> a -> Bool
           x /= y = not (x == y)
       |])

   In today's singletons-th, the generated SEq class will have default signatures for each of the method defaults:

   class SEq a where
     (%==) :: forall (x :: a) (y :: a).
              Sing x -> Sing y -> Sing (x == y)
     default (%==) :: forall (x :: a) (y :: a). ((x == y) ~ Not (x /= y)) =>
                      Sing x -> Sing y -> Sing (x == y)
     sx %== sy = sNot (sx %/= sy)
   
     (%/=) :: forall (x :: a) (y :: a).
              Sing x -> Sing y -> Sing (x /= y)
     default (%/=) :: forall (x :: a) (y :: a). ((x /= y) ~ Not (x == y)) =>
                      Sing x -> Sing y -> Sing (x /= y)
     sx %/= sy = sNot (sx %== sy)

   Note the equality constraints (e.g., (x == y) ~ Not (x /= y)) in each of the default type signatures, which are crucial to making the default implementations typecheck. Importantly, each of these equality constraints must mention both x and y.

   Now imagine what would happen if we instead generated the types of SEq's methods according to the plan above. It would look something like this:

   class SEq a where
     (%==) :: forall (x :: a). Sing x ->
              forall (y :: a). Sing y ->
              Sing (x == y)
     default (%==) :: forall (x :: a). Sing x ->
                      forall (y :: a). Sing y ->
                      ((x == y) ~ Not (x /= y)) =>
                      Sing (x == y)
     sx %== sy = sNot (sx %/= sy)
   
     (%/=) :: forall (x :: a). Sing x ->
              forall (y :: a). Sing y ->
              Sing (x /= y)
     default (%/=) :: forall (x :: a). Sing x ->
                      forall (y :: a). Sing y ->
                      ((x /= y) ~ Not (x == y)) =>
                      Sing (x /= y)
     sx %/= sy = sNot (sx %== sy)

   This class definition does typecheck, but we are on thin ice. In fact, the ice breaks completely when we try to define an instance of SEq that relies on one of these method defaults, e.g.,

   instance SEq Bool where
     SFalse %== SFalse = STrue
     STrue  %== STrue  = STrue
     SFalse %== STrue  = SFalse
     STrue  %== SFalse = SFalse

   This will fail to typecheck with:

   Bug.hs:78:10: error:
       • Couldn't match type: (Not (x == y) ~ Not (x == y)) =>
                              SBool (Not (x == y))
                        with: SBool (Not (x == y))
         Expected: Sing x -> forall (y :: Bool). Sing y -> Sing (x /= y)
           Actual: Sing x
                   -> forall (y :: Bool).
                      Sing y -> ((x /= y) ~ Not (x == y)) => Sing (x /= y)
       • In the expression: Bug.$dm%/= @(Bool)
         In an equation for ‘%/=’: (%/=) = Bug.$dm%/= @(Bool)
         In the instance declaration for ‘SEq Bool’
       • Relevant bindings include
           (%/=) :: Sing x -> forall (y :: Bool). Sing y -> Sing (x /= y)
             (bound at Bug.hs:78:10)
      |
   78 | instance SEq Bool where
      |          ^^^^^^^^
   

   Ouch! What happens here is that under the hood, GHC is filling in a default implementation for (%/=) roughly like so:

   defaultImpl :: forall a. SEq a =>
                  forall (x :: a). Sing x ->
                  forall (y :: a). Sing y ->
                  ((x /= y) ~ Not (x == y)) =>
                  Sing (x /= y)
   defaultImpl sx sy = sNot (sx %== sy)
   
   instance SEq Bool where
     SFalse %== SFalse = STrue
     STrue  %== STrue  = STrue
     SFalse %== STrue  = SFalse
     STrue  %== SFalse = SFalse
     
     (%/=) = defaultImpl

   The (%/=) = defaultImpl does not typecheck under simplified subsumption, however. It would typecheck if GHC instead generated code like x %/= y = defaultImpl x y, but DefaultSignatures does not attempt to eta expand default implementations like this. I even asked if GHC could do this for you in GHC#19432, but the consensus was that this would require a semantic change to the way DefaultSignatures worked, and I didn't feel like making a GHC proposal just for this one little thing.

   Unfortunately, singletons-th really does need to use DefaultSignatures here to make SEq instances with defaults typecheck—or, at the very least, something very close in spirit to DefaultSignatures. I can see the following ways to work around the issue, but I'm not particularly fond of any of them:

   • Carve out a special case for class methods and require them to have prenex foralls.
   • Require singletons-th users to enable DeepSubsumption to make the generated defaults typecheck.
   • Make a GHC proposal to change the behavior of DefaultSignatures to make it perform more eta expansion.
   • Instead of using DefaultSignatures, manually generate top-level defaultImpl functions and apply them in instances, using knowledge of how many visible arguments each method has to determine how many arguments should be eta expanded. This would imply that singletons-th users would need to be aware of these defaultImpl functions and export them from their modules, so we would have to come up with a suitable naming convention for them.

   Ugh. What a headache.

---

For now, I think I'm simply going to park this. My WIP implementation can be found in the T542-experiment branch.

[goldfirere]

Ugh. Nice write up. I agree with your conclusion.