closes#341
This is another instance of a compiler bug.
It is in the code that is still written in C/C++.
We need to infer types in the compiler, and we reused the kernel type
checker for this.
However, the compiler performs transformations that may produce type
incorrect terms.
This happens in code that makes heavy use of dependent types (like the
new test).
This is just a workaround for this particular instance of the problem.
The definitive solution will only happen when we replace
this part of the compiler with Lean code, and implement a custom
`inferType` method for the compiler.
The current commit only detects lambda expressions that should be
lifted eagerly.
@kha I added a comment describing why this optimization is useful.
Right now, we are not writing code that benefits from this optimization,
but it seems very useful for implementing combinators that return
a tuple containing functions. I think this is a useful idiom, for
example, the combinator may have two parts: one that is the actual
action, and another that collects "static properties".
Last summer, if I remember correctly, you considered building this
kind of combinator for the new Lean parser, but gave up because we
did not have compiler support for it. In your case, the "static
property" would be the set of tokens. It could also contain the left
most token for initializing the Pratt parser table, etc.
This commit is the first step to make this kind of code efficient.
It will also improve the experiment at `tests/playground/parser/`
