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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210710/c4434a0d/attachment.html>