module
/-!
# `deriving Inhabited` uses structure field defaults

https://github.com/leanprover/lean4/issues/9463
-/

/-!
This used to use `false` in the `default` instance.
-/
structure Config where
  iota := true
deriving Inhabited

/-- info: true -/
#guard_msgs in #eval (default : Config).iota

/-- info: instInhabitedConfig : Inhabited Config -/
#guard_msgs in #check instInhabitedConfig

/-!
We don't require that every field have a default value.
-/
structure Config' where
  iota := true
  n : Nat
deriving Inhabited

/-- info: true -/
#guard_msgs in #eval (default : Config').iota
/-- info: 0 -/
#guard_msgs in #eval (default : Config').n

/-- info: instInhabitedConfig' : Inhabited Config' -/
#guard_msgs in #check instInhabitedConfig'

/-!
It still includes an `[Inhabited _]` parameter when needed.
-/
structure Config'' (α : Type) where
  iota := true
  n : α
deriving Inhabited

/-- info: true -/
#guard_msgs in #eval (default : Config'' Nat).iota
/-- info: 0 -/
#guard_msgs in #eval (default : Config'' Nat).n

/-- info: instInhabitedConfig'' {a✝ : Type} [Inhabited a✝] : Inhabited (Config'' a✝) -/
#guard_msgs in #check instInhabitedConfig''

/-!
In this example we can see that it adds an inhabited parameter.
-/
structure Config''' (α : Type) where
  n : α → α
deriving Inhabited

/-- info: instInhabitedConfig''' {a✝ : Type} [Inhabited a✝] : Inhabited (Config''' a✝) -/
#guard_msgs in #check instInhabitedConfig'''

/-!
Providing a default value inhibits adding an inhabited parameter.
-/
structure Config'''' (α : Type) where
  n : α → α := id
deriving Inhabited

/-- info: instInhabitedConfig'''' {a✝ : Type} : Inhabited (Config'''' a✝) -/
#guard_msgs in #check instInhabitedConfig''''

/-!
Mixed needs for `Inhabited` parameters.
-/
structure S (α β : Type) where
  f : α → α := id
  g : β
deriving Inhabited

/-- info: instInhabitedS {a✝ a✝¹ : Type} [Inhabited a✝¹] : Inhabited (S a✝ a✝¹) -/
#guard_msgs in #check instInhabitedS

/-!
When there are structure field default value cycles, those defaults can be ignored.
-/
structure A (α : Type) where
  (x y : α)
deriving Inhabited
structure B extends A Nat where
  n : Nat := 2
  x := y + 1
  y := x + 1
deriving Inhabited

/-- info: 2 -/
#guard_msgs in #eval (default : B).n
/-- info: 0 -/
#guard_msgs in #eval (default : B).x
/-- info: 0 -/
#guard_msgs in #eval (default : B).y

/-!
Regression test: take `meta` into account.
-/
public meta section

inductive AliasInfo where
  | plain (n : Nat)
deriving Inhabited, Repr

/-- info: AliasInfo.plain 0 -/
#guard_msgs in #eval repr (default : AliasInfo)
end

/-!
Regression test: take namespace into account.
-/
structure MyNS.MyStruct where
  x : Nat
  deriving Inhabited
/-- info: MyNS.instInhabitedMyStruct.default : MyNS.MyStruct -/
#guard_msgs in #check MyNS.instInhabitedMyStruct.default
/-- info: MyNS.instInhabitedMyStruct : Inhabited MyNS.MyStruct -/
#guard_msgs in #check MyNS.instInhabitedMyStruct

/-!
Fix for https://github.com/leanprover/lean4/issues/13372
Should inherit parent structures' Inhabited instances.
-/

structure Foo where
  n : Nat
  m : Nat
  h : n ≤ m

instance : Inhabited Foo where
  default := ⟨5, 5, Nat.le.refl⟩

-- Was: "failed to generate Inhabited instance for Bar"
structure Bar extends Foo where
  extra : Bool := true
  a : Nat
  deriving Inhabited

/-- info: 5 -/
#guard_msgs in #eval (default : Bar).n
/-- info: true -/
#guard_msgs in #eval (default : Bar).extra
/-- info: 0 -/
#guard_msgs in #eval (default : Bar).a

/-- info: Bar.mk default true default : Bar -/
#guard_msgs in
set_option pp.structureInstances false in
#check (struct_inst_default% : Bar)