<div dir="ltr"><div>Hi everyone,</div><div><br></div><div>Recent refactors to the constraint solver have complicated the story for authors of type-checking plugins. Following a suggestion by Christiaan Baaij, and aided by Richard Eisenberg, I'm working on adding the ability for type-checking plugins to rewrite type family applications directly (hooking straight into GHC's type-family rewriting code). The goal is to ease migration for the plugin authors, hopefully simplifying the common operation of rewriting type family applications.<br></div><div><br></div><div></div><div><br></div><div>Let me now describe the current API for this new functionality, for which I would like feedback.<br></div><div><br></div><div>--------------------------------------------------------------------------<br></div><div><br></div><div>A new field is added to the TcPlugin data type, namely</div><div><br></div><div>tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter</div><div><br></div><div>Here s is the existential plugin state that users can choose as they wish for their own plugin.</div><div>Plugins thus register which type family TyCons they are interested in rewriting, like so:</div><div><br></div><div>myTcPluginRewrite :: MyPluginState -> UniqFM TyCon TcPluginRewriter<br></div><div>myTcPluginRewrite s@(MyPluginState {myFam1TyCon, myFam2TyCon}) =</div><div>  listToUFM [ (myFam1TyCon, myFam1Rewriter s), (myFam2TyCon, myFam2Rewriter s) ]<br></div><div><br></div><div>For each type family TyCon, the plugin should provide a rewriting function (corresponding to myFam1Rewriter and myFam2Rewriter above), of type</div><div><br></div><div>type TcPluginRewriter = [Ct] -> [TcType] -> TcPluginM TcPluginRewriteResult</div><div><br></div><div>This means that a rewriting function is supplied with the current Given constraints and the arguments of the (guaranteed to be saturated) type-family application, and should return a result of type:</div><div><br></div>data TcPluginRewriteResult where<br>  TcPluginRewriteError<br>    :: (Diagnostic a, Typeable a) => a -> TcPluginRewriteResult<br>  TcPluginNoRewrite<br>    :: TcPluginRewriteResult<br>  TcPluginRewriteTo<br>    :: { rewriteTo :: TcType<br>       , rewriteEvidence :: TcCoercion }<br><div>    -> TcPluginRewriteResult</div><div><br></div><div>That is, the plugin can specify what the type-family application should be rewritten to, throw an error, or do nothing.</div><div><br></div><div>
-------------------------------------------------------------------------- <br></div><div><br></div><div>
I'm hoping that the components of existing type-checking plugins concerned with type-family applications can instead use this mechanism and achieve more robust results by doing so, with less effort. <br></div><div><br></div><div>I would like to hear from plugin authors whether this API suits their needs. If you know of someone not on this list that might be interested, please invite them to join the conversation.</div><div><br></div><div>The current state of this patch can be found in the GHC MR 5909: <a href="https://gitlab.haskell.org/ghc/ghc/-/merge_requests/5909">https://gitlab.haskell.org/ghc/ghc/-/merge_requests/5909</a></div><div><br></div><div>Thanks,</div><div><br></div><div>Sam</div><div></div></div>