function expected

Stream: general

[Johan Commelin]

Is there any chance we can do something about errors like this?

function expected at
  aeval ℚ (mv_polynomial (idx × ℕ) ℚ) (witt_structure_rat p Φ)
term has type
  mv_polynomial ℕ ℚ →ₐ[ℚ] mv_polynomial (idx × ℕ) ℚ

Lean has correctly figured out the type... but by the time it didit's too late to check whether we can coerce to a function (if I understand the problem correctly). Maybe we can teach lean that there are second chances?

[Reid Barton]

Are you sure there aren't any funny metavariables lurking beneath the surface?

[Johan Commelin]

There are

[Johan Commelin]

But I want lean to not care about them, because it clearly figured out enough info to print this error message, and hence it should also be able to figure out the function.

[Reid Barton]

Oh, but then this is just the usual problem with coercions to function.

[Reid Barton]

Yes, maybe we should think about doing something about it.

[Johan Commelin]

Yes, I know. Maybe I should have explained better.

[Johan Commelin]

At the moment, this statement works... but I don't think it's very readable

theorem witt_structure_rat_prop (Φ : mv_polynomial idx ℚ) (n : ℕ) :
  (aeval ℚ (mv_polynomial (idx × ℕ) ℚ) (witt_structure_rat p Φ) :
    _ → (mv_polynomial (idx × ℕ) ℚ)) (witt_polynomial p n) =
  (aeval ℚ (mv_polynomial (idx × ℕ) ℚ)
    (λ b : idx, ((witt_polynomial p n).rename (λ i : ℕ, (b,i)))) :
     _ → (mv_polynomial (idx × ℕ) ℚ)) Φ :=

[Reid Barton]

My understanding is that currently Lean refuses to even consider the possibility of applying a coercion to function when the type in question contains metavariables. I think changing the behavior of instance search as discussed at #general > unusable arguments is a prerequisite for changing this.

[Yury G. Kudryashov]

Why this is a prerequisite? @Gabriel Ebner is it hard to do the following?

• catch "function expected" error,
• try to fill class instance metavariables using instance search,
• if succeeded, try has_coe_to_fun?

[Gabriel Ebner]

That's what we do right now?

[Gabriel Ebner]

It's just that instance search doesn't work (for no good reason) if the type contains metavariables.

[Reid Barton]

I'm not sure there is no good reason, but I also don't remember the exact supposed reason.

[Gabriel Ebner]

lean#251 ?

[Sebastian Ullrich]

Allowing mvars in the input problem sounds like a bad idea when you have overlapping instances. You really don't want to get a different solution when the elaborator hasn't resolved quite as many arguments as in a similar context.

[Gabriel Ebner]

Overlapping instances are always bad. We're actively removing them from mathlib.

[Gabriel Ebner]

There's little difference in doing type class resolution in a polymorphic declaration and then instantiating the polymorphic declaration, or doing typeclass resolution where the type contains a metavariable.

[Reid Barton]

Right, this is a good way to look at it.

[Gabriel Ebner]

Maybe I should clarify: overlapping instances are ok if they are definitionally equal. But they cause huge problems if they aren't.

[Reid Barton]

In GHC type variables that are bound by the type signature of a polymorphic function are called "rigid type variables", and we should think of metavariables in instance search problems as "rigid" too.

[Reid Barton]

At least, certainly the ones which existed prior to instance search. I'm still not entirely sure what Lean 3 implements.

[Gabriel Ebner]

From what you describe: rigid = regular.

[Gabriel Ebner]

That is, exactly what lean#251 implements.

[Reid Barton]

As opposed to temporary?

[Sebastian Ullrich]

Gabriel Ebner said:

There's little difference in doing type class resolution in a polymorphic declaration and then instantiating the polymorphic declaration, or doing typeclass resolution where the type contains a metavariable.

Sure, but I haven't heard of any issues yet where the elaborator applies an unexpected degree of polymorphism. Instanciveness of mvars is super-brittle on the other hand.

[Reid Barton]

Anyways, the test looks good! You could also backport https://github.com/leanprover/lean4/blob/master/tests/elabissues/Reid1.lean but it looks essentially the same. I suspect we won't run into issues in practice, because our has_coe_to_fun instances are (mostly?) for type constructors applied to a bunch of variables, and so don't involve further matching. (We must already have determined the outermost type constructor of e to get to this point, so that we know it's not ->, right?)

[Gabriel Ebner]

By polymorphic I mean def foo {α} := ... synthesize `has_one (α × α)` here .... Sure, in a small example the user has a bit more control in the sense that we search for has_one (α × α) and not has_one β. But over a large library, some definition will very likely infer the type class in the most general setting imaginable.

[Reid Barton]

I really hope this works in practice! :fingers_crossed: This would be way more exciting than a lousy 2x speed increase :upside_down:

[Gabriel Ebner]

Ok, I'll build mathlib with the change and see what happens.

[Yury G. Kudryashov]

I tried to drop some of : _ → _ and failed.

[Johan Commelin]

Where?

[Yury G. Kudryashov]

More precisely, I tried to drop : _ → _ in line 405 of group_theory/free_monoid_product in the free_monoid_prod branch.

[Yury G. Kudryashov]

Sorry for not using master for the test.

[Reid Barton]

I think the test is not whether you can drop : _ → _, but whether you can replace arguments to things that will be coerced to functions by _s.

[Reid Barton]

Then we can go and make those arguments implicit.

[Yury G. Kudryashov]

The reason for making them explicit is that otherwise you'll need : _ → _ everywhere.

[Yury G. Kudryashov]

And the problem is that the missing argument in my case is [decidable_eq _].

[Reid Barton]

In my experience even adding that : _ → _ is not enough

[Yury G. Kudryashov]

Sorry, I meant : α → β with full types for α and β.

[Yury G. Kudryashov]

With pp.all I get the following error:

function expected at
  @free_monoid_product.normalized.of.{u_1 u_2} ι M (λ (i : ι), _inst_1 i) ?m_1
    (λ (i : ι) (a b : M i), _inst_3 i a b)
    (@sigma.fst.{u_1 u_2} ι
       (λ (i : ι),
          @subtype.{u_2+1} (M i)
            (λ (x : M i), @ne.{u_2+1} (M i) x (@has_one.one.{u_2} (M i) (@monoid.to_has_one.{u_2} (M i) (_inst_1 i)))))
       a)
term has type
  @monoid_hom.{u_2 (max u_1 u_2)}
    (M
       (@sigma.fst.{u_1 u_2} ι
          (λ (i : ι),
             @subtype.{u_2+1} (M i)
               (λ (x : M i),
                  @ne.{u_2+1} (M i) x (@has_one.one.{u_2} (M i) (@monoid.to_has_one.{u_2} (M i) (_inst_1 i)))))
          a))
    (@free_monoid_product.normalized.{u_1 u_2} ι M (λ (i : ι), (λ (i : ι), _inst_1 i) i))
    ((λ (i : ι), _inst_1 i)
       (@sigma.fst.{u_1 u_2} ι
          (λ (i : ι),
             @subtype.{u_2+1} (M i)
               (λ (x : M i),
                  @ne.{u_2+1} (M i) x (@has_one.one.{u_2} (M i) (@monoid.to_has_one.{u_2} (M i) (_inst_1 i)))))
          a))
    (@free_monoid_product.normalized.monoid.{u_1 u_2} ι M (λ (i : ι), (λ (i : ι), _inst_1 i) i)
       (λ (a b : ι), ?m_1 a b)
       (λ (i : ι) (a b : M i), (λ (i : ι) (a b : M i), _inst_3 i a b) i a b))

[Reid Barton]

But even this is not enough! Since the problem is exactly that it fails to infer metavariables of e in e x from the expected type of e as a function.

[Reid Barton]

It needs to be, for example, (e : equiv a b) x.

[Gabriel Ebner]

@Yury G. Kudryashov Works for me:

lemma cons_eq_of_mul (a) (xs : normalized M) :
  cons a xs = of M a.1 a.2 * xs :=
by { simp only [of_eq_of', of'_val, sigma.eta], refl }

[Gabriel Ebner]

You can also remove fancier arrows:

@[ext] lemma hom_eq ⦃f g : normalized M →* N⦄
  (h : ∀ i x, f (of M i x) = g (of M i x)) :
  f = g :

[Gabriel Ebner]

Or make some arguments implicit:

@[simp] lemma lift_of (f : Π i, M i →* N) (i : ι) (x : M i) :
  lift _ _ f (of _ _ x) = f _ x :=

[Yury G. Kudryashov]

Sorry, I created a branch but didn't switch to it.

[Yury G. Kudryashov]

Rebuilding

[Gabriel Ebner]

Just to make this clear: this is with lean#251

[Patrick Massot]

@Sebastian Ullrich You should hurry up with Lean 4, because Gabriel is solving all issues of Lean 3 without waiting.

[Yury G. Kudryashov]

It works!!

[Johan Commelin]

This is really cool! As in: :cool:

[Yury G. Kudryashov]

Now it's time for me to come back to polynomials review...

[Johan Commelin]

But I'm getting headaches of the looming mv_polynomial refactor that is waiting for us now that we can have readable ring_hom versions of C, eval, eval\2, map, rename, and all the other friends

[Johan Commelin]

Hah, great minds think alike... (fools never differ...)

[Johan Commelin]

It's really crazy how big the difference is between lean 3.11 (last week) and lean 3.14 (yesterday)