Unification is at the heart of type checking and unification is doable with a SMT solver. So a SMT solver can be a type checker if you want which should show th

Unification is at the heart of type checking and unification is doable with a SMT solver. So a SMT solver can be a type checker if you want which should show that SMT is indeed much more complex than type checking.