From 8705840062131fed52c9455ab6288d42998d31f3 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 30 May 2024 07:26:46 -0400 Subject: [PATCH] Quantify class methods' kind variables in the correct order using TypeAbstractions When promoting a class with a standalone kind signature, it is possible to ensure that the promoted methods' kind variables are quantified in the same order as the original method's type variables. This is now possible thanks to the `TypeAbstractions` language extension, which lets `singletons-th` pick the exact order of kind variables in the promoted methods' associated type families using `@` binders. For the full details of how this is accomplished, see the expanded `Note [Promoted class methods and kind variable ordering]` in `D.S.TH.Promote` (specifically, `Case 1: Parent class with standalone kind signature`). As it turns out, many of the steps we need to perform to achieve this are the same steps that the `singDataSAK` function performs when producing a standalone kind signature for a singled `data` declaration. As such, I factored out the common bits into a helper function called `matchUpSAKWithDecl` in `D.S.TH.Util`. Fixes #589. --- README.md | 65 +++- .../tests/SingletonsBaseTestSuite.hs | 1 + .../compile-and-dump/Singletons/T326.golden | 20 +- .../compile-and-dump/Singletons/T378b.golden | 2 +- .../compile-and-dump/Singletons/T412.golden | 10 +- .../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 | 41 ++- singletons-th/CHANGES.md | 4 + .../src/Data/Singletons/TH/Promote.hs | 278 +++++++++++++++--- .../src/Data/Singletons/TH/Single/Data.hs | 80 +---- singletons-th/src/Data/Singletons/TH/Util.hs | 164 ++++++++++- 13 files changed, 693 insertions(+), 160 deletions(-) create mode 100644 singletons-base/tests/compile-and-dump/Singletons/T589.golden create mode 100644 singletons-base/tests/compile-and-dump/Singletons/T589.hs diff --git a/README.md b/README.md index 4a2f6820..9c6d154c 100644 --- a/README.md +++ b/README.md @@ -1178,32 +1178,67 @@ for the following constructs: yourself! * Kind signatures of promoted class methods. - The order of type variables will often "just work" by happy coincidence, but - there are some situations where this does not happen. Consider the following - class: + 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: ```haskell - class C (b :: Type) where + 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`. This order is preserved when singling `m`, but *not* when - promoting `m`. This is because the `C` class is promoted as follows: + `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: ```haskell - class PC (b :: Type) where - type M (x :: a) (y :: b) :: a + -- No standalone kind signature + class C b where + m :: forall a. a -> b -> a ``` - Due to the way GHC kind-checks associated type families, the kind of `M` is - `forall a b. a -> b -> a`, which binds `b` *after* `a`. Moreover, the - `StandaloneKindSignatures` extension does not provide a way to explicitly - declare the full kind of an associated type family, so this limitation is - not easy to work around. + 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 + type M (x :: a) (y :: b) :: a + ``` - The defunctionalization symbols for `M` will also follow a similar - order of type variables: + 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: ```haskell type MSym0 :: forall a b. a ~> b ~> a diff --git a/singletons-base/tests/SingletonsBaseTestSuite.hs b/singletons-base/tests/SingletonsBaseTestSuite.hs index de0e95f2..e2d6082c 100644 --- a/singletons-base/tests/SingletonsBaseTestSuite.hs +++ b/singletons-base/tests/SingletonsBaseTestSuite.hs @@ -155,6 +155,7 @@ tests = , compileAndDumpStdTest "T581" , compileAndDumpStdTest "T585" , compileAndDumpStdTest "TypeAbstractions" + , compileAndDumpStdTest "T589" ], testCompileAndDumpGroup "Promote" [ compileAndDumpStdTest "Constructors" diff --git a/singletons-base/tests/compile-and-dump/Singletons/T326.golden b/singletons-base/tests/compile-and-dump/Singletons/T326.golden index 4a9a89e3..fb6f759a 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T326.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T326.golden @@ -1,7 +1,7 @@ Singletons/T326.hs:0:0:: Splicing declarations genPromotions [''C1] ======> - type (<%>@#@$) :: forall a. (~>) a ((~>) a a) + type (<%>@#@$) :: forall (a :: Type). (~>) a ((~>) a a) data (<%>@#@$) :: (~>) a ((~>) a a) where (:<%>@#@$###) :: SameKind (Apply (<%>@#@$) arg) ((<%>@#@$$) arg) => @@ -10,7 +10,7 @@ Singletons/T326.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings (<%>@#@$) where suppressUnusedWarnings = snd ((,) (:<%>@#@$###) ()) infixl 9 <%>@#@$ - type (<%>@#@$$) :: forall a. a -> (~>) a a + type (<%>@#@$$) :: forall (a :: Type). a -> (~>) a a data (<%>@#@$$) (a0123456789876543210 :: a) :: (~>) a a where (:<%>@#@$$###) :: SameKind (Apply ((<%>@#@$$) a0123456789876543210) arg) ((<%>@#@$$$) a0123456789876543210 arg) => @@ -19,18 +19,18 @@ Singletons/T326.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings ((<%>@#@$$) a0123456789876543210) where suppressUnusedWarnings = snd ((,) (:<%>@#@$$###) ()) infixl 9 <%>@#@$$ - type (<%>@#@$$$) :: forall a. a -> a -> a - type family (<%>@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where + type (<%>@#@$$$) :: forall (a :: Type). a -> a -> a + type family (<%>@#@$$$) @(a :: Type) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where (<%>@#@$$$) a0123456789876543210 a0123456789876543210 = (<%>) a0123456789876543210 a0123456789876543210 infixl 9 <%>@#@$$$ type PC1 :: Type -> Constraint class PC1 (a :: Type) where - type family (<%>) (arg :: a) (arg :: a) :: a + type family (<%>) @(a :: Type) (arg :: a) (arg :: a) :: a infixl 9 <%> Singletons/T326.hs:0:0:: Splicing declarations genSingletons [''C2] ======> - type (<%%>@#@$) :: forall a. (~>) a ((~>) a a) + type (<%%>@#@$) :: forall (a :: Type). (~>) a ((~>) a a) data (<%%>@#@$) :: (~>) a ((~>) a a) where (:<%%>@#@$###) :: SameKind (Apply (<%%>@#@$) arg) ((<%%>@#@$$) arg) => @@ -39,7 +39,7 @@ Singletons/T326.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings (<%%>@#@$) where suppressUnusedWarnings = snd ((,) (:<%%>@#@$###) ()) infixl 9 <%%>@#@$ - type (<%%>@#@$$) :: forall a. a -> (~>) a a + type (<%%>@#@$$) :: forall (a :: Type). a -> (~>) a a data (<%%>@#@$$) (a0123456789876543210 :: a) :: (~>) a a where (:<%%>@#@$$###) :: SameKind (Apply ((<%%>@#@$$) a0123456789876543210) arg) ((<%%>@#@$$$) a0123456789876543210 arg) => @@ -48,13 +48,13 @@ Singletons/T326.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings ((<%%>@#@$$) a0123456789876543210) where suppressUnusedWarnings = snd ((,) (:<%%>@#@$$###) ()) infixl 9 <%%>@#@$$ - type (<%%>@#@$$$) :: forall a. a -> a -> a - type family (<%%>@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where + type (<%%>@#@$$$) :: forall (a :: Type). a -> a -> a + type family (<%%>@#@$$$) @(a :: Type) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where (<%%>@#@$$$) a0123456789876543210 a0123456789876543210 = (<%%>) a0123456789876543210 a0123456789876543210 infixl 9 <%%>@#@$$$ type PC2 :: Type -> Constraint class PC2 (a :: Type) where - type family (<%%>) (arg :: a) (arg :: a) :: a + type family (<%%>) @(a :: Type) (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 81b3db76..cc31d5ae 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 x y + class PC @b @a (x :: a) (y :: b) 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 b757f4e1..dc1e31a3 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T412.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T412.golden @@ -201,7 +201,7 @@ Singletons/T412.hs:(0,0)-(0,0): Splicing declarations Singletons/T412.hs:0:0:: Splicing declarations genSingletons [''C2, ''T2a, ''T2b, ''D2] ======> - type M2Sym0 :: forall a b. (~>) a ((~>) b Bool) + type M2Sym0 :: forall (a :: Type) (b :: Type). (~>) a ((~>) b Bool) data M2Sym0 :: (~>) a ((~>) b Bool) where M2Sym0KindInference :: SameKind (Apply M2Sym0 arg) (M2Sym1 arg) => @@ -210,7 +210,7 @@ Singletons/T412.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings M2Sym0 where suppressUnusedWarnings = snd ((,) M2Sym0KindInference ()) infix 6 `M2Sym0` - type M2Sym1 :: forall a b. a -> (~>) b Bool + type M2Sym1 :: forall (a :: Type) (b :: Type). a -> (~>) b Bool data M2Sym1 (a0123456789876543210 :: a) :: (~>) b Bool where M2Sym1KindInference :: SameKind (Apply (M2Sym1 a0123456789876543210) arg) (M2Sym2 a0123456789876543210 arg) => @@ -219,13 +219,13 @@ Singletons/T412.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings (M2Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) M2Sym1KindInference ()) infix 6 `M2Sym1` - type M2Sym2 :: forall a b. a -> b -> Bool - type family M2Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Bool where + type M2Sym2 :: forall (a :: Type) (b :: Type). a -> b -> Bool + type family M2Sym2 @(a :: Type) @(b :: Type) (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Bool where M2Sym2 a0123456789876543210 a0123456789876543210 = M2 a0123456789876543210 a0123456789876543210 infix 6 `M2Sym2` type PC2 :: Type -> Type -> Constraint class PC2 (a :: Type) (b :: Type) where - type family M2 (arg :: a) (arg :: b) :: Bool + type family M2 @(a :: Type) @(b :: Type) (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 a317c607..0d97f536 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 + class PC3 (a :: Bool) 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 new file mode 100644 index 00000000..1cea4900 --- /dev/null +++ b/singletons-base/tests/compile-and-dump/Singletons/T589.golden @@ -0,0 +1,127 @@ +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 new file mode 100644 index 00000000..6a9278b8 --- /dev/null +++ b/singletons-base/tests/compile-and-dump/Singletons/T589.hs @@ -0,0 +1,59 @@ +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 6e390106..a52c42dd 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden @@ -168,7 +168,10 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations type MkD4Sym1 :: forall a. a -> D4 @a type family MkD4Sym1 @a (a0123456789876543210 :: a) :: D4 @a where MkD4Sym1 a0123456789876543210 = MkD4 a0123456789876543210 - type Meth1Sym0 :: forall a b. (~>) (Proxy a) (Proxy b) + type Meth1Sym0 :: forall j + k + (a :: j) + (b :: k). (~>) (Proxy a) (Proxy b) data Meth1Sym0 :: (~>) (Proxy a) (Proxy b) where Meth1Sym0KindInference :: SameKind (Apply Meth1Sym0 arg) (Meth1Sym1 arg) => @@ -176,13 +179,16 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations type instance Apply Meth1Sym0 a0123456789876543210 = Meth1 a0123456789876543210 instance SuppressUnusedWarnings Meth1Sym0 where suppressUnusedWarnings = snd ((,) Meth1Sym0KindInference ()) - type Meth1Sym1 :: forall a b. Proxy a -> Proxy b - type family Meth1Sym1 @a @b (a0123456789876543210 :: Proxy a) :: Proxy b where + type Meth1Sym1 :: forall j k (a :: j) (b :: k). Proxy a -> Proxy b + type family Meth1Sym1 @j @k @(a :: j) @(b :: k) (a0123456789876543210 :: Proxy a) :: Proxy b where Meth1Sym1 a0123456789876543210 = Meth1 a0123456789876543210 type PC1 :: forall j k. j -> k -> Constraint class PC1 @j @k (a :: j) (b :: k) where - type family Meth1 (arg :: Proxy a) :: Proxy b - type Meth2Sym0 :: forall a b. (~>) (Proxy a) (Proxy b) + type family Meth1 @j @k @(a :: j) @(b :: k) (arg :: Proxy a) :: Proxy b + type Meth2Sym0 :: forall x + y + (a :: x) + (b :: y). (~>) (Proxy a) (Proxy b) data Meth2Sym0 :: (~>) (Proxy a) (Proxy b) where Meth2Sym0KindInference :: SameKind (Apply Meth2Sym0 arg) (Meth2Sym1 arg) => @@ -190,13 +196,16 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations type instance Apply Meth2Sym0 a0123456789876543210 = Meth2 a0123456789876543210 instance SuppressUnusedWarnings Meth2Sym0 where suppressUnusedWarnings = snd ((,) Meth2Sym0KindInference ()) - type Meth2Sym1 :: forall a b. Proxy a -> Proxy b - type family Meth2Sym1 @a @b (a0123456789876543210 :: Proxy a) :: Proxy b where + type Meth2Sym1 :: forall x y (a :: x) (b :: y). Proxy a -> Proxy b + type family Meth2Sym1 @x @y @(a :: x) @(b :: y) (a0123456789876543210 :: Proxy a) :: Proxy b where Meth2Sym1 a0123456789876543210 = Meth2 a0123456789876543210 type PC2 :: forall j k. j -> k -> Constraint class PC2 @x @y (a :: x) (b :: y) where - type family Meth2 (arg :: Proxy a) :: Proxy b - type Meth3Sym0 :: forall a b. (~>) (Proxy a) (Proxy b) + type family Meth2 @x @y @(a :: x) @(b :: y) (arg :: Proxy a) :: Proxy b + type Meth3Sym0 :: forall j + (a :: j) + k + (b :: k). (~>) (Proxy a) (Proxy b) data Meth3Sym0 :: (~>) (Proxy a) (Proxy b) where Meth3Sym0KindInference :: SameKind (Apply Meth3Sym0 arg) (Meth3Sym1 arg) => @@ -204,18 +213,18 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations type instance Apply Meth3Sym0 a0123456789876543210 = Meth3 a0123456789876543210 instance SuppressUnusedWarnings Meth3Sym0 where suppressUnusedWarnings = snd ((,) Meth3Sym0KindInference ()) - type Meth3Sym1 :: forall a b. Proxy a -> Proxy b - type family Meth3Sym1 @a @b (a0123456789876543210 :: Proxy a) :: Proxy b where + type Meth3Sym1 :: forall j (a :: j) k (b :: k). Proxy a -> Proxy b + type family Meth3Sym1 @j @(a :: j) @k @(b :: k) (a0123456789876543210 :: Proxy a) :: Proxy b where 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 (arg :: Proxy a) :: Proxy b - type Meth4Sym0 :: forall a. a - type family Meth4Sym0 @a :: a where + type family Meth3 @j @(a :: j) @k @(b :: k) (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 where - type family Meth4 :: a + class PC4 @(a :: Type) where + type family Meth4 @(a :: Type) :: 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 29cb7000..386e415a 100644 --- a/singletons-th/CHANGES.md +++ b/singletons-th/CHANGES.md @@ -5,6 +5,10 @@ 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 c25659dd..f1f603c5 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote.hs @@ -36,7 +36,8 @@ import Control.Arrow (second) import Control.Monad import Control.Monad.Trans.Maybe import Control.Monad.Writer -import Data.List (nub) +import Data.Function (on) +import Data.List (deleteFirstsBy, nub) import qualified Data.Map.Strict as Map import Data.Map.Strict ( Map ) import Data.Maybe @@ -257,7 +258,7 @@ promoteDataDec (DataDecl _ _ _ ctors) = do promoteClassDec :: UClassDecl -> PrM AClassDecl promoteClassDec decl@(ClassDecl { cd_name = cls_name - , cd_tvbs = cls_tvbs + , cd_tvbs = orig_cls_tvbs , cd_fds = fundeps , cd_atfs = atfs , cd_lde = lde@LetDecEnv @@ -270,19 +271,34 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name meth_names = map fst meth_sigs_list defaults_list = OMap.assocs defaults defaults_names = map fst defaults_list - cls_tvb_names = map extractTvbName cls_tvbs + cls_tvb_names = map extractTvbName orig_cls_tvbs mb_cls_sak <- dsReifyType cls_name - sig_decs <- mapM (uncurry promote_sig) meth_sigs_list + + -- 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). + 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) <- mapAndUnzip3M (promoteMethod DefaultMethods meth_sigs cls_tvb_names) defaults_list - defunAssociatedTypeFamilies cls_tvbs atfs + defunAssociatedTypeFamilies orig_cls_tvbs atfs infix_decls' <- mapMaybeM (uncurry (promoteInfixDecl Nothing)) $ OMap.assocs infix_decls 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 cls_tvbs fundeps + let pro_cls_dec = DClassD [] pClsName pro_cls_tvbs_vis 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 @@ -291,57 +307,245 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name return (decl { cd_lde = lde { lde_defns = OMap.fromList defaults_list' , lde_proms = OMap.fromList proms } }) where - promote_sig :: Name -> DType -> PrM DDec - promote_sig name ty = do + -- Promote a class method's type signature to an associated type family. + promote_sig :: + 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'. + -> Name + -- ^ The class method's name. + -> DType + -- ^ The class method's type. + -> PrM DDec + -- ^ The associated type family for the promoted class method. + promote_sig mb_full_cls_tvbs name meth_ty = do opts <- getOptions let proName = promotedTopLevelValueName opts name - -- When computing the kind to use for the defunctionalization symbols, - -- /don't/ use the type variable binders from the method's type... - (_, argKs, resK) <- promoteUnraveled ty - args <- mapM (const $ qNewName "arg") argKs - let proTvbs = zipWith (`DKindedTV` BndrReq) args argKs - -- ...instead, 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] - meth_sak_tvbs = changeDTVFlags SpecifiedSpec $ - toposortTyVarsOf $ argKs ++ [resK] - meth_sak = ravelVanillaDType meth_sak_tvbs [] argKs resK + (meth_expl_tvbs, 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. + 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). + 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 + -- 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). + Nothing -> + changeDTVFlags SpecifiedSpec $ + toposortTyVarsOf $ meth_arg_kis ++ [meth_res_ki] + 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 - proTvbs - (DKindSig resK) + all_meth_tvbs + (DKindSig meth_res_ki) Nothing) {- 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 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: +promoting type signatures, but there is a corner case where this is difficult: +class methods. + +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 +----- - class C (b :: Type) where +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 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: - class PC (b :: Type) where + -- No standalone kind signature + class PC b where type M (x :: a) (y :: b) :: a -Due to the way GHC kind-checks associated type families, the kind of `M` is -`forall a b. a -> b -> a`, which binds `b` *after* `a`. Moreover, the -`StandaloneKindSignatures` extension does not provide a way to explicitly -declare the full kind of an associated type family, so this limitation is -not easy to work around. - -The defunctionalization symbols for `M` will also follow a similar -order of type variables: +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: type MSym0 :: forall a b. a ~> b ~> a type MSym1 :: forall a b. a -> b ~> a @@ -349,7 +553,7 @@ order of type variables: There is one potential hack we could use to rectify this: type FlipConst x y = y - class PC (b :: Type) where + class PC b where type M (x :: FlipConst '(b, a) a) (y :: b) :: a Using `FlipConst` would cause `b` to be mentioned before `a`, which would give diff --git a/singletons-th/src/Data/Singletons/TH/Single/Data.hs b/singletons-th/src/Data/Singletons/TH/Single/Data.hs index 27932aa5..7817dc85 100644 --- a/singletons-th/src/Data/Singletons/TH/Single/Data.hs +++ b/singletons-th/src/Data/Singletons/TH/Single/Data.hs @@ -13,9 +13,7 @@ module Data.Singletons.TH.Single.Data import Language.Haskell.TH.Desugar as Desugar import Language.Haskell.TH.Syntax -import qualified Data.Map.Strict as Map import Data.Maybe -import Data.Traversable (mapAccumL) import Data.Singletons.TH.Names import Data.Singletons.TH.Options import Data.Singletons.TH.Promote.Type @@ -269,26 +267,12 @@ singCtor dataName (DCon con_tvbs cxt name fields rty) -- type SD :: forall j l (a :: l) (b :: j). D @j @l (a :: l) b -> Type -- @ -- --- Note that: +-- Note that the order of the invisible quantifiers is preserved, so both +-- @D \@Bool \@Ordering@ and @SD \@Bool \@Ordering@ will work the way you would +-- expect it to. -- --- * This function has a precondition that the length of @data_bndrs@ must --- always be equal to the number of visible quantifiers (i.e., the number of --- function arrows plus the number of visible @forall@–bound variables) in --- @sak@. @singletons-th@ maintains this invariant when constructing a --- 'DataDecl' (see the 'buildDataDTvbs' function). --- --- * The order of the invisible quantifiers is preserved, so both --- @D \@Bool \@Ordering@ and @SD \@Bool \@Ordering@ will work the way you would --- expect it to. --- --- * Whenever possible, this function reuses type variable names from the data --- type's user-written binders. This is why the standalone kind signature uses --- @forall j l@ instead of @forall j k@, since the @(a :: l)@ binder uses @l@ --- instead of @k@. We could have just as well chose the other way around, but --- we chose to pick variable names from the data type binders since they scope --- over other parts of the data type declaration (e.g., in @deriving@ --- clauses), so keeping these names avoids having to perform some --- alpha-renaming. +-- See also the comments on the 'matchUpSAKWithDecl' function (in +-- "Data.Singletons.TH.Util"), which also apply here. singDataSAK :: MonadFail q => DKind @@ -300,58 +284,10 @@ singDataSAK :: -> q DKind -- ^ The standalone kind signature for the singled data type singDataSAK data_sak data_bndrs data_k = do - -- (1) First, explicitly quantify any free kind variables in `data_sak` using - -- an invisible @forall@. This is done to ensure that precondition (2) in - -- `matchUpSigWithDecl` is upheld. (See the Haddocks for that function). - let data_sak_free_tvbs = - changeDTVFlags SpecifiedSpec $ toposortTyVarsOf [data_sak] - data_sak' = DForallT (DForallInvis data_sak_free_tvbs) data_sak - - -- (2) Next, compute type variable binders for the singled data type's - -- standalone kind signature using `matchUpSigWithDecl`. Note that these can - -- be biased towards type variable names mention in `data_sak` over names - -- mentioned in `data_bndrs`, but we will fix that up in the next step. - let (data_sak_args, _) = unravelDType data_sak' - sing_sak_tvbs <- matchUpSigWithDecl data_sak_args data_bndrs - - -- (3) Swizzle the type variable names so that names in `data_bndrs` are - -- preferred over names in `data_sak`. - -- - -- This is heavily inspired by similar code in GHC: - -- https://gitlab.haskell.org/ghc/ghc/-/blob/cec903899234bf9e25ea404477ba846ac1e963bb/compiler/GHC/Tc/Gen/HsType.hs#L2607-2616 - let invis_data_sak_args = filterInvisTvbArgs data_sak_args - invis_data_sak_arg_nms = map extractTvbName invis_data_sak_args - - invis_data_bndrs = toposortKindVarsOfTvbs data_bndrs - invis_data_bndr_nms = map extractTvbName invis_data_bndrs - - swizzle_env = - Map.fromList $ zip invis_data_sak_arg_nms invis_data_bndr_nms - (_, swizzled_sing_sak_tvbs) = - mapAccumL (swizzleTvb swizzle_env) Map.empty sing_sak_tvbs - swizzled_sing_sak_tvbs' = - map (fmap mk_data_sak_spec) swizzled_sing_sak_tvbs - - -- (4) Finally, construct the kind of the singled data type. - pure $ DForallT (DForallInvis swizzled_sing_sak_tvbs') + sing_sak_tvbs <- matchUpSAKWithDecl data_sak data_bndrs + let sing_sak_tvbs' = tvbForAllTyFlagsToSpecs sing_sak_tvbs + pure $ DForallT (DForallInvis sing_sak_tvbs') $ DArrowT `DAppT` data_k `DAppT` DConT typeKindName - where - -- Convert a ForAllTyFlag value to a Specificity value, i.e., a binder - -- suitable for use in an invisible `forall`. We convert Required values - -- to SpecifiedSpec values because all of the binders in the `forall` are - -- invisible. For instance, we would single this data type: - -- - -- type T :: forall k -> k -> Type - -- data T k (a :: k) where ... - -- - -- Like so: - -- - -- -- Note: the `k` is invisible, not visible - -- type ST :: forall k (a :: k). T k a -> Type - -- data ST z where ... - mk_data_sak_spec :: ForAllTyFlag -> Specificity - mk_data_sak_spec (Invisible spec) = spec - mk_data_sak_spec Required = SpecifiedSpec {- Note [singletons-th and record selectors] diff --git a/singletons-th/src/Data/Singletons/TH/Util.hs b/singletons-th/src/Data/Singletons/TH/Util.hs index 6bbf8504..1e9a37ea 100644 --- a/singletons-th/src/Data/Singletons/TH/Util.hs +++ b/singletons-th/src/Data/Singletons/TH/Util.hs @@ -267,6 +267,14 @@ maybeSigT ty (Just ki) = ty `DSigT` ki -- @ -- -- Note that note of @b@, @d@, or @e@ appear in the list. +-- +-- See also 'tvbForAllTyFlagsToBndrVis', which takes a list of @'DTyVarBndr' +-- 'ForAllTyFlag'@ as arguments instead of a list of 'DTyVarBndrSpec's. Note +-- that @'tvbSpecsToBndrVis' . 'tvbForAllTyFlagsToSpecs'@ is /not/ the same +-- thing as 'tvbForAllTyFlagsToBndrVis'. This is because 'tvbSpecsToBndrVis' +-- only produces 'BndrInvis' binders as output, whereas +-- 'tvbForAllTyFlagsToBndrVis' can produce both 'BndrReq' and 'BndrInvis' +-- binders. tvbSpecsToBndrVis :: [DTyVarBndrSpec] -> [DTyVarBndrVis] tvbSpecsToBndrVis = mapMaybe (traverse specificityToBndrVis) where @@ -720,6 +728,96 @@ mapAndUnzip3M f (x:xs) = do isHsLetter :: Char -> Bool isHsLetter c = isLetter c || c == '_' +-- @'matchUpSAKWithDecl' decl_sak decl_bndrs@ produces @'DTyVarBndr' +-- 'ForAllTyFlag'@s for a declaration, using the original declaration's +-- standalone kind signature (@decl_sak@) and its user-written binders +-- (@decl_bndrs@) as a template. For this example: +-- +-- @ +-- type D :: forall j k. k -> j -> Type +-- data D \@j \@l (a :: l) b = ... +-- @ +-- +-- We would produce the following @'DTyVarBndr' 'ForAllTyFlag'@s: +-- +-- @ +-- \@j \@l (a :: l) (b :: j) +-- @ +-- +-- From here, these @'DTyVarBndr' 'ForAllTyFlag'@s can be converted into other +-- forms of 'DTyVarBndr's: +-- +-- * They can be converted to 'DTyVarBndrSpec's using 'tvbForAllTyFlagsToSpecs'. +-- (See, for example, 'singDataSAK' in "Data.Singletons.TH.Single.Data", which +-- does this to construct the invisible @forall@s in the standalone kind +-- 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: +-- +-- * This function has a precondition that the length of @decl_bndrs@ must +-- always be equal to the number of visible quantifiers (i.e., the number of +-- function arrows plus the number of visible @forall@–bound variables) in +-- @decl_sak@. +-- +-- * Whenever possible, this function reuses type variable names from the +-- declaration's user-written binders. This is why the @'DTyVarBndr' +-- 'ForAllTyFlag'@ use @\@j \@l@ instead of @\@j \@k@, since the @(a :: l)@ +-- binder uses @l@ instead of @k@. We could have just as well chose the other +-- way around, but we chose to pick variable names from the user-written +-- binders since they scope over other parts of the declaration. (For example, +-- the user-written binders of a @data@ declaration scope over the type +-- variables mentioned in a @deriving@ clause.) As such, keeping these names +-- avoids having to perform some alpha-renaming. +-- +-- This function's implementation was heavily inspired by parts of GHC's +-- kcCheckDeclHeader_sig function: +-- https://gitlab.haskell.org/ghc/ghc/-/blob/1464a2a8de082f66ae250d63ab9d94dbe2ef8620/compiler/GHC/Tc/Gen/HsType.hs#L2524-2643 +matchUpSAKWithDecl :: + forall q. + MonadFail q + => DKind + -- ^ The declaration's standalone kind signature + -> [DTyVarBndrVis] + -- ^ The user-written binders in the declaration + -> q [DTyVarBndr ForAllTyFlag] +matchUpSAKWithDecl decl_sak decl_bndrs = do + -- (1) First, explicitly quantify any free kind variables in `decl_sak` using + -- an invisible @forall@. This is done to ensure that precondition (2) in + -- `matchUpSigWithDecl` is upheld. (See the Haddocks for that function). + let decl_sak_free_tvbs = + changeDTVFlags SpecifiedSpec $ toposortTyVarsOf [decl_sak] + decl_sak' = DForallT (DForallInvis decl_sak_free_tvbs) decl_sak + + -- (2) Next, compute type variable binders using `matchUpSigWithDecl`. Note + -- that these can be biased towards type variable names mention in `decl_sak` + -- over names mentioned in `decl_bndrs`, but we will fix that up in the next + -- step. + let (decl_sak_args, _) = unravelDType decl_sak' + sing_sak_tvbs <- matchUpSigWithDecl decl_sak_args decl_bndrs + + -- (3) Finally, swizzle the type variable names so that names in `decl_bndrs` + -- are preferred over names in `decl_sak`. + -- + -- This is heavily inspired by similar code in GHC: + -- https://gitlab.haskell.org/ghc/ghc/-/blob/cec903899234bf9e25ea404477ba846ac1e963bb/compiler/GHC/Tc/Gen/HsType.hs#L2607-2616 + let invis_decl_sak_args = filterInvisTvbArgs decl_sak_args + invis_decl_sak_arg_nms = map extractTvbName invis_decl_sak_args + + invis_decl_bndrs = toposortKindVarsOfTvbs decl_bndrs + invis_decl_bndr_nms = map extractTvbName invis_decl_bndrs + + swizzle_env = + Map.fromList $ zip invis_decl_sak_arg_nms invis_decl_bndr_nms + (_, swizzled_sing_sak_tvbs) = + mapAccumL (swizzleTvb swizzle_env) Map.empty sing_sak_tvbs + pure swizzled_sing_sak_tvbs + -- Match the quantifiers in a type-level declaration's standalone kind signature -- with the user-written binders in the declaration. This function assumes the -- following preconditions: @@ -896,7 +994,67 @@ swizzleTvb swizzle_env subst tvb = data ForAllTyFlag = Invisible !Specificity -- ^ If the 'Specificity' value is 'SpecifiedSpec', then the binder is - -- permitted by request. If the 'Specificity' value is 'InferredSpec', then - -- the binder is prohibited from appearing in source Haskell. + -- permitted by request (e.g., @\@a@). If the 'Specificity' value is + -- 'InferredSpec', then the binder is prohibited from appearing in source + -- Haskell (e.g., @\@{a}@). | Required - -- ^ The binder is required to appear in source Haskell + -- ^ The binder is required to appear in source Haskell (e.g., @a@). + +-- | Convert a list of @'DTyVarBndr' 'ForAllTyFlag'@s to a list of +-- 'DTyVarBndrSpec's, which is suitable for use in an invisible @forall@. +-- Specifically: +-- +-- * Variable binders that use @'Invisible' spec@ are converted to @spec@. +-- +-- * Variable binders that are 'Required' are converted to 'SpecifiedSpec', +-- as all of the 'DTyVarBndrSpec's are invisible. As an example of how this +-- is used, consider what would happen when singling this data type: +-- +-- @ +-- type T :: forall k -> k -> Type +-- data T k (a :: k) where ... +-- @ +-- +-- Here, the @k@ binder is 'Required'. When we produce the standalone kind +-- signature for the singled data type, we use 'tvbForAllTyFlagsToSpecs' to +-- produce the type variable binders in the outermost @forall@: +-- +-- @ +-- type ST :: forall k (a :: k). T k a -> Type +-- data ST z where ... +-- @ +-- +-- Note that the @k@ is bound visibily (i.e., using 'SpecifiedSpec') in the +-- outermost, invisible @forall@. +tvbForAllTyFlagsToSpecs :: [DTyVarBndr ForAllTyFlag] -> [DTyVarBndrSpec] +tvbForAllTyFlagsToSpecs = map (fmap to_spec) + where + to_spec :: ForAllTyFlag -> Specificity + to_spec (Invisible spec) = spec + to_spec Required = SpecifiedSpec + +-- | Convert a list of @'DTyVarBndr' 'ForAllTyFlag'@s to a list of +-- 'DTyVarBndrVis'es, which is suitable for use in a type-level declaration +-- (e.g., the @var_1 ... var_n@ in @class C var_1 ... var_n@). Specifically: +-- +-- * Variable binders that use @'Invisible' 'InferredSpec'@ are dropped +-- entirely. Such binders cannot be represented in source Haskell. +-- +-- * Variable binders that use @'Invisible' 'SpecifiedSpec'@ are converted to +-- 'BndrInvis'. +-- +-- * Variable binders that are 'Required' are converted to 'BndrReq'. +-- +-- See also 'tvbSpecsToBndrVis', which takes a list of 'DTyVarBndrSpec's as +-- arguments instead of a list of @'DTyVarBndr' 'ForAllTyFlag'@s. Note that +-- @'tvbSpecsToBndrVis' . 'tvbForAllTyFlagsToSpecs'@ is /not/ the same thing as +-- 'tvbForAllTyFlagsToBndrVis'. This is because 'tvbSpecsToBndrVis' only +-- produces 'BndrInvis' binders as output, whereas 'tvbForAllTyFlagsToBndrVis' +-- can produce both 'BndrReq' and 'BndrInvis' binders. +tvbForAllTyFlagsToBndrVis :: [DTyVarBndr ForAllTyFlag] -> [DTyVarBndrVis] +tvbForAllTyFlagsToBndrVis = catMaybes . map (traverse to_spec_maybe) + where + to_spec_maybe :: ForAllTyFlag -> Maybe BndrVis + to_spec_maybe (Invisible InferredSpec) = Nothing + to_spec_maybe (Invisible SpecifiedSpec) = Just BndrInvis + to_spec_maybe Required = Just BndrReq