Don't use defunctionalization when singling return types of type sign…

…atures

As noted in #608, you don't need to involve defunctionalization when promoting
class method defaults, as we always know that the promoted versions of the
defaults will be fully applied to all their arguments. In fact, there is
another situation in which we always know that a promoted type family will be
fully applied: the return type of a singled type signature. That it, if you
single this definition:

```hs
f :: a -> b -> a
```

You currently get this:

```hs
sF :: forall a b (x :: a) (y :: b).
      Sing x -> Sing y -> Sing (FSym0 `Apply` x `Apply` y)
```

But using `FSym0` in the return type of `sF` is silly, however, as we always
know that it will be fully applied to its arguments (`x` and `y`). As such, it
would be far more direct to instead generate the following:

```hs
sF :: forall a b (x :: a) (y :: b).
      Sing x -> Sing y -> Sing (F x y)
```

No defunctionalization required at all. This doesn't change the behavior of the
singled code at all, but it is more direct and will likely require less time to
typecheck due to fewer type family indirections being involved.

To accomplish this, the `lde_proms` field now maps term-level names to
`LetDecProm`s, where a `LetDecProm` consists of the promoted version of the
name and the local variables that it closes over. In this context, "promoted
version" means `F`, _not_ `FSym0`. Storing the non-defunctionalized name allows
us to fully apply `F` whenever it is convenient to do so, and in situations
where partial application may be required, we can always convert `F` to `FSym0`
before generating the partial application.

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

@@ -1216,33 +1216,27 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
       type (==) a a = TFHelper_0123456789876543210 a a
     sLookup ::
       (forall (t :: [AChar]) (t :: Schema).
-       Sing t
-       -> Sing t -> Sing (Apply (Apply LookupSym0 t) t :: U) :: Type)
+       Sing t -> Sing t -> Sing (Lookup t t :: U) :: Type)
     sOccurs ::
       (forall (t :: [AChar]) (t :: Schema).
-       Sing t
-       -> Sing t -> Sing (Apply (Apply OccursSym0 t) t :: Bool) :: Type)
+       Sing t -> Sing t -> Sing (Occurs t t :: Bool) :: Type)
     sDisjoint ::
       (forall (t :: Schema) (t :: Schema).
-       Sing t
-       -> Sing t -> Sing (Apply (Apply DisjointSym0 t) t :: Bool) :: Type)
+       Sing t -> Sing t -> Sing (Disjoint t t :: Bool) :: Type)
     sAttrNotIn ::
       (forall (t :: Attribute) (t :: Schema).
-       Sing t
-       -> Sing t
-          -> Sing (Apply (Apply AttrNotInSym0 t) t :: Bool) :: Type)
+       Sing t -> Sing t -> Sing (AttrNotIn t t :: Bool) :: Type)
     sAppend ::
       (forall (t :: Schema) (t :: Schema).
-       Sing t
-       -> Sing t -> Sing (Apply (Apply AppendSym0 t) t :: Schema) :: Type)
+       Sing t -> Sing t -> Sing (Append t t :: Schema) :: Type)
     sLookup _ (SSch SNil) = sUndefined
     sLookup
       (sName :: Sing name)
       (SSch (SCons (SAttr (sName' :: Sing name') (sU :: Sing u))
                    (sAttrs :: Sing attrs)))
       = let
           sScrutinee_0123456789876543210 ::
-            Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym0 name name' u attrs)
+            Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210 name name' u attrs)
           sScrutinee_0123456789876543210
             = applySing (applySing (singFun2 @(==@#@$) (%==)) sName) sName'
         in

singletons-base/tests/compile-and-dump/GradingClient/Main.golden

@@ -73,13 +73,13 @@ GradingClient/Main.hs:(0,0)-(0,0): Splicing declarations
     type LastName :: [AChar]
     type family LastName :: [AChar] where
       LastName = Apply (Apply (:@#@$) CLSym0) (Apply (Apply (:@#@$) CASym0) (Apply (Apply (:@#@$) CSSym0) (Apply (Apply (:@#@$) CTSym0) NilSym0)))
-    sNames :: (Sing (NamesSym0 :: Schema) :: Type)
-    sGradingSchema :: (Sing (GradingSchemaSym0 :: Schema) :: Type)
-    sMajorName :: (Sing (MajorNameSym0 :: [AChar]) :: Type)
-    sGradeName :: (Sing (GradeNameSym0 :: [AChar]) :: Type)
-    sYearName :: (Sing (YearNameSym0 :: [AChar]) :: Type)
-    sFirstName :: (Sing (FirstNameSym0 :: [AChar]) :: Type)
-    sLastName :: (Sing (LastNameSym0 :: [AChar]) :: Type)
+    sNames :: (Sing (Names :: Schema) :: Type)
+    sGradingSchema :: (Sing (GradingSchema :: Schema) :: Type)
+    sMajorName :: (Sing (MajorName :: [AChar]) :: Type)
+    sGradeName :: (Sing (GradeName :: [AChar]) :: Type)
+    sYearName :: (Sing (YearName :: [AChar]) :: Type)
+    sFirstName :: (Sing (FirstName :: [AChar]) :: Type)
+    sLastName :: (Sing (LastName :: [AChar]) :: Type)
     sNames
       = applySing
           (singFun1 @SchSym0 SSch)

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

@@ -133,15 +133,13 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
       Leq ('Succ a) ('Succ b) = Apply (Apply LeqSym0 a) b
     sInsertionSort ::
       (forall (t :: [Nat]).
-       Sing t -> Sing (Apply InsertionSortSym0 t :: [Nat]) :: Type)
+       Sing t -> Sing (InsertionSort t :: [Nat]) :: Type)
     sInsert ::
       (forall (t :: Nat) (t :: [Nat]).
-       Sing t
-       -> Sing t -> Sing (Apply (Apply InsertSym0 t) t :: [Nat]) :: Type)
+       Sing t -> Sing t -> Sing (Insert t t :: [Nat]) :: Type)
     sLeq ::
       (forall (t :: Nat) (t :: Nat).
-       Sing t
-       -> Sing t -> Sing (Apply (Apply LeqSym0 t) t :: Bool) :: Type)
+       Sing t -> Sing t -> Sing (Leq t t :: Bool) :: Type)
     sInsertionSort SNil = SNil
     sInsertionSort (SCons (sH :: Sing h) (sT :: Sing t))
       = applySing
@@ -152,7 +150,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
     sInsert (sN :: Sing n) (SCons (sH :: Sing h) (sT :: Sing t))
       = let
           sScrutinee_0123456789876543210 ::
-            Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym0 n h t)
+            Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210 n h t)
           sScrutinee_0123456789876543210
             = applySing (applySing (singFun2 @LeqSym0 sLeq) sN) sH
         in

singletons-base/tests/compile-and-dump/Singletons/AsPattern.golden

@@ -172,31 +172,29 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
       MaybePlus ('Just n) = Apply JustSym0 (Apply (Apply PlusSym0 (Apply SuccSym0 ZeroSym0)) n)
       MaybePlus 'Nothing = Let0123456789876543210PSym0
     sFoo ::
-      (forall (t :: [Nat]).
-       Sing t -> Sing (Apply FooSym0 t :: [Nat]) :: Type)
+      (forall (t :: [Nat]). Sing t -> Sing (Foo t :: [Nat]) :: Type)
     sTup ::
       (forall (t :: (Nat, Nat)).
-       Sing t -> Sing (Apply TupSym0 t :: (Nat, Nat)) :: Type)
+       Sing t -> Sing (Tup t :: (Nat, Nat)) :: Type)
     sBaz_ ::
       (forall (t :: Maybe Baz).
-       Sing t -> Sing (Apply Baz_Sym0 t :: Maybe Baz) :: Type)
+       Sing t -> Sing (Baz_ t :: Maybe Baz) :: Type)
     sBar ::
       (forall (t :: Maybe Nat).
-       Sing t -> Sing (Apply BarSym0 t :: Maybe Nat) :: Type)
+       Sing t -> Sing (Bar t :: Maybe Nat) :: Type)
     sMaybePlus ::
       (forall (t :: Maybe Nat).
-       Sing t -> Sing (Apply MaybePlusSym0 t :: Maybe Nat) :: Type)
+       Sing t -> Sing (MaybePlus t :: Maybe Nat) :: Type)
     sFoo SNil
       = let
-          sP :: Sing @_ Let0123456789876543210PSym0
+          sP :: Sing @_ Let0123456789876543210P
           sP = SNil
         in sP
     sFoo
       (SCons (sWild_0123456789876543210 :: Sing wild_0123456789876543210)
              SNil)
       = let
-          sP ::
-            Sing @_ (Let0123456789876543210PSym0 wild_0123456789876543210)
+          sP :: Sing @_ (Let0123456789876543210P wild_0123456789876543210)
           sP
             = applySing
                 (applySing (singFun2 @(:@#@$) SCons) sWild_0123456789876543210)
@@ -208,7 +206,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
                     (sWild_0123456789876543210 :: Sing wild_0123456789876543210)))
       = let
           sP ::
-            Sing @_ (Let0123456789876543210PSym0 wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210)
+            Sing @_ (Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210)
           sP
             = applySing
                 (applySing (singFun2 @(:@#@$) SCons) sWild_0123456789876543210)
@@ -221,7 +219,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
                (sWild_0123456789876543210 :: Sing wild_0123456789876543210))
       = let
           sP ::
-            Sing @_ (Let0123456789876543210PSym0 wild_0123456789876543210 wild_0123456789876543210)
+            Sing @_ (Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210)
           sP
             = applySing
                 (applySing
@@ -230,7 +228,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
         in sP
     sBaz_ SNothing
       = let
-          sP :: Sing @_ Let0123456789876543210PSym0
+          sP :: Sing @_ Let0123456789876543210P
           sP = SNothing
         in sP
     sBaz_
@@ -239,7 +237,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
                    (sWild_0123456789876543210 :: Sing wild_0123456789876543210)))
       = let
           sP ::
-            Sing @_ (Let0123456789876543210PSym0 wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210)
+            Sing @_ (Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210)
           sP
             = applySing
                 (singFun1 @JustSym0 SJust)
@@ -252,8 +250,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
     sBar
       (SJust (sWild_0123456789876543210 :: Sing wild_0123456789876543210))
       = let
-          sX ::
-            Sing @_ (Let0123456789876543210XSym0 wild_0123456789876543210)
+          sX :: Sing @_ (Let0123456789876543210X wild_0123456789876543210)
           sX = applySing (singFun1 @JustSym0 SJust) sWild_0123456789876543210
         in sX
     sBar SNothing = SNothing
@@ -267,7 +264,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
              sN)
     sMaybePlus SNothing
       = let
-          sP :: Sing @_ Let0123456789876543210PSym0
+          sP :: Sing @_ Let0123456789876543210P
           sP = SNothing
         in sP
     instance SingI (FooSym0 :: (~>) [Nat] [Nat]) where

singletons-base/tests/compile-and-dump/Singletons/BoxUnBox.golden

@@ -34,8 +34,7 @@ Singletons/BoxUnBox.hs:(0,0)-(0,0): Splicing declarations
     type family UnBox @a (a :: Box a) :: a where
       UnBox (FBox a) = a
     sUnBox ::
-      (forall (t :: Box a).
-       Sing t -> Sing (Apply UnBoxSym0 t :: a) :: Type)
+      (forall (t :: Box a). Sing t -> Sing (UnBox t :: a) :: Type)
     sUnBox (SFBox (sA :: Sing a)) = sA
     instance SingI (UnBoxSym0 :: (~>) (Box a) a) where
       sing = singFun1 @UnBoxSym0 sUnBox

singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden

@@ -168,18 +168,17 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations
     type Foo1 :: a -> Maybe a -> a
     type family Foo1 @a (a :: a) (a :: Maybe a) :: a where
       Foo1 d x = Case_0123456789876543210 d x x
-    sFoo5 ::
-      (forall (t :: a). Sing t -> Sing (Apply Foo5Sym0 t :: a) :: Type)
-    sFoo4 :: forall a (t :: a). Sing t -> Sing (Apply Foo4Sym0 t :: a)
+    sFoo5 :: (forall (t :: a). Sing t -> Sing (Foo5 t :: a) :: Type)
+    sFoo4 :: forall a (t :: a). Sing t -> Sing (Foo4 t :: a)
     sFoo3 ::
       (forall (t :: a) (t :: b).
-       Sing t -> Sing t -> Sing (Apply (Apply Foo3Sym0 t) t :: a) :: Type)
+       Sing t -> Sing t -> Sing (Foo3 t t :: a) :: Type)
     sFoo2 ::
       (forall (t :: a) (t :: Maybe a).
-       Sing t -> Sing t -> Sing (Apply (Apply Foo2Sym0 t) t :: a) :: Type)
+       Sing t -> Sing t -> Sing (Foo2 t t :: a) :: Type)
     sFoo1 ::
       (forall (t :: a) (t :: Maybe a).
-       Sing t -> Sing t -> Sing (Apply (Apply Foo1Sym0 t) t :: a) :: Type)
+       Sing t -> Sing t -> Sing (Foo1 t t :: a) :: Type)
     sFoo5 (sX :: Sing x)
       = id
           @(Sing (Case_0123456789876543210 x x))
@@ -201,13 +200,13 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations
           (case sX of
              (sY :: Sing y)
                -> let
-                    sZ :: (Sing (Let0123456789876543210ZSym0 a y x :: a) :: Type)
+                    sZ :: (Sing (Let0123456789876543210Z a y x :: a) :: Type)
                     sZ = sY
                   in sZ)
     sFoo3 (sA :: Sing a) (sB :: Sing b)
       = let
           sScrutinee_0123456789876543210 ::
-            Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym0 a b)
+            Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210 a b)
           sScrutinee_0123456789876543210
             = applySing (applySing (singFun2 @Tuple2Sym0 STuple2) sA) sB
         in
@@ -218,7 +217,7 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations
     sFoo2 (sD :: Sing d) _
       = let
           sScrutinee_0123456789876543210 ::
-            Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym0 d)
+            Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210 d)
           sScrutinee_0123456789876543210
             = applySing (singFun1 @JustSym0 SJust) sD
         in

singletons-base/tests/compile-and-dump/Singletons/Classes.golden

@@ -194,13 +194,10 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
       type (==) a a = TFHelper_0123456789876543210 a a
     sFooCompare ::
       (forall (t :: Foo) (t :: Foo).
-       Sing t
-       -> Sing t
-          -> Sing (Apply (Apply FooCompareSym0 t) t :: Ordering) :: Type)
+       Sing t -> Sing t -> Sing (FooCompare t t :: Ordering) :: Type)
     sConst ::
       (forall (t :: a) (t :: b).
-       Sing t
-       -> Sing t -> Sing (Apply (Apply ConstSym0 t) t :: a) :: Type)
+       Sing t -> Sing t -> Sing (Const t t :: a) :: Type)
     sFooCompare SA SA = SEQ
     sFooCompare SA SB = SLT
     sFooCompare SB SB = SGT
@@ -247,21 +244,15 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
     class SMyOrd a where
       sMycompare ::
         (forall (t :: a) (t :: a).
-         Sing t
-         -> Sing t
-            -> Sing (Apply (Apply MycompareSym0 t) t :: Ordering) :: Type)
+         Sing t -> Sing t -> Sing (Mycompare t t :: Ordering) :: Type)
       (%<=>) ::
         (forall (t :: a) (t :: a).
-         Sing t
-         -> Sing t
-            -> Sing (Apply (Apply (<=>@#@$) t) t :: Ordering) :: Type)
+         Sing t -> Sing t -> Sing ((<=>) t t :: Ordering) :: Type)
       infix 4 %<=>
       default (%<=>) ::
                 (forall (t :: a) (t :: a).
                  (((<=>) t t :: Ordering) ~ TFHelper_0123456789876543210 t t) =>
-                 Sing t
-                 -> Sing t
-                    -> Sing (Apply (Apply (<=>@#@$) t) t :: Ordering) :: Type)
+                 Sing t -> Sing t -> Sing ((<=>) t t :: Ordering) :: Type)
       (%<=>)
         (sA_0123456789876543210 :: Sing a_0123456789876543210)
         (sA_0123456789876543210 :: Sing a_0123456789876543210)

singletons-base/tests/compile-and-dump/Singletons/Contains.golden

@@ -32,9 +32,7 @@ Singletons/Contains.hs:(0,0)-(0,0): Splicing declarations
       Contains elt ('(:) h t) = Apply (Apply (||@#@$) (Apply (Apply (==@#@$) elt) h)) (Apply (Apply ContainsSym0 elt) t)
     sContains ::
       (forall (t :: a) (t :: [a]).
-       SEq a =>
-       Sing t
-       -> Sing t -> Sing (Apply (Apply ContainsSym0 t) t :: Bool) :: Type)
+       SEq a => Sing t -> Sing t -> Sing (Contains t t :: Bool) :: Type)
     sContains _ SNil = SFalse
     sContains (sElt :: Sing elt) (SCons (sH :: Sing h) (sT :: Sing t))
       = applySing

singletons-base/tests/compile-and-dump/Singletons/DataValues.golden

@@ -58,10 +58,10 @@ Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations
       ShowsPrec_0123456789876543210 @a @b (p_0123456789876543210 :: GHC.Num.Natural.Natural) (Pair arg_0123456789876543210 arg_0123456789876543210 :: Pair a b) (a_0123456789876543210 :: Symbol) = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Pair ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210
     instance PShow (Pair a b) where
       type ShowsPrec a a a = ShowsPrec_0123456789876543210 a a a
-    sAList :: Sing @_ AListSym0
-    sTuple :: Sing @_ TupleSym0
-    sComplex :: Sing @_ ComplexSym0
-    sPr :: Sing @_ PrSym0
+    sAList :: Sing @_ AList
+    sTuple :: Sing @_ Tuple
+    sComplex :: Sing @_ Complex
+    sPr :: Sing @_ Pr
     sAList
       = applySing
           (applySing (singFun2 @(:@#@$) SCons) SZero)

singletons-base/tests/compile-and-dump/Singletons/Error.golden

@@ -22,8 +22,7 @@ Singletons/Error.hs:(0,0)-(0,0): Splicing declarations
     type family Head @a (a :: [a]) :: a where
       Head ('(:) a _) = a
       Head '[] = Apply ErrorSym0 "head: empty list"
-    sHead ::
-      (forall (t :: [a]). Sing t -> Sing (Apply HeadSym0 t :: a) :: Type)
+    sHead :: (forall (t :: [a]). Sing t -> Sing (Head t :: a) :: Type)
     sHead (SCons (sA :: Sing a) _) = sA
     sHead SNil
       = applySing

singletons-base/tests/compile-and-dump/Singletons/Fixity.golden

@@ -67,8 +67,7 @@ Singletons/Fixity.hs:(0,0)-(0,0): Splicing declarations
     infix 4 %====
     (%====) ::
       (forall (t :: a) (t :: a).
-       Sing t
-       -> Sing t -> Sing (Apply (Apply (====@#@$) t) t :: a) :: Type)
+       Sing t -> Sing t -> Sing ((====) t t :: a) :: Type)
     (%====) (sA :: Sing a) _ = sA
     instance SingI ((====@#@$) :: (~>) a ((~>) a a)) where
       sing = singFun2 @(====@#@$) (%====)
@@ -80,9 +79,7 @@ Singletons/Fixity.hs:(0,0)-(0,0): Splicing declarations
     class SMyOrd a where
       (%<=>) ::
         (forall (t :: a) (t :: a).
-         Sing t
-         -> Sing t
-            -> Sing (Apply (Apply (<=>@#@$) t) t :: Ordering) :: Type)
+         Sing t -> Sing t -> Sing ((<=>) t t :: Ordering) :: Type)
       infix 4 %<=>
     instance SMyOrd a =>
              SingI ((<=>@#@$) :: (~>) a ((~>) a Ordering)) where

singletons-base/tests/compile-and-dump/Singletons/FunDeps.golden

@@ -58,13 +58,11 @@ Singletons/FunDeps.hs:(0,0)-(0,0): Splicing declarations
     instance PFD Bool Natural where
       type Meth a = Meth_0123456789876543210 a
       type L2r a = L2r_0123456789876543210 a
-    sT1 :: Sing @_ T1Sym0
+    sT1 :: Sing @_ T1
     sT1 = applySing (singFun1 @MethSym0 sMeth) STrue
     class SFD a b | a -> b where
-      sMeth ::
-        (forall (t :: a). Sing t -> Sing (Apply MethSym0 t :: a) :: Type)
-      sL2r ::
-        (forall (t :: a). Sing t -> Sing (Apply L2rSym0 t :: b) :: Type)
+      sMeth :: (forall (t :: a). Sing t -> Sing (Meth t :: a) :: Type)
+      sL2r :: (forall (t :: a). Sing t -> Sing (L2r t :: b) :: Type)
     instance SFD Bool Natural where
       sMeth (sA_0123456789876543210 :: Sing a_0123456789876543210)
         = applySing (singFun1 @NotSym0 sNot) sA_0123456789876543210

singletons-base/tests/compile-and-dump/Singletons/HigherOrder.golden

@@ -264,33 +264,22 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations
       Map f ('(:) h t) = Apply (Apply (:@#@$) (Apply f h)) (Apply (Apply MapSym0 f) t)
     sEtad ::
       (forall (t :: [Nat]) (t :: [Bool]).
-       Sing t
-       -> Sing t -> Sing (Apply (Apply EtadSym0 t) t :: [Nat]) :: Type)
+       Sing t -> Sing t -> Sing (Etad t t :: [Nat]) :: Type)
     sSplunge ::
       (forall (t :: [Nat]) (t :: [Bool]).
-       Sing t
-       -> Sing t -> Sing (Apply (Apply SplungeSym0 t) t :: [Nat]) :: Type)
+       Sing t -> Sing t -> Sing (Splunge t t :: [Nat]) :: Type)
     sFoo ::
       (forall (t :: (~>) ((~>) a b) ((~>) a b)) (t :: (~>) a b) (t :: a).
-       Sing t
-       -> Sing t
-          -> Sing t
-             -> Sing (Apply (Apply (Apply FooSym0 t) t) t :: b) :: Type)
+       Sing t -> Sing t -> Sing t -> Sing (Foo t t t :: b) :: Type)
     sZipWith ::
       (forall (t :: (~>) a ((~>) b c)) (t :: [a]) (t :: [b]).
-       Sing t
-       -> Sing t
-          -> Sing t
-             -> Sing (Apply (Apply (Apply ZipWithSym0 t) t) t :: [c]) :: Type)
+       Sing t -> Sing t -> Sing t -> Sing (ZipWith t t t :: [c]) :: Type)
     sLiftMaybe ::
       (forall (t :: (~>) a b) (t :: Maybe a).
-       Sing t
-       -> Sing t
-          -> Sing (Apply (Apply LiftMaybeSym0 t) t :: Maybe b) :: Type)
+       Sing t -> Sing t -> Sing (LiftMaybe t t :: Maybe b) :: Type)
     sMap ::
       (forall (t :: (~>) a b) (t :: [a]).
-       Sing t
-       -> Sing t -> Sing (Apply (Apply MapSym0 t) t :: [b]) :: Type)
+       Sing t -> Sing t -> Sing (Map t t :: [b]) :: Type)
     sEtad
       (sA_0123456789876543210 :: Sing a_0123456789876543210)
       (sA_0123456789876543210 :: Sing a_0123456789876543210)