Elaborating the type of a constant

Stream: new members

[Bolton Bailey]

Hello, something came up in my project that confused me, so I thought I would post it here. The MWE is

universes u

variables {F : Type u}
variables [field F]


constants n_foo n_bar : ℕ

constant u_foo : vector (polynomial F) n_foo
constant u_bar : vector (polynomial F) n_bar

constant a_foo : vector F n_foo

def my_property (a_bar : vector F n_bar) :
    ((vector.map₂ has_scalar.smul a_bar u_bar).to_list.sum + (vector.map₂ has_scalar.smul a_foo u_foo).to_list.sum)
    = 0
:=
sorry

This code complains of "don't know how to synthesize placeholder" on a_foo and u_foo. It gets fixed by elaborating the type of a_foo and u_foo

import data.mv_polynomial.basic
import data.polynomial.div




universes u

variables {F : Type u}
variables [field F]


constants n_foo n_bar : ℕ

constant u_foo : vector (polynomial F) n_foo
constant u_bar : vector (polynomial F) n_bar

constant a_foo : vector F n_foo

def my_property (a_bar : vector F n_bar) :
    ((vector.map₂ has_scalar.smul a_bar u_bar).to_list.sum + (vector.map₂ has_scalar.smul (a_foo : vector F n_foo) (u_foo : vector (polynomial F) n_foo)).to_list.sum)
    = 0
:=
sorry

This latter code has no errors. But I can't figure out why it is necessary to elaborate the type when it's specified right on line 20.

[Reid Barton]

The constants u_foo, etc. depend on the variable F, which might not mean what you think.
I would recommend not using constant at all.

[Eric Wieser]

@u_foo F _ would be shorter than the type annotations

[Reid Barton]

What's going on is slightly complicated but the basic issue is you have effectively a separate constant u_foo for each field