fix: ensure field names are atomic

src/Lean/Elab/Structure.lean

@@ -207,7 +207,9 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
           pure (some optBinderTacticDefault[0][1])
     let idents := fieldBinder[2].getArgs
     idents.foldlM (init := views) fun (views : Array StructFieldView) ident => withRef ident do
-      let name     := ident.getId
+      let name := ident.getId.eraseMacroScopes
+      unless name.isAtomic do
+        throwErrorAt ident "invalid field name '{name.eraseMacroScopes}', field names must be atomic"
       let declName := structDeclName ++ name
       let declName ← applyVisibility fieldModifiers.visibility declName
       addDocString' declName fieldModifiers.docString?

tests/lean/nonAtomicFieldName.lean

@@ -0,0 +1,2 @@
+structure A where
+  a.b : Nat

tests/lean/nonAtomicFieldName.lean.expected.out

@@ -0,0 +1 @@
+nonAtomicFieldName.lean:2:2-2:5: error: invalid field name 'a.b', field names must be atomic