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