Many fancy types (e.g., generalized algebraic data types, type families)
require a type checker plugin. These fancy types have a type index
(e.g., type level natural numbers) with an equality relation that is
difficult or impossible to represent using GHC's built-in type equality. The
most practical way to represent these equality relations is through a plugin
that asserts equality constraints. However, such plugins are
difficult to write and reason about.

In this paper, we (1) present a formal theory of reasoning about the
correctness of type checker plugins for type indices, and, (2) apply this
theory in creating Thoralf, a generic and extensible
plugin for type indices that translates GHC constraint problems to queries to
an external SMT solver. By "generic and extensible", we mean the
restrictions on extending Thoralf are slight, and, if some type index could
be encoded as an SMT sort, then a programmer could extend Thoralf by
providing this encoding function.