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

Simplify singling of instance method types by not inferring instance signatures #590

Open
RyanGlScott opened this issue May 12, 2024 · 0 comments

Comments

@RyanGlScott
Copy link
Collaborator

Currently, singletons-th always attempts to generate instance signatures for singled instance methods, even if the original instance code lacks instance signatures. For instance, singletons-th will take this code:

instance Eq Foo where
  MkFoo == MkFoo = True

And single it to:

instance SEq Foo where
  (%==) :: forall (x :: Foo) (y :: Foo).
           Sing x -> Sing y -> Sing (Foo x y)
  SMkFoo %== SMkFoo = STrue

Note that the original instance lacks an instance signature, but the singled instance includes one anway. In order to infer the instance signature for the singled instance, singletons-th will reify the type of the method (or, if that cannot be found, the singled version of the method) and manually apply a substitution from class variables to instance types. See this code.

This instance signature inference is quite involved, and what's more, it doesn't work in all cases:

This convention of inferring the instance signature dates all the way back to commit c9beec5. 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, that example was 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, I claim that instance signature inference no longer serves a useful purpose.

I propose that we remove the instance signature inference code, which would greatly simplify the overall process of singling instance declarations. (We can still single instance signatures if the user provides them, but there's no real benefit singletons-th inferring them if the user leaves them out.)

RyanGlScott added a commit that referenced this issue May 19, 2024
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant