What you're suggesting is essentially combining some sort of partial evaluation with type-checking. This is going to be hard to do in a consistent, intuitive way: either you only do a very small number of obvious cases (like if (false)) which is not all that useful and just adds complexity or you try to do it in a principled fashion which is difficult and still inherently limited.
Right now, the typing rule for if in Scala is reasonably simple. The condition is a boolean and the whole expression is the least upper bound of the left branch and the right branch. How much more complex would this rule have to be if it needed to fully specify when the condition gets simplified?
To be sure, your idea is interesting and could probably be done well in another language. I wouldn't be surprised if this sort of capability naturally comes up in some dependently typed systems. But it wouldn't work very well in Scala: you'd be adding a lot of complexity for relatively little gain.
I think I can understand if Scala does not want to consider this kind of constant folding: after all, in most code you are supposed to have the same type on the "then" and "else" branch (in OCaml for example you don't have the possibility, as far as I know, to reproduce this case).
I was surprised because I though it is quite a standard analysis in compilers nowadays. I had in mind SBCL precise type-checking (Common Lisp). Consider for example:
The derived type is NULL (which contains only NIL).
And, more importantly, the compiler signals the presence of dead code, which is helpful for finding typos. It can handle more complex situations where the mistake is not obvious.
The type system supports interval types like "(integer low high)":
I'm not too familiar with SBCL but I highly doubt that those are static types. This sort of information is pretty ascertainable if you really want it, but it's going to be rough going doing non-runtime checking over types this rich.
There are declared types and derived types, which are obtained by type inference and propagation. As much as possible, those types are used by the compiler, at compile-time, to signal type errors that are bound to happen at runtime, given the known types.
But the code is robust and you can give a string to a function that is declared to accept a number (e.g. from the REPL): your program won't crash, because types are checked at runtime too (you have an exception).
So, with default safety and speed optimization levels, adding type declarations will actually add runtime checks.
But if you say "trust me, this will be a fixnum, produce some efficient code", then the type discrimination that would happen at runtime is bypassed and you directly emit the opcodes related to your type and this is how you optimize your code. For example, requesting a high-level of speed and low safety/debug will report a lot of optimization notes from SBCL, like: "forced to do GENERIC-+ instead of FIXNUM-+ because of type uncertainty".
You can do ifs at the type level in Scala, using dependent types. The difference is that Scala draws a clear distinction between the value level and the type level. This was, after all, the original point of types (in the typed lambda calculus sense).
Right now, the typing rule for if in Scala is reasonably simple. The condition is a boolean and the whole expression is the least upper bound of the left branch and the right branch. How much more complex would this rule have to be if it needed to fully specify when the condition gets simplified?
To be sure, your idea is interesting and could probably be done well in another language. I wouldn't be surprised if this sort of capability naturally comes up in some dependently typed systems. But it wouldn't work very well in Scala: you'd be adding a lot of complexity for relatively little gain.