This PR migrates usages of `Std.Range` to the new polymorphic ranges.
This PR unfortunately increases the transitive imports for
frequently-used parts of `Init` because the ranges now rely on iterators
in order to provide their functionality for types other than `Nat`.
However, iteration over ranges in compiled code is as efficient as
before in the examples I checked. This is because of a special
`IteratorLoop` implementation provided in the PR for this purpose.
There were two issues that were uncovered during migration:
* In `IndPredBelow.lean`, migrating the last remaining range causes
`compilerTest1.lean` to break. I have minimized the issue and came to
the conclusion it's a compiler bug. Therefore, I have not replaced said
old range usage yet (see #9186).
* In `BRecOn.lean`, we are publicly importing the ranges. Making this
import private should theoretically work, but there seems to be a
problem with the module system, causing the build to panic later in
`Init.Data.Grind.Poly` (see #9185).
* In `FuzzyMatching.lean`, inlining fails with the new ranges, which
would have led to significant slowdown. Therefore, I have not migrated
this file either.
This PR improves the “expected type mismatch” error message by omitting
the type's types when they are defeq, and putting them into separate
lines when not.
I found it rather tediuos to parse the error message when the expected
type is long, because I had to find the `:` in the middle of a large
expression somewhere. Also, when both are of sort `Prop` or `Type` it
doesn't add much value to print the sort (and it’s only one hover away
anyways).
This PR implements first-class support for nondependent let expressions
in the elaborator; recall that a let expression `let x : t := v; b` is
called *nondependent* if `fun x : t => b` typechecks, and the notation
for a nondependent let expression is `have x := v; b`. Previously we
encoded `have` using the `letFun` function, but now we make use of the
`nondep` flag in the `Expr.letE` constructor for the encoding. This has
been given full support throughout the metaprogramming interface and the
elaborator. Key changes to the metaprogramming interface:
- Local context `ldecl`s with `nondep := true` are generally treated as
`cdecl`s. This is because in the body of a `have` expression the
variable is opaque. Functions like `LocalDecl.isLet` by default return
`false` for nondependent `ldecl`s. In the rare case where it is needed,
they take an additional optional `allowNondep : Bool` flag (defaults to
`false`) if the variable is being processed in a context where the value
is relevant.
- Functions such as `mkLetFVars` by default generalize nondependent let
variables and create lambda expressions for them. The
`generalizeNondepLet` flag (default true) can be set to false if `have`
expressions should be produced instead. **Breaking change:** Uses of
`letLambdaTelescope`/`mkLetFVars` need to use `generalizeNondepLet :=
false`. See the next item.
- There are now some mapping functions to make telescoping operations
more convenient. See `mapLetTelescope` and `mapLambdaLetTelescope`.
There is also `mapLetDecl` as a counterpart to `withLetDecl` for
creating `let`/`have` expressions.
- Important note about the `generalizeNondepLet` flag: it should only be
used for variables in a local context that the metaprogram "owns". Since
nondependent let variables are treated as constants in most cases, the
`value` field might refer to variables that do not exist, if for example
those variables were cleared or reverted. Using `mapLetDecl` is always
fine.
- The simplifier will cache its let dependence calculations in the
nondep field of let expressions.
- The `intro` tactic still produces *dependent* local variables. Given
that the simplifier will transform lets into haves, it would be
surprising if that would prevent `intro` from creating a local variable
whose value cannot be used.
Note that nondependence of lets is not checked by the kernel. To
external checker authors: If the elaborator gets the nondep flag wrong,
we consider this to be an elaborator error. Feel free to typecheck `letE
n t v b true` as if it were `app (lam n t b default) v` and please
report issues.
This PR follows up from #8751, which made sure the nondep flag was
preserved in the C++ interface.
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
