Simplify TH defunctionalization machinery slightly

The inner loop of the `defunctionalize` function was passing around
a higher-order function to compute the right-hand sides of `Apply`
instances. But this is really more complicated than it needs to be,
as it is quite feasible to determine what the right-hand side of any
`Apply` instance will be without keeping track of this extra state.
The general formula is simply:

```hs
type instnce Apply (DSym{n} a{1} ... a{n}) a_{n+1} =
  DSym{n+1} a{1} ... a{n} a{n+1}
```

Where `n` is the number of matchable arguments for the
defunctionalization symbol being generated.

Previously, `defunctionalize` had a special case for when
`n+1` equals the number of arguments the original type `D` accepts,
which caused it to generate `D a{1} ... a{n} a{n+1}` as the
right-hand side. Due to the aforementioned simplification, it now
generates `DSym{n+1} a{1} ... a{n} a{n+1}` instead, which causes
quite a number of golden test files to change. As a result, this
patch looks large, but the vast majority of the changes are simply
the result of `D` changing to `DSym{n+1}`.

src/Data/Singletons/Promote/Defun.hs

@@ -225,11 +225,9 @@ defunctionalize name m_fixity m_arg_tvbs' m_res_kind' = do
                           ++ maybeToList m_res_kind      -- (2)(i)(a)
 
       go :: Int -> [DTyVarBndr] -> Maybe DKind
-         -> ([DTyVarBndr] -> DType)  -- given the argument tyvar binders,
-                                     -- produce the RHS of the Apply instance
          -> PrM [DDec]
-      go _ [] _ _ = return []
-      go n (m_arg : m_args) m_result mk_rhs = do
+      go _ [] _ = return []
+      go n (m_arg : m_args) m_result = do
         extra_name <- qNewName "arg"
         let tyfun_name  = extractTvbName m_arg
             data_name   = promoteTySym name n
@@ -276,7 +274,8 @@ defunctionalize name m_fixity m_arg_tvbs' m_res_kind' = do
             app_eqn     = DTySynEqn Nothing
                                     (DConT applyName `DAppT` app_data_ty
                                                      `DAppT` DVarT tyfun_name)
-                                    (mk_rhs (m_args ++ [DPlainTV tyfun_name]))
+                                    (foldTypeTvbs (DConT next_name)
+                                                  (m_args ++ [DPlainTV tyfun_name]))
             app_decl    = DTySynInstD app_eqn
             suppress    = DInstanceD Nothing Nothing []
                             (DConT suppressClassName `DAppT` app_data_ty)
@@ -286,20 +285,18 @@ defunctionalize name m_fixity m_arg_tvbs' m_res_kind' = do
                                                        mkTupleDExp [DConE con_name,
                                                                     mkTupleDExp []])]]
 
-            mk_rhs'     = foldTypeTvbs (DConT data_name)
             -- See Note [Fixity declarations for defunctionalization symbols]
             fixity_decl = maybeToList $ fmap (mk_fix_decl data_name) m_fixity
 
-        decls <- go (n - 1) m_args m_tyfun mk_rhs'
+        decls <- go (n - 1) m_args m_tyfun
         return $ suppress : data_decl : app_decl : fixity_decl ++ decls
 
   let num_args       = length m_arg_tvbs
       sat_name       = promoteTySym name num_args
-      mk_rhs         = foldTypeTvbs (DConT name)
-      sat_dec        = DTySynD sat_name m_arg_tvbs (mk_rhs m_arg_tvbs)
+      sat_dec        = DTySynD sat_name m_arg_tvbs $ foldTypeTvbs (DConT name) m_arg_tvbs
       sat_fixity_dec = maybeToList $ fmap (mk_fix_decl sat_name) m_fixity
 
-  other_decs <- go (num_args - 1) (reverse m_arg_tvbs) m_res_kind mk_rhs
+  other_decs <- go (num_args - 1) (reverse m_arg_tvbs) m_res_kind
   return $ sat_dec : sat_fixity_dec ++ other_decs
   where
     eta_expand :: [DTyVarBndr] -> Maybe DKind -> PrM ([DTyVarBndr], Maybe DKind)

tests/compile-and-dump/GradingClient/Database.golden

@@ -17,7 +17,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
         SuccSym0KindInference :: forall t0123456789876543210
                                         arg. SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
                                  SuccSym0 t0123456789876543210
-    type instance Apply SuccSym0 t0123456789876543210 = Succ t0123456789876543210
+    type instance Apply SuccSym0 t0123456789876543210 = SuccSym1 t0123456789876543210
     type family Compare_0123456789876543210 (a :: Nat) (a :: Nat) :: Ordering where
       Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
       Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[])
@@ -34,7 +34,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                                                                a0123456789876543210
                                                                arg. SameKind (Apply (Compare_0123456789876543210Sym1 a0123456789876543210) arg) (Compare_0123456789876543210Sym2 a0123456789876543210 arg) =>
                                                         Compare_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
-    type instance Apply (Compare_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
+    type instance Apply (Compare_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
       suppressUnusedWarnings
         = snd (((,) Compare_0123456789876543210Sym0KindInference) ())
@@ -242,7 +242,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                                        t0123456789876543210
                                        arg. SameKind (Apply (VECSym1 t0123456789876543210) arg) (VECSym2 t0123456789876543210 arg) =>
                                 VECSym1 t0123456789876543210 t0123456789876543210
-    type instance Apply (VECSym1 t0123456789876543210) t0123456789876543210 = VEC t0123456789876543210 t0123456789876543210
+    type instance Apply (VECSym1 t0123456789876543210) t0123456789876543210 = VECSym2 t0123456789876543210 t0123456789876543210
     instance SuppressUnusedWarnings VECSym0 where
       suppressUnusedWarnings = snd (((,) VECSym0KindInference) ())
     data VECSym0 :: (~>) U ((~>) Nat U)
@@ -287,7 +287,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                                         t0123456789876543210
                                         arg. SameKind (Apply (AttrSym1 t0123456789876543210) arg) (AttrSym2 t0123456789876543210 arg) =>
                                  AttrSym1 t0123456789876543210 t0123456789876543210
-    type instance Apply (AttrSym1 t0123456789876543210) t0123456789876543210 = Attr t0123456789876543210 t0123456789876543210
+    type instance Apply (AttrSym1 t0123456789876543210) t0123456789876543210 = AttrSym2 t0123456789876543210 t0123456789876543210
     instance SuppressUnusedWarnings AttrSym0 where
       suppressUnusedWarnings = snd (((,) AttrSym0KindInference) ())
     data AttrSym0 :: (~>) [AChar] ((~>) U Attribute)
@@ -305,7 +305,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
         SchSym0KindInference :: forall t0123456789876543210
                                        arg. SameKind (Apply SchSym0 arg) (SchSym1 arg) =>
                                 SchSym0 t0123456789876543210
-    type instance Apply SchSym0 t0123456789876543210 = Sch t0123456789876543210
+    type instance Apply SchSym0 t0123456789876543210 = SchSym1 t0123456789876543210
     type Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 =
         Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
     instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym3 u0123456789876543210 name'0123456789876543210 name0123456789876543210) where
@@ -322,7 +322,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                                                                                        attrs0123456789876543210
                                                                                        arg. SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 arg) =>
                                                                                 Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
-    type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym3 u0123456789876543210 name'0123456789876543210 name0123456789876543210) attrs0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 u0123456789876543210 name'0123456789876543210 name0123456789876543210 attrs0123456789876543210
+    type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym3 u0123456789876543210 name'0123456789876543210 name0123456789876543210) attrs0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym4 u0123456789876543210 name'0123456789876543210 name0123456789876543210 attrs0123456789876543210
     instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name'0123456789876543210 name0123456789876543210) where
       suppressUnusedWarnings
         = snd
@@ -377,7 +377,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                                           a0123456789876543210
                                           arg. SameKind (Apply (LookupSym1 a0123456789876543210) arg) (LookupSym2 a0123456789876543210 arg) =>
                                    LookupSym1 a0123456789876543210 a0123456789876543210
-    type instance Apply (LookupSym1 a0123456789876543210) a0123456789876543210 = Lookup a0123456789876543210 a0123456789876543210
+    type instance Apply (LookupSym1 a0123456789876543210) a0123456789876543210 = LookupSym2 a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings LookupSym0 where
       suppressUnusedWarnings = snd (((,) LookupSym0KindInference) ())
     data LookupSym0 :: (~>) [AChar] ((~>) Schema U)
@@ -396,7 +396,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                                           a0123456789876543210
                                           arg. SameKind (Apply (OccursSym1 a0123456789876543210) arg) (OccursSym2 a0123456789876543210 arg) =>
                                    OccursSym1 a0123456789876543210 a0123456789876543210
-    type instance Apply (OccursSym1 a0123456789876543210) a0123456789876543210 = Occurs a0123456789876543210 a0123456789876543210
+    type instance Apply (OccursSym1 a0123456789876543210) a0123456789876543210 = OccursSym2 a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings OccursSym0 where
       suppressUnusedWarnings = snd (((,) OccursSym0KindInference) ())
     data OccursSym0 :: (~>) [AChar] ((~>) Schema Bool)
@@ -415,7 +415,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                                             a0123456789876543210
                                             arg. SameKind (Apply (DisjointSym1 a0123456789876543210) arg) (DisjointSym2 a0123456789876543210 arg) =>
                                      DisjointSym1 a0123456789876543210 a0123456789876543210
-    type instance Apply (DisjointSym1 a0123456789876543210) a0123456789876543210 = Disjoint a0123456789876543210 a0123456789876543210
+    type instance Apply (DisjointSym1 a0123456789876543210) a0123456789876543210 = DisjointSym2 a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings DisjointSym0 where
       suppressUnusedWarnings = snd (((,) DisjointSym0KindInference) ())
     data DisjointSym0 :: (~>) Schema ((~>) Schema Bool)
@@ -434,7 +434,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                                              a0123456789876543210
                                              arg. SameKind (Apply (AttrNotInSym1 a0123456789876543210) arg) (AttrNotInSym2 a0123456789876543210 arg) =>
                                       AttrNotInSym1 a0123456789876543210 a0123456789876543210
-    type instance Apply (AttrNotInSym1 a0123456789876543210) a0123456789876543210 = AttrNotIn a0123456789876543210 a0123456789876543210
+    type instance Apply (AttrNotInSym1 a0123456789876543210) a0123456789876543210 = AttrNotInSym2 a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings AttrNotInSym0 where
       suppressUnusedWarnings = snd (((,) AttrNotInSym0KindInference) ())
     data AttrNotInSym0 :: (~>) Attribute ((~>) Schema Bool)
@@ -453,7 +453,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                                           a0123456789876543210
                                           arg. SameKind (Apply (AppendSym1 a0123456789876543210) arg) (AppendSym2 a0123456789876543210 arg) =>
                                    AppendSym1 a0123456789876543210 a0123456789876543210
-    type instance Apply (AppendSym1 a0123456789876543210) a0123456789876543210 = Append a0123456789876543210 a0123456789876543210
+    type instance Apply (AppendSym1 a0123456789876543210) a0123456789876543210 = AppendSym2 a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings AppendSym0 where
       suppressUnusedWarnings = snd (((,) AppendSym0KindInference) ())
     data AppendSym0 :: (~>) Schema ((~>) Schema Schema)
@@ -493,7 +493,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                                                                  a0123456789876543210
                                                                  arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) =>
                                                           ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
-    type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
+    type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where
       suppressUnusedWarnings
         = snd (((,) ShowsPrec_0123456789876543210Sym1KindInference) ())
@@ -554,7 +554,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                                                                  a0123456789876543210
                                                                  arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) =>
                                                           ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
-    type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
+    type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where
       suppressUnusedWarnings
         = snd (((,) ShowsPrec_0123456789876543210Sym1KindInference) ())

tests/compile-and-dump/InsertionSort/InsertionSortImp.golden

@@ -12,7 +12,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
         SuccSym0KindInference :: forall t0123456789876543210
                                         arg. SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
                                  SuccSym0 t0123456789876543210
-    type instance Apply SuccSym0 t0123456789876543210 = Succ t0123456789876543210
+    type instance Apply SuccSym0 t0123456789876543210 = SuccSym1 t0123456789876543210
     data SNat :: Nat -> Type
       where
         SZero :: SNat (Zero :: Nat)
@@ -72,7 +72,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
                                                                                        t0123456789876543210
                                                                                        arg. SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 arg) =>
                                                                                 Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210 t0123456789876543210
-    type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 h0123456789876543210 n0123456789876543210) t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 h0123456789876543210 n0123456789876543210 t0123456789876543210
+    type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 h0123456789876543210 n0123456789876543210) t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym3 h0123456789876543210 n0123456789876543210 t0123456789876543210
     instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) where
       suppressUnusedWarnings
         = snd
@@ -113,7 +113,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
         InsertionSortSym0KindInference :: forall a0123456789876543210
                                                  arg. SameKind (Apply InsertionSortSym0 arg) (InsertionSortSym1 arg) =>
                                           InsertionSortSym0 a0123456789876543210
-    type instance Apply InsertionSortSym0 a0123456789876543210 = InsertionSort a0123456789876543210
+    type instance Apply InsertionSortSym0 a0123456789876543210 = InsertionSortSym1 a0123456789876543210
     type InsertSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: [Nat]) =
         Insert a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings (InsertSym1 a0123456789876543210) where
@@ -124,7 +124,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
                                           a0123456789876543210
                                           arg. SameKind (Apply (InsertSym1 a0123456789876543210) arg) (InsertSym2 a0123456789876543210 arg) =>
                                    InsertSym1 a0123456789876543210 a0123456789876543210
-    type instance Apply (InsertSym1 a0123456789876543210) a0123456789876543210 = Insert a0123456789876543210 a0123456789876543210
+    type instance Apply (InsertSym1 a0123456789876543210) a0123456789876543210 = InsertSym2 a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings InsertSym0 where
       suppressUnusedWarnings = snd (((,) InsertSym0KindInference) ())
     data InsertSym0 :: (~>) Nat ((~>) [Nat] [Nat])
@@ -143,7 +143,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
                                        a0123456789876543210
                                        arg. SameKind (Apply (LeqSym1 a0123456789876543210) arg) (LeqSym2 a0123456789876543210 arg) =>
                                 LeqSym1 a0123456789876543210 a0123456789876543210
-    type instance Apply (LeqSym1 a0123456789876543210) a0123456789876543210 = Leq a0123456789876543210 a0123456789876543210
+    type instance Apply (LeqSym1 a0123456789876543210) a0123456789876543210 = LeqSym2 a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings LeqSym0 where
       suppressUnusedWarnings = snd (((,) LeqSym0KindInference) ())
     data LeqSym0 :: (~>) Nat ((~>) Nat Bool)