@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.
@Vtec234 I was super confused about why the LEAN_PATH seemed to be set
up the wrong way when in reality an import failed to compile. If this is
an issue in the client or on Windows, we must fix it there.
@Kha The default value (false) for `pp.inaccessibleNames == false` help when
visualizing error messages (see test
`hidingInaccessibleNames.lean`). We added this feature after to hide
intermediate variables created by `match_syntax`.
However, this default value confused me in tactic mode. For example,
it will hide a hypotheses `x : Fin 0` if nobody depends on it, but as
a user we want to know we have it since we can close the goal using
it. Thus, I added `withPPInaccessibleNames act`, it executes `act`
using `pp.inaccessibleNames true` if the user did not explicitly set
it. I use this combinator at `FileWorker` and when producing the
`unsolved goals` error message. In all other scenarios, I believe
hiding these inaccessible variables is a good thing.
