19.03.2026
В статье автор экспериментирует с эмуляцией высших типов (HKTs) в Rust через обобщенные ассоциированные типы (GATs), пытаясь абстрагировать обертки для AST. Оказывается, в Rust это не так просто сделать. Решение в лоб приводит к рекурсивному определению типа, которое заставляет компилятор проверять бесконечное дерево доказательств для трейта PartialEq
Автор углубляется в теорию: объясняет индукцию на примерах из математики и Lean 4, а затем переходит к коиндукции, чтобы объяснить, почему рекурсивные структуры с типами-обертками приводят к сбою текущего солвера трейтов Rust
