An exploration of emulating higher-kinded types (HKTs) in Rust using Generic Associated Types (GATs), which accidentally triggers a trait requirement evaluation overflow. The post explains why: Rust's trait solver is inductive and cannot handle cyclic proof trees for non-coinductive traits like PartialEq. Along the way, it covers type theory fundamentals (kinds, type constructors), mathematical induction and structural induction, the Curry-Howard isomorphism, a hands-on Lean 4 proof of a divisibility theorem, and finally how Rust's chalk-based and next-gen trait solvers handle inductive vs. coinductive goals. The experiment ultimately triggers an internal compiler error (ICE) in rustc's next-gen solver when using -Znext-solver=globally.
Table of contents
Induction beyond natural numbers #That moment when Curry and Howard did a joint yaoi slay and caused a motherquake measuring 9.9 on the cunter scale #The self-indulgent Lean 4 part of the article #1 Comment
Sort: