Possible bug in typeclass search with inferred types

Stream: lean4

[Sven Manthe]

Edit: Now I have a minimal working example

class D where
def h (_ : D) := 0
theorem heq x : h x = h (by
  --have _ := x
  infer_instance) := rfl

Adding the commented line or specifying the type of the hypothesis x makes the typeclass inference work, but currently it fails. This is confusing since the proof state window in VS code still shows that x has type D.

The inferior old version, just for reference:
A small (although depending on parts of Mathlib) example is

import Mathlib.Tactic
open CategoryTheory

def C := Type*
instance : Category C := inferInstanceAs (Category Type*)

variable {S T U : C} (f : S ⟶ T) (g : T ⟶ U)
noncomputable def pInv (y : T) (_ : IsIso f) : S := inv f y

theorem pInv_comp (hg : _) (hf : IsIso f) :
  pInv (f ≫ g) y (by
    --have hg' := hg
    infer_instance)
  = pInv f (pInv g y hg) hf := by
  sorry

Currently infer_instance fails. Providing the type hg : IsIso g explicitly, or adding the commented line, fixes this.
Is this intended behavior?

[Kevin Buzzard]

I think that writing (hg : _) and expecting things to work is probably not intended behaviour :-) but I do see your point; somehow the type of hg can be inferred by the time we've got to pInv f... but perhaps typeclass inference wants to run on the LHS first? before unification has run or something?

[Sven Manthe]

Oh, I missed that before. The confusing thing is that the "Tactic state" window in the above example before the infer_instance shows hg : IsIso g; so in some sense the informations available to this window seem to be different to the ones available to typeclass search. Also, replacing pInv g y hg by pInv g y (hg : IsIso g) doesn't fix the issue. And that have hg' := hg helps still feels weird to me...

[Sven Manthe]

Today I discussed the issue with @Floris van Doorn. My current understanding: There is a typeclass cache, which gets updated by let/have, causing infer_instance only to work afterward. Thus, I won't report a bug. Nonetheless, if my understanding is correct, it may be more intuitive (and would at least resolve my original problem) if the tactic "infer_instance" updated this cache before running "exact inferInstance".
PS: I seemingly cannot mark this as resolved; feel free to do so

[Jovan Gerbscheid]

I don't think it has anything to do with type class cache. The line have _x := x adds another local variable _x, and because it knows the type of _x, it figures out _x is an instance. But looking at the trace, I see that it still doesn't recognize x as an instance. I think the issue is that Lean only checks once whether a local variable is an instance or not, which is at the moment that it adds the variable to the context. And here it figures out the type of x later than that.