# Zulip Chat Archive

## Stream: general

### Topic: Type inference

#### Bolton Bailey (Nov 21 2022 at 12:42):

With this code

```
import data.mv_polynomial.basic
lemma mwe {F : Type} [field F] {cols rows : ℕ}
(constraint : mv_polynomial (fin cols × fin rows) F)
(trace : fin cols -> fin rows -> F) :
mv_polynomial.eval (λ row_col , trace (row_col.fst) (row_col.snd)) constraint = 0
:= sorry
```

I get the following tooltips on `row_col`

:

```
row_col : fin cols × fin rows
```

and then

```
invalid field notation, type is not of the form (C ...) where C is a constant
row_col
has type
?m_1Lean
```

And the code

```
import data.mv_polynomial.basic
lemma mwe {F : Type} [field F] {cols rows : ℕ}
(constraint : mv_polynomial (fin cols × fin rows) F)
(trace : fin cols -> fin rows -> F) :
mv_polynomial.eval (λ row_col : (fin cols × fin rows), trace (row_col.fst) (row_col.snd)) constraint = 0
:= sorry
```

works fine. Why is VSCode smart enough to tell me the type of `row_col`

, but Lean apparently needs to be told it?

#### Kyle Miller (Nov 21 2022 at 12:53):

I'm going to guess it has to do with elaboration order and the fact that lean will continue elaborating despite errors. It's able to eventually figure out that `row_col`

has the type it does because it comes from the `constraint`

argument, but Lean visits arguments to functions in left-to-right order, so when it's handling dot/field notation it does not yet know the type of `row_col`

.

#### Kyle Miller (Nov 21 2022 at 12:55):

Flipping the argument order fixes it:

```
noncomputable
def mv_polynomial.eval' {R : Type*} {σ : Type*} [comm_semiring R] (p : mv_polynomial σ R) (f : σ → R) : R :=
mv_polynomial.eval f p
lemma mwe {F : Type} [field F] {cols rows : ℕ}
(constraint : mv_polynomial (fin cols × fin rows) F)
(trace : fin cols -> fin rows -> F) :
mv_polynomial.eval' constraint (λ row_col , trace (row_col.fst) (row_col.snd)) = 0
:= sorry
```

#### Eric Wieser (Nov 21 2022 at 13:03):

Inserting a `by exact`

might also change the elaboration order to the one that works

#### Kyle Miller (Nov 21 2022 at 13:08):

Not here, lambda expression bodies process all pending tactics

#### Eric Wieser (Nov 21 2022 at 13:09):

Works for me:

```
import data.mv_polynomial
lemma mwe {F : Type} [field F] {cols rows : ℕ}
(constraint : mv_polynomial (fin cols × fin rows) F)
(trace : fin cols -> fin rows -> F) :
mv_polynomial.eval (by exact λ row_col , trace (row_col.fst) (row_col.snd)) constraint = 0
:= sorry
```

#### Kyle Miller (Nov 21 2022 at 14:24):

Oh, I thought you meant *inside* the lambda. Your example working is consistent with the theory that elaboration of lambda bodies triggers the processing of pending tactic blocks.

#### Eric Wieser (Nov 21 2022 at 14:28):

I don't think it gives any evidence for that theory, the lambda doesn't even exist until the tactic block is execute there.

#### Kyle Miller (Nov 21 2022 at 14:51):

This is what I'm referring to: https://github.com/leanprover-community/lean/blob/master/src/frontends/lean/elaborator.cpp#L3404

#### Kyle Miller (Nov 21 2022 at 14:52):

The previous five lines visit the body of the lambda, and `synthesize()`

is for handling a number of deferred things, including pending tactics.

Last updated: Dec 20 2023 at 11:08 UTC