Implement partial support for promoting scoped type variables #573
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
Whenever we promote a function that closes over one or more local variables, we now use `noExactTyVars` to ensure that none of the local variables reuse unique `Name`s. This isn't strictly necessary right now, but this will be required in a future patch that will panic (triggering https://gitlab.haskell.org/ghc/ghc/-/issues/11812) unless `noExactTyVars` is used. While I was in the neighborhood, I took the opportunity to write `Note [Pitfalls of NameU/NameL]` with more context about why `noExactTyVars` is necessary in the first place, and I added references to the Note in all the places where we use it.
`singletons-th` can now promote a good number of uses of scoped type variables, save for the two exceptions now listed in the `singletons` `README`. This is accomplished by a combination of: 1. Bringing scoped type variables into scope on the left-hand sides of promoted type family equations through invisible `@` arguments when a function uses an outermost `forall` in its type signature (and does not close over any local variables). 2. Bringing scoped type variables into scope on the left-hand sides of promoted type family equations through explicit kind annotations on each of the type family's arguments when a function has an outermost `forall` in its type signature. 3. Closing over scoped type variables when lambda-lifting to ensure that the type variables are accessible when scoping over local definitions. See the new `Note [Scoped type variables]` in `Data.Singletons.TH.Promote.Monad` for more about how this is implemented. Fixes #433.
RyanGlScott
force-pushed
the
T433-take-two
branch
from
a7d1354 to
965f1ae
Compare
RyanGlScott
added a commit
that referenced
this pull request
May 19, 2024
Although #573 added some support for promoting/singling uses of scoped type variables, it did not properly support scoped type variables in class or instance declarations due to an oversight. This patch aims to correct that oversight. The key tricks to making this work are: * When promoting class or instance methods, we explicitly quantify the type variables in the "helper" type family so that we can bind them on the left-hand sides of the promoted type family equations. * In addition, we take care to only bring the _scoped_ type variables into scope over the right-hand sides of the promoted type family equations. See the new `Note [Scoped type variables and class methods]` in `Data.Singletons.TH.Promote.Monad` for the full details. Fixes #581.
RyanGlScott
added a commit
that referenced
this pull request
May 19, 2024
Although #573 added some support for promoting/singling uses of scoped type variables, it did not properly support scoped type variables in class or instance declarations due to an oversight. This patch aims to correct that oversight. The key tricks to making this work are: * When promoting class or instance methods, we explicitly quantify the type variables in the "helper" type family so that we can bind them on the left-hand sides of the promoted type family equations. * In addition, we take care to only bring the _scoped_ type variables into scope over the right-hand sides of the promoted type family equations. See the new `Note [Scoped type variables and class methods]` in `Data.Singletons.TH.Promote.Monad` for the full details. Fixes #581.
RyanGlScott
added a commit
that referenced
this pull request
May 19, 2024
Although #573 added some support for promoting/singling uses of scoped type variables, it did not properly support scoped type variables in class or instance declarations due to an oversight. This patch aims to correct that oversight. The key tricks to making this work are: * When promoting class or instance methods, we explicitly quantify the type variables in the "helper" type family so that we can bind them on the left-hand sides of the promoted type family equations. * In addition, we take care to only bring the _scoped_ type variables into scope over the right-hand sides of the promoted type family equations. See the new `Note [Scoped type variables and class methods]` in `Data.Singletons.TH.Promote.Monad` for the full details. Fixes #581.
RyanGlScott
added a commit
that referenced
this pull request
Jun 6, 2024
Although #573 added some support for promoting/singling uses of scoped type variables, it did not properly support scoped type variables in class or instance declarations due to an oversight. This patch aims to correct that oversight. The key tricks to making this work are: * When promoting class or instance methods, we explicitly quantify the type variables in the "helper" type family so that we can bind them on the left-hand sides of the promoted type family equations. * In addition, we take care to only bring the _scoped_ type variables into scope over the right-hand sides of the promoted type family equations. See the new `Note [Scoped type variables and class methods]` in `Data.Singletons.TH.Promote.Monad` for the full details. Fixes #581.
RyanGlScott
added a commit
that referenced
this pull request
Jun 6, 2024
Although #573 added some support for promoting/singling uses of scoped type variables, it did not properly support scoped type variables in class or instance declarations due to an oversight. This patch aims to correct that oversight. The key tricks to making this work are: * When promoting class or instance methods, we explicitly quantify the type variables in the "helper" type family so that we can bind them on the left-hand sides of the promoted type family equations. * In addition, we take care to only bring the _scoped_ type variables into scope over the right-hand sides of the promoted type family equations. See the new `Note [Scoped type variables and class methods]` in `Data.Singletons.TH.Promote.Monad` for the full details. Fixes #581.
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.
singletons-thcan now promote a good number of uses of scoped type variables, save for the two exceptions now listed in thesingletonsREADME. This is accomplished by a combination of:Bringing scoped type variables into scope on the left-hand sides of promoted type family equations through invisible
@arguments when a function uses an outermostforallin its type signature (and does not close over any local variables).Bringing scoped type variables into scope on the left-hand sides of promoted type family equations through explicit kind annotations on each of the type family's arguments when a function has an outermost
forallin its type signature.Closing over scoped type variables when lambda-lifting to ensure that the type variables are accessible when scoping over local definitions.
See the new
Note [Scoped type variables]inData.Singletons.TH.Promote.Monadfor more about how this is implemented.Fixes #433.