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.derbysh...@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@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