From 7720b843bb159d468a057fef69add0ceba42e882 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 23 Dec 2020 08:12:29 -0800
Subject: [PATCH] feat: allow users to use binders when setting default value
 for parent fields

---
 src/Lean/Elab/Structure.lean | 16 ++++++++++------
 tests/lean/run/struct3.lean  | 22 ++++++++++++----------
 2 files changed, 22 insertions(+), 16 deletions(-)

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 43beb3c182..a451876873 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -300,12 +300,16 @@ private partial def withFields
         match view.value? with
         | none       => throwError! "field '{view.name}' has been declared in parent structure"
         | some valStx => do
-          if !view.binders.getArgs.isEmpty || view.type?.isSome then
-            throwErrorAt! view.ref "omit field '{view.name}' type to set default value"
-          let fvarType ← inferType info.fvar
-          let value ← Term.elabTermEnsuringType valStx fvarType
-          let infos := infos.push { info with value? := value }
-          withFields views (i+1) infos k
+          if let some type := view.type? then
+            throwErrorAt! type "omit field '{view.name}' type to set default value"
+          else
+            let mut valStx := valStx
+            if view.binders.getArgs.size > 0 then
+              valStx ← `(fun $(view.binders.getArgs)* => $valStx:term)
+            let fvarType ← inferType info.fvar
+            let value ← Term.elabTermEnsuringType valStx fvarType
+            let infos := infos.push { info with value? := value }
+            withFields views (i+1) infos k
       | StructFieldKind.subobject => unreachable!
   else
     k infos
diff --git a/tests/lean/run/struct3.lean b/tests/lean/run/struct3.lean
index 28ccf3ef85..e96df1c457 100644
--- a/tests/lean/run/struct3.lean
+++ b/tests/lean/run/struct3.lean
@@ -1,14 +1,16 @@
-
-
 universes u v
 
-class Bind2 (m : Type u → Type v) :=
-(bind : ∀ {α β : Type u}, m α → (α → m β) → m β)
+class Bind2 (m : Type u → Type v) where
+  bind : ∀ {α β : Type u}, m α → (α → m β) → m β
 
-set_option pp.all true
+class Monad2 (m : Type u → Type v) extends Applicative m, Bind2 m : Type (max (u+1) v) where
+  map      := fun f x => Bind2.bind x (pure ∘ f)
+  seq      := fun f x => Bind2.bind f fun y => Functor.map y x
+  seqLeft  := fun x y => Bind2.bind x fun a => Bind2.bind y fun _ => pure a
+  seqRight := @fun β x y => Bind2.bind x fun _ => y -- Recall that `@` disables implicit lambda support
 
-class Monad2 (m : Type u → Type v) extends Applicative m, Bind2 m : Type (max (u+1) v) :=
-(map      := fun f x => Bind2.bind x (pure ∘ f))
-(seq      := fun f x => Bind2.bind f fun y => Functor.map y x)
-(seqLeft  := fun x y => Bind2.bind x fun a => Bind2.bind y fun _ => pure a)
-(seqRight := @fun β x y => Bind2.bind x fun _ => y) -- Recall that `@` disables implicit lambda support
+class Monad3 (m : Type u → Type v) extends Applicative m, Bind2 m : Type (max (u+1) v) where
+  map (f x)      := Bind2.bind x (pure ∘ f)
+  seq (f x)      := Bind2.bind f fun y => Functor.map y x
+  seqLeft (x y)  := Bind2.bind x fun a => Bind2.bind y fun _ => pure a
+  seqRight (x y) := Bind2.bind x fun _ => y