As a prelude, there is some terminological confusion in your question. The issue is about a type variable occurring in a result type of a function. This is fairly minor. A more serious one is when you say "my implementation happily infers the types of the above two functions to be ...". What functions? Functions are terms like (in this case) $\tt fun(x:T)e$ but the rule you quote is actually about function application, i.e. it applies to terms like $\tt f(e)$. Either way, the two things you present are types not terms. 915
What you seem to want to say is: given a function $\mathtt{f}\in\tt All(X)()\to X$, the expression $\tt f()$ seems to have the inferred type $\tt X$.
$\tt \sigma \in \bigwedge \overline{C} \Downarrow R$ implies that $\sigma$ is a map for all the variables in $\tt R$ or else it wouldn't even make sense. Maybe it doesn't make sense, but we see that in the rule you listed the constraint generation step produces a $\mathtt{\bar X}/V$ constraint and the substitution algorithm will thus produce a $\mathtt{\bar X}/V$ substitution which, by definition, has a mapping for each type variable in $\tt \bar X$. I assume your confusion is that you look at the minimal substitution generating algorithm $\sigma_{C\tt R}$ at the bottom of page 11, note that in your second case, for example, the constraint generation step produces an empty set of constraints and thus the "for each constraint" iterates over an empty set producing a substitution with no mappings which presumably would act as the identity. However, this would violate the definition of an $\mathtt{\bar X}/V$ substitution. The detail here is the definition of the empty constraint set. At the beginning of section 3.3 on page 9 it states:
The empty $\mathtt{\bar X}/V$ constraint set, written $\emptyset$, contains the trivial constraint $\tt Bot <: X_\mathit{i} <: Top$ for each variable $\mathtt{X}_i$.
Since the result type is covariant (in a top-level context), we'll get $\tt Bot$ in those cases. In particular, given that $\mathtt{f}\in\tt All(X)()\to X$, the expression $\tt f()$ will have the inferred type $\tt Bot$. The produced substitution $\sigma_{\emptyset\tt R}$ will map $\tt X$ to $\tt Bot$. 915