Typeclass inference completely fails if a term has a `let`

Stream: lean4

[Eric Rodriguez]

#mwe:

class Foo (R : Type) where
  a : R → R

class Bar (R : Type) extends Foo R where
  b : R → R

theorem amazing_lemma (R) [Bar R] : 4 = 4 := rfl

example (R) [Foo R] : False := by
  let s := by let x : R → R := Foo.a; exact Bar.mk x
  have := amazing_lemma R

amazing_lemma fails; it complains we lack a Bar R instance even though we just constructed it.

[Eric Rodriguez]

These can be changed to your favourite combination of have(I) and let(I)to have the exact same issue.

[Eric Rodriguez]

if you then repeat the instance with something like let e := s, then stuff will work again.

[Eric Wieser]

This is almost certainly a caching bug; even letI fails:

import Std

class Foo (R : Type) where
  a : R → R

class Bar (R : Type) extends Foo R where
  b : R → R

theorem amazing_lemma (R) [Bar R] : 4 = 4 := rfl

example (R) [Foo R] : False := by
  let s := by letI x : R → R := Foo.a; exact Bar.mk x
  -- let s' := Bar.mk (Foo.a : R → R)
  have := amazing_lemma R

[Eric Wieser]

(the goal view is indistinguishable between the s and s' case

[Eric Wieser]

Adding let s' : Bar R := s to your original example fixes it

[Eric Rodriguez]

OK, I think I've found the root cause, with another example:

class Foo (R : Type) where
  a : R → R

theorem amazing_lemma (R) [Foo R] : 4 = 4 := rfl

example (R S) [f : Foo R] (h : R = S) : False := by
  let s := h ▸ f
  have := amazing_lemma S

This similarly fails; however, if I say s : Foo S := ..., then stuff works. I think as Lean doesn't know the expected type, and doesn't expect it to be a class, the cache is not reset

[Eric Rodriguez]

For my applications, this is somewhat easy to work around, thankfully, but it is a bizarre issue when first found.

[Eric Wieser]

That sounds exactly like the problem

[Eric Wieser]

Qq also fails a lot of the time on let v := where it succeeds on let v : t :=

[Kevin Buzzard]

Is it worth opening an issue?

[Eric Wieser]

@Eric Rodriguez, you managed to make an even smaller mwe, right? Can you open an issue with that?

[Eric Rodriguez]

Yeah, I'll post it late tonight :)

[Eric Rodriguez]

lean4#2696