If the type error is at an implicit argument, we annotate
application with `pp.explicit := true`
Given the type incorrect definition
```
def f {a b c : α} : a = c :=
Eq.trans (a := a) (b := b = c)
```
We now generate the error
```
error: application type mismatch
@Eq.trans α a (b = c)
argument
b = c
has type
Prop
but is expected to have type
α
```
@Kha Note that we only enable `pp.explicit := true` for the relevant
application. That is, we set `pp.explicit := false` for each children.
Unfortunately, there is a corner case.
```
set_option pp.explicit true
def f {a b c : α} : a = c :=
Eq.trans (a := a) (b := b = c)
```
produces the error
```
error: application type mismatch
@Eq.trans α a (b = c)
argument
@Eq α b c
has type
Prop
but is expected to have type
α
```
The reset `pp.explicit := false` overwrote the user option.
I think the simplest solution is the following
1- The delaborator saves the initial set of Options `Init`
2- When it finds a node annotated with a `pp` options, it only
consider the option if it is not set by `Init`.
What do you think?
@Kha I was tired of writing `arbitrary _` :)
There 0 places in the stdlib where the type needs to be provided.
If in the future we need to specify the type we can use
`arbitrary (α := <type>)`
In the following example, the output produced by `dbgTrace!` was not
being captured. It could break the lean server. At least, it broke the lean4-mode.
```lean
def f (x : Nat) : Nat :=
dbgTrace! ">>> " ++ toString x;
x + 1
eval f 10
```
cc @Kha
@Kha We currently have a few macros that create binder names
such as `x`. These macros rely on the hygienic framework. This part is
great. Before this commit we were simply erasing the macro
scopes when creating the actual binders at `Expr.lean`.
The result produced expressions that were hard to debug.
For example, consider the following scenario
1- Macro creates a few binder names using ``x <- `(x)``
2- We create a lambda expression `t` with these binder names.
3- Then, we use `lambdaTelescope t fun xs body => ...`
Now, if we trace `xs` and `body`, we get `#[x, x, ... x]` and
we can't distinguish the different `x`s in `body`.
So, it is really hard to debug anything using the traces.
This commit adds `Name.simpMacroScopes` for simplying "macro scoped"
names. Example: given `x._@.Init.Data.List.Basic._hyg.2.5`, it
produces `x.2.5`. I exported this function, and used it in the old
pretty printer.
I have considered modifying `lambdaTelescope` to make sure it creates
unused names. I think this option is bad because it introduces
overhead, and in a few places we want to preserve the binder names.
I have also considered replacing the `let x := x.eraseMacroScopes` at
`Expr.lean` with `let x := x.simpMacroScopes`. I think this option is
bad since we are destroying scoping information and will not be able
to distiguish which variables have macro scopes when processing
tactics.
Anyway, the solution in this commit is good for this week, but we
should discuss a more permanent solution next week.
