Track the kinds of scoped type variables using `LocalVar`s

[RyanGlScott]

(Originally posted in https://github.com/goldfirere/singletons/pull/610#issuecomment-2190208845).

As of #610, we use LocalVars to track the kinds of promoted term-level variables, but not the kinds of scoped type variables:

https://github.com/goldfirere/singletons/blob/a3511058a6f0027edcfec891748e7433ffbb9188/singletons-th/src/Data/Singletons/TH/Promote/Monad.hs#L31-L35

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. As such, the kind of LetY is more general than intended:

LetY :: forall {k1} {k2}. k1 -> forall (a :: k2) -> Proxy a -> Proxy a 

This doesn't cause problems in any of the code in singletons-base, but I could easily foresee this being an issue in more sophisticated code. (See also #601.) 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).

[RyanGlScott]

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 retract this claim, as there is one place where we rely on pr_scoped_vars being an OSet: when promoting pattern signatures. For example, consider foo8 from the T183 test case:

https://github.com/goldfirere/singletons/blob/ae2a94ff73e5cb5fb47f7a91a1c1f0d396f2eb1c/singletons-base/tests/compile-and-dump/Singletons/T183.hs#L52-L54

When promoting the Just (_ :: a) pattern, should we bind a as a scoped type variable? It depends! If a is already in scope (i.e., due to an outermost forall, like what foo8's type signature uses), then we treat a as a bound variable rather than binding it as a scoped type variable. Otherwise, we do bind a. This means that we can't add to the scoped type variables unconditionally, as whether we do or not depends on whether pr_scoped_vars already contains a or not.

If pr_scoped_vars is an OSet, then checking this is easy: we just call OSet.insert a (pr_scoped_vars ...), and OSet.insert will do the heavy lifting of checking if a is already contained in the scoped type variables or not. If pr_scoped_vars were a list, however, we'd need to explicitly check if a is contained in the list beforehand, which is an O(n) operation. Not impossible, but a tad bit unsightly.

For this reason, I'm inclined to keep pr_scoped_vars as an OSet and instead change the Ord instance for LocalVar to only consider the Name (and not the Maybe DKind) for comparison purposes. We maintain the invariant that every LocalVar Name uniquely maps to a Maybe DKind, so this should be an acceptable thing to do.