diff --git a/library/algebra/category/adjoint.lean b/library/algebra/category/adjoint.lean
index b8b2fa735..ec6cb8c84 100644
--- a/library/algebra/category/adjoint.lean
+++ b/library/algebra/category/adjoint.lean
@@ -21,6 +21,11 @@ namespace adjoint
 
   variables {obC obD : Type} (C : category obC) {D : category obD}
 
+  variables (f : Cᵒᵖ ×c C ⇒ C ×c C) (g : C ×c C ⇒ C ×c C)
+  check g ∘f f
+
+  check natural_transformation (Hom D)
+
   definition adjoint (F : C ⇒ D) (G : D ⇒ C) :=
   natural_transformation (@functor.compose _ _ _ _ _ _ (Hom D) sorry)
                        --(Hom C ∘f sorry)
diff --git a/library/algebra/category/basic.lean b/library/algebra/category/basic.lean
index 33bfcda9d..84cf20719 100644
--- a/library/algebra/category/basic.lean
+++ b/library/algebra/category/basic.lean
@@ -17,7 +17,7 @@ mk : Π (hom : ob → ob → Type)
          category ob
 
 namespace category
-  variables {ob : Type} {C : category ob}
+  variables {ob : Type} [C : category ob]
   variables {a b c d : ob}
   include C
   definition hom [reducible] : ob → ob → Type := rec (λ hom compose id assoc idr idl, hom) C
diff --git a/library/algebra/category/constructions.lean b/library/algebra/category/constructions.lean
index f14930f31..efaf4a043 100644
--- a/library/algebra/category/constructions.lean
+++ b/library/algebra/category/constructions.lean
@@ -58,7 +58,7 @@ namespace category
 
   section
   open decidable unit empty
-  variables {A : Type} {H : decidable_eq A}
+  variables {A : Type} [H : decidable_eq A]
   include H
   definition set_hom (a b : A) := decidable.rec_on (H a b) (λh, unit) (λh, empty)
   theorem set_hom_subsingleton [instance] (a b : A) : subsingleton (set_hom a b) := _
@@ -71,7 +71,7 @@ namespace category
       (λh f, empty.rec _ f) f)
     (λh (g : empty), empty.rec _ g) g
 
-  definition set_category (A : Type) {H : decidable_eq A} : category A :=
+  definition set_category (A : Type) [H : decidable_eq A] : category A :=
   mk (λa b, set_hom a b)
      (λ a b c g f, set_compose g f)
      (λ a, rec_on_true rfl ⋆)
diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean
index c1ced7a9a..9f5334e48 100644
--- a/library/algebra/category/morphism.lean
+++ b/library/algebra/category/morphism.lean
@@ -8,7 +8,7 @@ open eq eq.ops category
 
 namespace morphism
   section
-  variables {ob : Type} {C : category ob} include C
+  variables {ob : Type} [C : category ob] include C
   variables {a b c d : ob} {h : @hom ob C c d} {g : @hom ob C b c} {f : @hom ob C a b} {i : @hom ob C b a}
   inductive is_section    [class] (f : @hom ob C a b) : Type
   := mk : ∀{g}, g ∘ f = id → is_section f
@@ -17,37 +17,37 @@ namespace morphism
   inductive is_iso        [class] (f : @hom ob C a b) : Type
   := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
   --remove implicit arguments in above lines
-  definition retraction_of (f : hom a b) {H : is_section f} : hom b a :=
+  definition retraction_of (f : hom a b) [H : is_section f] : hom b a :=
   is_section.rec (λg h, g) H
-  definition section_of    (f : hom a b) {H : is_retraction f} : hom b a :=
+  definition section_of    (f : hom a b) [H : is_retraction f] : hom b a :=
   is_retraction.rec (λg h, g) H
-  definition inverse       (f : hom a b) {H : is_iso f} : hom b a :=
+  definition inverse       (f : hom a b) [H : is_iso f] : hom b a :=
   is_iso.rec (λg h1 h2, g) H
 
   postfix `⁻¹` := inverse
 
-  theorem inverse_compose (f : hom a b) {H : is_iso f} : f⁻¹ ∘ f = id :=
+  theorem inverse_compose (f : hom a b) [H : is_iso f] : f⁻¹ ∘ f = id :=
   is_iso.rec (λg h1 h2, h1) H
 
-  theorem compose_inverse (f : hom a b) {H : is_iso f} : f ∘ f⁻¹ = id :=
+  theorem compose_inverse (f : hom a b) [H : is_iso f] : f ∘ f⁻¹ = id :=
   is_iso.rec (λg h1 h2, h2) H
 
-  theorem retraction_compose (f : hom a b) {H : is_section f} : retraction_of f ∘ f = id :=
+  theorem retraction_compose (f : hom a b) [H : is_section f] : retraction_of f ∘ f = id :=
   is_section.rec (λg h, h) H
 
-  theorem compose_section (f : hom a b) {H : is_retraction f} : f ∘ section_of f = id :=
+  theorem compose_section (f : hom a b) [H : is_retraction f] : f ∘ section_of f = id :=
   is_retraction.rec (λg h, h) H
 
-  theorem iso_imp_retraction [instance] (f : hom a b) {H : is_iso f} : is_section f :=
+  theorem iso_imp_retraction [instance] (f : hom a b) [H : is_iso f] : is_section f :=
   is_section.mk !inverse_compose
 
-  theorem iso_imp_section [instance] (f : hom a b) {H : is_iso f} : is_retraction f :=
+  theorem iso_imp_section [instance] (f : hom a b) [H : is_iso f] : is_retraction f :=
   is_retraction.mk !compose_inverse
 
   theorem id_is_iso [instance] : is_iso (ID a) :=
   is_iso.mk !id_compose !id_compose
 
-  theorem inverse_is_iso [instance] (f : a ⟶ b) {H : is_iso f} : is_iso (f⁻¹) :=
+  theorem inverse_is_iso [instance] (f : a ⟶ b) [H : is_iso f] : is_iso (f⁻¹) :=
   is_iso.mk !compose_inverse !inverse_compose
 
   theorem left_inverse_eq_right_inverse {f : hom a b} {g g' : hom b a}
@@ -59,30 +59,30 @@ namespace morphism
      ... = id ∘ g' : {Hl}
      ... = g' : !id_left
 
-  theorem retraction_eq_intro {H : is_section f} (H2 : f ∘ i = id) : retraction_of f = i
+  theorem retraction_eq_intro [H : is_section f] (H2 : f ∘ i = id) : retraction_of f = i
   := left_inverse_eq_right_inverse !retraction_compose H2
 
-  theorem section_eq_intro {H : is_retraction f} (H2 : i ∘ f = id) : section_of f = i
+  theorem section_eq_intro [H : is_retraction f] (H2 : i ∘ f = id) : section_of f = i
   := symm (left_inverse_eq_right_inverse H2 !compose_section)
 
-  theorem inverse_eq_intro_right {H : is_iso f} (H2 : f ∘ i = id) : f⁻¹ = i
+  theorem inverse_eq_intro_right [H : is_iso f] (H2 : f ∘ i = id) : f⁻¹ = i
   := left_inverse_eq_right_inverse !inverse_compose H2
 
-  theorem inverse_eq_intro_left {H : is_iso f} (H2 : i ∘ f = id) : f⁻¹ = i
+  theorem inverse_eq_intro_left [H : is_iso f] (H2 : i ∘ f = id) : f⁻¹ = i
   := symm (left_inverse_eq_right_inverse H2 !compose_inverse)
 
-  theorem section_eq_retraction (f : a ⟶ b) {Hl : is_section f} {Hr : is_retraction f} :
+  theorem section_eq_retraction (f : a ⟶ b) [Hl : is_section f] [Hr : is_retraction f] :
       retraction_of f = section_of f :=
   retraction_eq_intro !compose_section
 
-  theorem section_retraction_imp_iso (f : a ⟶ b) {Hl : is_section f} {Hr : is_retraction f}
+  theorem section_retraction_imp_iso (f : a ⟶ b) [Hl : is_section f] [Hr : is_retraction f]
       : is_iso f :=
   is_iso.mk (subst (section_eq_retraction f) (retraction_compose f)) (compose_section f)
 
   theorem inverse_unique (H H' : is_iso f) : @inverse _ _ _ _ f H = @inverse _ _ _ _ f H' :=
   inverse_eq_intro_left !inverse_compose
 
-  theorem inverse_involutive (f : a ⟶ b) {H : is_iso f} : (f⁻¹)⁻¹ = f :=
+  theorem inverse_involutive (f : a ⟶ b) [H : is_iso f] : (f⁻¹)⁻¹ = f :=
   inverse_eq_intro_right !inverse_compose
 
   theorem retraction_of_id : retraction_of (ID a) = id :=
@@ -94,7 +94,7 @@ namespace morphism
   theorem iso_of_id : ID a⁻¹ = id :=
   inverse_eq_intro_left !id_compose
 
-  theorem composition_is_section [instance] {Hf : is_section f} {Hg : is_section g}
+  theorem composition_is_section [instance] [Hf : is_section f] [Hg : is_section g]
       : is_section (g ∘ f) :=
   is_section.mk
     (calc
@@ -118,7 +118,7 @@ namespace morphism
   theorem composition_is_inverse [instance] (Hf : is_iso f) (Hg : is_iso g) : is_iso (g ∘ f) :=
   !section_retraction_imp_iso
 
-  inductive isomorphic (a b : ob) : Type := mk : ∀(g : a ⟶ b) {H : is_iso g}, isomorphic a b
+  inductive isomorphic (a b : ob) : Type := mk : ∀(g : a ⟶ b) [H : is_iso g], isomorphic a b
 
   end -- remove
   namespace isomorphic
@@ -150,12 +150,12 @@ namespace morphism
   inductive is_epi  [class] (f : @hom ob C a b) : Prop :=
   mk : (∀c (g h : hom b c), g ∘ f = h ∘ f → g = h) → is_epi f
 
-  theorem mono_elim {H : is_mono f} {g h : c ⟶ a} (H2 : f ∘ g = f ∘ h) : g = h
+  theorem mono_elim [H : is_mono f] {g h : c ⟶ a} (H2 : f ∘ g = f ∘ h) : g = h
   := is_mono.rec (λH3, H3 c g h H2) H
-  theorem epi_elim {H : is_epi f} {g h : b ⟶ c} (H2 : g ∘ f = h ∘ f) : g = h
+  theorem epi_elim [H : is_epi f] {g h : b ⟶ c} (H2 : g ∘ f = h ∘ f) : g = h
   := is_epi.rec  (λH3, H3 c g h H2) H
 
-  theorem section_is_mono [instance] (f : hom a b) {H : is_section f} : is_mono f :=
+  theorem section_is_mono [instance] (f : hom a b) [H : is_section f] : is_mono f :=
   is_mono.mk
     (λ c g h H,
       calc
@@ -167,7 +167,7 @@ namespace morphism
       ... = id ∘ h : {retraction_compose f}
       ... = h : !id_left)
 
-  theorem retraction_is_epi [instance] (f : hom a b) {H : is_retraction f} : is_epi f :=
+  theorem retraction_is_epi [instance] (f : hom a b) [H : is_retraction f] : is_epi f :=
   is_epi.mk
     (λ c g h H,
       calc
@@ -184,13 +184,13 @@ namespace morphism
   theorem id_is_mono : is_mono (ID a)
   theorem id_is_epi  : is_epi  (ID a)
 
-  theorem composition_is_mono [instance] {Hf : is_mono f} {Hg : is_mono g} : is_mono (g ∘ f) :=
+  theorem composition_is_mono [instance] [Hf : is_mono f] [Hg : is_mono g] : is_mono (g ∘ f) :=
   is_mono.mk
     (λ d h₁ h₂ H,
     have H2 : g ∘ (f ∘ h₁) = g ∘ (f ∘ h₂), from symm (assoc g f h₁)  ▸ symm (assoc g f h₂) ▸ H,
     mono_elim (mono_elim H2))
 
-  theorem composition_is_epi  [instance] {Hf : is_epi f}  {Hg : is_epi g}  : is_epi  (g ∘ f) :=
+  theorem composition_is_epi  [instance] [Hf : is_epi f] [Hg : is_epi g] : is_epi  (g ∘ f) :=
   is_epi.mk
     (λ d h₁ h₂ H,
     have H2 : (h₁ ∘ g) ∘ f = (h₂ ∘ g) ∘ f, from assoc h₁ g f  ▸ assoc h₂ g f ▸ H,
@@ -202,11 +202,11 @@ namespace morphism
 
   namespace iso
   section
-  variables {ob : Type} {C : category ob} include C
+  variables {ob : Type} [C : category ob] include C
   variables {a b c d : ob}                                         (f : @hom ob C b a)
                            (r : @hom ob C c d) (q : @hom ob C b c) (p : @hom ob C a b)
                            (g : @hom ob C d c)
-  variable {Hq : is_iso q} include Hq
+  variable [Hq : is_iso q] include Hq
   theorem compose_pV : q ∘ q⁻¹ = id := !compose_inverse
   theorem compose_Vp : q⁻¹ ∘ q = id := !inverse_compose
   theorem compose_V_pp : q⁻¹ ∘ (q ∘ p) = p :=
@@ -230,7 +230,7 @@ namespace morphism
       ... = f ∘ id : {inverse_compose q}
       ... = f : id_right f
 
-  theorem inv_pp {H' : is_iso p} : (q ∘ p)⁻¹ = p⁻¹ ∘ q⁻¹ :=
+  theorem inv_pp [H' : is_iso p] : (q ∘ p)⁻¹ = p⁻¹ ∘ q⁻¹ :=
   have H1 : (p⁻¹ ∘ q⁻¹) ∘ q ∘ p = p⁻¹ ∘ (q⁻¹ ∘ (q ∘ p)), from assoc (p⁻¹) (q⁻¹) (q ∘ p)⁻¹,
   have H2 : (p⁻¹) ∘ (q⁻¹ ∘ (q ∘ p)) = p⁻¹ ∘ p, from congr_arg _ (compose_V_pp q p),
   have H3 : p⁻¹ ∘ p = id, from inverse_compose p,
@@ -241,9 +241,9 @@ namespace morphism
   --     (p⁻¹ ∘ (q⁻¹)) ∘ q ∘ p = p⁻¹ ∘ (q⁻¹ ∘ (q ∘ p)) : assoc (p⁻¹) (q⁻¹) (q ∘ p)⁻¹
   --     ... = (p⁻¹) ∘ p : congr_arg (λx, p⁻¹ ∘ x) (compose_V_pp q p)
   --     ... = id : inverse_compose p)
-  theorem inv_Vp {H' : is_iso g} : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q := inverse_involutive q ▸ inv_pp (q⁻¹) g
-  theorem inv_pV {H' : is_iso f} : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ := inverse_involutive f ▸ inv_pp q (f⁻¹)
-  theorem inv_VV {H' : is_iso r} : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q := inverse_involutive r ▸ inv_Vp q (r⁻¹)
+  theorem inv_Vp [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q := inverse_involutive q ▸ inv_pp (q⁻¹) g
+  theorem inv_pV [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ := inverse_involutive f ▸ inv_pp q (f⁻¹)
+  theorem inv_VV [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q := inverse_involutive r ▸ inv_Vp q (r⁻¹)
 
   end
   section
@@ -254,7 +254,7 @@ namespace morphism
               {g : @hom ob C d c} {h : @hom ob C c b}
                        {x : @hom ob C b d} {z : @hom ob C a c}
                        {y : @hom ob C d b} {w : @hom ob C c a}
-  variable {Hq : is_iso q} include Hq
+  variable [Hq : is_iso q] include Hq
 
   theorem moveR_Mp (H : y = q⁻¹ ∘ g) : q ∘ y = g := H⁻¹ ▸ compose_p_Vp q g
   theorem moveR_pM (H : w = f ∘ q⁻¹) : w ∘ q = f := H⁻¹ ▸ compose_pV_p f q
diff --git a/library/algebra/relation.lean b/library/algebra/relation.lean
index bda2e0bf7..b2d56b32c 100644
--- a/library/algebra/relation.lean
+++ b/library/algebra/relation.lean
@@ -26,7 +26,7 @@ namespace is_reflexive
   definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_reflexive R) : reflexive R :=
   is_reflexive.rec (λu, u) C
 
-  definition infer ⦃T : Type⦄ (R : T → T → Prop) {C : is_reflexive R} : reflexive R :=
+  definition infer ⦃T : Type⦄ (R : T → T → Prop) [C : is_reflexive R] : reflexive R :=
   is_reflexive.rec (λu, u) C
 
 end is_reflexive
@@ -40,7 +40,7 @@ namespace is_symmetric
   definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_symmetric R) : symmetric R :=
   is_symmetric.rec (λu, u) C
 
-  definition infer ⦃T : Type⦄ (R : T → T → Prop) {C : is_symmetric R} : symmetric R :=
+  definition infer ⦃T : Type⦄ (R : T → T → Prop) [C : is_symmetric R] : symmetric R :=
   is_symmetric.rec (λu, u) C
 
 end is_symmetric
@@ -54,7 +54,7 @@ namespace is_transitive
   definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_transitive R) : transitive R :=
   is_transitive.rec (λu, u) C
 
-  definition infer ⦃T : Type⦄ (R : T → T → Prop) {C : is_transitive R} : transitive R :=
+  definition infer ⦃T : Type⦄ (R : T → T → Prop) [C : is_transitive R] : transitive R :=
   is_transitive.rec (λu, u) C
 
 end is_transitive
@@ -107,7 +107,7 @@ namespace congruence
   rec (λu, u) C x y
 
   theorem infer {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
-      (f : T1 → T2) {C : congruence R1 R2 f} ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
+      (f : T1 → T2) [C : congruence R1 R2 f] ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
   rec (λu, u) C x y
 
   definition app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
@@ -149,7 +149,7 @@ end congruence
 -- using congruence.
 
 theorem congruence_const [instance] {T2 : Type} (R2 : T2 → T2 → Prop)
-    {C : is_reflexive R2} ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
+    [C : is_reflexive R2] ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
   congruence R1 R2 (λu : T1, c) :=
 congruence.const R2 (is_reflexive.app C) R1 c
 
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 49bbe3d2d..3fe07adbb 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -195,7 +195,7 @@ induction_on l
           from H3 ▸ rfl,
         !exists_intro (!exists_intro H4)))
 
-definition mem.is_decidable [instance] {H : decidable_eq T} (x : T) (l : list T) : decidable (x ∈ l) :=
+definition mem.is_decidable [instance] (H : decidable_eq T) (x : T) (l : list T) : decidable (x ∈ l) :=
 rec_on l
   (decidable.inr (iff.false_elim !mem.nil))
   (take (h : T) (l : list T) (iH : decidable (x ∈ l)),
@@ -223,7 +223,7 @@ rec_on l
 -- Find
 -- ----
 section
-variable {H : decidable_eq T}
+variable [H : decidable_eq T]
 include H
 
 definition find (x : T) : list T → nat :=
diff --git a/library/logic/axioms/hilbert.lean b/library/logic/axioms/hilbert.lean
index 90ee81068..23c0e2f65 100644
--- a/library/logic/axioms/hilbert.lean
+++ b/library/logic/axioms/hilbert.lean
@@ -38,7 +38,7 @@ nonempty_imp_inhabited (obtain w Hw, from H, nonempty.intro w)
 -- the Hilbert epsilon function
 -- ----------------------------
 
-opaque definition epsilon {A : Type} {H : nonempty A} (P : A → Prop) : A :=
+opaque definition epsilon {A : Type} [H : nonempty A] (P : A → Prop) : A :=
 let u : {x : A, (∃y, P y) → P x} :=
   strong_indefinite_description P H in
 elt_of u
diff --git a/library/logic/axioms/piext.lean b/library/logic/axioms/piext.lean
index b80110a38..44e5985b6 100644
--- a/library/logic/axioms/piext.lean
+++ b/library/logic/axioms/piext.lean
@@ -7,7 +7,7 @@ import logic.inhabited logic.cast
 open inhabited
 
 -- Pi extensionality
-axiom piext {A : Type} {B B' : A → Type} {H : inhabited (Π x, B x)} :
+axiom piext {A : Type} {B B' : A → Type} [H : inhabited (Π x, B x)] :
    (Π x, B x) = (Π x, B' x) → B = B'
 
 theorem cast_app {A : Type} {B B' : A → Type} (H : (Π x, B x) = (Π x, B' x)) (f : Π x, B x)
diff --git a/library/logic/decidable.lean b/library/logic/decidable.lean
index b27bb6b4d..966adc2ff 100644
--- a/library/logic/decidable.lean
+++ b/library/logic/decidable.lean
@@ -24,11 +24,11 @@ namespace decidable
     C H :=
   decidable.rec H1 H2 H
 
-  definition rec_on_true {H : decidable p} {H1 : p → Type} {H2 : ¬p → Type} (H3 : p) (H4 : H1 H3)
+  definition rec_on_true [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type} (H3 : p) (H4 : H1 H3)
       : rec_on H H1 H2 :=
   rec_on H (λh, H4) (λh, false.rec_type _ (h H3))
 
-  definition rec_on_false {H : decidable p} {H1 : p → Type} {H2 : ¬p → Type} (H3 : ¬p) (H4 : H2 H3)
+  definition rec_on_false [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type} (H3 : ¬p) (H4 : H2 H3)
       : rec_on H H1 H2 :=
   rec_on H (λh, false.rec_type _ (H3 h)) (λh, H4)
 
@@ -45,13 +45,13 @@ namespace decidable
         d2)
       d1)
 
-  theorem em (p : Prop) {H : decidable p} : p ∨ ¬p :=
+  theorem em (p : Prop) [H : decidable p] : p ∨ ¬p :=
   induction_on H (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp)
 
-  definition by_cases {q : Type} {C : decidable p} (Hpq : p → q) (Hnpq : ¬p → q) : q :=
+  definition by_cases {q : Type} [C : decidable p] (Hpq : p → q) (Hnpq : ¬p → q) : q :=
   rec_on C (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp)
 
-  theorem by_contradiction {Hp : decidable p} (H : ¬p → false) : p :=
+  theorem by_contradiction [Hp : decidable p] (H : ¬p → false) : p :=
   or.elim (em p)
     (assume H1 : p, H1)
     (assume H1 : ¬p, false_elim (H H1))
@@ -92,7 +92,7 @@ namespace decidable
   definition decidable_eq_equiv (Hp : decidable p) (H : p = q) : decidable q :=
   decidable_iff_equiv Hp (eq_to_iff H)
 
-  protected theorem rec_subsingleton [instance] {H : decidable p} {H1 : p → Type} {H2 : ¬p → Type}
+  protected theorem rec_subsingleton [instance] [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type}
       (H3 : Π(h : p), subsingleton (H1 h)) (H4 : Π(h : ¬p), subsingleton (H2 h))
       : subsingleton (rec_on H H1 H2) :=
   rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent version of "by_cases"
diff --git a/library/logic/identities.lean b/library/logic/identities.lean
index 61e8ea4c0..0e609a931 100644
--- a/library/logic/identities.lean
+++ b/library/logic/identities.lean
@@ -37,13 +37,13 @@ calc
      ... ↔ b ∧ (a ∧ c)      : and.assoc
 
 
-theorem not_not_iff {a : Prop} {D : decidable a} : (¬¬a) ↔ a :=
+theorem not_not_iff {a : Prop} [D : decidable a] : (¬¬a) ↔ a :=
 iff.intro
   (assume H : ¬¬a,
     by_cases (assume H' : a, H') (assume H' : ¬a, absurd H' H))
   (assume H : a, assume H', H' H)
 
-theorem not_not_elim {a : Prop} {D : decidable a} (H : ¬¬a) : a :=
+theorem not_not_elim {a : Prop} [D : decidable a] (H : ¬¬a) : a :=
 iff.mp not_not_iff H
 
 theorem not_true : (¬true) ↔ false :=
@@ -52,7 +52,7 @@ iff.intro (assume H, H trivial) false_elim
 theorem not_false : (¬false) ↔ true :=
 iff.intro (assume H, trivial) (assume H H', H')
 
-theorem not_or {a b : Prop} {Da : decidable a} {Db : decidable b} : (¬(a ∨ b)) ↔ (¬a ∧ ¬b) :=
+theorem not_or {a b : Prop} [Da : decidable a] [Db : decidable b] : (¬(a ∨ b)) ↔ (¬a ∧ ¬b) :=
 iff.intro
   (assume H, or.elim (em a)
     (assume Ha, absurd (or.inl Ha) H)
@@ -64,7 +64,7 @@ iff.intro
       (assume Ha, absurd Ha (and.elim_left H))
       (assume Hb, absurd Hb (and.elim_right H)))
 
-theorem not_and {a b : Prop} {Da : decidable a} {Db : decidable b} : (¬(a ∧ b)) ↔ (¬a ∨ ¬b) :=
+theorem not_and {a b : Prop} [Da : decidable a] [Db : decidable b] : (¬(a ∧ b)) ↔ (¬a ∨ ¬b) :=
 iff.intro
   (assume H, or.elim (em a)
     (assume Ha, or.elim (em b)
@@ -76,7 +76,7 @@ iff.intro
       (assume Hna, absurd (and.elim_left N) Hna)
       (assume Hnb, absurd (and.elim_right N) Hnb))
 
-theorem imp_or {a b : Prop} {Da : decidable a} : (a → b) ↔ (¬a ∨ b) :=
+theorem imp_or {a b : Prop} [Da : decidable a] : (a → b) ↔ (¬a ∨ b) :=
 iff.intro
   (assume H : a → b, (or.elim (em a)
     (assume Ha  : a,   or.inr (H Ha))
@@ -84,24 +84,24 @@ iff.intro
   (assume (H : ¬a ∨ b) (Ha : a),
     or.resolve_right H (not_not_iff⁻¹ ▸ Ha))
 
-theorem not_implies {a b : Prop} {Da : decidable a} {Db : decidable b} : (¬(a → b)) ↔ (a ∧ ¬b) :=
+theorem not_implies {a b : Prop} [Da : decidable a] [Db : decidable b] : (¬(a → b)) ↔ (a ∧ ¬b) :=
 calc (¬(a → b)) ↔ (¬(¬a ∨ b)) : {imp_or}
             ... ↔ (¬¬a ∧ ¬b)  : not_or
             ... ↔ (a ∧ ¬b)    : {not_not_iff}
 
-theorem peirce {a b : Prop} {D : decidable a} : ((a → b) → a) → a :=
+theorem peirce {a b : Prop} [D : decidable a] : ((a → b) → a) → a :=
 assume H, by_contradiction (assume Hna : ¬a,
   have Hnna : ¬¬a, from not_implies_left (mt H Hna),
   absurd (not_not_elim Hnna) Hna)
 
-theorem not_exists_forall {A : Type} {P : A → Prop} {D : ∀x, decidable (P x)}
+theorem not_exists_forall {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)]
     (H : ¬∃x, P x) : ∀x, ¬P x :=
 take x, or.elim (em (P x))
   (assume Hp : P x,   absurd (exists_intro x Hp) H)
   (assume Hn : ¬P x, Hn)
 
-theorem not_forall_exists {A : Type} {P : A → Prop} {D : ∀x, decidable (P x)}
-    {D' : decidable (∃x, ¬P x)} (H : ¬∀x, P x) :
+theorem not_forall_exists {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)]
+    [D' : decidable (∃x, ¬P x)] (H : ¬∀x, P x) :
   ∃x, ¬P x :=
 @by_contradiction _ D' (assume H1 : ¬∃x, ¬P x,
   have H2 : ∀x, ¬¬P x, from @not_exists_forall _ _ (take x, not_decidable (D x)) H1,
diff --git a/library/logic/if.lean b/library/logic/if.lean
index e11b4a26e..b271ebc8d 100644
--- a/library/logic/if.lean
+++ b/library/logic/if.lean
@@ -7,24 +7,24 @@
 import logic.decidable tools.tactic
 open decidable tactic eq.ops
 
-definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A :=
+definition ite (c : Prop) [H : decidable c] {A : Type} (t e : A) : A :=
 decidable.rec_on H (assume Hc,  t) (assume Hnc, e)
 
 notation `if` c `then` t `else` e:45 := ite c t e
 
-theorem if_pos {c : Prop} {H : decidable c} (Hc : c) {A : Type} {t e : A} : (if c then t else e) = t :=
+theorem if_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t e : A} : (if c then t else e) = t :=
 decidable.rec
   (assume Hc : c,    eq.refl (@ite c (inl Hc) A t e))
   (assume Hnc : ¬c,  absurd Hc Hnc)
   H
 
-theorem if_neg {c : Prop} {H : decidable c} (Hnc : ¬c) {A : Type} {t e : A} : (if c then t else e) = e :=
+theorem if_neg {c : Prop} [H : decidable c] (Hnc : ¬c) {A : Type} {t e : A} : (if c then t else e) = e :=
 decidable.rec
   (assume Hc : c,    absurd Hc Hnc)
   (assume Hnc : ¬c,  eq.refl (@ite c (inr Hnc) A t e))
   H
 
-theorem if_t_t (c : Prop) {H : decidable c} {A : Type} (t : A) : (if c then t else t) = t :=
+theorem if_t_t (c : Prop) [H : decidable c] {A : Type} (t : A) : (if c then t else t) = t :=
 decidable.rec
   (assume Hc  : c,  eq.refl (@ite c (inl Hc)  A t t))
   (assume Hnc : ¬c, eq.refl (@ite c (inr Hnc) A t t))
@@ -36,7 +36,7 @@ if_pos trivial
 theorem if_false {A : Type} (t e : A) : (if false then t else e) = e :=
 if_neg not_false_trivial
 
-theorem if_cond_congr {c₁ c₂ : Prop} {H₁ : decidable c₁} {H₂ : decidable c₂} (Heq : c₁ ↔ c₂) {A : Type} (t e : A)
+theorem if_cond_congr {c₁ c₂ : Prop} [H₁ : decidable c₁] [H₂ : decidable c₂] (Heq : c₁ ↔ c₂) {A : Type} (t e : A)
                       : (if c₁ then t else e) = (if c₂ then t else e) :=
 decidable.rec_on H₁
  (assume Hc₁  : c₁,  decidable.rec_on H₂
@@ -46,12 +46,12 @@ decidable.rec_on H₁
    (assume Hc₂  : c₂,  absurd (iff.elim_right Heq Hc₂) Hnc₁)
    (assume Hnc₂ : ¬c₂, if_neg Hnc₁ ⬝ (if_neg Hnc₂)⁻¹))
 
-theorem if_congr_aux {c₁ c₂ : Prop} {H₁ : decidable c₁} {H₂ : decidable c₂} {A : Type} {t₁ t₂ e₁ e₂ : A}
+theorem if_congr_aux {c₁ c₂ : Prop} [H₁ : decidable c₁] [H₂ : decidable c₂] {A : Type} {t₁ t₂ e₁ e₂ : A}
                      (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) :
                  (if c₁ then t₁ else e₁) = (if c₂ then t₂ else e₂) :=
 Ht ▸ He ▸ (if_cond_congr Hc t₁ e₁)
 
-theorem if_congr {c₁ c₂ : Prop} {H₁ : decidable c₁} {A : Type} {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) :
+theorem if_congr {c₁ c₂ : Prop} [H₁ : decidable c₁] {A : Type} {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) :
                  (if c₁ then t₁ else e₁) = (@ite c₂ (decidable_iff_equiv H₁ Hc) A t₂ e₂) :=
 have H2 [visible] : decidable c₂, from (decidable_iff_equiv H₁ Hc),
 if_congr_aux Hc Ht He
diff --git a/library/logic/inhabited.lean b/library/logic/inhabited.lean
index 7b3b771d1..0ddb60662 100644
--- a/library/logic/inhabited.lean
+++ b/library/logic/inhabited.lean
@@ -22,6 +22,6 @@ definition dfun_inhabited [instance] (A : Type) {B : A → Type} (H : Πx, inhab
   inhabited (Πx, B x) :=
 mk (λa, destruct (H a) (λb, b))
 
-definition default (A : Type) {H : inhabited A} : A := destruct H (take a, a)
+definition default (A : Type) [H : inhabited A] : A := destruct H (take a, a)
 
 end inhabited
diff --git a/library/logic/instances.lean b/library/logic/instances.lean
index 5d92f55a3..30cb9779a 100644
--- a/library/logic/instances.lean
+++ b/library/logic/instances.lean
@@ -68,7 +68,7 @@ definition congruence_iff_compose [instance] := congruence.compose21 congruence_
 
 namespace general_operations
 
-theorem subst {T : Type} (R : T → T → Prop) ⦃P : T → Prop⦄ {C : congruence R iff P}
+theorem subst {T : Type} (R : T → T → Prop) ⦃P : T → Prop⦄ [C : congruence R iff P]
   {a b : T} (H : R a b) (H1 : P a) : P b := iff.elim_left (congruence.app C H) H1
 
 end general_operations
@@ -113,7 +113,7 @@ relation.mp_like.mk (iff.elim_left H)
 -- Substition for iff
 -- ------------------
 namespace iff
-theorem subst {P : Prop → Prop} {C : congruence iff iff P} {a b : Prop} (H : a ↔ b) (H1 : P a) :
+theorem subst {P : Prop → Prop} [C : congruence iff iff P] {a b : Prop} (H : a ↔ b) (H1 : P a) :
   P b :=
 @general_operations.subst Prop iff P C a b H H1
 end iff
diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean
index dd77e4a82..97b4de116 100644
--- a/library/logic/quantifiers.lean
+++ b/library/logic/quantifiers.lean
@@ -55,10 +55,10 @@ iff.intro
 theorem forall_true_iff_true (A : Type) : (∀x : A, true) ↔ true :=
 iff.intro (assume H, trivial) (assume H, take x, trivial)
 
-theorem forall_p_iff_p (A : Type) {H : inhabited A} (p : Prop) : (∀x : A, p) ↔ p :=
+theorem forall_p_iff_p (A : Type) [H : inhabited A] (p : Prop) : (∀x : A, p) ↔ p :=
 iff.intro (assume Hl, inhabited.destruct H (take x, Hl x)) (assume Hr, take x, Hr)
 
-theorem exists_p_iff_p (A : Type) {H : inhabited A} (p : Prop) : (∃x : A, p) ↔ p :=
+theorem exists_p_iff_p (A : Type) [H : inhabited A] (p : Prop) : (∃x : A, p) ↔ p :=
 iff.intro
   (assume Hl, obtain a Hp, from Hl, Hp)
   (assume Hr, inhabited.destruct H (take a, exists_intro a Hr))
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index d1d66058d..e8a3dd9e8 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -204,13 +204,20 @@ void elaborator::copy_info_to_manager(substitution s) {
 /** \brief Create a metavariable, and attach choice constraint for generating
     solutions using class-instances and tactic-hints.
 */
-expr elaborator::mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict, constraint_seq & cs) {
-    auto ec = mk_placeholder_elaborator(env(), ios(), m_context,
-                                        m_ngen.next(), m_relax_main_opaque, use_local_instances(),
-                                        is_strict, type, g, m_unifier_config);
-    register_meta(ec.first);
-    cs += ec.second;
-    return ec.first;
+expr elaborator::mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict,
+                                     bool is_inst_implicit, constraint_seq & cs) {
+    if (is_inst_implicit) {
+        auto ec = mk_placeholder_elaborator(env(), ios(), m_context,
+                                            m_ngen.next(), m_relax_main_opaque, use_local_instances(),
+                                            is_strict, type, g, m_unifier_config);
+        register_meta(ec.first);
+        cs += ec.second;
+        return ec.first;
+    } else {
+        expr m = m_context.mk_meta(m_ngen, type, g);
+        register_meta(m);
+        return m;
+    }
 }
 
 expr elaborator::visit_expecting_type(expr const & e, constraint_seq & cs) {
@@ -225,7 +232,8 @@ expr elaborator::visit_expecting_type(expr const & e, constraint_seq & cs) {
 
 expr elaborator::visit_expecting_type_of(expr const & e, expr const & t, constraint_seq & cs) {
     if (is_placeholder(e) && !placeholder_type(e)) {
-        expr r = mk_placeholder_meta(some_expr(t), e.get_tag(), is_strict_placeholder(e), cs);
+        bool inst_imp = true;
+        expr r = mk_placeholder_meta(some_expr(t), e.get_tag(), is_strict_placeholder(e), inst_imp, cs);
         save_placeholder_info(e, r);
         return r;
     } else if (is_choice(e)) {
@@ -283,7 +291,7 @@ static bool is_implicit_pi(expr const & e) {
     if (!is_pi(e))
         return false;
     binder_info bi = binding_info(e);
-    return bi.is_strict_implicit() || bi.is_implicit();
+    return bi.is_strict_implicit() || bi.is_implicit() || bi.is_inst_implicit();
 }
 
 /** \brief Auxiliary function for adding implicit arguments to coercions to function-class */
@@ -298,7 +306,8 @@ expr elaborator::add_implict_args(expr e, constraint_seq & cs, bool relax) {
         lean_assert(is_pi(type));
         tag g = e.get_tag();
         bool is_strict = true;
-        expr imp_arg   = mk_placeholder_meta(some_expr(binding_domain(type)), g, is_strict, cs);
+        bool inst_imp  = binding_info(type).is_inst_implicit();
+        expr imp_arg   = mk_placeholder_meta(some_expr(binding_domain(type)), g, is_strict, inst_imp, cs);
         e              = mk_app(e, imp_arg, g);
         type           = instantiate(binding_body(type), imp_arg);
         constraint_seq new_cs;
@@ -522,10 +531,13 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) {
     lean_assert(is_pi(f_type));
     if (!expl) {
         bool first = true;
-        while (binding_info(f_type).is_strict_implicit() || (!first && binding_info(f_type).is_implicit())) {
+        while (binding_info(f_type).is_strict_implicit() ||
+               (!first && binding_info(f_type).is_implicit()) ||
+               (!first && binding_info(f_type).is_inst_implicit())) {
             tag g          = f.get_tag();
             bool is_strict = true;
-            expr imp_arg   = mk_placeholder_meta(some_expr(binding_domain(f_type)), g, is_strict, f_cs);
+            bool inst_imp  = binding_info(f_type).is_inst_implicit();
+            expr imp_arg   = mk_placeholder_meta(some_expr(binding_domain(f_type)), g, is_strict, inst_imp, f_cs);
             f              = mk_app(f, imp_arg, g);
             auto f_t       = ensure_fun(f, f_cs);
             f              = f_t.first;
@@ -551,7 +563,8 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) {
 }
 
 expr elaborator::visit_placeholder(expr const & e, constraint_seq & cs) {
-    expr r = mk_placeholder_meta(placeholder_type(e), e.get_tag(), is_strict_placeholder(e), cs);
+    bool inst_implicit = true;
+    expr r = mk_placeholder_meta(placeholder_type(e), e.get_tag(), is_strict_placeholder(e), inst_implicit, cs);
     save_placeholder_info(e, r);
     return r;
 }
@@ -826,7 +839,8 @@ pair<expr, constraint_seq> elaborator::visit(expr const & e) {
         expr imp_arg;
         bool is_strict = true;
         while (is_pi(r_type)) {
-            if (!binding_info(r_type).is_implicit()) {
+            binder_info bi = binding_info(r_type);
+            if (!bi.is_implicit() && !bi.is_inst_implicit()) {
                 if (!consume_args)
                     break;
                 if (!has_free_var(binding_body(r_type), 0)) {
@@ -835,7 +849,8 @@ pair<expr, constraint_seq> elaborator::visit(expr const & e) {
                     break;
                 }
             }
-            imp_arg = mk_placeholder_meta(some_expr(binding_domain(r_type)), g, is_strict, cs);
+            bool inst_imp = bi.is_inst_implicit();
+            imp_arg = mk_placeholder_meta(some_expr(binding_domain(r_type)), g, is_strict, inst_imp, cs);
             r       = mk_app(r, imp_arg, g);
             r_type  = whnf(instantiate(binding_body(r_type), imp_arg), cs);
         }
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 3c8f589a1..382be3818 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -84,7 +84,7 @@ class elaborator : public coercion_info_manager {
     virtual void save_coercion_info(expr const & e, expr const & c);
     virtual void erase_coercion_info(expr const & e);
     void copy_info_to_manager(substitution s);
-    expr mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict, constraint_seq & cs);
+    expr mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict, bool inst_implicit, constraint_seq & cs);
 
     expr visit_expecting_type(expr const & e, constraint_seq & cs);
     expr visit_expecting_type_of(expr const & e, expr const & t, constraint_seq & cs);
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 57f099237..7684925f8 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -689,7 +689,7 @@ optional<binder_info> parser::parse_optional_binder_info() {
         }
     } else if (curr_is_token(get_lbracket_tk())) {
         next();
-        return some(mk_cast_binder_info());
+        return some(mk_inst_implicit_binder_info());
     } else if (curr_is_token(get_ldcurly_tk())) {
         next();
         return some(mk_strict_implicit_binder_info());
@@ -719,14 +719,14 @@ binder_info parser::parse_binder_info() {
      - default         : consume ')'
      - implicit        : consume '}'
      - strict implicit : consume '}}' or '⦄'
-     - cast            : consume ']'
+     - inst implicit   : consume ']'
 */
 void parser::parse_close_binder_info(optional<binder_info> const & bi) {
     if (!bi) {
         return;
     } else if (bi->is_implicit()) {
         check_token_next(get_rcurly_tk(), "invalid declaration, '}' expected");
-    } else if (bi->is_cast()) {
+    } else if (bi->is_inst_implicit()) {
         check_token_next(get_rbracket_tk(), "invalid declaration, ']' expected");
     } else if (bi->is_strict_implicit()) {
         if (curr_is_token(get_rcurly_tk())) {
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 55dea6202..dbe65a8e0 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -189,7 +189,7 @@ bool pretty_fn::is_implicit(expr const & f) {
     }
     try {
         binder_info bi = binding_info(m_tc.ensure_pi(m_tc.infer(f).first).first);
-        return bi.is_implicit() || bi.is_strict_implicit();
+        return bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit();
     } catch (exception &) {
         return false;
     }
@@ -346,7 +346,7 @@ bool pretty_fn::has_implicit_args(expr const & f) {
         expr type = m_tc.whnf(m_tc.infer(f).first).first;
         while (is_pi(type)) {
             binder_info bi = binding_info(type);
-            if (bi.is_implicit() || bi.is_strict_implicit())
+            if (bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit())
                 return true;
             expr local = mk_local(ngen.next(), binding_name(type), binding_domain(type), binding_info(type));
             type = m_tc.whnf(instantiate(binding_body(type), local)).first;
@@ -370,7 +370,7 @@ auto pretty_fn::pp_app(expr const & e) -> result {
 format pretty_fn::pp_binder_block(buffer<name> const & names, expr const & type, binder_info const & bi) {
     format r;
     if (bi.is_implicit()) r += format("{");
-    else if (bi.is_cast()) r += format("[");
+    else if (bi.is_inst_implicit()) r += format("[");
     else if (bi.is_strict_implicit() && m_unicode) r += format("⦃");
     else if (bi.is_strict_implicit() && !m_unicode) r += format("{{");
     else r += format("(");
@@ -380,7 +380,7 @@ format pretty_fn::pp_binder_block(buffer<name> const & names, expr const & type,
     }
     r += compose(colon(), nest(m_indent, compose(line(), pp_child(type, 0).first)));
     if (bi.is_implicit()) r += format("}");
-    else if (bi.is_cast()) r += format("]");
+    else if (bi.is_inst_implicit()) r += format("]");
     else if (bi.is_strict_implicit() && m_unicode) r += format("⦄");
     else if (bi.is_strict_implicit() && !m_unicode) r += format("}}");
     else r += format(")");
diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp
index 9eaca1d02..01d79eaa8 100644
--- a/src/frontends/lean/server.cpp
+++ b/src/frontends/lean/server.cpp
@@ -549,7 +549,7 @@ void server::display_decl(name const & short_name, name const & long_name, envir
         while (true) {
             if (!is_pi(type))
                 break;
-            if (!binding_info(type).is_implicit())
+            if (!binding_info(type).is_implicit() && !binding_info(type).is_inst_implicit())
                 break;
             std::string q("?");
             q += binding_name(type).to_string();
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index dda693d42..01cbc5a71 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -134,7 +134,7 @@ void expr_const::dealloc() {
 }
 
 unsigned binder_info::hash() const {
-    return (m_implicit << 3) | (m_cast << 2) | (m_contextual << 1) | m_strict_implicit;
+    return (m_implicit << 4) | (m_cast << 3) | (m_contextual << 2) | (m_strict_implicit << 1) | m_inst_implicit;
 }
 
 // Expr metavariables and local variables
@@ -196,7 +196,8 @@ bool operator==(binder_info const & i1, binder_info const & i2) {
         i1.is_implicit() == i2.is_implicit() &&
         i1.is_cast() == i2.is_cast() &&
         i1.is_contextual() == i2.is_contextual() &&
-        i1.is_strict_implicit() == i2.is_strict_implicit();
+        i1.is_strict_implicit() == i2.is_strict_implicit() &&
+        i1.is_inst_implicit() == i2.is_inst_implicit();
 }
 
 // Expr binders (Lambda, Pi)
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index b518fee89..dee56a4cf 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -229,21 +229,30 @@ public:
 class binder_info {
     unsigned m_implicit:1;        //! if true, binder argument is an implicit argument
     unsigned m_cast:1;            //! if true, binder argument is a target for using cast
-    unsigned m_contextual:1;      //! if true, binder argument is assumed to be part of the context, and may be argument for metavariables.
+    /** if m_contextual is true, binder argument is assumed to be part of the context,
+        and may be argument for metavariables. */
+    unsigned m_contextual:1;
     unsigned m_strict_implicit:1; //! if true, binder argument is assumed to be a strict implicit argument
+    /** \brief if m_inst_implicit is true, binder argument is an implicit argument, and should be
+        inferred by class-instance resolution. */
+    unsigned m_inst_implicit:1;
 public:
-    binder_info(bool implicit = false, bool cast = false, bool contextual = true, bool strict_implicit = false):
-        m_implicit(implicit), m_cast(cast), m_contextual(contextual), m_strict_implicit(strict_implicit) {}
+    binder_info(bool implicit = false, bool cast = false, bool contextual = true, bool strict_implicit = false,
+                bool inst_implicit = false):
+        m_implicit(implicit), m_cast(cast), m_contextual(contextual), m_strict_implicit(strict_implicit),
+        m_inst_implicit(inst_implicit) {}
     bool is_implicit() const { return m_implicit; }
     bool is_cast() const { return m_cast; }
     bool is_contextual() const { return m_contextual; }
     bool is_strict_implicit() const { return m_strict_implicit; }
+    bool is_inst_implicit() const { return m_inst_implicit; }
     unsigned hash() const;
-    binder_info update_contextual(bool f) const { return binder_info(m_implicit, m_cast, f, m_strict_implicit); }
+    binder_info update_contextual(bool f) const { return binder_info(m_implicit, m_cast, f, m_strict_implicit, m_inst_implicit); }
 };
 
 inline binder_info mk_implicit_binder_info() { return binder_info(true); }
 inline binder_info mk_strict_implicit_binder_info() { return binder_info(false, false, true, true); }
+inline binder_info mk_inst_implicit_binder_info() { return binder_info(false, false, true, false, true); }
 inline binder_info mk_cast_binder_info() { return binder_info(false, true); }
 inline binder_info mk_contextual_info(bool f) { return binder_info(false, false, f); }
 
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index 222fe7cd2..b79a1f7a4 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -285,12 +285,14 @@ static int binder_info_is_implicit(lua_State * L) { return push_boolean(L, to_bi
 static int binder_info_is_cast(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_cast()); }
 static int binder_info_is_contextual(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_contextual()); }
 static int binder_info_is_strict_implicit(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_strict_implicit()); }
+static int binder_info_is_inst_implicit(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_inst_implicit()); }
 static const struct luaL_Reg binder_info_m[] = {
     {"__gc",               binder_info_gc},
     {"is_implicit",        safe_function<binder_info_is_implicit>},
     {"is_cast",            safe_function<binder_info_is_cast>},
     {"is_contextual",      safe_function<binder_info_is_contextual>},
     {"is_strict_implicit", safe_function<binder_info_is_strict_implicit>},
+    {"is_inst_implicit",   safe_function<binder_info_is_inst_implicit>},
     {0, 0}
 };
 static void open_binder_info(lua_State * L) {
diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp
index 149f2b925..cbdcccfbd 100644
--- a/src/library/kernel_serializer.cpp
+++ b/src/library/kernel_serializer.cpp
@@ -121,6 +121,7 @@ serializer & operator<<(serializer & s, binder_info const & i) {
     s.write_bool(i.is_cast());
     s.write_bool(i.is_contextual());
     s.write_bool(i.is_strict_implicit());
+    s.write_bool(i.is_inst_implicit());
     return s;
 }
 
@@ -129,7 +130,8 @@ static binder_info read_binder_info(deserializer & d) {
     bool cast  = d.read_bool();
     bool ctx   = d.read_bool();
     bool s_imp = d.read_bool();
-    return binder_info(imp, cast, ctx, s_imp);
+    bool i_imp = d.read_bool();
+    return binder_info(imp, cast, ctx, s_imp, i_imp);
 }
 
 static name * g_binder_name = nullptr;
diff --git a/src/library/print.cpp b/src/library/print.cpp
index f81047b3d..ab334c9bf 100644
--- a/src/library/print.cpp
+++ b/src/library/print.cpp
@@ -148,7 +148,7 @@ struct print_expr_fn {
             expr const & n = p.second;
             if (binding_info(e).is_implicit())
                 out() << "{";
-            else if (binding_info(e).is_cast())
+            else if (binding_info(e).is_inst_implicit())
                 out() << "[";
             else if (!binding_info(e).is_contextual())
                 out() << "[[";
@@ -160,7 +160,7 @@ struct print_expr_fn {
             print(binding_domain(e));
             if (binding_info(e).is_implicit())
                 out() << "}";
-            else if (binding_info(e).is_cast())
+            else if (binding_info(e).is_inst_implicit())
                 out() << "]";
             else if (!binding_info(e).is_contextual())
                 out() << "]]";
diff --git a/tests/lean/cls_err.lean b/tests/lean/cls_err.lean
index 3d21d57a4..7f5b3132d 100644
--- a/tests/lean/cls_err.lean
+++ b/tests/lean/cls_err.lean
@@ -3,7 +3,7 @@ import logic
 inductive H [class] (A : Type) :=
 mk : A → H A
 
-definition foo {A : Type} {h : H A} : A :=
+definition foo {A : Type} [h : H A] : A :=
 H.rec (λa, a) h
 
 context
diff --git a/tests/lean/const.lean b/tests/lean/const.lean
index 70df5fc54..98d844398 100644
--- a/tests/lean/const.lean
+++ b/tests/lean/const.lean
@@ -1,10 +1,10 @@
 import logic
 
 
-definition foo {A : Type} {H : inhabited A} : A :=
+definition foo {A : Type} [H : inhabited A] : A :=
 inhabited.rec (λa, a) H
 
-constant bla {A : Type} {H : inhabited A} : Type.{1}
+constant bla {A : Type} [H : inhabited A] : Type.{1}
 
 set_option pp.implicit true
 
diff --git a/tests/lean/pp.lean.expected.out b/tests/lean/pp.lean.expected.out
index fa9299df1..2f4a648f8 100644
--- a/tests/lean/pp.lean.expected.out
+++ b/tests/lean/pp.lean.expected.out
@@ -2,6 +2,6 @@
 λ {A B : Type} (a : A) (b : B), a : ?M_1 → ?M_2 → ?M_1
 λ (A : Type) {B : Type} (a : A) (b : B), a : Π (A : Type) {B : Type}, A → B → A
 λ (A B : Type) (a : A) (b : B), a : Π (A B : Type), A → B → A
-λ [A : Type] (B : Type) (a : A) (b : B), a : Π [A : Type] (B : Type), A → B → A
+λ [A : Type] (B : Type) (a : A) (b : B), a : Π (B : Type), ?M_1 → B → ?M_1
 λ ⦃A : Type⦄ {B : Type} (a : A) (b : B), a : Π ⦃A : Type⦄ {B : Type}, A → B → A
 λ ⦃A B : Type⦄ (a : A) (b : B), a : Π ⦃A B : Type⦄, A → B → A
diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean
index 633e3d232..ed22f6ce3 100644
--- a/tests/lean/run/algebra1.lean
+++ b/tests/lean/run/algebra1.lean
@@ -21,12 +21,12 @@ namespace algebra
   inductive add_struct [class] (A : Type) : Type :=
   mk : (A → A → A) → add_struct A
 
-  definition mul  {A : Type} {s : mul_struct A} (a b : A)
+  definition mul  {A : Type} [s : mul_struct A] (a b : A)
   := mul_struct.rec (fun f, f) s a b
 
   infixl `*`:75 := mul
 
-  definition add  {A : Type} {s : add_struct A} (a b : A)
+  definition add  {A : Type} [s : add_struct A] (a b : A)
   := add_struct.rec (fun f, f) s a b
 
   infixl `+`:65 := add
diff --git a/tests/lean/run/class11.lean b/tests/lean/run/class11.lean
index 3dc8f54d7..faf7b9fa6 100644
--- a/tests/lean/run/class11.lean
+++ b/tests/lean/run/class11.lean
@@ -3,7 +3,7 @@ import logic
 constant C {A : Type} : A → Prop
 class C
 
-constant f {A : Type} (a : A) {H : C a} : Prop
+constant f {A : Type} (a : A) [H : C a] : Prop
 
 definition g {A : Type} (a b : A) {H1 : C a} {H2 : C b} : Prop :=
 f a ∧ f b
diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean
index 8c10d2827..bbb197123 100644
--- a/tests/lean/run/class5.lean
+++ b/tests/lean/run/class5.lean
@@ -4,7 +4,7 @@ namespace algebra
   inductive mul_struct [class] (A : Type) : Type :=
   mk : (A → A → A) → mul_struct A
 
-  definition mul {A : Type} {s : mul_struct A} (a b : A)
+  definition mul {A : Type} [s : mul_struct A] (a b : A)
   := mul_struct.rec (λ f, f) s a b
 
   infixl `*`:75 := mul
diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean
index d0e5a768e..e1421fffa 100644
--- a/tests/lean/run/elab_bug1.lean
+++ b/tests/lean/run/elab_bug1.lean
@@ -57,7 +57,7 @@ theorem congr_not [instance] (T : Type) (R : T → T → Prop) (f : T → Prop)
     (H : congruence R iff f) :
   congruence R iff (λx, ¬ f x) := sorry
 
-theorem subst_iff {T : Type} {R : T → T → Prop} {P : T → Prop} {C : congruence R iff P}
+theorem subst_iff {T : Type} {R : T → T → Prop} {P : T → Prop} [C : congruence R iff P]
     {a b : T} (H : R a b) (H1 : P a) : P b :=
 -- iff_mp_left (congruence.rec id C a b H) H1
 iff.elim_left (@congr_app _ _ R iff P C a b H) H1
diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean
index b08451b46..5c45ff341 100644
--- a/tests/lean/run/group2.lean
+++ b/tests/lean/run/group2.lean
@@ -28,7 +28,7 @@ definition group_to_struct [instance] (g : group) : group_struct (carrier g)
 
 check group_struct
 
-definition mul {A : Type} {s : group_struct A} (a b : A) : A
+definition mul {A : Type} [s : group_struct A] (a b : A) : A
 := group_struct.rec (λ mul one inv h1 h2 h3, mul) s a b
 
 infixl `*`:75 := mul
diff --git a/tests/lean/run/group3.lean b/tests/lean/run/group3.lean
index 854a96b3e..b48e0da12 100644
--- a/tests/lean/run/group3.lean
+++ b/tests/lean/run/group3.lean
@@ -22,9 +22,9 @@ inductive has_mul [class] (A : Type) : Type := mk : (A → A → A) → has_mul
 inductive has_one [class] (A : Type) : Type := mk : A → has_one A
 inductive has_inv [class] (A : Type) : Type := mk : (A → A) → has_inv A
 
-definition mul {A : Type} {s : has_mul A} (a b : A) : A := has_mul.rec (λf, f) s a b
-definition one {A : Type} {s : has_one A} : A := has_one.rec (λo, o) s
-definition inv {A : Type} {s : has_inv A} (a : A) : A := has_inv.rec (λi, i) s a
+definition mul {A : Type} [s : has_mul A] (a b : A) : A := has_mul.rec (λf, f) s a b
+definition one {A : Type} [s : has_one A] : A := has_one.rec (λo, o) s
+definition inv {A : Type} [s : has_inv A] (a : A) : A := has_inv.rec (λi, i) s a
 
 infix `*`    := mul
 postfix `⁻¹` := inv
@@ -40,7 +40,7 @@ mk : Π mul: A → A → A,
 
 namespace semigroup
 section
-  variables {A : Type} {s : semigroup A}
+  variables {A : Type} [s : semigroup A]
   variables a b c : A
   definition mul := semigroup.rec (λmul assoc, mul) s a b
   context
@@ -52,7 +52,7 @@ end
 end semigroup
 
 section
-  variables {A : Type} {s : semigroup A}
+  variables {A : Type} [s : semigroup A]
   include s
   definition semigroup_has_mul [instance] : has_mul A := has_mul.mk semigroup.mul
 
@@ -72,7 +72,7 @@ mk : Π (mul: A → A → A)
 
 namespace comm_semigroup
 section
-  variables {A : Type} {s : comm_semigroup A}
+  variables {A : Type} [s : comm_semigroup A]
   variables a b c : A
   definition mul (a b : A) : A := comm_semigroup.rec (λmul assoc comm, mul) s a b
   definition assoc : mul (mul a b) c = mul a (mul b c) :=
@@ -83,7 +83,7 @@ end
 end comm_semigroup
 
 section
-  variables {A : Type} {s : comm_semigroup A}
+  variables {A : Type} [s : comm_semigroup A]
   variables a b c : A
   include s
   definition comm_semigroup_semigroup [instance] : semigroup A :=
@@ -108,7 +108,7 @@ mk : Π (mul: A → A → A) (one : A)
 
 namespace monoid
   section
-  variables {A : Type} {s : monoid A}
+  variables {A : Type} [s : monoid A]
   variables a b c : A
   include s
   context
@@ -127,7 +127,7 @@ namespace monoid
 end monoid
 
 section
-  variables {A : Type} {s : monoid A}
+  variables {A : Type} [s : monoid A]
   variable a : A
   include s
   definition monoid_has_one [instance] : has_one A := has_one.mk (monoid.one)
@@ -153,7 +153,7 @@ mk : Π (mul: A → A → A) (one : A)
 
 namespace comm_monoid
   section
-  variables {A : Type} {s : comm_monoid A}
+  variables {A : Type} [s : comm_monoid A]
   variables a b c : A
   definition mul := comm_monoid.rec (λmul one assoc right_id left_id comm, mul) s a b
   definition one := comm_monoid.rec (λmul one assoc right_id left_id comm, one) s
@@ -169,7 +169,7 @@ namespace comm_monoid
 end comm_monoid
 
 section
-  variables {A : Type} {s : comm_monoid A}
+  variables {A : Type} [s : comm_monoid A]
   include s
   definition comm_monoid_monoid [instance] : monoid A :=
     monoid.mk comm_monoid.mul comm_monoid.one comm_monoid.assoc
diff --git a/tests/lean/run/univ_bug2.lean b/tests/lean/run/univ_bug2.lean
index cb12a4a14..d4ce5c812 100644
--- a/tests/lean/run/univ_bug2.lean
+++ b/tests/lean/run/univ_bug2.lean
@@ -16,7 +16,7 @@ namespace simplifies_to
 theorem get_eq {T : Type} {t1 t2 : T} (C : simplifies_to t1 t2) : t1 = t2 :=
 simplifies_to.rec (λx, x) C
 
-theorem infer_eq {T : Type} (t1 t2 : T) {C : simplifies_to t1 t2} : t1 = t2 :=
+theorem infer_eq {T : Type} (t1 t2 : T) [C : simplifies_to t1 t2] : t1 = t2 :=
 simplifies_to.rec (λx, x) C
 
 theorem simp_app [instance] (S : Type) (T : Type) (f1 f2 : S → T) (s1 s2 : S)