unknown local constant: _ffresh.0

Stream: general

[Scott Morrison]

Has anyone seen an otherwise successful def error with unknown local constant: _ffresh.0?

[Simon Hudon]

do you use variable or parameter? Do you use include?

[Scott Morrison]

Yes to all of the above. :-) Changing the name of an argument of the function solved the problem.... Looks bug-ish to me, but I don't have time to minimise now so will proceed with slightly strange argument names!

[Simon Hudon]

you probably have variable x, assumption h mentioning x, include h and then you declare x as an argument to your definition

[Simon Hudon]

Lean does not include the variable but includes h

[Andrew Yang]

Has anyone else seen this error? I tried renaming the variables but the error still persists.
A #mwe :

import topology.sheaves.stalks

open topological_space opposite category_theory

universes v u w

namespace Top

namespace presheaf

variables {X : Top.{w}} {C : Type u} [category.{v} C] [concrete_category C]

local attribute [instance] concrete_category.has_coe_to_sort

structure submonoid_presheaf [∀ X : C, mul_one_class X]
  [∀ (X Y : C), monoid_hom_class (X ⟶ Y) X Y] (F : X.presheaf C).

def localization {F : X.presheaf CommRing.{w}} (G : F.submonoid_presheaf) :
  X.presheaf CommRing := sorry

end presheaf

end Top

[Kevin Buzzard]

The error for me is

unknown local constant: 0._fresh.771.40

As far as I'm concerned this is a new error, so you get a point. Congratulations!

[Eric Wieser]

What about the one from 2019 upthread?

[Kevin Buzzard]

oh darn it

[Junyan Xu]

@Andrew Yang G : @submonoid_presheaf _ CommRing _ _ _ _ F works.

[Andrew Yang]

It also works if I use variables {F : X.presheaf CommRing.{w}} (G : F.submonoid_presheaf) instead.
I have no idea why though.