@Kha This commit addresses an issue reported by Kevin. Holes and tactic
blocks represent a discontinuity in the elaboration process.
By introducing inaccessible variables (or "things" as Kevin calls
them), we create error message that are harder to understand (see
affected test), and goals where we didn't allow the user to select the
variable name and/or eagerly unfolded a definition.
BTW, I first considered using "reducible" setting when deciding
whether to insert implicit lambdas or not. This is a bad idea.
See `monotone.lean` test. The decision should not depend on
reducibility status, but whether there is "discontinuity" on the
elaboration process or not. As Kevin pointed out,
"introducing implicits work great if you finish the job".
If generated type is not correct, we should abort "discriminant
refinement", and use the original error message because users may
be confused by a type error on something they did not write.
@Kha It seems the recent parser modifications created some unexpected
problems. I didn't investigate them. I am "lost" in the elaborator and
dependent pattern matching land.
1) We can't write anymore
```
f [1, 2, 3] |>.run' 0 = Except.ok ()
```
We have to use parentheses and the error message is weird :(
```
(f [1, 2, 3] |>.run' 0) = Except.ok ()
```
2) I had to add comments to `macro.lean`, I didn't find a workaround
for one of the rules. BTW, I had to add a bunch of `:term` for fixing
the other rules, and the error messages were counterintuitive.
