Skip to content

Commit

Permalink
Quantify class methods' kind variables in the correct order using Typ…
Browse files Browse the repository at this point in the history
…eAbstractions

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.
RyanGlScott committed Jun 6, 2024
1 parent d8c48c5 commit 0f4bfc3
Showing 13 changed files with 693 additions and 160 deletions.
65 changes: 50 additions & 15 deletions README.md
Original file line number Diff line number Diff line change
@@ -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
1 change: 1 addition & 0 deletions singletons-base/tests/SingletonsBaseTestSuite.hs
Original file line number Diff line number Diff line change
@@ -155,6 +155,7 @@ tests =
, compileAndDumpStdTest "T581"
, compileAndDumpStdTest "T585"
, compileAndDumpStdTest "TypeAbstractions"
, compileAndDumpStdTest "T589"
],
testCompileAndDumpGroup "Promote"
[ compileAndDumpStdTest "Constructors"
20 changes: 10 additions & 10 deletions singletons-base/tests/compile-and-dump/Singletons/T326.golden
Original file line number Diff line number Diff line change
@@ -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
(%<%%>) ::
Original file line number Diff line number Diff line change
@@ -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
10 changes: 5 additions & 5 deletions singletons-base/tests/compile-and-dump/Singletons/T412.golden
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
@@ -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
127 changes: 127 additions & 0 deletions singletons-base/tests/compile-and-dump/Singletons/T589.golden
Original file line number Diff line number Diff line change
@@ -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
59 changes: 59 additions & 0 deletions singletons-base/tests/compile-and-dump/Singletons/T589.hs
Original file line number Diff line number Diff line change
@@ -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
Loading

0 comments on commit 0f4bfc3

Please sign in to comment.