From 39ce3044ec65db2dc0da7a4c9ce5ae3e1250e655 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 Aug 2021 20:56:20 -0700
Subject: [PATCH] feat: emit warning message when failed to copy default value

---
 src/Lean/Elab/Structure.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 23797b79a8..1f3813044c 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -381,19 +381,23 @@ private partial def copyDefaultValue? (fieldMap : FieldMap) (expandedStructNames
     let us ← mkFreshLevelMVarsFor cinfo
     go? (cinfo.instantiateValueLevelParams us)
 where
+  failed : TermElabM (Option Expr) := do
+    logWarning s!"ignoring default value for field '{fieldName}' defined at '{structName}'"
+    return none
+
   go? (e : Expr) : TermElabM (Option Expr) := do
     match e with
     | Expr.lam n d b c =>
       if c.binderInfo.isExplicit then
         let fieldName := n
         match fieldMap.find? n with
-        | none     => return none -- TODO Generate warning?
+        | none => failed
         | some val =>
           let valType ← inferType val
           if (← isDefEq valType d) then
             go? (b.instantiate1 val)
           else
-            return none -- TODO Generate warning?
+            failed
       else
         let arg ← mkFreshExprMVar d
         go? (b.instantiate1 arg)