Type Checking with Rewriting Rules

Type classes support the implementation of highly reusable algorithms and data structures without loss of efficiency. Initially developed in Haskell, they have become central to the design of several modern programming languages, including Swift, Rust, Hylo, and Carbon. A key part of their success is the ability to express sophisticated abstractions using constraints on the types associated with their operations. However, this expressiveness invites thorny theoretical and engineering questions. In particular, the support of recursive constraints—i.e., constraints specifying that an associated type of an abstraction must be a model of that abstraction—leaves type equivalence undecidable. This paper studies a semi-decidable technique to tackle this problem that was first developed in Swift’s compiler. The core idea is to encode constraints into a term rewriting system and use normalization to answer type checking queries. We describe this approach formally through the lens of FG, a calculus originally designed to capture generic programming best practices; and discuss an implementation in the context of Hylo, a language inspired by Swift and Rust.