Instances don't cache if the expected type isn't known at the time of creation

[ericrbg]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

If the expected type of the expression is not known at the time of adding an expression into the local context. See this example:

class Foo

theorem test [h : Foo] : False := sorry

example : False := by
  have := by exact Foo.mk
  -- have : Foo := by exact Foo.mk
  /- have := by exact Foo.mk
  have := this -/
  exact test

The commented versions all succeed, the un-commented one fails.

Context

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Typeclass.20inference.20completely.20fails.20if.20a.20term.20has.20a.20.60let.60 is my thread about the issue; it has some examples of when the issue originally popped up, for example, when using a let binding to add the issue.

Expected behavior: The instance of Foo being available in the cache.

Actual behavior: The instance of Foo does not appear in the cache.

Versions

Lean (version 4.2.0-rc2, commit f98fb8a, Release)
MacOS Sonoma 14.0

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[Kha]

If the expected type of the expression is not known at the time of adding an expression into the local context

But that is the spec: when a variable is added to the local context, it is registered as an instance if it is a class. Which is not known here, so it isn't registered. There is no caching going on here, it is an eager, one-time decision.