feat: mutually dependent structure default values, and avoiding self-dependence

tests/elab/struct3.lean

@@ -20,3 +20,16 @@ class Monad4 (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m,
   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 ()
+
+/-!
+Can provide type signatures when setting defaults of inherited fields.
+-/
+class Monad5 (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m, Bind2 m where
+  map {α β} (f : α → β) (x : m α) : m β :=
+    Bind2.bind x (pure ∘ f)
+  seq {α β} (f : m (α → β)) (x : Unit -> m α) : m β :=
+    Bind2.bind f fun y => Functor.map y (x ())
+  seqLeft {α β} (x : m α) (y : Unit → m β) :=
+    Bind2.bind x fun a => Bind2.bind (y ()) fun _ => pure a
+  seqRight {α β} (x : m α) (y : Unit → m β) :=
+    Bind2.bind x fun _ => y ()

tests/elab/structureElab.lean

@@ -449,41 +449,134 @@ structure S4 extends S2, S3
 
 end TestO2
 
+namespace TestOptParam
+
+/-!
+All fields are in scope when elaborating default values.
+-/
+structure Loop where
+  x : Nat := y
+  y : Nat := x
+  deriving Repr
+
+/-- info: { x := 1, y := 1 } -/
+#guard_msgs in #eval { x := 1 : Loop }
+/-- info: { x := 2, y := 2 } -/
+#guard_msgs in #eval { y := 2 : Loop }
+/-- info: { x := 1, y := 2 } -/
+#guard_msgs in #eval { x := 1, y := 2 : Loop }
+
+/-!
+Testing a loop that goes through the parent structure.
+-/
+structure Base where
+  x : Nat
+  y : Nat := x
+  deriving Repr
+structure Loop2 extends Base where
+  x := y
+  deriving Repr
+/-- info: { toBase := { x := 1, y := 1 } } -/
+#guard_msgs in #eval { x := 1 : Loop2 }
+/-- info: { toBase := { x := 2, y := 2 } } -/
+#guard_msgs in #eval { y := 2 : Loop2 }
+
+/-!
+Restating the type of an inherited field is OK
+-/
+structure RestateType extends Base where
+  x : Nat := 1
+  deriving Repr
+/-- info: { toBase := { x := 1, y := 1 } } -/
+#guard_msgs in #eval { : RestateType }
+
+/-!
+Restating the type of an inherited field is a valid
+way to change the binder names.
+-/
+structure A (m : Type → Type) where
+  map (f : α → β) : m α → m β
+structure A' extends A List where
+  map {α β} (g : α → β) (xs : List α) : List β := List.map g xs
+
+/-- info: A'.mk (A.mk fun {α β} g xs => List.map g xs) : A' -/
+#guard_msgs in #check { : A'}
+
+/-!
+Default values cannot refer to the field.
+-/
+/-- error: Unknown identifier `x` -/
+#guard_msgs in
+structure InapplicableDefault1 where
+  x : Nat := x + 1
+
+/-!
+Default values can refer to later fields.
+-/
+structure ApplicableDefault2 where
+  x : Nat := y + 1
+  y : Fin 2
+
+/-!
+Default values cannot refer to later fields if they depend on the field.
+-/
+/-- error: Unknown identifier `y` -/
+#guard_msgs in
+structure InpplicableDefault3 where
+  x : Nat := y + 1
+  y : Fin x
+
+/-!
+Default values cannot refer to the field, even for inherited fields.
+-/
+structure Base2 where
+  x : Nat
+/-- error: Unknown identifier `x` -/
+#guard_msgs in
+structure InapplicableDefault2 extends Base2 where
+  x := x
+
+end TestOptParam
+
 /-!
 Some failures from unsupported autoparams
 -/
 namespace TestFail1
 
-/-- error: Invalid field declaration: Type must be provided when auto-param tactic is used -/
+/-- error: Failed to infer type of field `x` -/
 #guard_msgs in
 structure F1 where
   x := by exact 0
 
 structure F2 where
   x (n : Nat) : Nat
-/-- error: Omit the type of field `x` to set its auto-param tactic -/
+/--
+error: Invalid field: Uexpected type for field `x` when setting auto-param tactic for inherited field
+-/
 #guard_msgs in
 structure F3 extends F2 where
   x : Nat → Nat := by exact 0
 
-/-- error: Invalid field: Unexpected binders when setting auto-param tactic for inherited field -/
+/--
+error: Invalid field: Unexpected binders for field `x` when setting auto-param tactic for inherited field
+-/
 #guard_msgs in
 structure F4 extends F2 where
   x (n : Nat) := by exact 0
 
-/-- error: A new default value for field `x` has already been set in this structure -/
+/-- error: A default value for field `x` has already been set for this structure -/
 #guard_msgs in
 structure F5 extends F2 where
   x := by exact 0
   x := by exact 0
 
-/-- error: A new default value for field `x` has already been set in this structure -/
+/-- error: A default value for field `x` has already been set for this structure -/
 #guard_msgs in
 structure F6 extends F2 where
   x := id
   x := by exact 0
 
-/-- error: A new default value for field `x` has already been set in this structure -/
+/-- error: A default value for field `x` has already been set for this structure -/
 #guard_msgs in
 structure F7 extends F2 where
   x := by exact 0

tests/elab_fail/mvarAtDefaultValue.lean.out.expected

@@ -1,6 +1,4 @@
 mvarAtDefaultValue.lean:5:7-5:8: error: Failed to infer default value for field `x`
 mvarAtDefaultValue.lean:8:7-8:8: error: don't know how to synthesize placeholder
 context:
-x : Nat
-toA : A := ⋯
 ⊢ Nat

tests/elab_fail/struct1.lean

@@ -36,22 +36,22 @@ structure S' extends A Nat where
 (x := true) -- error type mismatch
 
 structure S extends A Nat where
-(x : Bool := true) -- error omit type
+(x : Bool := true) -- error type mismatch
 
 structure S'' where
 (x : Nat := true) -- error type mismatch
 
-private structure S where
+private structure Spriv where
 private mk :: (x : Nat)
 
-private structure S where
+private structure Spriv where
 protected mk :: (x : Nat)
 
-private structure S where
+private structure Spriv where
 protected (x : Nat)
 
-private structure S where
+private structure Spriv where
 mk2 :: (x : Nat)
 
-#check S
+#check Spriv
 #check S.mk2

tests/elab_fail/struct1.lean.out.expected

@@ -21,7 +21,12 @@ has type
   Bool
 but is expected to have type
   Nat
-struct1.lean:39:5-39:9: error: Omit the type of field `x` to set its default value
+struct1.lean:39:1-39:2: error: Type mismatch
+  true
+has type
+  Bool
+but is expected to have type
+  Nat
 struct1.lean:42:12-42:16: error: Type mismatch
   true
 has type
@@ -34,5 +39,5 @@ Hint: Remove `private` modifier from constructor
   p̵r̵i̵v̵a̵t̵e̵ ̵mk ::
 struct1.lean:48:0-48:15: error: Constructor cannot be `protected` because this structure is `private`
 struct1.lean:51:0-51:19: error: Field cannot be marked `protected` because this structure is `private`
-S : Type
-S.mk2 (x : Nat) : S
+Spriv : Type
+struct1.lean:57:7-57:12: error(lean.unknownIdentifier): Unknown constant `S.mk2`

tests/elab_fail/structDefValueOverride.lean.out.expected

@@ -1 +1 @@
-structDefValueOverride.lean:6:2-6:3: error: A new default value for field `x` has already been set in this structure
+structDefValueOverride.lean:6:2-6:3: error: A default value for field `x` has already been set for this structure