From cc1c7f69f1483ccbb6e4b92cf63ef792a729f837 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 16 Jun 2024 10:56:20 -0400 Subject: [PATCH 1/3] Partially revert TypeAbstractions-related changes in #596 The changes in #596 cause `singletons-th` to use `TypeAbstractions` to explicitly quantify the kind variables of promoted class methods whenever the parent class has a standalone kind signature, thereby ensuring that the order of kind variables matches the order in which the user wrote them. At least, that was the intention. Unfortunately, as #605 reveals, this approach sometimes causes `singletons-th` to generate ill-kinded code for promoted class methods, and there isn't an obvious way to work around this limitation. As such, this patch reverts the `TypeAbstractions`-related changes from #596. Once again, `singletons-th` now does not make any guarantees about the order of kind variables for promoted class methods or their defunctionalization symbols. On the other hand, this patch _does_ keep the changes from #596 that cause `singletons-th` to propagate kind information from the parent class's standalone kind signature through to the promoted class methods' defunctionalization symbols, as this feature is useful independent of the `TypeAbstractions`-related changes. I have taken the opportunity to document why we do this in the new `Note [Propagating kind information from class standalone kind signatures]` in `D.S.TH.Promote`. I've removed the `T589` test case, as the functionality it was testing no longer exists after reverting the `TypeAbstractions`-related changes. I have also added a new `T605` test case that ensures that the regression from #605 stays fixed. In a subsequent commit, I will add another test case that demonstrates that the kind propagation works as intended. Fixes #605. --- README.md | 70 +--- .../tests/SingletonsBaseTestSuite.hs | 2 +- .../compile-and-dump/Promote/T605.golden | 39 ++ .../tests/compile-and-dump/Promote/T605.hs | 11 + .../compile-and-dump/Singletons/T326.golden | 4 +- .../compile-and-dump/Singletons/T378b.golden | 2 +- .../compile-and-dump/Singletons/T412.golden | 2 +- .../compile-and-dump/Singletons/T414.golden | 2 +- .../compile-and-dump/Singletons/T589.golden | 127 ------ .../tests/compile-and-dump/Singletons/T589.hs | 59 --- .../Singletons/TypeAbstractions.golden | 10 +- singletons-th/CHANGES.md | 4 - .../src/Data/Singletons/TH/Promote.hs | 387 ++++++++---------- .../src/Data/Singletons/TH/Promote/Defun.hs | 80 +--- singletons-th/src/Data/Singletons/TH/Util.hs | 4 - 15 files changed, 262 insertions(+), 541 deletions(-) create mode 100644 singletons-base/tests/compile-and-dump/Promote/T605.golden create mode 100644 singletons-base/tests/compile-and-dump/Promote/T605.hs delete mode 100644 singletons-base/tests/compile-and-dump/Singletons/T589.golden delete mode 100644 singletons-base/tests/compile-and-dump/Singletons/T589.hs diff --git a/README.md b/README.md index 5f2b9771..926b0a65 100644 --- a/README.md +++ b/README.md @@ -1179,72 +1179,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 diff --git a/singletons-base/tests/SingletonsBaseTestSuite.hs b/singletons-base/tests/SingletonsBaseTestSuite.hs index 14988c72..8698b7c3 100644 --- a/singletons-base/tests/SingletonsBaseTestSuite.hs +++ b/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 diff --git a/singletons-base/tests/compile-and-dump/Promote/T605.golden b/singletons-base/tests/compile-and-dump/Promote/T605.golden new file mode 100644 index 00000000..b6b54e9f --- /dev/null +++ b/singletons-base/tests/compile-and-dump/Promote/T605.golden @@ -0,0 +1,39 @@ +Promote/T605.hs:(0,0)-(0,0): Splicing declarations + promoteOnly + [d| type Traversable' :: (Type -> Type) -> Constraint + + class (Functor t, Foldable t) => Traversable' t where + traverse' :: Applicative f => (a -> f b) -> t a -> t (f b) |] + ======> + type Traverse'Sym0 :: forall (t :: Type -> Type) + a + f + b. (~>) ((~>) a (f b)) ((~>) (t a) (t (f b))) + data Traverse'Sym0 :: (~>) ((~>) a (f b)) ((~>) (t a) (t (f b))) + where + Traverse'Sym0KindInference :: SameKind (Apply Traverse'Sym0 arg) (Traverse'Sym1 arg) => + Traverse'Sym0 a0123456789876543210 + type instance Apply Traverse'Sym0 a0123456789876543210 = Traverse'Sym1 a0123456789876543210 + instance SuppressUnusedWarnings Traverse'Sym0 where + suppressUnusedWarnings = snd ((,) Traverse'Sym0KindInference ()) + type Traverse'Sym1 :: forall (t :: Type -> Type) + a + f + b. (~>) a (f b) -> (~>) (t a) (t (f b)) + data Traverse'Sym1 (a0123456789876543210 :: (~>) a (f b)) :: (~>) (t a) (t (f b)) + where + Traverse'Sym1KindInference :: SameKind (Apply (Traverse'Sym1 a0123456789876543210) arg) (Traverse'Sym2 a0123456789876543210 arg) => + Traverse'Sym1 a0123456789876543210 a0123456789876543210 + type instance Apply (Traverse'Sym1 a0123456789876543210) a0123456789876543210 = Traverse' a0123456789876543210 a0123456789876543210 + instance SuppressUnusedWarnings (Traverse'Sym1 a0123456789876543210) where + suppressUnusedWarnings = snd ((,) Traverse'Sym1KindInference ()) + type Traverse'Sym2 :: forall (t :: Type -> Type) + a + f + b. (~>) a (f b) -> t a -> t (f b) + type family Traverse'Sym2 @(t :: Type + -> Type) @a @f @b (a0123456789876543210 :: (~>) a (f b)) (a0123456789876543210 :: t a) :: t (f b) where + Traverse'Sym2 a0123456789876543210 a0123456789876543210 = Traverse' a0123456789876543210 a0123456789876543210 + type PTraversable' :: (Type -> Type) -> Constraint + class PTraversable' t where + type family Traverse' (arg :: (~>) a (f b)) (arg :: t a) :: t (f b) diff --git a/singletons-base/tests/compile-and-dump/Promote/T605.hs b/singletons-base/tests/compile-and-dump/Promote/T605.hs new file mode 100644 index 00000000..f307475e --- /dev/null +++ b/singletons-base/tests/compile-and-dump/Promote/T605.hs @@ -0,0 +1,11 @@ +module T605 where + +import Data.Kind +import Data.Singletons.Base.TH +import Prelude.Singletons + +$(promoteOnly [d| + type Traversable' :: (Type -> Type) -> Constraint + class (Functor t, Foldable t) => Traversable' t where + traverse' :: Applicative f => (a -> f b) -> t a -> t (f b) + |]) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T326.golden b/singletons-base/tests/compile-and-dump/Singletons/T326.golden index fb6f759a..e9df6e8a 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T326.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T326.golden @@ -25,7 +25,7 @@ Singletons/T326.hs:0:0:: Splicing declarations infixl 9 <%>@#@$$$ type PC1 :: Type -> Constraint class PC1 (a :: Type) where - type family (<%>) @(a :: Type) (arg :: a) (arg :: a) :: a + type family (<%>) (arg :: a) (arg :: a) :: a infixl 9 <%> Singletons/T326.hs:0:0:: Splicing declarations genSingletons [''C2] @@ -54,7 +54,7 @@ Singletons/T326.hs:0:0:: Splicing declarations infixl 9 <%%>@#@$$$ type PC2 :: Type -> Constraint class PC2 (a :: Type) where - type family (<%%>) @(a :: Type) (arg :: a) (arg :: a) :: a + type family (<%%>) (arg :: a) (arg :: a) :: a infixl 9 <%%> class SC2 (a :: Type) where (%<%%>) :: diff --git a/singletons-base/tests/compile-and-dump/Singletons/T378b.golden b/singletons-base/tests/compile-and-dump/Singletons/T378b.golden index cc31d5ae..81b3db76 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T378b.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T378b.golden @@ -74,7 +74,7 @@ Singletons/T378b.hs:(0,0)-(0,0): Splicing declarations type family F @b @a (a :: a) (a :: b) :: () where F @b @a (_ :: a) (_ :: b) = Tuple0Sym0 type PC :: forall b a. a -> b -> Constraint - class PC @b @a (x :: a) (y :: b) + class PC x y sNatMinus :: (forall (t :: Nat) (t :: Nat). Sing t diff --git a/singletons-base/tests/compile-and-dump/Singletons/T412.golden b/singletons-base/tests/compile-and-dump/Singletons/T412.golden index dc1e31a3..761aa0c0 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T412.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T412.golden @@ -225,7 +225,7 @@ Singletons/T412.hs:0:0:: Splicing declarations infix 6 `M2Sym2` type PC2 :: Type -> Type -> Constraint class PC2 (a :: Type) (b :: Type) where - type family M2 @(a :: Type) @(b :: Type) (arg :: a) (arg :: b) :: Bool + type family M2 (arg :: a) (arg :: b) :: Bool infix 5 `PC2` infix 6 `M2` class SC2 (a :: Type) (b :: Type) where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T414.golden b/singletons-base/tests/compile-and-dump/Singletons/T414.golden index 0d97f536..a317c607 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T414.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T414.golden @@ -70,7 +70,7 @@ Singletons/T414.hs:(0,0)-(0,0): Splicing declarations type family T3Sym2 (a0123456789876543210 :: Bool) (a0123456789876543210 :: Type) :: Type where T3Sym2 a0123456789876543210 a0123456789876543210 = T3 a0123456789876543210 a0123456789876543210 type PC3 :: Bool -> Constraint - class PC3 (a :: Bool) + class PC3 a class SC1 (a :: Bool) class SC2 a class SC3 a diff --git a/singletons-base/tests/compile-and-dump/Singletons/T589.golden b/singletons-base/tests/compile-and-dump/Singletons/T589.golden deleted file mode 100644 index 1cea4900..00000000 --- a/singletons-base/tests/compile-and-dump/Singletons/T589.golden +++ /dev/null @@ -1,127 +0,0 @@ -Singletons/T589.hs:(0,0)-(0,0): Splicing declarations - singletons - [d| type C1 :: Type -> Constraint - type C2 :: k -> Constraint - - class C1 b where - m1 :: forall a. a -> b -> a - class C2 b where - m2 :: a -> Proxy b - - instance C1 Ordering where - m1 x _ = x - instance C2 Ordering where - m2 _ = Proxy |] - ======> - type C1 :: Type -> Constraint - class C1 b where - m1 :: forall a. a -> b -> a - instance C1 Ordering where - m1 x _ = x - type C2 :: k -> Constraint - class C2 b where - m2 :: a -> Proxy b - instance C2 Ordering where - m2 _ = Proxy - type M1Sym0 :: forall (b :: Type) a. (~>) a ((~>) b a) - data M1Sym0 :: (~>) a ((~>) b a) - where - M1Sym0KindInference :: SameKind (Apply M1Sym0 arg) (M1Sym1 arg) => - M1Sym0 a0123456789876543210 - type instance Apply M1Sym0 a0123456789876543210 = M1Sym1 a0123456789876543210 - instance SuppressUnusedWarnings M1Sym0 where - suppressUnusedWarnings = snd ((,) M1Sym0KindInference ()) - type M1Sym1 :: forall (b :: Type) a. a -> (~>) b a - data M1Sym1 (a0123456789876543210 :: a) :: (~>) b a - where - M1Sym1KindInference :: SameKind (Apply (M1Sym1 a0123456789876543210) arg) (M1Sym2 a0123456789876543210 arg) => - M1Sym1 a0123456789876543210 a0123456789876543210 - type instance Apply (M1Sym1 a0123456789876543210) a0123456789876543210 = M1 a0123456789876543210 a0123456789876543210 - instance SuppressUnusedWarnings (M1Sym1 a0123456789876543210) where - suppressUnusedWarnings = snd ((,) M1Sym1KindInference ()) - type M1Sym2 :: forall (b :: Type) a. a -> b -> a - type family M1Sym2 @(b :: Type) @a (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where - M1Sym2 a0123456789876543210 a0123456789876543210 = M1 a0123456789876543210 a0123456789876543210 - type PC1 :: Type -> Constraint - class PC1 (b :: Type) where - type family M1 @(b :: Type) @a (arg :: a) (arg :: b) :: a - type M2Sym0 :: forall k (b :: k) a. (~>) a (Proxy b) - data M2Sym0 :: (~>) a (Proxy b) - where - M2Sym0KindInference :: SameKind (Apply M2Sym0 arg) (M2Sym1 arg) => - M2Sym0 a0123456789876543210 - type instance Apply M2Sym0 a0123456789876543210 = M2 a0123456789876543210 - instance SuppressUnusedWarnings M2Sym0 where - suppressUnusedWarnings = snd ((,) M2Sym0KindInference ()) - type M2Sym1 :: forall k (b :: k) a. a -> Proxy b - type family M2Sym1 @k @(b :: k) @a (a0123456789876543210 :: a) :: Proxy b where - M2Sym1 a0123456789876543210 = M2 a0123456789876543210 - type PC2 :: k -> Constraint - class PC2 @k (b :: k) where - type family M2 @k @(b :: k) @a (arg :: a) :: Proxy b - type M1_0123456789876543210 :: forall a. a -> Ordering -> a - type family M1_0123456789876543210 @a (a :: a) (a :: Ordering) :: a where - M1_0123456789876543210 @a x _ = x - type M1_0123456789876543210Sym0 :: forall a. (~>) a ((~>) Ordering a) - data M1_0123456789876543210Sym0 :: (~>) a ((~>) Ordering a) - where - M1_0123456789876543210Sym0KindInference :: SameKind (Apply M1_0123456789876543210Sym0 arg) (M1_0123456789876543210Sym1 arg) => - M1_0123456789876543210Sym0 a0123456789876543210 - type instance Apply M1_0123456789876543210Sym0 a0123456789876543210 = M1_0123456789876543210Sym1 a0123456789876543210 - instance SuppressUnusedWarnings M1_0123456789876543210Sym0 where - suppressUnusedWarnings - = snd ((,) M1_0123456789876543210Sym0KindInference ()) - type M1_0123456789876543210Sym1 :: forall a. a -> (~>) Ordering a - data M1_0123456789876543210Sym1 (a0123456789876543210 :: a) :: (~>) Ordering a - where - M1_0123456789876543210Sym1KindInference :: SameKind (Apply (M1_0123456789876543210Sym1 a0123456789876543210) arg) (M1_0123456789876543210Sym2 a0123456789876543210 arg) => - M1_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 - type instance Apply (M1_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = M1_0123456789876543210 a0123456789876543210 a0123456789876543210 - instance SuppressUnusedWarnings (M1_0123456789876543210Sym1 a0123456789876543210) where - suppressUnusedWarnings - = snd ((,) M1_0123456789876543210Sym1KindInference ()) - type M1_0123456789876543210Sym2 :: forall a. a -> Ordering -> a - type family M1_0123456789876543210Sym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: Ordering) :: a where - M1_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = M1_0123456789876543210 a0123456789876543210 a0123456789876543210 - instance PC1 Ordering where - type M1 a a = Apply (Apply M1_0123456789876543210Sym0 a) a - type M2_0123456789876543210 :: forall a. a -> Proxy Ordering - type family M2_0123456789876543210 @a (a :: a) :: Proxy Ordering where - M2_0123456789876543210 @a _ = ProxySym0 - type M2_0123456789876543210Sym0 :: forall a. (~>) a (Proxy Ordering) - data M2_0123456789876543210Sym0 :: (~>) a (Proxy Ordering) - where - M2_0123456789876543210Sym0KindInference :: SameKind (Apply M2_0123456789876543210Sym0 arg) (M2_0123456789876543210Sym1 arg) => - M2_0123456789876543210Sym0 a0123456789876543210 - type instance Apply M2_0123456789876543210Sym0 a0123456789876543210 = M2_0123456789876543210 a0123456789876543210 - instance SuppressUnusedWarnings M2_0123456789876543210Sym0 where - suppressUnusedWarnings - = snd ((,) M2_0123456789876543210Sym0KindInference ()) - type M2_0123456789876543210Sym1 :: forall a. a -> Proxy Ordering - type family M2_0123456789876543210Sym1 @a (a0123456789876543210 :: a) :: Proxy Ordering where - M2_0123456789876543210Sym1 a0123456789876543210 = M2_0123456789876543210 a0123456789876543210 - instance PC2 Ordering where - type M2 a = Apply M2_0123456789876543210Sym0 a - class SC1 b where - sM1 :: - forall a (t :: a) (t :: b). Sing t - -> Sing t -> Sing (Apply (Apply M1Sym0 t) t :: a) - class SC2 b where - sM2 :: - (forall (t :: a). - Sing t -> Sing (Apply M2Sym0 t :: Proxy b) :: Type) - instance SC1 Ordering where - sM1 (sX :: Sing x) _ = sX - instance SC2 Ordering where - sM2 _ = SProxy - type SC1 :: Type -> Constraint - instance SC1 b => SingI (M1Sym0 :: (~>) a ((~>) b a)) where - sing = singFun2 @M1Sym0 sM1 - instance (SC1 b, SingI d) => - SingI (M1Sym1 (d :: a) :: (~>) b a) where - sing = singFun1 @(M1Sym1 (d :: a)) (sM1 (sing @d)) - instance SC1 b => SingI1 (M1Sym1 :: a -> (~>) b a) where - liftSing (s :: Sing (d :: a)) = singFun1 @(M1Sym1 (d :: a)) (sM1 s) - type SC2 :: k -> Constraint - instance SC2 b => SingI (M2Sym0 :: (~>) a (Proxy b)) where - sing = singFun1 @M2Sym0 sM2 diff --git a/singletons-base/tests/compile-and-dump/Singletons/T589.hs b/singletons-base/tests/compile-and-dump/Singletons/T589.hs deleted file mode 100644 index 6a9278b8..00000000 --- a/singletons-base/tests/compile-and-dump/Singletons/T589.hs +++ /dev/null @@ -1,59 +0,0 @@ -module T589 where - -import Data.Kind -import Data.Proxy -import Data.Proxy.Singletons -import Data.Singletons.Base.TH -import Prelude.Singletons - -$(singletons [d| - type C1 :: Type -> Constraint - class C1 b where - m1 :: forall a. a -> b -> a - - instance C1 Ordering where - m1 x _ = x - - type C2 :: k -> Constraint - class C2 b where - m2 :: a -> Proxy b - - instance C2 Ordering where - m2 _ = Proxy - |]) - --- Test some type variable orderings -m1Ex :: Bool -> Ordering -> Bool -m1Ex = m1 @Ordering @Bool - -type M1Ex :: Bool -type M1Ex = M1 @Ordering @Bool True EQ - -type M1Ex0 :: Bool ~> Ordering ~> Bool -type M1Ex0 = M1Sym0 @Ordering @Bool - -type M1Ex1 :: Bool -> Ordering ~> Bool -type M1Ex1 = M1Sym1 @Ordering @Bool - -type M1Ex2 :: Bool -type M1Ex2 = M1Sym2 @Ordering @Bool True EQ - -sM1Ex :: forall (x :: Bool) (y :: Ordering). - Sing x -> Sing y -> Sing (M1 @Ordering @Bool x y) -sM1Ex = sM1 @Ordering @Bool - -m2Ex :: Bool -> Proxy Ordering -m2Ex = m2 @Type @Ordering @Bool - -type M2Ex :: Proxy Ordering -type M2Ex = M2 @Type @Ordering @Bool True - -type M2Ex0 :: Bool ~> Proxy Ordering -type M2Ex0 = M2Sym0 @Type @Ordering @Bool - -type M2Ex1 :: Proxy Ordering -type M2Ex1 = M2Sym1 @Type @Ordering @Bool True - -sM2Ex :: forall (x :: Bool). - Sing x -> Sing (M2 @Type @Ordering @Bool x) -sM2Ex = sM2 @Type @Ordering @Bool diff --git a/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden b/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden index a52c42dd..15ea8bd6 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden @@ -184,7 +184,7 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations Meth1Sym1 a0123456789876543210 = Meth1 a0123456789876543210 type PC1 :: forall j k. j -> k -> Constraint class PC1 @j @k (a :: j) (b :: k) where - type family Meth1 @j @k @(a :: j) @(b :: k) (arg :: Proxy a) :: Proxy b + type family Meth1 (arg :: Proxy a) :: Proxy b type Meth2Sym0 :: forall x y (a :: x) @@ -201,7 +201,7 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations Meth2Sym1 a0123456789876543210 = Meth2 a0123456789876543210 type PC2 :: forall j k. j -> k -> Constraint class PC2 @x @y (a :: x) (b :: y) where - type family Meth2 @x @y @(a :: x) @(b :: y) (arg :: Proxy a) :: Proxy b + type family Meth2 (arg :: Proxy a) :: Proxy b type Meth3Sym0 :: forall j (a :: j) k @@ -218,13 +218,13 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations Meth3Sym1 a0123456789876543210 = Meth3 a0123456789876543210 type PC3 :: forall j. j -> forall k. k -> Constraint class PC3 @j (a :: j) @k (b :: k) where - type family Meth3 @j @(a :: j) @k @(b :: k) (arg :: Proxy a) :: Proxy b + type family Meth3 (arg :: Proxy a) :: Proxy b type Meth4Sym0 :: forall (a :: Type). a type family Meth4Sym0 @(a :: Type) :: a where Meth4Sym0 = Meth4 type PC4 :: forall (a :: Type). Constraint - class PC4 @(a :: Type) where - type family Meth4 @(a :: Type) :: a + class PC4 @a where + type family Meth4 :: a type SD1 :: forall j k (a :: j) (b :: k). D1 @j @k a b -> Type data SD1 :: forall j k (a :: j) (b :: k). D1 @j @k a b -> Type where diff --git a/singletons-th/CHANGES.md b/singletons-th/CHANGES.md index 386e415a..29cb7000 100644 --- a/singletons-th/CHANGES.md +++ b/singletons-th/CHANGES.md @@ -5,10 +5,6 @@ next [????.??.??] ----------------- * Add support for promoting and singling type variables that scope over the bodies of class method defaults and instance methods. -* When promoting a class with a standalone kind signature, `singletons-th` will - now guarantee that the promoted class methods will quantify their kind - variables in the exact same order as the type variables in the original class - methods' types. 3.4 [2024.05.12] ---------------- diff --git a/singletons-th/src/Data/Singletons/TH/Promote.hs b/singletons-th/src/Data/Singletons/TH/Promote.hs index 694790bb..6ec9bb22 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote.hs @@ -277,16 +277,9 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name -- If the class has a standalone kind signature, we take the original, -- user-written class binders (`orig_cls_tvbs`) and fill them out using -- `matchUpSAKWithDecl` to produce the "full" binders, as described in - -- Note [Promoted class methods and kind variable ordering] (Case 1: - -- Parent class with standalone kind signature). + -- Note [Propagating kind information from class standalone kind signatures]. mb_full_cls_tvbs <- traverse (\cls_sak -> matchUpSAKWithDecl cls_sak orig_cls_tvbs) mb_cls_sak - -- Compute the DTyVarBndrVis binders to use in the promoted class declaration. - -- If the class has a standalone kind signature, these will be the full - -- binders (see `mb_full_cls_tvbs above`). Otherwise, these will be the - -- original binders (`orig_cls_tvbs`). - let pro_cls_tvbs_vis = - maybe orig_cls_tvbs tvbForAllTyFlagsToBndrVis mb_full_cls_tvbs sig_decs <- mapM (uncurry (promote_sig mb_full_cls_tvbs)) meth_sigs_list (default_decs, ann_rhss, prom_rhss) @@ -298,7 +291,7 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name cls_infix_decls <- promoteReifiedInfixDecls $ cls_name:meth_names -- no need to do anything to the fundeps. They work as is! - let pro_cls_dec = DClassD [] pClsName pro_cls_tvbs_vis fundeps + let pro_cls_dec = DClassD [] pClsName orig_cls_tvbs fundeps (sig_decs ++ default_decs ++ infix_decls') mb_pro_cls_sak = fmap (DKiSigD pClsName) mb_cls_sak emitDecs $ maybeToList mb_pro_cls_sak ++ pro_cls_dec:cls_infix_decls @@ -312,10 +305,9 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name Maybe [DTyVarBndr ForAllTyFlag] -- ^ If the parent class has a standalone kind signature, then this -- will be @'Just' full_bndrs@, where @full_bndrs@ are the full type - -- variable binders described in - -- @Note [Promoted class methods and kind variable ordering]@ (Case 1: - -- Parent class with standalone kind signature). Otherwise, this will - -- be 'Nothing'. + -- variable binders described in @Note [Propagating kind information + -- from class standalone kind signatures]@. Otherwise, this will be + -- 'Nothing'. -> Name -- ^ The class method's name. -> DType @@ -325,69 +317,47 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name promote_sig mb_full_cls_tvbs name meth_ty = do opts <- getOptions let proName = promotedTopLevelValueName opts name - (meth_expl_tvbs, meth_arg_kis, meth_res_ki) <- promoteUnraveled meth_ty + (_, meth_arg_kis, meth_res_ki) <- promoteUnraveled meth_ty args <- mapM (const $ qNewName "arg") meth_arg_kis let pro_meth_args = zipWith (`DKindedTV` BndrReq) args meth_arg_kis - -- Compute the type variables to use in the invisible `forall`s in the - -- defunctionalization symbols' standalone kind signatures. + -- Binders for all of the type variables mentioned in the argument and + -- result kinds of the promoted class method. This includes both class + -- variables and variables that only scope over the method itself. + -- + -- This quantifies the variables in a simple left-to-right order, + -- which may not be the same order in which the original method's type + -- quantifies them. This is a known limitation: see + -- Note [Promoted class methods and kind variable ordering]. + meth_tvbs = changeDTVFlags SpecifiedSpec $ + toposortTyVarsOf $ meth_arg_kis ++ [meth_res_ki] + -- The type variable binders to use in the standalone kind signatures + -- for the promoted class method's defunctionalization symbols. meth_sak_tvbs = case tvbForAllTyFlagsToSpecs <$> mb_full_cls_tvbs of - -- If the parent class has a standalone kind signature, then make - -- sure that the order of type variables in the `forall`s matches - -- the order in the method's original type signature. As described - -- in Note [Promoted class methods and kind variable ordering] - -- (Case 1: Parent class with standalone kind signature), this - -- consists of the class variables (`full_cls_tvbs_spec`) followed - -- by the method variables (see `meth_tvbs` below). + -- If the parent class has a standalone kind signature, then + -- propagate as much of the kind information as possible by + -- incorporating the full class binders. See Note [Propagating + -- kind information from class standalone kind signatures]. Just full_cls_tvbs_spec -> - -- Compute the type variabes that the method's type signature - -- quantifies. - let meth_tvbs - -- If the method's type signature lacks an explicit - -- `forall`, then we infer the order in which the method - -- implicitly quantifies its type variables using - -- `toposortTyVarsOf`. Make sure to exclude the type - -- variables already bound by the class header, as we - -- don't want to re-quantify them. - | null meth_expl_tvbs - = deleteFirstsBy - ((==) `on` extractTvbName) - (changeDTVFlags SpecifiedSpec - (toposortTyVarsOf (meth_arg_kis ++ [meth_res_ki]))) - full_cls_tvbs_spec - -- If the method's type signature has an explicit - -- `forall`,then just use the type variables quantified by - -- that `forall`. - | otherwise - = meth_expl_tvbs in - full_cls_tvbs_spec ++ meth_tvbs + -- `meth_tvbs` can include class binder names, so make sure to + -- delete type variables from `meth_tvbs` whose names are also + -- bound by the full class binders. + let meth_tvbs_without_cls_tvbs = + deleteFirstsBy + ((==) `on` extractTvbName) + meth_tvbs + full_cls_tvbs_spec in + full_cls_tvbs_spec ++ meth_tvbs_without_cls_tvbs -- If the parent class lacks a standalone kind signature, then we - -- cannot make any guarantees about the order in which the type - -- variables appear. Still, we should at least pick /some/ order - -- for the type variables. We compute the type variable binders in - -- a left-to-right order, since that is the same order that the - -- promoted method's kind will use. See - -- Note [Promoted class methods and kind variable ordering] - -- (Case 2: Parent class without standalone kind signature). + -- simply return `meth_tvbs`. Nothing -> - changeDTVFlags SpecifiedSpec $ - toposortTyVarsOf $ meth_arg_kis ++ [meth_res_ki] + meth_tvbs meth_sak = ravelVanillaDType meth_sak_tvbs [] meth_arg_kis meth_res_ki - -- All of the type variable binders to use in the promoted method - -- declaration. If the parent class has a standalone kind signature, - -- these will include both invisible binders (`meth_sak_tvbs`) and - -- visible binders (`pro_meth_args`). Otherwise, this will only - -- include visible binders (`pro_meth_args`). - all_meth_tvbs - | isJust mb_full_cls_tvbs - = tvbSpecsToBndrVis meth_sak_tvbs ++ pro_meth_args - | otherwise - = pro_meth_args m_fixity <- reifyFixityWithLocals name emitDecsM $ defunctionalize proName m_fixity $ DefunSAK meth_sak return $ DOpenTypeFamilyD (DTypeFamilyHead proName - all_meth_tvbs + pro_meth_args (DKindSig meth_res_ki) Nothing) @@ -395,172 +365,159 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name Note [Promoted class methods and kind variable ordering] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In general, we make an effort to preserve the order of type variables when -promoting type signatures, but there is a corner case where this is difficult: -class methods. +promoting type signatures, but there is an annoying corner case where this is +difficult: class methods. When promoting class methods, the order of kind +variables in their kinds will often "just work" by happy coincidence, but +there are some situations where this does not happen. Consider the following +class: -Specifically, we are able only able to preserve the order of type variables in -class method types when the parent class has a standalone kind signature. This -is because we use the TypeAbstractions language extension to explicitly bind -the promoted classes' kind variables in the intended order, and one can only -use TypeAbstractions in associated type families when the parent class has a -standalone kind signature. (Let's call this Case 1.) - -The flip side is that when the parent class lacks a standalone kind signature, -we cannot use TypeAbstractions in the promoted classes. In such cases, we -cannot make any guarantees about the order of kind variables for promoted -classes. (Let's call this Case 2.) - ------ --- Case 1: Parent class with standalone kind signature ------ - -As an example, consider: - - type C :: Type -> Constraint - class C b 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 `m`: - - type PC :: Type -> Constraint - class PC b where - type M @b @a (x :: a) (y :: b) :: a - -Here, we use TypeAbstractions to explicitly bind `b` before `a` in the -declaration for `M`, thus ensuring that `M :: forall b a. a -> b -> a`. We -preserve this order of kind variables in `M`'s defunctionalization symbols as -well: - - type MSym0 :: forall b a. a ~> b ~> a - type MSym1 :: forall b a. a -> b ~> a - -Therefore, the trick is to figure out what variables to bind with -TypeAbstractions in the promoted class declarations. Roughly speaking, we have -the following formula: - - type M @ ... @ ... ... :: - -In the example above: - -* The class variables are: @b -* The method variables are: @a -* The method arguments are: (x :: a) (y :: b) -* The method result is: a - -The hardest part of this formula to get right are the class variables. Here is -a slightly more interesting example which illustrates the challenges: - - type C :: k -> Constraint - class C b where - m :: forall a. a -> Proxy b - -A naïve attempt at promoting `C` would be: - - type PC :: k -> Constraint - class PC b where - type M @b @a (x :: a) :: Proxy b - -However, this is not quite right. This is because `k` is specified in the type -of `m`: - - m :: forall k (b :: k). C b => forall a. a -> Proxy b - -But `k` is /inferred/ in the kind of `M`: - - M :: forall {k} (b :: k) a. a -> Proxy b - -The reason this happens is because GHC determines the visibilities of kind -variables for associated type families independently of the parent class's -standalone kind signature. That is, it only considers `type M @b @a (x :: a) :: -Proxy b` in isolation, and since we didn't write out `k` explicitly in this -declaration, GHC considers `k` to be inferred. - -In order to make `k` specified in `M`'s kind, we need to instead promote `C` to -something that looks closer to this: - - type PC :: k -> Constraint - class PC @k (b :: k) where - type M @k @(b :: k) @a (x :: a) :: Proxy b - -- Because we wrote out `k`, we now have: - -- M :: forall {k} (b :: k) a. a -> Proxy b - -In the declaration for `M`, we have: - -* The class variables are: @k @(b :: k) -* The method variables are: @a -* The method arguments are: (x :: a) -* The method result is: Proxy b - -Note that we now have `class PC @k (b :: k)` instead of simply `class PC b`. -This is a slight departure from what the user originally wrote (without any @ -binders), but it is a necessary departure, as `k` would not be in scope over -the definition of `M` otherwise. - -As such, we need a way to go from `class PC b` (which lacks the `k` from the -standalone kind signature) to `class PC @k (b :: k)` (which does include `k`). -Let's call the former's type variable binders the /original/ binders, and let's -call the latter's type variable binders the /full/ binders. (They are "full" in -the sense that we have filled them out using type variable binders from the -standalone kind signature.) - -We use the `matchUpSAKWithDecl` function to take the original binders (plus the -parent class's standalone kind signature) as input and produce the full binders -as output. With the full binders in hand, we can complete the rest of the -promoted class declaration: - -* We can produce the `@k (b :: k)` part of `class PC @k (b :: k)` by calling - `tvbForAllTyFlagsToVis` on the full binders. -* For each promoted method `M`, we can produce the in - `type M @ ...` by calling - `tvbSpecsToBndrVis . tvbForAllTyFlagsToSpecs` on the full binders. Note that - this is /not/ the same thing as calling `tvbForAllTyFlagsToVis`, as we want - all of the to be invisible, which `tvbSpecsToBndrVis` - accomplishes. - ------ --- Case 2: Parent class without standalone kind signature ------ - -If the parent class does /not/ have a standalone kind signature, then we do 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 class: - - -- No standalone kind signature - 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`. This order is preserved when singling `m`, but *not* when promoting `m`. This is because the `C` class is promoted as follows: - -- No standalone kind signature - class PC b where + class PC (b :: Type) where type M (x :: a) (y :: b) :: a -Because `PC` does not have a standalone kind signature, 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. + +The defunctionalization symbols for `M` will also follow a similar +order of type variables: type MSym0 :: forall a b. a ~> b ~> a type MSym1 :: forall a b. a -> b ~> a -There is one potential hack we could use to rectify this: +In the past, we have considered different ways to rectify this, but none of +the approaches that we have tried are quite satisfactory: + +* We could hackily specify the order of kind variables using a type synonym + like `FlipConst`: + + type FlipConst x y = y + class PC (b :: Type) where + type M (x :: FlipConst '(b, a) a) (y :: b) :: a + + Using `FlipConst` would cause `b` to be mentioned before `a`, which would give + `M` the kind `forall b a. FlipConst '(b, a) a -> b -> a`. While the order of + type variables would be preserved, the downside is that the ugly `FlipConst` + type synonym leaks into the kind. I'm not particularly fond of this, so I have + decided not to use this hack unless someone specifically requests it. - type FlipConst x y = y - class PC b where - type M (x :: FlipConst '(b, a) a) (y :: b) :: a +* We could specify the order of kind variables using the TypeAbstractions + language extension: + + class PC (b :: Type) where + type M @(b :: Type) @a (x :: a) (y :: b) :: a -Using `FlipConst` would cause `b` to be mentioned before `a`, which would give -`M` the kind `forall b a. FlipConst '(b, a) a -> b -> a`. While the order of -type variables would be preserved, the downside is that the ugly `FlipConst` -type synonym leaks into the kind. I'm not particularly fond of this, so I have -decided not to use this hack unless someone specifically requests it. + This is much nicer to look at than the `FlipConst` hack above. However, this + approach has its own drawbacks. For one thing, GHC only permits using + TypeAbstractions in an associated type family declaration if its parent class + also has a standalone kind signature. As such, this trick would only work some + of the time. + + Even if we /did/ give the parent class a standalone kind signature, however, + it is still not guaranteed that the promoted method would kind-check. Consider + what would happen if you promoted this class: + + type Traversable :: (Type -> Type) -> Constraint + class (Functor t, Foldable t) => Traversable t where + traverse :: Applicative f => (a -> f b) -> t a -> t (f b) + + This would be promoted to: + + type PTraversable :: (Type -> Type) -> Constraint + class PTraversable t where + type PTraverse @(t :: Type -> Type) @f @a @b + (x :: a ~> f b) (y :: t a) :: t (f b) + + There is a subtle problem with this definition: because the `@f` binder lacks + an explicit kind signature, GHC defaults its kind to `Type`. This is very bad, + however, because `f`'s kind must be `Type -> Type`, not `Type`! Nor would it + be straightforward to generate `@(f :: Type -> Type)`, as nothing in the + original definition of `traverse` explicitly indicates that `f` has the kind + `Type -> Type`. + + In theory, we could implement kind inference inside of Template Haskell to + infer that `f :: Type -> Type`, but this is a tall order. Best to keep things + simple and not do this. + +Note [Propagating kind information from class standalone kind signatures] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider what happens when you promote this example: + + type Alternative :: (Type -> Type) -> Constraint + class Applicative f => Alternative f where + empty :: f a + ... + +We want the promoted `Empty` type family, as well as the `EmptySym0` +defunctionalization symbol, to have the kind +`forall (f :: Type -> Type) a. f a`. Giving `Empty` the appropriate kind is +easy enough, as we can simply copy over `Alternative`'s standalone kind +signature to `PAltenative`, its promoted counterpart: + + type PAlternative :: (Type -> Type) -> Constraint + class PAlternative f where + type Empty :: f a + ... + +Giving `EmptySym0` the appropriate kind is trickier, however. A naïve approach +would be to generate this: + + type EmptySym0 :: f a + type family EmptySym0 where + EmptySym0 = Empty + +This would give EmptySym0 a more general kind than what we want, however, as +GHC will generalize this to: + + EmptySym0 :: forall {k} (f :: k -> Type) (a :: k). f a + +This is undesirable, as now `EmptySym0` can be called on kinds that cannot have +`PAlternative` instances. What's more, if GHC proposal #425 were fully +implemented (see +https://github.com/ghc-proposals/ghc-proposals/blob/8443acc903437cef1a7fbb56de79b6dce77b1a09/proposals/0425-decl-invis-binders.rst#proposed-change-specification-instances), +then this code would simply not kind-check, as the left-hand side of the +`EmptySym0 = Empty` would be too general for its right-hand side. + +Instead, we strive to generate this code for `EmptySym0` instead: + + type EmptySym0 :: forall (f :: Type -> Type) a. f a + type family EmptySym0 where + EmptySym0 = Empty + +This is very doable because the user gave `Alternative` a standalone kind +signature, so it should be possible to match up the `Type -> Type` part of the +standalone kind signature with `f`. And that is exactly what we do: + +* In `promoteClassDec`, we use the `matchUpSAKWithDecl` function to take the + original class type variable binders and the class standalone kind signature + as input and produce a new set of class binders as output, where the new + binders have been annotated with kinds taken from the standalone kind + signature. We will call these new class type variable binders the /full/ + binders. + +* When generating a defunctionalization symbol for a promoted class method, we + always quantify the defunctionalization symbol's kind using an explicit + `forall`, where the `forall` looks like: + + forall . ... + + This ensures that the kind information from the full class binders is + propagated through to the defunctionalization symbol. (Note that we do not + make any guarantees about the /order/ of these type variables, however. See + Note [Promoted class methods and kind variable ordering].) + +If the parent class lacks a standalone kind signature, then we skip all of this +and simply quantify the the defunctionalization symbols' kind variables in a +left-to-right order. Again, the order of these kind variables in unspecified, so +we are free to choose a simpler implementation that makes our lives easier. -} -- returns (unpromoted method name, ALetDecRHS) pairs diff --git a/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs b/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs index c9a7abcf..33ce7281 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs @@ -773,77 +773,23 @@ equation, we could use a type synonym to define ConstSym2: type ConstSym2 :: a -> b -> a type ConstSym2 x y = Const x y -This approach has various downsides which make it impractical: +This approach has a downside which makes it impractical: type synonyms are +often not expanded in the output of GHCi's :kind! command. As issue #445 +chronicles, this can significantly impact the readability of even simple :kind! +queries. It can be the difference between this: -* Type synonyms are often not expanded in the output of GHCi's :kind! command. - As issue #445 chronicles, this can significantly impact the readability of - even simple :kind! queries. It can be the difference between this: + λ> :kind! Map IdSym0 '[1,2,3] + Map IdSym0 '[1,2,3] :: [Nat] + = 1 :@#@$$$ '[2, 3] - λ> :kind! Map IdSym0 '[1,2,3] - Map IdSym0 '[1,2,3] :: [Nat] - = 1 :@#@$$$ '[2, 3] +And this: - And this: + λ> :kind! Map IdSym0 '[1,2,3] + Map IdSym0 '[1,2,3] :: [Nat] + = '[1, 2, 3] - λ> :kind! Map IdSym0 '[1,2,3] - Map IdSym0 '[1,2,3] :: [Nat] - = '[1, 2, 3] - - Making fully saturated defunctionalization symbols like (:@#@$$$) type - families makes this issue moot, since :kind! always expands type families. -* There are a handful of corner cases where using type synonyms can actually - make fully saturated defunctionalization symbols fail to typecheck. - Here is one such corner case: - - $(promote [d| - class Applicative f where - pure :: a -> f a - ... - (*>) :: f a -> f b -> f b - |]) - - ==> - - class PApplicative f where - type Pure (x :: a) :: f a - type (*>) (x :: f a) (y :: f b) :: f b - - What would happen if we were to defunctionalize the promoted version of (*>)? - We'd end up with the following defunctionalization symbols: - - type (*>@#@$) :: f a ~> f b ~> f b - data (*>@#@$) f where ... - - type (*>@#@$$) :: f a -> f b ~> f b - data (*>@#@$$) x f where ... - - type (*>@#@$$$) :: f a -> f b -> f b - type (*>@#@$$$) x y = (*>) x y - - It turns out, however, that (*>@#@$$$) will not kind-check. Because (*>@#@$$$) - has a standalone kind signature, it is kind-generalized *before* kind-checking - the actual definition itself. Therefore, the full kind is: - - type (*>@#@$$$) :: forall {k} (f :: k -> Type) (a :: k) (b :: k). - f a -> f b -> f b - type (*>@#@$$$) x y = (*>) x y - - However, the kind of (*>) is - `forall (f :: Type -> Type) (a :: Type) (b :: Type). f a -> f b -> f b`. - This is not general enough for (*>@#@$$$), which expects kind-polymorphic `f`, - `a`, and `b`, leading to a kind error. You might think that we could somehow - infer this information, but note the quoted definition of Applicative (and - PApplicative, as a consequence) omits the kinds of `f`, `a`, and `b` entirely. - Unless we were to implement full-blown kind inference inside of Template - Haskell (which is a tall order), the kind `f a -> f b -> f b` is about as good - as we can get. - - Making (*>@#@$$$) a type family rather than a type synonym avoids this issue - since type family equations are allowed to match on kind arguments. In this - example, (*>@#@$$$) would have kind-polymorphic `f`, `a`, and `b` in its kind - signature, but its equation would implicitly equate `k` with `Type`. Note - that (*>@#@$) and (*>@#@$$), which are GADTs, also use a similar trick by - equating `k` with `Type` in their GADT constructors. +Making fully saturated defunctionalization symbols like (:@#@$$$) type families +makes this issue moot, since :kind! always expands type families. ----- -- Wrinkle: avoiding reduction stack overflows diff --git a/singletons-th/src/Data/Singletons/TH/Util.hs b/singletons-th/src/Data/Singletons/TH/Util.hs index 1e9a37ea..472a89b5 100644 --- a/singletons-th/src/Data/Singletons/TH/Util.hs +++ b/singletons-th/src/Data/Singletons/TH/Util.hs @@ -753,10 +753,6 @@ isHsLetter c = isLetter c || c == '_' -- signature for a singled @data@ declaration.) -- -- * They can be converted to 'DTyVarBndrVis'es using 'tvbForAllTyFlagsToVis'. --- (See, for example, 'promoteClassDec' in "Data.Singletons.TH.Promote", which --- does this to compute the \"full\" user-written binders for a promoted class --- declaration, as described in @Note [Promoted class methods and kind variable --- ordering] (Case 1: Case 1: Parent class with standalone kind signature).) -- -- Note that: -- From e16fecb45fa07733eb9c33c40778b6db38a73dba Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 16 Jun 2024 11:19:29 -0400 Subject: [PATCH 2/3] README.md: Document constraint limitations more thoroughly In particular, make note of the circumstances under which issues like #604. There is no way for `singletons-th` to generate code that avoids the problems in #604 in all cases, so we instead advise users to be wary when promoting code involving classes that are parameterized over higher-kinded type variables (e.g., `Alternative`). --- README.md | 83 ++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 82 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 926b0a65..92f0c7e3 100644 --- a/README.md +++ b/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 From e8cb2aa9732b2ec37df5ed20bbba92da13e8ea4f Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 16 Jun 2024 11:35:55 -0400 Subject: [PATCH 3/3] Give PAlternative (and friends) the correct kinds Previously, `singletons-th` would generalize the kinds of `PAlternative` and related classes (e.g., `PMonadPlus`), as well of the kinds of the defunctionalization symbols for various classes that are parameterized over a higher-kinded type variable. As described in the "Class constraints" section of the `README.md`, the recommended workaround for this issue is to give the classes in question explicit kinds, so this patch does just that by giving `Alternative`, `MonadPlus`, etc. standalone kind signatures. This causes the code in `singletons-base` to deviate a bit from the original code in the `base` library. I have written a new `Note [Using standalone kind signatures not present in the base library]` and cited it in all of the places where such a deviation occurs. Fixes #604. --- singletons-base/CHANGES.md | 20 +++++++++++++ .../src/Control/Monad/Fail/Singletons.hs | 5 ++++ .../src/Control/Monad/Singletons/Internal.hs | 29 +++++++++++++++++++ .../src/Control/Monad/Zip/Singletons.hs | 5 ++++ .../src/Data/Foldable/Singletons.hs | 3 ++ .../src/Data/Traversable/Singletons.hs | 4 +++ 6 files changed, 66 insertions(+) diff --git a/singletons-base/CHANGES.md b/singletons-base/CHANGES.md index d250f0a0..691111f3 100644 --- a/singletons-base/CHANGES.md +++ b/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] ---------------- diff --git a/singletons-base/src/Control/Monad/Fail/Singletons.hs b/singletons-base/src/Control/Monad/Fail/Singletons.hs index f2b99b03..6a3c1899 100644 --- a/singletons-base/src/Control/Monad/Fail/Singletons.hs +++ b/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 diff --git a/singletons-base/src/Control/Monad/Singletons/Internal.hs b/singletons-base/src/Control/Monad/Singletons/Internal.hs index 67508006..dd4f0dd3 100644 --- a/singletons-base/src/Control/Monad/Singletons/Internal.hs +++ b/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. +-} diff --git a/singletons-base/src/Control/Monad/Zip/Singletons.hs b/singletons-base/src/Control/Monad/Zip/Singletons.hs index c60f53f8..21e7b809 100644 --- a/singletons-base/src/Control/Monad/Zip/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Foldable/Singletons.hs b/singletons-base/src/Data/Foldable/Singletons.hs index 9b56db26..05c665bc 100644 --- a/singletons-base/src/Data/Foldable/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Traversable/Singletons.hs b/singletons-base/src/Data/Traversable/Singletons.hs index 49e829f7..6109600b 100644 --- a/singletons-base/src/Data/Traversable/Singletons.hs +++ b/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 #-}