f(x) + g(x) For any type of x is enumerable. What that means is that for this specific expression, you can enumerate all of the types that x may take, and then

f(x) + g(x) For any type of x is enumerable. What that means is that for this specific expression, you can enumerate all of the types that x may take, and then enumerate all of the types that a function would return, given the types (if you can). You can then decide whether this expression is true or not. Now it depends on the implementation of f and g. And type systems, in most of the practical cases - would be able to deal with this. x = 1 print_int(x) x="a" print_string(x) The second example is always decidable, if we agree that semantics of '=' are generally a question of equivalence.