Reed Mullanix
Reed Mullanix
IIUC the subtlety starts to sneak in when you have to think about how let-generalization behaves. With that in mind, `MonoLocalBinds` might also be good to have on by default.
The other question that needs to be answered is how the compiler ought to operate. A batch mode compiler is simpler, but does make writing tooling much, much harder (see...
I would avoid using bound tbh. It can be super slow, and if you have a renaming pass most of the problems it solves disapear.
> Can this be unified with Cat.Functor.Coherence? Should be able to! We will need to generalize `make-copattern` to work on functions into record types, but this shouldn't be too hard.
Should be good to go. Played around with a version of "deep" `cohere!` that would let us solve things like https://1lab.dev/Cat.Functor.Adjoint.html#25843 but this proved to be a bit tricky
Sorry, have been quite busy recently! Sheaves would be a good place, likewise for categories of free F-algebras
Just putting this up for a CI run, prose is still a bit rough
In a similar vein `Ignore` looks very useful. #30 should be a starting point for an implementation.
I totally agree with you on abstracting out the more general notion of substitution out of `Subst`. As for literature, Erwin Brady's [paper on Idris Elaboration](https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf) should be a good...
Yeah, that sounds like a much better solution. I'll hopefully have something by the end of day.