<div dir="auto">This sounds very cool!</div><div dir="auto"><br></div><div dir="auto">FYI the Inria paper link in the readme seems to not be correct? </div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Jul 9, 2021 at 6:56 PM Sam Derbyshire <<a href="mailto:sam.derbyshire@gmail.com">sam.derbyshire@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Hi all,</div><div><br></div><div>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 (<a href="https://github.com/sheaf/ghc-tcplugin-api" target="_blank">https://github.com/sheaf/ghc-tcplugin-api</a>), see the readme.</div><div><br></div><div>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!</div><div>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.<br></div><div><br></div><div>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:</div><div><br></div><div>  - 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.<br></div><div>  - 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.<br></div><div>  - 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.)<br></div><div><br></div><div>Please let me know if you have any other ideas, or suggestions on how to tackle the above. Thanks.<br></div><div><br></div><div>Best,</div><div><br></div><div>Sam<br></div><div><br></div></div>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div></div>