From a63cf05bfb7b21c61b3f97521eb4ac3e017296b2 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 22 Jul 2024 08:19:17 -0400 Subject: [PATCH] Remove wrinkle 2 (and revise wrinkle 3) of Note [Preserve the order of type variables during singling] Now that https://github.com/goldfirere/th-desugar/issues/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 | 14 +++ .../src/Data/Functor/Compose/Singletons.hs | 36 +----- .../src/Data/Functor/Const/Singletons.hs | 51 +------- .../src/Data/Functor/Product/Singletons.hs | 40 +----- .../src/Data/Functor/Sum/Singletons.hs | 47 +------ singletons-base/src/Data/Proxy/Singletons.hs | 23 +--- .../tests/SingletonsBaseTestSuite.hs | 1 + .../compile-and-dump/Singletons/T565.golden | 16 +++ .../tests/compile-and-dump/Singletons/T565.hs | 8 ++ .../src/Data/Singletons/TH/Single/Data.hs | 2 +- .../src/Data/Singletons/TH/Single/Type.hs | 118 +++++++----------- 11 files changed, 101 insertions(+), 255 deletions(-) create mode 100644 singletons-base/tests/compile-and-dump/Singletons/T565.golden create mode 100644 singletons-base/tests/compile-and-dump/Singletons/T565.hs diff --git a/README.md b/README.md index 92f0c7e3..a33fabce 100644 --- a/README.md +++ b/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 +``` diff --git a/singletons-base/src/Data/Functor/Compose/Singletons.hs b/singletons-base/src/Data/Functor/Compose/Singletons.hs index eedf3f9a..1b3bf820 100644 --- a/singletons-base/src/Data/Functor/Compose/Singletons.hs +++ b/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) diff --git a/singletons-base/src/Data/Functor/Const/Singletons.hs b/singletons-base/src/Data/Functor/Const/Singletons.hs index 58cdb5d9..e5d2694d 100644 --- a/singletons-base/src/Data/Functor/Const/Singletons.hs +++ b/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) diff --git a/singletons-base/src/Data/Functor/Product/Singletons.hs b/singletons-base/src/Data/Functor/Product/Singletons.hs index 8c056070..a4858f97 100644 --- a/singletons-base/src/Data/Functor/Product/Singletons.hs +++ 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) diff --git a/singletons-base/src/Data/Functor/Sum/Singletons.hs b/singletons-base/src/Data/Functor/Sum/Singletons.hs index 2056447b..2e9c584b 100644 --- a/singletons-base/src/Data/Functor/Sum/Singletons.hs +++ b/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) diff --git a/singletons-base/src/Data/Proxy/Singletons.hs b/singletons-base/src/Data/Proxy/Singletons.hs index 0cad9048..43383f9c 100644 --- a/singletons-base/src/Data/Proxy/Singletons.hs +++ b/singletons-base/src/Data/Proxy/Singletons.hs @@ -32,17 +32,16 @@ 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 @@ -50,27 +49,13 @@ 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 diff --git a/singletons-base/tests/SingletonsBaseTestSuite.hs b/singletons-base/tests/SingletonsBaseTestSuite.hs index e327f9d6..17a00494 100644 --- a/singletons-base/tests/SingletonsBaseTestSuite.hs +++ b/singletons-base/tests/SingletonsBaseTestSuite.hs @@ -150,6 +150,7 @@ tests = , compileAndDumpStdTest "T555" , compileAndDumpStdTest "T559" , compileAndDumpStdTest "T563" + , compileAndDumpStdTest "T565" , compileAndDumpStdTest "T567" , compileAndDumpStdTest "T571" , compileAndDumpStdTest "T581" diff --git a/singletons-base/tests/compile-and-dump/Singletons/T565.golden b/singletons-base/tests/compile-and-dump/Singletons/T565.golden new file mode 100644 index 00000000..b3fe9409 --- /dev/null +++ b/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 diff --git a/singletons-base/tests/compile-and-dump/Singletons/T565.hs b/singletons-base/tests/compile-and-dump/Singletons/T565.hs new file mode 100644 index 00000000..deb21007 --- /dev/null +++ b/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 + |]) diff --git a/singletons-th/src/Data/Singletons/TH/Single/Data.hs b/singletons-th/src/Data/Singletons/TH/Single/Data.hs index 5c92c644..2b71ce91 100644 --- a/singletons-th/src/Data/Singletons/TH/Single/Data.hs +++ b/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 diff --git a/singletons-th/src/Data/Singletons/TH/Single/Type.hs b/singletons-th/src/Data/Singletons/TH/Single/Type.hs index 27f7d1a4..09805389 100644 --- a/singletons-th/src/Data/Singletons/TH/Single/Type.hs +++ b/singletons-th/src/Data/Singletons/TH/Single/Type.hs @@ -36,7 +36,7 @@ singType prom ty = do res' = singFamily `DAppT` (foldType prom (map DVarT arg_names) `DSigT` prom_res) -- Make sure to include an explicit `prom_res` kind annotation. -- See Note [Preserve the order of type variables during singling], - -- wrinkle 3. + -- wrinkle 2. arg_tvbs = zipWith (`DKindedTV` SpecifiedSpec) arg_names prom_args -- If the original type signature lacks an explicit `forall`, then do not -- give the singled type signature an outermost `forall`. Instead, give it @@ -204,56 +204,7 @@ Some further complications: SMkT :: forall a (x :: a). Sing x -> ST (MkT x) ----- --- Wrinkle 2: The TH reification swamp ------ - -There is another issue with type signatures that lack explicit `forall`s, one -which the current design of Template Haskell does not make simple to fix. -If we single code that is wrapped in TH quotes, such as in the following example: - - {-# LANGUAGE PolyKinds, ... #-} - $(singletons [d| - data Proxy a = MkProxy - |]) - -Then our job is made much easier when singling MkProxy, since we know that the -only type variable that must be quantified is `a`, as that is the only one -specified by the user. This results in the following type signature for -MkProxy: - - MkProxy :: forall a. Proxy a - -However, this is not the only possible way to single MkProxy. One can -alternatively use $(genSingletons [''Proxy]), which uses TH reification to -infer the type of MkProxy. There is perilous, however, because this is how -TH reifies Proxy: - - DataD - [] ''Proxy [KindedTV a () (VarT k)] Nothing - [NormalC 'MkProxy []] - [] - -We must then construct a type signature for MkProxy using nothing but the type -variables from the data type header. But notice that `KindedTV a () (VarT k)` -gives no indication of whether `k` is specified or inferred! As a result, we -conservatively assume that `k` is specified, resulting the following type -signature for MkProxy: - - MkProxy :: forall k (a :: k). Proxy a - -Contrast this with `MkProxy :: Proxy a`, where `k` is inferred. In other words, -if you single MkProxy using genSingletons, then `Proxy @True` will typecheck -but `SMkProxy @True` will /not/ typecheck—you'd have to use -`SMkProxy @_ @True` instead. Urk! - -At present, Template Haskell does not have a way to distinguish among the -specificities bound by a data type header. Without this knowledge, it is -unclear how one could work around this issue. Thankfully, this issue is -only likely to surface in very limited circumstances, so the damage is somewhat -minimal. - ------ --- Wrinkle 3: Where to put explicit kind annotations +-- Wrinkle 2: Where to put explicit kind annotations ----- Type variable binders are only part of the story—we must also determine what @@ -304,28 +255,49 @@ instead: SNothing :: forall a. SMaybe (Nothing @a) This does work for many cases, but there are also some corner cases where this -approach fails. Recall the `MkProxy` example from Wrinkle 2 above: - - {-# LANGUAGE PolyKinds, ... #-} - data Proxy a = MkProxy - $(genSingletons [''Proxy]) - -Due to the design of Template Haskell (discussed in Wrinkle 2), `MkProxy` will -be reified with the type of `forall k (a :: k). Proxy a`. This means that -if we used visible kind applications in the result type, we would end up with -this: - - SMkProxy :: forall k (a :: k). SProxy (MkProxy @k @a) - -This will not kind-check because MkProxy only accepts /one/ visible kind argument, -whereas this supplies it with two. To avoid this issue, we instead use the type -`forall k (a :: k). SProxy (MkProxy :: Proxy a)`. Granted, this type is /still/ -technically wrong due to the fact that it explicitly quantifies `k`, but at the -very least it typechecks. If Template Haskell gained the ability to distinguish -among the specificities of type variables bound by a data type header -(perhaps by way of a language feature akin to -https://github.com/ghc-proposals/ghc-proposals/pull/326), then we could revisit -this design choice. +approach fails. Suppose that `Nothing` was declared like so: + + Nothing :: forall {a}. Maybe a + +Then we couldn't write `Nothing @a`, as `a` wouldn't be eligible for visible +kind application. (GHC Core would let you write `Nothing @{a}`, but this isn't +possible in source Haskell.) As such, the only way to fix the type of `a` in +`Maybe a` would be to write `Nothing :: Maybe a`. + +An even more obscure corner case is when a type quantifies a type variable +without mentioning it at all in the rest of the type, e.g., + + C :: forall a. D + +At present, singletons-th does not handle this type of corner case at all. It +wouldn't suffice to single `C` to the following: + + SC :: forall a. SD (C :: D) + +This is because the `a` argument to `C` is left ambiguous in the type `C :: D`, +as the return kind `D` doesn't indicate what `a` should be. In theory, we +/could/ write `C @a :: D` instead, which would solve that particular problem. +But there would still be trouble on the horizon, as there are other types of +code that singletons-th generates which exhibit similar sorts of ambiguity. For +example, here is the defunctionalization symbol that singletons-th would +generate for `C`: + + type CSym0 :: forall a. D + type family CSym0 @a :: D where + CSym0 = C + +GHC will reject this type family equation, also for ambiguity-related reasons: + + error: [GHC-16220] + • Uninferrable type variables k0, (a0 :: k0) in + the type family equation right-hand side: C @{k0} @a0 + • In the type family declaration for ‘CSym0’ + +This is fixable, but we would need to audit all potential sources of type +variable-related ambiguity in singletons-th–generated code and make sure that +we have covered our bases. Given that types such as `forall a. D` are rare in +practice, I'm inclined not to worry about this unless someone specifically asks +for this featurette. Finally, note that we need only write `Sing x_1 -> ... -> Sing x_p`, and not `Sing (x_1 :: PT_1) -> ... Sing (x_p :: PT_p)`. This is simply because we