Clean up some code smells in D.S.{Promote,Single}.Defun

While looking at the defunctionalization code recently, I discovered
several smelly aspects of the code. This patch does not fix all such
code smells (I plan to tackle more of them while tackling #378), but
this does pick some of the lower-hanging fruit. Here are the
highlights:

1. The `reverse` function is used an awful lot in
   `D.S.Promote.Defun.defunctionalize`. It's used here, when the
   inner loop (`go`) is first invoked:

   https://github.com/goldfirere/singletons/blob/2ec18435b8c57afcfcec0b7da872621b1179d45f/src/Data/Singletons/Promote/Defun.hs#L299

   And it's also used here, inside of `go` itself:

   https://github.com/goldfirere/singletons/blob/2ec18435b8c57afcfcec0b7da872621b1179d45f/src/Data/Singletons/Promote/Defun.hs#L237-L240

   This makes my head spin. Moreover, there other some parts of `go`
   that use `m_args` instead of using `reverse m_args`, which
   causes some odd-looking code to be generated (e.g., generating
   both `data BlahSym2 x y :: z ~> Type` _and_
   `type instance Apply (BlahSym2 y x) z = BlahSym3 y x z`). None of
   this is technially wrong, but I find it hard to follow.

   Luckily, we can get away without needing either use of `reverse`.
   Instead of processing a single list of `TyVarBndr`s in reverse
   order inside of `go`, we can track two lists of `TyVarBndr`s.
   To how this works, imagine we are to generate these
   defunctionalization symbols:

   ```hs
   data BlahSym0 :: x ~> y ~> z ~> Type
   data BlahSym1    x :: y ~> z ~> Type
   data BlahSym2    x    y :: z ~> Type
   ```

   We can accomplish this by "cycling" through the `TyVarBndr`s with
   two lists: one for the arguments and another for the result kind.
   Or, in code:

   ```hs
   []     [x, y, z] -- BlahSym0
   [x]       [y, z] -- BlahSym1
   [x, y]       [z] -- BlahSym2
   ```

   Notice that at each iteration of `go`, we take the first
   `TyVarBndr` from the second list and append it to the end of the
   first. This makes `go` run in quadratic time, but this is not a
   new precedent, since `go` was quadratic before due to invoking
   `reverse` in each iteration. Given the choice between these two
   quadratic-time designs, I prefer the new one. I've applied this
   refactor to the `go` functions in
   `D.S.Promote.Defun.defunctionalize` and
   `D.S.Single.Defun.singDefuns`, and left some comments explaining
   what is going on.
2. The inner loop of `D.S.Promote.Defun.defunctionalize` works by
   starting from `n - 1` (where `n` is the number of arguments) and
   iterating until `0` is reached. On the flip side, the inner loop
   of `D.S.Single.Defun.singDefuns` works by starting from `0` and
   iterating until `n - 1` is reached. For the sake of consistency,
   I have adopted the `singDefuns` convention (start from `0` and
   count up) for both pieces of code.
3. The inner loops of `D.S.Promote.Defun.defunctionalize` and
   `D.S.Single.Defun.singDefuns` are monadic, but they don't need to
   be. The only monadic things they do are generate unique names, but
   this can be done more easily outside of the inner loops
   themselves. This patch refactors the code to do just that, making
   the inner loop code pure.

A consequence of (2) is that `D.S.Promote.Defun.defunctionalize` now
generates defunctionalization symbols in the opposite order that it
used to. This causes many, many test cases to have different expected
output, making the patch appear larger than it actually is.

src/Data/Singletons/Promote/Defun.hs

@@ -215,6 +215,7 @@ defunctionalize :: Name
 defunctionalize name m_fixity m_arg_tvbs' m_res_kind' = do
   (m_arg_tvbs, m_res_kind) <- eta_expand (noExactTyVars m_arg_tvbs')
                                          (noExactTyVars m_res_kind')
+  extra_name <- qNewName "arg"
 
   let -- Implements part (2)(i) from Note [Defunctionalization and dependent quantification]
       tvb_to_type_map :: Map Name DType
@@ -224,20 +225,52 @@ defunctionalize name m_fixity m_arg_tvbs' m_res_kind' = do
                         map dTyVarBndrToDType m_arg_tvbs
                           ++ maybeToList m_res_kind      -- (2)(i)(a)
 
-      go :: Int -> [DTyVarBndr] -> Maybe DKind
-         -> PrM [DDec]
-      go _ [] _ = return []
-      go n (m_arg : m_args) m_result = do
-        extra_name <- qNewName "arg"
-        let tyfun_name  = extractTvbName m_arg
+      -- The inner loop. @go n arg_tvbs res_tvbs@ returns @(m_result, decls)@.
+      -- Using one particular example:
+      --
+      -- @
+      -- data ExampleSym2 (x :: a) (y :: b) :: c ~> d ~> Type where ...
+      -- type instance Apply (ExampleSym2 x y) z = ExampleSym3 x y z
+      -- ...
+      -- @
+      --
+      -- We have:
+      --
+      -- * @n@ is 2. This is incremented in each iteration of `go`.
+      --
+      -- * @arg_tvbs@ is [(x :: a), (y :: b)].
+      --
+      -- * @res_tvbs@ is [(z :: c), (w :: d)]. The kinds of these type variable
+      --   binders appear in the result kind.
+      --
+      -- * @m_result@ is `Just (c ~> d ~> Type)`. @m_result@ is returned so
+      --   that earlier defunctionalization symbols can build on the result
+      --   kinds of later symbols. For instance, ExampleSym1 would get the
+      --   result kind `b ~> c ~> d ~> Type` by prepending `b` to ExampleSym2's
+      --   result kind `c ~> d ~> Type`.
+      --
+      -- * @decls@ are all of the declarations corresponding to ExampleSym2
+      --   and later defunctionalization symbols. This is the main payload of
+      --   the function.
+      --
+      -- This function is quadratic because it appends a variable at the end of
+      -- the @arg_tvbs@ list at each iteration. In practice, this is unlikely
+      -- to be a performance bottleneck since the number of arguments rarely
+      -- gets to be that large.
+      go :: Int -> [DTyVarBndr] -> [DTyVarBndr]
+         -> (Maybe DKind, [DDec])
+      go _ _        []                 = (m_res_kind, [])
+      go n arg_tvbs (res_tvb:res_tvbs) =
+        let (m_result, decls) = go (n+1) (arg_tvbs ++ [res_tvb]) res_tvbs
+
+            tyfun_name  = extractTvbName res_tvb
             data_name   = promoteTySym name n
             next_name   = promoteTySym name (n+1)
             con_name    = prefixName "" ":" $ suffixName "KindInference" "###" data_name
-            m_tyfun     = buildTyFunArrow_maybe (extractTvbKind m_arg) m_result
+            m_tyfun     = buildTyFunArrow_maybe (extractTvbKind res_tvb) m_result
             arg_params  = -- Implements part (2)(ii) from
                           -- Note [Defunctionalization and dependent quantification]
-                          map (map_tvb_kind (substType tvb_to_type_map)) $
-                          reverse m_args
+                          map (map_tvb_kind (substType tvb_to_type_map)) arg_tvbs
             arg_names   = map extractTvbName arg_params
             params      = arg_params ++ [DPlainTV tyfun_name]
             con_eq_ct   = DConT sameKindName `DAppT` lhs `DAppT` rhs
@@ -270,12 +303,12 @@ defunctionalize name m_fixity m_arg_tvbs' m_res_kind' = do
                                          map tvb_to_type $      -- (2)(iii)(b)
                                          toList $ fvDType tyfun -- (2)(iii)(a)
                         in (arg_params, Just (DForallT ForallInvis tyfun_tvbs tyfun))
-            app_data_ty = foldTypeTvbs (DConT data_name) m_args
+            app_data_ty = foldTypeTvbs (DConT data_name) arg_tvbs
             app_eqn     = DTySynEqn Nothing
                                     (DConT applyName `DAppT` app_data_ty
                                                      `DAppT` DVarT tyfun_name)
                                     (foldTypeTvbs (DConT next_name)
-                                                  (m_args ++ [DPlainTV tyfun_name]))
+                                                  (arg_tvbs ++ [DPlainTV tyfun_name]))
             app_decl    = DTySynInstD app_eqn
             suppress    = DInstanceD Nothing Nothing []
                             (DConT suppressClassName `DAppT` app_data_ty)
@@ -287,17 +320,15 @@ defunctionalize name m_fixity m_arg_tvbs' m_res_kind' = do
 
             -- 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
-        return $ suppress : data_decl : app_decl : fixity_decl ++ decls
+        in (m_tyfun, suppress : data_decl : app_decl : fixity_decl ++ decls)
 
   let num_args       = length m_arg_tvbs
       sat_name       = promoteTySym name num_args
       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
-  return $ sat_dec : sat_fixity_dec ++ other_decs
+      (_, other_decs) = go 0 [] m_arg_tvbs
+  return $ other_decs ++ sat_dec : sat_fixity_dec
   where
     eta_expand :: [DTyVarBndr] -> Maybe DKind -> PrM ([DTyVarBndr], Maybe DKind)
     eta_expand m_arg_tvbs Nothing = pure (m_arg_tvbs, Nothing)

src/Data/Singletons/Single/Defun.hs

@@ -13,6 +13,7 @@
 
 module Data.Singletons.Single.Defun (singDefuns) where
 
+import Control.Monad
 import Data.List
 import Data.Singletons.Names
 import Data.Singletons.Promote.Defun
@@ -57,71 +58,101 @@ singDefuns n ns ty_ctxt mb_ty_args mb_ty_res =
     [] -> pure [] -- If a function has no arguments, then it has no
                   -- defunctionalization symbols, so there's nothing to be done.
     _  -> do sty_ctxt <- mapM singPred ty_ctxt
-             go 0 sty_ctxt [] mb_ty_args
+             names    <- replicateM (length mb_ty_args) $ qNewName "d"
+             let tvbs       = zipWith inferMaybeKindTV names mb_ty_args
+                 (_, insts) = go 0 sty_ctxt [] tvbs
+             pure insts
   where
     num_ty_args :: Int
     num_ty_args = length mb_ty_args
 
-    -- Sadly, this algorithm is quadratic, because in each iteration of the loop
-    -- we must:
+    -- The inner loop. @go n ctxt arg_tvbs res_tvbs@ returns @(m_result, insts)@.
+    -- Using one particular example:
     --
-    -- * Construct an arrow type of the form (a ~> ... ~> z), using a suffix of
-    --   the promoted argument types.
-    -- * Append a new type variable to the end of an ordered list.
+    -- @
+    -- instance (SingI a, SingI b, SEq c, SEq d) =>
+    --   SingI (ExampleSym2 (x :: a) (y :: b) :: c ~> d ~> Type) where ...
+    -- @
     --
-    -- In practice, this is unlikely to be a bottleneck, as singletons does not
-    -- support functions with more than 7 or so arguments anyways.
-    go :: Int -> DCxt -> [DTyVarBndr] -> [Maybe DKind] -> SgM [DDec]
-    go sym_num sty_ctxt tvbs mb_tyss
-      | sym_num < num_ty_args
-      , mb_ty:mb_tys <- mb_tyss
-      = do new_tvb_name <- qNewName "d"
-           let new_tvb = inferMaybeKindTV new_tvb_name mb_ty
-           insts <- go (sym_num + 1) sty_ctxt (tvbs ++ [new_tvb]) mb_tys
-           pure $ new_insts ++ insts
-      | otherwise
-      = pure []
+    -- We have:
+    --
+    -- * @n@ is 2. This is incremented in each iteration of `go`.
+    --
+    -- * @ctxt@ is (SEq c, SEq d). The (SingI a, SingI b) part of the instance
+    --   context is added separately.
+    --
+    -- * @arg_tvbs@ is [(x :: a), (y :: b)].
+    --
+    -- * @res_tvbs@ is [(z :: c), (w :: d)]. The kinds of these type variable
+    --   binders appear in the result kind.
+    --
+    -- * @m_result@ is `Just (c ~> d ~> Type)`. @m_result@ is returned so
+    --   that earlier defunctionalization symbols can build on the result
+    --   kinds of later symbols. For instance, ExampleSym1 would get the
+    --   result kind `b ~> c ~> d ~> Type` by prepending `b` to ExampleSym2's
+    --   result kind `c ~> d ~> Type`.
+    --
+    -- * @insts@ are all of the instance declarations corresponding to
+    --   ExampleSym2 and later defunctionalization symbols. This is the main
+    --   payload of the function.
+    --
+    -- This function is quadratic because it appends a variable at the end of
+    -- the @arg_tvbs@ list at each iteration. In practice, this is unlikely
+    -- to be a performance bottleneck since the number of arguments rarely
+    -- gets to be that large.
+    go :: Int -> DCxt -> [DTyVarBndr] -> [DTyVarBndr]
+       -> (Maybe DKind, [DDec])
+    go _       _        _        []                 = (mb_ty_res, [])
+    go sym_num sty_ctxt arg_tvbs (res_tvb:res_tvbs) =
+      (mb_new_res, new_inst:insts)
       where
+        mb_res :: Maybe DKind
+        insts  :: [DDec]
+        (mb_res, insts) = go (sym_num + 1) sty_ctxt (arg_tvbs ++ [res_tvb]) res_tvbs
+
+        mb_new_res :: Maybe DKind
+        mb_new_res = mk_inst_kind res_tvb mb_res
+
         sing_fun_num :: Int
         sing_fun_num = num_ty_args - sym_num
 
         mk_sing_fun_expr :: DExp -> DExp
         mk_sing_fun_expr sing_expr =
           foldl' (\f tvb_n -> f `DAppE` (DVarE singMethName `DAppTypeE` DVarT tvb_n))
                  sing_expr
-                 (map extractTvbName tvbs)
+                 (map extractTvbName arg_tvbs)
 
         singI_ctxt :: DCxt
-        singI_ctxt = map (DAppT (DConT singIName) . tvbToType) tvbs
+        singI_ctxt = map (DAppT (DConT singIName) . tvbToType) arg_tvbs
 
         mk_inst_ty :: DType -> DType
         mk_inst_ty inst_head
-          = case mb_inst_kind of
+          = case mb_new_res of
               Just inst_kind -> inst_head `DSigT` inst_kind
               Nothing        -> inst_head
 
-        tvb_tys :: [DType]
-        tvb_tys = map dTyVarBndrToDType tvbs
+        arg_tvb_tys :: [DType]
+        arg_tvb_tys = map dTyVarBndrToDType arg_tvbs
 
         -- Construct the arrow kind used to annotate the defunctionalization
         -- symbol (e.g., the `a ~> a ~> Bool` in
         -- `SingI (FooSym0 :: a ~> a ~> Bool)`).
         -- If any of the argument kinds or result kind isn't known (i.e., is
         -- Nothing), then we opt not to construct this arrow kind altogether.
         -- See Note [singDefuns and type inference]
-        mb_inst_kind :: Maybe DType
-        mb_inst_kind = foldr buildTyFunArrow_maybe mb_ty_res mb_tyss
-
-        new_insts :: [DDec]
-        new_insts = [DInstanceD Nothing Nothing
-                                (sty_ctxt ++ singI_ctxt)
-                                (DConT singIName `DAppT` mk_inst_ty defun_inst_ty)
-                                [DLetDec $ DValD (DVarP singMethName)
-                                         $ wrapSingFun sing_fun_num defun_inst_ty
-                                         $ mk_sing_fun_expr sing_exp ]]
+        mk_inst_kind :: DTyVarBndr -> Maybe DKind -> Maybe DKind
+        mk_inst_kind tvb' = buildTyFunArrow_maybe (extractTvbKind tvb')
+
+        new_inst :: DDec
+        new_inst = DInstanceD Nothing Nothing
+                              (sty_ctxt ++ singI_ctxt)
+                              (DConT singIName `DAppT` mk_inst_ty defun_inst_ty)
+                              [DLetDec $ DValD (DVarP singMethName)
+                                       $ wrapSingFun sing_fun_num defun_inst_ty
+                                       $ mk_sing_fun_expr sing_exp ]
           where
             defun_inst_ty :: DType
-            defun_inst_ty = foldType (DConT (promoteTySym n sym_num)) tvb_tys
+            defun_inst_ty = foldType (DConT (promoteTySym n sym_num)) arg_tvb_tys
 
             sing_exp :: DExp
             sing_exp = case ns of