\sec{Type checking}{type-checkin}{Type_checking.html}
%
{\mlton}'s type checker follows the Definition of SML closely, so you
may find differences between {\mlton} and other SML compilers that do
not follow the Definition so closely.  In particular, {\smlnj} has
many deviations from the Definition -- please see
\appref{nj-deviations} for a list of those that we are aware of.

In some respects {\mlton}'s type checker is more powerful than other
SML compilers, so there are programs that {\mlton} accepts that are
rejected by some other SML compilers.  These kinds of programs fall
into a few simple categories.

\begin{itemize}

\item
{\mlton} resolves flexible record patterns using a larger context than
many other SML compilers.  For example, {\mlton} accepts the
following.
\begin{verbatim}
fun f {x, ...} = x
val _ = f {x = 13, y = "foo"}
\end{verbatim}
%
\item
{\mlton} uses as large a context as possible to resolve the type of
variables constrained by the value resriction to be monotypes.  For
example, {\mlton} accepts the following.
\begin{verbatim}
structure S:
   sig
      val f: int -> int
   end =
   struct
      val f = (fn x => x) (fn y => y)
   end
\end{verbatim}

\end{itemize}

\subsection{Type error messages}

To aid in the understanding of type errors, {\mlton}'s type checker
displays type errors differently than other SML compilers.  In
particular, when two types are different, it is important for the
programmer to easily understand why they are different.  So, {\mlton}
displays only the differences between two types that don't match,
using underscores for the parts that do.  For example, if a
function expects {\tt real * int} but gets {\tt real * real}, the type
error message would look like
\begin{verbatim}
expects: _ * [int]
but got: _ * [real]
\end{verbatim}
As another aid to spotting differences, {\mlton} places brackets {\tt
[]} around the parts of the types that don't match.  A common
situation is when a function receives a different number of arguments
than it expects, in which case you might see an error like
\begin{verbatim}
expects: [int * real]
but got: [int * real * string]
\end{verbatim}
The brackets make it easy to see that the problem is that the tuples
have different numbers of components -- not that the components don't
match.  Contrast that with a case where a function receives the right
number of arguments, but in the wrong order.
\begin{verbatim}
expects: [int] * [real]
but got: [real] * [int]
\end{verbatim}
Here the brackets make it easy to see that the components do not
match.

{\mlton}'s type checker is fairly new.  If you encounter a difference
between {\mlton} and another SML compiler, or even with an older
version of {\mlton}, and are not able to determine if it is a bug,
please send mail to {\mltonmail}.  We would also appreciate feedback
on any type error messages that you find confusing, or suggestions you
may have for improvements to error messages.

\subsection{Type information about programs}

{\mlton} has a flag, {\tt -show-basis } {\it file}, that causes
{\mlton} to pretty print to {\it file} the basis defined by the input
program.  For example, if {\tt foo.sml} contains
\begin{verbatim}
fun f x = x + 1
\end{verbatim}
then {\tt mlton -show-basis foo.basis foo.sml} will create {\tt
foo.basis} with the following contents.
\begin{verbatim}
val f: int -> int
\end{verbatim}
If you only want to see the basis and do not wish to compile the
program, you can call {\mlton} with {\tt -stop tc}.

When displaying signatures, {\mlton} prefixes types defined in the
signature them with {\tt ?.} to distinguish them from types defined in
the environment.  For example,
\begin{verbatim}
signature SIG =
   sig
      type t
      val x: t * int -> unit
   end
\end{verbatim}
is displayed as
\begin{verbatim}
signature SIG = 
   sig
      type t = ?.t
      val x: (?.t * int) -> unit
   end
\end{verbatim}
Notice that {\tt int} occurs without the {\tt ?.} prefix.

{\mlton} also uses a canonical name for each type in the signature,
and that name is used everywhere for that type, no matter what the
input signature looked like.  For example
\begin{verbatim}
signature SIG =
   sig
      type t
      type u = t
      val x: t
      val y: u
   end
\end{verbatim}
is displayed as
\begin{verbatim}
signature SIG = 
   sig
      type t = ?.t
      type u = ?.t
      val x: ?.t
      val y: ?.t
   end
\end{verbatim}

Canonical names are always relative to the ``top'' of the signature,
even when used in nested substructures.  For example,
\begin{verbatim}
signature S =
   sig
      type t
      val w: t
      structure U:
         sig
            type u
            val x: t
            val y: u
         end
      val z: U.u
   end
\end{verbatim}
is displayed as
\begin{verbatim}
signature S = 
   sig
      type t = ?.t
      val w: ?.t
      val z: ?.U.u
      structure U:
         sig
            type u = ?.U.u
            val x: ?.t
            val y: ?.U.u
         end
   end
\end{verbatim}

When displaying structures, {\mlton} uses signature contstraints
wherever possible, combined with {\tt where type} clauses to specify
the meanings of the types defined within the signature.

\begin{verbatim}
signature SIG =
   sig
      type t
      val x: t
   end
structure S: SIG =
   struct
      type t = int
      val x = 13
   end
structure S2:> SIG = S
\end{verbatim}
is displayed as
\begin{verbatim}
structure S: SIG
             where type t = int
structure S2: SIG
              where type t = S2.t
signature SIG = 
   sig
      type t = ?.t
      val x: ?.t
   end
\end{verbatim}