How do typing rules look if most types are user-defined?

Funny, I remember also having this question when I was first learning how types systems work.

The short answer is they look pretty similar. I'll give an example somewhat taken from Types and Programming Languages, which is an excellent reference work for this sort of thing. Please consider this to be extending the system laid out in Alexis King's guide to type system notation.

Let's consider a slightly more complicated language.

Products

We extend the syntax for products as such.

$$ \begin{array}{rcll} e \hskip{-10mu} &::=&\hskip{-10mu}...\\ & | &\hskip{-10mu} (e,e) &\textrm{pairs}\\ & | &\hskip{-10mu} \textbf{car}\ e &\textrm{left projection}\\ & | &\hskip{-10mu} \textbf{cdr}\ e &\textrm{right projection}\\[8pt] τ \hskip{-10mu} &::=&\hskip{-10mu}...\\ & | &\hskip{-10mu} τ \times τ &\textrm{products} \end{array} $$

Here, we are restricting ourselves to a limited form of products: pairs. There are other types that can be interpreted as a product - structs, tuples, records (if you draw such a distinction)... but I'm sticking with pairs as they are the simplest to work with. (If you are interested in other minutely different systems, check out TAPL.)

Historically left and right projection is known as "car" and "cdr" respectively (from Lisp - etymology): though in languages with infix notation you will more commonly see something like $e.1$ or $e[1]$. I have bolded $\textbf{car}$ and $\textbf{cdr}$ above to emphasize that they are destructors. They are taking in a pair, and deconstructing it: $\text{car}\ (e_1, e_2)$ gives you $e_1$, and $\text{cdr}\ (e_1, e_2)$ gives you $e_2$. On the other hand, $(e_1, e_2)$ is a constructor: it is returning a pair.

But on to the typing rules. They are as follows:

$$ \begin{array}{l} Γ ⊢ e : τ_1 × τ_2 \\ \hline \hskip{5mu} Γ ⊢ \text{car}\ e : τ_1 \end{array} \quad \quad \begin{array}{l} Γ ⊢ e : τ_1 × τ_2 \\ \hline \hskip{5mu} Γ ⊢ \text{cdr}\ e : τ_2 \end{array} $$

$$ \begin{array}{l} Γ ⊢ e_1 : τ_1 \hskip{25mu} Γ ⊢ e_2 : τ_2 \\ \hline \hskip{20mu} Γ ⊢ (e_1, e_2) : τ_1 × τ_2 \end{array} $$

These look pretty similar to function types, with their $τ_1$ and $τ_2$ type variables. Indeed, they can be thought of as user-definable in the same way. Just like one can define an arbitrary amount of function types of the form $τ_1 → τ_2$, one can also define an arbitrary amount of product types of the form $τ_1 × τ_2$.

But what about product types with more than two entries?

There are two approaches that can be taken. One, stick with our binary product types, treat $τ_1 × (τ_2 × τ_3)$ as $τ_1 × τ_2 × τ_3$ by convention, and define syntactic sugar for direct field access ($e.1, e.2, e.3$) that desugars to the more formally-specified $\text{car}$ and $\text{cdr}$ deconstructors. This is a perfectly valid approach. Two, use an extension of standard type system notation to explicitly specify semantics for products of arbitrary size. This is somewhat of a bad idea: it is much easier to reason about typing rules when you have a finite set of constructors and destructors. To quote TAPL: "such notations [of arbitrary arity] are always a bit problematic, as there is some inevitable tension between rigor and readability".

But what if we wanted to label the entries of our product types?

Again, we should consider why we want to deal with this in our typing rules. It is perhaps a better idea to not. But, a valid approach would be to define a new class of labels: $l ::= l_i \in \mathcal{L}^{i \in 1..n}$ for some $n$, and extend our typing rules with them. (This notation is arbitrary. I am not aware of any standard notation.)

Sums

Now let us consider sum types. These are a little more confusing.

$$ \begin{array}{rcll} e \hskip{-10mu} &::=&\hskip{-10mu}...\\ & | &\hskip{-10mu} \text{inl}\ e &\textrm{left tag}\\ & | &\hskip{-10mu} \text{inr}\ e &\textrm{right tag}\\ & | &\hskip{-10mu} \textbf{case}\ e\ &\textrm{case} \\ & & \textbf{of}\ \text{inl}\ x ⇒ e\\ & & \textbf{of}\ \text{inr}\ x ⇒ e\\[8pt] τ \hskip{-10mu} &::=&\hskip{-10mu}...\\ & | &\hskip{-10mu} τ + τ &\textrm{sums} \end{array} $$

You will notice the $\text{inl}$ and $\text{inr}$ constructors. Those probably don't look like anything you've seen before. That is because we are similarly restricting ourselves to a limited form of sums here: our sums here may only be identified by the "left" and "right" tags. ($\text{inl}$ and $\text{inr}$ come from "injection" + "left" / "right".)

The $\text{case}$ statement should provide a hint as to how they are used: our case expression explicitly is defined for fixed tags: instead of user-defined tags (ex. Just, Nothing, Some...) common in real-world languages with sum types. This means our constructors (and destructors) are finite, and so we do not need to extend the type system notation itself. And in a similar fashion to our treatment of products of arbitrary-arity above, we can treat $τ_1 + (τ_2 + τ_3)$ as $τ_1 + τ_2 + τ_3$ by convention, and define syntactic sugar atop.

Our typing rules are as follows:

$$ \begin{array}{l} \hskip{30mu} Γ ⊢ e : τ_1 \\ \hline Γ ⊢ \text{inl}\ e : τ_1 + τ_2 \end{array} \quad \quad \begin{array}{l} \hskip{30mu} Γ ⊢ e : τ_2 \\ \hline Γ ⊢ \text{inr}\ e : τ_1 + τ_2 \end{array} $$

$$ \begin{array}{l} \hskip{100mu} Γ ⊢ e : τ_1 + τ_2 \\ \hskip{25mu} Γ,x_1 : τ_1 ⊢ e_1 : τ \hskip{25mu} Γ,x_2 : τ_2 ⊢ e_2 : τ \\ \hline Γ ⊢ \text{case}\ e\ \text{of}\ \text{inl}\ x_1 ⇒ e_1\ \text{of}\ \text{inr}\ x_2 ⇒ e_2 : τ \end{array} $$

There are a few items of note here. $\text{case}$ is deconstructing some term of type $τ_1 + τ_2$ into a third type $τ$. This is necessary in order for the case expression to be of a consistent type. Also, the rules for the $\text{inl}$ and $\text{inr}$ constructors introduce new types $τ_2$ and $τ_1$ not previously introduced above the bar: these are arbitrary types and are in practice necessarily determined by explicit type annotations.

You store user-defined data types in the context as bindings for types and values; you then look up value constructors when they occur in expressions similarly to how you look up let-bound variables in the context when they are used.

A full example is The Definition of Standard ML by Milner et al.. Inference rules are on pages 23-31 (pages 37-45 of the PDF). The types of the metavariables (C for contexts, TE for type environments, VE for value environments, etc.) are given on page 18, and the rest of Chapter 4 defines the operations and notations used in inference rules.

When you define a data type,

datatype my_ty = MyCon of int

the identifiers my_ty and MyCon are respectively introduced in the type environment and value environment. This involves two declaration-level rules, simplified below (pages 26-27): rule 17 generates bindings from a single datatype declaration, and rule 24 accumulates the bindings from one declaration to typecheck the subsequent declaration(s):

$$ \begin{array}{c} C \oplus \mathit{TE} \vdash \mathit{datbind} \Rightarrow \mathit{VE},\mathit{TE} \\ \hline C \vdash \mathbf{datatype}\;\mathit{datbind} \Rightarrow \mathit{VE},\mathit{TE} \;\;\mathrm{in}\;\mathit{Env} \end{array} (17) $$

$$ \begin{array}{c} C \vdash \mathit{dec}_1 \Rightarrow E_1 \quad C \oplus E_1 \vdash \mathit{dec}_2 \Rightarrow E_2 \\ \hline C \vdash \mathit{dec}_1;\mathit{dec}_2 \Rightarrow E_1 \oplus E_2 \end{array} (24) $$

The following rule shows how one of those bindings is generated. A data type declaration introduces value constructors, which are basically functions. For example, the clause MyCon of int above introduces a constructor MyCon of type t0 -> my_ty. This is handled by rule 29, where the resulting binding is $\{\mathit{tid} \mapsto (\tau'\to\tau, \mathtt{c})\}$---it is a map with key $\mathit{tid}$ and associated value $(\tau'\to\tau, \mathtt{c})$. The binding also contains a tag $\mathtt{c}$ to remember that MyCon is a constructor, as opposed to a plain value. In ML, constructors are either nullary or unary. For brevity, we only consider unary constructors:

$$ \begin{array}{c} C \vdash \mathit{ty} \Rightarrow \tau' \\ \hline C, \tau \vdash \mathit{tid}\;\mathtt{of}\;\mathit{ty} \Rightarrow \{\mathit{tid}\mapsto (\tau'\to\tau, \mathtt{c})\} \end{array} (29) $$

Constructors can be used in expressions in two ways: as values, and in patterns to decompose values. As values, we use the same rule for constructors as for regular (let-bound) values (rule 2). In words: to infer the type of $\mathit{longvid}$ in context $C$, look up the identifier $\mathit{longvid}$ in $C$, it should be bound to some type scheme $\sigma$, monomorphize it to $\tau$.

$$ \begin{array}{c} C(\mathit{longvid}) = \sigma \quad \sigma \succ \tau \\ \hline C \vdash \mathit{longvid} \Rightarrow \tau \end{array} (2) $$

Patterns occur in lambdas (anonymous functions). The typing rule for lambdas is rule 12; lambdas are sequences of matches (rule 13), where a match is of the form pat => exp (rule 14). The last relevant rule is the rule for constructors in patterns, rule 41 below (or rule 35 for nullary constructors). For example, in the expression fn MyCon(x) => x, the pattern MyCon(x) would be typed by an instance of this rule with MyCon as $\mathit{longvid}$ and (x) as $\mathit{atpat}$. The condition $\mathit{is}\neq \mathtt{v}$ ensures that $\mathit{longvid}$ is not a regular value; the tag $\mathit{is}$ must be either $\mathtt{c}$ or $\mathtt{e}$ (for exceptions, which behave like constructors). $\mathit{longvid}\;\mathit{atpat}$ has type $\tau$ when $\mathit{longvid}$ has type $\tau'\to\tau$ and $\mathit{atpat}$ has type $\tau'$. (The $\mathit{VE}$ in the result contains the variables bound by the pattern, like x in MyCon(x).)

$$ \begin{array}{c} C(\mathit{longvid}) = (\sigma, \mathit{is}) \quad \mathit{is} \neq \mathtt{v} \quad \sigma\succ \tau' \to \tau \quad C\vdash \mathit{atpat} \Rightarrow (\mathit{VE}, \tau') \\ \hline C \vdash \mathit{longvid}\;\mathit{atpat} \Rightarrow (\mathit{VE},\tau) \end{array} (41) $$