§ Weakly implicit arguments in Lean

variables {α : Type} (f : α → α)
def injective {α Β: Type} (f: α → β) : Prop :=
  ∀ {{x y}}, f x = f y → x = y -- NOTE: weakly implicit
def injective2 {α β : Type} (f : α → β) : Prop :=
    ∀ {x y}, f x = f y → x = y -- NOTE: implicit

def foo (h: injective f) : false := sorry
example (h: injective f) : false :=
begin
  have := @foo,
  unfold injective2 at *,
  exact this f h
end


def bar (h : injective2 f) : false := sorry
example (h : injective2 f) : false :=
begin
  have := @bar,
  unfold injective2 at *,
  exact this f h
end

type mismatch at application
  this f h
term
  h
has type
  f ?m_1 = f ?m_2 → ?m_1 = ?m_2
but is expected to have type
  ∀ {x y : α}, f x = f y → x = y