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.

Author: RyanGlScott

Diff for: 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 for: 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
 ----------