> Podle téhle definice by staticky typovaný jazyk byl dost na nic, protože by v něm nešlo napsat např. následující konstrukci
Konkrétně s touto definicí není problém, ne? Protože to přetypování provádíte ve větvi, kde už je ten typ zřejmý a typová chyba nenastane (ano předpokládám, že se mezitím o nezmění).
Podobnou analýzu dělá třeba kompilátor jazyka Mercury. Samozřejmě kompilátor není úplně nejchytřejší a třeba konstrukci
if a > 10 then ... else if a <= 10 then ...
vám neuzná (vynucuje se pokrytí všech možností), protože nevidí, že jiná možnost nenastává a je třeba ji změnit na
if a > 10 then ... else ...
kde už je zřejmé, že jsou všechny případy pokryty.
Podobné je to při dokazování vět nebo algoritmů na počítači, kde ten dokazovací systém často něco nevidí a je třeba to prostě rozepsat.
