"The Name is not in scope" error with VDQ in standalone kind signature

[RyanGlScott]

The following program:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -ddump-splices -dsuppress-uniques #-}
module Bug where

import Data.Kind (Type)
import Data.Proxy (Proxy)
import Data.Singletons.TH.Options
import Data.Singletons.Base.TH

$(withOptions defaultOptions{genSingKindInsts = False} $
  singletons [d|
  type D :: forall k. forall (a :: k) -> Proxy a -> Type
  data D x p = MkD
  |])

Will cause singletons-th to emit an out-of-scope Name error, which shouldn't happen under normal circumstances:

[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
Bug.hs:(14,2)-(18,5): Splicing declarations
    withOptions defaultOptions {genSingKindInsts = False}
      $ singletons
          [d| type D :: forall k. forall (a :: k) -> Proxy a -> Type

              data D x p = MkD |]
  ======>
    type D :: forall k. forall (a :: k) -> Proxy a -> Type
    data D x p = MkD
    type MkDSym0 :: forall x p. D x p
    type family MkDSym0 :: D x p where
      MkDSym0 = MkD
    type SD :: forall k (a :: k) (p :: Proxy a). D x p -> Type
    data SD :: forall k (a :: k) (p :: Proxy a). D x p -> Type
      where SMkD :: forall x p. SD (MkD :: D x p)
    type instance Sing @(D x p) = SD
    instance SingI MkD where
      sing = SMkD

Bug.hs:14:2: error: [GHC-97784]
    The Name ‘x’ is not in scope.
    Suggested fix:
      If you bound a unique Template Haskell name (NameU)
      perhaps via newName,
      then -ddump-splices might be useful.
   |
14 | $(withOptions defaultOptions{genSingKindInsts = False} $
   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Specifically, the culprit is in the standalone kind signature for SD, which mentions x in D x p without binding it:

    type SD :: forall k (a :: k) (p :: Proxy a). D x p -> Type

[RyanGlScott]

After looking at the code which generates standalone kind signatures for things like SD, it's clearer why this bug arises:

https://github.com/goldfirere/singletons/blob/2c91ce4ad7e80518f08ea7cf962c48820e83b309/singletons-th/src/Data/Singletons/TH/Single/Data.hs#L79-L96

Here, sing_data_sak is the final standalone kind signature (e.g., for SD), data_sak is the standalone kind signature for the original data type (e.g., for D), and tvbs are the type variable binders for the data type (e.g., the x p in data D x p). There are two things that are suspicious about this code:

1. This code splits partitions the invisible arguments in data_sak (invis_args) from the visible arguments (vis_args), and then prepends all of the invisible arguments before all of the visible arguments. This is very questionable, considering that a visible argument can precede an invisible argument due to nested foralls. (In this example, I don't think this ends up mattering, but it is fishy nonetheless.)

2. This code uses replaceTvbKind, which is defined like so:

   https://github.com/goldfirere/singletons/blob/2c91ce4ad7e80518f08ea7cf962c48820e83b309/singletons-th/src/Data/Singletons/TH/Util.hs#L366-L369

   The DVisFADep case is very suspect. In effect, this will discard a type variable binder in tvbs in favor of a visible dependent forall from data_sak. In the example above, that means discarding a in favor of x, which is the root of the issue above.

To do this properly, I think we will need to get rid of replaceTvbKind (which is quite broken w.r.t. visible dependent foralls) and instead implement something akin to the zipSAKS algorithm from this GHC proposal, which solves a similar problem.

[RyanGlScott]

GHC's implementation of zipSAKS is called matchUpSigWithDecl, which is very relevant here. An interesting thing about matchUpSigWithDecl: if you look up the D example above with :info in GHCi, you'll get:

  λ> :info D
  type D :: forall k. forall (x :: k) -> Proxy x -> Type
  data D x p = MkD

Note that the binders in data D x p have remained unchanged, but the a variable in the standalone kind signature has been renamed to x. I think we will want to do a similar renaming in singletons-th.