From 40ecbb7cbce55d415faa71b8161ee7c540744e21 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 May 2019 09:33:17 -0700
Subject: [PATCH] feat(library/init/control/monad): mark `monadInhabited` as an
 instance

---
 library/init/control/monad.lean               | 6 ++----
 library/init/data/array/basic.lean            | 4 ----
 library/init/lean/compiler/ir/borrow.lean     | 2 --
 library/init/lean/compiler/ir/boxing.lean     | 1 -
 library/init/lean/compiler/ir/checker.lean    | 2 --
 library/init/lean/compiler/ir/emitcpp.lean    | 1 -
 library/init/lean/compiler/ir/emitutil.lean   | 1 -
 library/init/lean/compiler/ir/livevars.lean   | 2 --
 library/init/lean/compiler/ir/normids.lean    | 4 ----
 library/init/lean/compiler/ir/rc.lean         | 2 --
 library/init/lean/compiler/ir/resetreuse.lean | 1 -
 library/init/lean/parser/syntax.lean          | 1 -
 12 files changed, 2 insertions(+), 25 deletions(-)

diff --git a/library/init/control/monad.lean b/library/init/control/monad.lean
index 603d2882ec..34c4e85b19 100644
--- a/library/init/control/monad.lean
+++ b/library/init/control/monad.lean
@@ -27,11 +27,9 @@ class Monad (m : Type u → Type v) extends Applicative m, HasBind m : Type (max
 (seqLeft  := λ α β x y, x >>= λ a, y >>= λ _, pure a)
 (seqRight := λ α β x y, x >>= λ _, y)
 
-/- We do not add these instances by default because they are rarely needed,
-   and could slow down the current type class resolution procedure. -/
-
-def monadInhabited {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabited (m α) :=
+instance monadInhabited {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabited (m α) :=
 ⟨pure $ default _⟩
 
+/- Alternative instance -/
 def monadInhabited' {α : Type u} {m : Type u → Type v} [Monad m] : Inhabited (α → m α) :=
 ⟨pure⟩
diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean
index 462fd7398d..a6a498934c 100644
--- a/library/init/data/array/basic.lean
+++ b/library/init/data/array/basic.lean
@@ -172,8 +172,6 @@ miterate₂Aux a₁ a₂ f 0 b
 @[inline] def mfoldl₂ (f : β → α → σ → m β) (b : β) (a₁ : Array α) (a₂ : Array σ): m β :=
 miterate₂ a₁ a₂ b (λ _ a₁ a₂ b, f b a₁ a₂)
 
-local attribute [instance] monadInhabited
-
 -- TODO(Leo): justify termination using wf-rec
 @[specialize] partial def mfindAux (a : Array α) (f : α → m (Option β)) : Nat → m (Option β)
 | i :=
@@ -213,7 +211,6 @@ Id.run $ mfindAux a f 0
 
 section
 variables {m : Type → Type v} [Monad m]
-local attribute [instance] monadInhabited
 
 @[specialize] partial def anyMAux (a : Array α) (p : α → m Bool) : Nat → m Bool
 | i :=
@@ -307,7 +304,6 @@ as.foldl (λ bs a, bs.push (f a)) (mkEmpty as.size)
 
 section
 variables {m : Type u → Type u} [Monad m]
-local attribute [instance] monadInhabited
 
 @[specialize]
 partial def mforAux {α : Type w} {β : Type u} (f : α → m β) (a : Array α) : Nat → m PUnit
diff --git a/library/init/lean/compiler/ir/borrow.lean b/library/init/lean/compiler/ir/borrow.lean
index ba5b524782..81d9d3d7b1 100644
--- a/library/init/lean/compiler/ir/borrow.lean
+++ b/library/init/lean/compiler/ir/borrow.lean
@@ -45,8 +45,6 @@ let fmts := map.fold (λ fmt k ps,
 instance : HasFormat ParamMap := ⟨ParamMap.fmt⟩
 instance : HasToString ParamMap := ⟨λ m, Format.pretty (format m)⟩
 
-local attribute [instance] monadInhabited
-
 namespace InitParamMap
 
 /- Mark parameters that take a reference as borrow -/
diff --git a/library/init/lean/compiler/ir/boxing.lean b/library/init/lean/compiler/ir/boxing.lean
index 2f6b74c487..8f77a6d863 100644
--- a/library/init/lean/compiler/ir/boxing.lean
+++ b/library/init/lean/compiler/ir/boxing.lean
@@ -27,7 +27,6 @@ Assumptions:
 - This transformation is applied after `reset` and `reuse` instructions have been added.
   Reason: `resetreuse.lean` ignores `box` and `unbox` instructions.
 -/
-local attribute [instance] monadInhabited
 
 /- Infer scrutinee type using `case` alternatives.
    This can be done whenever `alts` does not contain an `Alt.default _` value. -/
diff --git a/library/init/lean/compiler/ir/checker.lean b/library/init/lean/compiler/ir/checker.lean
index 377102931d..776bf8a13b 100644
--- a/library/init/lean/compiler/ir/checker.lean
+++ b/library/init/lean/compiler/ir/checker.lean
@@ -72,8 +72,6 @@ do ctx ← read,
       pure $ ctx.addParam p) ctx,
    adaptReader (λ _, ctx) k
 
-local attribute [instance] monadInhabited
-
 partial def checkFnBody : FnBody → M Unit
 | (FnBody.vdecl x t v b)    := do
   checkExpr t v,
diff --git a/library/init/lean/compiler/ir/emitcpp.lean b/library/init/lean/compiler/ir/emitcpp.lean
index 6f070f8c95..1e61c27fd3 100644
--- a/library/init/lean/compiler/ir/emitcpp.lean
+++ b/library/init/lean/compiler/ir/emitcpp.lean
@@ -12,7 +12,6 @@ import init.lean.compiler.ir.emitutil
 namespace Lean
 namespace IR
 namespace EmitCpp
-local attribute [instance] monadInhabited
 
 def leanMainFn := "_lean_main"
 
diff --git a/library/init/lean/compiler/ir/emitutil.lean b/library/init/lean/compiler/ir/emitutil.lean
index ca07d8b0da..624f18e6e8 100644
--- a/library/init/lean/compiler/ir/emitutil.lean
+++ b/library/init/lean/compiler/ir/emitutil.lean
@@ -11,7 +11,6 @@ import init.lean.compiler.ir.compilerm
 
 namespace Lean
 namespace IR
-local attribute [instance] monadInhabited
 
 namespace UsesLeanNamespace
 
diff --git a/library/init/lean/compiler/ir/livevars.lean b/library/init/lean/compiler/ir/livevars.lean
index 49a0a6c492..9e8ca88f5c 100644
--- a/library/init/lean/compiler/ir/livevars.lean
+++ b/library/init/lean/compiler/ir/livevars.lean
@@ -46,8 +46,6 @@ abbrev M := State LocalContext
 @[inline] def visitArgs (w : Index) (as : Array Arg) : M Bool := pure (HasIndex.visitArgs w as)
 @[inline] def visitExpr (w : Index) (e : Expr) : M Bool := pure (HasIndex.visitExpr w e)
 
-local attribute [instance] monadInhabited
-
 partial def visitFnBody (w : Index) : FnBody → M Bool
 | (FnBody.vdecl x _ v b)    := visitExpr w v <||> visitFnBody b
 | (FnBody.jdecl j ys v b)   := visitFnBody v <||> visitFnBody b
diff --git a/library/init/lean/compiler/ir/normids.lean b/library/init/lean/compiler/ir/normids.lean
index 56fc8dfb71..4f81c69be8 100644
--- a/library/init/lean/compiler/ir/normids.lean
+++ b/library/init/lean/compiler/ir/normids.lean
@@ -22,8 +22,6 @@ do found ← get,
 def checkParams (ps : Array Param) : M Bool :=
 ps.allM $ λ p, checkId p.x.idx
 
-local attribute [instance] monadInhabited
-
 partial def checkFnBody : FnBody → M Bool
 | (FnBody.vdecl x _ _ b)  := checkId x.idx <&&> checkFnBody b
 | (FnBody.jdecl j ys _ b) := checkId j.idx <&&> checkParams ys <&&> checkFnBody b
@@ -99,8 +97,6 @@ abbrev N := ReaderT IndexRenaming (State Nat)
 instance MtoN {α} : HasCoe (M α) (N α) :=
 ⟨λ x m, pure $ x m⟩
 
-local attribute [instance] monadInhabited
-
 partial def normFnBody : FnBody → N FnBody
 | (FnBody.vdecl x t v b)     := do v ← normExpr v, withVar x $ λ x, FnBody.vdecl x t v <$> normFnBody b
 | (FnBody.jdecl j ys v b)    := do
diff --git a/library/init/lean/compiler/ir/rc.lean b/library/init/lean/compiler/ir/rc.lean
index 5b7f8ea86a..a3d32130e6 100644
--- a/library/init/lean/compiler/ir/rc.lean
+++ b/library/init/lean/compiler/ir/rc.lean
@@ -15,8 +15,6 @@ namespace ExplicitRC
    that introduce the instructions `release` and `set`
 -/
 
-local attribute [instance] monadInhabited
-
 structure VarInfo :=
 (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
diff --git a/library/init/lean/compiler/ir/resetreuse.lean b/library/init/lean/compiler/ir/resetreuse.lean
index 5585a3526b..50dcbeb612 100644
--- a/library/init/lean/compiler/ir/resetreuse.lean
+++ b/library/init/lean/compiler/ir/resetreuse.lean
@@ -56,7 +56,6 @@ private partial def S (w : VarId) (c : CtorInfo) : FnBody → FnBody
 
 /- We use `Context` to track join points in scope. -/
 abbrev M := ReaderT LocalContext (StateT Index Id)
-local attribute [instance] monadInhabited
 
 private def mkFresh : M VarId :=
 do idx ← getModify (+1),
diff --git a/library/init/lean/parser/syntax.lean b/library/init/lean/parser/syntax.lean
index a992adc41d..7d30188424 100644
--- a/library/init/lean/parser/syntax.lean
+++ b/library/init/lean/parser/syntax.lean
@@ -127,7 +127,6 @@ def isOfKind (k : SyntaxNodeKind) : Syntax → Bool
 
 section
 variables {m : Type → Type} [Monad m] (r : Syntax → m (Option Syntax))
-local attribute [instance] monadInhabited
 
 partial def mreplace : Syntax → m Syntax
 | stx@(rawNode n) := do