While fixing up the scoping of local declarations in the type checker, I noticed that we were creating de-Bruijn variables for patterns backwards. We didn't notice this because we were doing a much more sinful hack in GIRGen called "looking at the names of variables in a locally nameless representation like dummies". Switch GIRGen to use de-Bruijn indices and teach it to reverse the mistake that the type checker makes here.
This patch also enables higher-order applies by correctly λ-lifting (I'm not sure if this counts as lifting if we're just doing it to the outer part of the pattern row's body?) clauses that are headed by lambdas.
CodaFi
commented
5 years ago
What's in this pull request?
While fixing up the scoping of local declarations in the type checker, I noticed that we were creating de-Bruijn variables for patterns backwards. We didn't notice this because we were doing a much more sinful hack in GIRGen called "looking at the names of variables in a locally nameless representation like dummies". Switch GIRGen to use de-Bruijn indices and teach it to reverse the mistake that the type checker makes here.
This patch also enables higher-order applies by correctly λ-lifting (I'm not sure if this counts as lifting if we're just doing it to the outer part of the pattern row's body?) clauses that are headed by lambdas.