From ae5aa51712f68b7152489bda7c9a79f4c14d3fe8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 8 Dec 2020 06:14:03 -0800
Subject: [PATCH] chore: add explicit `discard`

---
 src/Init/Control/Basic.lean            | 2 +-
 src/Lean/Compiler/IR/EmitC.lean        | 2 +-
 src/Lean/Elab/App.lean                 | 3 +--
 src/Lean/Elab/Binders.lean             | 2 +-
 src/Lean/Elab/BuiltinNotation.lean     | 2 +-
 src/Lean/Elab/Match.lean               | 8 +++-----
 src/Lean/Elab/StructInst.lean          | 3 +--
 src/Lean/Elab/Structure.lean           | 5 ++---
 src/Lean/Elab/Tactic/Basic.lean        | 9 ++++++---
 src/Lean/Elab/Tactic/ElabTerm.lean     | 2 +-
 src/Lean/Elab/Term.lean                | 2 +-
 src/Lean/Meta/Check.lean               | 3 +--
 src/Lean/Meta/ExprDefEq.lean           | 5 ++---
 src/Lean/Meta/Instances.lean           | 6 ++----
 src/Lean/Meta/Match/Match.lean         | 2 +-
 src/Lean/Meta/RecursorInfo.lean        | 3 +--
 src/Lean/Meta/UnificationHint.lean     | 3 +--
 src/Lean/Parser/Extension.lean         | 4 ++--
 src/Lean/ParserCompiler/Attribute.lean | 2 +-
 src/Lean/Server.lean                   | 2 +-
 20 files changed, 31 insertions(+), 39 deletions(-)

diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean
index 1dca06d9cb8e..1232b0db16ef 100644
--- a/src/Init/Control/Basic.lean
+++ b/src/Init/Control/Basic.lean
@@ -13,7 +13,7 @@ universes u v w
 
 infixr:100 " <&> " => Functor.mapRev
 
-def Functor.discard {f : Type u → Type v} {α : Type u} [Functor f] (x : f α) : f PUnit :=
+@[inline] def Functor.discard {f : Type u → Type v} {α : Type u} [Functor f] (x : f α) : f PUnit :=
   Functor.mapConst PUnit.unit x
 
 export Functor (discard)
diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean
index cfc21c255367..124dbb57215a 100644
--- a/src/Lean/Compiler/IR/EmitC.lean
+++ b/src/Lean/Compiler/IR/EmitC.lean
@@ -383,7 +383,7 @@ def toStringArgs (ys : Array Arg) : List String :=
 def emitSimpleExternalCall (f : String) (ps : Array Param) (ys : Array Arg) : M Unit := do
   emit f; emit "("
   -- We must remove irrelevant arguments to extern calls.
-  ys.size.foldM
+  discard <| ys.size.foldM
     (fun i (first : Bool) =>
       if ps[i].ty.isIrrelevant then
         pure first
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 56c6678759dc..aef7c124227a 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -336,8 +336,7 @@ private def finalize : M Expr := do
   | some expectedType =>
      trace[Elab.app.finalize]! "expected type: {expectedType}"
      -- Try to propagate expected type. Ignore if types are not definitionally equal, caller must handle it.
-     isDefEq expectedType eType
-     pure ()
+     discard <| isDefEq expectedType eType
   synthesizeAppInstMVars
   pure e
 
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index eb9970711fc5..218024efeb26 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -298,7 +298,7 @@ private def propagateExpectedType (fvar : Expr) (fvarType : Expr) (s : State) :
     let expectedType ← whnfForall expectedType
     match expectedType with
     | Expr.forallE _ d b _ =>
-      isDefEq fvarType d
+      discard <| isDefEq fvarType d
       let b := b.instantiate1 fvar
       pure { s with expectedType? := some b }
     | _ => pure { s with expectedType? := none }
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 8089e6504b00..9d6bebb51178 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -322,7 +322,7 @@ private def elabCDot (stx : Syntax) (expectedType? : Option Expr) : TermElabM Ex
   let m ← elabTerm m (← mkArrow (mkSort levelOne) (mkSort levelOne))
   let ω ← mkFreshExprMVar (mkSort levelOne)
   let stWorld ← mkAppM `STWorld #[ω, m]
-  mkInstMVar stWorld
+  discard <| mkInstMVar stWorld
   mkAppM `StateRefT' #[ω, σ, m]
 
 end Lean.Elab.Term
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 1483061cc9e3..100a83a73888 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -471,7 +471,7 @@ partial def collect : Syntax → M Syntax
       /- Recall that
          def namedPattern := check... >> tparser! "@" >> termParser -/
       let id := stx[0]
-      processVar id
+      discard <| processVar id
       let pat := stx[2]
       let pat ← collect pat
       `(namedPattern $id $pat)
@@ -521,8 +521,7 @@ def getPatternVars (patternStx : Syntax) : TermElabM (Array PatternVar) := do
 def getPatternsVars (patterns : Array Syntax) : TermElabM (Array PatternVar) := do
   let collect : CollectPatternVars.M Unit := do
     for pattern in patterns do
-      CollectPatternVars.collect (← liftMacroM $ expandMacros pattern)
-      pure ()
+      discard <| CollectPatternVars.collect (← liftMacroM $ expandMacros pattern)
   let (_, s) ← collect.run {}
   pure s.vars
 
@@ -552,8 +551,7 @@ private partial def withPatternVars {α} (pVars : Array PatternVar) (k : Array P
       decls.forM fun decl => match decl with
         | PatternVarDecl.anonymousVar mvarId fvarId => do
           let type ← inferType (mkFVar fvarId)
-          mkFreshExprMVarWithId mvarId type
-          pure ()
+          discard <| mkFreshExprMVarWithId mvarId type
         | _ => pure ()
       k decls
   loop 0 #[]
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 8057142d9c26..53e39195ff4b 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -504,8 +504,7 @@ private def propagateExpectedType (type : Expr) (numFields : Nat) (expectedType?
       | none           => pure ()
       | some typeBody =>
         unless typeBody.hasLooseBVars do
-          isDefEq expectedType typeBody
-          pure ()
+          discard <| isDefEq expectedType typeBody
 
 private def mkCtorHeader (ctorVal : ConstructorVal) (expectedType? : Option Expr) : TermElabM CtorHeaderResult := do
   let lvls ← ctorVal.lparams.mapM fun _ => mkFreshLevelMVar
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 29265db4b006..56008b70418b 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -339,8 +339,7 @@ private def withUsed {α} (scopeVars : Array Expr) (params : Array Expr) (fieldI
 
 private def levelMVarToParamFVar (fvar : Expr) : StateRefT Nat TermElabM Unit := do
   let type ← inferType fvar
-  Term.levelMVarToParam' type
-  pure ()
+  discard <| Term.levelMVarToParam' type
 
 private def levelMVarToParamFVars (fvars : Array Expr) : StateRefT Nat TermElabM Unit :=
   fvars.forM levelMVarToParamFVar
@@ -445,7 +444,7 @@ private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name ×
     defaultAuxDecls.forM fun (declName, type, value) => do
       /- The identity function is used as "marker". -/
       let value ← mkId value
-      mkAuxDefinition declName type value (zeta := true)
+      discard <| mkAuxDefinition declName type value (zeta := true)
       setReducibleAttribute declName
 
 private def elabStructureView (view : StructView) : TermElabM Unit := do
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index bc04880fc40c..4764a3e52220 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -184,7 +184,7 @@ def getMainTag : TacticM Name := do
 def ensureHasNoMVars (e : Expr) : TacticM Unit := do
   let e ← instantiateMVars e
   let pendingMVars ← getMVars e
-  Term.logUnassignedUsingErrorInfos pendingMVars
+  discard <| Term.logUnassignedUsingErrorInfos pendingMVars
   if e.hasExprMVar then
     throwError! "tactic failed, resulting expression contains metavariables{indentExpr e}"
 
@@ -244,8 +244,11 @@ def try? {α} (tactic : TacticM α) : TacticM (Option α) := do
 
 -- TODO: rename?
 def «try» {α} (tactic : TacticM α) : TacticM Bool := do
-  try tactic; pure true
-  catch _ => pure false
+  try
+    discard tactic
+    pure true
+  catch _ =>
+    pure false
 
 /--
   Use `parentTag` to tag untagged goals at `newGoals`.
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index 5788a603581b..44fe4a922046 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -48,7 +48,7 @@ def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix :
     else
       let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← getMVarDecl mvarId).kind.isNatural
       let syntheticMVarIds ← newMVarIds.filterM fun mvarId => return !(← getMVarDecl mvarId).kind.isNatural
-      Term.logUnassignedUsingErrorInfos naturalMVarIds
+      discard <| Term.logUnassignedUsingErrorInfos naturalMVarIds
       pure syntheticMVarIds.toList
   tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds
   pure (val, newMVarIds)
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index d0a19c39981d..4fc38d77f9c6 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1264,7 +1264,7 @@ def resolveName (n : Name) (preresolved : List (Name × List String)) (explicitL
 private def mkFreshTypeMVarFor (expectedType? : Option Expr) : TermElabM Expr := do
   let typeMVar ← mkFreshTypeMVar MetavarKind.synthetic
   match expectedType? with
-  | some expectedType => isDefEq expectedType typeMVar; pure ()
+  | some expectedType => discard <| isDefEq expectedType typeMVar
   | _                 => pure ()
   return typeMVar
 
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index 2dcfba5a2648..95eb569cfa4b 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -14,8 +14,7 @@ whether terms produced by tactics and `isDefEq` are type correct.
 namespace Lean.Meta
 
 private def ensureType (e : Expr) : MetaM Unit := do
-  getLevel e
-  pure ()
+  discard <| getLevel e
 
 def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
   let lctx ← getLCtx
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index fe54a3419c56..085515389ba4 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -166,9 +166,8 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
         let a₂   := args₂[i]
         let info := finfo.paramInfo[i]
         if info.instImplicit then
-          trySynthPending a₁
-          trySynthPending a₂
-          pure ()
+          discard <| trySynthPending a₁
+          discard <| trySynthPending a₂
         withAtLeastTransparency TransparencyMode.default $ Meta.isExprDefEqAux a₁ a₂
     else
       pure false
diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
index 33f314884a2e..ef29050ed32c 100644
--- a/src/Lean/Meta/Instances.lean
+++ b/src/Lean/Meta/Instances.lean
@@ -56,8 +56,7 @@ builtin_initialize
     descr := "type class instance"
     add   := fun declName args attrKind => do
       if args.hasArgs then throwError "invalid attribute 'instance', unexpected argument"
-      addInstance declName attrKind |>.run {} {}
-      return ()
+      discard <| addInstance declName attrKind |>.run {} {}
   }
 
 @[export lean_is_instance]
@@ -123,8 +122,7 @@ builtin_initialize
         else
           throwErrorAt args "too many arguments at attribute 'defaultInstance', numeral expected"
       unless kind == AttributeKind.global do throwError "invalid attribute 'defaultInstance', must be global"
-      addDefaultInstance declName prio |>.run {} {}
-      pure ()
+      discard <| addDefaultInstance declName prio |>.run {} {}
   }
 
 def getDefaultInstancesPriorities [Monad m] [MonadEnv m] : m PrioritySet :=
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index fbabd19d7be8..d551ce2c0f88 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -589,7 +589,7 @@ def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss :
     let matcher ← mkAuxDefinition matcherName type val (compile := generateMatcherCode (← getOptions))
     trace[Meta.Match.debug]! "matcher levels: {matcher.getAppFn.constLevels!}, uElim: {uElimGen}"
     let uElimPos? ← getUElimPos? matcher.getAppFn.constLevels! uElimGen
-    isLevelDefEq uElimGen uElim
+    discard <| isLevelDefEq uElimGen uElim
     addMatcherInfo matcherName { numParams := matcher.getAppNumArgs, numDiscrs := numDiscrs, altNumParams := minors.map Prod.snd, uElimPos? := uElimPos? }
     setInlineAttribute matcherName
     trace[Meta.Match.debug]! "matcher: {matcher}"
diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean
index e78134446bef..70f23fdb3ebd 100644
--- a/src/Lean/Meta/RecursorInfo.lean
+++ b/src/Lean/Meta/RecursorInfo.lean
@@ -270,8 +270,7 @@ builtin_initialize recursorAttribute : ParametricAttribute Nat ←
     descr := "user defined recursor, numerical parameter specifies position of the major premise",
     getParam := fun _ stx => ofExcept $ syntaxToMajorPos stx,
     afterSet := fun declName majorPos => do
-      (mkRecursorInfoCore declName (some majorPos)).run'
-      pure ()
+      discard <| mkRecursorInfoCore declName (some majorPos) |>.run'
   }
 
 def getMajorPos? (env : Environment) (declName : Name) : Option Nat :=
diff --git a/src/Lean/Meta/UnificationHint.lean b/src/Lean/Meta/UnificationHint.lean
index 49415657296b..40f163e34adc 100644
--- a/src/Lean/Meta/UnificationHint.lean
+++ b/src/Lean/Meta/UnificationHint.lean
@@ -85,8 +85,7 @@ builtin_initialize
     descr := "unification hint"
     add   := fun declName args kind => do
       if args.hasArgs then throwError "invalid attribute 'unificationHint', unexpected argument"
-      addUnificationHint declName kind |>.run
-      pure ()
+      discard <| addUnificationHint declName kind |>.run
   }
 
 def tryUnificationHints (t s : Expr) : MetaM Bool := do
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 28035f27210c..00a46de11c50 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -376,8 +376,8 @@ def categoryParserFnImpl (catName : Name) : ParserFn := fun ctx s =>
 def addToken (env : Environment) (tk : Token) : Except String Environment := do
   -- Recall that `ParserExtension.addEntry` is pure, and assumes `addTokenConfig` does not fail.
   -- So, we must run it here to handle exception.
-  addTokenConfig (parserExtension.getState env).tokens tk
-  pure $ parserExtension.addEntry env <| ParserExtension.Entry.token tk
+  discard <| addTokenConfig (parserExtension.getState env).tokens tk
+  return parserExtension.addEntry env <| ParserExtension.Entry.token tk
 
 def addSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Environment :=
   parserExtension.addEntry env <| ParserExtension.Entry.kind k
diff --git a/src/Lean/ParserCompiler/Attribute.lean b/src/Lean/ParserCompiler/Attribute.lean
index a9703252ac51..56386d8eb214 100644
--- a/src/Lean/ParserCompiler/Attribute.lean
+++ b/src/Lean/ParserCompiler/Attribute.lean
@@ -31,7 +31,7 @@ def registerCombinatorAttribute (name : Name) (descr : String)
       let env ← getEnv
       match attrParamSyntaxToIdentifier args with
       | some parserDeclName => do
-        getConstInfo parserDeclName
+        discard <| getConstInfo parserDeclName
         setEnv <| ext.addEntry env (parserDeclName, decl)
       | none            => throwError! "invalid [{name}] argument, expected identifier"
   }
diff --git a/src/Lean/Server.lean b/src/Lean/Server.lean
index df3c28416b35..f2180ff591c2 100644
--- a/src/Lean/Server.lean
+++ b/src/Lean/Server.lean
@@ -229,7 +229,7 @@ def initAndRunServer (i o : FS.Stream) : IO Unit := do
       { capabilities := mkLeanServerCapabilities,
         serverInfo? := some { name := "Lean 4 server",
                               version? := "0.0.1" } : InitializeResult }
-    readLspNotificationAs "initialized" InitializedParams
+    discard <| readLspNotificationAs "initialized" InitializedParams
     mainLoop ()
     let Message.notification "exit" none ← readLspMessage
       | throw (userError "Expected an Exit Notification.")