From 366c47ecb761d97f8524f3e8b4da43239f47eed9 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Wed, 4 Sep 2019 20:29:59 -0400
Subject: [PATCH] Make singling preserve type variable order in type signatures

This patch tweaks `singType` (and its sister function `singCtor`) to
produce type signatures that preserve the order in which type
variables appear. For instance, if one writes this:

```hs
const2 :: forall b a. a -> b -> a
```

Then its singled counterpart will now quantify `b` and `a` in the
same order:

```hs
sConst2 :: forall b a (x :: a) (y :: b). Sing x -> Sing y -> Sing (Const2 x y)
```

This is important if one wants to combine `sConst2` with visible type
applications, as this means that the meaning of `@T1 @T2` in
`const @T1 @T2` will be preserved when one writes `sConst2 @T1 @T2`.
This also paves the way for #378, which seeks to fully support
promoting/singling type applications in the TH machinery.

Most of the interesting parts of this patch are described in
`Note [Preserve the order of type variables during singling]`
in `D.S.Single.Type`, so start that is a good starting point when
looking at this patch for the first time.

Fixes chunk (1) in
https://github.com/goldfirere/singletons/issues/378#issuecomment-528519679,
but there are still other parts of #378 that remain to be fixed.
---
 CHANGES.md                                    |   4 +
 README.md                                     |  36 +++
 src/Data/Singletons/Promote/Monad.hs          |  22 +-
 src/Data/Singletons/Single/Data.hs            |  29 +--
 src/Data/Singletons/Single/Type.hs            | 231 +++++++++++++++++-
 tests/SingletonsTestSuite.hs                  |   1 +
 .../GradingClient/Database.ghc88.template     |  68 +++---
 .../InsertionSortImp.ghc88.template           |   4 +-
 .../Singletons/AsPattern.ghc88.template       |   3 +-
 .../Singletons/BoundedDeriving.ghc88.template |  23 +-
 .../Singletons/BoxUnBox.ghc88.template        |   3 +-
 .../Singletons/Classes.ghc88.template         |  12 +-
 .../Singletons/Classes2.ghc88.template        |   4 +-
 .../Singletons/DataValues.ghc88.template      |   2 +-
 .../Singletons/EnumDeriving.ghc88.template    |  10 +-
 .../FunctorLikeDeriving.ghc88.template        |  10 +-
 .../Singletons/HigherOrder.ghc88.template     |   6 +-
 .../Singletons/Lambdas.ghc88.template         |   2 +-
 .../Singletons/Maybe.ghc88.template           |   4 +-
 .../Singletons/Nat.ghc88.template             |   4 +-
 .../Singletons/Operators.ghc88.template       |   4 +-
 .../Singletons/OrdDeriving.ghc88.template     |  40 +--
 .../Singletons/PatternMatching.ghc88.template |   2 +-
 .../Singletons/PolyKindsApp.ghc88.template    |   3 +-
 .../Singletons/Records.ghc88.template         |   4 +-
 .../Singletons/ShowDeriving.ghc88.template    |  15 +-
 .../StandaloneDeriving.ghc88.template         |   6 +-
 .../Singletons/Star.ghc88.template            |  10 +-
 .../Singletons/T159.ghc88.template            |  24 +-
 .../Singletons/T163.ghc88.template            |   4 +-
 .../Singletons/T178.ghc88.template            |   6 +-
 .../Singletons/T190.ghc88.template            |   2 +-
 .../Singletons/T197b.ghc88.template           |   4 +-
 .../Singletons/T200.ghc88.template            |   8 +-
 .../Singletons/T209.ghc88.template            |   2 +-
 .../Singletons/T249.ghc88.template            |   9 +-
 .../Singletons/T271.ghc88.template            |   7 +-
 .../Singletons/T297.ghc88.template            |   4 +-
 .../Singletons/T332.ghc88.template            |   3 +-
 .../Singletons/T371.ghc88.template            |  10 +-
 .../Singletons/T378a.ghc88.template           |  81 ++++++
 tests/compile-and-dump/Singletons/T378a.hs    |  46 ++++
 .../TopLevelPatterns.ghc88.template           |   6 +-
 43 files changed, 581 insertions(+), 197 deletions(-)
 create mode 100644 tests/compile-and-dump/Singletons/T378a.ghc88.template
 create mode 100644 tests/compile-and-dump/Singletons/T378a.hs

diff --git a/CHANGES.md b/CHANGES.md
index 06a96b45..32aeb439 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -4,6 +4,10 @@ Changelog for singletons project
 next
 ----
 * Require GHC 8.10.
+* `singletons` now does a much better job of preserving the order of type
+  variables when singling the type signatures of top-level functions and data
+  constructors. See the `Support for TypeApplications` section of the `README`
+  for more details.
 * `singletons` now does a more much thorough job of rejecting higher-rank types
   during promotion or singling, as `singletons` cannot support them.
   (Previously, `singletons` would sometimes accept them, often changing rank-2
diff --git a/README.md b/README.md
index e14a399a..c4428376 100644
--- a/README.md
+++ b/README.md
@@ -712,6 +712,42 @@ mechanism will not promote `TypeRep` to `*`.
 of types with which to work. See the Haddock documentation for the function
 `singletonStar` for more info.
 
+Support for `TypeApplications`
+------------------------------
+
+`singletons` currently cannot handle promoting or singling code that uses
+`TypeApplications` syntax, so `singletons` will simply drop any visible type
+applications. For example, `id @Bool True` will be promoted to `Id True` and
+singled to `sId STrue`. See
+[#378](https://github.com/goldfirere/singletons/issues/378) for a discussion
+of how `singletons` may support `TypeApplications` in the future.
+
+On the other hand, `singletons` does make an effort to preserve the order of
+type variables when singling type signatures. For example, this type signature:
+
+```haskell
+const2 :: forall b a. a -> b -> a
+```
+
+Will single to the following:
+
+```haskell
+sConst2 :: forall b a (x :: a) (y :: a). Sing x -> Sing y -> Sing (Const x y)
+```
+
+Therefore, writing `const2 @T1 @T2` works just as well as writing
+`sConst2 @T1 @T2`, since the type signatures for `const2` and `sConst2` both
+begin with `forall b a.`, in that order. Again, it is worth emphasizing that
+the TH machinery does not support singling `const2 @T1 @T2` directly, but you
+can write the type applications by hand if you so choose.
+
+It is not yet guaranteed that promotion preserves the order of type variables.
+For instance, if one writes `const @T1 @T2`, then one would have to write
+`Const @T2 @T1` at the kind level (and similarly for `Const`'s
+defunctionalization symbols). See
+[#378](https://github.com/goldfirere/singletons/issues/378) for a discussion
+of how this may be fixed in the future.
+
 Known bugs
 ----------
 
diff --git a/src/Data/Singletons/Promote/Monad.hs b/src/Data/Singletons/Promote/Monad.hs
index 19e63b7e..ce926151 100644
--- a/src/Data/Singletons/Promote/Monad.hs
+++ b/src/Data/Singletons/Promote/Monad.hs
@@ -35,7 +35,7 @@ type LetExpansions = OMap Name DType  -- from **term-level** name
 data PrEnv =
   PrEnv { pr_lambda_bound :: OMap Name Name
         , pr_let_bound    :: LetExpansions
-        , pr_forall_bound :: OSet Name -- See Note [Explicitly quantifying kinds variables]
+        , pr_forall_bound :: OSet Name -- See Note [Explicitly binding kind variables]
         , pr_local_decls  :: [Dec]
         }
 
@@ -129,17 +129,17 @@ promoteMDecs locals thing = do
 
 {-
 Note [Explicitly binding kind variables]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We want to ensure that when we single type signatures for functions, we should
-explicitly quantify every kind variable bound by a forall. For example, if we
-were to single the identity function:
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We want to ensure that when we single type signatures for functions and data
+constructors, we should explicitly quantify every kind variable bound by a
+forall. For example, if we were to single the identity function:
 
   identity :: forall a. a -> a
   identity x = x
 
 We want the final result to be:
 
-  sIdentity :: forall a (x :: a). Sing x -> Sing (Identity x)
+  sIdentity :: forall a (x :: a). Sing x -> Sing (Identity x :: a)
   sIdentity sX = sX
 
 Accomplishing this takes a bit of care during promotion. When promoting a
@@ -160,7 +160,7 @@ consider this more complicated example:
 
 When singling, we would eventually end up in this spot:
 
-  sF :: forall a (x :: a). Sing a -> Sing (F a)
+  sF :: forall a (x :: a). Sing a -> Sing (F a :: a)
   sF = sG
     where
       sG :: _
@@ -168,10 +168,10 @@ When singling, we would eventually end up in this spot:
 
 We must make sure /not/ to fill in the following type for _:
 
-  sF :: forall a (x :: a). Sing a -> Sing (F a)
+  sF :: forall a (x :: a). Sing a -> Sing (F a :: a)
   sF = sG
     where
-      sG :: forall a (y :: a). Sing a -> Sing (G a)
+      sG :: forall a (y :: a). Sing a -> Sing (G a :: a)
       sG x = x
 
 This would be incorrect, as the `a` bound by sF /must/ be the same one used in
@@ -179,9 +179,9 @@ sG, as per the scoping of the original `f` function. Thus, we ensure that the
 bound variables from `f` are put into lde_bound_kvs when promoting `g` so
 that we subtract out `a` and are left with the correct result:
 
-  sF :: forall a (x :: a). Sing a -> Sing (F a)
+  sF :: forall a (x :: a). Sing a -> Sing (F a :: a)
   sF = sG
     where
-      sG :: forall (y :: a). Sing a -> Sing (G a)
+      sG :: forall (y :: a). Sing a -> Sing (G a :: a)
       sG x = x
 -}
diff --git a/src/Data/Singletons/Single/Data.hs b/src/Data/Singletons/Single/Data.hs
index c35074b9..3ceff40c 100644
--- a/src/Data/Singletons/Single/Data.hs
+++ b/src/Data/Singletons/Single/Data.hs
@@ -11,7 +11,6 @@ Singletonizes constructors.
 module Data.Singletons.Single.Data where
 
 import Language.Haskell.TH.Desugar
-import Language.Haskell.TH.Desugar.OSet (OSet)
 import Language.Haskell.TH.Syntax
 import Data.Singletons.Single.Defun
 import Data.Singletons.Single.Monad
@@ -22,7 +21,6 @@ import Data.Singletons.Util
 import Data.Singletons.Names
 import Data.Singletons.Syntax
 import Control.Monad
-import Data.Foldable
 
 -- We wish to consider the promotion of "Rep" to be *
 -- not a promoted data constructor.
@@ -129,12 +127,12 @@ singDataD (DataDecl name tvbs ctors) = do
           pure $ DClause [DVarP x]
                $ DConE someSingDataName `DAppE` DCaseE (DVarE x) []
 
--- refine a constructor.
+-- Single a constructor.
 singCtor :: Name -> DCon -> SgM DCon
  -- polymorphic constructors are handled just
  -- like monomorphic ones -- the polymorphism in
  -- the kind is automatic
-singCtor dataName (DCon _tvbs cxt name fields rty)
+singCtor dataName (DCon con_tvbs cxt name fields rty)
   | not (null cxt)
   = fail "Singling of constrained constructors not yet supported"
   | otherwise
@@ -144,13 +142,13 @@ singCtor dataName (DCon _tvbs cxt name fields rty)
       sCon = DConE sName
       pCon = DConT name
   indexNames <- mapM (const $ qNewName "n") types
-  let indices = map DVarT indexNames
   kinds <- mapM promoteType types
-  let bound_kvs = foldMap fvDType kinds
-  args <- zipWithM (buildArgType bound_kvs) types indices
   rty' <- promoteType rty
-  let tvbs = map DPlainTV (toList bound_kvs) ++ zipWith DKindedTV indexNames kinds
+  let indices = map DVarT indexNames
       kindedIndices = zipWith DSigT indices kinds
+      args = map (DAppT singFamily) indices
+      kvbs = singTypeKVBs con_tvbs kinds [] rty' mempty
+      all_tvbs = kvbs ++ zipWith DKindedTV indexNames kinds
 
   -- SingI instance for data constructor
   emitDecs
@@ -172,12 +170,9 @@ singCtor dataName (DCon _tvbs cxt name fields rty)
                       DRecC [ (singValName field_name, noBang, arg)
                             | (field_name, _, _) <- rec_fields
                             | arg <- args ]
-  return $ DCon tvbs
-                []
-                sName
-                conFields
-                (DConT (singTyConName dataName) `DAppT` foldType pCon indices)
-  where buildArgType :: OSet Name -> DType -> DType -> SgM DType
-        buildArgType bound_kvs ty index = do
-          (ty', _, _, _, _, _) <- singType bound_kvs index ty
-          return ty'
+  return $ DCon all_tvbs [] sName conFields
+                (DConT (singTyConName dataName) `DAppT`
+                  (foldType pCon indices `DSigT` rty'))
+                  -- Make sure to include an explicit `rty'` kind annotation.
+                  -- See Note [Preserve the order of type variables during singling],
+                  -- wrinkle 3, in D.S.Single.Type.
diff --git a/src/Data/Singletons/Single/Type.hs b/src/Data/Singletons/Single/Type.hs
index f5819321..8b5bfa9e 100644
--- a/src/Data/Singletons/Single/Type.hs
+++ b/src/Data/Singletons/Single/Type.hs
@@ -9,7 +9,6 @@ Singletonizes types.
 module Data.Singletons.Single.Type where
 
 import Language.Haskell.TH.Desugar
-import qualified Language.Haskell.TH.Desugar.OSet as OSet
 import Language.Haskell.TH.Desugar.OSet (OSet)
 import Language.Haskell.TH.Syntax
 import Data.Singletons.Names
@@ -18,6 +17,8 @@ import Data.Singletons.Promote.Type
 import Data.Singletons.Util
 import Control.Monad
 import Data.Foldable
+import Data.Function
+import Data.List
 
 singType :: OSet Name      -- the set of bound kind variables in this scope
                            -- see Note [Explicitly binding kind variables]
@@ -32,25 +33,50 @@ singType :: OSet Name      -- the set of bound kind variables in this scope
                 , DKind )  -- the kind of the result type
 singType bound_kvs prom ty = do
   checkVanillaDType ty
-  let (_, cxt, args, res) = unravelVanillaDType ty
-      num_args            = length args
+  let (orig_tvbs, cxt, args, res) = unravelVanillaDType ty
+      num_args                    = length args
   cxt' <- mapM singPred_NC cxt
   arg_names <- replicateM num_args (qNewName "t")
   prom_args <- mapM promoteType_NC args
   prom_res  <- promoteType_NC res
   let args' = map (\n -> singFamily `DAppT` (DVarT n)) arg_names
       res'  = singFamily `DAppT` (foldl apply prom (map DVarT arg_names) `DSigT` prom_res)
+                -- Make sure to include an explicit `prom_res` kind annotation.
+                -- See Note [Preserve the order of type variables during singling],
+                -- wrinkle 3.
       tau   = ravel args' res'
-      -- Make sure to subtract out the bound variables currently in scope, lest we
-      -- accidentally shadow them in this type signature.
-      kv_names_to_bind = foldMap fvDType (prom_args ++ cxt' ++ [prom_res])
-                            OSet.\\ bound_kvs
-      kvs_to_bind      = toList kv_names_to_bind
-  let ty' = DForallT ForallInvis
-                     (map DPlainTV kvs_to_bind ++ zipWith DKindedTV arg_names prom_args) $
-            DConstrainedT cxt' tau
+      kvbs     = singTypeKVBs orig_tvbs prom_args cxt' prom_res bound_kvs
+      all_tvbs = kvbs ++ zipWith DKindedTV arg_names prom_args
+      ty' = DForallT ForallInvis all_tvbs $ DConstrainedT cxt' tau
   return (ty', num_args, arg_names, cxt, prom_args, prom_res)
 
+-- Compute the kind variable binders to use in the singled version of a type
+-- signature. This has two main call sites: singType and D.S.Single.Data.singCtor.
+--
+-- This implements the advice documented in
+-- Note [Preserve the order of type variables during singling], wrinkle 1.
+singTypeKVBs ::
+     [DTyVarBndr] -- ^ The bound type variables from the original type signature.
+  -> [DType]      -- ^ The argument types of the signature (promoted).
+  -> DCxt         -- ^ The context of the signature (singled).
+  -> DType        -- ^ The result type of the signature (promoted).
+  -> OSet Name    -- ^ The type variables previously bound in the current scope.
+  -> [DTyVarBndr] -- ^ The kind variables for the singled type signature.
+singTypeKVBs orig_tvbs prom_args sing_ctxt prom_res bound_tvbs
+  | null orig_tvbs
+  -- There are no explicitly `forall`ed type variable binders, so we must
+  -- infer them ourselves.
+  = deleteFirstsBy
+      ((==) `on` extractTvbName)
+      (toposortTyVarsOf $ prom_args ++ sing_ctxt ++ [prom_res])
+      (map DPlainTV $ toList bound_tvbs)
+      -- Make sure to subtract out the bound variables currently in scope,
+      -- lest we accidentally shadow them in this type signature.
+      -- See Note [Explicitly binding kind variables] in D.S.Promote.Monad.
+  | otherwise
+  -- There is an explicit `forall`, so this case is easy.
+  = orig_tvbs
+
 -- Single a DPred, checking that it is a vanilla type in the process.
 -- See [Vanilla-type validity checking during promotion]
 -- in Data.Singletons.Promote.Type.
@@ -89,3 +115,186 @@ singPredRec _ctx DArrowT =
   fail "(->) spotted at head of a constraint"
 singPredRec _ctx (DLitT {}) =
   fail "Type-level literal spotted at head of a constraint"
+
+{-
+Note [Preserve the order of type variables during singling]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+singletons does its best to preseve the order in which users write type
+variables in type signatures for functions and data constructors. They are
+"preserved" in the sense that if one writes `foo @T1 @T2`, one should be
+able to write out `sFoo @T1 @T2` by hand and have the same order of visible
+type applications still work. Accomplishing this is surprisingly nontrivial,
+so this Note documents the various wrinkles one must iron out to get this
+working.
+
+-----
+-- Wrinkle 1: Dealing with the presence (and absence) of `forall`
+-----
+
+If we single a function that has an explicit `forall`, such as this example:
+
+  const2 :: forall b a. a -> b -> a
+  const2 x _ = x
+
+Then our job is easy, as the exact order of type variables has already been
+spelled out in advance. We single this to:
+
+  sConst2 :: forall b a (x :: a) (y :: b). Sing x -> Sing y -> Sing (Const2 x y :: a)
+  sConst2 = ...
+
+What happens if there is no explicit `forall`, as in this example?
+
+  data V a
+
+  absurd :: V a -> b
+  absurd v = case v of {}
+
+This time, the order of type variables vis-à-vis TypeApplications is determined
+by their left-to-right order of appearance in the type signature. It's tempting
+to think that since there is no explicit `forall` in the original type
+signature, we could get away without an explicit `forall` in the singled type
+signature. That is, one could write:
+
+  sAbsurd :: Sing (v :: V a) -> Sing (Absurd :: b)
+
+This would have the right type variable order, but unfortunately, this approach
+does not play well with singletons' style of code generation. Consider the code
+that would be generated for the body of sAbsurd:
+
+  sAbsurd :: Sing (v :: V a) -> Sing (Absurd :: b)
+  sAbsurd (sV :: Sing v) = id @(Case v v :: b) (case sV of {})
+
+Note the use of the type `Case v v :: b` in the right-hand side of sAbsurd.
+However, because `b` was not bound by a top-level `forall`, it won't be in
+scope here, resulting in an error!
+
+(Why do we generate the code `id @(Case v v :: b)` in the first place? See
+Note [The id hack; or, how singletons learned to stop worrying and avoid kind generalization]
+in D.S.Single.)
+
+The simplest approach is to just always generate singled type signatures with
+explicit `forall`s. In the event that the original type signature lacks an
+explicit `forall`, we inferr the correct type variable ordering ourselves and
+synthesize a `forall` with that order. The `singTypeKVBs` function implements
+this logic.
+
+-----
+-- Wrinkle 2: The TH reification swamp
+-----
+
+There is another issue with type signatures that lack explicit `forall`s, one
+which the current design of Template Haskell does not make simple to fix.
+If we single code that is wrapped in TH quotes, such as in the following example:
+
+  $(singletons [d|
+    data Proxy (a :: k) where
+      MkProxy :: Proxy a
+    |])
+
+Then our job is made much easier when singling MkProxy, since we know that the
+only type variable that must be quantified is `a`, as that is the only one
+specified in the type signature.
+
+However, this is not the only possible way to single MkProxy. One can
+alternatively use $(genSingletons [''Proxy]), which uses TH reification to
+infer the type of MkProxy. There is perilous, however, because this is how
+TH reifies MkProxy:
+
+  ForallC [KindedTV k StarT,KindedTV a (VarT k)] []
+          (GadtC [MkProxy] [] (AppT (ConT Proxy) (VarT a)))
+
+In terms of actual Haskell code, that's:
+
+  MkProxy :: forall k (a :: k). Proxy a
+
+This is subtly different than before, as `k` is now specified. Contrast this
+with `MkProxy :: Proxy a`, where `k` is invisible. In other words, if you
+single MkProxy using genSingletons, then `Proxy @True` will typecheck but
+`SMkProxy @True` will /not/ typecheck—you'd have to use `SMkProxy @_ @True`
+instead. Urk!
+
+At present, Template Haskell does not have a way to distinguish specified from
+inferred type variables—see GHC #17159—and it is unclear how one could work
+around this issue withouf first fixing #17159 upstream. Thankfully, it is
+only likely to bite in situations where the original type signature uses
+inferred variables, so the damage is somewhat minimal.
+
+-----
+-- Wrinkle 3: Where to put explicit kind annotations
+-----
+
+Type variable binders are only part of the story—we must also determine what
+the body of the type signature will be singled to. As a general rule, if the
+original type signature is of the form:
+
+  f :: forall a_1 ... a_m. (C_1, ..., C_n)
+    => T_1 -> ... -> T_p -> R
+
+Then the singled type signature will be:
+
+  sF :: forall a_1 ... a_m (x_1 :: PT_1) ... (x_p :: PT_p). (SC_1, ..., SC_n)
+     => Sing x1 -> ... -> Sing x_p -> SRes (F x1 ... x_p :: PR)
+
+Where:
+
+* x_i is a fresh type variable of kind PT_i.
+* PT_i is the promoted version of the type T_i, and PR is the promoted version
+  of the type R.
+* SC_i is the singled version of the constraint SC_i.
+* SRes is either `Sing` if dealing with a function, or a singled data type if
+  dealing with a data constructor. For instance, SRes is `SBool` in
+  `STrue :: SBool (True :: Bool)`.
+
+One aspect of this worth pointing out is the explicit `:: PR` kind annotation
+in the result type `Sing (F x1 ... x_p :: PR)`. As it turns out, this kind
+annotation is mandatory, as omitting can result in singled type signatures
+with the wrong semantics. For instance, consider the `Nothing` data
+constructor:
+
+  Nothing :: forall a. Maybe a
+
+Consider what would happen if it were singled to this type:
+
+  SNothing :: forall a. SMaybe Nothing
+
+This is not what we want at all, since the `a` has no connection to the
+`Nothing` in the result type. It's as if we had written this:
+
+  SNothing :: forall {t} a. SMaybe (Nothing :: Maybe t)
+
+If we instead generate `forall a. SMaybe (Nothing :: Maybe a)`, then this issue
+is handily avoided.
+
+You might wonder if it would be cleaner to use visible kind applications
+instead:
+
+  SNothing :: forall a. SMaybe (Nothing @a)
+
+This does work for many cases, but there are also some corner cases where this
+approach fails. Recall the `MkProxy` example from Wrinkle 2 above:
+
+  data Proxy (a :: k) where
+    MkProxy :: Proxy a
+  $(genSingletons [''Proxy])
+
+Due to the design of Template Haskell (discussed in Wrinkle 2), `MkProxy` will
+be reified with the type of `forall k (a :: k). Proxy a`. This means that
+if we used visible kind applications in the result type, we would end up with
+this:
+
+  SMkProxy :: forall k (a :: k). SProxy (MkProxy @k @a)
+
+This will not kind-check because MkProxy only accepts /one/ visible kind argument,
+whereas this supplies it with two. To avoid this issue, we instead use the type
+`forall k (a :: k). SProxy (MkProxy :: Proxy a)`. Granted, this type is /still/
+technically wrong due to the fact that it explicitly quantifies `k`, but at the
+very least it typechecks. If GHC #17159 were fixed, we could revisit this
+design choice.
+
+Finally, note that we need only write `Sing x_1 -> ... -> Sing x_p`, and not
+`Sing (x_1 :: PT_1) -> ... Sing (x_p :: PT_p)`. This is simply because we
+always use explicit `forall`s in singled type signatures, and therefore always
+explicitly bind `(x_1 :: PT_1) ... (x_p :: PT_p)`, which fully determine the
+kinds of `x_1 ... x_p`. It wouldn't be wrong to add extra kind annotations to
+`Sing x_1 -> ... -> Sing x_p`, just redundant.
+-}
diff --git a/tests/SingletonsTestSuite.hs b/tests/SingletonsTestSuite.hs
index df34ff63..088cb1d8 100644
--- a/tests/SingletonsTestSuite.hs
+++ b/tests/SingletonsTestSuite.hs
@@ -117,6 +117,7 @@ tests =
     , compileAndDumpStdTest "T367"
     , compileAndDumpStdTest "T371"
     , compileAndDumpStdTest "T376"
+    , compileAndDumpStdTest "T378a"
     , compileAndDumpStdTest "T401"
     , compileAndDumpStdTest "T402"
     ],
diff --git a/tests/compile-and-dump/GradingClient/Database.ghc88.template b/tests/compile-and-dump/GradingClient/Database.ghc88.template
index 8c85205a..a10e4d60 100644
--- a/tests/compile-and-dump/GradingClient/Database.ghc88.template
+++ b/tests/compile-and-dump/GradingClient/Database.ghc88.template
@@ -54,8 +54,8 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
       type (==) a b = Equals_0123456789876543210 a b
     data SNat :: Nat -> Type
       where
-        SZero :: SNat Zero
-        SSucc :: forall (n :: Nat). (Sing (n :: Nat)) -> SNat (Succ n)
+        SZero :: SNat (Zero :: Nat)
+        SSucc :: forall (n :: Nat). (Sing n) -> SNat (Succ n :: Nat)
     type instance Sing @Nat = SNat
     instance SingKind Nat where
       type Demote Nat = Nat
@@ -717,11 +717,11 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
       sing = (singFun1 @(AppendSym1 (d :: Schema))) (sAppend (sing @d))
     data SU :: U -> Type
       where
-        SBOOL :: SU BOOL
-        SSTRING :: SU STRING
-        SNAT :: SU NAT
+        SBOOL :: SU (BOOL :: U)
+        SSTRING :: SU (STRING :: U)
+        SNAT :: SU (NAT :: U)
         SVEC :: forall (n :: U) (n :: Nat).
-                (Sing (n :: U)) -> (Sing (n :: Nat)) -> SU (VEC n n)
+                (Sing n) -> (Sing n) -> SU (VEC n n :: U)
     type instance Sing @U = SU
     instance SingKind U where
       type Demote U = U
@@ -739,32 +739,32 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
             (,) (SomeSing c) (SomeSing c) -> SomeSing ((SVEC c) c) }
     data SAChar :: AChar -> Type
       where
-        SCA :: SAChar CA
-        SCB :: SAChar CB
-        SCC :: SAChar CC
-        SCD :: SAChar CD
-        SCE :: SAChar CE
-        SCF :: SAChar CF
-        SCG :: SAChar CG
-        SCH :: SAChar CH
-        SCI :: SAChar CI
-        SCJ :: SAChar CJ
-        SCK :: SAChar CK
-        SCL :: SAChar CL
-        SCM :: SAChar CM
-        SCN :: SAChar CN
-        SCO :: SAChar CO
-        SCP :: SAChar CP
-        SCQ :: SAChar CQ
-        SCR :: SAChar CR
-        SCS :: SAChar CS
-        SCT :: SAChar CT
-        SCU :: SAChar CU
-        SCV :: SAChar CV
-        SCW :: SAChar CW
-        SCX :: SAChar CX
-        SCY :: SAChar CY
-        SCZ :: SAChar CZ
+        SCA :: SAChar (CA :: AChar)
+        SCB :: SAChar (CB :: AChar)
+        SCC :: SAChar (CC :: AChar)
+        SCD :: SAChar (CD :: AChar)
+        SCE :: SAChar (CE :: AChar)
+        SCF :: SAChar (CF :: AChar)
+        SCG :: SAChar (CG :: AChar)
+        SCH :: SAChar (CH :: AChar)
+        SCI :: SAChar (CI :: AChar)
+        SCJ :: SAChar (CJ :: AChar)
+        SCK :: SAChar (CK :: AChar)
+        SCL :: SAChar (CL :: AChar)
+        SCM :: SAChar (CM :: AChar)
+        SCN :: SAChar (CN :: AChar)
+        SCO :: SAChar (CO :: AChar)
+        SCP :: SAChar (CP :: AChar)
+        SCQ :: SAChar (CQ :: AChar)
+        SCR :: SAChar (CR :: AChar)
+        SCS :: SAChar (CS :: AChar)
+        SCT :: SAChar (CT :: AChar)
+        SCU :: SAChar (CU :: AChar)
+        SCV :: SAChar (CV :: AChar)
+        SCW :: SAChar (CW :: AChar)
+        SCX :: SAChar (CX :: AChar)
+        SCY :: SAChar (CY :: AChar)
+        SCZ :: SAChar (CZ :: AChar)
     type instance Sing @AChar = SAChar
     instance SingKind AChar where
       type Demote AChar = AChar
@@ -823,7 +823,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
     data SAttribute :: Attribute -> Type
       where
         SAttr :: forall (n :: [AChar]) (n :: U).
-                 (Sing (n :: [AChar])) -> (Sing (n :: U)) -> SAttribute (Attr n n)
+                 (Sing n) -> (Sing n) -> SAttribute (Attr n n :: Attribute)
     type instance Sing @Attribute = SAttribute
     instance SingKind Attribute where
       type Demote Attribute = Attribute
@@ -836,7 +836,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
     data SSchema :: Schema -> Type
       where
         SSch :: forall (n :: [Attribute]).
-                (Sing (n :: [Attribute])) -> SSchema (Sch n)
+                (Sing n) -> SSchema (Sch n :: Schema)
     type instance Sing @Schema = SSchema
     instance SingKind Schema where
       type Demote Schema = Schema
diff --git a/tests/compile-and-dump/InsertionSort/InsertionSortImp.ghc88.template b/tests/compile-and-dump/InsertionSort/InsertionSortImp.ghc88.template
index 1cc6d28d..afa838d5 100644
--- a/tests/compile-and-dump/InsertionSort/InsertionSortImp.ghc88.template
+++ b/tests/compile-and-dump/InsertionSort/InsertionSortImp.ghc88.template
@@ -15,8 +15,8 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
     type instance Apply SuccSym0 t0123456789876543210 = Succ t0123456789876543210
     data SNat :: Nat -> Type
       where
-        SZero :: SNat Zero
-        SSucc :: forall (n :: Nat). (Sing (n :: Nat)) -> SNat (Succ n)
+        SZero :: SNat (Zero :: Nat)
+        SSucc :: forall (n :: Nat). (Sing n) -> SNat (Succ n :: Nat)
     type instance Sing @Nat = SNat
     instance SingKind Nat where
       type Demote Nat = Nat
diff --git a/tests/compile-and-dump/Singletons/AsPattern.ghc88.template b/tests/compile-and-dump/Singletons/AsPattern.ghc88.template
index 53b2aa31..3c9aabf4 100644
--- a/tests/compile-and-dump/Singletons/AsPattern.ghc88.template
+++ b/tests/compile-and-dump/Singletons/AsPattern.ghc88.template
@@ -366,8 +366,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
     data SBaz :: Baz -> GHC.Types.Type
       where
         SBaz :: forall (n :: Nat) (n :: Nat) (n :: Nat).
-                (Sing (n :: Nat))
-                -> (Sing (n :: Nat)) -> (Sing (n :: Nat)) -> SBaz (Baz n n n)
+                (Sing n) -> (Sing n) -> (Sing n) -> SBaz (Baz n n n :: Baz)
     type instance Sing @Baz = SBaz
     instance SingKind Baz where
       type Demote Baz = Baz
diff --git a/tests/compile-and-dump/Singletons/BoundedDeriving.ghc88.template b/tests/compile-and-dump/Singletons/BoundedDeriving.ghc88.template
index f181c6a0..423471ee 100644
--- a/tests/compile-and-dump/Singletons/BoundedDeriving.ghc88.template
+++ b/tests/compile-and-dump/Singletons/BoundedDeriving.ghc88.template
@@ -124,7 +124,7 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations
     instance PBounded Pair where
       type MinBound = MinBound_0123456789876543210Sym0
       type MaxBound = MaxBound_0123456789876543210Sym0
-    data SFoo1 :: Foo1 -> Type where SFoo1 :: SFoo1 Foo1
+    data SFoo1 :: Foo1 -> Type where SFoo1 :: SFoo1 (Foo1 :: Foo1)
     type instance Sing @Foo1 = SFoo1
     instance SingKind Foo1 where
       type Demote Foo1 = Foo1
@@ -132,11 +132,11 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations
       toSing Foo1 = SomeSing SFoo1
     data SFoo2 :: Foo2 -> Type
       where
-        SA :: SFoo2 A
-        SB :: SFoo2 B
-        SC :: SFoo2 C
-        SD :: SFoo2 D
-        SE :: SFoo2 E
+        SA :: SFoo2 (A :: Foo2)
+        SB :: SFoo2 (B :: Foo2)
+        SC :: SFoo2 (C :: Foo2)
+        SD :: SFoo2 (D :: Foo2)
+        SE :: SFoo2 (E :: Foo2)
     type instance Sing @Foo2 = SFoo2
     instance SingKind Foo2 where
       type Demote Foo2 = Foo2
@@ -151,7 +151,8 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations
       toSing D = SomeSing SD
       toSing E = SomeSing SE
     data SFoo3 :: forall a. Foo3 a -> Type
-      where SFoo3 :: forall a (n :: a). (Sing (n :: a)) -> SFoo3 (Foo3 n)
+      where
+        SFoo3 :: forall a (n :: a). (Sing n) -> SFoo3 (Foo3 n :: Foo3 a)
     type instance Sing @(Foo3 a) = SFoo3
     instance SingKind a => SingKind (Foo3 a) where
       type Demote (Foo3 a) = Foo3 (Demote a)
@@ -161,8 +162,10 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations
             SomeSing c -> SomeSing (SFoo3 c) }
     data SFoo4 :: forall a b. Foo4 a b -> Type
       where
-        SFoo41 :: SFoo4 Foo41
-        SFoo42 :: SFoo4 Foo42
+        SFoo41 :: forall (a :: Type) (b :: Type).
+                  SFoo4 (Foo41 :: Foo4 (a :: Type) (b :: Type))
+        SFoo42 :: forall (a :: Type) (b :: Type).
+                  SFoo4 (Foo42 :: Foo4 (a :: Type) (b :: Type))
     type instance Sing @(Foo4 a b) = SFoo4
     instance (SingKind a, SingKind b) => SingKind (Foo4 a b) where
       type Demote (Foo4 a b) = Foo4 (Demote a) (Demote b)
@@ -173,7 +176,7 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations
     data SPair :: Pair -> Type
       where
         SPair :: forall (n :: Bool) (n :: Bool).
-                 (Sing (n :: Bool)) -> (Sing (n :: Bool)) -> SPair (Pair n n)
+                 (Sing n) -> (Sing n) -> SPair (Pair n n :: Pair)
     type instance Sing @Pair = SPair
     instance SingKind Pair where
       type Demote Pair = Pair
diff --git a/tests/compile-and-dump/Singletons/BoxUnBox.ghc88.template b/tests/compile-and-dump/Singletons/BoxUnBox.ghc88.template
index 360e9cb2..1628e835 100644
--- a/tests/compile-and-dump/Singletons/BoxUnBox.ghc88.template
+++ b/tests/compile-and-dump/Singletons/BoxUnBox.ghc88.template
@@ -38,7 +38,8 @@ Singletons/BoxUnBox.hs:(0,0)-(0,0): Splicing declarations
     instance SingI (UnBoxSym0 :: (~>) (Box a) a) where
       sing = (singFun1 @UnBoxSym0) sUnBox
     data SBox :: forall a. Box a -> GHC.Types.Type
-      where SFBox :: forall a (n :: a). (Sing (n :: a)) -> SBox (FBox n)
+      where
+        SFBox :: forall a (n :: a). (Sing n) -> SBox (FBox n :: Box a)
     type instance Sing @(Box a) = SBox
     instance SingKind a => SingKind (Box a) where
       type Demote (Box a) = Box (Demote a)
diff --git a/tests/compile-and-dump/Singletons/Classes.ghc88.template b/tests/compile-and-dump/Singletons/Classes.ghc88.template
index 3e43f01f..29c0014c 100644
--- a/tests/compile-and-dump/Singletons/Classes.ghc88.template
+++ b/tests/compile-and-dump/Singletons/Classes.ghc88.template
@@ -313,8 +313,8 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
       sing = (singFun1 @(ConstSym1 (d :: a))) (sConst (sing @d))
     data SFoo :: Foo -> GHC.Types.Type
       where
-        SA :: SFoo A
-        SB :: SFoo B
+        SA :: SFoo (A :: Foo)
+        SB :: SFoo (B :: Foo)
     type instance Sing @Foo = SFoo
     instance SingKind Foo where
       type Demote Foo = Foo
@@ -324,8 +324,8 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
       toSing B = SomeSing SB
     data SFoo2 :: Foo2 -> GHC.Types.Type
       where
-        SF :: SFoo2 F
-        SG :: SFoo2 G
+        SF :: SFoo2 (F :: Foo2)
+        SG :: SFoo2 (G :: Foo2)
     type instance Sing @Foo2 = SFoo2
     instance SingKind Foo2 where
       type Demote Foo2 = Foo2
@@ -542,8 +542,8 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
       type Mycompare a a = Apply (Apply Mycompare_0123456789876543210Sym0 a) a
     data SNat' :: Nat' -> GHC.Types.Type
       where
-        SZero' :: SNat' Zero'
-        SSucc' :: forall (n :: Nat'). (Sing (n :: Nat')) -> SNat' (Succ' n)
+        SZero' :: SNat' (Zero' :: Nat')
+        SSucc' :: forall (n :: Nat'). (Sing n) -> SNat' (Succ' n :: Nat')
     type instance Sing @Nat' = SNat'
     instance SingKind Nat' where
       type Demote Nat' = Nat'
diff --git a/tests/compile-and-dump/Singletons/Classes2.ghc88.template b/tests/compile-and-dump/Singletons/Classes2.ghc88.template
index 16bb9f92..4a58381a 100644
--- a/tests/compile-and-dump/Singletons/Classes2.ghc88.template
+++ b/tests/compile-and-dump/Singletons/Classes2.ghc88.template
@@ -55,9 +55,9 @@ Singletons/Classes2.hs:(0,0)-(0,0): Splicing declarations
       type Mycompare a a = Apply (Apply Mycompare_0123456789876543210Sym0 a) a
     data SNatFoo :: NatFoo -> GHC.Types.Type
       where
-        SZeroFoo :: SNatFoo ZeroFoo
+        SZeroFoo :: SNatFoo (ZeroFoo :: NatFoo)
         SSuccFoo :: forall (n :: NatFoo).
-                    (Sing (n :: NatFoo)) -> SNatFoo (SuccFoo n)
+                    (Sing n) -> SNatFoo (SuccFoo n :: NatFoo)
     type instance Sing @NatFoo = SNatFoo
     instance SingKind NatFoo where
       type Demote NatFoo = NatFoo
diff --git a/tests/compile-and-dump/Singletons/DataValues.ghc88.template b/tests/compile-and-dump/Singletons/DataValues.ghc88.template
index 004aae41..67722630 100644
--- a/tests/compile-and-dump/Singletons/DataValues.ghc88.template
+++ b/tests/compile-and-dump/Singletons/DataValues.ghc88.template
@@ -124,7 +124,7 @@ Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations
     data SPair :: forall a b. Pair a b -> GHC.Types.Type
       where
         SPair :: forall a b (n :: a) (n :: b).
-                 (Sing (n :: a)) -> (Sing (n :: b)) -> SPair (Pair n n)
+                 (Sing n) -> (Sing n) -> SPair (Pair n n :: Pair a b)
     type instance Sing @(Pair a b) = SPair
     instance (SingKind a, SingKind b) => SingKind (Pair a b) where
       type Demote (Pair a b) = Pair (Demote a) (Demote b)
diff --git a/tests/compile-and-dump/Singletons/EnumDeriving.ghc88.template b/tests/compile-and-dump/Singletons/EnumDeriving.ghc88.template
index 6564904d..b23e6d3f 100644
--- a/tests/compile-and-dump/Singletons/EnumDeriving.ghc88.template
+++ b/tests/compile-and-dump/Singletons/EnumDeriving.ghc88.template
@@ -56,9 +56,9 @@ Singletons/EnumDeriving.hs:(0,0)-(0,0): Splicing declarations
       type FromEnum a = Apply FromEnum_0123456789876543210Sym0 a
     data SFoo :: Foo -> GHC.Types.Type
       where
-        SBar :: SFoo Bar
-        SBaz :: SFoo Baz
-        SBum :: SFoo Bum
+        SBar :: SFoo (Bar :: Foo)
+        SBaz :: SFoo (Baz :: Foo)
+        SBum :: SFoo (Bum :: Foo)
     type instance Sing @Foo = SFoo
     instance SingKind Foo where
       type Demote Foo = Foo
@@ -70,8 +70,8 @@ Singletons/EnumDeriving.hs:(0,0)-(0,0): Splicing declarations
       toSing Bum = SomeSing SBum
     data SQuux :: Quux -> GHC.Types.Type
       where
-        SQ1 :: SQuux Q1
-        SQ2 :: SQuux Q2
+        SQ1 :: SQuux (Q1 :: Quux)
+        SQ2 :: SQuux (Q2 :: Quux)
     type instance Sing @Quux = SQuux
     instance SingKind Quux where
       type Demote Quux = Quux
diff --git a/tests/compile-and-dump/Singletons/FunctorLikeDeriving.ghc88.template b/tests/compile-and-dump/Singletons/FunctorLikeDeriving.ghc88.template
index 74eb7516..3a217be9 100644
--- a/tests/compile-and-dump/Singletons/FunctorLikeDeriving.ghc88.template
+++ b/tests/compile-and-dump/Singletons/FunctorLikeDeriving.ghc88.template
@@ -1248,12 +1248,10 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations
                         (n :: a)
                         (n :: Maybe a)
                         (n :: Maybe (Maybe a)).
-                 (Sing (n :: x))
-                 -> (Sing (n :: a))
-                    -> (Sing (n :: Maybe a))
-                       -> (Sing (n :: Maybe (Maybe a))) -> ST (MkT1 n n n n)
-        SMkT2 :: forall x (n :: Maybe x).
-                 (Sing (n :: Maybe x)) -> ST (MkT2 n)
+                 (Sing n)
+                 -> (Sing n) -> (Sing n) -> (Sing n) -> ST (MkT1 n n n n :: T x a)
+        SMkT2 :: forall x a (n :: Maybe x).
+                 (Sing n) -> ST (MkT2 n :: T x a)
     type instance Sing @(T x a) = ST
     instance (SingKind x, SingKind a) => SingKind (T x a) where
       type Demote (T x a) = T (Demote x) (Demote a)
diff --git a/tests/compile-and-dump/Singletons/HigherOrder.ghc88.template b/tests/compile-and-dump/Singletons/HigherOrder.ghc88.template
index bead0ce4..7341f34f 100644
--- a/tests/compile-and-dump/Singletons/HigherOrder.ghc88.template
+++ b/tests/compile-and-dump/Singletons/HigherOrder.ghc88.template
@@ -454,8 +454,10 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations
       sing = (singFun1 @(MapSym1 (d :: (~>) a b))) (sMap (sing @d))
     data SEither :: forall a b. Either a b -> GHC.Types.Type
       where
-        SLeft :: forall a (n :: a). (Sing (n :: a)) -> SEither (Left n)
-        SRight :: forall b (n :: b). (Sing (n :: b)) -> SEither (Right n)
+        SLeft :: forall a b (n :: a).
+                 (Sing n) -> SEither (Left n :: Either a b)
+        SRight :: forall a b (n :: b).
+                  (Sing n) -> SEither (Right n :: Either a b)
     type instance Sing @(Either a b) = SEither
     instance (SingKind a, SingKind b) => SingKind (Either a b) where
       type Demote (Either a b) = Either (Demote a) (Demote b)
diff --git a/tests/compile-and-dump/Singletons/Lambdas.ghc88.template b/tests/compile-and-dump/Singletons/Lambdas.ghc88.template
index 56d8dadc..66aa6865 100644
--- a/tests/compile-and-dump/Singletons/Lambdas.ghc88.template
+++ b/tests/compile-and-dump/Singletons/Lambdas.ghc88.template
@@ -815,7 +815,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations
     data SFoo :: forall a b. Foo a b -> GHC.Types.Type
       where
         SFoo :: forall a b (n :: a) (n :: b).
-                (Sing (n :: a)) -> (Sing (n :: b)) -> SFoo (Foo n n)
+                (Sing n) -> (Sing n) -> SFoo (Foo n n :: Foo a b)
     type instance Sing @(Foo a b) = SFoo
     instance (SingKind a, SingKind b) => SingKind (Foo a b) where
       type Demote (Foo a b) = Foo (Demote a) (Demote b)
diff --git a/tests/compile-and-dump/Singletons/Maybe.ghc88.template b/tests/compile-and-dump/Singletons/Maybe.ghc88.template
index 80c25866..bf7aabe1 100644
--- a/tests/compile-and-dump/Singletons/Maybe.ghc88.template
+++ b/tests/compile-and-dump/Singletons/Maybe.ghc88.template
@@ -66,8 +66,8 @@ Singletons/Maybe.hs:(0,0)-(0,0): Splicing declarations
       type (==) a b = Equals_0123456789876543210 a b
     data SMaybe :: forall a. Maybe a -> GHC.Types.Type
       where
-        SNothing :: SMaybe Nothing
-        SJust :: forall a (n :: a). (Sing (n :: a)) -> SMaybe (Just n)
+        SNothing :: forall a. SMaybe (Nothing :: Maybe a)
+        SJust :: forall a (n :: a). (Sing n) -> SMaybe (Just n :: Maybe a)
     type instance Sing @(Maybe a) = SMaybe
     instance SingKind a => SingKind (Maybe a) where
       type Demote (Maybe a) = Maybe (Demote a)
diff --git a/tests/compile-and-dump/Singletons/Nat.ghc88.template b/tests/compile-and-dump/Singletons/Nat.ghc88.template
index d6cd6be4..5dfed3c0 100644
--- a/tests/compile-and-dump/Singletons/Nat.ghc88.template
+++ b/tests/compile-and-dump/Singletons/Nat.ghc88.template
@@ -161,8 +161,8 @@ Singletons/Nat.hs:(0,0)-(0,0): Splicing declarations
       sing = (singFun1 @(PlusSym1 (d :: Nat))) (sPlus (sing @d))
     data SNat :: Nat -> GHC.Types.Type
       where
-        SZero :: SNat Zero
-        SSucc :: forall (n :: Nat). (Sing (n :: Nat)) -> SNat (Succ n)
+        SZero :: SNat (Zero :: Nat)
+        SSucc :: forall (n :: Nat). (Sing n) -> SNat (Succ n :: Nat)
     type instance Sing @Nat = SNat
     instance SingKind Nat where
       type Demote Nat = Nat
diff --git a/tests/compile-and-dump/Singletons/Operators.ghc88.template b/tests/compile-and-dump/Singletons/Operators.ghc88.template
index 8c99e774..3150dfc3 100644
--- a/tests/compile-and-dump/Singletons/Operators.ghc88.template
+++ b/tests/compile-and-dump/Singletons/Operators.ghc88.template
@@ -97,9 +97,9 @@ Singletons/Operators.hs:(0,0)-(0,0): Splicing declarations
       sing = (singFun1 @ChildSym0) sChild
     data SFoo :: Foo -> GHC.Types.Type
       where
-        SFLeaf :: SFoo FLeaf
+        SFLeaf :: SFoo (FLeaf :: Foo)
         (:%+:) :: forall (n :: Foo) (n :: Foo).
-                  (Sing (n :: Foo)) -> (Sing (n :: Foo)) -> SFoo ((:+:) n n)
+                  (Sing n) -> (Sing n) -> SFoo ((:+:) n n :: Foo)
     type instance Sing @Foo = SFoo
     instance SingKind Foo where
       type Demote Foo = Foo
diff --git a/tests/compile-and-dump/Singletons/OrdDeriving.ghc88.template b/tests/compile-and-dump/Singletons/OrdDeriving.ghc88.template
index e931a301..ac819e12 100644
--- a/tests/compile-and-dump/Singletons/OrdDeriving.ghc88.template
+++ b/tests/compile-and-dump/Singletons/OrdDeriving.ghc88.template
@@ -444,8 +444,8 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations
       type (==) a b = Equals_0123456789876543210 a b
     data SNat :: Nat -> GHC.Types.Type
       where
-        SZero :: SNat Zero
-        SSucc :: forall (n :: Nat). (Sing (n :: Nat)) -> SNat (Succ n)
+        SZero :: SNat (Zero :: Nat)
+        SSucc :: forall (n :: Nat). (Sing n) -> SNat (Succ n :: Nat)
     type instance Sing @Nat = SNat
     instance SingKind Nat where
       type Demote Nat = Nat
@@ -458,29 +458,29 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations
     data SFoo :: forall a b c d. Foo a b c d -> GHC.Types.Type
       where
         SA :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d).
-              (Sing (n :: a))
-              -> (Sing (n :: b))
-                 -> (Sing (n :: c)) -> (Sing (n :: d)) -> SFoo (A n n n n)
+              (Sing n)
+              -> (Sing n)
+                 -> (Sing n) -> (Sing n) -> SFoo (A n n n n :: Foo a b c d)
         SB :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d).
-              (Sing (n :: a))
-              -> (Sing (n :: b))
-                 -> (Sing (n :: c)) -> (Sing (n :: d)) -> SFoo (B n n n n)
+              (Sing n)
+              -> (Sing n)
+                 -> (Sing n) -> (Sing n) -> SFoo (B n n n n :: Foo a b c d)
         SC :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d).
-              (Sing (n :: a))
-              -> (Sing (n :: b))
-                 -> (Sing (n :: c)) -> (Sing (n :: d)) -> SFoo (C n n n n)
+              (Sing n)
+              -> (Sing n)
+                 -> (Sing n) -> (Sing n) -> SFoo (C n n n n :: Foo a b c d)
         SD :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d).
-              (Sing (n :: a))
-              -> (Sing (n :: b))
-                 -> (Sing (n :: c)) -> (Sing (n :: d)) -> SFoo (D n n n n)
+              (Sing n)
+              -> (Sing n)
+                 -> (Sing n) -> (Sing n) -> SFoo (D n n n n :: Foo a b c d)
         SE :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d).
-              (Sing (n :: a))
-              -> (Sing (n :: b))
-                 -> (Sing (n :: c)) -> (Sing (n :: d)) -> SFoo (E n n n n)
+              (Sing n)
+              -> (Sing n)
+                 -> (Sing n) -> (Sing n) -> SFoo (E n n n n :: Foo a b c d)
         SF :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d).
-              (Sing (n :: a))
-              -> (Sing (n :: b))
-                 -> (Sing (n :: c)) -> (Sing (n :: d)) -> SFoo (F n n n n)
+              (Sing n)
+              -> (Sing n)
+                 -> (Sing n) -> (Sing n) -> SFoo (F n n n n :: Foo a b c d)
     type instance Sing @(Foo a b c d) = SFoo
     instance (SingKind a, SingKind b, SingKind c, SingKind d) =>
              SingKind (Foo a b c d) where
diff --git a/tests/compile-and-dump/Singletons/PatternMatching.ghc88.template b/tests/compile-and-dump/Singletons/PatternMatching.ghc88.template
index 43e241e4..6af64abb 100644
--- a/tests/compile-and-dump/Singletons/PatternMatching.ghc88.template
+++ b/tests/compile-and-dump/Singletons/PatternMatching.ghc88.template
@@ -124,7 +124,7 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations
     data SPair :: forall a b. Pair a b -> GHC.Types.Type
       where
         SPair :: forall a b (n :: a) (n :: b).
-                 (Sing (n :: a)) -> (Sing (n :: b)) -> SPair (Pair n n)
+                 (Sing n) -> (Sing n) -> SPair (Pair n n :: Pair a b)
     type instance Sing @(Pair a b) = SPair
     instance (SingKind a, SingKind b) => SingKind (Pair a b) where
       type Demote (Pair a b) = Pair (Demote a) (Demote b)
diff --git a/tests/compile-and-dump/Singletons/PolyKindsApp.ghc88.template b/tests/compile-and-dump/Singletons/PolyKindsApp.ghc88.template
index a119d01c..eb58336a 100644
--- a/tests/compile-and-dump/Singletons/PolyKindsApp.ghc88.template
+++ b/tests/compile-and-dump/Singletons/PolyKindsApp.ghc88.template
@@ -9,4 +9,5 @@ Singletons/PolyKindsApp.hs:(0,0)-(0,0): Splicing declarations
     class PCls (a :: k -> Type) where
       type Fff :: (a :: k -> Type) (b :: k)
     class SCls (a :: k -> Type) where
-      sFff :: forall b. Sing (FffSym0 :: (a :: k -> Type) (b :: k))
+      sFff ::
+        forall (b :: k). Sing (FffSym0 :: (a :: k -> Type) (b :: k))
diff --git a/tests/compile-and-dump/Singletons/Records.ghc88.template b/tests/compile-and-dump/Singletons/Records.ghc88.template
index d9d393f8..5898869c 100644
--- a/tests/compile-and-dump/Singletons/Records.ghc88.template
+++ b/tests/compile-and-dump/Singletons/Records.ghc88.template
@@ -52,8 +52,8 @@ Singletons/Records.hs:(0,0)-(0,0): Splicing declarations
     data SRecord :: forall a. Record a -> GHC.Types.Type
       where
         SMkRecord :: forall a (n :: a) (n :: Bool).
-                     {sField1 :: (Sing (n :: a)), sField2 :: (Sing (n :: Bool))}
-                     -> SRecord (MkRecord n n)
+                     {sField1 :: (Sing n), sField2 :: (Sing n)}
+                     -> SRecord (MkRecord n n :: Record a)
     type instance Sing @(Record a) = SRecord
     instance SingKind a => SingKind (Record a) where
       type Demote (Record a) = Record (Demote a)
diff --git a/tests/compile-and-dump/Singletons/ShowDeriving.ghc88.template b/tests/compile-and-dump/Singletons/ShowDeriving.ghc88.template
index bec87044..832d791c 100644
--- a/tests/compile-and-dump/Singletons/ShowDeriving.ghc88.template
+++ b/tests/compile-and-dump/Singletons/ShowDeriving.ghc88.template
@@ -270,7 +270,8 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations
     infixl 5 :%&:
     infixl 5 :%*:
     infixl 5 `SMkFoo2b`
-    data SFoo1 :: Foo1 -> GHC.Types.Type where SMkFoo1 :: SFoo1 MkFoo1
+    data SFoo1 :: Foo1 -> GHC.Types.Type
+      where SMkFoo1 :: SFoo1 (MkFoo1 :: Foo1)
     type instance Sing @Foo1 = SFoo1
     instance SingKind Foo1 where
       type Demote Foo1 = Foo1
@@ -279,13 +280,13 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations
     data SFoo2 :: forall a. Foo2 a -> GHC.Types.Type
       where
         SMkFoo2a :: forall a (n :: a) (n :: a).
-                    (Sing (n :: a)) -> (Sing (n :: a)) -> SFoo2 (MkFoo2a n n)
+                    (Sing n) -> (Sing n) -> SFoo2 (MkFoo2a n n :: Foo2 a)
         SMkFoo2b :: forall a (n :: a) (n :: a).
-                    (Sing (n :: a)) -> (Sing (n :: a)) -> SFoo2 (MkFoo2b n n)
+                    (Sing n) -> (Sing n) -> SFoo2 (MkFoo2b n n :: Foo2 a)
         (:%*:) :: forall a (n :: a) (n :: a).
-                  (Sing (n :: a)) -> (Sing (n :: a)) -> SFoo2 ((:*:) n n)
+                  (Sing n) -> (Sing n) -> SFoo2 ((:*:) n n :: Foo2 a)
         (:%&:) :: forall a (n :: a) (n :: a).
-                  (Sing (n :: a)) -> (Sing (n :: a)) -> SFoo2 ((:&:) n n)
+                  (Sing n) -> (Sing n) -> SFoo2 ((:&:) n n :: Foo2 a)
     type instance Sing @(Foo2 a) = SFoo2
     instance SingKind a => SingKind (Foo2 a) where
       type Demote (Foo2 a) = Foo2 (Demote a)
@@ -308,8 +309,8 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations
     data SFoo3 :: Foo3 -> GHC.Types.Type
       where
         SMkFoo3 :: forall (n :: Bool) (n :: Bool).
-                   {sGetFoo3a :: (Sing (n :: Bool)), %*** :: (Sing (n :: Bool))}
-                   -> SFoo3 (MkFoo3 n n)
+                   {sGetFoo3a :: (Sing n), %*** :: (Sing n)}
+                   -> SFoo3 (MkFoo3 n n :: Foo3)
     type instance Sing @Foo3 = SFoo3
     instance SingKind Foo3 where
       type Demote Foo3 = Foo3
diff --git a/tests/compile-and-dump/Singletons/StandaloneDeriving.ghc88.template b/tests/compile-and-dump/Singletons/StandaloneDeriving.ghc88.template
index cf58e99a..cb730334 100644
--- a/tests/compile-and-dump/Singletons/StandaloneDeriving.ghc88.template
+++ b/tests/compile-and-dump/Singletons/StandaloneDeriving.ghc88.template
@@ -241,7 +241,7 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations
     data ST :: forall a b. T a b -> GHC.Types.Type
       where
         (:%*:) :: forall a b (n :: a) (n :: b).
-                  (Sing (n :: a)) -> (Sing (n :: b)) -> ST ((:*:) n n)
+                  (Sing n) -> (Sing n) -> ST ((:*:) n n :: T a b)
     type instance Sing @(T a b) = ST
     instance (SingKind a, SingKind b) => SingKind (T a b) where
       type Demote (T a b) = T (Demote a) (Demote b)
@@ -251,8 +251,8 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations
             (,) (SomeSing c) (SomeSing c) -> SomeSing (((:%*:) c) c) }
     data SS :: S -> GHC.Types.Type
       where
-        SS1 :: SS S1
-        SS2 :: SS S2
+        SS1 :: SS (S1 :: S)
+        SS2 :: SS (S2 :: S)
     type instance Sing @S = SS
     instance SingKind S where
       type Demote S = S
diff --git a/tests/compile-and-dump/Singletons/Star.ghc88.template b/tests/compile-and-dump/Singletons/Star.ghc88.template
index aa8853c6..906fc7ca 100644
--- a/tests/compile-and-dump/Singletons/Star.ghc88.template
+++ b/tests/compile-and-dump/Singletons/Star.ghc88.template
@@ -141,12 +141,12 @@ Singletons/Star.hs:0:0:: Splicing declarations
       type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
     data SRep :: Type -> Type
       where
-        SNat :: SRep Nat
-        SInt :: SRep Int
-        SString :: SRep String
-        SMaybe :: forall (n :: Type). (Sing (n :: Type)) -> SRep (Maybe n)
+        SNat :: SRep (Nat :: Type)
+        SInt :: SRep (Int :: Type)
+        SString :: SRep (String :: Type)
+        SMaybe :: forall (n :: Type). (Sing n) -> SRep (Maybe n :: Type)
         SVec :: forall (n :: Type) (n :: Nat).
-                (Sing (n :: Type)) -> (Sing (n :: Nat)) -> SRep (Vec n n)
+                (Sing n) -> (Sing n) -> SRep (Vec n n :: Type)
     type instance Sing @Type = SRep
     instance SingKind Type where
       type Demote Type = Rep
diff --git a/tests/compile-and-dump/Singletons/T159.ghc88.template b/tests/compile-and-dump/Singletons/T159.ghc88.template
index fb5dec3d..318961e8 100644
--- a/tests/compile-and-dump/Singletons/T159.ghc88.template
+++ b/tests/compile-and-dump/Singletons/T159.ghc88.template
@@ -9,12 +9,12 @@ Singletons/T159.hs:0:0:: Splicing declarations
     type FSym0 = 'F
     data ST0 :: T0 -> GHC.Types.Type
       where
-        SA :: ST0 'A
-        SB :: ST0 'B
-        SC :: ST0 'C
-        SD :: ST0 'D
-        SE :: ST0 'E
-        SF :: ST0 'F
+        SA :: ST0 ('A :: T0)
+        SB :: ST0 ('B :: T0)
+        SC :: ST0 ('C :: T0)
+        SD :: ST0 ('D :: T0)
+        SE :: ST0 ('E :: T0)
+        SF :: ST0 ('F :: T0)
     type instance Sing @T0 = ST0
     instance SingKind T0 where
       type Demote T0 = T0
@@ -87,11 +87,11 @@ Singletons/T159.hs:0:0:: Splicing declarations
     infixr 5 :&&@#@$
     data ST1 :: T1 -> GHC.Types.Type
       where
-        SN1 :: ST1 'N1
+        SN1 :: ST1 ('N1 :: T1)
         SC1 :: forall (n :: T0) (n :: T1).
-               (Sing (n :: T0)) -> (Sing (n :: T1)) -> ST1 ('C1 n n)
+               (Sing n) -> (Sing n) -> ST1 ('C1 n n :: T1)
         (:%&&) :: forall (n :: T0) (n :: T1).
-                  (Sing (n :: T0)) -> (Sing (n :: T1)) -> ST1 ('(:&&) n n)
+                  (Sing n) -> (Sing n) -> ST1 ('(:&&) n n :: T1)
     type instance Sing @T1 = ST1
     instance SingKind T1 where
       type Demote T1 = T1
@@ -185,11 +185,11 @@ Singletons/T159.hs:(0,0)-(0,0): Splicing declarations
     infixr 5 `SC2`
     data ST2 :: T2 -> GHC.Types.Type
       where
-        SN2 :: ST2 N2
+        SN2 :: ST2 (N2 :: T2)
         SC2 :: forall (n :: T0) (n :: T2).
-               (Sing (n :: T0)) -> (Sing (n :: T2)) -> ST2 (C2 n n)
+               (Sing n) -> (Sing n) -> ST2 (C2 n n :: T2)
         (:%||) :: forall (n :: T0) (n :: T2).
-                  (Sing (n :: T0)) -> (Sing (n :: T2)) -> ST2 ((:||) n n)
+                  (Sing n) -> (Sing n) -> ST2 ((:||) n n :: T2)
     type instance Sing @T2 = ST2
     instance SingKind T2 where
       type Demote T2 = T2
diff --git a/tests/compile-and-dump/Singletons/T163.ghc88.template b/tests/compile-and-dump/Singletons/T163.ghc88.template
index 2dfa342c..bca88173 100644
--- a/tests/compile-and-dump/Singletons/T163.ghc88.template
+++ b/tests/compile-and-dump/Singletons/T163.ghc88.template
@@ -26,8 +26,8 @@ Singletons/T163.hs:0:0:: Splicing declarations
     type instance Apply RSym0 t0123456789876543210 = R t0123456789876543210
     data (%+) :: forall a b. (+) a b -> GHC.Types.Type
       where
-        SL :: forall a (n :: a). (Sing (n :: a)) -> (%+) (L n)
-        SR :: forall b (n :: b). (Sing (n :: b)) -> (%+) (R n)
+        SL :: forall a b (n :: a). (Sing n) -> (%+) (L n :: (+) a b)
+        SR :: forall a b (n :: b). (Sing n) -> (%+) (R n :: (+) a b)
     type instance Sing @((+) a b) = (%+)
     instance (SingKind a, SingKind b) => SingKind ((+) a b) where
       type Demote ((+) a b) = (+) (Demote a) (Demote b)
diff --git a/tests/compile-and-dump/Singletons/T178.ghc88.template b/tests/compile-and-dump/Singletons/T178.ghc88.template
index 4ff427cd..942fb031 100644
--- a/tests/compile-and-dump/Singletons/T178.ghc88.template
+++ b/tests/compile-and-dump/Singletons/T178.ghc88.template
@@ -103,9 +103,9 @@ Singletons/T178.hs:(0,0)-(0,0): Splicing declarations
     sEmpty = Data.Singletons.Prelude.Instances.SNil
     data SOcc :: Occ -> GHC.Types.Type
       where
-        SStr :: SOcc Str
-        SOpt :: SOcc Opt
-        SMany :: SOcc Many
+        SStr :: SOcc (Str :: Occ)
+        SOpt :: SOcc (Opt :: Occ)
+        SMany :: SOcc (Many :: Occ)
     type instance Sing @Occ = SOcc
     instance SingKind Occ where
       type Demote Occ = Occ
diff --git a/tests/compile-and-dump/Singletons/T190.ghc88.template b/tests/compile-and-dump/Singletons/T190.ghc88.template
index 0ce00fed..f420ecb2 100644
--- a/tests/compile-and-dump/Singletons/T190.ghc88.template
+++ b/tests/compile-and-dump/Singletons/T190.ghc88.template
@@ -117,7 +117,7 @@ Singletons/T190.hs:0:0:: Splicing declarations
       Equals_0123456789876543210 (_ :: T) (_ :: T) = FalseSym0
     instance PEq T where
       type (==) a b = Equals_0123456789876543210 a b
-    data ST :: T -> GHC.Types.Type where ST :: ST T
+    data ST :: T -> GHC.Types.Type where ST :: ST (T :: T)
     type instance Sing @T = ST
     instance SingKind T where
       type Demote T = T
diff --git a/tests/compile-and-dump/Singletons/T197b.ghc88.template b/tests/compile-and-dump/Singletons/T197b.ghc88.template
index 379f1acf..86d6d165 100644
--- a/tests/compile-and-dump/Singletons/T197b.ghc88.template
+++ b/tests/compile-and-dump/Singletons/T197b.ghc88.template
@@ -59,7 +59,7 @@ Singletons/T197b.hs:(0,0)-(0,0): Splicing declarations
     data (%:*:) :: forall a b. (:*:) a b -> GHC.Types.Type
       where
         (:%*:) :: forall a b (n :: a) (n :: b).
-                  (Sing (n :: a)) -> (Sing (n :: b)) -> (%:*:) ((:*:) n n)
+                  (Sing n) -> (Sing n) -> (%:*:) ((:*:) n n :: (:*:) a b)
     type instance Sing @((:*:) a b) = (%:*:)
     instance (SingKind a, SingKind b) => SingKind ((:*:) a b) where
       type Demote ((:*:) a b) = (:*:) (Demote a) (Demote b)
@@ -70,7 +70,7 @@ Singletons/T197b.hs:(0,0)-(0,0): Splicing declarations
     data SPair :: forall a b. Pair a b -> GHC.Types.Type
       where
         SMkPair :: forall a b (n :: a) (n :: b).
-                   (Sing (n :: a)) -> (Sing (n :: b)) -> SPair (MkPair n n)
+                   (Sing n) -> (Sing n) -> SPair (MkPair n n :: Pair a b)
     type instance Sing @(Pair a b) = SPair
     instance (SingKind a, SingKind b) => SingKind (Pair a b) where
       type Demote (Pair a b) = Pair (Demote a) (Demote b)
diff --git a/tests/compile-and-dump/Singletons/T200.ghc88.template b/tests/compile-and-dump/Singletons/T200.ghc88.template
index 225c857d..83c7f6d1 100644
--- a/tests/compile-and-dump/Singletons/T200.ghc88.template
+++ b/tests/compile-and-dump/Singletons/T200.ghc88.template
@@ -135,13 +135,11 @@ Singletons/T200.hs:(0,0)-(0,0): Splicing declarations
     data SErrorMessage :: ErrorMessage -> GHC.Types.Type
       where
         (:%$$:) :: forall (n :: ErrorMessage) (n :: ErrorMessage).
-                   (Sing (n :: ErrorMessage))
-                   -> (Sing (n :: ErrorMessage)) -> SErrorMessage ((:$$:) n n)
+                   (Sing n) -> (Sing n) -> SErrorMessage ((:$$:) n n :: ErrorMessage)
         (:%<>:) :: forall (n :: ErrorMessage) (n :: ErrorMessage).
-                   (Sing (n :: ErrorMessage))
-                   -> (Sing (n :: ErrorMessage)) -> SErrorMessage ((:<>:) n n)
+                   (Sing n) -> (Sing n) -> SErrorMessage ((:<>:) n n :: ErrorMessage)
         SEM :: forall (n :: [Bool]).
-               (Sing (n :: [Bool])) -> SErrorMessage (EM n)
+               (Sing n) -> SErrorMessage (EM n :: ErrorMessage)
     type instance Sing @ErrorMessage = SErrorMessage
     instance SingKind ErrorMessage where
       type Demote ErrorMessage = ErrorMessage
diff --git a/tests/compile-and-dump/Singletons/T209.ghc88.template b/tests/compile-and-dump/Singletons/T209.ghc88.template
index b467e922..d5263dde 100644
--- a/tests/compile-and-dump/Singletons/T209.ghc88.template
+++ b/tests/compile-and-dump/Singletons/T209.ghc88.template
@@ -69,7 +69,7 @@ Singletons/T209.hs:(0,0)-(0,0): Splicing declarations
              SingI (MSym2 (d :: a) (d :: b) :: (~>) Bool Bool) where
       sing
         = (singFun1 @(MSym2 (d :: a) (d :: b))) ((sM (sing @d)) (sing @d))
-    data SHm :: Hm -> GHC.Types.Type where SHm :: SHm Hm
+    data SHm :: Hm -> GHC.Types.Type where SHm :: SHm (Hm :: Hm)
     type instance Sing @Hm = SHm
     instance SingKind Hm where
       type Demote Hm = Hm
diff --git a/tests/compile-and-dump/Singletons/T249.ghc88.template b/tests/compile-and-dump/Singletons/T249.ghc88.template
index b1487fba..5fb03d18 100644
--- a/tests/compile-and-dump/Singletons/T249.ghc88.template
+++ b/tests/compile-and-dump/Singletons/T249.ghc88.template
@@ -42,7 +42,8 @@ Singletons/T249.hs:(0,0)-(0,0): Splicing declarations
     type instance Apply MkFoo3Sym0 t0123456789876543210 = MkFoo3 t0123456789876543210
     data SFoo1 :: forall a. Foo1 a -> Type
       where
-        SMkFoo1 :: forall a (n :: a). (Sing (n :: a)) -> SFoo1 (MkFoo1 n)
+        SMkFoo1 :: forall a (n :: a).
+                   (Sing n) -> SFoo1 (MkFoo1 n :: Foo1 a)
     type instance Sing @(Foo1 a) = SFoo1
     instance SingKind a => SingKind (Foo1 a) where
       type Demote (Foo1 a) = Foo1 (Demote a)
@@ -52,7 +53,8 @@ Singletons/T249.hs:(0,0)-(0,0): Splicing declarations
             SomeSing c -> SomeSing (SMkFoo1 c) }
     data SFoo2 :: forall a. Foo2 a -> Type
       where
-        SMkFoo2 :: forall x (n :: x). (Sing (n :: x)) -> SFoo2 (MkFoo2 n)
+        SMkFoo2 :: forall x (n :: x).
+                   (Sing n) -> SFoo2 (MkFoo2 n :: Foo2 x)
     type instance Sing @(Foo2 a) = SFoo2
     instance SingKind a => SingKind (Foo2 a) where
       type Demote (Foo2 a) = Foo2 (Demote a)
@@ -62,7 +64,8 @@ Singletons/T249.hs:(0,0)-(0,0): Splicing declarations
             SomeSing c -> SomeSing (SMkFoo2 c) }
     data SFoo3 :: forall a. Foo3 a -> Type
       where
-        SMkFoo3 :: forall x (n :: x). (Sing (n :: x)) -> SFoo3 (MkFoo3 n)
+        SMkFoo3 :: forall x (n :: x).
+                   (Sing n) -> SFoo3 (MkFoo3 n :: Foo3 x)
     type instance Sing @(Foo3 a) = SFoo3
     instance SingKind a => SingKind (Foo3 a) where
       type Demote (Foo3 a) = Foo3 (Demote a)
diff --git a/tests/compile-and-dump/Singletons/T271.ghc88.template b/tests/compile-and-dump/Singletons/T271.ghc88.template
index 7cc7b24c..720e9c80 100644
--- a/tests/compile-and-dump/Singletons/T271.ghc88.template
+++ b/tests/compile-and-dump/Singletons/T271.ghc88.template
@@ -101,8 +101,9 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations
       type (==) a b = Equals_0123456789876543210 a b
     data SConstant :: forall a b. Constant a b -> Type
       where
-        SConstant :: forall a (n :: a).
-                     (Sing (n :: a)) -> SConstant (Constant n)
+        SConstant :: forall (a :: Type) (b :: Type) (n :: a).
+                     (Sing n)
+                     -> SConstant (Constant n :: Constant (a :: Type) (b :: Type))
     type instance Sing @(Constant a b) = SConstant
     instance (SingKind a, SingKind b) => SingKind (Constant a b) where
       type Demote (Constant a b) = Constant (Demote a) (Demote b)
@@ -113,7 +114,7 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations
     data SIdentity :: forall a. Identity a -> Type
       where
         SIdentity :: forall a (n :: a).
-                     (Sing (n :: a)) -> SIdentity (Identity n)
+                     (Sing n) -> SIdentity (Identity n :: Identity a)
     type instance Sing @(Identity a) = SIdentity
     instance SingKind a => SingKind (Identity a) where
       type Demote (Identity a) = Identity (Demote a)
diff --git a/tests/compile-and-dump/Singletons/T297.ghc88.template b/tests/compile-and-dump/Singletons/T297.ghc88.template
index c91e27fc..ce74f201 100644
--- a/tests/compile-and-dump/Singletons/T297.ghc88.template
+++ b/tests/compile-and-dump/Singletons/T297.ghc88.template
@@ -49,7 +49,9 @@ Singletons/T297.hs:(0,0)-(0,0): Splicing declarations
     instance SingI FSym0 where
       sing = (singFun1 @FSym0) sF
     data SMyProxy :: forall a. MyProxy a -> Type
-      where SMyProxy :: SMyProxy MyProxy
+      where
+        SMyProxy :: forall (a :: Type).
+                    SMyProxy (MyProxy :: MyProxy (a :: Type))
     type instance Sing @(MyProxy a) = SMyProxy
     instance SingKind a => SingKind (MyProxy a) where
       type Demote (MyProxy a) = MyProxy (Demote a)
diff --git a/tests/compile-and-dump/Singletons/T332.ghc88.template b/tests/compile-and-dump/Singletons/T332.ghc88.template
index bd121148..72c44f1a 100644
--- a/tests/compile-and-dump/Singletons/T332.ghc88.template
+++ b/tests/compile-and-dump/Singletons/T332.ghc88.template
@@ -46,7 +46,8 @@ Singletons/T332.hs:(0,0)-(0,0): Splicing declarations
     sB SMkBar = STuple0
     instance SingI (BSym0 :: (~>) Bar ()) where
       sing = (singFun1 @BSym0) sB
-    data SBar :: Bar -> GHC.Types.Type where SMkBar :: SBar MkBar
+    data SBar :: Bar -> GHC.Types.Type
+      where SMkBar :: SBar (MkBar :: Bar)
     type instance Sing @Bar = SBar
     instance SingKind Bar where
       type Demote Bar = Bar
diff --git a/tests/compile-and-dump/Singletons/T371.ghc88.template b/tests/compile-and-dump/Singletons/T371.ghc88.template
index 605d3898..a7b33d67 100644
--- a/tests/compile-and-dump/Singletons/T371.ghc88.template
+++ b/tests/compile-and-dump/Singletons/T371.ghc88.template
@@ -117,8 +117,9 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations
       type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
     data SX :: forall a. X a -> Type
       where
-        SX1 :: SX X1
-        SX2 :: forall a (n :: Y a). (Sing (n :: Y a)) -> SX (X2 n)
+        SX1 :: forall (a :: Type). SX (X1 :: X (a :: Type))
+        SX2 :: forall (a :: Type) (n :: Y a).
+               (Sing n) -> SX (X2 n :: X (a :: Type))
     type instance Sing @(X a) = SX
     instance SingKind a => SingKind (X a) where
       type Demote (X a) = X (Demote a)
@@ -130,8 +131,9 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations
             SomeSing c -> SomeSing (SX2 c) }
     data SY :: forall a. Y a -> Type
       where
-        SY1 :: SY Y1
-        SY2 :: forall a (n :: X a). (Sing (n :: X a)) -> SY (Y2 n)
+        SY1 :: forall (a :: Type). SY (Y1 :: Y (a :: Type))
+        SY2 :: forall (a :: Type) (n :: X a).
+               (Sing n) -> SY (Y2 n :: Y (a :: Type))
     type instance Sing @(Y a) = SY
     instance SingKind a => SingKind (Y a) where
       type Demote (Y a) = Y (Demote a)
diff --git a/tests/compile-and-dump/Singletons/T378a.ghc88.template b/tests/compile-and-dump/Singletons/T378a.ghc88.template
new file mode 100644
index 00000000..06c81c51
--- /dev/null
+++ b/tests/compile-and-dump/Singletons/T378a.ghc88.template
@@ -0,0 +1,81 @@
+Singletons/T378a.hs:(0,0)-(0,0): Splicing declarations
+    singletons
+      [d| constBA :: forall b a. a -> b -> a
+          constBA x _ = x
+          
+          data Proxy :: forall k. k -> Type
+            where
+              Proxy1 :: Proxy a
+              Proxy2 :: Proxy (a :: k)
+              Proxy3 :: forall a. Proxy a
+              Proxy4 :: forall k (a :: k). Proxy a |]
+  ======>
+    constBA :: forall b a. a -> b -> a
+    constBA x _ = x
+    data Proxy :: forall k. k -> Type
+      where
+        Proxy1 :: Proxy a
+        Proxy2 :: Proxy (a :: k)
+        Proxy3 :: forall a. Proxy a
+        Proxy4 :: forall k (a :: k). Proxy a
+    type Proxy1Sym0 = Proxy1
+    type Proxy2Sym0 = Proxy2
+    type Proxy3Sym0 = Proxy3
+    type Proxy4Sym0 = Proxy4
+    type ConstBASym2 (a0123456789876543210 :: a0123456789876543210) (a0123456789876543210 :: b0123456789876543210) =
+        ConstBA a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings (ConstBASym1 a0123456789876543210) where
+      suppressUnusedWarnings = snd (((,) ConstBASym1KindInference) ())
+    data ConstBASym1 (a0123456789876543210 :: a0123456789876543210) :: forall b0123456789876543210.
+                                                                       (~>) b0123456789876543210 a0123456789876543210
+      where
+        ConstBASym1KindInference :: forall a0123456789876543210
+                                           a0123456789876543210
+                                           arg. SameKind (Apply (ConstBASym1 a0123456789876543210) arg) (ConstBASym2 a0123456789876543210 arg) =>
+                                    ConstBASym1 a0123456789876543210 a0123456789876543210
+    type instance Apply (ConstBASym1 a0123456789876543210) a0123456789876543210 = ConstBA a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings ConstBASym0 where
+      suppressUnusedWarnings = snd (((,) ConstBASym0KindInference) ())
+    data ConstBASym0 :: forall a0123456789876543210
+                               b0123456789876543210.
+                        (~>) a0123456789876543210 ((~>) b0123456789876543210 a0123456789876543210)
+      where
+        ConstBASym0KindInference :: forall a0123456789876543210
+                                           arg. SameKind (Apply ConstBASym0 arg) (ConstBASym1 arg) =>
+                                    ConstBASym0 a0123456789876543210
+    type instance Apply ConstBASym0 a0123456789876543210 = ConstBASym1 a0123456789876543210
+    type family ConstBA (a :: a) (a :: b) :: a where
+      ConstBA x _ = x
+    sConstBA ::
+      forall b a (t :: a) (t :: b).
+      Sing t -> Sing t -> Sing (Apply (Apply ConstBASym0 t) t :: a)
+    sConstBA (sX :: Sing x) _ = sX
+    instance SingI (ConstBASym0 :: (~>) a ((~>) b a)) where
+      sing = (singFun2 @ConstBASym0) sConstBA
+    instance SingI d => SingI (ConstBASym1 (d :: a) :: (~>) b a) where
+      sing = (singFun1 @(ConstBASym1 (d :: a))) (sConstBA (sing @d))
+    data SProxy :: forall a. Proxy a -> Type
+      where
+        SProxy1 :: forall a. SProxy (Proxy1 :: Proxy a)
+        SProxy2 :: forall k (a :: k). SProxy (Proxy2 :: Proxy (a :: k))
+        SProxy3 :: forall a. SProxy (Proxy3 :: Proxy a)
+        SProxy4 :: forall k (a :: k). SProxy (Proxy4 :: Proxy a)
+    type instance Sing @(Proxy a) = SProxy
+    instance SingKind a => SingKind (Proxy a) where
+      type Demote (Proxy a) = Proxy (Demote a)
+      fromSing SProxy1 = Proxy1
+      fromSing SProxy2 = Proxy2
+      fromSing SProxy3 = Proxy3
+      fromSing SProxy4 = Proxy4
+      toSing Proxy1 = SomeSing SProxy1
+      toSing Proxy2 = SomeSing SProxy2
+      toSing Proxy3 = SomeSing SProxy3
+      toSing Proxy4 = SomeSing SProxy4
+    instance SingI Proxy1 where
+      sing = SProxy1
+    instance SingI Proxy2 where
+      sing = SProxy2
+    instance SingI Proxy3 where
+      sing = SProxy3
+    instance SingI Proxy4 where
+      sing = SProxy4
diff --git a/tests/compile-and-dump/Singletons/T378a.hs b/tests/compile-and-dump/Singletons/T378a.hs
new file mode 100644
index 00000000..f6a37807
--- /dev/null
+++ b/tests/compile-and-dump/Singletons/T378a.hs
@@ -0,0 +1,46 @@
+module T378a where
+
+import Data.Kind
+import Data.Singletons.Prelude hiding (Proxy(..))
+import Data.Singletons.TH hiding (Proxy(..))
+
+$(singletons [d|
+  constBA :: forall b a. a -> b -> a
+  constBA x _ = x
+
+  data Proxy :: forall k. k -> Type where
+    Proxy1 :: Proxy a
+    Proxy2 :: Proxy (a :: k)
+    Proxy3 :: forall a. Proxy a
+    Proxy4 :: forall k (a :: k). Proxy a
+  |])
+
+ex1 :: [Bool]
+ex1 = [] @Bool
+
+sEx1 :: SList ('[] @Bool)
+sEx1 = SNil @Bool
+
+ex2 :: Bool
+ex2 = constBA @Ordering @Bool True LT
+
+sEx2 :: Sing (ConstBA True LT)
+sEx2 = sConstBA @Ordering @Bool STrue SLT
+
+proxyEx1, proxyEx2, proxyEx3, proxyEx4 :: Proxy True
+proxyEx1 = Proxy1 @True
+proxyEx2 = Proxy2 @Bool @True
+proxyEx3 = Proxy3 @True
+proxyEx4 = Proxy4 @Bool @True
+
+sProxyEx1 :: SProxy (Proxy1 @True)
+sProxyEx1 = SProxy1 @True
+
+sProxyEx2 :: SProxy (Proxy2 @Bool @True)
+sProxyEx2 = SProxy2 @Bool @True
+
+sProxyEx3 :: SProxy (Proxy3 @True)
+sProxyEx3 = SProxy3 @True
+
+sProxyEx4 :: SProxy (Proxy4 @Bool @True)
+sProxyEx4 = SProxy4 @Bool @True
diff --git a/tests/compile-and-dump/Singletons/TopLevelPatterns.ghc88.template b/tests/compile-and-dump/Singletons/TopLevelPatterns.ghc88.template
index 017dbcfa..17934170 100644
--- a/tests/compile-and-dump/Singletons/TopLevelPatterns.ghc88.template
+++ b/tests/compile-and-dump/Singletons/TopLevelPatterns.ghc88.template
@@ -30,8 +30,8 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations
     type instance Apply BarSym0 t0123456789876543210 = BarSym1 t0123456789876543210
     data SBool :: Bool -> GHC.Types.Type
       where
-        SFalse :: SBool False
-        STrue :: SBool True
+        SFalse :: SBool (False :: Bool)
+        STrue :: SBool (True :: Bool)
     type instance Sing @Bool = SBool
     instance SingKind Bool where
       type Demote Bool = Bool
@@ -42,7 +42,7 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations
     data SFoo :: Foo -> GHC.Types.Type
       where
         SBar :: forall (n :: Bool) (n :: Bool).
-                (Sing (n :: Bool)) -> (Sing (n :: Bool)) -> SFoo (Bar n n)
+                (Sing n) -> (Sing n) -> SFoo (Bar n n :: Foo)
     type instance Sing @Foo = SFoo
     instance SingKind Foo where
       type Demote Foo = Foo