TIL: Rust's lack of HKTs can cause inductive cycles that ICE the compiler

Velx Dev — Sat, 14 Mar 2026 20:35:34 +0000

Just spent some time reading a really wild blog post about Rust's type system and I had to share the rabbit hole it took me down.

The setup: someone was writing an FP scripting language and wanted to abstract over wrapper types (like Spanned<T> vs Simple<T>) using a GAT-based HKT emulation pattern. Pretty standard stuff for type-fu enthusiasts.

The problem: when they derived PartialEq on their recursive type that used this pattern, rustc threw an E0275 overflow evaluating trait requirements. The derive was creating a circular dependency: to prove Foo<W>: PartialEq, you need W::Wrapper<Foo<W>>: PartialEq, which requires Foo<W>: PartialEq again.

This is actually a coinduction problem. Rust's trait solver is inductive by default - proofs must terminate. Only auto-traits like Send/Sync are coinductive (allowing infinite/cyclic proof trees). So you literally cannot derive PartialEq on certain recursive GAT types right now.

The author went on a detour into mathematical induction vs coinduction, even writing proofs in Lean 4 to understand what was happening. Then someone found an ICE (internal compiler error) using -Znext-solver=globally with these patterns.

The fix is coming with the next-gen trait solver, but it's not stable yet.

TIL: type theory rabbit holes can start from something as innocent as wanting to wrap AST nodes differently. Also coinduction is wild.

Original article: https://www.harudagondi.space/blog/torturing-rustc-by-emulating-hkts

DEV Community: Velx Dev

TIL: Rust's lack of HKTs can cause inductive cycles that ICE the compiler