GHC typechecker plugins are a useful mechanism through which users can introduce knowledge into GHC’s typechecker, such as augmenting GHC with a solver for propositional logic [1], Presburger [2] or Peano arithmetic [3], dimensional analysis [4], regular grammars [5].

However, it can be difficult to maintain a typechecker plugin to work across GHC versions, as internal aspects of GHC’s typechecker change.

In this talk, I present a new interface for typechecking plugins which aims to solve this problem. This includes:

• a review of the existing type-checking plugin functionality,
• an illustration of the new functionality for rewriting type-family applications,
• the ghc-tcplugin-api library which aims to provide a stable interface for authors of typechecking plugins.

[1] Matt Noonan - Ghosts of Departed Proofs (https://doi.org/10.1145/3299711.3242755)

[2] Hiromi Ishii - ghc-typelits-presburger library (https://hackage.haskell.org/package/ghc-typelits-presburger)

[3] Christiaan Baaij - ghc-typelits-natnormalise library (https://hackage.haskell.org/package/ghc-typelits-natnormalise)

[4] Adam Gundry - A Typechecker Plugin for Units of Measure (https://doi.org/10.1145/2804302.2804305)

[5] Oleg Grenrus - Regular Expressions of Types (http://oleg.fi/gists/posts/2018-09-13-regular-expressions-of-types.html)