Type mismatch with dependent types

Stream: Type theory

[Clayton Knittel]

I am unsure why the following code doesn't compile:

example {p : Prop} : ¬(p ↔ ¬p) :=
  λ h : p ↔ ¬p, absurd (iff.mp h)

I would expect the type of the lambda expression to be p ↔ ¬p → false, or ¬(p ↔ ¬p), but the type according to the compiler is Π (h : p ↔ ¬p), ¬(p → ¬p) → ?m_1[h] : Sort ?. It appears to make a distinction between dependent types and regular types (h is a dependent type in the lambda expression), but I'm not sure how to introduce ¬(p ↔ ¬p) without hypothesizing something first, and a hypothesis involving p appears to always introduce a dependent type.

There may be other issues with the code I'm trying to compile, but in general I think the meaning of dependent types in lean is still a bit fuzzy to me, so any clarification of that would be much appreciated!

[Yakov Pechersky]

absurd takes two arguments to produce false. What two arguments do you want to provide here?

[Clayton Knittel]

I see, I assumed passing something of type p → ¬p would consume both of those arguments. It makes sense intuitively to me that there would be a way to "unpack" arguments to a function like that

[Mario Carneiro]

Even if you could do something like that, it would presumably be a value of type p /\ ¬p, not p → ¬p.

[Kevin Buzzard]

"p implies not p" is not absurd, because p could be false and then the implication is fine.