Instance cache weirdness

Stream: mathlib4

[Eric Wieser]

In !4#3466, I have a place where I have to write

replace fin : FiniteDimensional _ _ := fin -- porting note: fails without this line

It looks like there's some weirdness going on with the instance cache (if that still exists), because the type of fin before and after that line is unchanged.

[Eric Wieser]

replace fin : _ := fin doesn't work, so it's something to do with the type annotation being present

[Kevin Buzzard]

Is it really unchanged including things like universe metavariables and pp.all etc etc?

[Eric Wieser]

I only tested with pp.explicit; but if I use have instead of replace then I get fin fin : FiniteDimensional K V which I assume means they are really the same type

[Eric Rodriguez]

and does the have instead of replace still solve the issue?

[Eric Wieser]

Yes, have and replace are interchangeable there

[Eric Rodriguez]

Eric Wieser said:

In !4#3466, I have a place where I have to write

replace fin : FiniteDimensional _ _ := fin -- porting note: fails without this line

It looks like there's some weirdness going on with the instance cache (if that still exists), because the type of fin before and after that line is unchanged.

as far as I know, btw, the instance cache does still exist and tactics have to make sure to reset it if needed; however, resetting it after every have and such like is now sound performance-wise.

[Eric Rodriguez]

I see that you use by_cases, I wonder if that's related and it's not been written in this "correct" way

[Eric Rodriguez]

ok, another theory, Lean doesn't realise to reset the instance cache because it's only _defeq_ to a class, not a class itself

[Eric Rodriguez]

there seems to be no way to test this as Lean doesn't allow defs to be classes

[Eric Rodriguez]

Mario Carneiro said:

Eric Wieser said:

Am I imagining that Lean 4 did away with the instance cache and that therefore casesI isn't needed?

Yes to the second part, no to the first. Lean 4 didn't do away with the instance cache, it now effectively calls resetI whenever the local context changes at all. Some internals had to be changed to make this performant enough

this is where I remember this from

[Eric Rodriguez]

Floris van Doorn said:

Together with Kyle Miller I figured out what causes this.

• cases and cases' both call docs#Lean.MVarId.introN
• introN (via introNImp) calls docs4#Lean.Meta.withNewLocalInstances that checks whether certain fvars are classes using two methods isClassQuick? and isClassExpensive?. These two functions both have some support dealing with metavariables, but it makes the wrong decision in certain cases, not recognizing that Foo T is a class in Kyle's latest example. We tested that this fix fixes Kyle's latest example. Is a PR with this change welcome?

And indeed later on in the thread there's a solution given; Adam notices that rcases and obtain don't have this issue. Sorry for all the incidental pings, but it seems that your solution, Eric, will come in a PR that fixes cases/cases'/by_cases, which hasn't come yet

[Eric Rodriguez]

(for now you can use something like obtain fin | fin := Classical.em (FiniteDimensional K V))

[Kevin Buzzard]

Lean 4 didn't do away with the instance cache, it now effectively calls resetI whenever the local context changes at all.

Ironically, in Eric's case the local context doesn't change at all and yet resetI is being called.

[Kyle Miller]

I was just about to mention Floris's message but I see @Eric Rodriguez already mentioned it. It's possible that another workaround is change _ at fin since that will do a revert/intro dance, and intro is what updates the set of local instances.

[Scott Morrison]

change _ at fin doesn't work here.

[Kyle Miller]

Thanks for checking. I tried change FiniteDimensional _ _ at fin too, but what I didn't account for is that this doesn't necessarily change the local variable's actual type expression.

[Kyle Miller]

Re the bug Floris is fixing, we can observe what the issue is with the instance cache. If you add the following tactic:

namespace Mathlib.Tactic
open Lean Parser Tactic Elab Tactic Meta

syntax (name := foo) "foo " term : tactic

elab_rules : tactic | `(tactic| foo $t) => do
  withMainContext <| do
  let t ← Term.elabTerm t none
  let ty ← inferType t
  forallTelescopeReducing ty fun _ ty =>
    logInfo m!"term is {toString ty}"

end Mathlib.Tactic

then if you do foo fin after the by_cases fin : FiniteDimensional K V line, you see a metavariable. This tactic is reproducing some of the code for the instance class computation, and it expects to see an application, not a metavariable, because it forgets to expand metavariables here.

[Kyle Miller]

On the other hand, if you do

    replace fin : FiniteDimensional _ _ := fin
    foo fin

you see that now fin is no longer a metavariable, and the instance cache computation sees that fin is an application involving FiniteDimensional.