Jon Sterling
Jon Sterling
What I don't like about the current unification algorithm is that by restricting the pattern fragment to things applied to spines of variables, we end up needing to do a...
Lean has a really nice feature where names are hierarchical, so a single declaration `foo` might elaborate such that `foo` has a meaning, but also `foo.x` and `foo.y` etc. have...
I want a hole to be able to range over a suffix to the spine. While we support interactive backward construction already, this would enable interactive *forward* construction.
It would be nice to print holes using the source language rather than the core language by default, since users shouldn't be expected to understand the intricacies of the core....
In order to unleash #118, it will be necessary to have a (non-core/untrusted) version of the typechecker that runs in the `Contextual` monad and invokes the unifier at key points....
So far we have needed some kind of fancy subtyping rules for restriction and extension types (which I majorly bungled before)---and I was thinking that there may be a better...
I'm mostly meaning "informative for the developer" than for the user at this point---the problem is that in many parts of the code, we just ask *whether* something typechecks or...
Now it's time to find out what it means to do unification under a restriction `r=r'`. The issue is that the naive version results in unleashing solutions that only make...
I wonder if all this would be easier using hereditary substitutions and a purely syntactic approach, than the NBE machinery. I'm not exactly sure, but I want to consider it...