Re: Rewriting plugins: request for feedback

[Sam Derbyshire]

Hi everyone,

I've uploaded the new type-checking plugin API to Hackage:
https://hackage.haskell.org/package/ghc-tcplugin-api.

Let me know how you get on. It should be much easier to iterate on the
design and add new functionality, now that the API isn't tied to GHC.

Thanks,

Sam
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Rewriting plugins: request for feedback

[Sam Derbyshire]

>
> FYI the Inria paper link in the readme seems to not be correct?
>

The HAL-Inria server seems to be down at the moment.
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Rewriting plugins: request for feedback

[Carter Schonwald]

This sounds very cool!

FYI the Inria paper link in the readme seems to not be correct?

On Fri, Jul 9, 2021 at 6:56 PM Sam Derbyshire 
wrote:

> Hi all,
>
> I have now written a much more substantial type-checking plugin, which I
> used to typecheck an intrinsically typed implementation of System F. I've
> added the example to the repository (
> https://github.com/sheaf/ghc-tcplugin-api), see the readme.
>
> This uncovered several bugs in the implementation of the aforementioned
> compatibility layer for GHC 9.0 and 9.2, which have all been fixed. I can
> now in good conscience recommend that type-checking plugin authors try it
> out for themselves!
> There are slight inconsistencies in behaviour around emitting additional
> constraints when rewriting a type-family application (which I hope to iron
> out soon), but I expect the impact of this to be very minimal. Other than
> that, you can expect feature and behaviour parity with the native
> implementation.
>
> Please let me know how you get on, and which pain points you would like to
> see addressed. My current ideas for improvement are as follows:
>
>   - Functionality that would perform all the name resolution necessary in
> the plugin initialisation. The user would provide a record of the types to
> look up (a TyCon named ... in module ..., a Class named ... in module ...),
> and the library would look up everything. This would be quite
> straightforward with a library such as barbies, but I don't necessarily
> want to impose that cognitive overhead on users who are not familiar with
> it.
>   - An interface for handling type family rewritings that provides a type
> system that kind checks everything. For instance, instead of manually
> calling splitTyConAppMaybe, we could feasibly instead use a pattern with
> existential variables (matching on this pattern would introduce the kinds),
> and then use a smart constructor instead of mkTyConApp (which would
> kind-check the application). I certainly would have appreciated something
> like this when writing my System F plugin, as handling all the kinds
> explicitly was rather tiresome and error prone.
>   - Functionality for recognising that a type has a certain form, making
> use of Givens. For example, it can be quite annoying to find out whether a
> given type is a type family application, as one needs to look through the
> Givens to go through levels of indirection. For instance, one might come
> across a variable "x" (ostensibly not a type family application), but have
> Givens [G] y ~ x, [G] F a ~ y. (This happens often with flattening skolems.)
>
> Please let me know if you have any other ideas, or suggestions on how to
> tackle the above. Thanks.
>
> Best,
>
> Sam
>
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Rewriting plugins: request for feedback

[Sam Derbyshire]

Hi all,

I have now written a much more substantial type-checking plugin, which I
used to typecheck an intrinsically typed implementation of System F. I've
added the example to the repository (
https://github.com/sheaf/ghc-tcplugin-api), see the readme.

This uncovered several bugs in the implementation of the aforementioned
compatibility layer for GHC 9.0 and 9.2, which have all been fixed. I can
now in good conscience recommend that type-checking plugin authors try it
out for themselves!
There are slight inconsistencies in behaviour around emitting additional
constraints when rewriting a type-family application (which I hope to iron
out soon), but I expect the impact of this to be very minimal. Other than
that, you can expect feature and behaviour parity with the native
implementation.

Please let me know how you get on, and which pain points you would like to
see addressed. My current ideas for improvement are as follows:

  - Functionality that would perform all the name resolution necessary in
the plugin initialisation. The user would provide a record of the types to
look up (a TyCon named ... in module ..., a Class named ... in module ...),
and the library would look up everything. This would be quite
straightforward with a library such as barbies, but I don't necessarily
want to impose that cognitive overhead on users who are not familiar with
it.
  - An interface for handling type family rewritings that provides a type
system that kind checks everything. For instance, instead of manually
calling splitTyConAppMaybe, we could feasibly instead use a pattern with
existential variables (matching on this pattern would introduce the kinds),
and then use a smart constructor instead of mkTyConApp (which would
kind-check the application). I certainly would have appreciated something
like this when writing my System F plugin, as handling all the kinds
explicitly was rather tiresome and error prone.
  - Functionality for recognising that a type has a certain form, making
use of Givens. For example, it can be quite annoying to find out whether a
given type is a type family application, as one needs to look through the
Givens to go through levels of indirection. For instance, one might come
across a variable "x" (ostensibly not a type family application), but have
Givens [G] y ~ x, [G] F a ~ y. (This happens often with flattening skolems.)

Please let me know if you have any other ideas, or suggestions on how to
tackle the above. Thanks.

Best,

Sam
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Rewriting plugins: request for feedback

[Sam Derbyshire]

Hello everyone,

I'm happy to report that I have implemented a compatibility layer in the
ghc-tcplugin-api library which provides type-family rewriting functionality
on GHC 9.0 and 9.2.
This means that plugin authors should now be able to use the exact same API
from GHC 9.0 onwards (and in particular, without waiting for a version of
GHC containing the new implementation of type-family rewriting plugins).

To refresh your memory, writing a type-checking plugin with this library
currently consists of the provision of a record

data TcPlugin = forall s. TcPlugin
  { tcPluginInit:: TcPluginM Init s
  , tcPluginSolve   :: s -> TcPluginSolver
  , tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter
  , tcPluginStop:: s -> TcPluginM Stop ()
  }

with the following type synonyms:

type TcPluginSolver
  =  [GHC.Ct] -- ^ Givens
  -> [GHC.Ct] -- ^ Wanteds
  -> TcPluginM Solve TcPluginSolveResult

Note that Deriveds are no longer passed explicitly. (It is possible to
retrieve the Derived constraints from the TcPluginM Solve monad; as they
are not commonly used, it made sense to make them less conspicuous.)

type TcPluginRewriter
  =  [GHC.Ct] -- ^ Givens
  -> [GHC.Type]   -- ^ Type family arguments (saturated)
  -> TcPluginM Rewrite TcPluginRewriteResult


On GHC 9.0 and 9.2, the tcPluginRewrite function will get hooked in as a
pre-pass of the user-supplied tcPluginSolve function.
There are small differences in behaviour that arise from solver plugins not
always getting a chance to run when GHC can solve the wanteds on its own,
but I expect this to have minimal impact.
On top of this, I expect (but have not measured) a performance degradation
compared to the "native" plugin type-family rewriting functionality, as the
solver plugin must traverse all constraints to find type-family
applications.

I have not tested this compatibility layer extensively, so I welcome all
feedback from plugin authors.

Note that I have also reduced the amount of re-exported datatype
constructors and accessors in an attempt to improve cross compatibility.
Please let me know of any difficulties that you encounter as a consequence,
and I will endeavour to re-export cross-compatible non-internal definitions.

Thanks,

Sam
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Rewriting plugins: request for feedback

[Sam Derbyshire]

Hi everyone,

Just a short message to let authors of type-checking plugins know that I've
updated the ghc-tcplugin-api library with backwards compatibility for GHC
9.0 and 9.2.
The functionality for rewriting type family applications will obviously not
be present on those versions, but I hope this will allow plugin authors to
try out the API for themselves and see what they think.

It shouldn't be much different from what you are used to; mostly a change
from "TcPluginM a" to MTL-style "MonadTcPlugin m => m a", or explicit
solver monad  "TcPluginM Solve a".
The main improvements that this library offers in its current state are, in
my opinion, as follows:
  - Decoupling from GHC, which has several upsides:
- needs of plugin authors can be addressed rapidly without needing to
wait for new GHC releases (of course, this doesn't apply to the changes
which require commensurate changes to GHC),
- cross-compatibility across GHC versions, hopefully lightening the CPP
burden on plugin authors.
  - More extensive documentation that should help people get started with
typechecking plugins. The haddocks remain available at the same page:
https://sheaf.github.io/ghc-tcplugin-api/GHC-TcPlugin-API.html

The library is available on the GitHub repository as before:
https://github.com/sheaf/ghc-tcplugin-api
I will upload the library to Hackage soon.

Thanks all,

Sam
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Rewriting plugins: request for feedback

[Christiaan Baaij]

Hi Sam,

Thanks for picking this up, the API looks good so far.
I'll try to port our https://hackage.haskell.org/package/ghc-typelits-extra
package to the new API.

Though first I need to upgrade
https://hackage.haskell.org/package/ghc-typelits-natnormalise to the GHC
9.2+ API,
which is got somewhat more complicated than usual GHC upgrades due to a
change in representation of (<=? :: Nat -> Nat -> Bool) in
https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e

I'll report back any issues I encounter if/when I encounter any.

Cheers,

Christiaan


On Wed, 16 Jun 2021 at 23:04, Sam Derbyshire 
wrote:

> Hey everyone,
>
> I've put up some haddocks for this new type-checking plugin API, see here:
> https://sheaf.github.io/ghc-tcplugin-api/GHC-TcPlugin-API.html.
> (The page is mainly meant to be navigated using the contents pane.)
>
> I hope this might be a more welcoming point of entry for people who are
> interested in learning about GHC typechecker plugins.
>
> Let me know what you think,
>
> Thanks,
>
> Sam
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Rewriting plugins: request for feedback

[Sam Derbyshire]

Hey everyone,

I've put up some haddocks for this new type-checking plugin API, see here:
https://sheaf.github.io/ghc-tcplugin-api/GHC-TcPlugin-API.html.
(The page is mainly meant to be navigated using the contents pane.)

I hope this might be a more welcoming point of entry for people who are
interested in learning about GHC typechecker plugins.

Let me know what you think,

Thanks,

Sam
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Rewriting plugins: request for feedback

[Sam Derbyshire]

Hi again everyone,


I've been making some more adjustments to the API of type-checking plugins.
Following a suggestion by Richard, the mechanism for reporting errors while
rewriting type family applications now consists of emitting a wanted
constraint with a custom type error message. There are several technical
reasons for this, which I will not get into.
This means there are now only two constructors of TcPluginRewriteResult:
TcPluginNoRewrite and TcPluginRewriteTo. Both of these now take an extra
argument: additional wanted constraints, which will be processed and
emitted by GHC.


Coming back to the type-checking plugin API as a whole (not just the
rewriting of type family applications), I've come to the realisation that
it is probably best to keep GHC's interface as simple as possible, to allow
library authors to write their own APIs.
After all, most of the API doesn't need to live within the GHC codebase,
and instead (in my opinion) belongs in libraries that simply import the ghc
package (which thankfully doesn't hide any exports one might want to use).
This means we don't have to tie any experimentation with type-checking
plugin APIs to the GHC release schedule.

To that end, I have concluded that one single non-backwards-compatible
change seems important: changing the TcPluginM monad from being isomorphic
to "ReaderT EvBindsVar TcM" to simply being a newtype around TcM. Then, we
instead pass an EvBindsVar as an extra argument to tcPluginSolve.
This avoids all the silly business with functions whose documentation said
"only call this within tcPluginSolve or it will cause a crash" (a situation
which was only made worse by the addition of rewriting plugins). It's also
less opinionated: library authors can use a ReaderT wrapper in their API if
they desire, but are not forced to do so.
Please note that I don't make this change lightly, as I know it is already
time-consuming enough to maintain type-checking plugins, especially as much
more significant changes abound (removal of flattening variables in GHC
9.2, removal of derived constraints (possibly in GHC 9.4)). I hope
nevertheless that you might find this acceptable.


Finally, facilitated by the above, I have started implementing a library
providing a simple API for type-checking plugins; see here
https://github.com/sheaf/ghc-tcplugin-api.
An example of a not-totally-trivial rewriting plugin is given here:
https://github.com/sheaf/ghc-tcplugin-api/blob/ad6ca964c3b27c28bb27392d7ba406cfac82176d/examples/RewriterPlugin/plugin/RewriterPlugin.hs
.
Note that I barely had to import anything from the ghc package; I hope this
can remain true for more involved plugins (up to a point).
Please let me know what you think, in particular if you think certain
important functions are missing from the API.

For this library specifically, I have added back ReaderT layers (but only
in the appropriate situations, to avoid reintroducing the aforementioned
problem with "only call this in tcPluginSolve"), and provided MTL-style
typeclasses for operations that work with multiple different phases of the
plugin.
Other design options are of course possible; at any rate, I think it is
preferable to be making these API choices outside of GHC itself whenever
possible.
I've also included helpers for creating custom type errors within
type-checking plugins, as that was unnecessarily cumbersome. (One still
needs to provide a CtLoc to inform GHC of the source location of the error;
one can get this from a constraint fed to the plugin in a solver plugin, or
from the rewriting environment in a rewriter plugin).


Note that this all still depends on the WIP GHC MR 5909, available at
https://gitlab.haskell.org/ghc/ghc/-/merge_requests/5909.


I look forward to your feedback,

Thanks,

Sam
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Rewriting plugins: request for feedback

[Sam Derbyshire]

Hi everyone,

Recent refactors to the constraint solver have complicated the story for
authors of type-checking plugins. Following a suggestion by Christiaan
Baaij, and aided by Richard Eisenberg, I'm working on adding the ability
for type-checking plugins to rewrite type family applications directly
(hooking straight into GHC's type-family rewriting code). The goal is to
ease migration for the plugin authors, hopefully simplifying the common
operation of rewriting type family applications.


Let me now describe the current API for this new functionality, for which I
would like feedback.

--

A new field is added to the TcPlugin data type, namely

tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter

Here s is the existential plugin state that users can choose as they wish
for their own plugin.
Plugins thus register which type family TyCons they are interested in
rewriting, like so:

myTcPluginRewrite :: MyPluginState -> UniqFM TyCon TcPluginRewriter
myTcPluginRewrite s@(MyPluginState {myFam1TyCon, myFam2TyCon}) =
  listToUFM [ (myFam1TyCon, myFam1Rewriter s), (myFam2TyCon, myFam2Rewriter
s) ]

For each type family TyCon, the plugin should provide a rewriting function
(corresponding to myFam1Rewriter and myFam2Rewriter above), of type

type TcPluginRewriter = [Ct] -> [TcType] -> TcPluginM TcPluginRewriteResult

This means that a rewriting function is supplied with the current Given
constraints and the arguments of the (guaranteed to be saturated)
type-family application, and should return a result of type:

data TcPluginRewriteResult where
  TcPluginRewriteError
:: (Diagnostic a, Typeable a) => a -> TcPluginRewriteResult
  TcPluginNoRewrite
:: TcPluginRewriteResult
  TcPluginRewriteTo
:: { rewriteTo :: TcType
   , rewriteEvidence :: TcCoercion }
-> TcPluginRewriteResult

That is, the plugin can specify what the type-family application should be
rewritten to, throw an error, or do nothing.

--

I'm hoping that the components of existing type-checking plugins concerned
with type-family applications can instead use this mechanism and achieve
more robust results by doing so, with less effort.

I would like to hear from plugin authors whether this API suits their
needs. If you know of someone not on this list that might be interested,
please invite them to join the conversation.

The current state of this patch can be found in the GHC MR 5909:
https://gitlab.haskell.org/ghc/ghc/-/merge_requests/5909

Thanks,

Sam
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs