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
Top comments (0)