Partially revert #596, give PAlternative (and friends) the correct kinds

README.md

@@ -819,7 +819,6 @@ The following constructs are fully supported:
 * sections
 * undefined
 * error
-* class constraints (though these sometimes fail with `let`, `lambda`, and `case`)
 * literal expressions (for `Natural`, `Symbol`, and `Char`), including
   overloaded number literals
 * datatypes that store `Natural`
@@ -839,6 +838,7 @@ The following constructs are fully supported:
 
 The following constructs are partially supported:
 
+* class constraints
 * scoped type variables
 * `deriving`
 * finite arithmetic sequences
@@ -852,6 +852,87 @@ The following constructs are partially supported:
 
 See the following sections for more details.
 
+### Class constraints
+
+`singletons-th` supports promoting and singling class constraints, but with
+some caveats about the particular sorts of constraints involved. Suppose you
+have a function that looks like this:
+
+```hs
+foo :: Eq a => a -> Bool
+foo x = (x == x)
+```
+
+`singletons-th` will promote `foo` to the following type family:
+
+```hs
+type Foo :: a -> Bool
+type family Foo x where
+  Foo x = (x == x)
+```
+
+Note that the standalone kind signature for `Foo` does not mention `PEq` (the
+promoted version of `Eq`) anywhere. This is because GHC does not permit
+constraints in kinds, so it would be an error to give `Foo` the kind `Eq a => a
+-> Bool`. Thankfully, we don't need to mention `PEq` in `Foo`'s kind anyway, as
+the promoted `(==)` type family can be used independently of a `PEq`
+constraint.
+
+`singletons-th` will single `foo` to the following definition:
+
+```hs
+sFoo :: forall a (x :: a). SEq a => Sing x -> Sing (Foo x)
+sFoo sX = sX %== sX
+```
+
+This time, we can (and must) mention `SEq` (the singled version of `Eq`) in the
+type signature for `sFoo`.
+
+In general, `singletons-th` only supports constraints of the form `C T_1 ...
+T_n`, where `C` is a type class constructor and each `T_i` is a type that does
+not mention any other type classes. `singletons-th` does not support non-class
+constraints, such as equality constraint (`(~)`) or `Coercible` constraints.
+
+`singletons-th` only supports constraints that appear in _vanilla_ types. (See
+the "Rank-n types" section below for what "vanilla" means.) `singletons-th` does
+not support existential constraints that appear in data constructors.
+
+Because `singletons-th` omits constraints when promoting types to kinds, it is
+possible for some promoted types to have more general kinds than what is
+intended. For example, consider this example:
+
+```hs
+bar :: Alternative f => f a
+bar = empty
+```
+
+The kind of `f` in the type of `bar` should be `Type -> Type`, and GHC will
+infer this because of the `Alternative f` constraint. If you promote this to
+a type family, however, you instead get:
+
+```hs
+type Bar :: f a
+type family Bar @f @a where
+  Bar = Empty
+```
+
+Now, GHC will infer that the full kind of `Bar` is `forall {k} (f :: k -> Type)
+(a :: k). f a`, which is more general that the original definition! This is not
+desirable, as this means that `Bar` can be called on kinds that cannot have
+`PAlternative` instances.
+
+In general, the only way to avoid this problem is to ensure that type variables
+like `f` are given explicit kinds. For example, `singletons-th` will promote
+this to a type family with the correct kind:
+
+```hs
+bar :: forall (f :: Type -> Type) a. Alternative f => f a
+bar = empty
+```
+
+Be especially aware of this limitation is you are dealing with classes that are
+parameterized over higher-kinded type variables such as `f`.
+
 ### Scoped type variables
 
 `singletons-th` makes an effort to track scoped type variables during promotion
@@ -1179,72 +1260,34 @@ for the following constructs:
   yourself!
 
 * Kind signatures of promoted class methods.
-  The order of type variables is only guaranteed to be preserved if the parent
-  class has a standalone kind signature. For example, given this class:
+  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
-  type C :: Type -> Constraint
-  class C b where
+  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`. Because `C` has a standalone kind signature, the order of
-  type variables is preserved when promoting and singling `m`:
-
-  ```hs
-  type PC :: Type -> Constraint
-  class PC b where
-    type M @b @a (x :: a) (y :: b) :: a
-
-  type MSym0 :: forall b a. a ~> b ~> a
-  type MSym1 :: forall b a. a -> b ~> a
-
-  type SC :: Type -> Constraint
-  class SC b where
-    sM :: forall a (x :: a) (y :: b).
-          Sing x -> Sing y -> Sing (M x y)
-  ```
-
-  Note that `M`, `M`'s defunctionalization symbols, and `sM` all quantify `b`
-  before `a` in their types. The key to making this work is by using the
-  `TypeAbstractions` language extension in declaration for `M`, which is only
-  possible due to `PC` having a standalone kind signature.
-
-  If the parent class does _not_ have a standalone kind signature, then
-  `singletons-th` does not make any guarantees about the order of kind
-  variables in the promoted methods' kinds. The order will often "just work" by
-  happy coincidence, but there are some situations where this does not happen.
-  Consider the following variant of the class example above:
+  `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
-  -- No standalone kind signature
-  class C b where
-    m :: forall a. a -> b -> a
-  ```
-
-  Again, 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
-  -- No standalone kind signature
-  class PC b where
+  class PC (b :: Type) where
     type M (x :: a) (y :: b) :: a
   ```
 
-  This time, `PC` does not have a standalone kind signature, so we cannot use
-  `TypeAbstractions` in the declaration for `M`. As such, GHC will quantify the
-  kind variables in left-to-right order, so the kind of `M` will be inferred to
-  be `forall a b. a -> b -> a`, which binds `b` *after* `a`. The
-  defunctionalization symbols for `M` will also follow a similar order of type
-  variables:
+  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.
 
-  ```haskell
-  type MSym0 :: forall a b. a ~> b ~> a
-  type MSym1 :: forall a b. a -> b ~> a
-  ```
+  As a result, one should not depend on the order of kind variables for promoted
+  class methods like `M`. The order of kind variables in defunctionalization
+  symbols for promoted class methods (e.g. `MSym0` and `MSym1`) is similarly
+  unspecified.
 
 ### Wildcard types
 

singletons-base/CHANGES.md

@@ -23,6 +23,26 @@ next [????.??.??]
   now have improve type inference and avoid the need for special casing. If you
   truly need the full polymorphism of the old type signatures, use `error`,
   `errorWithoutStackTrace`, or `undefined` instead.
+* The kinds of `PAlternative` (and other classes in `singletons-base` that are
+  parameterized over a higher-kinded type variable) are less polymorphic than
+  they were before:
+
+  ```diff
+  -type PAlternative :: (k    -> Type) -> Constraint
+  +type PAlternative :: (Type -> Type) -> Constraint
+
+  -type PMonadZip :: (k    -> Type) -> Constraint
+  +type PMonadZip :: (Type -> Type) -> Constraint
+
+  -type PMonadPlus :: (k    -> Type) -> Constraint
+  +type PMonadPlus :: (Type -> Type) -> Constraint
+  ```
+
+  Similarly, the kinds of defunctionalization symbols for these classes (e.g.,
+  `EmptySym0` and `(<|>@#@$)`) now use `Type -> Type` instead of `k -> Type`.
+  The fact that these were kind-polymorphic to begin with was an oversight, as
+  these could not be used when `k` was instantiated to any other kind besides
+  `Type`.
 
 3.4 [2024.05.12]
 ----------------

singletons-base/src/Control/Monad/Fail/Singletons.hs

@@ -25,6 +25,7 @@ module Control.Monad.Fail.Singletons (
   ) where
 
 import Control.Monad.Singletons.Internal
+import Data.Kind
 import Data.Singletons.Base.Instances
 import Data.Singletons.TH
 
@@ -49,6 +50,10 @@ $(singletonsOnly [d|
   -- @
   -- fail _ = mzero
   -- @
+
+  -- See Note [Using standalone kind signatures not present in the base library]
+  -- in Control.Monad.Singletons.Internal.
+  type MonadFail :: (Type -> Type) -> Constraint
   class Monad m => MonadFail m where
       fail :: String -> m a
 

singletons-base/src/Control/Monad/Singletons/Internal.hs

@@ -33,6 +33,7 @@ module Control.Monad.Singletons.Internal where
 
 import Control.Applicative
 import Control.Monad
+import Data.Kind
 import Data.List.NonEmpty (NonEmpty(..))
 import Data.Singletons.Base.Instances
 import Data.Singletons.TH
@@ -51,6 +52,8 @@ $(singletonsOnly [d|
   satisfy these laws.
   -}
 
+  -- See Note [Using standalone kind signatures not present in the base library]
+  type   Functor :: (Type -> Type) -> Constraint
   class  Functor f  where
       fmap        :: (a -> b) -> f a -> f b
 
@@ -126,6 +129,8 @@ $(singletonsOnly [d|
   --
   -- (which implies that 'pure' and '<*>' satisfy the applicative functor laws).
 
+  -- See Note [Using standalone kind signatures not present in the base library]
+  type Applicative :: (Type -> Type) -> Constraint
   class Functor f => Applicative f where
       -- {-# MINIMAL pure, ((<*>) | liftA2) #-}
       -- -| Lift a value.
@@ -243,6 +248,9 @@ $(singletonsOnly [d|
   The instances of 'Monad' for lists, 'Data.Maybe.Maybe' and 'System.IO.IO'
   defined in the "Prelude" satisfy these laws.
   -}
+
+  -- See Note [Using standalone kind signatures not present in the base library]
+  type Monad :: (Type -> Type) -> Constraint
   class Applicative m => Monad m where
       -- -| Sequentially compose two actions, passing any value produced
       -- by the first as an argument to the second.
@@ -352,6 +360,9 @@ $(singletonsOnly [d|
   -- -* @'some' v = (:) '<$>' v '<*>' 'many' v@
   --
   -- -* @'many' v = 'some' v '<|>' 'pure' []@
+
+  -- See Note [Using standalone kind signatures not present in the base library]
+  type Alternative :: (Type -> Type) -> Constraint
   class Applicative f => Alternative f where
       -- -| The identity of '<|>'
       empty :: f a
@@ -386,6 +397,9 @@ $(singletonsOnly [d|
   -- The MonadPlus class definition
 
   -- -| Monads that also support choice and failure.
+
+  -- See Note [Using standalone kind signatures not present in the base library]
+  type MonadPlus :: (Type -> Type) -> Constraint
   class (Alternative m, Monad m) => MonadPlus m where
      -- -| The identity of 'mplus'.  It should also satisfy the equations
      --
@@ -479,3 +493,18 @@ $(singletonsOnly [d|
   instance MonadPlus Maybe
   instance MonadPlus []
   |])
+
+{-
+Note [Using standalone kind signatures not present in the base library]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Various type class definitions in singletons-base (Functor, Foldable,
+Alternative, etc.) are defined using standalone kind signatures. These
+standalone kind signatures are /not/ present in the original `base` library,
+however: these are specifically required by singletons-th. More precisely, all
+of these classes are parameterized by a type variable of kind `Type -> Type`,
+and we want to ensure that the promoted class (and the defunctionalization
+symbols for its class methods) all use `Type -> Type` in their kinds as well.
+For more details on why singletons-th requires this, see Note [Propagating kind
+information from class standalone kind signatures] in D.S.TH.Promote in
+singletons-th.
+-}

singletons-base/src/Control/Monad/Zip/Singletons.hs

@@ -30,6 +30,7 @@ module Control.Monad.Zip.Singletons (
 import Control.Monad.Singletons.Internal
 import Data.Functor.Identity
 import Data.Functor.Identity.Singletons
+import Data.Kind
 import Data.List.Singletons
        ( ZipSym0, ZipWithSym0, UnzipSym0
        , sZip,    sZipWith,    sUnzip )
@@ -56,6 +57,10 @@ $(singletonsOnly [d|
   --   > ==>
   --   > munzip (mzip ma mb) = (ma, mb)
   --
+
+  -- See Note [Using standalone kind signatures not present in the base library]
+  -- in Control.Monad.Singletons.Internal.
+  type MonadZip :: (Type -> Type) -> Constraint
   class Monad m => MonadZip m where
       -- {-# MINIMAL mzip | mzipWith #-}
 

singletons-base/src/Data/Foldable/Singletons.hs

@@ -215,6 +215,9 @@ $(singletonsOnly [d|
   --
   -- > foldMap f . fmap g = foldMap (f . g)
 
+  -- See Note [Using standalone kind signatures not present in the base library]
+  -- in Control.Monad.Singletons.Internal.
+  type Foldable :: (Type -> Type) -> Constraint
   class Foldable t where
       -- {-# MINIMAL foldMap | foldr #-}
 

singletons-base/src/Data/Traversable/Singletons.hs

@@ -171,6 +171,10 @@ $(singletonsOnly [d|
   --    equivalent to traversal with a constant applicative functor
   --    ('foldMapDefault').
   --
+
+  -- See Note [Using standalone kind signatures not present in the base library]
+  -- in Control.Monad.Singletons.Internal.
+  type Traversable :: (Type -> Type) -> Constraint
   class (Functor t, Foldable t) => Traversable t where
       -- {-# MINIMAL traverse | sequenceA #-}
 

singletons-base/tests/SingletonsBaseTestSuite.hs

@@ -156,7 +156,6 @@ tests =
     , compileAndDumpStdTest "T582"
     , compileAndDumpStdTest "T585"
     , compileAndDumpStdTest "TypeAbstractions"
-    , compileAndDumpStdTest "T589"
     ],
     testCompileAndDumpGroup "Promote"
     [ compileAndDumpStdTest "Constructors"
@@ -167,6 +166,7 @@ tests =
     , compileAndDumpStdTest "Prelude"
     , compileAndDumpStdTest "T180"
     , compileAndDumpStdTest "T361"
+    , compileAndDumpStdTest "T605"
     ],
     testGroup "Database client"
     [ compileAndDumpTest "GradingClient/Database" ghcOpts