Record local variables' kinds during lambda lifting

[RyanGlScott]

Previously, singletons-th made no effort to track the kinds of local variables when generating lambda-lifted code, instead generating local variable binders with no kind annotations. As a result, GHC would generalize the kinds of these lambda-lifted definitions to things that are way more polymorphic than intended. While this technically works in today's GHC, it won't in a future version of GHC that implements GHC#23515.

In general, generating kinds for every local variable would require singletons-th to implement something akin to full-blown type inference over the Template Haskell AST, which is not something I am eager to implement.

Fortunately, there is a relatively simple approach we can do to alleviate this problem that doesn't require full type inference. In situations where we know the kind of a local variable (e.g., when there is a top-level signature or there is a pattern signature), we record the variable's kind and use it when generating binders for any lambda-lifted definitions that close over the variable. For the full story on how this works, see Note [Local variables and kind information] D.S.TH.Promote.Syntax.LocalVar.

This is not a perfect solution, as there will still be examples of the original problem that won't be covered by this simple approach (see the Note). This approach is still much better than what singletons-th was doing before, and I think it's worth using this simple approach even if it doesn't fix 100% of all cases.

This patch mostly resolves the "Overly polymorphic lambda-lifting, part 2" section of #601.

[RyanGlScott]

I've marked this as a draft because I still need to test these changes with a version of GHC that is built with the changes from GHC!12776. My hope is that this patch will be enough to fix the breakages that I noticed in #601 (comment), but I need to check.

[RyanGlScott]

While implementing this patch, I also discovered another place where we could make use of LocalVars where we currently do not. Namely, we use LocalVars to track the kinds of promoted term-level variables, but not the kinds of scoped type variables:

singletons/singletons-th/src/Data/Singletons/TH/Promote/Monad.hs

Lines 31 to 35 in a351105

	data PrEnv =
	PrEnv { pr_options :: Options
	, pr_scoped_vars :: OSet Name
	-- ^ The set of scoped type variables currently in scope.
	-- See @Note [Scoped type variables]@.

Note that pr_scoped_vars uses a set of Names rather than LocalVars. This means that if we were to promote something like this:

f :: forall k (a :: k). Proxy a -> Proxy a
f x = y
  where
    y = x

Then we promote y, we would get something like this:

type family LetY k a (x :: Proxy a) where
  LetY k a x = x

This doesn't record the fact that a :: k, unfortunately. If we used LocalVars in pr_scoped_vars, however, this would be possible. Note that if we did this, we might consider changing pr_scoped_vars to use a list of LocalVars instead of an OSet, as otherwise we would be sorting all of the LocalVars using their DKind's Ord instance, which seems wasteful. This is probably worth doing anyway, as we aren't really making essential use of the fact that pr_scoped_vars is an OSet (i.e., we aren't really using that many set-like operations on pr_scoped_vars).

I haven't bothered implementing this idea in this PR, as it wasn't important to fixing the examples of breakages that I observed in #601 (comment). I've opened a follow-up issue (#613) to track this idea as a separate improvement, however.

[RyanGlScott]

I've verified that this patch allows all of the examples in #601 (comment) to compile with a version of GHC that is built with the changes from GHC!12776. As such, I think this is ready to land.