[PDF], might be better to switch to the abstract page at https://dl.acm.org/doi/10.1145/66068.66075 https://dl.acm.org/doi/10.1145/66068.66075 Occurs-check-les

[PDF], might be better to switch to the abstract page at https://dl.acm.org/doi/10.1145/66068.66075 https://dl.acm.org/doi/10.1145/66068.66075 Occurs-check-less unification is in fact a well-defined operation once you realize it’s just giving you infinite (specifically regular) trees, but those are not at all straightforward (or fast) to process, and I don’t know if you can build a convincing Prolog out of them. I do know that basically nobody uses equirecursive types (that is recursive types described as potentially infinite type constructor expressions) because the resulting regular tree wrangling is hell on your typechecker’s performance (and maybe also because non-regular recursive algebraic types are occasionally useful).