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
#378 (comment),
but there are still other parts of #378 that remain to be fixed.

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

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
 ----------
 

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,28 +160,28 @@ 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 :: _
       sG x = x
 
 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
 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
 -}

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.