Reduce defunctionalization symbol bloat related to local variables

[RyanGlScott]

Consider this example:

{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -ddump-splices #-}
module Bug where

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

$(singletons
  [d| f :: forall a b c. Maybe (a, b, c)
      f = let x = Nothing in x
    |])

This will generate a surprising amount of code related to defunctionalization symbols:

[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
Bug.hs:(13,2)-(16,7): Splicing declarations
    singletons
      [d| f_a8bM ::
            forall a_a8bN b_a8bO c_a8bP. Maybe (a_a8bN, b_a8bO, c_a8bP)
          f_a8bM = let x_a8bQ = Nothing in x_a8bQ |]
  ======>
    f_a8di ::
      forall a_a8df b_a8dg c_a8dh. Maybe (a_a8df, b_a8dg, c_a8dh)
    f_a8di = let x_a8dj = Nothing in x_a8dj
    data Let6989586621679041395XSym0 a6989586621679041365
      where
        Let6989586621679041395XSym0KindInference :: SameKind (Apply Let6989586621679041395XSym0 arg_a8dK) (Let6989586621679041395XSym1 arg_a8dK) =>
                                                    Let6989586621679041395XSym0 a6989586621679041365
    type instance Apply Let6989586621679041395XSym0 a6989586621679041365 = Let6989586621679041395XSym1 a6989586621679041365
    instance SuppressUnusedWarnings Let6989586621679041395XSym0 where
      suppressUnusedWarnings
        = snd ((,) Let6989586621679041395XSym0KindInference ())
    data Let6989586621679041395XSym1 a6989586621679041365 b6989586621679041366
      where
        Let6989586621679041395XSym1KindInference :: SameKind (Apply (Let6989586621679041395XSym1 a6989586621679041365) arg_a8dK) (Let6989586621679041395XSym2 a6989586621679041365 arg_a8dK) =>
                                                    Let6989586621679041395XSym1 a6989586621679041365 b6989586621679041366
    type instance Apply (Let6989586621679041395XSym1 a6989586621679041365) b6989586621679041366 = Let6989586621679041395XSym2 a6989586621679041365 b6989586621679041366
    instance SuppressUnusedWarnings (Let6989586621679041395XSym1 a6989586621679041365) where
      suppressUnusedWarnings
        = snd ((,) Let6989586621679041395XSym1KindInference ())
    data Let6989586621679041395XSym2 a6989586621679041365 b6989586621679041366 c6989586621679041367
      where
        Let6989586621679041395XSym2KindInference :: SameKind (Apply (Let6989586621679041395XSym2 a6989586621679041365 b6989586621679041366) arg_a8dK) (Let6989586621679041395XSym3 a6989586621679041365 b6989586621679041366 arg_a8dK) =>
                                                    Let6989586621679041395XSym2 a6989586621679041365 b6989586621679041366 c6989586621679041367
    type instance Apply (Let6989586621679041395XSym2 a6989586621679041365 b6989586621679041366) c6989586621679041367 = Let6989586621679041395X a6989586621679041365 b6989586621679041366 c6989586621679041367
    instance SuppressUnusedWarnings (Let6989586621679041395XSym2 a6989586621679041365 b6989586621679041366) where
      suppressUnusedWarnings
        = snd ((,) Let6989586621679041395XSym2KindInference ())
    type family Let6989586621679041395XSym3 a6989586621679041365 b6989586621679041366 c6989586621679041367 where
      Let6989586621679041395XSym3 a6989586621679041365 b6989586621679041366 c6989586621679041367 = Let6989586621679041395X a6989586621679041365 b6989586621679041366 c6989586621679041367
    type family Let6989586621679041395X a6989586621679041365 b6989586621679041366 c6989586621679041367 where
      Let6989586621679041395X a_a8df b_a8dg c_a8dh = NothingSym0
    type FSym0 :: forall a_a8df b_a8dg c_a8dh. Maybe (a_a8df, b_a8dg,
                                                      c_a8dh)
    type family FSym0 @a_a8df @b_a8dg @c_a8dh :: Maybe (a_a8df, b_a8dg,
                                                        c_a8dh) where
      FSym0 = F
    type F :: forall a_a8df b_a8dg c_a8dh. Maybe (a_a8df, b_a8dg,
                                                  c_a8dh)
    type family F @a_a8df @b_a8dg @c_a8dh :: Maybe (a_a8df, b_a8dg,
                                                    c_a8dh) where
      F @a_a8df @b_a8dg @c_a8dh = Let6989586621679041395XSym3 a_a8df b_a8dg c_a8dh
    sF ::
      forall a_a8df b_a8dg c_a8dh. Sing (FSym0 :: Maybe (a_a8df, b_a8dg,
                                                         c_a8dh))
    sF
      = let
          sX :: Sing @_ (Let6989586621679041395XSym3 a_a8df b_a8dg c_a8dh)
          sX = SNothing
        in sX

This generates Sym0 through Sym3 variants of Let6989586621679041395X, which allows Let6989586621679041395X to be partially applied with 0, 1, or 2 arguments. This work all goes to waste, however, as singletons-th will always apply Let6989586621679041395X to 3 arguments: the a, b, and c type variables. This is because a, b, and c are local variables, and local variables are always fully applied to local definitions, never partially applied.

As a result, we could get away with generating many fewer defunctionalization-related definitions here. I propose that singletons-th generate something like this:

    type family Let6989586621679039292XSym0 a6989586621679038864 b6989586621679038865 c6989586621679038866 where
      Let6989586621679039292XSym0 a6989586621679038864 b6989586621679038865 c6989586621679038866 = Let6989586621679039292X a6989586621679038864 b6989586621679038865 c6989586621679038866
    type family Let6989586621679039292X a6989586621679038864 b6989586621679038865 c6989586621679038866 where
      Let6989586621679039292X a_a7yU b_a7yV c_a7yW = NothingSym0
    type FSym0 :: forall a_a7yU b_a7yV c_a7yW. Maybe (a_a7yU, b_a7yV,
                                                      c_a7yW)
    type family FSym0 @a_a7yU @b_a7yV @c_a7yW :: Maybe (a_a7yU, b_a7yV,
                                                        c_a7yW) where
      FSym0 = F
    type F :: forall a_a7yU b_a7yV c_a7yW. Maybe (a_a7yU, b_a7yV,
                                                  c_a7yW)
    type family F @a_a7yU @b_a7yV @c_a7yW :: Maybe (a_a7yU, b_a7yV,
                                                    c_a7yW) where
      F @a_a7yU @b_a7yV @c_a7yW = Let6989586621679039292XSym0 a_a7yU b_a7yV c_a7yW
    sF ::
      forall a_a7yU b_a7yV c_a7yW. Sing (FSym0 :: Maybe (a_a7yU, b_a7yV,
                                                         c_a7yW))
    sF
      = let
          sX :: Sing @_ (Let6989586621679039292XSym0 a_a7yU b_a7yV c_a7yW)
          sX = SNothing
        in sX

Note that we only generate a single Sym0 definition, where the local variables (a, b, and c) are always passed as arguments. This means that the number <N> in Sym<N> would no longer takes local variables into account, only direct arguments.