Support self dependent recursive types. Such as inductive families and equality.
Context
The current hackish solution for introduction of self types and coercion breaks when meeting a lambda, here I just add propagation through the lambdas by tracking the alias and essentially doing eta expansion in a terrible way.
Additionally, there is some bugs in coercion, which I mitigate by doing equality on every coercion, of course this makes coercion quadratic, but it's good enough for now.
Goals
Support self dependent recursive types. Such as inductive families and equality.
Context
The current hackish solution for introduction of self types and coercion breaks when meeting a lambda, here I just add propagation through the lambdas by tracking the alias and essentially doing eta expansion in a terrible way.
Additionally, there is some bugs in coercion, which I mitigate by doing equality on every coercion, of course this makes coercion quadratic, but it's good enough for now.
Related
199