 A different way to look at the problem of typing \(\textsf{WI}\) is to say that \(\textsf{W}\) should have a type similar to the formula \((A\rightarrow (A\rightarrow B))\rightarrow A\rightarrow B\), but in which the formulas in place of the two formulas \(A\) and \(A\rightarrow B\) in the antecedent can be unified. This is the motivation for the inclusion of conjunction (\(\land\)) and top (\(\top\)) as new type constructors.