chore: use deriving Inhabited

src/Init/Core.lean

@@ -440,20 +440,7 @@ instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT :
 instance : Inhabited Prop where
   default := True
 
-instance : Inhabited Bool where
-  default := false
-
-instance : Inhabited True where
-  default := trivial
-
-instance : Inhabited NonScalar where
-  default := ⟨arbitrary⟩
-
-instance : Inhabited PNonScalar.{u} where
-  default := ⟨arbitrary⟩
-
-instance {α} [Inhabited α] : Inhabited (ForInStep α) where
-  default := ForInStep.done (arbitrary)
+deriving instance Inhabited for Bool, NonScalar, PNonScalar, True, ForInStep
 
 class inductive Nonempty (α : Sort u) : Prop where
   | intro (val : α) : Nonempty α

src/Init/Meta.lean

@@ -73,11 +73,10 @@ end Name
 structure NameGenerator where
   namePrefix : Name := `_uniq
   idx        : Nat  := 1
+  deriving Inhabited
 
 namespace NameGenerator
 
-instance : Inhabited NameGenerator := ⟨{}⟩
-
 @[inline] def curr (g : NameGenerator) : Name :=
   Name.mkNum g.namePrefix g.idx
 

src/Init/System/IOError.lean

@@ -51,6 +51,7 @@ inductive IO.Error where
 
   | unexpectedEof
   | userError (msg : String)
+  deriving Inhabited
 
 @[export mk_io_user_error]
 def IO.userError (s : String) : IO.Error :=
@@ -190,6 +191,5 @@ def toString : IO.Error → String
   | userError msg                            => msg
 
 instance : ToString IO.Error := ⟨ IO.Error.toString ⟩
-instance : Inhabited IO.Error := ⟨ userError "" ⟩
 
 end IO.Error

src/Lean/Class.lean

@@ -20,11 +20,10 @@ end ClassEntry
 
 structure ClassState where
   hasOutParam : SMap Name Bool := SMap.empty
+  deriving Inhabited
 
 namespace ClassState
 
-instance : Inhabited ClassState := ⟨{}⟩
-
 def addEntry (s : ClassState) (entry : ClassEntry) : ClassState :=
   { s with hasOutParam := s.hasOutParam.insert entry.name entry.hasOutParam }
 

src/Lean/Compiler/IR/Basic.lean

@@ -23,10 +23,12 @@ abbrev Index := Nat
 /- Variable identifier -/
 structure VarId where
   idx : Index
+  deriving Inhabited
 
 /- Join point identifier -/
 structure JoinPointId where
   idx : Index
+  deriving Inhabited
 
 abbrev Index.lt (a b : Index) : Bool := a < b
 
@@ -80,6 +82,7 @@ inductive IRType where
   | irrelevant | object | tobject
   | struct (leanTypeName : Option Name) (types : Array IRType) : IRType
   | union (leanTypeName : Name) (types : Array IRType) : IRType
+  deriving Inhabited
 
 namespace IRType
 
@@ -134,6 +137,7 @@ end IRType
 inductive Arg where
   | var (id : VarId)
   | irrelevant
+  deriving Inhabited
 
 protected def Arg.beq : Arg → Arg → Bool
   | var x,      var y      => x == y
@@ -141,7 +145,6 @@ protected def Arg.beq : Arg → Arg → Bool
   | _,          _          => false
 
 instance : BEq Arg := ⟨Arg.beq⟩
-instance : Inhabited Arg := ⟨Arg.irrelevant⟩
 
 @[export lean_ir_mk_var_arg] def mkVarArg (id : VarId) : Arg := Arg.var id
 
@@ -233,8 +236,7 @@ structure Param where
   x : VarId
   borrow : Bool
   ty : IRType
-
-instance : Inhabited Param := ⟨{ x := { idx := 0 }, borrow := false, ty := IRType.object }⟩
+  deriving Inhabited
 
 @[export lean_ir_mk_param]
 def mkParam (x : VarId) (borrow : Bool) (ty : IRType) : Param := ⟨x, borrow, ty⟩

src/Lean/Compiler/IR/ElimDeadBranches.lean

@@ -15,11 +15,10 @@ inductive Value where
   | top -- any value
   | ctor (i : CtorInfo) (vs : Array Value)
   | choice (vs : List Value)
+  deriving Inhabited
 
 namespace Value
 
-instance : Inhabited Value := ⟨top⟩
-
 protected partial def beq : Value → Value → Bool
   | bot, bot => true
   | top, top => true

src/Lean/Compiler/IR/LiveVars.lean

@@ -81,7 +81,8 @@ def FnBody.hasLiveVar (b : FnBody) (ctx : LocalContext) (x : VarId) : Bool :=
 abbrev LiveVarSet   := VarIdSet
 abbrev JPLiveVarMap := Std.RBMap JoinPointId LiveVarSet (fun j₁ j₂ => j₁.idx < j₂.idx)
 
-instance : Inhabited LiveVarSet := ⟨{}⟩
+instance : Inhabited LiveVarSet where
+  default := {}
 
 def mkLiveVarSet (x : VarId) : LiveVarSet :=
   Std.RBTree.empty.insert x

src/Lean/Compiler/IR/RC.lean

@@ -17,12 +17,10 @@ structure VarInfo where
   ref        : Bool := true  -- true if the variable may be a reference (aka pointer) at runtime
   persistent : Bool := false -- true if the variable is statically known to be marked a Persistent at runtime
   consume    : Bool := false -- true if the variable RC must be "consumed"
+  deriving Inhabited
 
 abbrev VarMap := Std.RBMap VarId VarInfo (fun x y => x.idx < y.idx)
 
-instance : Inhabited VarInfo where
-  default := {}
-
 structure Context where
   env            : Environment
   decls          : Array Decl

src/Lean/Compiler/InlineAttrs.lean

@@ -10,11 +10,10 @@ namespace Lean.Compiler
 
 inductive InlineAttributeKind where
   | inline | noinline | macroInline | inlineIfReduce
+  deriving Inhabited
 
 namespace InlineAttributeKind
 
-instance : Inhabited InlineAttributeKind := ⟨InlineAttributeKind.inline⟩
-
 protected def beq : InlineAttributeKind → InlineAttributeKind → Bool
   | inline, inline => true
   | noinline, noinline => true

src/Lean/Data/Position.lean

@@ -10,6 +10,7 @@ namespace Lean
 structure Position where
   line   : Nat
   column : Nat
+  deriving Inhabited
 
 namespace Position
 instance : DecidableEq Position :=
@@ -30,20 +31,16 @@ instance : ToFormat Position :=
 
 instance : ToString Position :=
   ⟨fun ⟨l, c⟩ => "⟨" ++ toString l ++ ", " ++ toString c ++ "⟩"⟩
-
-instance : Inhabited Position := ⟨⟨1, 0⟩⟩
 end Position
 
 structure FileMap where
   source    : String
   positions : Array String.Pos
   lines     : Array Nat
+  deriving Inhabited
 
 namespace FileMap
 
-instance : Inhabited FileMap :=
-  ⟨{ source := "", positions := #[], lines := #[] }⟩
-
 partial def ofString (s : String) : FileMap :=
   let rec loop (i : String.Pos) (line : Nat) (ps : Array String.Pos) (lines : Array Nat) : FileMap :=
     if s.atEnd i then { source := s, positions := ps.push i, lines := lines.push line }

src/Lean/Declaration.lean

@@ -34,6 +34,7 @@ inductive ReducibilityHints where
   | opaque   : ReducibilityHints
   | «abbrev» : ReducibilityHints
   | regular  : UInt32 → ReducibilityHints
+  deriving Inhabited
 
 @[export lean_mk_reducibility_hints_regular]
 def mkReducibilityHintsRegularEx (h : UInt32) : ReducibilityHints :=
@@ -47,8 +48,6 @@ def ReducibilityHints.getHeightEx (h : ReducibilityHints) : UInt32 :=
 
 namespace ReducibilityHints
 
-instance : Inhabited ReducibilityHints := ⟨opaque⟩
-
 def lt : ReducibilityHints → ReducibilityHints → Bool
   | «abbrev»,   «abbrev»   => false
   | «abbrev»,   _          => true
@@ -63,8 +62,7 @@ structure ConstantVal where
   name : Name
   lparams : List Name
   type : Expr
-
-instance : Inhabited ConstantVal := ⟨{ name := arbitrary, lparams := arbitrary, type := arbitrary }⟩
+  deriving Inhabited
 
 structure AxiomVal extends ConstantVal where
   isUnsafe : Bool
@@ -136,8 +134,7 @@ inductive Declaration where
   | quotDecl
   | mutualDefnDecl  (defns : List DefinitionVal) -- All definitions must be marked as `unsafe`
   | inductDecl      (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool)
-
-instance : Inhabited Declaration := ⟨Declaration.quotDecl⟩
+  deriving Inhabited
 
 @[export lean_mk_inductive_decl]
 def mkInductiveDeclEs (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool) : Declaration :=
@@ -185,9 +182,7 @@ structure InductiveVal extends ConstantVal where
   isUnsafe : Bool
   isReflexive : Bool
   isNested : Bool
-
-instance : Inhabited InductiveVal where
-  default := ⟨arbitrary, 0, 0, [], [], false, false, false, false⟩
+  deriving Inhabited
 
 @[export lean_mk_inductive_val]
 def mkInductiveValEx (name : Name) (lparams : List Name) (type : Expr) (nparams nindices : Nat)
@@ -218,6 +213,7 @@ structure ConstructorVal extends ConstantVal where
   nparams : Nat   -- Number of parameters in inductive datatype `induct`
   nfields : Nat   -- Number of fields (i.e., arity - nparams)
   isUnsafe : Bool
+  deriving Inhabited
 
 @[export lean_mk_constructor_val]
 def mkConstructorValEx (name : Name) (lparams : List Name) (type : Expr) (induct : Name) (cidx nparams nfields : Nat) (isUnsafe : Bool) : ConstructorVal := {
@@ -233,9 +229,6 @@ def mkConstructorValEx (name : Name) (lparams : List Name) (type : Expr) (induct
 
 @[export lean_constructor_val_is_unsafe] def ConstructorVal.isUnsafeEx (v : ConstructorVal) : Bool := v.isUnsafe
 
-instance : Inhabited ConstructorVal :=
-  ⟨{ toConstantVal := arbitrary, induct := arbitrary, cidx := 0, nparams := 0, nfields := 0, isUnsafe := true }⟩
-
 /-- Information for reducing a recursor -/
 structure RecursorRule where
   ctor : Name   -- Reduction rule for this Constructor

src/Lean/Elab/App.lean

@@ -23,8 +23,7 @@ def hasElabWithoutExpectedType (env : Environment) (declName : Name) : Bool :=
 inductive Arg where
   | stx  (val : Syntax)
   | expr (val : Expr)
-
-instance : Inhabited Arg := ⟨Arg.stx arbitrary⟩
+  deriving Inhabited
 
 instance : ToString Arg := ⟨fun
   | Arg.stx  val => toString val
@@ -35,12 +34,11 @@ structure NamedArg where
   ref  : Syntax := Syntax.missing
   name : Name
   val  : Arg
+  deriving Inhabited
 
 instance : ToString NamedArg where
   toString s := "(" ++ toString s.name ++ " := " ++ toString s.val ++ ")"
 
-instance : Inhabited NamedArg := ⟨{ name := arbitrary, val := arbitrary }⟩
-
 def throwInvalidNamedArg {α} (namedArg : NamedArg) (fn? : Option Name) : TermElabM α :=
   withRef namedArg.ref $ match fn? with
     | some fn => throwError! "invalid argument name '{namedArg.name}' for function '{fn}'"

src/Lean/Elab/Command.lean

@@ -21,8 +21,7 @@ structure Scope where
   openDecls     : List OpenDecl := []
   levelNames    : List Name := []
   varDecls      : Array Syntax := #[]
-
-instance : Inhabited Scope := ⟨{ header := "" }⟩
+  deriving Inhabited
 
 structure State where
   env            : Environment
@@ -32,8 +31,7 @@ structure State where
   maxRecDepth    : Nat
   nextInstIdx    : Nat := 1 -- for generating anonymous instance names
   ngen           : NameGenerator := {}
-
-instance : Inhabited State := ⟨{ env := arbitrary, maxRecDepth := 0 }⟩
+  deriving Inhabited
 
 def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State := {
   env := env
@@ -241,7 +239,8 @@ def adaptExpander (exp : Syntax → CommandElabM Syntax) : CommandElab := fun st
 private def getVarDecls (s : State) : Array Syntax :=
   s.scopes.head!.varDecls
 
-instance {α} : Inhabited (CommandElabM α) := ⟨throw arbitrary⟩
+instance {α} : Inhabited (CommandElabM α) where
+  default := throw arbitrary
 
 private def mkMetaContext : Meta.Context := {
   config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true }

src/Lean/Elab/DeclModifiers.lean

@@ -26,6 +26,7 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception
 
 inductive Visibility where
   | regular | «protected» | «private»
+  deriving Inhabited
 
 instance : ToString Visibility := ⟨fun
   | Visibility.regular     => "regular"
@@ -39,6 +40,7 @@ structure Modifiers where
   isPartial       : Bool := false
   isUnsafe        : Bool := false
   attrs           : Array Attribute := #[]
+  deriving Inhabited
 
 def Modifiers.isPrivate : Modifiers → Bool
   | { visibility := Visibility.private, .. } => true

src/Lean/Elab/DefView.lean

@@ -16,6 +16,7 @@ namespace Lean.Elab
 
 inductive DefKind where
   | «def» | «theorem» | «example» | «opaque» | «abbrev»
+  deriving Inhabited
 
 def DefKind.isTheorem : DefKind → Bool
   | «theorem» => true
@@ -39,6 +40,7 @@ structure DefView where
   binders       : Syntax
   type?         : Option Syntax
   value         : Syntax
+  deriving Inhabited
 
 namespace Command
 

src/Lean/Elab/Do.lean

@@ -80,6 +80,7 @@ structure Alt (σ : Type) where
   vars : Array Name
   patterns : Syntax
   rhs : σ
+  deriving Inhabited
 
 /-
   Auxiliary datastructure for representing a `do` code block, and compiling "reassignments" (e.g., `x := x + 1`).
@@ -143,12 +144,7 @@ inductive Code where
   | ite          (ref : Syntax) (h? : Option Name) (optIdent : Syntax) (cond : Syntax) (thenBranch : Code) (elseBranch : Code)
   | «match»      (ref : Syntax) (discrs : Syntax) (optType : Syntax) (alts : Array (Alt Code))
   | jmp          (ref : Syntax) (jpName : Name) (args : Array Syntax)
-
-instance : Inhabited Code :=
-  ⟨Code.«break» arbitrary⟩
-
-instance : Inhabited (Alt Code) :=
-  ⟨{ ref := arbitrary, vars := #[], patterns := arbitrary, rhs := arbitrary }⟩
+  deriving Inhabited
 
 /- A code block, and the collection of variables updated by it. -/
 structure CodeBlock where

src/Lean/Elab/Inductive.lean

@@ -49,9 +49,7 @@ structure CtorView where
   declName  : Name
   binders   : Syntax
   type?     : Option Syntax
-
-instance : Inhabited CtorView :=
-  ⟨{ ref := arbitrary, modifiers := {}, inferMod := false, declName := arbitrary, binders := arbitrary, type? := none }⟩
+  deriving Inhabited
 
 structure InductiveView where
   ref             : Syntax
@@ -63,10 +61,7 @@ structure InductiveView where
   type?           : Option Syntax
   ctors           : Array CtorView
   derivingClasses : Array DerivingClassView
-
-instance : Inhabited InductiveView :=
-  ⟨{ ref := arbitrary, modifiers := {}, shortDeclName := arbitrary, declName := arbitrary,
-     levelNames := [], binders := arbitrary, type? := none, ctors := #[], derivingClasses := #[] }⟩
+  deriving Inhabited
 
 structure ElabHeaderResult where
   view       : InductiveView
@@ -74,9 +69,7 @@ structure ElabHeaderResult where
   localInsts : LocalInstances
   params     : Array Expr
   type       : Expr
-
-instance : Inhabited ElabHeaderResult :=
-  ⟨{ view := arbitrary, lctx := arbitrary, localInsts := arbitrary, params := #[], type := arbitrary }⟩
+  deriving Inhabited
 
 private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc : Array ElabHeaderResult) : TermElabM (Array ElabHeaderResult) := do
   if h : i < views.size then

src/Lean/Elab/Match.lean

@@ -268,8 +268,7 @@ structure Context where
   namedArgs     : Array NamedArg
   args          : List Arg
   newArgs       : Array Syntax := #[]
-
-instance : Inhabited Context := ⟨⟨arbitrary, none, false, false, #[], 0, #[], [], #[]⟩⟩
+  deriving Inhabited
 
 private def isDone (ctx : Context) : Bool :=
   ctx.paramDeclIdx ≥ ctx.paramDecls.size

src/Lean/Elab/MutualDef.lean

@@ -22,9 +22,7 @@ structure DefViewElabHeader where
   numParams     : Nat
   type          : Expr -- including the parameters
   valueStx      : Syntax
-
-instance : Inhabited DefViewElabHeader :=
-  ⟨⟨arbitrary, {}, DefKind.«def», arbitrary, arbitrary, [], 0, arbitrary, arbitrary ⟩⟩
+  deriving Inhabited
 
 namespace Term
 

src/Lean/Elab/PreDefinition/Basic.lean

@@ -24,6 +24,7 @@ structure PreDefinition where
   declName  : Name
   type      : Expr
   value     : Expr
+  deriving Inhabited
 
 instance : Inhabited PreDefinition :=
   ⟨⟨DefKind.«def», [], {}, arbitrary, arbitrary, arbitrary⟩⟩

src/Lean/Environment.lean

@@ -15,7 +15,8 @@ namespace Lean
 /- Opaque environment extension state. -/
 constant EnvExtensionStateSpec : PointedType.{0}
 def EnvExtensionState : Type := EnvExtensionStateSpec.type
-instance : Inhabited EnvExtensionState := ⟨EnvExtensionStateSpec.val⟩
+instance : Inhabited EnvExtensionState where
+  default := EnvExtensionStateSpec.val
 
 def ModuleIdx := Nat
 
@@ -47,6 +48,7 @@ structure EnvironmentHeader where
   imports      : Array Import := #[] -- direct imports
   regions      : Array CompactedRegion := #[] -- compacted regions of all imported modules
   moduleNames  : NameSet      := {}  -- names of all imported modules
+  deriving Inhabited
 
 open Std (HashMap)
 
@@ -55,12 +57,10 @@ structure Environment where
   constants    : ConstMap
   extensions   : Array EnvExtensionState
   header       : EnvironmentHeader := {}
+  deriving Inhabited
 
 namespace Environment
 
-instance : Inhabited Environment :=
-  ⟨{ const2ModIdx := {}, constants := {}, extensions := #[] }⟩
-
 def addAux (env : Environment) (cinfo : ConstantInfo) : Environment :=
   { env with constants := env.constants.insert cinfo.name cinfo }
 
@@ -148,15 +148,16 @@ structure EnvExtensionInterface where
   getState     {σ} (e : ext σ) (env : Environment) : σ
   mkInitialExtStates : IO (Array EnvExtensionState)
 
-instance : Inhabited EnvExtensionInterface := ⟨{
-  ext                := id,
-  inhabitedExt       := id,
-  registerExt        := fun mk => mk,
-  setState           := fun _ env _ => env,
-  modifyState        := fun _ env _ => env,
-  getState           := fun ext _ => ext,
-  mkInitialExtStates := pure #[]
-}⟩
+instance : Inhabited EnvExtensionInterface where
+  default := {
+    ext                := id,
+    inhabitedExt       := id,
+    registerExt        := fun mk => mk,
+    setState           := fun _ env _ => env,
+    modifyState        := fun _ env _ => env,
+    getState           := fun ext _ => ext,
+    mkInitialExtStates := pure #[]
+  }
 
 /- Unsafe implementation of `EnvExtensionInterface` -/
 namespace EnvExtensionInterfaceUnsafe
@@ -164,8 +165,7 @@ namespace EnvExtensionInterfaceUnsafe
 structure Ext (σ : Type) where
   idx       : Nat
   mkInitial : IO σ
-
-instance {σ} : Inhabited (Ext σ) := ⟨{idx := 0, mkInitial := arbitrary }⟩
+  deriving Inhabited
 
 private def mkEnvExtensionsRef : IO (IO.Ref (Array (Ext EnvExtensionState))) := IO.mkRef #[]
 @[builtinInit mkEnvExtensionsRef] private constant envExtensionsRef : IO.Ref (Array (Ext EnvExtensionState))
@@ -285,14 +285,15 @@ instance : Inhabited EnvExtensionEntry := ⟨EnvExtensionEntrySpec.val⟩
 instance {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtensionState α σ) :=
   ⟨{importedEntries := #[], state := arbitrary }⟩
 
-instance {α β σ} [Inhabited σ] : Inhabited (PersistentEnvExtension α β σ) := ⟨{
-   toEnvExtension := arbitrary,
-   name := arbitrary,
-   addImportedFn := fun _ => arbitrary,
-   addEntryFn := fun s _ => s,
-   exportEntriesFn := fun _ => #[],
-   statsFn := fun _ => Format.nil
-}⟩
+instance {α β σ} [Inhabited σ] : Inhabited (PersistentEnvExtension α β σ) where
+  default := {
+     toEnvExtension := arbitrary,
+     name := arbitrary,
+     addImportedFn := fun _ => arbitrary,
+     addEntryFn := fun s _ => s,
+     exportEntriesFn := fun _ => #[],
+     statsFn := fun _ => Format.nil
+  }
 
 namespace PersistentEnvExtension
 

src/Lean/KeyedDeclsAttribute.lean

@@ -36,9 +36,7 @@ structure Def (γ : Type) where
     fun builtin arg => match attrParamSyntaxToIdentifier arg with
       | some id => pure id
       | none    => throwError "invalid attribute argument, expected identifier"
-
-instance {γ} : Inhabited (Def γ) :=
-  ⟨{ builtinName := arbitrary, name := arbitrary, descr := arbitrary, valueTypeName := arbitrary }⟩
+  deriving Inhabited
 
 structure OLeanEntry where
   key  : Key
@@ -54,6 +52,7 @@ abbrev Table (γ : Type) := SMap Key (List γ)
 structure ExtensionState (γ : Type) where
   newEntries : List OLeanEntry := []
   table      : Table γ := {}
+  deriving Inhabited
 
 abbrev Extension (γ : Type) := PersistentEnvExtension OLeanEntry (AttributeEntry γ) (ExtensionState γ)
 
@@ -65,6 +64,7 @@ structure KeyedDeclsAttribute (γ : Type) where
   tableRef : IO.Ref (KeyedDeclsAttribute.Table γ)
   -- instances from current module
   ext      : KeyedDeclsAttribute.Extension γ
+  deriving Inhabited
 
 namespace KeyedDeclsAttribute
 
@@ -73,11 +73,6 @@ def Table.insert {γ : Type} (table : Table γ) (k : Key) (v : γ) : Table γ :=
   | some vs => SMap.insert table k (v::vs)
   | none    => SMap.insert table k [v]
 
-instance {γ} : Inhabited (ExtensionState γ) := ⟨{}⟩
-
-instance {γ} : Inhabited (KeyedDeclsAttribute γ) :=
-  ⟨{ defn := arbitrary, tableRef := arbitrary, ext := arbitrary }⟩
-
 private def mkInitial {γ} (tableRef : IO.Ref (Table γ)) : IO (ExtensionState γ) := do
   let table ← tableRef.get
   pure { table := table }

src/Lean/LocalContext.lean

@@ -12,6 +12,7 @@ namespace Lean
 inductive LocalDecl where
   | cdecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo)
   | ldecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nonDep : Bool)
+  deriving Inhabited
 
 @[export lean_mk_local_decl]
 def mkLocalDeclEx (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) : LocalDecl :=
@@ -25,7 +26,6 @@ def LocalDecl.binderInfoEx : LocalDecl → BinderInfo
   | _                          => BinderInfo.default
 
 namespace LocalDecl
-instance : Inhabited LocalDecl := ⟨ldecl arbitrary arbitrary arbitrary arbitrary arbitrary false⟩
 
 def isLet : LocalDecl → Bool
   | cdecl .. => false
@@ -96,9 +96,9 @@ open Std (PersistentHashMap PersistentArray PArray)
 structure LocalContext where
   fvarIdToDecl : PersistentHashMap FVarId LocalDecl := {}
   decls        : PersistentArray (Option LocalDecl) := {}
+  deriving Inhabited
 
 namespace LocalContext
-instance : Inhabited LocalContext := ⟨{}⟩
 
 @[export lean_mk_empty_local_ctx]
 def mkEmpty : Unit → LocalContext := fun _ => {}

src/Lean/Message.lean

@@ -19,6 +19,7 @@ def mkErrorStringWithPos (fileName : String) (line col : Nat) (msg : String) : S
 
 inductive MessageSeverity where
   | information | warning | error
+  deriving Inhabited
 
 structure MessageDataContext where
   env : Environment
@@ -51,6 +52,7 @@ inductive MessageData where
      Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure". -/
   | tagged            : Name → MessageData → MessageData
   | node              : Array MessageData → MessageData
+  deriving Inhabited
 
 namespace MessageData
 
@@ -65,8 +67,6 @@ def isNest : MessageData → Bool
   | nest _ _ => true
   | _        => false
 
-instance : Inhabited MessageData := ⟨MessageData.ofFormat arbitrary⟩
-
 def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext := {
   env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts,
   currNamespace := nCtx.currNamespace, openDecls := nCtx.openDecls
@@ -142,6 +142,7 @@ structure Message where
   severity : MessageSeverity := MessageSeverity.error
   caption  : String          := ""
   data     : MessageData
+  deriving Inhabited
 
 @[export lean_mk_message]
 def mkMessageEx (fileName : String) (pos : Position) (endPos : Option Position) (severity : MessageSeverity) (caption : String) (text : String) : Message :=

src/Lean/Meta/Basic.lean

@@ -60,8 +60,7 @@ structure ParamInfo where
   instImplicit : Bool      := false
   hasFwdDeps   : Bool      := false
   backDeps     : Array Nat := #[]
-
-instance : Inhabited ParamInfo := ⟨{}⟩
+  deriving Inhabited
 
 def ParamInfo.isExplicit (p : ParamInfo) : Bool :=
   !p.implicit && p.instImplicit
@@ -74,9 +73,9 @@ structure InfoCacheKey where
   transparency : TransparencyMode
   expr         : Expr
   nargs?       : Option Nat
+  deriving Inhabited
 
 namespace InfoCacheKey
-instance : Inhabited InfoCacheKey := ⟨⟨arbitrary, arbitrary, arbitrary⟩⟩
 instance : Hashable InfoCacheKey :=
   ⟨fun ⟨transparency, expr, nargs⟩ => mixHash (hash transparency) $ mixHash (hash expr) (hash nargs)⟩
 instance : BEq InfoCacheKey :=
@@ -93,6 +92,7 @@ structure Cache where
   synthInstance : SynthInstanceCache := {}
   whnfDefault   : PersistentExprStructMap Expr := {} -- cache for closed terms and `TransparencyMode.default`
   whnfAll       : PersistentExprStructMap Expr := {} -- cache for closed terms and `TransparencyMode.all`
+  deriving Inhabited
 
 structure PostponedEntry where
   lhs       : Level
@@ -104,8 +104,7 @@ structure State where
   /- When `trackZeta == true`, then any let-decl free variable that is zeta expansion performed by `MetaM` is stored in `zetaFVarIds`. -/
   zetaFVarIds : NameSet := {}
   postponed   : PersistentArray PostponedEntry := {}
-
-instance : Inhabited State := ⟨{}⟩
+  deriving Inhabited
 
 structure Context where
   config         : Config         := {}
@@ -114,22 +113,18 @@ structure Context where
 
 abbrev MetaM  := ReaderT Context $ StateRefT State CoreM
 
-instance : Inhabited (MetaM α) := {
+instance : Inhabited (MetaM α) where
   default := fun _ _ => arbitrary
-}
 
-instance : MonadLCtx MetaM := {
-  getLCtx := do pure (← read).lctx
-}
+instance : MonadLCtx MetaM where
+  getLCtx := return (← read).lctx
 
-instance : MonadMCtx MetaM := {
-  getMCtx    := do pure (← get).mctx,
-  modifyMCtx := fun f => modify fun s => { s with mctx := f s.mctx }
-}
+instance : MonadMCtx MetaM where
+  getMCtx    := return (← get).mctx
+  modifyMCtx f := modify fun s => { s with mctx := f s.mctx }
 
-instance : AddMessageContext MetaM := {
+instance : AddMessageContext MetaM where
   addMessageContext := addMessageContextFull
-}
 
 @[inline] def MetaM.run (x : MetaM α) (ctx : Context := {}) (s : State := {}) : CoreM (α × State) :=
   x ctx |>.run s

src/Lean/Meta/Closure.lean

@@ -100,9 +100,7 @@ namespace Closure
 structure ToProcessElement where
   fvarId : FVarId
   newFVarId : FVarId
-
-instance : Inhabited ToProcessElement :=
-  ⟨⟨arbitrary, arbitrary⟩⟩
+  deriving Inhabited
 
 structure Context where
   zeta : Bool

src/Lean/Meta/SynthInstance.lean

@@ -29,8 +29,7 @@ structure GeneratorNode where
   mctx            : MetavarContext
   instances       : Array Expr
   currInstanceIdx : Nat
-
-instance : Inhabited GeneratorNode := ⟨⟨arbitrary, arbitrary, arbitrary, arbitrary, 0⟩⟩
+  deriving Inhabited
 
 structure ConsumerNode where
   mvar     : Expr
@@ -38,9 +37,7 @@ structure ConsumerNode where
   mctx     : MetavarContext
   subgoals : List Expr
   size     : Nat -- instance size so far
-
-instance : Inhabited ConsumerNode where
-  default := { mvar := arbitrary, key := arbitrary, mctx := arbitrary, subgoals := [], size := 0 }
+  deriving Inhabited
 
 inductive Waiter where
   | consumerNode : ConsumerNode → Waiter

src/Lean/MetavarContext.lean

@@ -221,6 +221,7 @@ we may solve the issue by implementing `isDefEqCheap` that never invokes TC and
 structure LocalInstance where
   className : Name
   fvar      : Expr
+  deriving Inhabited
 
 abbrev LocalInstances := Array LocalInstance
 
@@ -237,6 +238,7 @@ inductive MetavarKind where
   | natural
   | synthetic
   | syntheticOpaque
+  deriving Inhabited
 
 def MetavarKind.isSyntheticOpaque : MetavarKind → Bool
   | MetavarKind.syntheticOpaque => true
@@ -254,13 +256,12 @@ structure MetavarDecl where
   localInstances : LocalInstances
   kind           : MetavarKind
   numScopeArgs   : Nat := 0 -- See comment at `CheckAssignment` `Meta/ExprDefEq.lean`
+  deriving Inhabited
 
 @[export lean_mk_metavar_decl]
 def mkMetavarDeclEx (userName : Name) (lctx : LocalContext) (type : Expr) (depth : Nat) (localInstances : LocalInstances) (kind : MetavarKind) : MetavarDecl :=
   { userName := userName, lctx := lctx, type := type, depth := depth, localInstances := localInstances, kind := kind }
 
-instance : Inhabited MetavarDecl := ⟨{ lctx := arbitrary, type := arbitrary, depth := 0, localInstances := #[], kind := MetavarKind.natural }⟩
-
 /--
   A delayed assignment for a metavariable `?m`. It represents an assignment of the form
   `?m := (fun fvars => val)`. The local context `lctx` provides the declarations for `fvars`.

src/Lean/Parser/Basic.lean

@@ -116,10 +116,7 @@ structure InputContext where
   input    : String
   fileName : String
   fileMap  : FileMap
-
-instance : Inhabited InputContext := ⟨{
-  input := "", fileName := "", fileMap := arbitrary
-}⟩
+  deriving Inhabited
 
 /-- Input context derived from elaboration of previous commands. -/
 structure ParserModuleContext where
@@ -142,9 +139,9 @@ def ParserContext.resolveName (ctx : ParserContext) (id : Name) : List (Name ×
 structure Error where
   unexpected : String := ""
   expected : List String := []
+  deriving Inhabited
 
 namespace Error
-instance : Inhabited Error := ⟨{}⟩
 
 private def expectedToString : List String → String
   | []       => ""
@@ -262,13 +259,15 @@ end ParserState
 
 def ParserFn := ParserContext → ParserState → ParserState
 
-instance : Inhabited ParserFn := ⟨fun _ => id⟩
+instance : Inhabited ParserFn where
+  default := fun ctx s => s
 
 inductive FirstTokens where
   | epsilon   : FirstTokens
   | unknown   : FirstTokens
   | tokens    : List Token → FirstTokens
   | optTokens : List Token → FirstTokens
+  deriving Inhabited
 
 namespace FirstTokens
 
@@ -305,13 +304,12 @@ structure ParserInfo where
   collectTokens : List Token → List Token := id
   collectKinds  : SyntaxNodeKindSet → SyntaxNodeKindSet := id
   firstTokens   : FirstTokens := FirstTokens.unknown
+  deriving Inhabited
 
 structure Parser where
   info : ParserInfo := {}
   fn   : ParserFn
-
-instance : Inhabited Parser :=
-  ⟨{ fn := fun _ s => s }⟩
+  deriving Inhabited
 
 abbrev TrailingParser := Parser
 

src/Lean/Parser/Extension.lean

@@ -54,18 +54,14 @@ inductive OLeanEntry where
   | kind      (val : SyntaxNodeKind) : OLeanEntry
   | category  (catName : Name) (leadingIdentAsSymbol : Bool)
   | parser    (catName : Name) (declName : Name) (prio : Nat) : OLeanEntry
+  deriving Inhabited
 
 inductive Entry where
   | token     (val : Token) : Entry
   | kind      (val : SyntaxNodeKind) : Entry
   | category  (catName : Name) (leadingIdentAsSymbol : Bool)
   | parser    (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : Entry
-
-instance : Inhabited OLeanEntry where
-  default := OLeanEntry.token arbitrary
-
-instance : Inhabited Entry where
-  default := Entry.token arbitrary
+  deriving Inhabited
 
 def Entry.toOLeanEntry : Entry → OLeanEntry
   | token v             => OLeanEntry.token v
@@ -77,8 +73,7 @@ structure State where
   tokens      : TokenTable := {}
   kinds       : SyntaxNodeKindSet := {}
   categories  : ParserCategories := {}
-
-instance : Inhabited State := ⟨{}⟩
+  deriving Inhabited
 
 end ParserExtension
 

src/Lean/Parser/Module.lean

@@ -31,8 +31,7 @@ end Module
 structure ModuleParserState where
   pos        : String.Pos := 0
   recovering : Bool       := false
-
-instance : Inhabited ModuleParserState := ⟨{}⟩
+  deriving Inhabited
 
 private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : String) : Message :=
   let pos := c.fileMap.toPosition pos

src/Lean/ParserCompiler/Attribute.lean

@@ -14,7 +14,7 @@ namespace ParserCompiler
 structure CombinatorAttribute where
   impl : AttributeImpl
   ext  : SimplePersistentEnvExtension (Name × Name) (NameMap Name)
-
+  deriving Inhabited
 -- TODO(Sebastian): We'll probably want priority support here at some point
 
 def registerCombinatorAttribute (name : Name) (descr : String)
@@ -40,8 +40,6 @@ def registerCombinatorAttribute (name : Name) (descr : String)
 
 namespace CombinatorAttribute
 
-instance : Inhabited CombinatorAttribute := ⟨{ impl := arbitrary, ext := arbitrary }⟩
-
 def getDeclFor? (attr : CombinatorAttribute) (env : Environment) (parserDecl : Name) : Option Name :=
   (attr.ext.getState env).find? parserDecl
 

src/Lean/Util/CollectFVars.lean

@@ -10,8 +10,7 @@ namespace Lean.CollectFVars
 structure State where
   visitedExpr  : ExprSet  := {}
   fvarSet      : NameSet  := {}
-
-instance : Inhabited State := ⟨{}⟩
+  deriving Inhabited
 
 abbrev Visitor := State → State
 

src/Std/Data/BinomialHeap.lean

@@ -15,13 +15,12 @@ structure HeapNodeAux (α : Type u) (h : Type u) where
 inductive Heap (α : Type u) : Type u where
   | empty     : Heap α
   | heap  (ns : List (HeapNodeAux α (Heap α))) : Heap α
+  deriving Inhabited
 
 abbrev HeapNode (α) := HeapNodeAux α (Heap α)
 
 variables {α : Type u}
 
-instance : Inhabited (Heap α) := ⟨Heap.empty⟩
-
 def hRank : List (HeapNode α) → Nat
   | []   => 0
   | h::_ => h.rank

src/Std/Data/HashMap.lean

@@ -124,7 +124,8 @@ def mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (nbuckets := 8)
 namespace HashMap
 variables {α : Type u} {β : Type v} [BEq α] [Hashable α]
 
-instance : Inhabited (HashMap α β) := ⟨mkHashMap⟩
+instance : Inhabited (HashMap α β) where
+  default := mkHashMap
 
 instance : EmptyCollection (HashMap α β) := ⟨mkHashMap⟩
 

src/Std/Data/HashSet.lean

@@ -116,7 +116,8 @@ def mkHashSet {α : Type u} [BEq α] [Hashable α] (nbuckets := 8) : HashSet α
 namespace HashSet
 variables {α : Type u} [BEq α] [Hashable α]
 
-instance : Inhabited (HashSet α) := ⟨mkHashSet⟩
+instance : Inhabited (HashSet α) where
+  default := mkHashSet
 
 instance : EmptyCollection (HashSet α) := ⟨mkHashSet⟩
 

src/Std/Data/PersistentArray.lean

@@ -10,11 +10,10 @@ namespace Std
 inductive PersistentArrayNode (α : Type u) where
   | node (cs : Array (PersistentArrayNode α)) : PersistentArrayNode α
   | leaf (vs : Array α)                       : PersistentArrayNode α
+  deriving Inhabited
 
 namespace PersistentArrayNode
 
-instance {α : Type u} : Inhabited (PersistentArrayNode α) := ⟨leaf #[]⟩
-
 def isNode {α} : PersistentArrayNode α → Bool
   | node _ => true
   | leaf _ => false
@@ -34,6 +33,7 @@ structure PersistentArray (α : Type u) where
   size    : Nat                   := 0
   shift   : USize                 := PersistentArray.initShift
   tailOff : Nat                   := 0
+  deriving Inhabited
 
 abbrev PArray (α : Type u) := PersistentArray α
 
@@ -47,8 +47,6 @@ def empty : PersistentArray α := {}
 
 def isEmpty (a : PersistentArray α) : Bool := a.size == 0
 
-instance : Inhabited (PersistentArray α) := ⟨{}⟩
-
 def mkEmptyArray : Array α := Array.mkEmpty branching.toNat
 
 abbrev mul2Shift (i : USize) (shift : USize) : USize := i.shiftLeft shift