As described at issue #1760, the new error message is:
```
1760.lean:6:18: error: type mismatch at application
f x
term
x
has type
big_type : Type 1
but is expected to have type
?m_1 : Type
```
Remarks:
- Some tests do not produce error messages anymore because they can be
processed using the new equation compiler preprocessor.
- Some error messages got worse because of the preprocessing step.
We use metavariables in the preprocessing step. This information
may "leak" to users. Another problem is that some variable names
are lost. Example: in the following definition
def to_nat : ∀ {n}, fi n → nat
| (succ n) f0 := 0
| (succ n) (fs i) := succ (to_nat i)
The preprocessing step uses metavariables for pattern variables.
Thus, we have
def to_nat : ∀ {n}, fi n → nat
| (succ ?n) (@f0 ?x) := 0
| (succ ?n) (@fs ?x ?i) := succ (to_nat i)
when solving the constraint `succ ?n =?= succ ?x`, Lean assigns
?n := ?x
after solving these constraints, the preprocessor converts
metavariables into pattern variables again, and we have
def to_nat : ∀ {n}, fi n → nat
| (succ x) (@f0 x) := 0
| (succ x) (@fs x i) := succ (to_nat i)
So, we get the following equation lemmas:
to_nat.equations._eqn_1 : ∀ (x : ℕ), @to_nat (succ x) (@f0 x) = 0
to_nat.equations._eqn_2 : ∀ (x : ℕ) (i : fi x), @to_nat (succ x) (@fs x i) = succ (@to_nat x i)
instead of
to_nat.equations._eqn_1 : ∀ (n : ℕ), @to_nat (succ n) (@f0 n) = 0
to_nat.equations._eqn_2 : ∀ (n : ℕ) (i : fi n), @to_nat (succ n) (@fs n i) = succ (@to_nat n i)
@kha I'm trying to improve the equation compiler. I have added a
preprocessing step, and got the following wierd output when testing
tests/lean/interactive/info_goal.lean
```
> {"record":{"doc":"This tactic applies to any goal. It gives directly the exact proof\nterm of the goal. Let `T` be our goal, let `p` be a term of type `U` then\n`exact p` succeeds iff `T` and `U` are definitionally equal.","source":,"state":"⊢ ℕ → ℕ","tactic_params":["<error while executing interactive.param_desc: don't know how to pretty print lean.parser.pexpr 2>"],"text":"exact","type":"interactive.parse interactive.types.texpr → tactic unit"},"response":"ok","seq_num":4}
```
The problem seems to be the pattern
`(parser.pexpr)
which is sugar for
`(parser.pexpr std.prec.max)
and will not match `(pexpr 2)`
So, I fixed it by replacing the pattern with `(parser.pexpr %%v).
However, it is not clear to me why it was working before.
Any ideas?
To make the equation compiler more convenient to use, we will add a
couple of preprocessing steps.
This commit adds the first one of them. In this step, we use
type inference to refine pattern variables, and we relax the
restrictions on inaccessible annotations.
We will also add a preprocessing step that implements the "complete
transition" step before we execute the elim_match step.
Reason: vector in in init folder was introducing an overload (`::`) for
all Lean users. The workaround (use `local infix ::`) was
counterintuitive.
We currently have no special support for bitvectors in the code
generator. Thus, there is no need to have vector and bitvec in the init
folder right now. Moreover, the new parser and elaborator (issue #1674) should
provide better ways of managing overloaded symbols.
The issue was that instantiate_mvars(infer(m)) had a metavariable, while
infer(instantiate_mvars(m)) did not. Changing the call from assign to
is_def_eq also unifies the type, assigning the metavariable inside the
type.
