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 <sam.derbyshire at gmail.com>
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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210709/79148987/attachment.html>