"unused variable" warning for variable used by typclass inference

[andres-erbsen]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

class Foo
def bar [Foo] := 0
def baz := let x := Foo.mk; bar -- unused variable `x`
def baz':=                  bar -- failed to synthesize instance of type class Foo

Expected behavior: Either both variants of baz fail to compile or the first one doesn't warn.

Actual behavior: Misleading warning on first baz

Versions

d3b0487