diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 9528eea8d0..c90c79ea84 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -1149,7 +1149,7 @@ private partial def mkBaseProjections (baseStructName : Name) (structName : Name private def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := do if baseName == `Function then return (← whnfR type).isForall - else if type.consumeMData.isAppOf baseName then + else if type.cleanupAnnotations.isAppOf baseName then return true else return (← whnfR type).isAppOf baseName diff --git a/tests/lean/run/3745.lean b/tests/lean/run/3745.lean new file mode 100644 index 0000000000..eff827f09c --- /dev/null +++ b/tests/lean/run/3745.lean @@ -0,0 +1,31 @@ +/-! +# Issue 3745 + +Field notation for abbreviations would fail if the argument for field notation was an optional parameter. +-/ + +structure A + +abbrev B := A + +def A.x (_ : A) := 1 +def B.x (_ : B) := 2 + +def A.y (_ : A) := 1 +def B.y (_ : B := {}) := 2 + +/-! +These were OK before the fix. +-/ +/-- info: 1 -/ +#guard_msgs in #eval (show A from {}).x +/-- info: 2 -/ +#guard_msgs in #eval (show B from {}).x + +/-! +The second of these failed before the fix. +-/ +/-- info: 1 -/ +#guard_msgs in #eval (show A from {}).y +/-- info: 2 -/ +#guard_msgs in #eval (show B from {}).y