Matching on a constructor that takes an instance argument using swift notation wrongfully tries to synthesize the instance

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

Matching on a .constructor that takes an instance argument wrongfully attempts to synthesize the instance.
When trying to match on a value of an inductive type that has a constructor taking an instance argument, Lean tries to synthesize the instance in the dot pattern, while it doesn't need to. The instance should be brought in scope in the corresponding branch, as it is contained in the value being matched on, but it doesn't make sense to synthesize the instance in the pattern itself.
Note that replacing the dot notation (.ctor) with a qualified constructor (Foo.ctor) or a bare constructor (open Foo then matching on ctor) fixes the issue.

Context

I was trying to reproduce something similar to Trees that Grow/Coq à la Carte to have an extensible inductive type, but using typeclasses to avoid syntactic overhead.

Steps to Reproduce

class Foo where

inductive Bar where
  | bar : [Foo] → Bar

example : Bar → True
  | .bar => .intro
/-  ^^^^
test.lean:7:4: error: failed to synthesize instance
  Foo
-/

-- works
example : Bar → True
  | Bar.bar => .intro

-- works
open Bar
example : Bar → True
  | bar => .intro

Expected behavior: Same as Bar.bar or open Bar then bar, i.e. bring the Foo instance in scope and don't try to synthesize the Foo instance in the pattern.

Actual behavior: Lean tries to synthesize the instance while it doesn't need to.

Versions

• Lean (version 4.0.0-nightly-2023-06-10, commit bff612e59e48, Release)
• Lean master at the time of writing this issue
• Linux 5.15.111 # 1-NixOS SMP Thu May 11 14:00:40 UTC 2023 x86_64 GNU/Linux

Impact

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

Fixing the bug

Trying to find the origin of the bug, grepping for dotIdent in the entire codebase only shows up four occurrences, only 1 being relevant from what I can tell: https://github.com/leanprover/lean4/blob/89b65c8f1d6fa7700d73f1bc12db0b140c728e32/src/Lean/Elab/PatternVar.lean#L216-L227

Start with the minimal reproducer in the issue and inspect src/Lean/Elab/PatternVar.lean around lines 216–227, the relevant dotIdent occurrence identified by the report. Run the example with the dot-pattern and qualified constructor forms. Done means the dot form no longer tries to synthesize Foo and behaves like the working forms.