Out-of-scope type variable when using `ScopedTypeVariables` in class method RHS

[RyanGlScott]

The following:

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

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

$(singletons
  [d| class C a where
        m :: forall b. a -> Maybe b
        m _ = Nothing :: Maybe b
    |])

Will cause singletons-th to generate ill-scoped code:

[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
Bug.hs:(13,2)-(17,7): Splicing declarations
    singletons
      [d| class C_alaI a_alaK where
            m_alaJ :: forall b_alaL. a_alaK -> Maybe b_alaL
            m_alaJ _ = Nothing :: Maybe b_alaL |]
  ======>
    class C_albX a_albZ where
      m_albY :: forall b_alc0. a_albZ -> Maybe b_alc0
      m_albY _ = Nothing :: Maybe b_alc0
    type MSym0 :: forall a_albZ b_alc0. (~>) a_albZ (Maybe b_alc0)
    data MSym0 :: (~>) a_albZ (Maybe b_alc0)
      where
        MSym0KindInference :: SameKind (Apply MSym0 arg_alce) (MSym1 arg_alce) =>
                              MSym0 a6989586621679091275
    type instance Apply MSym0 a6989586621679091275 = M a6989586621679091275
    instance SuppressUnusedWarnings MSym0 where
      suppressUnusedWarnings = snd ((,) MSym0KindInference ())
    type MSym1 :: forall a_albZ b_alc0. a_albZ -> Maybe b_alc0
    type family MSym1 (a6989586621679091275 :: a_albZ) :: Maybe b_alc0 where
      MSym1 a6989586621679091275 = M a6989586621679091275
    type M_6989586621679091277 :: a_albZ -> Maybe b_alc0
    type family M_6989586621679091277 (a_alcj :: a_albZ) :: Maybe b_alc0 where
      M_6989586621679091277 _ = NothingSym0 :: Maybe b_alc0
    type M_6989586621679091277Sym0 :: (~>) a_albZ (Maybe b_alc0)
    data M_6989586621679091277Sym0 :: (~>) a_albZ (Maybe b_alc0)
      where
        M_6989586621679091277Sym0KindInference :: SameKind (Apply M_6989586621679091277Sym0 arg_alck) (M_6989586621679091277Sym1 arg_alck) =>
                                                  M_6989586621679091277Sym0 a6989586621679091281
    type instance Apply M_6989586621679091277Sym0 a6989586621679091281 = M_6989586621679091277 a6989586621679091281
    instance SuppressUnusedWarnings M_6989586621679091277Sym0 where
      suppressUnusedWarnings
        = snd ((,) M_6989586621679091277Sym0KindInference ())
    type M_6989586621679091277Sym1 :: a_albZ -> Maybe b_alc0
    type family M_6989586621679091277Sym1 (a6989586621679091281 :: a_albZ) :: Maybe b_alc0 where
      M_6989586621679091277Sym1 a6989586621679091281 = M_6989586621679091277 a6989586621679091281
    class PC a_albZ where
      type family M (arg_alcd :: a_albZ) :: Maybe b_alc0
      type M a_alcg = Apply M_6989586621679091277Sym0 a_alcg
    class SC a_albZ where
      sM ::
        forall b_alc0 (t_alcm :: a_albZ). Sing t_alcm
                                          -> Sing (Apply MSym0 t_alcm :: Maybe b_alc0)
      default sM ::
                forall b_alc0
                       (t_alcm :: a_albZ). ((Apply MSym0 t_alcm :: Maybe b_alc0)
                                            ~ Apply M_6989586621679091277Sym0 t_alcm) =>
                                           Sing t_alcm -> Sing (Apply MSym0 t_alcm :: Maybe b_alc0)
      sM _ = SNothing :: Sing (NothingSym0 :: Maybe b_alc0)
    instance SC a_albZ =>
             SingI (MSym0 :: (~>) a_albZ (Maybe b_alc0)) where
      sing = singFun1 @MSym0 sM

Bug.hs:13:2: error: [GHC-97784]
    The Name ‘b_alc0’ is not in scope.
    Suggested fix:
      If you bound a unique Template Haskell name (NameU)
      perhaps via newName,
      then -ddump-splices might be useful.
   |
13 | $(singletons
   |  ^^^^^^^^^^^...

The culprit is this:

type M_6989586621679091277 :: a_albZ -> Maybe b_alc0
type family M_6989586621679091277 (a_alcj :: a_albZ) :: Maybe b_alc0 where
  M_6989586621679091277 _ = NothingSym0 :: Maybe b_alc0

Note that the b_alc0 in NothingSym0 :: Maybe b_alc0 is out of scope. I think we could reasonably fix this if we instead generated code that looked more like this:

type M_6989586621679091277 :: a_albZ -> Maybe b_alc0
type family M_6989586621679091277 @a_albZ @b_alc0 (a_alcj :: a_albZ) :: Maybe b_alc0 where
  M_6989586621679091277 @a_albZ @b_alc0 _ = NothingSym0 :: Maybe b_alc0

[RyanGlScott]

Another way to observe the issue:

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

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

$(singletons
  [d| class C a where
        m :: a -> Maybe a
        m _ = Nothing :: Maybe a
    |])

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

Bug.hs:12:2: error: [GHC-97784]
    The Name ‘a_a889’ is not in scope.
    Suggested fix:
      If you bound a unique Template Haskell name (NameU)
      perhaps via newName,
      then -ddump-splices might be useful.
   |
12 | $(singletons
   |  ^^^^^^^^^^^...