`variable` is not hygienic

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

I'm not sure how to describe this one, beyond showing some variations.

Steps to Reproduce

This one has an error that shouldn't be there on the variable line, and a missing error on def G.CC:

class C (V : Type) where
  n : Nat
  m : Nat

structure F (V : Type) [C V]

variable {V : Type} [C V] -- failed to synthesize instance _root_.C ?m.152

def G.C : C (F V) where
  n := 5
  m := 7

def G.CC : C (F V) where
  n := 5
  -- No error about missing field!

Commenting out G.CC makes the error on the variable line disappear.

Changing G.CC to H.CC makes the error on the variable line disappear, and the error about the missing field reappear.

Versions

Lean (version 4.0.0-nightly-2022-11-21, commit 1b73fa3fa1f6, Release)

Additional Information

This is obstructing my attempts to port category theory in Lean 4. (Actually, it's breaking my attempts to provide a #mwe for a different bug encountered there!)

Start by running the self-contained Lean reproduction in the issue and compare the diagnostics on the variable, def G.C, and def G.CC declarations, including the H.CC variation. Investigate the compiler's handling of hygiene and name resolution; done means the spurious instance error disappears and the missing-field error is reported consistently.