Type inference

Stream: general

[Bolton Bailey]

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]

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]

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]

Inserting a by exact might also change the elaboration order to the one that works

[Kyle Miller]

Not here, lambda expression bodies process all pending tactics

[Eric Wieser]

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]

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]

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]

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

[Kyle Miller]

The previous five lines visit the body of the lambda, and synthesize() is for handling a number of deferred things, including pending tactics.