Higher-Order Matching with Many Atoms

Allow simple types to be built from an arbitrary finite set of atomic type variables rather than one atom.

1. Is higher-order matching decidable in this many-atom setting?

2. Given types $\rho$ and $\tau$, is it decidable whether $\rho$ is a retract of $\tau$, meaning that there are typed terms $F:\rho\to\tau$ and $G:\tau\to\rho$ with $G\circ F=_{\beta\eta}I_\rho$?

3. In the polymorphic setting, does mutual retraction $\rho\triangleleft\tau$ and $\tau\triangleleft\rho$ imply that $\rho$ and $\tau$ are isomorphic?