This content originally appeared on DEV Community and was authored by Velx Dev
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
This content originally appeared on DEV Community and was authored by Velx Dev
Velx Dev | Sciencx (2026-03-14T20:35:34+00:00) TIL: Rust’s lack of HKTs can cause inductive cycles that ICE the compiler. Retrieved from https://www.scien.cx/2026/03/14/til-rusts-lack-of-hkts-can-cause-inductive-cycles-that-ice-the-compiler-3/
Please log in to upload a file.
There are no updates yet.
Click the Upload button above to add an update.