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?
`MacroM` will implement `MonadRef` because
1- It will be easier to throw errors from macros
2- We will be able to `getRef` to retrieve the syntax node at macro
rules.
I renamed `Ref` to `MonadRef` to make it consistent with other classes
providing monadic methods (e.g. `MonadEnv`, `MonadState`, etc).
cc @Kha
The idea is to make clear that the field `posponed` is transient
state. It is only used during `isDefEq`.
The refactoring was motivated by a bug I found where the `posponed`
constraints were not being handled correctly. For example,
the `check (e : Expr)` method was returning `true`, but leaving pending
universe constraints at `postponed`.
cc @Kha
