## 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: Aug 03 2023 at 10:10 UTC