This PR refines the new wording of the "application type mismatch" error
message to avoid ambiguity in references to the "final" argument in a
subexpression that may be followed by additional arguments.
It does so by replacing "final" with "last," rephrasing the message so
that this adjective modifies the argument itself rather than the word
"argument," and only displaying this wording when two arguments could be
confused (determined by expression equality).
These changes were motivated by a report that in cases where a function
application `f a b c` fails to elaborate because `b` is incorrectly
typed, the existing error message's reference to `b` being the "final"
argument in the application `f a b` may create confusion because it is
not the final argument in the full application expression.
This PR changes `addPPExplicitToExposeDiff` to show universe differences
and to visit into projections, e.g.:
```
error: tactic 'rfl' failed, the left-hand side
(Test.mk (∀ (x : PUnit.{1}), True)).1
is not definitionally equal to the right-hand side
(Test.mk (∀ (x : PUnit.{2}), True)).1
```
for
```lean
inductive Test where
| mk (x : Prop)
example : (Test.mk (∀ _ : PUnit.{1}, True)).1 = (Test.mk (∀ _ : PUnit.{2}, True)).1 := by
rfl
```
This PR rewords the `application type mismatch` error message by more
specifically mentioning that the problem is with the final argument.
This is useful when the same argument is passed to the function multiple
times.
We decided against using a wording which specifically mentions the
"function expression", because users who are not used to currying might
not think of the `f a` in `f a b` as a function.
This PR makes it harder to create "fake" theorems about definitions that
are stubbed-out with `sorry` by ensuring that each `sorry` is not
definitionally equal to any other. For example, this now fails:
```lean
example : (sorry : Nat) = sorry := rfl -- fails
```
However, this still succeeds, since the `sorry` is a single
indeterminate `Nat`:
```lean
def f (n : Nat) : Nat := sorry
example : f 0 = f 1 := rfl -- succeeds
```
One can be more careful by putting parameters to the right of the colon:
```lean
def f : (n : Nat) → Nat := sorry
example : f 0 = f 1 := rfl -- fails
```
Most sources of synthetic sorries (recall: a sorry that originates from
the elaborator) are now unique, except for elaboration errors, since
making these unique tends to cause a confusing cascade of errors. In
general, however, such sorries are labeled. This enables "go to
definition" on `sorry` in the Infoview, which brings you to its origin.
The option `set_option pp.sorrySource true` causes the pretty printer to
show source position information on sorries.
**Details:**
* Adds `Lean.Meta.mkLabeledSorry`, which creates a sorry that is labeled
with its source position. For example, `(sorry : Nat)` might elaborate
to
```
sorryAx (Lean.Name → Nat) false
`lean.foo.12.8.12.13.8.13._sorry._@.lean.foo._hyg.153
```
It can either be made unique (like the above) or merely labeled. Labeled
sorries use an encoding that does not impact defeq:
```
sorryAx (Unit → Nat) false (Function.const Lean.Name ()
`lean.foo.14.7.13.7.13.69._sorry._@.lean.foo._hyg.174)
```
* Makes the `sorry` term, the `sorry` tactic, and every elaboration
failure create labeled sorries. Most are unique sorries, but some
elaboration errors are labeled sorries.
* Renames `OmissionInfo` to `DelabTermInfo` and adds configuration
options to control LSP interactions. One field is a source position to
use for "go to definition". This is used to implement "go to definition"
on labeled sorries.
* Makes hovering over a labeled `sorry` show something friendlier than
that full `sorryAx` expression. Instead, the first hover shows the
simplified ``sorry `«lean.foo:48:11»``. Hovering over that hover shows
the full `sorryAx`. Setting `set_option pp.sorrySource true` makes
`sorry` always start with printing with this source position
information.
* Removes `Lean.Meta.mkSyntheticSorry` in favor of `Lean.Meta.mkSorry`
and `Lean.Meta.mkLabeledSorry`.
* Changes `sorryAx` so that the `synthetic` argument is no longer
optional.
* Gives `addPPExplicitToExposeDiff` awareness of labeled sorries. It can
set `pp.sorrySource` when source positions differ.
* Modifies the delaborator framework so that delaborators can set Info
themselves without it being overwritten.
Incidentally closes#4972.
Inspired by [this Zulip
thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Is.20a.20.60definition_wanted.60.20keyword.20possible.3F/near/477260277).
Example: Normally subtype notation pretty prints as `{ x // x > 0 }`,
but now the difference in domains is exposed:
```lean
example (h : {x : Int // x > 0}) : {x : Nat // x > 0} := h
/-
error: type mismatch
h
has type
{ x : Int // x > 0 } : Type
but is expected to have type
{ x : Nat // x > 0 } : Type
-/
```
Example:
```lean
example : 0 = (0 : Nat) := by
exact Eq.refl (0 : Int)
/-
error: type mismatch
Eq.refl 0
has type
(0 : Int) = 0 : Prop
but is expected to have type
(0 : Nat) = 0 : Prop
-/
```
Type mismatch errors have a nice feature where expressions are annotated
with `pp.explicit` to expose differences via `isDefEq` checking.
However, this procedure has side effects since `isDefEq` may assign
metavariables. This PR wraps the procedure with `withoutModifyingState`
to prevent assignments from escaping.
Assignments can lead to confusing behavior. For example, in the
following a higher-order unification fails, but the difference-finding
procedure unifies metavariables in a naive way, producing a baffling
error message:
```lean
theorem test {f g : Nat → Nat} (n : Nat) (hfg : ∀a, f (g a) = a) :
f (g n) = n := hfg n
example {g2 : ℕ → ℕ} (n2 : ℕ) : (λx => x * 2) (g2 n2) = n2 := by
with_reducible refine test n2 ?_
/-
type mismatch
test n2 ?m.648
has type
(fun x ↦ x * 2) (g2 n2) = n2 : Prop
but is expected to have type
(fun x ↦ x * 2) (g2 n2) = n2 : Prop
-/
```
With the change, it now says `has type ?m.153 (?m.154 n2) = n2`.
Note: this uses `withoutModifyingState` instead of `withNewMCtxDepth`
because we want to know something about where `isDefEq` failed — we are
trying to simulate a very basic version of `isDefEq` for function
applications, and we want the state at the point of failure to know
which argument is "at fault".
@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 :)
@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?
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
