Achieve a more predictable support for inductive types and easier support for unification.
Context
As I lack a dual for dependent intersections, I'm starting to feel like it is better presented as a self type + an intersection type, additionally dependent intersections require some form of coercion in the general case, while self types just require instantiation, which fits neatly in an HM-like system.
Goals
Achieve a more predictable support for inductive types and easier support for unification.
Context
As I lack a dual for dependent intersections, I'm starting to feel like it is better presented as a self type + an intersection type, additionally dependent intersections require some form of coercion in the general case, while self types just require instantiation, which fits neatly in an HM-like system.
Related
186