Is F<: with bottom undecidable? We all know that F&lt;: is undecidable: http://www.cse.chalmers.se/~abela/lehre/SS07/Typen/pierce93bounded.pdf

However, I have difficulties finding that anyone claiming the version with bottom added being also undecidable: https://www.cs.indiana.edu/pub/techreports/TR492.pdf

Intuitively F&lt;: with bottom should be undecidable, but if one claims that without proving it, I feel it's just a sloppy belief. In particular, I think that the proof must involve showing S-BOT rule from the version with bottom must be either non-existent, or can be removed from the derivation tree, which doesn't seem immediate to me.

So I am wondering if there is any source actually showing adding bottom doesn't turn the calculus decidable (as expected)?
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.