Argument interpreted as instance?

Stream: new members

[Pedro Minicz]

Why is unfreezeI necessary in the following example? I'd expect hX not to be an instance, as I specified it as an argument ((hX : nonempty X)) not an instance ([nonempty X] or [hX : nonempty X]).

example (hX : nonempty X) (hY : #Y ≤ 1) :
  ¬ ∃ (f : X → Y) (B : set Y), f '' (f ⁻¹' B) ⊊ B :=
begin
  rintros ⟨f, A, h₁, h₂⟩,
  refine h₂ (le_antisymm h₁ _),
  intros y hy,
  rw cardinal.le_one_iff_subsingleton at hY,
  cases hY with hY,
  unfreezeI,
  cases hX with x,
  use x,
  specialize hY (f x) y,
  simpa [hY]
end

[Reid Barton]

The binder type matters to your caller, not to you.

[Pedro Minicz]

But the type of the lemma is still nonempty ?m_1 → _, so it doesn't seem that the argument would even be given as an instance by the user.

[Reid Barton]

It wouldn't, but what would happen at a hypothetical use site is not relevant to processing the definition itself.

[Reid Barton]

The different binder types don't make a difference for the purpose of the definition. hX is treated as an instance because nonempty is a class.

[Pedro Minicz]

Weird behavior. I'd expect my definition to specify how hX is treated.