Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support scoped type variables in class/instance declarations #591

Merged
merged 2 commits into from
Jun 6, 2024

Conversation

RyanGlScott
Copy link
Collaborator

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.

Previously, `singletons-th` would always attempt to generate instance
signatures for singled instance methods, even if the original instance code
lacks instance signatures. To do so, `singletons-th` will infer an instance
signature by reifying the type of the method (or, if that cannot be found, the
singled version of the method) and manually applying a substitution from class
variables to instance types. This process is quite involved, and what's more,
it doesn't work in all cases:

* As noted in #358, inferred instance signatures can sometimes be ill-kinded.
* In order to support singling examples like the ones from #581, we need type
  variables from class method defaults and instance methods to scope over their
  bodies. However, the approach that `singletons-th` used to reify the method
  type for the singled code will sometimes reify _different_ type variables
  than the ones used in the promoted code, leading to disaster.

This convention of inferring the instance signature dates all the way back to
commit
c9beec5,
and it's unclear why this choice was made. At the time of writing #358, I was
convinced that inferred instance signatures were necessary to support examples
like the one in
#358 (comment).
However, this example is only problematic due to the use of an explicit kind
annotation on a promoted `case` expression, and these explicit kind annotations
were removed in the fix for #547. As such, this convention no longer serves a
useful purpose.

This patch removes the instance signature inference code, greatly simplifying
the overall process of singling instance declarations.

Fixes #590.
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 RyanGlScott merged commit e854192 into master Jun 6, 2024
24 checks passed
@RyanGlScott RyanGlScott deleted the T581 branch June 6, 2024 11:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Out-of-scope type variable when using ScopedTypeVariables in class method RHS
1 participant