Is F<: with bottom undecidable?
OK, fine. Since people seem to keep liking this question, I decide to answer this question myself.

TLDR : yes, F&lt;:+bot is undecidable, as shown a proof of translation from it to F&lt;: in the following link by myself: https://gitlab.com/JasonHuZS/AlgDotCalculus/blob/master/agda/FsubBot.agda

bot⇒full : ∀ {Γ S U} → List.map _* Γ ⊢ S * &lt;: U * → Γ ⊢F S &lt;: U
full⇒bot : ∀ {Γ S U} → Γ ⊢F S &lt;: U → List.map _* Γ ⊢ S * &lt;: U *




Despite such intuitive fact, I have to emphasize that, in the presence of subtyping, a syntactical extension of an undecidable language does not have to generate yet another undecidable language. More specifically, the decidability is a very global property of a language which depends on every interaction of the rules, and should not be assumed if a proof is not present.

In the case of F&lt;:, the proof can easily discharge all usage of bot, merely because in F&lt;:+bot, there isn't other creative way of using bot, to a point that it turns the translation of derivation tree to a non-trivial level.

In particular, I am working on another calculus (D&lt;: in another source code), in which bot has so creative behavior to a point that the translation from it to F&lt;: does not generally hold, and therefore, the calculus could be decidable, or, if it's undecidable, F&lt;: does not reside in it as a sub-language.