@Kha this is a fix for the example that @gebner posted on Zulip.
There are other possible workarounds, but I think this one is
"intuitive".
Here is the problem description and workaround.
We currently use the `withPosition` combinator at `matchAlts`. The
original motivation was nested `match`-expressions without
parenthesis.
We also have the `checkColGt` in the application parser.
Thus, `frob 5` is not parsed as an application. That is, the term
parser after the `then` keyword stops at `frob`.
Then, we get the weird "expected 'else'" error message at `5` :)
In this commit, I add a `checkColGe` check at the beginning of each
alternative right-hand-side.
The effect on the stdlib was minimal. It basically affected old code
that used the Lean 3 workaround for partial functions
```
partial def f : N -> N | i =>
...
```
In Lean 4, we can use the more natural
```
partial def f (i : N) : N :=
...
```
or
```
partial def f : N -> N := fun i =>
...
```
It also affected code such as
```
instance : Repr String.Iterator where
reprPrec | ⟨s, pos⟩, prec =>
Repr.addAppParen ("String.Iterator.mk " ++ reprArg s ++ " " ++ reprArg pos) prec
```
This is a workaround for a missing feature. We really wanted to write
```
instance : Repr String.Iterator where
reprPrec ⟨s, pos⟩ prec :=
Repr.addAppParen ("String.Iterator.mk " ++ reprArg s ++ " " ++ reprArg pos) prec
```
@Kha I marked the corresponding methods as `protected`.
I currently can't stand `throw_error`, and I am optimistic about
server highlighting feature you are working on :)
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.
@Kha, Jason's example on issue #337 suggests that injecting
implicit-lambdas while elaborating patterns is problematic.
The elaborator was injecting `fun {Γ} =>` before the
pattern variable `ftm`.
So, I disabled the implicit-lambda during pattern elaboration. I
didn't find an example where it would be useful.
see #337
cc @JasonGross
@Kha we do that in Lean 3. It helps when the error is due to incorrect universe levels.
BTW, I had to update `tests/lean/server/content_diag.json` since the
error message is different, but a few other stuff changed too.
Could you please take a look whether the test is still correct?
