Quantify class methods' kind variables in the correct order using TypeAbstractions
#596
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
In a subsequent commit, we will want to use these functions in D.S.TH.Promote, which was not possible when these functions lived in D.S.TH.Single.Data.
…a types `matchUpSigWithDecl` is useful for any sort of type-level declaration, not just data types. Moreover, in a subsequent commit we will actually use `matchUpSigWithDecl` on a class declaration instead of a data type declaration. This patch ensures that `matchUpSigWithDecl`'s comments and argument names aren't overfitted to data types.
There is no reason to specialize this to `DTyVarBndrSpec`, as this works for any `flag` type.
For now, this is simply a refactoring. We will make use of this more in a subsequent commit in which we use `matchUpSigWithDecl` to determine the binders of a promoted class declaration, in which case we will need to be able to tell invisible binders from visible ones.
…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
force-pushed
the
T589-class-method-type-variable-order
branch
from
33e351e
to
8705840
Compare
RyanGlScott
added a commit
that referenced
this pull request
Jun 16, 2024
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.
RyanGlScott
added a commit
that referenced
this pull request
Jun 18, 2024
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.
RyanGlScott
added a commit
that referenced
this pull request
Jun 30, 2024
When promoting a class or instance method, we generate a "helper" type family
definition that contains the actual implementation of the class or instance
method. Prior to this patch, it was possible that the kind of the helper type
family could be more polymorphic than desired. For instance, `singletons-th`
would promote this:
```hs
$(promote [d|
type MyApplicative :: (Type -> Type) -> Constraint
class Functor f => MyApplicative f where
ap :: f (a -> b) -> f a -> f b
rightSparrow :: f a -> f b -> f b
rightSparrow x y = ap (id <$ x) y
|])
```
To this:
```hs
type PMyApplicative :: (Type -> Type) -> Constraint
class PMyApplicative f where
type Ap (x :: f (a ~> b)) (y :: f a) :: f b
type RightSparrow (x :: f a) (y :: f b) :: f b
type RightSparrow x y = RightSparrowDefault x y
-- The helper type family
type RightSparrowDefault :: forall f a b. f a -> f b -> f b
type family RightSparrowDefault x y where
RightSparrowDefault x y = Ap (IdSym0 <$ x) y
```
Note that GHC would generalize the standalone kind signature of
`RightSparrowDefault` to:
```hs
type RightSparrowDefault :: forall {k} (f :: k -> Type) (a :: k) (b :: k).
f a -> f b -> f b
```
This is more general than intended, as we want `f` to be of kind `Type -> Type`
instead. After all, we said as much in the standalone kind signature for
`MyApplicative`! This excessive polymorphism doesn't actively cause problems in
today's GHC, but they will cause problems in a future version of GHC that
implements [GHC#23515](https://gitlab.haskell.org/ghc/ghc/-/issues/23515).
(See #601.)
This patch resolves the issue by propagating kind information from the class's
standalone kind signature (or, in the case of instance declarations, the
instance head) to the helper type family declarations. After this patch, we now
generate the following kind for `RightSparrowDefault` (as verified by the new
`T601a` test case):
```hs
type RightSparrowDefault :: forall (f :: Type -> Type) a b.
f a -> f b -> f b
```
This piggybacks on machinery that was added in #596 to do most of the heavy
lifting.
Resolves the "Overly polymorphic promoted class defaults" section of #601.
RyanGlScott
added a commit
that referenced
this pull request
Jun 30, 2024
When promoting a class or instance method, we generate a "helper" type family
definition that contains the actual implementation of the class or instance
method. Prior to this patch, it was possible that the kind of the helper type
family could be more polymorphic than desired. For instance, `singletons-th`
would promote this:
```hs
$(promote [d|
type MyApplicative :: (Type -> Type) -> Constraint
class Functor f => MyApplicative f where
ap :: f (a -> b) -> f a -> f b
rightSparrow :: f a -> f b -> f b
rightSparrow x y = ap (id <$ x) y
|])
```
To this:
```hs
type PMyApplicative :: (Type -> Type) -> Constraint
class PMyApplicative f where
type Ap (x :: f (a ~> b)) (y :: f a) :: f b
type RightSparrow (x :: f a) (y :: f b) :: f b
type RightSparrow x y = RightSparrowDefault x y
-- The helper type family
type RightSparrowDefault :: forall f a b. f a -> f b -> f b
type family RightSparrowDefault x y where
RightSparrowDefault x y = Ap (IdSym0 <$ x) y
```
Note that GHC would generalize the standalone kind signature of
`RightSparrowDefault` to:
```hs
type RightSparrowDefault :: forall {k} (f :: k -> Type) (a :: k) (b :: k).
f a -> f b -> f b
```
This is more general than intended, as we want `f` to be of kind `Type -> Type`
instead. After all, we said as much in the standalone kind signature for
`MyApplicative`! This excessive polymorphism doesn't actively cause problems in
today's GHC, but they will cause problems in a future version of GHC that
implements [GHC#23515](https://gitlab.haskell.org/ghc/ghc/-/issues/23515).
(See #601.)
This patch resolves the issue by propagating kind information from the class's
standalone kind signature (or, in the case of instance declarations, the
instance head) to the helper type family declarations. After this patch, we now
generate the following kind for `RightSparrowDefault` (as verified by the new
`T601a` test case):
```hs
type RightSparrowDefault :: forall (f :: Type -> Type) a b.
f a -> f b -> f b
```
This piggybacks on machinery that was added in #596 to do most of the heavy
lifting.
Resolves the "Overly polymorphic promoted class defaults" section of #601.
RyanGlScott
added a commit
that referenced
this pull request
Jul 1, 2024
When promoting a class or instance method, we generate a "helper" type family
definition that contains the actual implementation of the class or instance
method. Prior to this patch, it was possible that the kind of the helper type
family could be more polymorphic than desired. For instance, `singletons-th`
would promote this:
```hs
$(promote [d|
type MyApplicative :: (Type -> Type) -> Constraint
class Functor f => MyApplicative f where
ap :: f (a -> b) -> f a -> f b
rightSparrow :: f a -> f b -> f b
rightSparrow x y = ap (id <$ x) y
|])
```
To this:
```hs
type PMyApplicative :: (Type -> Type) -> Constraint
class PMyApplicative f where
type Ap (x :: f (a ~> b)) (y :: f a) :: f b
type RightSparrow (x :: f a) (y :: f b) :: f b
type RightSparrow x y = RightSparrowDefault x y
-- The helper type family
type RightSparrowDefault :: forall f a b. f a -> f b -> f b
type family RightSparrowDefault x y where
RightSparrowDefault x y = Ap (IdSym0 <$ x) y
```
Note that GHC would generalize the standalone kind signature of
`RightSparrowDefault` to:
```hs
type RightSparrowDefault :: forall {k} (f :: k -> Type) (a :: k) (b :: k).
f a -> f b -> f b
```
This is more general than intended, as we want `f` to be of kind `Type -> Type`
instead. After all, we said as much in the standalone kind signature for
`MyApplicative`! This excessive polymorphism doesn't actively cause problems in
today's GHC, but they will cause problems in a future version of GHC that
implements [GHC#23515](https://gitlab.haskell.org/ghc/ghc/-/issues/23515).
(See #601.)
This patch resolves the issue by propagating kind information from the class's
standalone kind signature (or, in the case of instance declarations, the
instance head) to the helper type family declarations. After this patch, we now
generate the following kind for `RightSparrowDefault` (as verified by the new
`T601a` test case):
```hs
type RightSparrowDefault :: forall (f :: Type -> Type) a b.
f a -> f b -> f b
```
This piggybacks on machinery that was added in #596 to do most of the heavy
lifting.
Resolves the "Overly polymorphic promoted class defaults" section of #601.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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
TypeAbstractionslanguage extension, which letssingletons-thpick 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 expandedNote [Promoted class methods and kind variable ordering]inD.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
singDataSAKfunction performs when producing a standalone kind signature for a singleddatadeclaration. As such, I factored out the common bits into a helper function calledmatchUpSAKWithDeclinD.S.TH.Util.Fixes #589.