What is the relation between syntax and type theory?
The division line between syntax and additional type checking can indeed be blurred, if so desired, but usually we make a distinction as follows:


the syntax is described using a formal grammar, preferrably one that is not very complex, such as a context-free gramar, or one that is even simpler than that.
the typing rules are described using inference rules whose complexity tyically exceeds that of a context-free formal grammar.


In general, a programming language might stratify the task of getting from the source code to the compiled code as follows:


Parsing converts the input string to an abstract syntax which represents the input as a tree.
Elaboration performs certain simple transformation of input syntax, such as getting rid of syntactic sugar.
Type-checking and inference verifies that the program is well-typed, thereby guaranteeing that later stages will not get stuck. It may also augment the input source with extra information about types.
Several phases of compilation may follow, each translating from its input to a simpler language. The final language may be machine code, or byte code, or in general some intermediate code.
The program is executed.


While you may consider merging some of these phases together, and sometimes that is a good idea, it is in general better to keep them separate. From a conceptual point of view parsing is very different from type checking. After all, these two phases serve different purposes: one is just a translation from strings to trees, while the other one statically analyzes the structure of the program in order to detect possible errors and to aid further compilation.

An example of merging different phases is "just in time" compilation: we run a program in an "interpreted" mode so that there is no delay because of compilation, and at the same time we perform on-the-fly compilation of those parts of the code in which the program is spending most of the time. I believe some browsers do that with Javascript.