singletons icon indicating copy to clipboard operation
singletons copied to clipboard

Simplify singling of instance method types by not inferring instance signatures

Open RyanGlScott opened this issue 9 months ago • 0 comments

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:

  • 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 uses 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. (I don't have an example off-hand of this happening, as this relies on in-flight changes in a fix for #581, but this is a real problem.)

This convention of inferring the instance signature dates all the way back to commit https://github.com/goldfirere/singletons/commit/c9beec58a791af8c63152cdb54c758fd9fb04deb. At the time of writing #358, I was convinced that inferred instance signatures were necessary to support examples like the one in https://github.com/goldfirere/singletons/issues/358#issuecomment-416691475. 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 avatar May 12 '24 11:05 RyanGlScott