fix: remove Inhabited Environment instance

src/Init/Data/Array/QSort.lean

@@ -8,9 +8,9 @@ import Init.Data.Array.Basic
 
 namespace Array
 -- TODO: remove the [Inhabited α] parameters as soon as we have the tactic framework for automating proof generation and using Array.fget
--- TODO: remove `partial` using well-founded recursion
 
-@[inline] def qpartition {α : Type} [Inhabited α] (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat × Array α :=
+def qpartition (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat × Array α :=
+  if h : as.size = 0 then (0, as) else have : Inhabited α := ⟨as[0]'(by revert h; cases as.size <;> simp [Nat.zero_lt_succ])⟩ -- TODO: remove
   let mid := (lo + hi) / 2
   let as  := if lt (as.get! mid) (as.get! lo) then as.swap! lo mid else as
   let as  := if lt (as.get! hi)  (as.get! lo) then as.swap! lo hi  else as
@@ -29,7 +29,7 @@ namespace Array
   loop as lo lo
 termination_by _ => hi - j
 
-@[inline] partial def qsort {α : Type} [Inhabited α] (as : Array α) (lt : α → α → Bool) (low := 0) (high := as.size - 1) : Array α :=
+@[inline] partial def qsort (as : Array α) (lt : α → α → Bool) (low := 0) (high := as.size - 1) : Array α :=
   let rec @[specialize] sort (as : Array α) (low high : Nat) :=
     if low < high then
       let p := qpartition as lt low high;

src/Lean/CoreM.lean

@@ -46,7 +46,6 @@ structure State where
   messages        : MessageLog     := {}
   /-- Info tree. We have the info tree here because we want to update it while adding attributes. -/
   infoState       : Elab.InfoState := {}
-  deriving Inhabited
 
 /-- Context for the CoreM monad. -/
 structure Context where

src/Lean/Elab/App.lean

@@ -1428,12 +1428,14 @@ private def mergeFailures (failures : Array (TermElabResult Expr)) : TermElabM
 
 private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array Arg) (ellipsis : Bool) (expectedType? : Option Expr) : TermElabM Expr := do
   let candidates ← elabAppFn f [] namedArgs args expectedType? (explicit := false) (ellipsis := ellipsis) (overloaded := false) #[]
-  if candidates.size == 1 then
-    applyResult candidates[0]!
+  if h : candidates.size = 1 then
+    have : 0 < candidates.size := by rw [h]; decide
+    applyResult candidates[0]
   else
     let successes ← getSuccesses candidates
-    if successes.size == 1 then
-      applyResult successes[0]!
+    if h : successes.size = 1 then
+      have : 0 < successes.size := by rw [h]; decide
+      applyResult successes[0]
     else if successes.size > 1 then
       let msgs : Array MessageData ← successes.mapM fun success => do
         match success with

src/Lean/Elab/Command.lean

@@ -32,7 +32,6 @@ structure State where
   ngen           : NameGenerator := {}
   infoState      : InfoState := {}
   traceState     : TraceState := {}
-  deriving Inhabited
 
 structure Context where
   fileName       : String

src/Lean/Elab/InfoTree/Types.lean

@@ -23,7 +23,6 @@ structure ContextInfo where
   currNamespace : Name           := Name.anonymous
   openDecls     : List OpenDecl  := []
   ngen          : NameGenerator -- We must save the name generator to implement `ContextInfo.runMetaM` and making we not create `MVarId`s used in `mctx`.
-  deriving Inhabited
 
 /-- Base structure for `TermInfo`, `CommandInfo` and `TacticInfo`. -/
 structure ElabInfo where

src/Lean/Elab/Term.lean

@@ -131,7 +131,6 @@ structure Snapshot where
   term   : Term.State
   tactic : Tactic.State
   stx    : Syntax
-  deriving Inhabited
 
 /--
   Key for the cache used to implement the `save` tactic.
@@ -242,7 +241,6 @@ instance : Inhabited (TermElabM α) where
 structure SavedState where
   meta   : Meta.SavedState
   «elab» : State
-  deriving Inhabited
 
 protected def saveState : TermElabM SavedState :=
   return { meta := (← Meta.saveState), «elab» := (← get) }
@@ -262,9 +260,6 @@ instance : MonadBacktrack SavedState TermElabM where
 
 abbrev TermElabResult (α : Type) := EStateM.Result Exception SavedState α
 
-instance [Inhabited α] : Inhabited (TermElabResult α) where
-  default := EStateM.Result.ok default default
-
 /--
   Execute `x`, save resulting expression and new state.
   We remove any `Info` created by `x`.

src/Lean/Environment.lean

@@ -24,7 +24,7 @@ def ModuleIdx := Nat
 
 abbrev ModuleIdx.toNat (midx : ModuleIdx) : Nat := midx
 
-instance : Inhabited ModuleIdx := inferInstanceAs (Inhabited Nat)
+instance : Inhabited ModuleIdx where default := (0 : Nat)
 
 abbrev ConstMap := SMap Name ConstantInfo
 
@@ -143,7 +143,9 @@ structure Environment where
   extraConstNames : NameSet
   /-- The header contains additional information that is not updated often. -/
   header       : EnvironmentHeader := {}
-  deriving Inhabited
+
+instance : Nonempty Environment :=
+  ⟨by refine' {..} <;> exact default⟩
 
 namespace Environment
 
@@ -299,6 +301,7 @@ unsafe def setState {σ} (ext : Ext σ) (env : Environment) (s : σ) : Environme
   if h : ext.idx < env.extensions.size then
     { env with extensions := env.extensions.set ⟨ext.idx, h⟩ (unsafeCast s) }
   else
+    have : Inhabited Environment := ⟨env⟩
     panic! invalidExtMsg
 
 @[inline] unsafe def modifyState {σ : Type} (ext : Ext σ) (env : Environment) (f : σ → σ) : Environment :=
@@ -309,6 +312,7 @@ unsafe def setState {σ} (ext : Ext σ) (env : Environment) (s : σ) : Environme
         let s : σ := f s
         unsafeCast s }
   else
+    have : Inhabited Environment := ⟨env⟩
     panic! invalidExtMsg
 
 unsafe def getState {σ} [Inhabited σ] (ext : Ext σ) (env : Environment) : σ :=
@@ -555,6 +559,7 @@ instance : Inhabited TagDeclarationExtension :=
   inferInstanceAs (Inhabited (SimplePersistentEnvExtension Name NameSet))
 
 def tag (ext : TagDeclarationExtension) (env : Environment) (declName : Name) : Environment :=
+  have : Inhabited Environment := ⟨env⟩
   assert! env.getModuleIdxFor? declName |>.isNone -- See comment at `TagDeclarationExtension`
   ext.addEntry env declName
 
@@ -584,6 +589,7 @@ instance : Inhabited (MapDeclarationExtension α) :=
   inferInstanceAs (Inhabited (SimplePersistentEnvExtension ..))
 
 def insert (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (val : α) : Environment :=
+  have : Inhabited Environment := ⟨env⟩
   assert! env.getModuleIdxFor? declName |>.isNone -- See comment at `MapDeclarationExtension`
   ext.addEntry env (declName, val)
 

src/Lean/Meta/Basic.lean

@@ -261,7 +261,6 @@ structure State where
 structure SavedState where
   core        : Core.State
   meta        : State
-  deriving Inhabited
 
 /--
   Contextual information for the `MetaM` monad.

src/Lean/Server/FileWorker.lean

@@ -90,7 +90,7 @@ section Elab
       : AsyncElabM (Option Snapshot) := do
     cancelTk.check
     let s ← get
-    let lastSnap := s.snaps.back
+    let .some lastSnap := s.snaps.back? | panic! "empty snapshots"
     if lastSnap.isAtEnd then
       publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
       publishProgressDone m ctx.hOut
@@ -123,7 +123,7 @@ section Elab
   def unfoldCmdSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken) (startAfterMs : UInt32)
       : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
     let ctx ← read
-    let headerSnap := snaps[0]!
+    let some headerSnap := snaps[0]? | panic! "empty snapshots"
     if headerSnap.msgLog.hasErrors then
       -- Treat header processing errors as fatal so users aren't swamped with
       -- followup errors
@@ -290,17 +290,16 @@ section Updates
         cancelTk.check
         IO.Process.exit 2
     else EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) (prio := .dedicated) fun headSnap?? => do
-      let headSnap? ← MonadExcept.ofExcept headSnap??
       -- There is always at least one snapshot absent exceptions
-      let headSnap := headSnap?.get!
+      let some headSnap ← MonadExcept.ofExcept headSnap?? | panic! "empty snapshots"
       let newHeaderSnap := { headSnap with stx := newHeaderStx, mpState := newMpState }
       let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source
       -- Ignore exceptions, we are only interested in the successful snapshots
       let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix
       -- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only
       -- when really necessary, we could do a whitespace-aware `Syntax` comparison instead.
-      let mut validSnaps := cmdSnaps.takeWhile (fun s => s.endPos < changePos)
-      if validSnaps.length ≤ 1 then
+      let mut validSnaps ← pure (cmdSnaps.takeWhile (fun s => s.endPos < changePos))
+      if h : validSnaps.length ≤ 1 then
         validSnaps := [newHeaderSnap]
       else
         /- When at least one valid non-header snap exists, it may happen that a change does not fall
@@ -308,10 +307,12 @@ section Updates
            We check for this here. We do not currently handle crazy grammars in which an appended
            token can merge two or more previous commands into one. To do so would require reparsing
            the entire file. -/
-        let mut lastSnap := validSnaps.getLast!
-        let preLastSnap := if validSnaps.length ≥ 2
-          then validSnaps.get! (validSnaps.length - 2)
-          else newHeaderSnap
+        have : validSnaps.length ≥ 2 := Nat.gt_of_not_le h
+        let mut lastSnap := validSnaps.getLast (by subst ·; simp at h)
+        let preLastSnap :=
+          have : 0 < validSnaps.length := Nat.lt_of_lt_of_le (by decide) this
+          have : validSnaps.length - 2 < validSnaps.length := Nat.sub_lt this (by decide)
+          validSnaps[validSnaps.length - 2]
         let newLastStx ← parseNextCmd newMeta.mkInputContext preLastSnap
         if newLastStx != lastSnap.stx then
           validSnaps := validSnaps.dropLast

src/Lean/Server/References.lean

@@ -21,7 +21,6 @@ structure Reference where
   ci : ContextInfo
   info : Info
   isBinder : Bool
-  deriving Inhabited
 
 structure RefInfo where
   definition : Option Reference

src/Lean/Server/Snapshots.lean

@@ -39,16 +39,6 @@ structure Snapshot where
   interactiveDiags : PersistentArray Widget.InteractiveDiagnostic
   tacticCache : IO.Ref Tactic.Cache
 
-instance : Inhabited Snapshot where
-  default := {
-    beginPos         := default
-    stx              := default
-    mpState          := default
-    cmdState         := default
-    interactiveDiags := default
-    tacticCache      := dummyTacticCache
-  }
-
 namespace Snapshot
 
 def endPos (s : Snapshot) : String.Pos :=

src/Lean/Widget/Basic.lean

@@ -18,7 +18,7 @@ functionality is purpose-specific to showing the contents of infoview popups.
 structure InfoWithCtx where
   ctx  : Elab.ContextInfo
   info : Elab.Info
-  deriving Inhabited, TypeName
+  deriving TypeName
 
 deriving instance TypeName for MessageData
 

src/Lean/Widget/InteractiveCode.lean

@@ -36,7 +36,7 @@ structure SubexprInfo where
   -- kind : Lsp.SymbolKind
   /-- Ask the renderer to highlight this node in the given color. -/
   diffStatus? : Option DiffTag := none
-  deriving Inhabited, RpcEncodable
+  deriving RpcEncodable
 
 /-- Pretty-printed syntax (usually but not necessarily an `Expr`) with embedded `Info`s. -/
 abbrev CodeWithInfos := TaggedText SubexprInfo

src/lake

@@ -1 +1 @@
-Subproject commit 5a54cfe4272046ef770c1a00eb26d60e772f4e89
+Subproject commit d0b530530f14dde97a547b03abf87eee06360d60