The great StandaloneKindSignatures patch of 2020

.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,15 @@ 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 (and, by extension, the
+  `NoCUSKs` 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

@@ -54,10 +54,12 @@ following:
 * `GADTs`
 * `InstanceSigs`
 * `KindSignatures`
+* `NoCUSKs`
 * `NoStarIsType`
 * `PolyKinds`
 * `RankNTypes`
 * `ScopedTypeVariables`
+* `StandaloneKindSignatures`
 * `TemplateHaskell`
 * `TypeApplications`
 * `TypeFamilies`
@@ -151,21 +153,23 @@ Please refer to the singletons paper for a more in-depth explanation of these
 definitions. Many of the definitions were developed in tandem with Iavor Diatchki.
 
 ```haskell
-type family Sing :: k -> Type
+type Sing :: k -> Type
+type family Sing
 ```
 
 The type family of singleton types. A new instance of this type family is
 generated for every new singleton type.
 
 ```haskell
-class SingI (a :: k) where
+class SingI a where
   sing :: Sing a
 ```
 
 A class used to pass singleton values implicitly. The `sing` method produces
 an explicit singleton value.
 
 ```haskell
+type SomeSing :: Type -> Type
 data SomeSing k where
   SomeSing :: Sing (a :: k) -> SomeSing k
 ```
@@ -176,6 +180,7 @@ can be used when you have a singleton, but you don't know at compile time what
 it will be. `SomeSing Thing` is isomorphic to `Thing`.
 
 ```haskell
+type SingKind :: Type -> Constraint
 class SingKind k where
   type Demote k :: *
   fromSing :: Sing (a :: k) -> Demote k
@@ -190,7 +195,8 @@ The `Demote` associated
 kind-indexed type family maps the kind `Nat` back to the type `Nat`.
 
 ```haskell
-data SingInstance (a :: k) where
+type SingInstance :: k -> Type
+data SingInstance a where
   SingInstance :: SingI a => SingInstance a
 singInstance :: Sing a -> SingInstance a
 ```
@@ -236,7 +242,8 @@ addition, there is a `ShowSing` constraint synonym provided in the
 `Data.Singletons.ShowSing` module:
 
 ```haskell
-type ShowSing k = (forall z. Show (Sing (z :: k))
+type ShowSing :: Type -> Constraint
+type ShowSing k = (forall z. Show (Sing (z :: k)) -- Approximately
 ```
 
 This facilitates the ability to write `Show` instances for `Sing` instances.
@@ -268,7 +275,8 @@ The `singletons` library provides two different ways to handle errors:
 * The `Error` type family, from `Data.Singletons.TypeLits`:
 
   ```haskell
-  type family Error (str :: a) :: k where {}
+  type Error :: a -> k
+  type family Error str where {}
   ```
 
   This is simply an empty, closed type family, which means that it will fail
@@ -599,15 +607,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 +680,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 +706,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 +757,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/Decide.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE RankNTypes, PolyKinds, DataKinds, TypeOperators,
              TypeFamilies, FlexibleContexts, UndecidableInstances,
-             GADTs, TypeApplications #-}
+             GADTs, TypeApplications, StandaloneKindSignatures #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 -----------------------------------------------------------------------------
@@ -25,6 +25,7 @@ module Data.Singletons.Decide (
   decideEquality, decideCoercion
   ) where
 
+import Data.Kind
 import Data.Singletons.Internal
 import Data.Type.Coercion
 import Data.Type.Equality
@@ -37,16 +38,19 @@ import Data.Void
 -- | Because we can never create a value of type 'Void', a function that type-checks
 -- at @a -> Void@ shows that objects of type @a@ can never exist. Thus, we say that
 -- @a@ is 'Refuted'
+type Refuted :: Type -> Type
 type Refuted a = (a -> Void)
 
 -- | A 'Decision' about a type @a@ is either a proof of existence or a proof that @a@
 -- cannot exist.
+type Decision :: Type -> Type
 data Decision a = Proved a               -- ^ Witness for @a@
                 | Disproved (Refuted a)  -- ^ Proof that no @a@ exists
 
 -- | Members of the 'SDecide' "kind" class support decidable equality. Instances
 -- of this class are generated alongside singleton definitions for datatypes that
 -- derive an 'Eq' instance.
+type SDecide :: Type -> Constraint
 class SDecide k where
   -- | Compute a proof or disproof of equality, given two singletons.
   (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)