elaboration issue involving powers and sums

Stream: mathlib4

[Floris van Doorn]

The new elaborators of +, *, ^ work very well. I just encountered an example where it still got confused.
Here is a MWE:

import Mathlib.Algebra.BigOperators.Basic

open BigOperators

example (x : ℕ) (y : ℤ) (s : Finset ℕ) :
  x = ∑ _k in s, y * (x ^ 2 /-: ℕ-/ /-: ℤ-/) := by sorry
-- elaboration error. It works when adding either coercion around the power
-- the error still occurs when replacing x ^ 2 by y ^ 2

[Floris van Doorn]

@Kyle Miller

[Yaël Dillies]

Yes, ∑ is not currently considered an arithmetic operator

[Kyle Miller]

This is a big open question in the expression tree elaborator. Right now, there's no way for anything other than simple arithmetic operations to participate in the coercion calculation.

We could perhaps develop a bigop% node to handle these sorts of expressions, to let the types propagate into and out of the body of a sum. But, adding operator types like this one at a time makes me worry that this expression tree elaborator will start to subsume all of elaboration.

I've been wondering if elaboration needs a more sophisticated bidirectional protocol. The current setup is that the Syntax is recursively traversed to produce an Expr, and an expected type is propagated toward the leaves. (With the extra complication that elaboration problems can also defer processing by elaborating to a metavariable and registering some code to be run later.) Expected types are just a suggestion, and elaborators do not need to respect them.

What could happen is that there be two phases, one that recursively traverses expressions to propagate expected types and then collect actual types (or at least what's likely going to be the actual type) and then another that then actually elaborates using this collected information.

With x = ∑ _k in s, y * x ^ 2, the way it could work is that = does the first phase for both sides, discovering that the LHS is Nat and the RHS is Int. Since it's using the expression tree elaborator, it computes that everything coerces to Int, so commits to Int for both sides.

[Kyle Miller]

Here are two fixes for your original example by the way:

example (x : ℕ) (y : ℤ) (s : Finset ℕ) :
  (x : ℤ) = ∑ _k in s, y * x ^ 2 := by sorry

example (x : ℕ) (y : ℤ) (s : Finset ℕ) :
  x = (∑ _k in s, y * x ^ 2 :) := by sorry

For some reason ∑ _k in s, y * x ^ 2 doesn't realize it's an Int in time for elaboration of Eq. It might be a bug in the expression tree elaborator, I'll have to check...

[Kyle Miller]

Minimized:

/--
error: failed to synthesize instance
  HMul Int Int Nat
-/
#guard_msgs in
example (x : Nat) (y : Int) :
  x = id (y * x ^ 2) := sorry

-- Succeeds
example (x : Nat) (y : Int) :
  x = id (y * x ^ 2 :) := sorry

-- Succeeds
example (x : Nat) (y : Int) :
  x = id (y * x ^ 2 : Int) := sorry

-- Succeeds
example (x : Nat) (y : Int) :
  (x : Int) = id (y * x ^ 2) := sorry

[Yaël Dillies]

Kyle Miller said:

I've been wondering if elaboration needs a more sophisticated bidirectional protocol. The current setup is that the Syntax is recursively traversed to produce an Expr, and an expected type is propagated toward the leaves. (With the extra complication that elaboration problems can also defer processing by elaborating to a metavariable and registering some code to be run later.)

Also recall that I have complained (and Mario agreed) that there is only one "post-defer" point, rather than several. It is a big complication in #11582 because overriding the Set builder notation with a Finset builder that waits for the type to be available makes the overriden Set notation also wait for the type, which causes elaboration failures.

[Kyle Miller]

My understanding so far is that it should be considered to be a bug in how ^ is handled.

The issue is that it's deferring deciding which ^ to use until much later than it needs to. The following works, since it causes ^ to specialize.

example (x : Nat) (y : Int) :
  x = id (y * x ^ (2 : Nat)) := sorry

[Kyle Miller]

I think I have a fix for this in lean4#4215. The issue is that when the expression tree elaborator constructs the expression at the end of elaboration, it doesn't record the computed "max type" in the operators. So for example, while it decides that y * x ^ 2 should be an Int, it was just remembering that the HMul is Int -> ?_ -> ?_ since the x ^ 2 hasn't resolved its instance yet. With this PR, it specializes HMul to Int -> Int -> Int. That then causes the elaborator for = to see that the RHS is an Int, and then it all works.

Hopefully it's not premature saying that this is actually a fix. I'm still waiting on mathlib to compile :fingers_crossed:

[Kyle Miller]

This now works with lean4#4215:

example (x : ℕ) (y : ℤ) (s : Finset ℕ) :
    x = ∑ _k in s, y * x ^ 2 := by
  -- ⊢ ↑x = ∑ _k ∈ s, y * ↑x ^ 2
  sorry

The rule is now: if all the leaf terms have known types and they can all be coerced to the same type, then the entire arithmetic expression is made to have that type. In this case, y * x ^ 2 has leaf terms y and x, they both have known types (Int and Nat), they're both coerceable to Int, so, in the end, the HMul instance is HMul Int ?_ Int rather than HMul Int ?_ ?_.