fix(*): make RelaxedImplicit default inferred implicit kind (#175)

library/data/buffer/parser.lean

@@ -19,7 +19,7 @@ variables {α β γ : Type}
 protected def bind (p : parser α) (f : α → parser β) : parser β :=
 λ input pos, match p input pos with
 | parse_result.done pos a           := f a input pos
-| parse_result.fail ._ pos expected := parse_result.fail β pos expected
+| parse_result.fail pos expected := parse_result.fail pos expected
 end
 
 protected def pure (a : α) : parser α :=
@@ -45,7 +45,7 @@ all_goals {refl}
 end
 
 protected def fail (msg : string) : parser α :=
-λ _ pos, parse_result.fail α pos (dlist.singleton msg)
+λ _ pos, parse_result.fail pos (dlist.singleton msg)
 
 instance : monad parser :=
 { pure := @parser.pure, bind := @parser.bind }
@@ -59,20 +59,20 @@ instance : monad_fail parser :=
 { fail := @parser.fail, ..parser.monad }
 
 protected def failure : parser α :=
-λ _ pos, parse_result.fail α pos dlist.empty
+λ _ pos, parse_result.fail pos dlist.empty
 
 protected def orelse (p q : parser α) : parser α :=
 λ input pos, match p input pos with
-| parse_result.fail ._ pos₁ expected₁ :=
-  if pos₁ ≠ pos then parse_result.fail _ pos₁ expected₁ else
+| parse_result.fail pos₁ expected₁ :=
+  if pos₁ ≠ pos then parse_result.fail pos₁ expected₁ else
   match q input pos with
-  | parse_result.fail ._ pos₂ expected₂ :=
+  | parse_result.fail pos₂ expected₂ :=
     if pos₁ < pos₂ then
-      parse_result.fail _ pos₁ expected₁
+      parse_result.fail pos₁ expected₁
     else if pos₂ < pos₁ then
-      parse_result.fail _ pos₂ expected₂
+      parse_result.fail pos₂ expected₂
     else -- pos₁ = pos₂
-      parse_result.fail _ pos₁ (expected₁ ++ expected₂)
+      parse_result.fail pos₁ (expected₁ ++ expected₂)
   | ok := ok
   end
   | ok := ok
@@ -88,8 +88,8 @@ instance : inhabited (parser α) :=
 /-- Overrides the expected token name, and does not consume input on failure. -/
 def decorate_errors (msgs : thunk (list string)) (p : parser α) : parser α :=
 λ input pos, match p input pos with
-| parse_result.fail ._ _ expected :=
-  parse_result.fail _  pos (dlist.lazy_of_list (msgs ()))
+| parse_result.fail _ expected :=
+  parse_result.fail pos (dlist.lazy_of_list (msgs ()))
 | ok := ok
 end
 
@@ -105,9 +105,9 @@ if h : pos < input.size then
   if p c then
     parse_result.done (pos+1) $ input.read ⟨pos, h⟩
   else
-    parse_result.fail _ pos dlist.empty
+    parse_result.fail pos dlist.empty
 else
-  parse_result.fail _ pos dlist.empty
+  parse_result.fail pos dlist.empty
 
 /-- Matches the empty word. -/
 def eps : parser unit := return ()
@@ -212,7 +212,7 @@ left_ctx.map (λ _, ' ') ++ "^\n".to_char_buffer ++
 def run (p : parser α) (input : char_buffer) : sum string α :=
 match (p <* eof) input 0 with
 | parse_result.done pos res := sum.inr res
-| parse_result.fail ._ pos expected :=
+| parse_result.fail pos expected :=
   sum.inl $ buffer.to_string $ mk_error_msg input pos expected
 end
 

library/data/lazy_list.lean

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 universes u v w
 
 inductive lazy_list (α : Type u) : Type u
-| nil {} : lazy_list
+| nil : lazy_list
 | cons (hd : α) (tl : thunk lazy_list) : lazy_list
 
 namespace lazy_list

library/init/algebra/classes.lean

@@ -14,7 +14,7 @@ universes u v
 (comm : ∀ a b, op a b = op b a)
 
 instance is_symm_op_of_is_commutative (α : Type u) (op : α → α → α) [is_commutative α op] : is_symm_op α α op :=
-{symm_op := is_commutative.comm op}
+{symm_op := is_commutative.comm}
 
 @[algebra] class is_associative (α : Type u) (op : α → α → α) : Prop :=
 (assoc : ∀ a b c, op (op a b) c = op a (op b c))
@@ -101,7 +101,7 @@ instance is_symm_op_of_is_symm (α : Type u) (r : α → α → Prop) [is_symm 
 
 instance is_total_preorder_is_preorder (α : Type u) (r : α → α → Prop) [s : is_total_preorder α r] : is_preorder α r :=
 {trans := s.trans,
- refl  := λ a, or.elim (is_total.total r a a) id id}
+ refl  := λ a, or.elim (@is_total.total _ r _ a a) id id}
 
 @[algebra] class is_partial_order (α : Type u) (r : α → α → Prop) extends is_preorder α r, is_antisymm α r : Prop.
 
@@ -131,10 +131,10 @@ variables {α : Type u} {r : α → α → Prop}
 local infix `≺`:50 := r
 
 lemma irrefl [is_irrefl α r] (a : α) : ¬ a ≺ a :=
-is_irrefl.irrefl _ a
+is_irrefl.irrefl a
 
 lemma refl [is_refl α r] (a : α) : a ≺ a :=
-is_refl.refl _ a
+is_refl.refl a
 
 lemma trans [is_trans α r] {a b c : α} : a ≺ b → b ≺ c → a ≺ c :=
 is_trans.trans _ _ _
@@ -149,7 +149,7 @@ lemma asymm [is_asymm α r] {a b : α} : a ≺ b → ¬ b ≺ a :=
 is_asymm.asymm _ _
 
 lemma trichotomous [is_trichotomous α r] : ∀ (a b : α), a ≺ b ∨ a = b ∨ b ≺ a :=
-is_trichotomous.trichotomous r
+is_trichotomous.trichotomous
 
 lemma incomp_trans [is_incomp_trans α r] {a b c : α} : (¬ a ≺ b ∧ ¬ b ≺ a) → (¬ b ≺ c ∧ ¬ c ≺ b) → (¬ a ≺ c ∧ ¬ c ≺ a) :=
 is_incomp_trans.incomp_trans _ _ _
@@ -177,7 +177,7 @@ lemma asymm_of [is_asymm α r] {a b : α} : a ≺ b → ¬ b ≺ a := asymm
 
 @[elab_simple]
 lemma total_of [is_total α r] (a b : α) : a ≺ b ∨ b ≺ a :=
-is_total.total _ _ _
+is_total.total _ _
 
 @[elab_simple]
 lemma trichotomous_of [is_trichotomous α r] : ∀ (a b : α), a ≺ b ∨ a = b ∨ b ≺ a := trichotomous

library/init/algebra/field.lean

@@ -37,7 +37,7 @@ lemma division_def (a b : α) : a / b = a * b⁻¹ :=
 rfl
 
 @[simp] lemma inv_zero : 0⁻¹ = (0:α) :=
-division_ring.inv_zero α
+division_ring.inv_zero
 
 @[simp]
 lemma inv_mul_cancel {a : α} (h : a ≠ 0) : a⁻¹ * a = 1 :=

library/init/algebra/order.lean

@@ -37,7 +37,7 @@ preorder.le_refl
 preorder.le_trans
 
 lemma lt_iff_le_not_le [preorder α] : ∀ {a b : α}, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) :=
-preorder.lt_iff_le_not_le _
+preorder.lt_iff_le_not_le
 
 lemma lt_of_le_not_le [preorder α] : ∀ {a b : α}, a ≤ b → ¬ b ≤ a → a < b
 | a b hab hba := lt_iff_le_not_le.mpr ⟨hab, hba⟩
@@ -219,13 +219,13 @@ class decidable_linear_order (α : Type u) extends linear_order α :=
     @decidable_lt_of_decidable_le _ _ decidable_le)
 
 instance [decidable_linear_order α] (a b : α) : decidable (a < b) :=
-decidable_linear_order.decidable_lt α a b
+decidable_linear_order.decidable_lt a b
 
 instance [decidable_linear_order α] (a b : α) : decidable (a ≤ b) :=
-decidable_linear_order.decidable_le α a b
+decidable_linear_order.decidable_le a b
 
 instance [decidable_linear_order α] (a b : α) : decidable (a = b) :=
-decidable_linear_order.decidable_eq α a b
+decidable_linear_order.decidable_eq a b
 
 lemma eq_or_lt_of_not_lt [decidable_linear_order α] {a b : α} (h : ¬ a < b) : a = b ∨ b < a :=
 if h₁ : a = b then or.inl h₁

library/init/algebra/ordered_ring.lean

@@ -105,7 +105,7 @@ section linear_ordered_semiring
 variable [linear_ordered_semiring α]
 
 lemma zero_lt_one : 0 < (1:α) :=
-linear_ordered_semiring.zero_lt_one α
+linear_ordered_semiring.zero_lt_one
 
 lemma zero_le_one : 0 ≤ (1:α) :=
 le_of_lt zero_lt_one

library/init/category/alternative.lean

@@ -19,7 +19,7 @@ section
 variables {f : Type u → Type v} [alternative f] {α : Type u}
 
 @[inline] def failure : f α :=
-alternative.failure f
+alternative.failure
 /-- If the condition `p` is decided to be false, then fail, otherwise, return unit. -/
 @[inline] def guard {f : Type → Type v} [alternative f] (p : Prop) [decidable p] : f unit :=
 if p then pure () else failure

library/init/category/applicative.lean

@@ -9,7 +9,7 @@ open function
 universes u v
 
 class has_pure (f : Type u → Type v) :=
-(pure {} {α : Type u} : α → f α)
+(pure {α : Type u} : α → f α)
 
 export has_pure (pure)
 

library/init/category/except.lean

@@ -11,8 +11,8 @@ import init.category.alternative init.category.lift
 universes u v w
 
 inductive except (ε : Type u) (α : Type v)
-| error {} : ε → except
-| ok {} : α → except
+| error : ε → except
+| ok : α → except
 
 namespace except
 section
@@ -97,8 +97,8 @@ end except_t
 
 /-- An implementation of [MonadError](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Except.html#t:MonadError) -/
 class monad_except (ε : out_param (Type u)) (m : Type v → Type w) :=
-(throw {} {α : Type v} : ε → m α)
-(catch {} {α : Type v} : m α → (ε → m α) → m α)
+(throw {α : Type v} : ε → m α)
+(catch {α : Type v} : m α → (ε → m α) → m α)
 
 namespace monad_except
 variables {ε : Type u} {m : Type v → Type w}
@@ -123,11 +123,11 @@ instance (m ε) [monad m] : monad_except ε (except_t ε m) :=
     Note: This class can be seen as a simplification of the more "principled" definition
     ```
     class monad_except_functor (ε ε' : out_param (Type u)) (n n' : Type u → Type u) :=
-    (map {} {α : Type u} : (∀ {m : Type u → Type u} [monad m], except_t ε m α → except_t ε' m α) → n α → n' α)
+    (map {α : Type u} : (∀ {m : Type u → Type u} [monad m], except_t ε m α → except_t ε' m α) → n α → n' α)
     ```
     -/
 class monad_except_adapter (ε ε' : out_param (Type u)) (m m' : Type u → Type v) :=
-(adapt_except {} {α : Type u} : (ε → ε') → m α → m' α)
+(adapt_except {α : Type u} : (ε → ε') → m α → m' α)
 export monad_except_adapter (adapt_except)
 
 section

library/init/category/lawful.lean

@@ -104,7 +104,7 @@ section
   @[simp] lemma run_map (f : α → β) [is_lawful_monad m] :
     (f <$> x).run st = (λ p : α × σ, (f (prod.fst p), prod.snd p)) <$> x.run st :=
   begin
-    rw ←bind_pure_comp_eq_map m,
+    rw ← bind_pure_comp_eq_map _ (x.run st),
     change (x >>= pure ∘ f).run st = _,
     simp
   end
@@ -143,7 +143,7 @@ namespace except_t
   rfl
   @[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run = except.map f <$> x.run :=
   begin
-    rw ←bind_pure_comp_eq_map m,
+    rw ← bind_pure_comp_eq_map _ x.run,
     change x.run >>= except_t.bind_cont (pure ∘ f) = _,
     apply bind_ext_congr,
     intro a; cases a; simp [except_t.bind_cont, except.map]
@@ -189,7 +189,7 @@ section
   @[simp] lemma run_bind (f : α → reader_t ρ m β) :
     (x >>= f).run r = x.run r >>= λ a, (f a).run r := rfl
   @[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run r = f <$> x.run r :=
-  by rw ←bind_pure_comp_eq_map m; refl
+  by rw ← bind_pure_comp_eq_map _ (x.run r); refl
   @[simp] lemma run_monad_lift {n} [has_monad_lift_t n m] (x : n α) :
     (monad_lift x : reader_t ρ m α).run r = (monad_lift x : m α) := rfl
   @[simp] lemma run_monad_map {m' n n'} [monad m'] [monad_functor_t n n' m m'] (f : ∀ {α}, n α → n' α) :
@@ -217,7 +217,7 @@ namespace option_t
   rfl
   @[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run = option.map f <$> x.run :=
   begin
-    rw ←bind_pure_comp_eq_map m,
+    rw ← bind_pure_comp_eq_map _ x.run,
     change x.run >>= option_t.bind_cont (pure ∘ f) = _,
     apply bind_ext_congr,
     intro a; cases a; simp [option_t.bind_cont, option.map, option.bind]

library/init/category/lift.lean

@@ -19,13 +19,13 @@ universes u v w
     but `n` does not have to be a monad transformer.
     Alternatively, an implementation of [MonadLayer](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLayer) without `layerInvmap` (so far). -/
 class has_monad_lift (m : Type u → Type v) (n : Type u → Type w) :=
-(monad_lift {} : ∀ {α}, m α → n α)
+(monad_lift : ∀ {α}, m α → n α)
 
 /-- The reflexive-transitive closure of `has_monad_lift`.
     `monad_lift` is used to transitively lift monadic computations such as `state_t.get` or `state_t.put s`.
     Corresponds to [MonadLift](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLift). -/
 class has_monad_lift_t (m : Type u → Type v) (n : Type u → Type w) :=
-(monad_lift {} : ∀ {α}, m α → n α)
+(monad_lift : ∀ {α}, m α → n α)
 
 export has_monad_lift_t (monad_lift)
 
@@ -48,13 +48,13 @@ instance has_monad_lift_t_refl (m) : has_monad_lift_t m m :=
     but not restricted to monad transformers.
     Alternatively, an implementation of [MonadTransFunctor](http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadTransFunctor). -/
 class monad_functor (m m' : Type u → Type v) (n n' : Type u → Type w) :=
-(monad_map {} {α : Type u} : (∀ {α}, m α → m' α) → n α → n' α)
+(monad_map {α : Type u} : (∀ {α}, m α → m' α) → n α → n' α)
 
 /-- The reflexive-transitive closure of `monad_functor`.
     `monad_map` is used to transitively lift monad morphisms such as `state_t.zoom`.
     A generalization of [MonadLiftFunctor](http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadLiftFunctor), which can only lift endomorphisms (i.e. m = m', n = n'). -/
 class monad_functor_t (m m' : Type u → Type v) (n n' : Type u → Type w) :=
-(monad_map {} {α : Type u} : (∀ {α}, m α → m' α) → n α → n' α)
+(monad_map {α : Type u} : (∀ {α}, m α → m' α) → n α → n' α)
 
 export monad_functor_t (monad_map)
 
@@ -78,6 +78,6 @@ instance monad_functor_t_refl (m m') : monad_functor_t m m' m m' :=
     ```
     -/
 class monad_run (out : out_param $ Type u → Type v) (m : Type u → Type v) :=
-(run {} {α : Type u} : m α → out α)
+(run {α : Type u} : m α → out α)
 
 export monad_run (run)

library/init/category/monad_fail.lean

@@ -9,7 +9,7 @@ import init.category.lift init.data.string.basic
 universes u v
 
 class monad_fail (m : Type u → Type v) :=
-(fail {} : Π {a}, string → m a)
+(fail : Π {a}, string → m a)
 
 def match_failed {α : Type u} {m : Type u → Type v} [monad_fail m] : m α :=
 monad_fail.fail "match failed"

library/init/category/reader.lean

@@ -77,11 +77,11 @@ end reader_t
     Note: This class can be seen as a simplification of the more "principled" definition
     ```
     class monad_reader (ρ : out_param (Type u)) (n : Type u → Type u) :=
-    (lift {} {α : Type u} : (∀ {m : Type u → Type u} [monad m], reader_t ρ m α) → n α)
+    (lift {α : Type u} : (∀ {m : Type u → Type u} [monad m], reader_t ρ m α) → n α)
     ```
     -/
 class monad_reader (ρ : out_param (Type u)) (m : Type u → Type v) :=
-(read {} : m ρ)
+(read : m ρ)
 
 export monad_reader (read)
 
@@ -100,11 +100,11 @@ instance {ρ : Type u} {m : Type u → Type v} [monad m] : monad_reader ρ (read
     Note: This class can be seen as a simplification of the more "principled" definition
     ```
     class monad_reader_functor (ρ ρ' : out_param (Type u)) (n n' : Type u → Type u) :=
-    (map {} {α : Type u} : (∀ {m : Type u → Type u} [monad m], reader_t ρ m α → reader_t ρ' m α) → n α → n' α)
+    (map {α : Type u} : (∀ {m : Type u → Type u} [monad m], reader_t ρ m α → reader_t ρ' m α) → n α → n' α)
     ```
     -/
 class monad_reader_adapter (ρ ρ' : out_param (Type u)) (m m' : Type u → Type v) :=
-(adapt_reader {} {α : Type u} : (ρ' → ρ) → m α → m' α)
+(adapt_reader {α : Type u} : (ρ' → ρ) → m α → m' α)
 export monad_reader_adapter (adapt_reader)
 
 section

library/init/category/state.lean

@@ -85,14 +85,14 @@ end state_t
     Note: This class can be seen as a simplification of the more "principled" definition
     ```
     class monad_state_lift (σ : out_param (Type u)) (n : Type u → Type u) :=
-    (lift {} {α : Type u} : (∀ {m : Type u → Type u} [monad m], state_t σ m α) → n α)
+    (lift {α : Type u} : (∀ {m : Type u → Type u} [monad m], state_t σ m α) → n α)
     ```
     which better describes the intent of "we can lift a `state_t` from anywhere in the monad stack".
     However, by parametricity the types `∀ m [monad m], σ → m (α × σ)` and `σ → α × σ` should be
     equivalent because the only way to obtain an `m` is through `pure`.
     -/
 class monad_state (σ : out_param (Type u)) (m : Type u → Type v) :=
-(lift {} {α : Type u} : state σ α → m α)
+(lift {α : Type u} : state σ α → m α)
 
 section
 variables {σ : Type u} {m : Type u → Type v}
@@ -147,7 +147,7 @@ end
     Note: This class can be seen as a simplification of the more "principled" definition
     ```
     class monad_state_functor (σ σ' : out_param (Type u)) (n n' : Type u → Type u) :=
-    (map {} {α : Type u} : (∀ {m : Type u → Type u} [monad m], state_t σ m α → state_t σ' m α) → n α → n' α)
+    (map {α : Type u} : (∀ {m : Type u → Type u} [monad m], state_t σ m α → state_t σ' m α) → n α → n' α)
     ```
     which better describes the intent of "we can map a `state_t` anywhere in the monad stack".
     If we look at the unfolded type of the first argument `∀ m [monad m], (σ → m (α × σ)) → σ' → m (α × σ')`, we see that it has the lens type `∀ f [functor f], (α → f α) → β → f β` with `f` specialized to `λ σ, m (α × σ)` (exercise: show that this is a lawful functor). We can build all lenses we are insterested in from the functions `split` and `join` as
@@ -157,7 +157,7 @@ end
     ```
     -/
 class monad_state_adapter (σ σ' : out_param (Type u)) (m m' : Type u → Type v) :=
-(adapt_state {} {σ'' α : Type u} (split : σ' → σ × σ'') (join : σ → σ'' → σ') : m α → m' α)
+(adapt_state {σ'' α : Type u} (split : σ' → σ × σ'') (join : σ → σ'' → σ') : m α → m' α)
 export monad_state_adapter (adapt_state)
 
 section