We show how the subtype relation of the well-known second-order polymorphic system $F_\leq$ with bounded type quantification dupoly Cardelli, Wegner, Bruce, Longo, Curien, Ghelli, proved undecidable Ca Pierce, can be interpreted in a (weak) monadic second-order theory of one (Büchi), two (Rabin), several, or infinitely many successor functions. These \bf (W)SnS-interpretations show that undecidable $F_\leq$ possesses consistent decidable extensions, i.e., $F_\leq$ is not essentially undecidable (Tarski, 1949). We demonstrate an infinite class of ``structurWe dem decidable extensions of $F_\leq$, which combine traddecidable exten inference rules with the above \bf (W)SnS-interpretations. All thesi extensions, which we call systems $F_\leq^SnS$, are still more powerful than $F_\leq$, but less coarse than the direct \bf (W)SnS-interpretations: \[F_\leq\ \subset\ F_\l\[F_\leq\ \subset\ F (W)SnS\mbox-interpretations\] The main distinctive featuresThe main distinctive features of decidability, 2) closure w.r.t. transitivity; 3) structurednedecidabil they never subtype a functional type to a universal one or vice versa, 4) they all contain the powerful rule for subtyping boundedly quantified types: \[\frac\Gamma\ \v\[\frac\Gamma\ \vdash \tau_1\ \leq\ \sigma_ \Gamma\,,\,\alpha\ \leq\ \tau_1\ \vdash\ \sigma_2\ \leq\ \t \Ga