Promoting expression signatures can fail on GHC 8.10+

[RyanGlScott]

singletons used to have no trouble promoting this code:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Singletons.Prelude
import Data.Singletons.TH

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

However, if you try compiling this with GHC 8.10, you'll get the following error:

[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:14:3: error:
    The exact Name ‘a_a83H’ is not in scope
      Probable cause: you used a unique Template Haskell name (NameU), 
      perhaps via newName, but did not bind it
      If that's it, then -ddump-splices might be useful
   |
14 | $(singletons [d|
   |   ^^^^^^^^^^^^^^...

Big yikes. What changed? Inspecting the -ddump-simpl reveals that this is how f is promoted:

    type family F (a_a83K :: a_a83H) :: a_a83H where
      F x_a83M = Apply IdSym0 (x_a83M :: a_a83H)

Note that on GHC 8.10 or later, the a_a83H in Apply IdSym0 (x_a83M :: a_a83H) is out of scope due to GHC Proposal 103 having been implemented. Unfortunately, this presents another incongruity between terms and types that singletons must bridge, since not even giving F a standalone kind signature would bring a_a83H into scope.

One possibile way forward here is to use visible kind applications to bind kind variables. That is, promote F like this instead:

type family F (x :: a) :: a where
  F @a x = Apply IdSym0 (x :: a)

This works in that particular example, but there is danger on the horizon. What about this code?

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

This works today in both GHC 8.8 and 8.10. However, if we adopt our proposed redesign above, we would end up promoting g like this:

type family G (x :: a) :: a where
  G @a (x :: b) = Apply IdSym0 (x :: b)

While we can make b an alias for a at the term level, the same trick is not possible at the type level, as this type error proves:

[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:27:9: error:
    • Expected kind ‘a’, but ‘x :: b’ has kind ‘b’
    • In the second argument of ‘G’, namely ‘(x :: b)’
      In the type family declaration for ‘G’
   |
27 |   G @a (x :: b) = Apply IdSym0 (x :: b)
   |         ^^^^^^

I'm honestly not sure how we can restore singletons' previous expressivity vis-à-vis expression signatures going forward. Does anyone have any suggestions?

[RyanGlScott]

This bug is another obstacle in the way of fixing chunk (3) of #378 (comment). If this doesn't promote:

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

Then this will also be difficult to promote:

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

[goldfirere]

Could you go through the type and manually add kind signatures to all arguments?

Or we could use syntax like

    type family F (a_a83K :: a_a83H) :: a_a83H where
      forall x_a83M a_a83H. F x_a83M = Apply IdSym0 (x_a83M :: a_a83H)

Note that I didn't even need to put kind signatures on the forall bit. (Though I'm worried about knowing what order to put the variables in.) That would, at least, restore the previous behavior. Both the old version and the new version don't really mimic the behavior of -XScopedTypeVariables though.

Separately, I think it's a bug that kind signatures in type family equation left-hand sides are not pattern-like. Perhaps fixing that in GHC is another way forward.

[RyanGlScott]

There have been three potential remedies proposed so far:

1. Use visible kind applications:

   type family F (x :: a) :: a where
     F @a x = Apply IdSym0 (x :: a)

2. Annotate every required argument with a kind signature:

   type family F (x :: a) :: a where
     F (x :: a) = Apply IdSym0 (x :: a)

3. Explicitly quantify all variables in each type family equation:

   type family F (x :: a) :: a where
     forall a x. F x = Apply IdSym0 (x :: a)

I would characterize all of these solutions as roughly equivalent. They all fix F but do not work for things like G, since all of the following fail to typecheck:

1. type family G (x :: a) :: a where
     G @a (x :: b) = Apply IdSym0 (x :: b)

   Bug.hs:27:9: error:
       • Expected kind ‘a’, but ‘x :: b’ has kind ‘b’
       • In the second argument of ‘G’, namely ‘(x :: b)’
         In the type family declaration for ‘G’
      |
   27 |   G @a (x :: b) = Apply IdSym0 (x :: b)
      |         ^^^^^^
   

2. type family G (x :: a) :: a where
     G ((x :: b) :: a) = Apply IdSym0 (x :: b)

   Bug.hs:27:7: error:
       • Expected kind ‘a’, but ‘x :: b’ has kind ‘b’
       • In the first argument of ‘G’, namely ‘((x :: b) :: a)’
         In the type family declaration for ‘G’
      |
   27 |   G ((x :: b) :: a) = Apply IdSym0 (x :: b)
      |       ^^^^^^
   

3. type family G (x :: a) :: a where
     forall x a b. G (x :: b) = Apply IdSym0 (x :: b)

   Bug.hs:27:3: error:
       • Type variables ‘k’, ‘a’ are bound by a forall,
           but not used in the family instance
       • In the equations for closed type family ‘G’
         In the type family declaration for ‘G’
      |
   27 |   forall x a b. G (x :: b) = Apply IdSym0 (x :: b)
      |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   

Unfortunately, this means that none of the remedies quite get us back to the previous behavior.

Separately, I think it's a bug that kind signatures in type family equation left-hand sides are not pattern-like. Perhaps fixing that in GHC is another way forward.

I agree. In fact, I proposed this at one point, but it was deemed a "red herring" at the time. I think the herring has finally changed color!

[RyanGlScott]

Sigh. G isn't the only source of problems, it seems. Consider this function from D.S.Prelude.List:

singletons/src/Data/Singletons/Prelude/List/Internal.hs

Lines 648 to 649 in 94a1054

	genericTake :: (Integral i) => i -> [a] -> [a]
	genericTake = take

When promoted, this turns into:

type family GenericTake (x :: i) (y :: [a]) :: [a] where
    GenericTake x y = TakeSym0 @@ x @@ y

Seems straightforward enough. What happens if we try binding the kind variables as well?

type family GenericTake (x :: i) (y :: [a]) :: [a] where
    GenericTake @i @a x y = TakeSym0 @@ x @@ y

After doing this, GenericTake no longer compiles!

Bug.hs:34:41: error:
    • Expected kind ‘GHC.Types.Nat’, but ‘x’ has kind ‘i’
    • In the second argument of ‘(@@)’, namely ‘x’
      In the first argument of ‘(@@)’, namely ‘TakeSym0 @@ x’
      In the type ‘TakeSym0 @@ x @@ y’
   |
34 |     GenericTake @i @a x y = TakeSym0 @@ x @@ y
   |                                         ^

As it turns out, TakeSym0 :: Nat ~> [a] ~> [a], which means that the equation for GenericTake implicitly matches i against Nat. In order to do this correctly, we'd have to infer that i ~ Nat and then generate GenericTake @Nat @a x y = TakeSym0 @@ x @@ y. Ugh.

[goldfirere]

But that genericTake makes no sense. How does that compile? It's more polymorphic than its definition. I'm baffled.

[RyanGlScott]

Note that genericTake is only promoted, not singled:

singletons/src/Data/Singletons/Prelude/List/Internal.hs

Lines 641 to 648 in 94a1054

	-- These functions use Integral or Num typeclass instead of Int.
	--
	-- genericLength, genericTake, genericDrop, genericSplitAt, genericIndex
	-- genericReplicate
	--
	-- We provide aliases below to improve compatibility
	genericTake :: (Integral i) => i -> [a] -> [a]

It would indeed fail to compiled in singled form.

[goldfirere]

It also is not accepted in unsingled form -- in plain Haskell, it's meaningless. We are not in the business of taking ill-typed code and magically making it work. Either we strip these functions from our library or update their type signatures to be correct (and not polymorphic). I vote the former.

[RyanGlScott]

I'd be fine with removing these definitions as well. They've given me headaches in the past, but I never had a solid excuse to remove them until now. (My apologies to Jan, who originally added them in b0542d6.)

Still, there may be a future where promoted functions could conceivably match on invisible arguments. After all, there has been talk of supporting GADTs in singletons. If we really really want to support GADTs, then the remedies above would be at odds with definitions that match on GADT constructors.

[goldfirere]

then the remedies above would be at odds with definitions that match on GADT constructors.

How so?

[RyanGlScott]

What happens if you promote this code?

sym :: a :~: b -> b :~: a
sym Refl = Refl

Using today's promotion algorithm, you would get something like this:

type family Sym (x :: a :~: b) :: b :~: a where
  Sym Refl = Refl

This is fine. But if you explicitly bind the kind variables a and b:

type family Sym (x :: a :~: b) :: b :~: a where
  Sym @a @b Refl = Refl

Then GHC gripes thusly:

Bug.hs:15:13: error:
    • Expected kind ‘a :~: b’, but ‘Refl’ has kind ‘a :~: a’
    • In the third argument of ‘Sym’, namely ‘Refl’                                                
      In the type family declaration for ‘Sym’                                                     
   |                                                                                               
15 |   Sym @a @b Refl = Refl                                                                       
   |             ^^^^

In order to do this correctly, we'd have to infer that a ~ b and instead generate the equation Sym @a @a Refl = Refl.

[goldfirere]

I still like option (3) of #433 (comment). The problem you ran into there is very superficial: either we teach GHC to warn (not error) on unused bound variables in that position, or we teach singletons (or perhaps even th-desugar) to winnow the bound variables to only those that are lexically mentioned.

[RyanGlScott]

Option (3) might work if we scrape away any bound variables that aren't mentioned in a type family equation, but it will be tricky to get right. Here is a corner case:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Singletons.Prelude
import Data.Singletons.TH

$(singletons [d|
  f :: forall p. p -> p
  f = g
    where
      g = id :: p -> p
  |])

Currently, this promotes to approximately the following code (ignore the :: p -> p part for a moment):

    type family F (a :: p) :: p where
      forall a. F a = Apply (Let123Sym1 a) a

    ...

    type family Let123 a where
      forall a. Let123 a = IdSym0

Suppose that we wanted to preserve the :: p -> p during promotion. This would mean that we'd have to generate the equation Let123 a = IdSym0 :: p ~> p. But the p kind variable is nowhere in sight, neither in the equation itself nor in the type family header. This suggests that we would have to capture bound variables during lambda-lifting so that we could generate this code instead:

    type family F (a :: p) :: p where
      forall p a. F a = Apply (Let123Sym2 p a) a

    ...

    type family Let123 p a where
      forall p a. Let123 p a = IdSym0 :: p ~> p

[goldfirere]

Can you double-check that? What is the variable a in your Let123 equation? It's unused on the RHS.

But it would stand to reason that, if we have to do special munging with term-level variables in lambda-lifting, we would have to do the same with type-level variables.

[RyanGlScott]

Can you double-check that?

Yes, this is taken directly from the output of -ddump-splices (modulo simplification of names for presentation purposes).

What is the variable a in your Let123 equation? It's unused on the RHS.

When singling a function, singletons closes over local variables and promotes them as part of lambda lifting. The a happens to come from f, which has a local variable after eta expansion (done here):

  f :: forall p. p -> p
  f a = g a
    where
      g = id :: p -> p

You're correct in observing that a is unused in the definition of Let123 (or rather, in the definition of the lambda-lifted g). We should strive to do better some day, but the fact that a is unused is not relevant to the issue at hand. The thing that matters is the absence of p in Let123.

But it would stand to reason that, if we have to do special munging with term-level variables in lambda-lifting, we would have to do the same with type-level variables.

I'm not sure what you mean by "special munging", but it is certainly true that we lambda-lift term variables. I'm simply proposing that we lambda-lift type variables as well.

[goldfirere]

OK. Thanks for the explanation. Yes, we will have to close over scoped type variables when we lambda-lift, as this example demonstrates. But any treatment of expression type signatures will require careful work around scoped type variables...

[RyanGlScott]

I've encountered a tricky example that I'm not sure how to deal with:

$(promote [d|
  foo :: forall a. a -> ()
  foo x = const () (Nothing :: Maybe a)
  |])

This is a strange-looking function, but singletons generates code very similar to foo in various places. If you promote foo according to the approach in #433 (comment), you'll end up with something close to this:

type family Foo (x :: a) :: () where
  forall a x. Foo x = Const '() (Nothing :: Maybe a)

This, unfortunately, does not typecheck:

[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:24:10: error:
    • Type variable ‘a2’ is mentioned in the RHS,
        but not bound on the LHS of the family instance
    • In the equations for closed type family ‘Foo’
      In the type family declaration for ‘Foo’
   |
24 |   forall a x. Foo x = Const '() (Nothing :: Maybe a)
   |          ^

That error message is strange (it refers to a2, not a), but there is nevertheless a very real issue to contend with. GHC does not know that the a in Nothing :: Maybe a is also the kind of x, and therefore it concludes that a is not bound anywhere on the LHS. Major bummer.

A tempting solution is to annotate x with its kind to get forall a x. Foo (x :: a) = Const '() (Nothing :: Maybe a). That does work, but it's treading on thin ice. What if the user had written this instead?

$(promote [d|
  foo :: forall a. a -> ()
  foo (x :: b) = const () (Nothing :: Maybe a)
  |])

Then you'd generate this:

type family Foo (x :: a) :: () where
  forall a b x. Foo ((x :: b) :: a) = Const '() (Nothing :: Maybe a)

Which also doesn't typecheck:

[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:24:23: error:
    • Expected kind ‘a’, but ‘x :: b’ has kind ‘b’
    • In the first argument of ‘Foo’, namely ‘((x :: b) :: a)’
      In the type family declaration for ‘Foo’
   |
24 |   forall a b x. Foo ((x :: b) :: a) = Const '() (Nothing :: Maybe a)
   |                       ^^^^^^

In effect, this would prevent you from promoting any pattern-like type variables (unless they happened to be exactly the same as the argument type, e.g. ((x :: a) :: a)).

[RyanGlScott]

In fact, the annotate-arguments-with-their-kinds trick in #433 (comment) won't always work. Here is a counterexample:

$(singletons [d|
  bar :: forall a. ()
  bar = const () (Nothing :: Maybe a)
  |])

If we tried promoting bar to this:

type Bar :: forall a. ()
type family Bar where
  forall a. Bar = Const '() (Nothing :: Maybe a)

Then just like Foo in #433 (comment), Bar won't typecheck:

../Bug.hs:25:10: error:
    • Type variable ‘a2’ is mentioned in the RHS,
        but not bound on the LHS of the family instance
    • In the equations for closed type family ‘Bar’
      In the type family declaration for ‘Bar’
   |
25 |   forall a. Bar = Const '() (Nothing :: Maybe a)
   |          ^

Moreover, Bar does not have any visible arguments to annotate. As far as I can tell, the only possible way to make Bar work is with visible kind applications, like so:

type Bar :: forall a. ()
type family Bar where
  Bar @a = Const '() (Nothing :: Maybe a)

[RyanGlScott]

All of this makes me wonder: is supporting pattern-like variables in singletons doomed to fail? Perhaps we should just note in the singletons README that things like this:

$(singletons [d|
  baz :: a -> a
  baz (x :: b) = x
  |])

Are doomed to fail (unless something changes in the way GHC typechecks type family equations with pattern-like variables). This would be a breaking change, but then again, singletons only very recently gained the ability to have type variables in patterns in the first place. It might not be the worst thing in the world to take away (or partially take away) that ability.

[goldfirere]

If the feature is hard to support because GHC is stupid, then I'm OK with dropping the feature. The "stupid" bit is the fact that we have pattern-like variables in terms but not in types.

[RyanGlScott]

Alright. To summarize the events so far:

1. There might be a way forward if we abandon supporting pattern-like variables in promoted functions.
2. Visible kind applications seem like the way to go for mimicking the behavior of ScopedTypeVariables in type families, since unlike pattern signatures or explicit foralls, they are capable of handling examples like Bar in Promoting expression signatures can fail on GHC 8.10+ #433 (comment).

Unfortunately, I just discovered another roadblock. Here is an extra spicy example:

$(promote [d|
  f local = g
    where
      g :: forall a. a -> a
      g x = const (x :: a) local
  |])

If we use visible kind applications, then g will get lambda-lifted to something like this:

type family Let123 local (x :: a) :: a where
  Let123 @a local x = Const (x :: a) local

Notice that Let123 does not have a standalone kind signature—not even a CUSK, in fact. Surprisingly, this does not play well with the use of @a in the equation for Let123. Here is the error message you get when trying to compile this example:

Bug.hs:28:3: error:
    • Cannot apply function of kind ‘k0 -> a -> a’
      to visible kind argument ‘a’
    • In the type family declaration for ‘Let123’
   |
28 |   Let123 @a local x = Const (x :: a) local
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I'm honestly somewhat shocked that this doesn't work, since the kind of Let123 is forall {b} a. b -> a -> a. Shouldn't that imply that Let123 @a would work? Perhaps this doesn't work by design, however. It doesn't typecheck in 8.8.2, 8.10.1-rc1, or HEAD, so I might just be missing something about the way visible kind application works for CUSK-less declarations.

[goldfirere]

Visible kind application in an equation is essentially a form of polymorphic recursion. And that's not allowed unless you have a CUSK or SAK.

[RyanGlScott]

Visible kind application in an equation is essentially a form of polymorphic recursion. And that's not allowed unless you have a CUSK or SAK.

Uh oh. That might be the final nail in the coffin for making this work in the GHC of today (i.e., 8.10), since singletons actually generates this sort of code (see, for example, baz in the T312 test case). Unless you have some other idea to try?

[RyanGlScott]

For now, I have decided to just add some documentation to the README in #441 stating that promoting functions that rely on ScopedTypeVariables is fragile. Perhaps a future version of GHC will make this issue easier to solve.

[RyanGlScott]

I originally opened this issue in the wake of GHC proposal #103, which removes all implicit quantification of kind variables on the right-hand sides of type family equations. Well, almost all implicit quantification—there was still an exception for outermost kind variables, such as in the example below:

type family F :: Maybe a where
  F = Nothing :: Maybe a

Well, I'm here to report that that exception has been removed in GHC 9.8, which implements GHC proposal #425. What surprised me is that this regresses singletons in a couple of places. In particular, consider this example from the T183 test case:

singletons/singletons-base/tests/compile-and-dump/Singletons/T183.hs

Lines 52 to 54 in b6ca612

	foo8 :: forall a. Maybe a -> Maybe a
	foo8 x@(Just (_ :: a) :: Maybe a) = x
	foo8 x@(Nothing :: Maybe a) = x

Because th-desugar has no notion of @-patterns, this first desugars to something like:

foo8 :: forall a. Maybe a -> Maybe a
foo8 x@(Just (_ :: a) :: Maybe a) = x
foo8 x@(Nothing :: Maybe a)       = x

foo8 :: forall a. Maybe a -> Maybe a
foo8 (Just (wild :: a) :: Maybe a) =
  let x = Just (wild :: a) :: Maybe a
  in x
foo8 (Nothing :: Maybe a) =
  let x = Nothing :: Maybe a
  in x

When promoting the x in the second foo8 equation to a type family, it becomes:

type family LetX :: Maybe a where
  LetX = Nothing :: Maybe a

This relies on outermost kind variables being implicitly quantified to kind-check, so this no longer works in GHC 9.8! As such, if we want to avoid singletons from regressing in 9.8, we will need to come up with a different plan.

[RyanGlScott]

Here is a half-baked (read: not yet implemented) plan:

• singletons-th should adopt the position that all promoted/singled code is assumed to adhere to -Werror=pattern-signature-binds, as in GHC proposal #448 (modern scoped type variables). That is, examples like this one:

  g :: forall a. Maybe a -> Maybe a
  g (x :: b) = id (x :: b)

  Will be rejected by singletons-th.

• When promoting a function with a top-level type signature, track its type variables and bind them in the corresponding type family equations using @. For instance, promote this function:

  f :: forall p. p -> p
  f x = g (x :: p)
    where
      g x = (id :: p -> p) x

  To the following:

  type F :: forall p. p -> p
  type family F x where
    F @p x = LetG p (x :: p)
  
  type family LetG p x where
    LetG p x = Apply (IdSym0 :: p ~> p) x

  Also note that LetG closes over the scoped type variable p, making it a visible argument. The choice to make it a visible argument is important. Because LetG lacks a standalone kind signature, we cannot write this:

  type family LetG x where
    LetG @p x = Apply (IdSym0 :: p ~> p) x

  As that would constitute "essentially a form of polymorphic recursion" (see Promoting expression signatures can fail on GHC 8.10+ #433 (comment)).

I think that would cover most of the useful examples in this thread. Am I overlooking anything?

[RyanGlScott]

Am I overlooking anything?

Ugh, yes, I am overlooking something. Recall the extra-spicy example from #433 (comment):

f local = g
  where
    g :: forall a. a -> a
    g x = const (x :: a) local

What makes this so spicy is that g is both (1) a local function that closes over a free variable local, whose type is unspecified, and (2) uses a scoped type variable in its type signature. My comment above doesn't specify what should happen in this case, since the one example it gives has a local function without a type signature. At first, I had an idea to try this:

type G :: forall a. forall local -> a -> a
type family G local x where
  G local x = Const (x :: a) local

Notice that I am using visible dependent quantification to bind the local argument without having to specify what its kind is. And in this case, this trick works! GHC does warn that local is unused in the standalone kind signature, but we could fix this with a hack like this:

-- This is essentially just `Const` with a different name
type WithLocals x y = x

type G :: forall a. local -> a -> a `WithLocals` local

This trick is fragile, however. Here is a slight variant of this example to increase the spice one level further:

konst :: a -> Bool -> a
konst x _ = x

f local = g
  where
    g :: forall a. a -> a
    g x = konst (x :: a) local

This time, local must be inferred to have type Bool in order for for f to typecheck. According to the promotion strategy described above, we would get:

type Konst :: a -> Bool -> a
type family Konst x y where
  Konst x _ = x

type G :: forall a. forall local -> a -> a
type family G local x where
  G local x = Konst (x :: a) local

Here is where things get dicey. Because G has a standalone kind signature, GHC will kind-generalize it before kind-checking the body of G, so the full kind of G is:

type G :: forall {k} a. forall (local :: k) -> a -> a

Note that local is of kind k, not Bool, which is more general than what we want. Despite this, the body of G actually does kind-check in today's GHC. This is because it is tantamount to writing this:

type G :: forall {k} a. forall (local :: k) -> a -> a
type family G local x where
  G @Bool (local :: Bool) x = Konst (x :: a) local

But note that the left-hand side of the original question lacks the @Bool part, which means that the left-hand side does not fully determine instantiation. While this works in today's GHC, this would no longer work once this part of GHC proposal #425 is implemented (see this MR, which implements it). I'd hate to add a feature only to see it be removed within a small number of GHC releases, so this gives me pause.

What should we do about all this? I suppose singletons-th chould throw an error whenever a local function both (1) closes over free variables and (2) uses scoped type variables in its a standalone kind signature. That would likely reject code that is currently in use in singletons-base, but perhaps we could repair it.

[goldfirere]

The challenge is to promote

f local = g
  where
    g :: forall a. a -> a
    g x = konst (x :: a) local

The text above suggests that it's the scoped type variable that causes trouble. Why is that? That is, I would imagine any signature on g would cause trouble, whether or not it binds a scoped type variable. Is it because you can't have e.g. LetG @a ... = ... without a signature? So if there are no scoped type variables, maybe you can just omit the signature entirely. If there is a scoped type variable, could that be passed as a required argument? Presumably yes -- it's demonstrated above -- but the problem then moves to call sites, where you won't know how to instantiate the parameter. I'm tempted to use _ as the argument, but that won't work -- only @_ works.

Sadly, this thinking aloud doesn't end in a solution, but maybe it help further the conversation.

[RyanGlScott]

The text above suggests that it's the scoped type variable that causes trouble. Why is that? That is, I would imagine any signature on g would cause trouble, whether or not it binds a scoped type variable.

Fair enough, there are actually two distinct (but related) issues here:

1. Finding a way to promote scoped type variables in a way that interacts well with singletons-th's lambda lifting.
2. Finding a way to lambda lift in a way that infers appropriate kinds for local variables that a lambda closes over.

Issue (1) is specifically about local functions that bind scoped type variables, but issue (2) arises for any local function that has a type signature. Currently, singletons-th implements a hacky solution for (2) in which any local function that closes over local variables will be promoted to a type family without a standalone kind signature. This is unfortunate, since that does change the local function's behavior vis-à-vis type inference—imagine if the local function was polymorphically recursive, for instance. singletons-th does not attempt to solve issue (1) at all, which is why I originally opened this issue.

My half-baked plan in #433 (comment) attempts to address both issues. It attempts to address issue (1) by binding scoped type variables by promoting them to uses of @ in type family equations (and by passing them to local functions as required arguments), and it attempts to address issue (2) by promoting local functions' type signatures to standalone kind signatures using visible dependent quantification. As noted in #433 (comment), this plan doesn't really work, but that's how I'm thinking about it.

Is it because you can't have e.g. LetG @a ... = ... without a signature?

Yes, that's a key part of issue (1).

So if there are no scoped type variables, maybe you can just omit the signature entirely.

Indeed, we could fall back to the hacky solution for issue (2) when a function does not bind any scoped type variables—that would be no worse that the current status quo. (Of course, the extra-spicy given in #433 (comment) does bind a scoped type variable in g, so this is of no help there.)

If there is a scoped type variable, could that be passed as a required argument? Presumably yes -- it's demonstrated above -- but the problem then moves to call sites, where you won't know how to instantiate the parameter. I'm tempted to use _ as the argument, but that won't work -- only @_ works.

Indeed, if we could promote g to this:

type G a local (x :: a) :: a where
  G a local (x :: a) = Konst (x :: a) local

Then we wouldn't need to write @a, and therefore, we wouldn't need to give G a standalone kind signature. But as you say, the tricky part would be knowing what a should be when we invoke G. That sounds hard to determine in general without performing type inference, which would be challenging in a Template Haskell–based setting like ours.

Sadly, this thinking aloud doesn't end in a solution, but maybe it help further the conversation.

One thing that popped into my mind while writing this up: how could we change GHC to make this easier? My first thought was implementing updated partial type signatures, which would let us more directly specify that things like local should have the kinds inferred, not generalized. That sounds like a lot of work, however. An alternative would be to use the @_ trick to prevent kind generalization. For instance, if you write this:

konst :: a -> Bool -> a
konst x _ = x

type KindOf (a :: k) = k
type family Any :: k

g :: forall (local :: KindOf @_ Any) a. a -> a
g x = konst (x :: a) @local

Then local's kind will be inferred to be Bool instead of being generalized to k. This is because visibly applying @_ signals to GHC not to perform kind generalization, instead letting kind inference do its job.

Sadly, the same trick doesn't work in standalone kind signatures. If you write this:

type G :: forall (local :: KindOf @_ Any) a. a -> a

Then you run into this GHC issue. So perhaps fixing that issue would provide one relatively quick way to make this work, without the need to implement a large-scale proposal like updated partial type signatures.

[goldfirere]

OK. That all makes some sense.

The quick way you highlight at the end of your comment won't work. Even if we had wildcards in kind signatures, the presence of any such wildcard would disable polymorphic recursion, and we'd be back to square 1. (Wildcards in kind signatures would be lovely, but they wouldn't solve this problem.)

Updated partial type signatures likely would solve this problem, but I agree that's a long way off.

... wandered off in several directions, none of which worked ...

Tell me more about hacky approach (2). Going back to our challenge

f local = g
  where
    g :: forall a. a -> a
    g x = konst (x :: a) local

what if we promote g like this:

type family LetG local x where
  LetG local (x :: a) = Konst (x :: a) local

? The :: a to the left of the = came from the type signature on the original g, broken into pieces and then inserted as type signatures. This approach basically ignores the presence of the scoped type variable, but works regardless.

(Digression: though I'm now worried about

f :: forall a. a -> a
f x = g x True
  where
    g :: b -> a -> b
    g y _ = y

where the a in the type of g is not scoped and refers to a different type than the outer a. Though I suppose the renamer would sort that out? Actually probably OK, but perhaps worth testing.)

This new approach wouldn't work if the only mention of a scoped type variable is in the result, because of upcoming changes to GHC, which require all type variables brought into scope in a type family equation to appear to the left of the =. But the approach at least moves us forward. And then the way forward from there seems clear: we add result type signatures to type family equations in GHC. That is we really should allow this:

type family F x where
  F x :: a = x

where that :: a appears to the left of the = but actually is the type of the RHS (or, equivalently, the entire LHS, including the F). We recently have these for term definitions. So let's have them for types, too. And then we should be in good shape here. The medium term would be OK in this plan: a scoped type variable appearing only in a result type would be lost, and programs wouldn't compile, but they'd still never be misinterpreted.

What do you think?

[RyanGlScott]

what if we promote g like this:

type family LetG local x where
  LetG local (x :: a) = Konst (x :: a) local

? The :: a to the left of the = came from the type signature on the original g, broken into pieces and then inserted as type signatures. This approach basically ignores the presence of the scoped type variable, but works regardless.

Ah, this is an interesting idea. As you say later in the comment, this wouldn't work in situations where the scoped type variable is only mentioned in the result. And in fact, this is exactly what happens in the T183 example mentioned in #433 (comment), which was the example that motivated me to revive this discussion. It would be sad to still not accept that, but on the other hand, it would also be cool to accept the extra-spicy example using your approach.

I suppose we could combine your approach (attach explicit kind signatures to type family arguments whenever possible) with mine (use type variables as required arguments in lambda-lifting, plus use @ whenever possible) to get the best of both worlds. That would allow us to accept both T183 and the extra-spicy example, I believe. It wouldn't be enough to accept something like this:

f local = g
  where
    g :: forall a. Nothing a
    g = konst (Nothing :: a) local

But as you say, we could get there if type family left-hand sides supported result signatures. So I think I'm on board. I'll see what happens when I implement this.

(Digression: though I'm now worried about

f :: forall a. a -> a
f x = g x True
  where
    g :: b -> a -> b
    g y _ = y

where the a in the type of g is not scoped and refers to a different type than the outer a. Though I suppose the renamer would sort that out? Actually probably OK, but perhaps worth testing.)

A good thing to worry about. I tried splicing such a function into GHC using a TH quote (ensuring that NoScopedTypeVariables was set), and -ddump-splices told me this:

Bug.hs:(5,2)-(10,7): Splicing declarations
    [d| f_aBv :: forall a_aBw. a_aBw -> a_aBw
        f_aBv x_aBx
          = g_aBy x_aBx True
          where
              g_aBy :: b_aBz -> a_aBA -> b_aBz
              g_aBy y_aBB _ = y_aBB |]
  ======>
    f_a260 :: forall a_a25Z. a_a25Z -> a_a25Z
    f_a260 x_a261
      = g_a264 x_a261 True
      where
          g_a264 :: b_a262 -> a_a263 -> b_a262
          g_a264 y_a265 _ = y_a265

Those two as (a_a25Z and a_a263) have different uniques, so that's a good sign. My hope (currently untested) is that g would be promoted to something like this:

type family G a1 x (y :: b) (z :: a2) :: b where
  G a1 x (y :: b) (z :: a2) = y

Which shouldn't pose any issues.

[goldfirere]

Good. This does seem like a way forward, imperfect though it is.

[RyanGlScott]

I've made an attempt at implementing this in the T443 branch. Happily, the "attach explicit kind signatures to type family arguments whenever possible" part of the plan works like a charm. Much less happily, however, the "use type variables as required arguments in lambda-lifting, plus use @ whenever possible" part of the plan causes singletons-base to panic when compiled:

$ cabal build -w ghc-9.6 singletons-base
Build profile: -w ghc-9.6.2 -O1
In order, the following will be built (use -v for more details):
 - singletons-base-3.2 (lib:singletons-base) (file /home/ryanglscott/Documents/Hacking/Haskell/ci-maintenance/checkout/goldfirere/singletons/dist-newstyle/build/x86_64-linux/ghc-9.6.2/singletons-th-3.2/cache/build changed)
Preprocessing library for singletons-base-3.2..
Building library for singletons-base-3.2..
[34 of 48] Compiling Data.Traversable.Singletons ( src/Data/Traversable/Singletons.hs, /home/ryanglscott/Documents/Hacking/Haskell/ci-maintenance/checkout/goldfirere/singletons/dist-newstyle/build/x86_64-linux/ghc-9.6.2/singletons-base-3.2/build/Data/Traversable/Singletons.o, /home/ryanglscott/Documents/Hacking/Haskell/ci-maintenance/checkout/goldfirere/singletons/dist-newstyle/build/x86_64-linux/ghc-9.6.2/singletons-base-3.2/build/Data/Traversable/Singletons.dyn_o ) [Control.Monad.Singletons.Internal changed]

<no location info>: error:
    panic! (the 'impossible' happened)
  GHC version 9.6.2:
        NoFlexi
  m_aojw[tyv:1] :: *
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/GHC/Utils/Panic.hs:189:37 in ghc:GHC.Utils.Panic
        pprPanic, called at compiler/GHC/Tc/Utils/Zonk.hs:1821:18 in ghc:GHC.Tc.Utils.Zonk
  CallStack (from HasCallStack):
    panic, called at compiler/GHC/Utils/Error.hs:454:29 in ghc:GHC.Utils.Error


Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug

Error: cabal: Failed to build singletons-base-3.2.

What's more, if you copy the -ddump-splices output from Data.Traversable.Singletons and paste it directly as non-TH code, then compilation succeeds. This makes me believe that we are once again running into our old foe GHC#11812.

You can hack around this issue by tweaking the code in Data.Traversable.Singletons slightly:

diff --git a/singletons-base/src/Data/Traversable/Singletons.hs b/singletons-base/src/Data/Traversable/Singletons.hs
index 65e226e..5f91f4c 100644
--- a/singletons-base/src/Data/Traversable/Singletons.hs
+++ b/singletons-base/src/Data/Traversable/Singletons.hs
@@ -297,7 +297,7 @@ $(singletonsOnly [d|
   foldMapDefault :: forall t m a . (Traversable t, Monoid m)
                  => (a -> m) -> t a -> m
   foldMapDefault f x = case traverse (mkConst . f) x of Const y -> y
-    where
-      mkConst :: m -> Const m ()
-      mkConst = Const
+
+  mkConst :: m -> Const m ()
+  mkConst = Const
   |])

That's enough to get a complete build of singletons-base, but then you'll run into similar NoFlexi panics in the CaseExpressions, T183, and T296 test cases. All of these test cases involve interesting uses of scoped type variables in some way, but beyond that, it's difficult to tell if there is a specific pattern that triggers the panic.

Our usual workaround for GHC#11812 is to sprinkle uses of noExactTyVars in various places. Doing so is enough to fix some, but not all, of the panics seen above. I need to do more digging to see what exactly causes each panic, which might reveal potential workarounds.

[RyanGlScott]

Here is a workaround for the panics seen in #433 (comment):

diff --git a/singletons-th/src/Data/Singletons/TH/Promote.hs b/singletons-th/src/Data/Singletons/TH/Promote.hs
index 300347c..7618dee 100644
--- a/singletons-th/src/Data/Singletons/TH/Promote.hs
+++ b/singletons-th/src/Data/Singletons/TH/Promote.hs
@@ -760,7 +760,7 @@ promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do
           m_fixity   = OMap.lookup name fix_env
 
           mk_tf_head :: [DTyVarBndrUnit] -> DFamilyResultSig -> DTypeFamilyHead
-          mk_tf_head tvbs res_sig = DTypeFamilyHead proName tvbs res_sig Nothing
+          mk_tf_head tvbs res_sig = DTypeFamilyHead proName (noExactTyVars tvbs) (noExactTyVars res_sig) Nothing
 
           (lde_kvs_to_bind, m_sak_dec, defun_ki, tf_head) =
               -- There are three possible cases:
@@ -1093,7 +1093,7 @@ promoteExp (DCaseE exp matches) = do
   tyvarName  <- qNewName "t"
   let all_args = all_locals ++ [tyvarName]
       tvbs     = map (`DPlainTV` ()) all_args
-  emitDecs [DClosedTypeFamilyD (DTypeFamilyHead caseTFName tvbs DNoSig Nothing) eqns]
+  emitDecs [DClosedTypeFamilyD (DTypeFamilyHead caseTFName (noExactTyVars tvbs) DNoSig Nothing) eqns]
     -- See Note [Annotate case return type] in Single
   let applied_case = prom_case `DAppT` exp'
   return ( applied_case
diff --git a/singletons-th/src/Data/Singletons/TH/Util.hs b/singletons-th/src/Data/Singletons/TH/Util.hs
index c0600fc..a4e0171 100644
--- a/singletons-th/src/Data/Singletons/TH/Util.hs
+++ b/singletons-th/src/Data/Singletons/TH/Util.hs
@@ -390,8 +390,12 @@ noExactTyVars = everywhere go
 
 -- changes a Name not to be a NameU. Workaround for GHC#11812/#17537/#19743
 noExactName :: Name -> Name
-noExactName (Name (OccName occ) (NameU unique)) = mkName (occ ++ show unique)
-noExactName n                                   = n
+noExactName (Name (OccName occ) nf)
+  | NameU unique <- nf = mk_name unique
+  | NameL unique <- nf = mk_name unique
+  where
+    mk_name u = mkName (occ ++ show u)
+noExactName n = n
 
 substKind :: Map Name DKind -> DKind -> DKind
 substKind = substType

The part that I was missing was extending noExactName to include NameLs in addition to NameUs. It turns out that if you write f (x :: a) = ..., where a is not previously bound by a scoped type variable, than a becomes a NameL, so it's important to change those as well.

While this is a serviceable workaround, it does degrade the quality of the Haddocks a bit, since now you'd end up with things like type Foo (a :: a01234567890123456789) :: a01234567890123456789 in the rendered Haddocks. At the very least, I think we can be a bit more clever and only apply noExactName to local variables, which only appear in definitions that are less important Haddock-wise.