Decidability of Subtype Entailment

Simple type expressions are finite terms built from variables, constants $\bot$ and $\top$, and a binary constructor. Interpret them as possibly differently shaped trees under the non-structural order in which $\bot$ is below every tree and $\top$ is above every tree. Given a finite constraint set

$$C=\{\tau_i\leq\tau_i' : 1\leq i\leq n\}$$

and types $\tau,\tau'$, is it decidable whether every valuation satisfying $C$ also satisfies $\tau\leq\tau'$, that is, whether $C\models\tau\leq\tau'$?