Remove wrinkle 2 (and revise wrinkle 3) of Note [Preserve the order o…

…f type variables during singling]

Now that goldfirere/th-desugar#199 has been fixed,
`singletons-th` can always guarantee that the type variable specificities that
it reifies will be accurate. As such, all of wrinkle 2 in `Note [Preserve the
order of type variables during singling]` is moot, so this PR deletes this
wrinkle entirely. Wrinkle 3 has now been renamed to wrinkle 2.

What was formerly known as wrinkle 3 is mostly kept the same, although I have
expanded upon it a little to clarify what we single data constructors such as
`Nothing :: forall a. Maybe a` to `SNothing :: forall a. SMaybe (Nothing ::
Maybe a)` rather than, say, `SNothing :: forall a. SMaybe (Nothing @A)`. For
instance, imagine if `a` was inferred rather than specified!

I have added a `T565` test case which ensures that `singletons-th` generates
valid code for the case when a data constructor uses an inferred type variable
binder. I have also added an addendum to the `README` noting that
`singletons-th` does not currently support `AllowAmbiguousTypes` at all, which
would be perhaps the one convincing argument in favor of using explicit kind
applications when singling return types (rather than explicit return kinds).

Fixes #565.

README.md

@@ -1585,6 +1585,7 @@ The following constructs are either unsupported or almost never work:
 * `{-# UNPACK #-}` pragmas
 * partial application of the `(->)` type
 * invisible type patterns
+* `AllowAmbiguousTypes`
 
 See the following sections for more details.
 
@@ -1783,3 +1784,16 @@ f @t x = x :: t
 
 See [this `singletons`
 issue](https://github.com/goldfirere/singletons/issues/583).
+
+### `AllowAmbiguousTypes`
+
+`singletons-th` does not currently support promoting or singling types with
+ambiguous type variables, which require the `AllowAmbiguousTypes` language
+extension to define. For instance, `singletons-th` does not support definitions
+such as this one:
+
+```hs
+{-# LANGUAGE AllowAmbiguousTypes #-}
+class HasName a where
+  name :: String -- This type is ambiguous
+```

singletons-base/src/Data/Functor/Compose/Singletons.hs

@@ -36,45 +36,15 @@ import Data.Functor.Singletons
 import Data.Ord.Singletons
 import Data.Kind
 import Data.Semigroup.Singletons
-import Data.Singletons
 import Data.Singletons.Base.Instances (SList(..), (:@#@$), NilSym0)
 import Data.Singletons.TH
+import Data.Singletons.TH.Options
 import Data.Traversable.Singletons
 
-{-
-In order to keep the type arguments to Compose poly-kinded and with inferred
-specificities, we define the singleton version of Compose, as well as its
-defunctionalization symbols, by hand. This is very much in the spirit of the
-code in Data.Functor.Const.Singletons. (See the comments above SConst in that
-module for more details on this choice.)
--}
-infixr 9 `SCompose`
-type SCompose :: Compose f g a -> Type
-data SCompose :: Compose f g a -> Type where
-  SCompose :: forall f g a (x :: f (g a)).
-              Sing x -> SCompose ('Compose @f @g @a x)
-type instance Sing @(Compose f g a) = SCompose
-instance SingI x => SingI ('Compose x) where
-  sing = SCompose sing
-instance SingI1 'Compose where
-  liftSing = SCompose
-
-infixr 9 `ComposeSym0`
-type ComposeSym0 :: f (g a) ~> Compose f g a
-data ComposeSym0 z
-type instance Apply ComposeSym0 x = 'Compose x
-instance SingI ComposeSym0 where
-  sing = singFun1 SCompose
-
-infixr 9 `ComposeSym1`
-type ComposeSym1 :: f (g a) -> Compose f g a
-type family ComposeSym1 x where
-  ComposeSym1 x = 'Compose x
+$(withOptions defaultOptions{genSingKindInsts = False}
+    (genSingletons [''Compose]))
 
 $(singletonsOnly [d|
-  getCompose :: Compose f g a -> f (g a)
-  getCompose (Compose x) = x
-
   deriving instance Eq (f (g a)) => Eq (Compose f g a)
   deriving instance Ord (f (g a)) => Ord (Compose f g a)
 

singletons-base/src/Data/Functor/Const/Singletons.hs

@@ -32,73 +32,28 @@ import Control.Applicative
 import Control.Monad.Singletons.Internal
 import Data.Eq.Singletons
 import Data.Foldable.Singletons
-import Data.Kind (Type)
 import Data.Monoid.Singletons
 import Data.Ord.Singletons
 import Data.Semigroup.Singletons.Internal.Classes
-import Data.Singletons
 import Data.Singletons.Base.Instances hiding (FoldlSym0, sFoldl)
 import Data.Singletons.Base.Enum
 import Data.Singletons.TH
+import Data.Singletons.TH.Options
 import GHC.Base.Singletons
   hiding ( Const, ConstSym0, ConstSym1
          , Foldr, FoldrSym0, sFoldr )
 import GHC.Num.Singletons
 import Text.Show.Singletons
 
-{-
-Const's argument `b` is poly-kinded, and as a result, we have a choice as to
-what singleton type to give it. We could use either
+$(withOptions defaultOptions{genSingKindInsts = False}
+    (genSingletons [''Const]))
 
-1. type SConst :: forall {k :: Type} (a :: Type) (b :: k).    Const a b -> Type
-2. type SConst :: forall             (a :: Type) (b :: Type). Const a b -> Type
-
-Option (1) is the more permissive one, so we opt for that. However, singletons-th's
-TH machinery does not jive with this option, since the SingKind instance it
-tries to generate:
-
-  instance (SingKind a, SingKind b) => SingKind (Const a b) where
-    type Demote (Const a b) = Const (Demote a) (Demote b)
-
-Assumes that `b` is of kind Type. Until we get a more reliable story for
-poly-kinded Sing instances (see #150), we simply write the singleton type by
-hand.
-
-Note that we cannot use genSingletons to generate this code because we
-would end up with the wrong specificity for the kind of `a` when singling the
-Const constructor. See Note [Preserve the order of type variables during
-singling] in D.S.TH.Single.Type, wrinkle 2. Similarly, we must define the
-defunctionalization symbols for the Const data constructor by hand to get the
-specificities right.
--}
-type SConst :: Const a b -> Type
-data SConst :: Const a b -> Type where
-  SConst :: forall {k} a (b :: k) (x :: a).
-            Sing x -> SConst ('Const @a @b x)
-type instance Sing @(Const a b) = SConst
 instance SingKind a => SingKind (Const a b) where
   type Demote (Const a b) = Const (Demote a) b
   fromSing (SConst sa) = Const (fromSing sa)
   toSing (Const a) = withSomeSing a $ SomeSing . SConst
-instance SingI a => SingI ('Const a) where
-  sing = SConst sing
-instance SingI1 'Const where
-  liftSing = SConst
-
-type ConstSym0 :: a ~> Const a b
-data ConstSym0 z
-type instance Apply ConstSym0 x = 'Const x
-instance SingI ConstSym0 where
-  sing = singFun1 SConst
-
-type ConstSym1 :: a -> Const a b
-type family ConstSym1 x where
-  ConstSym1 x = 'Const x
 
 $(singletonsOnly [d|
-  getConst :: Const a b -> a
-  getConst (Const x) = x
-
   deriving instance Bounded a => Bounded (Const a b)
   deriving instance Eq      a => Eq      (Const a b)
   deriving instance Ord     a => Ord     (Const a b)

singletons-base/src/Data/Functor/Product/Singletons.hs

@@ -42,46 +42,12 @@ import Data.Monoid.Singletons hiding (SProduct(..))
 import Data.Semigroup.Singletons hiding (SProduct(..))
 import Data.Singletons.Base.Instances (SList(..), (:@#@$), NilSym0)
 import Data.Ord.Singletons
-import Data.Singletons
 import Data.Singletons.TH
+import Data.Singletons.TH.Options
 import Data.Traversable.Singletons
 
-{-
-In order to keep the type arguments to Product poly-kinded and with inferred
-specificities, we define the singleton version of Product, as well as its
-defunctionalization symbols, by hand. This is very much in the spirit of the
-code in Data.Functor.Const.Singletons. (See the comments above SConst in that
-module for more details on this choice.)
--}
-type SProduct :: Product f g a -> Type
-data SProduct :: Product f g a -> Type where
-  SPair :: forall f g a (x :: f a) (y :: g a).
-           Sing x -> Sing y -> SProduct ('Pair @f @g @a x y)
-type instance Sing @(Product f g a) = SProduct
-instance (SingI x, SingI y) => SingI ('Pair x y) where
-  sing = SPair sing sing
-instance SingI x => SingI1 ('Pair x) where
-  liftSing = SPair sing
-instance SingI2 'Pair where
-  liftSing2 = SPair
-
-type PairSym0 :: forall f g a. f a ~> g a ~> Product f g a
-data PairSym0 z
-type instance Apply PairSym0 x = PairSym1 x
-instance SingI PairSym0 where
-  sing = singFun2 SPair
-
-type PairSym1 :: forall f g a. f a -> g a ~> Product f g a
-data PairSym1 fa z
-type instance Apply (PairSym1 x) y = 'Pair x y
-instance SingI x => SingI (PairSym1 x) where
-  sing = singFun1 $ SPair (sing @x)
-instance SingI1 PairSym1 where
-  liftSing s = singFun1 $ SPair s
-
-type PairSym2 :: forall f g a. f a -> g a -> Product f g a
-type family PairSym2 x y where
-  PairSym2 x y = 'Pair x y
+$(withOptions defaultOptions{genSingKindInsts = False}
+    (genSingletons [''Product]))
 
 $(singletonsOnly [d|
   deriving instance (Eq (f a), Eq (g a)) => Eq (Product f g a)

singletons-base/src/Data/Functor/Sum/Singletons.hs

@@ -32,56 +32,15 @@ import Data.Eq.Singletons
 import Data.Foldable.Singletons hiding (Sum)
 import Data.Functor.Singletons
 import Data.Functor.Sum
-import Data.Kind
 import Data.Ord.Singletons
 import Data.Semigroup.Singletons hiding (SSum(..))
-import Data.Singletons
 import Data.Singletons.Base.Instances (SList(..), (:@#@$), NilSym0)
 import Data.Singletons.TH
+import Data.Singletons.TH.Options
 import Data.Traversable.Singletons
 
-{-
-In order to keep the type arguments to Sum poly-kinded and with inferred
-specificities, we define the singleton version of Sum, as well as its
-defunctionalization symbols, by hand. This is very much in the spirit of the
-code in Data.Functor.Const.Singletons. (See the comments above SConst in that
-module for more details on this choice.)
--}
-type SSum :: Sum f g a -> Type
-data SSum :: Sum f g a -> Type where
-  SInL :: forall f g a (x :: f a).
-          Sing x -> SSum ('InL @f @g @a x)
-  SInR :: forall f g a (y :: g a).
-          Sing y -> SSum ('InR @f @g @a y)
-type instance Sing @(Sum f g a) = SSum
-instance SingI x => SingI ('InL x) where
-  sing = SInL sing
-instance SingI1 'InL where
-  liftSing = SInL
-instance SingI y => SingI ('InR y) where
-  sing = SInR sing
-instance SingI1 'InR where
-  liftSing = SInR
-
-type InLSym0 :: forall f g a. f a ~> Sum f g a
-data InLSym0 z
-type instance Apply InLSym0 x = 'InL x
-instance SingI InLSym0 where
-  sing = singFun1 SInL
-
-type InLSym1 :: forall f g a. f a -> Sum f g a
-type family InLSym1 x where
-  InLSym1 x = 'InL x
-
-type InRSym0 :: forall f g a. g a ~> Sum f g a
-data InRSym0 z
-type instance Apply InRSym0 y = 'InR y
-instance SingI InRSym0 where
-  sing = singFun1 SInR
-
-type InRSym1 :: forall f g a. g a -> Sum f g a
-type family InRSym1 x where
-  InRSym1 y = 'InR y
+$(withOptions defaultOptions{genSingKindInsts = False}
+    (genSingletons [''Sum]))
 
 $(singletonsOnly [d|
   deriving instance (Eq (f a), Eq (g a)) => Eq (Sum f g a)

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

@@ -32,45 +32,30 @@ import Control.Applicative
 import Control.Monad
 import Control.Monad.Singletons.Internal
 import Data.Eq.Singletons
-import Data.Kind
 import Data.Monoid.Singletons
 import Data.Ord.Singletons
 import Data.Proxy
 import Data.Semigroup (Semigroup(..))
 import Data.Semigroup.Singletons.Internal.Classes
 import Data.Singletons.Decide
-import Data.Singletons
 import Data.Singletons.Base.Enum
 import Data.Singletons.Base.Instances
 import Data.Singletons.TH
+import Data.Singletons.TH.Options
 import Data.Type.Coercion
 import Data.Type.Equality hiding (type (==))
 import GHC.Base.Singletons
 import GHC.Num.Singletons
 import GHC.TypeLits.Singletons.Internal
 import Text.Show.Singletons
 
-{-
-In order to keep the type argument to Proxy poly-kinded and with an inferred
-specificity, we define the singleton version of Proxy, as well as its
-defunctionalization symbols, by hand. This is very much in the spirit of the
-code in Data.Functor.Const.Singletons. (See the comments above SConst in that
-module for more details on this choice.)
--}
-type SProxy :: Proxy t -> Type
-data SProxy :: Proxy t -> Type where
-  SProxy :: forall t. SProxy ('Proxy @t)
-type instance Sing @(Proxy t) = SProxy
+$(withOptions defaultOptions{genSingKindInsts = False}
+    (genSingletons [''Proxy]))
+
 instance SingKind (Proxy t) where
   type Demote (Proxy t) = Proxy t
   fromSing SProxy = Proxy
   toSing Proxy = SomeSing SProxy
-instance SingI 'Proxy where
-  sing = SProxy
-
-type ProxySym0 :: Proxy t
-type family ProxySym0 where
-  ProxySym0 = 'Proxy
 
 instance Eq (SProxy z) where
   _ == _ = True

singletons-base/tests/SingletonsBaseTestSuite.hs

@@ -150,6 +150,7 @@ tests =
     , compileAndDumpStdTest "T555"
     , compileAndDumpStdTest "T559"
     , compileAndDumpStdTest "T563"
+    , compileAndDumpStdTest "T565"
     , compileAndDumpStdTest "T567"
     , compileAndDumpStdTest "T571"
     , compileAndDumpStdTest "T581"

singletons-base/tests/compile-and-dump/Singletons/T565.golden

@@ -0,0 +1,16 @@
+Singletons/T565.hs:(0,0)-(0,0): Splicing declarations
+    singletons [d| data C a where D :: forall {a}. C a |]
+  ======>
+    data C a where D :: forall {a}. C a
+    type DSym0 :: forall {a}. C a
+    type family DSym0 :: C a where
+      DSym0 = D
+    data SC :: forall a. C a -> Type
+      where SD :: forall {a}. SC (D :: C a)
+    type instance Sing @(C a) = SC
+    instance SingKind a => SingKind (C a) where
+      type Demote (C a) = C (Demote a)
+      fromSing SD = D
+      toSing D = SomeSing SD
+    instance SingI D where
+      sing = SD

singletons-base/tests/compile-and-dump/Singletons/T565.hs

@@ -0,0 +1,8 @@
+module T565 where
+
+import Data.Singletons.TH
+
+$(singletons [d|
+  data C a where
+    D :: forall {a}. C a
+  |])

singletons-th/src/Data/Singletons/TH/Single/Data.hs

@@ -231,7 +231,7 @@ singCtor dataName (DCon con_tvbs cxt name fields rty)
                   (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.TH.Single.Type.
+                  -- wrinkle 2, in D.S.TH.Single.Type.
   where
     mk_source_unpackedness :: SourceUnpackedness -> SgM SourceUnpackedness
     mk_source_unpackedness su = case su of