Make TH generate standalone kind signatures

This patch addresses chunk (2) in
#378 (comment)
by making the TH machinery generate standalone kind signatures
wherever possible, inching closer to the goal of preserving the order
of `forall`'s type variables in all promoted and singled code. I say
"inching" since this post does not quite get there (see the "Caveats"
section at the bottom of this commit message), but it comes very
close.

In brief, the TH machinery now generates SAKS for the following:

* Promoted top-level functions

  See `D.S.Promote.promoteLetDecRHS` for how this is implemented.

* Defunctionalization symbols

  SAKS provide a wonderful opportunity to clean up the implementation
  in `D.S.Promote.Defun`, which is currently somewhat crufty. The
  code used to jump through hoops in order to give
  defunctionalization symbols CUSKs, but now that we live in a
  post-CUSKs world, we can get rid of all the ad hoc-ness in
  `Note [Defunctionalization and dependent quantification]`.
  Instead, we now use a much simpler algorithm that only depends
  on whether the thing being defunctionalized has a SAK or not.
  See `Note [Defunctionalization game plan]` in `D.S.Promote.Defun`.

* Singled data type declarations

  If a data type's order of kind variables is known (e.g., if it was
  declared with a SAK), then the singled version of the data type
  will use a SAK to preserve the same kind variable order. See the
  code in `D.S.Single.Data.singDataD`.

* Promoted and singled class declarations

  Similarly, if the order of kind variables is known for a class `C`,
  then the TH machinery will generate SAKS for `PC` and `SC` to
  preserve the same kind variable order. See the code in
  `D.S.Promote.promoteClassDec` and `D.S.Single.singClassD`.

Naturally, lots of test cases' expected outputs change as a result of
this patch. See `Singletons.T378{a,b}` for some new (or altered)
cases that test new code paths.

-------------
-- Caveats --
-------------

Alas, not everything preserves the order of type variables after this
patch. Some notable exceptions are:

* `let`- or `where`-bound functions

  When promoting this function:

  ```hs
  f :: Bool
  f = let x = True
          g :: () -> Bool
          g _ = x
      in g ()
  ```

  The TH machinery will give the promoted `F` type family a SAK, but
  not the `G` type family. See
  `Note [No SAKs for let-decs with local variables]` in `D.S.Promote`
  for an explanation.

* Promoted class methods

  This class:

  ```hs
  class C (b :: Type) where
    m :: forall a. a -> b -> a
  ```

  Is promoted like so:

  ```hs
  class PC (b :: Type) where
    type M (x :: a) (y :: b) :: a
  ```

  The order of the variables `a` and `b` are different between the
  type of `m` and the kind of `M`. See
  `Note [Promoted class methods and kind variable ordering]` in
  `D.S.Promote`.

* Fully saturated defunctionalization symbols

  If you defunctionalize the `Id` type family, you'll generate two
  defunctionalization symbols:

  ```hs
  type IdSym0 :: forall a. a ~> a
  data IdSym0 f where ...

  type IdSym1 (x :: a) = Id x :: a
  ```

  Notice that unlike `IdSym0`, `IdSym1` (the "fully saturated"
  defunctionalization symbol) does _not_ have a SAK. This is because
  in general, giving fully saturated defunctionalization symbols SAKS
  can lead to kind errors. See
  `Note [No SAKs for fully saturated defunctionalization symbols]` in
  `D.S.Promote.Defun` for the sordid story.

.travis.yml

@@ -101,7 +101,7 @@ install:
     echo "source-repository-package"                            >> cabal.project
     echo "  type:     git"                                      >> cabal.project
     echo "  location: https://github.com/goldfirere/th-desugar" >> cabal.project
-    echo "  tag:      4e8f7d46954e690530c17b2eac9d302170ff994f" >> cabal.project
+    echo "  tag:      a6c902914ff6fcca021619dbb4919327fb98c404" >> cabal.project
     echo ""                                                     >> cabal.project
     echo "package th-desugar"                                   >> cabal.project
     echo "  tests:      False"                                  >> cabal.project
@@ -133,7 +133,7 @@ script:
     echo "source-repository-package"                            >> cabal.project
     echo "  type:     git"                                      >> cabal.project
     echo "  location: https://github.com/goldfirere/th-desugar" >> cabal.project
-    echo "  tag:      4e8f7d46954e690530c17b2eac9d302170ff994f" >> cabal.project
+    echo "  tag:      a6c902914ff6fcca021619dbb4919327fb98c404" >> cabal.project
     echo ""                                                     >> cabal.project
     echo "package th-desugar"                                   >> cabal.project
     echo "  tests:      False"                                  >> cabal.project

CHANGES.md

@@ -24,9 +24,14 @@ Changelog for singletons project
   Most TH functions are now polymorphic over `OptionsMonad` instead of
   `DsMonad`.
 * `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.
+  variables in type signatures during promotion and singling. See the
+  `Support for TypeApplications` section of the `README` for more details.
+
+  When generating type-level declarations in particular (e.g., promoted type
+  families or defunctionalization symbols), `singletons` will likely also
+  generate standalone kind signatures to preserve type variable order. As a
+  result, most `singletons` code that uses Template Haskell will require the
+  use of the `StandaloneKindSignatures` extension to work.
 * `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

@@ -58,6 +58,7 @@ following:
 * `PolyKinds`
 * `RankNTypes`
 * `ScopedTypeVariables`
+* `StandaloneKindSignatures`
 * `TemplateHaskell`
 * `TypeApplications`
 * `TypeFamilies`
@@ -599,15 +600,6 @@ The following constructs are fully supported:
 * functional dependencies (with limitations -- see below)
 * type families (with limitations -- see below)
 
-Higher-kinded type variables in `class`/`data` declarations must be annotated
-explicitly. This is due to GHC's handling of *complete
-user-specified kind signatures*, or [CUSKs](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#complete-user-supplied-kind-signatures-and-polymorphic-recursion).
-Briefly, `singletons` has a hard
-time conforming to the precise rules that GHC imposes around CUSKs and so
-needs a little help around kind inference here. See
-[this pull request](https://github.com/goldfirere/singletons/pull/171) for more
-background.
-
 `singletons` is slightly more conservative with respect to `deriving` than GHC is.
 The stock classes listed above (`Eq`, `Ord`, `Show`, `Bounded`, `Enum`, `Functor`,
 `Foldable`, and `Traversable`) are the only ones that `singletons` will derive
@@ -681,8 +673,11 @@ The following constructs are not supported:
 
 * datatypes that store arrows, `Nat`, or `Symbol`
 * literals (limited support)
+* rank-n types
+
+See the following sections for more details.
 
-Why are these out of reach?
+## Arrows, `Nat`, `Symbol`, and literals
 
 As described in the promotion paper, promotion of datatypes that store arrows is
 currently impossible. So if you have a declaration such as
@@ -704,6 +699,21 @@ This is the same line of reasoning that forbids the use of `Nat` or `Symbol`
 in datatype definitions. But, see [this bug
 report](https://github.com/goldfirere/singletons/issues/76) for a workaround.
 
+## Rank-n types
+
+`singletons` does not support type signatures that have higher-rank types.
+More precisely, the only types that can be promoted or singled are
+_vanilla_ types,  where a vanilla function type is a type that:
+
+1. Only uses a @forall@ at the top level, if used at all. That is to say, it
+   does not contain any nested or higher-rank @forall@s.
+
+2. Only uses a context (e.g., @c => ...@) at the top level, if used at all,
+   and only after the top-level @forall@ if one is present. That is to say,
+   it does not contain any nested or higher-rank contexts.
+
+3. Contains no visible dependent quantification.
+
 Support for `*`
 ---------------
 
@@ -740,30 +750,109 @@ singled to `sId STrue`. See
 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:
+type variables when promoting and singling certain constructors. These include:
+
+* Kind signatures of promoted top-level functions
+* Type signatures of singled top-level functions
+* Kind signatures of singled data type declarations
+* Type signatures of singled data constructors
+* Kind signatures of singled class declarations
+* Type signatures of singled class methods
+
+For example, consider this type signature:
 
 ```haskell
 const2 :: forall b a. a -> b -> a
 ```
 
-Will single to the following:
+The promoted version of `const` will have the following kind signature:
+
+```haskell
+type Const2 :: forall b a. a -> b -> a
+```
+
+The singled version of `const2` will have the following type signature:
 
 ```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.
+`Const2 @T1 @T2` or `sConst2 @T1 @T2`, since the signatures for `const2`, `Const2`,
+and `sConst2` all begin with `forall b a.`, in that order. Again, it is worth
+emphasizing that the TH machinery does not support promoting or singling
+`const2 @T1 @T2` directly, but you can write the type applications by hand if
+you so choose.
+
+`singletons` also has limited support for preserving the order of type variables
+for the following constructs:
+
+* Kind signatures of defunctionalization symbols.
+  The order of type variables is only guaranteed to be preserved if:
+
+  1. The thing being defunctionalized has a standalone type (or kind)
+     signature.
+  2. The type (or kind) signature of the thing being defunctionalized is
+     a vanilla type. (See the "Rank-n types" section above for what "vanilla"
+     means.)
+
+  If either of these conditions do not hold, `singletons` will fall back to
+  a slightly different approach to generating defunctionalization symbols that
+  does *not* guarantee the order of type variables. As an example, consider the
+  following example:
+
+  ```haskell
+  data T (x :: a) :: forall b. b -> Type
+  $(genDefunSymbols [''T])
+  ```
+
+  The kind of `T` is `forall a. a -> forall b. b -> Type`, which is not
+  vanilla. Currently, `singletons` will generate the following
+  defunctionalization symbols for `T`:
+
+  ```haskell
+  data TSym0 :: a ~> b ~> Type
+  data TSym1 (x :: a) :: b ~> Type
+  ```
+
+  In both symbols, the kind starts with `forall a b.` rather than quantifying
+  the `b` after the visible argument of kind `a`. These symbols can still be
+  useful even with this flaw, so `singletons` permits generating them
+  regardless. Be aware of this drawback if you try doing something similar
+  yourself!
+
+* Kind signatures of promoted class methods.
+  The order of type variables will often "just work" by happy coincidence, but
+  there are some situations where this does not happen. Consider the following
+  class:
+
+  ```haskell
+  class C (b :: Type) where
+    m :: forall a. a -> b -> a
+  ```
+
+  The full type of `m` is `forall b. C b => forall a. a -> b -> a`, which binds
+  `b` before `a`. This order is preserved when singling `m`, but *not* when
+  promoting `m`. This is because the `C` class is promoted as follows:
+
+  ```haskell
+  class PC (b :: Type) where
+    type M (x :: a) (y :: b) :: a
+  ```
+
+  Due to the way GHC kind-checks associated type families, the kind of `M` is
+  `forall a b. a -> b -> a`, which binds `b` *after* `a`. Moreover, the
+  `StandaloneKindSignatures` extension does not provide a way to explicitly
+  declare the full kind of an associated type family, so this limitation is
+  not easy to work around.
+
+  The defunctionalization symbols for `M` will also follow a similar
+  order of type variables:
+
+  ```haskell
+  type MSym0 :: forall a b. a ~> b ~> a
+  type MSym1 :: forall a b. a -> b ~> a
+  ```
 
 Known bugs
 ----------

cabal.project

@@ -3,4 +3,4 @@ packages: .
 source-repository-package
   type: git
   location: https://github.com/goldfirere/th-desugar
-  tag: 4e8f7d46954e690530c17b2eac9d302170ff994f
+  tag: a6c902914ff6fcca021619dbb4919327fb98c404

src/Data/Singletons.hs

@@ -9,6 +9,7 @@
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}

src/Data/Singletons/CustomStar.hs

@@ -96,7 +96,7 @@ singletonStar names = do
                                             promoteDerivedEqDec dataDeclEqInst
                                             traverse (promoteInstanceDec mempty mempty)
                                               [ordInst, showInst]
-    singletonDecls <- singDecsM [] $ do decs1 <- singDataD dataDecl
+    singletonDecls <- singDecsM [] $ do decs1 <- singDataD mempty dataDecl
                                         decs2 <- singDerivedEqDecs dataDeclEqInst
                                         decs3 <- traverse singInstD pInsts
                                         return (decs1 ++ decs2 ++ decs3)

src/Data/Singletons/Partition.hs

@@ -49,17 +49,23 @@ data PartitionedDecs =
         , pd_ty_syn_decs :: [TySynDecl]
         , pd_open_type_family_decs :: [OpenTypeFamilyDecl]
         , pd_closed_type_family_decs :: [ClosedTypeFamilyDecl]
+        , pd_standalone_kind_sigs :: Map Name DKind
+          -- ^ Maps names of type-level declarations to their standalone kind
+          --   signatures (if they have them). This is tracked separately from
+          --   lde_types in LetDecEnv since standalone kind signatures can only
+          --   appear at the top level, unlike let-declarations.
         , pd_derived_eq_decs :: [DerivedEqDecl]
         , pd_derived_show_decs :: [DerivedShowDecl]
         }
 
 instance Semigroup PartitionedDecs where
-  PDecs a1 b1 c1 d1 e1 f1 g1 h1 i1 <> PDecs a2 b2 c2 d2 e2 f2 g2 h2 i2 =
+  PDecs a1 b1 c1 d1 e1 f1 g1 h1 i1 j1 <> PDecs a2 b2 c2 d2 e2 f2 g2 h2 i2 j2 =
     PDecs (a1 <> a2) (b1 <> b2) (c1 <> c2) (d1 <> d2) (e1 <> e2) (f1 <> f2)
-          (g1 <> g2) (h1 <> h2) (i1 <> i2)
+          (g1 <> g2) (h1 <> h2) (i1 <> i2) (j1 <> j2)
 
 instance Monoid PartitionedDecs where
-  mempty = PDecs [] [] [] [] [] [] [] [] []
+  mempty = PDecs mempty mempty mempty mempty mempty
+                 mempty mempty mempty mempty mempty
   mappend = (<>)
 
 -- | Split up a @[DDec]@ into its pieces, extracting 'Ord' instances
@@ -151,6 +157,8 @@ partitionDec (DStandaloneDerivD mb_strat _ ctxt ty) =
                        ++ show data_ty
               _ -> fail $ "Cannot find " ++ show data_ty
     _ -> return mempty
+partitionDec (DKiSigD n ki) =
+  pure $ mempty { pd_standalone_kind_sigs = Map.singleton n ki }
 partitionDec dec =
   fail $ "Declaration cannot be promoted: " ++ pprint (decToTH dec)
 

src/Data/Singletons/Prelude/Applicative.hs

@@ -5,6 +5,7 @@
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}

src/Data/Singletons/Prelude/Base.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE TemplateHaskell, TypeOperators, DataKinds, PolyKinds,
              ScopedTypeVariables, TypeFamilies, GADTs,
-             UndecidableInstances, BangPatterns, TypeApplications #-}
+             UndecidableInstances, BangPatterns, TypeApplications,
+             StandaloneKindSignatures #-}
 
 -----------------------------------------------------------------------------
 -- |

src/Data/Singletons/Prelude/Bool.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators,
              GADTs, ScopedTypeVariables, DeriveDataTypeable, UndecidableInstances,
-             DataKinds, PolyKinds #-}
+             DataKinds, PolyKinds, StandaloneKindSignatures #-}
 
 -----------------------------------------------------------------------------
 -- |

src/Data/Singletons/Prelude/Const.hs

@@ -85,7 +85,8 @@ instance SingI ConstSym0 where
   sing = singFun1 SConst
 
 $(singletons [d|
-  type family GetConst (x :: Const a b) :: a where
+  type GetConst :: Const a b -> a
+  type family GetConst x where
     GetConst ('Const x) = x
   |])
 

src/Data/Singletons/Prelude/Either.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE TemplateHaskell, ScopedTypeVariables, TypeFamilies, GADTs,
              RankNTypes, UndecidableInstances, DataKinds, PolyKinds,
-             TypeApplications #-}
+             TypeApplications, StandaloneKindSignatures #-}
 
 -----------------------------------------------------------------------------
 -- |

src/Data/Singletons/Prelude/Enum.hs

@@ -1,7 +1,7 @@
 {-# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, ScopedTypeVariables,
              TypeFamilies, TypeOperators, GADTs, UndecidableInstances,
              FlexibleContexts, DefaultSignatures, BangPatterns,
-             InstanceSigs, TypeApplications #-}
+             InstanceSigs, TypeApplications, StandaloneKindSignatures #-}
 
 -----------------------------------------------------------------------------
 -- |

src/Data/Singletons/Prelude/Foldable.hs

@@ -6,6 +6,7 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}

src/Data/Singletons/Prelude/Function.hs

@@ -19,7 +19,8 @@
 
 {-# LANGUAGE TemplateHaskell, ScopedTypeVariables, TypeFamilies,
              TypeOperators, UndecidableInstances, GADTs,
-             DataKinds, PolyKinds, TypeApplications #-}
+             DataKinds, PolyKinds, TypeApplications,
+             StandaloneKindSignatures #-}
 
 module Data.Singletons.Prelude.Function (
     -- * "Prelude" re-exports

src/Data/Singletons/Prelude/Functor.hs

@@ -6,6 +6,7 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}

src/Data/Singletons/Prelude/Identity.hs

@@ -5,6 +5,7 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}

src/Data/Singletons/Prelude/Instances.hs

@@ -11,7 +11,7 @@ re-exported from various places.
 {-# LANGUAGE DataKinds, PolyKinds, RankNTypes, GADTs, TypeFamilies, EmptyCase,
              FlexibleContexts, TemplateHaskell, ScopedTypeVariables,
              UndecidableInstances, TypeOperators, FlexibleInstances,
-             TypeApplications #-}
+             TypeApplications, StandaloneKindSignatures #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Data.Singletons.Prelude.Instances (

src/Data/Singletons/Prelude/IsString.hs

@@ -3,6 +3,7 @@
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}

src/Data/Singletons/Prelude/List/Internal.hs

@@ -1,7 +1,7 @@
 {-# LANGUAGE TypeOperators, DataKinds, PolyKinds, TypeFamilies,
              TemplateHaskell, GADTs, UndecidableInstances, RankNTypes,
              ScopedTypeVariables, FlexibleContexts,
-             TypeApplications #-}
+             TypeApplications, StandaloneKindSignatures #-}
 {-# OPTIONS_GHC -O0 #-}
 
 -----------------------------------------------------------------------------

src/Data/Singletons/Prelude/List/Internal/Disambiguation.hs

@@ -14,7 +14,7 @@
 
 {-# LANGUAGE TemplateHaskell, ScopedTypeVariables, TypeFamilies,
              UndecidableInstances, GADTs, DataKinds, PolyKinds,
-             TypeApplications #-}
+             TypeApplications, StandaloneKindSignatures #-}
 
 module Data.Singletons.Prelude.List.Internal.Disambiguation where