Exercise 7.11
Let $S : ∗$ and $P,Q : S →∗$. Let $y : Πα : ∗. ((Πx : S. (P x →α)) →α)$, $z : Πx : S. (P x →Qx)$ and $x : S$.
(a) Find a correct type for $y(Qx)$.
(b) Why is the application $y(Qx)z$ incorrect?
(c) Check that this results corresponds with Remark 7.5.2.
(a) We start with $Qx : *$. To avoid the $x$ in $Qx$ being captured by the $\Pi x:S$ in $y$, we should rename the variable $x$ to $z$. This gives us
$$ y(Qx) \; : \; (Πz : S. (P z → Qx)) → Qx $$
(b) The function $y(Qz)$ takes an argument of type $Πz : S. (P z → Qx)$.
The type of $z$ is $ Πx : S. (P x →Qx)$, which is different, and so $y(Qz)$ cannot be applied to $z$.
(c) This result supports Remark 7.5.2.
