statcor.tex

\section{Static Semantics for the Core}
Our\index{20.1} first task in presenting the semantics -- whether for Core or Modules,
static or dynamic -- is to define the objects concerned. In addition
to the class of {\sl syntactic} objects, which we have already defined, 
there are classes of so-called {\sl semantic} objects used to describe
the meaning of the syntactic objects. Some classes contain {\sl simple}
semantic objects; such objects are usually identifiers or names of some
kind. Other classes contain {\sl compound} semantic objects, such as
types or environments, which are constructed from component objects.

\subsection{Simple Objects}
% (cvr
% All semantic objects in the static semantics of the entire 
% language are built from identifiers and two further kinds of simple objects: 
% type constructor names and structure names.
% Type constructor names are the values taken by type constructors; we shall
% usually refer to them briefly as type names, but they are to be clearly
% distinguished from type variables and type constructors. 
% Structure names play an active role only in
% the Modules semantics; they enter the Core semantics only because
% they appear in structure environments, which (in turn) are needed in the Core
% semantics only to determine the values of long identifiers. The simple object
% classes, and the variables ranging over them, are shown in
% Figure~\ref{simple-objects}. We have included $\TyVar$ in the table to
% make visible the use of $\alpha$ in the semantics to range over $\TyVar$.\index{20.2}
% cvr)
All semantic objects in the static semantics of the entire language
are built from identifiers and two further kinds of simple objects:
type variables, type constructor names and identifier status descriptors.
Type variables are the semantic counterparts of type identifiers and range
over types.
Type
constructor names range over the values taken by type constructors; we shall
usually refer to them briefly as type names, but they are to be
clearly distinguished from type variables and type constructors. The
simple object classes, and the variables ranging over them, are shown
in Figure~\ref{simple-objects}.
% We have included \TyVar\ in the table to make visible the
%use of $\alpha$ in the semantics to range over \TyVar.
\index{20.2}

\vspace{-7mm}
\begin{figure}[h]
\vspace{2pt}
\begin{displaymath}
\begin{array}{rclr}
\alpha\ {\rm or}\ \tyvar & \in   & \TyVar	& \mbox{type variables}\\
\t\ {\rm or}\ \u\               & \in   & \TyName	& \mbox{type names}\\
\is               & \in   & $\IdStatus = \{\cstatus, \estatus, \vstatus\} $
                         &  \mbox{identifier status descriptors}\\
% \m		& \in	& \StrNames	& \mbox{structure names} % (cvr)
\end{array}
\end{displaymath}
\caption{Simple Semantic Objects}
\label{simple-objects}
%\vspace{3pt}
\end{figure}

Each\index{20.3} $\alpha \in\TyVar$ possesses a boolean {\sl equality} attribute,
which determines whether or not it {\sl admits equality}.
% , i.e. whether it is a member of EtyVar (defined on page~\pageref{etyvar-lab}).
%-- in which case we
%also say that it is an {\sl equality} type variable. 
%poly 
% (cvr
% Independently hereof, each $\alpha$ possesses a boolean attribute,
% the {\sl imperative} attribute, which determines whether it is imperative,
% i.e. whether it is a member of $\ImpTyVar$ (defined on page~\pageref{etyvar-lab})
% or not.
% cvr)
% (cvr
% Each $\t\in\TyNames$ has
% an arity $k\geq 0$, and also possesses an equality attribute.
% We denote the class of type names with arity $k$ by $\TyNamesk$.
Each $\t\in\TyName$ has
a kind  $\K\ \in\ \Kind$ (defined
in Figure~\ref{compound-objects}). 
We denote the class of type names with kind \K\ by $\TyName[\K]$, letting
\t[\K] range over elements of \TyName[\K]. 
A type name \t\ {\sl has arity \k}, if, and only if, it has kind \k\ or \keq.
A type name \t\ {\sl admits equality}, or is an {\sl equality type name}, if, and only if, it has kind \keq.


% cvr)

% (cvr
% With\index{20.35} each special constant {\scon} we associate a type
% name $\scontype(\scon)$ which is either {\INT}, {\REAL} or {\STRING}
% as indicated by Section~\ref{cr:speccon}.
With\index{20.35} each special constant {\scon} we associate a type
name $\scontype(\scon)$ which is either {\INT}, {\REAL}, {\WORD}, {\CHAR}
or {\STRING}
as indicated by Section~\ref{cr:speccon}.
(However, see Appendix~\ref{overloading-app} concerning types of overloaded special constants.)

% cvr)

\subsection{Compound Objects}
When\index{20.4} $A$ and $B$ are sets $\Fin A$ denotes the set of finite subsets of $A$,
and $\finfun{A}{B}$ denotes the set of {\sl finite maps} (partial functions
with finite domain) from $A$ to $B$.
The domain\index{21.1} and range of a finite map, $f$, are denoted $\Dom f$ and
$\Ran f$.
A finite map will often be written explicitly in the form $\kmap{a}{b},
\ k\geq 0$;
in particular the empty map is $\emptymap$.
We shall use the form $\{x\mapsto e\  ;\  \phi\}$ -- a form of set
comprehension -- to stand for the finite map $f$ whose domain
is the set of values $x$ which satisfy the condition $\phi$, and
whose value on this domain is given by $f(x)=e$.

When $f$ and $g$ are finite maps the map $\plusmap{f}{g}$, called
$f$ {\sl modified} by $g$, is the finite map with domain
$\Dom f \cup \Dom g$ and values
\[(\plusmap{f}{g})(a) = \mbox{if $a\in\Dom g$ then $g(a)$ else $f(a)$.}
\]

The compound objects for the static semantics of the Core Language are
shown in Figures~\ref{compound-objects} and \ref{compound-objects-continued}.
We take $\cup$ to mean disjoint union over
semantic object classes. We also understand all the defined object
classes to be disjoint.

\begin{figure}[h]
%\vspace{2pt}
\begin{displaymath}
\begin{array}{rcl}
% (cvr
   \k\         & \in\ & \Arity = \{\k; \k \geq 0 \} \\
   \K\ {\rm or}\ \k\ {\rm or}\ \keq\ {\rm or}\ \Karr{\K}{\K'} 
                & \in  & \Kind = \Arity \cup \Arity \cup
                                         (\Kind \times \Kind) \\
% cvr)
        \tau	&\in	&\Type = \TyVar\cup\RecType\cup\FunType\cup{}\\
                &       & \qquad \ConsType\cup\PackType\\
 \longtauk\ {\rm or}\ \tauk
                & \in   & \Type^{(k)}\\
 \longalphak\ {\rm or}\ \alphak
                & \in   & \TyVar^{(k)}\\
 \varrho        & \in   & \RecType = \finfun{\Lab}{\Type} \\
 \tau\rightarrow\tau'
                & \in   & \FunType = \Type\times\Type \\
                &       & \ConsType = \cup_{\k\in\Arity}\ConsType^{\k}\\
 \apptype{\tauk}{\typeapp[\k]} & \in 	& \ConsType^{k} = \Type^{(k)}\times\TypeApp[\k]  \\
 \longpackagetype\ & \in & \PackType = \ExMod \\
% \typefnc[\k]$ {\rm or}\ \typetypefnc{\alphak}{\tau}\
%   {\rm or}\ \typeapptypefnc{\typeapp[\k]}
%         	& \in	& \TypeFnc[\k] = 
%                                      (\TyVar^{(\k)}\times\Type)
%                                      \cup \TypeApp[\k] \\
% \typefnc[\Karr{\K}{\K'}]\ {\rm or}\ \typefnctypefnc{\t[\K]}{\typefnc[\K']}\
%   {\rm or}\ \typeapptypefnc{\typeapp[\Karr{\K}{\K'}]}
%         	& \in	& \TypeFnc[\Karr{\K}{\K'}] = 
%                                     (\TyName[\K]\times\TypeFnc[\K'])
%                                     \cup
%                                     \TypeApp[\Karr{\K}{\K'}] \\
% \typeapp[\K]\ {\rm or}\ \tynametypeapp{\t[K]}\ 
% \ {\rm or}\ \apptypeapp{\typeapp[\Karr{\K'}{\K}]}{\typefnc[\K']}
%         	& \in	& \TypeApp[\K] = 
%                                     \TyName[\K]
%                                     \cup
%                                     (\cup_{\K' \in\ \Kind}
%                                      (\TypeApp[\Karr{\K'}{\K}]
%                                        \times \TypeFnc[\K']) )\\
\typefnc[\k]\ {\rm or}\ 
\typetypefnc{\alphak}{\tau}\ {\rm or}\ 
\typeapptypefnc{\typeapp[\k]}\  & \in	& \TypeFnc[\k] = {} \\
                                &       & \qquad (\TyVar^{(\k)}\times\Type)
                                                 \cup \TypeApp[\k] \\
\typefnc[\keq]\  & \in	& \TypeFnc[\keq] = {}  \\
                                &       & \qquad \{\typefnc[\k]\in\TypeFnc[\k] \; ; \; \typefnc[\k] \mbox{{\sl admits equality}} \}\\
\typefnc[\Karr{\K}{\K'}]\ {\rm or}\ \typefnctypefnc{\t[\K]}{\typefnc[\K']}\
  {\rm or}\ \typeapptypefnc{\typeapp[\Karr{\K}{\K'}]}
        	& \in	& \TypeFnc[\Karr{\K}{\K'}] = {} \\
                &       & \qquad    (\TyName[\K]\times\TypeFnc[\K']) \cup {} \\
                &       & \qquad    \TypeApp[\Karr{\K}{\K'}] \\
\typeapp[\K]\ {\rm or}\ \tynametypeapp{\t[K]}\ 
\ {\rm or}\ \apptypeapp{\typeapp[\Karr{\K'}{\K}]}{\typefnc[\K']}
        	& \in	& \TypeApp[\K] = {} \\
                &       & \qquad    \TyName[\K] \cup {}\\
                &       & \qquad     (\cup_{\K'\in\Kind}
                                     (\TypeApp[\Karr{\K'}{\K}]
                                       \times \TypeFnc[\K']) )\\

\tych\ {\rm or}\ \longtych
        	& \in	& \TypeScheme = \cup_{k\geq 0}\TyVar^{(k)}\times\Type\\
% \S\ {\rm or}\ (\m,\E) & \in	& \Str = \StrNames\times\Env \\ % (cvr)
% (\typefnc[\k],\VE)    & \in   & \TyStr = (\cup_{\k\in\Arity}\TypeFnc[\k])\times\ValEnv\\
% % \SE		& \in	& \StrEnv = \finfun{\StrId}{\Str}\\ % (cvr)
% % \ME		& \in	& \ModEnv = \finfun{\ModId}{\Mod}\\
% \TE		& \in	& \TyEnv = \finfun{\TyCon}{\TyStr}\\
% % \CE             & \in   & \ConEnv = \finfun{\Con}{\TypeScheme}\\ % (cvr)
% % \VE		& \in	& \VarEnv = \finfun{(\Var\cup\Con\cup\Exn)}{\TypeScheme}\\ % (cvr)
% \VE		& \in	& \ValEnv = \finfun{\VId}{\TypeScheme\times\IdStatus}\\ % (cvr)
% % (cvr
% % \EE		& \in	& \ExnEnv = \finfun{\Exn}{\Type}\\ 
% % \E\ {\rm or}\ \longE
% %                 & \in	& \Env = \StrEnv\times\TyEnv\times\VarEnv
% %                                          \times\ExnEnv\\
% % cvr)
%  \E\ {\rm or}\ \longenv
%                  & \in	& \Env = \FunEnv\times\SigEnv\times \\
%                  &      & \qquad \ModEnv\times\TyEnv\times\ValEnv \\
% \T              & \in   & \TyNameSets = \Fin(\TyName)\\
% % \U              & \in   & \TyVarSet = \Fin(\TyVar)\\
% \IE              & \in   & \IdEnv = \finfun{\TyId}{\Type}\\
% \C\ or\ \longcontext   & \in   & \Context =\TyVarSet\times\Env
\end{array}
\end{displaymath}
\caption{Compound Semantic Objects\index{21.2}}
\label{compound-objects}
%\vspace{3pt}
\end{figure}

\begin{figure}[h]
%\vspace{2pt}
\begin{displaymath}
\begin{array}{rcl}
% \S\ {\rm or}\ (\m,\E) & \in	& \Str = \StrNames\times\Env \\ % (cvr)
(\typefnc[\k],\VE)    & \in   & \TyStr = (\cup_{\k\in\Arity}\TypeFnc[\k])\times\ValEnv\\
% \SE		& \in	& \StrEnv = \finfun{\StrId}{\Str}\\ % (cvr)
% \ME		& \in	& \ModEnv = \finfun{\ModId}{\Mod}\\

\TE		& \in	& \TyEnv = \finfun{\TyCon}{\TyStr}\\
% \CE             & \in   & \ConEnv = \finfun{\Con}{\TypeScheme}\\ % (cvr)
% \VE		& \in	& \VarEnv = \finfun{(\Var\cup\Con\cup\Exn)}{\TypeScheme}\\ % (cvr)
\VE		& \in	& \ValEnv = \finfun{\VId}{\TypeScheme\times\IdStatus}\\ % (cvr)
% (cvr
% \EE		& \in	& \ExnEnv = \finfun{\Exn}{\Type}\\ 
% \E\ {\rm or}\ \longE
%                 & \in	& \Env = \StrEnv\times\TyEnv\times\VarEnv
%                                          \times\ExnEnv\\
% cvr)
 \E\ {\rm or}\ \longenv
                 & \in	& \Env = \SigEnv\times\FunEnv\times \\
                 &      & \qquad \StrEnv\times\TyEnv\times\ValEnv \\
\T              & \in   & \TyNameSets = \Fin(\TyName)\\
% \U              & \in   & \TyVarSet = \Fin(\TyVar)\\
\IE              & \in   & \IdEnv = \finfun{\TyId}{\Type}\\
\C\ or\ \longcontext   & \in   & \Context =\IdEnv\times\Env
\end{array}
\end{displaymath}
\caption{Compound Semantic Objects (continued)\index{21.2}}
\label{compound-objects-continued}
%\vspace{3pt}
\end{figure}

% \end{document}
Note that $\Lambda$\index{21.3} and $\forall$ bind type variables.  For any semantic object
$A$, $\TyNamesFcn A$ and $\TyVarsFcn A$ denote respectively the set of
type names and the set of type variables occurring free in $A$.
% (cvr
% Moreover, $\imptyvars A$ and $\apptyvars A$ denote respectively the set
% of imperative type variables and the set of applicative
% type variables occurring free in $A$.\index{21.4}
% cvr)

% (cvr
Also note that a value environment maps value identifiers to a pair of
a type scheme and an identifier status. If $\VE(\vid)=(\tych,\is)$,
we say that $\vid$ {\sl has status} $\is$ in $\VE$.  An occurrence of a
value identifier which is elaborated in $\VE$ is referred to as a
{\sl value variable}, a {\sl value constructor} or an {\sl exception constructor},
depending on whether its status in $\VE$ is $\vstatus$, $\cstatus$ or $\estatus$, respectively.
% cvr)
\subsection{Projection, Injection and Modification}
\label{stat-proj}\index{22.1}
{\bf Projection}: We often need to select components of tuples -- for example,
the variable-environment component of a context. In such cases we
rely on  variable names to indicate which component
is selected. For instance ``$\of{\VE}{\E}$'' means ``the variable-environment
component
of $\E$''.
% and ``$\of{\m}{\S}$'' means ``the structure name of $\S$''. % (cvr)

% Moreover, % (cvr)
When a tuple contains a finite map we shall ``apply'' the
tuple to an argument, relying on the syntactic class of the argument to
determine the relevant function. For instance $\C(\tycon)$ means
$(\of{\TE}{\C})\tycon$.

% (cvr
% A particular case needs mention:  $\C(\con)$ is taken to stand for
% $(\of{\VE}{\C})\con$; similarly, $\C(\exn)$ is taken to stand for
% $(\of{\VE}{\C})\exn$.
%   The type scheme of a value constructor is
% held in $\VE$ as well as in $\TE$ (where it will be recorded within
% a $\CE$); similarly, the type of an exception constructor is held in
% $\VE$ as well as in $\EE$.
% Thus the re-binding of a constructor of either kind is given proper
% effect by accessing it in $\VE$, rather than in $\TE$ or in $\EE$.
% cvr)

% (cvr
% Finally, environments may be applied to long identifiers.
% For instance if $\longcon = \strid_1.\cdots.\strid_k.\con$ then
% $\E(\longcon)$ means
% \[ (\of{\VE}
%        {(\of{\SE}
%             {\cdots(\of{\SE}
%                        {(\of{\SE}{\E})\strid_1}
%                    )\strid_2\cdots}
%         )\strid_k}
%     )\con.
% \]
% cvr)

{\bf Injection}: Components may be injected into tuple classes; for example,\linebreak
``$\VE\ \In\ \Env$'' means the environment
% $(\emptymap,\emptymap,\VE,\emptymap)$. % (cvr)
$(\emptymap,\emptymap,\emptymap,\emptymap, \VE).$ % (cvr)



{\bf Modification}: The modification of one map $f$ by another map $g$,
written $f+g$, has already been mentioned.  It is commonly used for
environment modification, for example $\E+\E'$.  Often, empty components
will be left implicit in a modification; for example $\E+\VE$ means
% $\E+(\emptymap,\emptymap,\VE,\emptymap)$. % (cvr) 
$\E+(\emptymap,\emptymap,\emptymap,\emptymap,\VE)$.  % (cvr) 

%  For set components, modification
% means union, so that 
% % (cvr
% % $\C+(\T,\VE)$ means
% % \[ (\ (\of{\T}{\C})\cup\T,\ \of{\U}{\C},\ (\of{\E}{\C})+\VE\ ) \]
% $\C+(\U,\VE)$ means
% % % \[ (\ (\of{\U}{\C})\cup\U,\ (\of{\E}{\C})+\VE\ ) \]
% % cvr)

% (cvr
% Finally, we frequently need to modify a context $\C$ by an environment $\E$
% (or a type environment $\TE$ say),
% at the same time extending $\of{\T}{\C}$ to include the type names of $\E$
% (or of $\TE$ say).
% We therefore define $\C\oplus\TE$,\index{22.2} for example, to mean
% $\C+(\TyNamesFcn\TE,\TE)$.
% cvr)

% \subsection{Types and Type functions} % (cvr)
\subsection{Types, Type Applications and Type functions} % (cvr)
\label{tyfun-sec}
A type $\tau$ is an {\sl equality type},\index{22.3} or {\sl admits equality}, if it is
of one of the forms
\begin{itemize}
\item $\alpha$, where $\alpha$ admits equality;
\item $\{\lab_1\mapsto\tau_1,\ \cdots,\ \lab_n\mapsto\tau_n\}$,
      where each $\tau_i$ admits equality;
% \item $\tauk\t$, where $t$ and all members of $\tauk$ admit equality; % (cvr)
\item $\apptype{\tauk}{\typeapp}$, where $\typeapp\ \in \TypeApp[\keq]$  and all members of $\tauk$ admit equality; % (cvr)
\item $(\tau')\REF$.\index{23.1}
\end{itemize}
% (cvr
(Note that  if $\tau$ is a package type \longpackagetype\ then 
it \emph{does not} admit equality.)

% A type application $\typeapp$ is an {\sl equality type application},
% \index{22.3} or {\sl admits equality}, if it is
% of one of the forms
% \begin{itemize}
% \item $\t$, where $\t$ admits equality;
% \item $\apptypeapp{\typeapp'}{\typefnc}$, where \typeapp\ and \typefnc\ both
%        admit equality.
% \end{itemize}

A type function $\typefnc$ is an {\sl equality type function},
\index{22.3} or {\sl admits equality}, if it is
of one of the forms
\begin{itemize}
\item \typetypefnc{\alphak}{\tau}, where, when the type variables $\alphak$
      are chosen to admit equality, then $\tau$ also admits equality;
%\item \typefnctypefnc{\t}{\typefnc'}, where,  when the type name $\t$
%      is chosen to admit equality, then $\typefnc'$ also admits equality;
\item \typeapptypefnc{\typeapp}, where $\typeapp\ \in \TypeApp[\keq]$.
\end{itemize}

% cvr)
% (cvr
% \label{tyfcn-lab}
% A type function $\theta=\Lambda\alphak.\tau$\index{23.2}
%  has arity $k$; it must be
% {\sl closed} -- i.e.
% $\TyVarFcn(\tau)\subseteq\alphak$ -- and the bound variables must
% be distinct. Two type functions are considered equal
% if they only differ in their choice of bound variables (alpha-conversion).
% In particular, the equality attribute has no significance in a 
% bound variable of a type function; for example, $\Lambda\alpha.\alpha\to
% \alpha$ and $\Lambda\beta.\beta\to\beta$ are equal type functions
% even if $\alpha$ admits equality but $\beta$ does not.
% %poly 
% Similarly, the imperative attribute has no significance 
% in the bound variable of a type function.
% If $t$ has arity $k$, then we write $t$ to mean $\Lambda\alphak.\alphak\t$
% (eta-conversion); thus $\TyNames\subseteq\TypeFcn$. $\theta=\Lambda\alphak.\tau$
% is an {\sl equality} type function, or {\sl admits equality}, if when the
% type variables $\alphak$ are chosen to admit equality then $\tau$ also admits
% equality.
\label{tyfcn-lab}
The  bound variables of a type function $\theta=\Lambda\alphak.\tau$\index{23.2} must be distinct. 
The type function has the arity $\k$ as its kind. It  may also have kind $\keq$,  provided it admits equality.
A type function $\typefnc=\typefnctypefnc{\t[\K]}{\typefnc'}$\index{23.2}
has kind $\Karr{\K}{\K'}$, provided $\typefnc'$ has kind $\K'$.

Two type functions are considered equal if they have the same kind
and differ only in their choice of bound variables or
type names.
In particular, the equality attribute has no significance in a 
bound type variable of a type function;
for example, $\Lambda\alpha.\alpha\to\alpha$ 
and $\Lambda\beta.\beta\to\beta$
are equal type functions
even if $\alpha$
admits equality but $\beta$ does not.

If the type application \typeapp\ has kind \k\ then we
identify the type function $\typefnc = \typeapp$ with the type function
\typetypefnc{\alphak}{\apptype{\alphak}{\typeapp}}\ 
(provided $(\TyVarsFcn \alphak) \cap (\TyVarsFcn \typeapp) = \emptyset$) (eta-conversion).
If the type application \typeapp\ has kind \Karr{\K}{\K'} then we
identify the type function $\typefnc = \typeapp$ with the type function
\typefnctypefnc{\t[\K]}{\typeapptypefnc{\apptypeapp{\typeapp}{\typeapptypefnc{\t}}}}\
 (provided $\t\not \in \TyNamesFcn \typeapp$) (eta-conversion).

For convenience, when $\t$ has arity $k$, we 
shall write the type name $\t$ to mean
the type function $\typetypefnc{\alphak}{\apptype{\alphak}{\tynametypeapp{\t}}}$.

% cvr)

We write the application of a type function $\typefnc[\k]$ to a vector
$\tauk$ of types as $\tauk\theta$.
If $\typefnc=\typetypefnc{\alphak}{\tau}$ we set $\tauk\theta=\tau\{\tauk/\alphak\}$
(beta-conversion). 

We write $\tau\{\theta^{(\k)}/\t^{(\k)}\}$ for the result of substituting type
functions $\theta^{(k)}$ for type names $\t^{(k)}$ in $\tau$.
We assume that all beta-conversions
are carried out after substitution, so that for example
\[(\tauk\t)\{\typetypefnc{\alphak}{\tau}/\t\}=\tau\{\tauk/\alphak\}.\]
(assuming $\t \not \in \TyNamesFcn \tauk$); and
\[(\typeapptypefnc{\apptypeapp{\t}{\typefnc}})\{\typefnctypefnc{\u}{\typefnc'}/\t\}=
     \typefnc'\{\typefnc/\u\}.\]
(assuming $\t \not \in \TyNamesFcn \typefnc$).

\subsection{Type Schemes}
\label{type-scheme-sec}
A type scheme $\tych=\forall\alphak.\tau$\index{23.3}
 {\sl generalises} a type $\tau'$,
written $\tych \succ\tau'$,
if $\tau'=\tau\{\tauk/\alphak\}$ for some $\tauk$, where each member $\tau_i$
of $\tauk$ admits equality if $\alpha_i$ does.
%poly 
% and $\tau_i$ is imperative if $\alpha_i$ is imperative. % (cvr)
If $\tych'=\forall\beta^{(l)}.\tau'$ then $\tych$ {\sl generalises} $\tych'$,
written $\tych\succ\tych'$, if $\tych\succ\tau'$ and $\beta^{(l)}$ contains
no free type variable of $\tych$.
It can be shown that $\tych\succ\tych'$ iff, for all $\tau''$, whenever
$\tych'\succ\tau''$ then also $\tych\succ\tau''$.

Two type schemes $\tych$ and $\tych'$ are considered equal
if they can be obtained from each other by
renaming and reordering of bound type variables, and deleting type
variables from the prefix which do not occur in the body.
Here, in contrast to the case for type functions, the equality attribute
must be preserved in renaming; for example $\forall\alpha.\alpha\to\alpha$
and $\forall\beta.\beta\to\beta$ are only equal if either both $\alpha$
and $\beta$ admit equality, or neither does.
%poly 
% Similarly, the imperative attribute of a bound type variable of a % (cvr)
% type scheme {\sl is} significant. % (cvr) 
It can be shown that $\tych=\tych'$ iff $\tych\succ\tych'$ and
$\tych'\succ\tych$.

We consider a type $\tau$ to be a type scheme, identifying it with
$\forall().\tau$.

% \subsection{Scope of Explicit Type Variables}
% \label{scope-sec}

% % In\index{23.10} the Core language, a type or datatype binding can 
% % explicitly introduce type variables whose scope is that binding.
% % In the modules, a description of a value, type, or datatype
% % may contain explicit type variables whose scope is that
% % description. However, we\index{23.11} still have to account for the
% % scope of an explicit type variable occurring in the ``\ml{:} $\ty$'' 
% % of a typed expression or pattern 
% % or in the ``\ml{of} $\ty$'' of an exception binding. For the rest
% % of this section, we consider such occurrences of type variables only.

% % Every occurrence of a value declaration is said to
% % {\sl scope} a set of explicit type variables determined as follows.

% % %Every explicit type variable $\alpha$ is {\sl scoped at} a value binding
% % %which is determined as follows.

% % First, an occurrence of $\alpha$ in a value declaration $\valdec$ is said
% % to be {\sl unguarded} if the occurrence is not part of a smaller value
% % declaration within $\valbind$.
% % In this case we say that $\alpha$ {\sl occurs unguarded} in the 
% % value declaration.

% % Then we say that $\alpha$ is {\sl scoped at} a particular occurrence
% % $O$ of $\valdec$ in a program if 
% % (1) $\alpha$ occurs unguarded in this value declaration, and 
% % (2) $\alpha$ does not occur unguarded in any larger value declaration
% % containing the occurrence $O$.\label{scope-def-lab}

% % Hence, associated with every occurrence of a value declaration there is 
% % a set $\U$ of the explicit type variables that are scoped at that
% % occurrence. One may think of each occurrence of $\VAL$ as being implicitly
% % decorated with such a  set, for instance:

% % \vspace*{3mm}
% % \halign{\indent$#$&$#$&$#$\cr
% % \mbox{$\VAL_{\{\}}$ \ml{x = }}&\mbox{\ml{(}}&
% % \mbox{\ml{let $\VAL_{\{\mbox{\ml{'a}}\}}$ Id1:'a->'a = fn z=>z in Id1 Id1 end,}}\cr
% % & &\mbox{\ml{let $\VAL_{\{\mbox{\ml{'a}}\}}$ Id2:'a->'a = fn z=>z in Id2 Id2 end)}}\cr
% % \noalign{\vspace*{3mm}}
% % \mbox{$\VAL_{\{\mbox{\ml{'a}}\}}$ \ml{x = }}&\mbox{\ml{(}}&
% % \mbox{\ml{let $\VAL_{\{\}}$ Id:'a->'a = fn z=>z in Id Id end,}}\cr
% % & &\mbox{\ml{fn z=> z:'a)}}\cr}

% % According to the inference rules in Section~\ref{stat-cor-inf-rules}
% % the first example can be elaborated, but the second cannot since \ml{'a}
% % is bound at the outer value declaration leaving no possibility of two 
% % different instantiations of the type of \ml{Id} in the application
% % \ml{Id Id}.

% In\index{23.10} the Core language, a type or datatype binding can explicitly
% introduce type variables whose scope is that binding. Moreover, in a
% value declaration \valdec, the sequence \tyvarseq\ binds
% type variables: a type variable occurs free in \valdec\
% iff it occurs free in \valbind\ and is not in the sequence
% \tyvarseq. However,\index{23.11} explicit binding of type variables at \ml{val}\ is
% optional, so we still have to account for the scope of an explicit
% type variable occurring in the ": \ty" of a typed expression or pattern
% or in the "of \ty" of an exception binding. For the rest of this
% section, we consider such free occurrences of type variables only.

% Every occurrence of a value declaration is said to {\sl scope} a set of explicit type variables determined as follows.

% First, a free occurrence of $\alpha$ in a value declaration
% \valdec\ is said to be {\sl unguarded} if the occurrence is not part
% of a smaller value declaration within \valbind . In this case we say
% that {\sl $\alpha$ occurs unguarded} in the value declaration.

% Then we say that $\alpha$ is {\sl implicitly} scoped at a particular value
% declaration \valdec\ in a program if (1) $\alpha$ occurs
% unguarded in this value declaration, and (2) $\alpha$ does not occur
% unguarded in any larger value declaration containing the given one.
% \label{scope-def-lab}

% Henceforth, we assume that for every value declaration $\VAL\ \tyvarseq\cdots$
%  occurring in the program, every explicit type variable implicitly scoped at the val has been added to \tyvarseq . Thus for example, in the two declarations

% \begin{verbatim}
% val x = let val id:'a->'a = fn z=>z in id id end 
% val x = (let val id:'a->'a = fn z=>z in id id end; fn z=>z:'a)
% \end{verbatim}
% the type variable \verb+'a+ is scoped differently; they become respectively

% \begin{verbatim}
% val x = let val 'a id:'a->'a = fn z=>z in id id end
% val 'a x = (let val id:'a->'a = fn z=>z in id id end; fn z=>z:'a)
% \end{verbatim}

% Then, according to the inference rules in Section~\ref{stat-cor-inf-rules} the first example can be elaborated, but the second cannot since
% \verb+'a+ is bound at the outer value declaration leaving no possibility of two different instantiations of the type of
% \verb+id+ in the application \verb+id id+.




\subsection{Non-expansive Expressions}
\label{expansive-sec}
% (cvr
% In\index{23.4} order to treat polymorphic references and exceptions,
% the set Exp of expressions is partitioned into two classes, the {\sl 
% expansive} and the {\sl non-expansive} expressions. Any variable,
% constructor and $\FN$ expression, possibly constrained by one or more
% type expressions, is non-expansive; all other expressions are said to
% be expansive.  The idea is that the dynamic evaluation of a
% non-expansive expression will neither generate an exception nor extend
% the domain of the memory, while the evaluation of an expansive
% expression might.
% cvr)

In\index{23.4} order to treat polymorphic references and exceptions,
 the set {\rm Exp} of expressions is partitioned into two classes, the
 {\sl expansive} and the {\sl non-expansive} expressions. An
 expression is {\sl non-expansive in context $\C$} if, after replacing
 infixed forms by their equivalent prefixed forms, and derived forms
 by their equivalent forms, it can be generated by the following
 grammar from the non-terminal ${\it nexp}$:

%\begin{figure}[h]
%\vspace{4pt}
\makeatletter{}
\tabskip\@centering
\halign to\textwidth
{\hfil$#$\tabskip1em&\hfil$#$\hfil&$#$\hfil&#\hfil\tabskip\@centering\cr
% (cv
%\nvidpath & ::= & \opp\longvid & \cr
%          &     & \nanonvidpath & \cr
\nexp   & ::= & \scon & \cr
        &     & \opp\longvid & \cr
        &     & \ttlbrace\langle\nexprow\rangle\ttrbrace & \cr
        &     & \verb+(+\nexp\verb+)+ & \cr
        &     & \conexp\ \nexp & \cr
        &     & \nexp \verb+:+ \ty & \cr
        &     & \FN\ \match &\cr
        &     & \nstructureexp & \cr        
        &     & \nfunctorexp & \cr        
\nexprow & ::= & \lab\ \tteq\ \nexp\ \langle\ \verb+,+ \nexprow \rangle & \cr
\conexp & ::= & \verb+(+ \conexp \langle\verb+:+\ty\rangle\verb+)+ & \cr
        &     &  \opp\longvid & \cr
%Restriction: $\nvidpath \neq \REF$ and \cr
%        &     &  & ${\C\ts\nvidpath\ra(\tych,\is)}$  where \cr
%        &     &  & $\is \in\{\cstatus,\estatus\}$ \cr
\nmodexp  & ::= & \opp\longmodid & \cr
          &     & \nparatmodexp\ & \cr
          &     & \nconmodexp\ & \cr
          &     & \nabsmodexp\ & \cr
          &     & \ngenfunctormodexp\ & \cr
          &     & \nappfunctormodexp\ & \cr
          &     & \nrecmodexp\ & \cr
}
\makeatother
%\vspace{2mm}
%\end{figure}

%\hangindent=\parindent\hangafter=0
\noindent
{\sl Restriction:}\/ Within a $\conexp$, we require $\longvid\neq\REF$ and
$\of{\is\,}{\,\C(\longvid)}\in\{\cstatus,\estatus\}$.\medskip

All other expressions are said to be {\sl expansive (in C)}. The idea is that the dynamic evaluation of a non-expansive expression will neither generate an exception nor extend the domain of the memory, while the evaluation of an expansive expression might.

\subsection{Closure}
\label{closure-sec}
Let\index{24.2} $\tau$ be a type and $A$ a semantic object. Then $\cl{A}{(\tau)}$,
the {\sl closure} of $\tau$ with respect to $A$, is the type scheme
$\forall\alphak.\tau$, where $\alphak=\TyVarFcn(\tau)\setminus\TyVarFcn A$.
Commonly, $A$ will be a context $\C$.
We abbreviate the {\sl total} closure $\cl{\emptymap}{(\tau)}$ to
$\cl{}{(\tau)}$.
If the range of a 
% variable  % (cvr)
value % (cvr)
environment $\VE$ contains only types (rather than
arbitrary type schemes) we set
% \[\cl{A}{\VE}=\{\id\mapsto\cl{A}{(\tau)}\ ;\ \VE(\id)=\tau\}\] % (cvr)
\[\cl{A}{\VE}=\{\vid\mapsto(\cl{A}{(\tau),\is)}\ ;\ \VE(\vid)=(\tau,\is)\}\] % (cvr)
% with a similar definition for $\cl{A}{\CE}$. % (cvr)

\label{clos-def-lab}
Closing\index{24.3} a variable environment $\VE$ that stems from
the elaboration of a value binding $\valbind$ requires extra
care to ensure type security of references and exceptions and correct
scoping of explicit type variables.
Recall that $\valbind$ is not allowed to bind the
same variable twice. 
% Thus, for each $\var\in\Dom\VE$ 
% there is a unique \mbox{\pat\ \ml{=} \exp}
% in $\valbind$ which binds $\var$. 
% If $\VE(\var)=\tau$, let 
% $\cl{\C,\valbind}{\VE(\var)}=\longtych$, where
% \[\alphak=\cases{\TyVarFcn\tau\setminus\TyVarFcn\C,&if $\exp$ 
%                                                     is non-expansive;\cr
%                  \apptyvars\tau\setminus\TyVarFcn\C,&if $\exp$ is expansive.}
% \]
Thus, for each $\vid\in\Dom\VE$ 
there is a unique \mbox{\pat\ \ml{=} \exp}
in $\valbind$ which binds $\vid$. 
If $\VE(\vid)=(\tau,\is)$, let 
$\cl{\C,\valbind}{\VE(\vid)}=(\longtych,\is)$, where
\[\alphak=\cases{\TyVarFcn\tau\setminus\TyVarFcn\C,&if $\exp$ 
                                                    is non-expansive in $\C$;\cr
                 ()                                &if $\exp$ is expansive in $\C$.}
\]

%(Explicit type variables necessitate a slight strengthening of the requirements
%which a type variable must satisfy in order to be bound: a type variable 
%occurring unguarded in $\valbind$ can be admitted among $\alphak$ only
%if it is scoped at the particular occurrence of $\valbind$ at which
%the closure operation is performed.)

% (cvr
% Notice that the form of $\valbind$ does not affect the binding of
% applicative type variables, only the binding of imperative
% type variables.
% cvr)
\subsection{Existential and Parameterised Objects}

When $A$ is a set of semantic objects,
 the set \EXISTENTIAL{A}\ of
\emph{existentially quantified objects in $A$} and the set
\PARAMETERISED{A}\ of \emph{parameterised objects in $A$} 
are defined as follows:
\begin{displaymath}
\begin{array}{rcl}
   \EXISTS{\T}{a} & \in  & \EXISTENTIAL{A} = \TyNameSets \times  A \\
   \LAMBDA{\T}{a} & \in  & \PARAMETERISED{A}  = \TyNameSets \times A 
\end{array}
\end{displaymath}
(where $a$ ranges over elements of $A$).

The prefixes \EXISTS{\T}{\_}\ and \LAMBDA{\T}{\_} are binding constructs.
Two objects in \EXISTENTIAL{A}\ ( \PARAMETERISED{A}) are considered equal
if they are equivalent up to a 
kind 
%and attribute 
preserving renaming of their bound types names.

\subsection{Type Structures and Type Environments}
\label{typeenv-wf-sec}

% A type\index{24.4} structure $(\theta,\CE)$ is {\sl well-formed} if either
% $\CE=\emptymap$, or $\theta$ is a type name $t$.
% (The latter case arises, with $\CE\neq\emptymap$, in $\DATATYPE$
% declarations.)
% All type structures occurring in elaborations are assumed to
% be well-formed.

A type\index{24.4} structure $(\typefnc[\k],\VE)$ is {\sl well-formed} if either
$\VE=\emptymap$, or $\typefnc[\k]$ is a type application $\typeapp[\k]$.
(The latter case arises, with $\VE\neq\emptymap$, in $\DATATYPE$
declarations.)
All type structures occurring in elaborations are assumed to
be well-formed.

% {\bf
% WE EITHER HAVE TO GENERALISE THE NOTION OF 
% WELL-FORMEDNESS TO HIGHER-ORDER
% OR DROP THE REQUIREMENT ALTOGETHER PROVIDED IT DOESN'T VIOLATE SOUNDNESS.
% NOTE THAT WELL-FORMEDNESS OCCURS AS A SIDE CONDITION IN PRECISELY ONE RULE ---
% RULE 64 IN SML'97 FOR PHRASE:
% \[ \wheresigexp. \]
% THE ORIGINAL DEFINITION IS:
% \begin{quote}
% ``A type\index{24.4} structure $(\typefnc,\VE)$ is {\sl well-formed} if either
% $\VE=\emptymap$, or $\typefnc$ is a type name $t$.
% (The latter case arises, with $\VE\neq\emptymap$, in $\DATATYPE$
%  declarations.)
%  All type structures occurring in elaborations are assumed to
%  be well-formed.''
% \end{quote} 
% \bf}

% (cvr
% A type structure $(\t,\CE)$ is said to
% {\sl respect equality} if, whenever $\t$ admits equality, then
% either $\t=\REF$ (see Appendix~\ref{init-stat-bas-app}) or,
% for each $\CE(\con)$ of the form 
% $\forall\alphak.(\tau\rightarrow\alphak\t)$,
% the type function $\Lambda\alphak.\tau$ also admits equality.
% (This ensures that the equality
% predicate ~{\tt =}~ will be applicable to a constructed value $(\con,v)$ of
% type $\tauk\t$ only when it is applicable to the value $v$ itself,
% whose type is $\tau\{\tauk/\alphak\}$.)
% A type environment $\TE$ {\sl respects equality} if all its type
% structures do so.

% Let $\TE$ be a type environment, and let $T$ be the set of type names
% $\t$ such that $(\t,\CE)$ occurs in $\TE$ for some
% $\CE\neq\emptymap$.  Then $\TE$ is said to {\sl maximise equality}
% if (a) $\TE$ respects equality, and also (b) if any larger subset of
% $T$ were to admit equality (without any change in the equality
% attribute of any type names not in $T$) then $\TE$ would cease to
% respect equality.


% For any $\TE$ of the form
% \[\TE=\{\tycon_i\mapsto(t_i,\CE_i)\ ;\ 1\leq i\leq k\},\]
% where no $\CE_i$ is the empty map, and for any $\E$ we define
% $\Abs(\TE,\E)$ to\index{25.1} be the environment obtained from 
% $\E$ and $\TE$ as
% follows. First, let $\Abs(\TE)$ be the type environment
% $\{\tycon_i\mapsto(t_i,\emptymap)\ ;\ 1\leq i\leq k\}$
% in which all constructor
% environments $\CE_i$ have been replaced by the empty map. 
% Let $t_1',\cdots,t_k'$ be new distinct type names none of which
% admit equality. Then $\Abs(\TE,\E)$ is the result of simultaneously
% substituting
% $t_i'$ for $t_i$, $1\leq i\leq k$,  throughout $\Abs(\TE)+\E$. 
% (The effect of the latter substitution is to ensure that the use of 
% equality on  an $\ABSTYPE$ is restricted to the $\WITH$ part.)
% \label{abs-lab}
% \clearpage
 
A type structure $(\typeapp,\VE)$ is said to
{\sl respect equality} if, whenever $\typeapp\in\TypeApp[\keq]$ 
(i.e.\ \typeapp\ admits equality), then
either $\typeapp=\REF$ (see Appendix~\ref{init-stat-bas-app}) or,
for each $\VE(\vid)$ of the form 
$\forall\alphak.(\tau\rightarrow\alphak\typeapp)$,
the type function $\typetypefnc{\alphak}{\tau}$ also admits equality.
(This ensures that the equality
predicate ~{\tt =}~ will be applicable to a constructed value $(\vid,v)$ of
type $\tauk\typeapp$ only when it is applicable to the value $v$ itself,
whose type is $\tau\{\tauk/\alphak\}$.)
A type environment $\TE$ {\sl respects equality} if all its type
structures do so.

Let $\TE$ be a type environment, and let $T$ be the set of type names
$\t$ such that $(\t,\VE)$ occurs in $\TE$ for some
$\VE\neq\emptymap$.  Then $\TE$ is said to {\sl maximise equality}
if (a) $\TE$ respects equality, and also (b) if any larger subset of
$T$ were to admit equality (without any change in the equality
attribute of any type names not in $T$) then $\TE$ would cease to
respect equality.


For any $\TE$ of the form
\[\TE=\{\tycon_i\mapsto(t_i,\VE_i)\ ;\ 1\leq i\leq k\},\]
where no $\VE_i$ is the empty map, and for any $\E$ we define
$\Abs(\TE,\E)$ to\index{25.1} be the environment obtained from 
$\E$ and $\TE$ as
follows. First, let $\Abs(\TE)$ be the type environment
$\{\tycon_i\mapsto(t_i,\emptymap)\ ;\ 1\leq i\leq k\}$
in which all value
environments $\VE_i$ have been replaced by the empty map. 
Let $T'=\{t_1',\cdots,t_k'\}$ be a set of new distinct type names,
 none of which admit equality,
and where  $t_i'$ has the same arity as $t_i$ for $1\leq i\leq k$.
Then $\Abs(\TE,\E)=\EXISTS{\T'}{\E'}$, where $\E'$ is the result of simultaneously
substituting
$t_i'$ for $t_i$, $1\leq i\leq k$,  throughout $\Abs(\TE)+\E$, i.e.\
$\E' = (\Abs(\TE)+\E)\{t'^{(k)}/ t^{(k)}\} $ 
(The effect of the latter substitution is to ensure that the use of 
equality on  an $\ABSTYPE$ is restricted to the $\WITH$ part.)
\label{abs-lab}
%\clearpage

% cvr)

\subsection{Inference Rules}
\label{stat-cor-inf-rules}
% (cvr
% Each rule\index{26.1} of the semantics allows inferences among sentences of the form
% \[A\ts{\it phrase}\ra A'\]
% where
% $A$ is usually an environment or a context, {\it phrase} is a phrase of
% the Core, and $A'$ is a semantic object -- usually a type or an
% environment.  It may be pronounced ``{\it phrase} elaborates to $A'$ in
% (context or environment) $A$''.  Some rules have extra hypotheses not of
% this form; they are called {\sl side conditions}.  

Each rule\index{26.1} of the semantics allows inferences among sentences of the form
\[A\ts{\it phrase}\ra A'\]
where
$A$ is typically a context, {\it phrase} is a phrase of
the Core, and $A'$ is a semantic object -- typically a type or an
existentially quantified environment. 
It may be pronounced ``{\it phrase} elaborates to $A'$ in
(context or environment) $A$''.  Some rules have extra hypotheses not of
this form; they are called {\sl side conditions}.  
% cvr)
In the presentation of the rules, phrases within single
angle brackets ~$\langle\ \rangle$~ are called {\sl
first options}, and those within double
angle brackets ~$\langle\langle\ \rangle\rangle$~ are called {\sl
second options}.  To reduce the number of rules, we have adopted the
following convention:
\begin{quote} In each instance of a rule, the
first options must be either all present or all absent;
similarly the second options must be either all present or all absent.
\end{quote}

% (cvr
% Although not assumed in our definitions, it is intended that every
% context $\C=\T,\U,\E$ has the property that $\TyNamesFcn\E\subseteq\T$.
% Thus $\T$ may be thought of, loosely, as containing all type names
% which ``have been generated''. It is necessary to include $\T$ as a
% separate component in a context, since $\TyNamesFcn\E$ may not contain
% all the type names which have been generated; one reason is that a
% context $\T,\emptyset,\E$ is a projection of the basis
% $\B=(\M,\T),\F,\G,\E$ whose other components $\F$ and $\G$
% could contain other such names -- recorded in $\T$ but not present in
% $\E$.  Of course, remarks about what ``has been generated'' are not
% precise in terms of the semantic rules. But the following precise result
% may easily be demonstrated:
% \begin{quote}
% Let S be a sentence
% ~$\T,\U,\E\ts{\it phrase}\ra A$~ such that
% $\TyNamesFcn\E\subseteq\T$,
% and let S$'$ be a sentence
% ~$\T',\U',\E'\ts{\it phrase}'\ra A'$~
% occurring in a proof of S; then also
% $\TyNamesFcn\E'\subseteq\T'$.
% \end{quote}
% cvr)

\rulesec{Long Value Identifiers}{\C\ts\longvid\ra(\tych,\is)}

\begin{equation}	% idlongvid
\label{idlongvid-rule}
\frac{\vid\in\Dom\C}
     {\C\ts\idlongid{\vid}\ra\C(\vid)}
\end{equation}

\begin{equation}	% dotlongvid
%\label{dotlongvid-rule}
\frac{\begin{array}{lcr}
      \C\ts\longstrid\ra\RS & 
      \S = \of\S\RS&
      \vid\in\Dom\S
      \end{array}
      }
     {\C\ts\dotlongid{\longstrid}{\vid}\ra\S(\vid)}
\end{equation}

%\rulesec{Value Identifier Paths}{\C\ts\vidpath\ra(\tych,\is)}

% \begin{equation}	% longvidvidpath
% \label{longvidpath-rule}
% \frac{\C\ts\longvid\ra(\tych,\is)}
%      {\C\ts\longvidpath\ra(\tych,\is)}
% \end{equation}

% \begin{equation}	% anonvidpath
% \label{anonvidpath-rule}
% \frac{\begin{array}{l}
%       \C\ts^\expectstr\modexp\ra\exmod{\T}{RS} \\
%       \C+\{\strid\mapsto\RS\}\ts\longvidpath\ra(\tych,\is)\\
%       \T\cap(\TyNamesFcn(\C) \cup \TyNamesFcn(\tych)) = \emptyset 
%       \end{array}
%       }
%      {\C\ts\anonvidpath\ra(\tych,\is)}
% \end{equation}


%                       Atomic Expressions
%
\rulesec{Atomic Expressions\index{26.2}}{\C\vdash\atexp\ra\tau}
%\begin{figure}[h]

\begin{equation}	% special constant
\label{sconexp-rule}
\frac{}
     {\C\ts\scon\ra\scontype(\scon)}\index{26.3}
\end{equation}

% (cvr
%  \begin{equation}	% value variable
%  \label{vidpath-rule}
%   \frac{\begin{array}{lr}
%        \C\ts\vidpath\ra(\tych,\is) &
%        \tych\succ\tau
%        \end{array}}
%       {\C\ts\vidpath\ra\tau}
%  \end{equation}

\begin{equation}	% value variable
  \label{longvidexp-rule}
   \frac{\begin{array}{lr}
        \C\ts\longvid\ra(\tych,\is) &
        \tych\succ\tau
        \end{array}}
       {\C\ts\longvid\ra\tau}
\end{equation}

% \begin{equation}	% value variable
% \label{varexp-rule}
% \frac{\C(\longvar)\succ\tau}
%      {\C\ts\longvar\ra\tau}
% \end{equation}

% \begin{equation}	% value constructor
% \label{conexp-rule}
% \frac{\C(\longcon)\succ\tau}
%      {\C\ts\longcon\ra\tau}
% \end{equation}

% \begin{equation}      % exception constant
% %\label{exconexp-rule}
% \frac{\C(\longexn)=\tau}
%      {\C\ts\longexn\ra\tau}
% \end{equation}

\begin{equation}	% record expression
%\label{recexp-rule}
\frac{\langle\C\ts\labexps\ra\varrho\rangle}
     {\C\ts\ttlbrace\ \recexp\ \ttrbrace\ra\emptymap\langle +\ \varrho\rangle{\rm\ in\ \Type}}\index{27.0}
\end{equation}
% cvr)

% (cvr
% \begin{equation}        % local declaration
% \label{let-rule}
% \frac{\C\ts\dec\ra\E\qquad\C\oplus\E\ts\exp\ra\tau}
%      {\C\ts\letexp\ra\tau}\index{27.1}
% \end{equation}

 \begin{equation}        % local declaration
 \label{let-rule}
 \frac{\begin{array}{lr}
       \C\ts\dec\ra\EXISTS{\T}{\E} &
       \T \cap \TyNamesFcn \C = \emptyset \\
       \C + \E\ts\exp\ra\tau &
       \T \cap \TyNamesFcn \tau = \emptyset \\
      \end{array}}
      {\C\ts\letexp\ra\tau}\index{27.1}
 \end{equation}

% cvr)

\begin{equation}        % structure expression
\label{structureatexp-rule}
 \frac{\begin{array}{l}
       \C\ts^\expectstr\modexp\ra\exmod{\T}{\RS} \\
       \C\ts\sigexp\ra\sig{\T'}{\RS'} \\
       \T \cap \TyNamesFcn (\sig{\T'}{\RS'}) = \emptyset \\
       \siginstantiates{\sig{\T'}{\RS'}}{\RS''}\prec\RS\\ 
      \end{array}}
      {\C\ts\structureatexp\ra\packagetype{\exmod{\T'}{\RS'}}}%\index{27.1}
\end{equation}

\begin{equation}        % functor expression
\label{functoratexp-rule}
 \frac{\begin{array}{l}
       \C\ts^\expectfun\modexp\ra\exmod{\T}{\F} \\
       \C\ts\sigexp\ra\sig{\T'}{\F'} \\
       \T \cap \TyNamesFcn (\sig{\T'}{\F'}) = \emptyset \\
       \siginstantiates{\sig{\T'}{\F'}}{\F''}\prec\F\\ 
      \end{array}}
      {\C\ts\functoratexp\ra\packagetype{\exmod{\T'}{\F'}}}%\index{27.1}
\end{equation}



% \begin{equation}        % pack expression
% \label{openatexp-rule}
%  \frac{\begin{array}{l}
%        \C\ts\exp_1\ra\packagetype{\exmod{\T}{\M}}\\
%        \C\ts\sigexp\ra\sig{\T}{\M} \\
%        \T \cap \TyNamesFcn (\C) = \emptyset \\
%        C + \{\modid\mapsto\M\}\ts\exp_2\ra\tau\\
%        \T \cap \TyNamesFcn (\tau) = \emptyset \\ 
%       \end{array}}
%       {\C\ts\openatexp\ra\tau}%\index{27.1}
% \end{equation}


\begin{equation}	% paren expression
%\label{parexp-rule}
\frac{\C\ts\exp\ra\tau}
     {\C\ts\parexp\ra\tau}
\end{equation}
\comments
\begin{description}
% \item{(\ref{varexp-rule}),(\ref{conexp-rule})}  % (cvr)
\item{(\ref{longvidexp-rule})}  % (cvr)
The instantiation of 
type schemes allows different occurrences of a single $\longvid$ 
to assume different types.
\item{(\ref{let-rule})} 
% The use of $\oplus$, here and elsewhere, ensures that
% type names generated by the first sub-phrase are different from 
% type names generated by the second sub-phrase
The first side condition (that also occurs elsewhere in the rules)
ensures that type names generated by the first sub-phrase are distinct
from type names already appearing in the context. 
The second side condition prevents these type names from escaping
outside the local declaration. 
\end{description}

\rulesec{Expression Rows}{\C\ts\labexps\ra\varrho}
\begin{equation}	% expression rows
%\label{labexps-rule}
\frac{\C\ts\exp\ra\tau\qquad\langle\C\ts\labexps\ra\varrho\rangle}
     {\C\ts\longlabexps\ra\{\lab\mapsto\tau\}\langle +\ \varrho\rangle}\index{27.2}
\end{equation}


%                        Expressions
%
\rulesec{Expressions}{\C\ts\exp\ra\tau}
%\vspace{6pt}
%\fbox{$\C\ts\exp\ra\tau$}
\begin{equation}	% atomic
\label{atexp-rule}
\frac{\C\ts\atexp\ra\tau}
     {\C\ts\atexp\ra\tau}\index{27.3}
\end{equation}

\begin{equation}	% application
%\label{app-rule}
\frac{\C\ts\exp\ra\tau'\rightarrow\tau\qquad\C\ts\atexp\ra\tau'}
     {\C\ts\appexp\ra\tau}
\end{equation}

\begin{equation}	% typed
\label{typedexp-rule}
\frac{\C\ts\exp\ra\tau\qquad\C\ts\ty\ra\tau}
     {\C\ts\typedexp\ra\tau}
\end{equation}

\begin{equation}        % handle exception
%\label{handlexp-rule}
\frac{\C\ts\exp\ra\tau\qquad\C\ts\match\ra\EXCN\rightarrow\tau}
     {\C\ts\handlexp\ra\tau}
\end{equation}

\begin{equation}        % raise exception
\label{raiseexp-rule}
\frac{\C\ts\exp\ra\EXCN}
     {\C\ts\raisexp\ra\tau}
\end{equation}

\begin{equation}        % function
%\label{fnexp-rule}
\frac{\C\ts\match\ra\tau}
     {\C\ts\fnexp\ra\tau}
\end{equation}
\comments
\begin{description}
\item{(\ref{atexp-rule})}
The relational symbol $\ts$ is overloaded for all syntactic classes (here
atomic expressions and expressions).
\item{(\ref{typedexp-rule})}
Here $\tau$ is determined by $\C$ and $\ty$. Notice that type variables
in $\ty$ cannot be instantiated in obtaining $\tau$; thus the expression
\verb+1:'a+ will not elaborate successfully, nor will the expression
\verb+(fn x=>x):'a->'b+.
The effect of type variables in an explicitly typed expression is
to indicate exactly the degree of polymorphism present in the expression.\index{27.4}
\item{(\ref{raiseexp-rule})}
Note that $\tau$ does not occur in the premise; thus a $\RAISE$
expression has ``arbitrary'' type.
\end{description}
%                        Matches 
%
\rulesec{Matches}{\C\ts\match\ra\tau}
\begin{equation}	% match
%\label{match-rule}
\frac{\C\ts\mrule\ra\tau\qquad\langle\C\ts\match\ra\tau\rangle}
     {\C\ts\longmatch\ra\tau}\index{28.1}
\end{equation}
\rulesec{Match Rules}{\C\ts\mrule\ra\tau}
\begin{equation}	% mrule
%\label{mrule-rule}
\frac{\C\ts\pat\ra(\VE,\tau)\qquad\C+\VE\ts\exp\ra\tau'}
     {\C\ts\longmrule\ \ra\tau\rightarrow\tau'}
\end{equation}
\comment  This rule allows new free type variables to enter
the context. These new type variables will be chosen, in effect, during
the elaboration of $\pat$ (i.e., in the inference of the first
hypothesis). In particular, their choice may have to be made to
agree with type variables present in any explicit type expression
occurring within $\exp$ (see rule~\ref{typedexp-rule}).

%
%                        Declarations
%
% \rulesec{Declarations}{\C\ts\dec\ra\E} % (cvr)
\rulesec{Declarations}{\C\ts\dec\ra\EXISTS{\T}{\E}} % (cvr)

% (cvr
% %poly
%  \begin{equation}	% value declaration
%  \label{valdec-rule}
%  \frac{\plusmap{\C}{\U}\ts\valbind\ra\VE\qquad 
%        \VE'=\cl{\C,\valbind}{\VE}\qquad
%        \U\cap\TyVarFcn\VE'=\emptyset}
%       {\C\ts\valdecS\ra\VE'\ \In\ \Env}\index{28.2}
%  \end{equation}
% % from version 1, without polymorphic refs:
% %\begin{equation}	% value declaration
% %\label{valdec-rule}
% %\frac{\C\ts\valbind\ra\VE}
% %     {\C\ts\valdec\ra\cl{\C}{\VE}\ \In\ \Env}
% %\end{equation}

% \begin{equation}	% type declaration
% %\label{typedec-rule}
% \frac{\C\ts\typbind\ra\TE}
%      {\C\ts\typedec\ra\TE\ \In\ \Env}
% \end{equation}

% \begin{equation}	% datatype declaration
% \label{datatypedec-rule}
% \frac{\begin{array}{c}
% \C\oplus\TE\ts\datbind\ra\VE,\TE\qquad
%       \forall(\t,\CE)\in\Ran\TE,\ \t\notin(\of{\T}{\C}) \\
%      \mbox{$\TE$ maximises equality}
%      \end{array}
%      }
%      {\C\ts\datatypedec\ra(\VE,\TE)\ \In\ \Env}
% \end{equation}

% \begin{equation}	% abstype declaration
% \label{abstypedec-rule}
% \frac{\begin{array}{rl}
%       \C\oplus\TE\ts\datbind\ra\VE,\TE\qquad &
%       \forall(\t,\CE)\in\Ran\TE,\ \t\notin(\of{\T}{\C})\\
%       \C\oplus(\VE,\TE)\ts\dec\ra\E\qquad & 
%      \mbox{$\TE$ maximises equality}
%       \end{array}
%      }
%      {\C\ts\abstypedec\ra\Abs(\TE,\E)}
% \end{equation}

% \begin{equation}	% exception declaration
% \label{exceptiondec-rule}
% \frac{\C\ts\exnbind\ra\EE\quad\VE=\EE }
%      {\C\ts\exceptiondec\ra(\VE,\EE)\ \In\ \Env }
% \end{equation}

% \begin{equation}	% local declaration
% %\label{localdec-rule}
% \frac{\C\ts\dec_1\ra\E_1\qquad\C\oplus\E_1\ts\dec_2\ra\E_2}
%      {\C\ts\localdec\ra\E_2}\index{28.3}
% \end{equation}

% \begin{equation}                % open declaration
% %\label{open-dec-rule}
% \frac{ \C(\longstrid_1)=(\m_1,\E_1)
%             \quad\cdots\quad
%        \C(\longstrid_n)=(\m_n,\E_n) }
%      { \C\ts\openstrdec\ra \E_1 + \cdots + \E_n }
% \end{equation}

% \begin{equation}	% empty declaration
% %\label{emptydec-rule}
% \frac{}
%      {\C\ts\emptydec\ra\emptymap\ \In\ \Env}
% \end{equation}

% \begin{equation}	% sequential declaration
% %\label{seqdec-rule}
% \frac{\C\ts\dec_1\ra\E_1\qquad\C\oplus\E_1\ts\dec_2\ra\E_2}
%      {\C\ts\seqdec\ra\plusmap{E_1}{E_2}}
% \end{equation}

% cvr)

 \begin{equation}	% value declaration
 \label{valdec-rule}
 \frac{\begin{array}{lr}
       \C\ts\tyidseq\ra(\alpha_1,\cdots,\alpha_k),{\IE} &
       \plusmap{\C}{\IE}\ts\valbind\ra\VE \\
       \VE'=\cl{\C,\valbind}{\VE} & 
       \{\alpha_1,\cdots,\alpha_k\} \cap {\TyVarsFcn\VE'}=\emptyset
       \end{array}}
      {\C\ts\valdec\ra\EXISTS{\emptyset}{\VE'\ \In\ \Env}}\index{28.2}
 \end{equation}


\begin{equation}	% type declaration
%\label{typedec-rule}
\frac{\C\ts\typbind\ra\TE}
     {\C\ts\typedec\ra\EXISTS{\emptyset}{\TE\ \In\ \Env}}
\end{equation}

\begin{equation}	% datatype declaration
\label{datatypedec-rule}
\frac{\begin{array}{l}
      \C + \TE\ts\datbind\ra\VE,\TE \\
      \T = \{\t; (\t, \VE') \in\Ran\TE\} \\
      \T \cap \TyNamesFcn \C = \emptyset \\
      \mbox{$\TE$ maximises equality}
     \end{array}
     }
     {\C\ts\datatypedec\ra\EXISTS{\T}{(\VE,\TE)\ \In\ \Env}}
\end{equation}


\begin{equation}	% datatype replication
\label{datatyperepdec-rule}
\frac{\begin{array}{c}
      \C\ts\tyconpath\ra(\typefnc,\VE) \\
      \TE = \{ \tycon\mapsto(\typefnc,\VE)\}
     \end{array}
     }
     {\begin{array}{c}
        \C\ts\datatyperepdec\ra\\
         \qquad\EXISTS{\emptyset}{(\VE,\TE)\ \In\ \Env}
      \end{array}}
\end{equation}

\begin{equation}	% abstype declaration
\label{abstypedec-rule}
\frac{\begin{array}{lr}
      \C+\TE\ts\datbind\ra\VE,\TE &
      \T = \{\t; (\t, \VE) \in\Ran\TE\} \\
      \mbox{$\TE$ maximises equality} &
      \T \cap \TyNamesFcn \C = \emptyset\\
      \C+(\VE,\TE)\ts\dec\ra\EXISTS{\T'}{\E} & 
      \T' \cap \T = \emptyset \\
      \Abs(\TE,E) = \EXISTS{\T''}{\E'} &
      \T'' \cap \T' = \emptyset 
      \end{array}
     }
     {\C\ts\abstypedec\ra\EXISTS{\T'\cup\T''}{\Abs(\TE,\E)}}
\end{equation}

\begin{equation}	% exception declaration
\label{exceptiondec-rule}
\frac{\C\ts\exnbind\ra\VE }
     {\C\ts\exceptiondec\ra\EXISTS{\emptyset}{\VE\ \In\ \Env}}
\end{equation}

\begin{equation}	% local declaration
%\label{localdec-rule}
\frac{\begin{array}{lr}
      \C\ts\dec_1\ra\EXISTS{\T_1}{\E_1} &
      \T_1 \cap \TyNamesFcn \C = \emptyset \\
      \C+\E_1\ts\dec_2\ra\EXISTS{\T_2}{\E_2} &
      \T_2 \cap \T_1  = \emptyset
      \end{array}}
     {\C\ts\localdec\ra\EXISTS{\T_1\cup\T_2}{\E_2}}
     \index{28.3}
\end{equation}

\begin{equation}                % open declaration
%\label{open-dec-rule}
\frac{\begin{array}{c}
       \C\ts\longstrid_1\ra\RS_1  \quad \S_1 = \of{\S}{\RS_1}\\
            \vdots \\
       \C\ts\longstrid_n\ra\RS_n \quad \S_n = \of{\S}{\RS_n}
      \end{array}}
     {\C\ts\opendec\ra\EXISTS{\emptyset}{ (\S_1 + \cdots + \S_n)\ \In\ \Env }}
\end{equation}

% \begin{equation}	% module declaration
% \label{moduledec-rule}
% \frac{\C\ts\modbind\ra\EXISTS{\T}{\ME} }
%      {\C\ts\moduledec\ra\EXISTS{\T}{\ME\ \In\ \Env}}
% \end{equation}

\begin{equation}	% structure declaration
\label{structuredec-rule}
\frac{ \C\ts\strbind\ra\EXISTS{\T}{\SE}}
     {\C\ts\structuredec\ra\EXISTS{\T}{\SE\ \In\ \Env}}
\end{equation}

\begin{equation}	% functor declaration
\label{functordec-rule}
\frac{\C\ts\funbind\ra\EXISTS{\T}{\FE}}
     {\C\ts\functordec\ra\EXISTS{\T}{\FE\ \In\ \Env}}
\end{equation}

\begin{equation}	% signature declaration
\label{signaturedec-rule}
\frac{\C\ts\sigbind\ra\GE }
     {\C\ts\signaturedec\ra\EXISTS{\emptyset}{\GE\ \In\ \Env}}
\end{equation}

\begin{equation}	% empty declaration
%\label{emptydec-rule}
\frac{}
     {\C\ts\emptydec\ra\EXISTS{\emptyset}{\emptymap\ \In\ \Env}}
\end{equation}

\begin{equation}	% sequential declaration
%\label{seqdec-rule}
\frac{\begin{array}{lr}
      \C\ts\dec_1\ra\EXISTS{\T_1}{\E_1} &
      \T_1 \cap \TyNamesFcn \C = \emptyset \\
      \C+\E_1\ts\dec_2\ra\EXISTS{\T_2}{\E_2} &
      \T_2 \cap (\T_1 \cup \TyNamesFcn \E_1) = \emptyset
      \end{array}}
     {\C\ts\seqdec\ra\EXISTS{\T_1\cup\T_2}{\plusmap{E_1}{E_2}}}
\end{equation}

% (cvr
% \comments
% \begin{description}
% \item{(\ref{valdec-rule})}
% Here $\VE$ will contain types rather than general
% type schemes. The closure of $\VE$ is exactly what allows variables to
% be used polymorphically, via 
% % rule~\ref{varexp-rule}. % (cvr)
% rule~\ref{vidpath-rule}. % (cvr)

% Moreover, $\IE$ is the set of explicit type variables scoped at this particular
% occurrence of $\valdec$, cf. Section~\ref{scope-sec}, 
% page~\pageref{scope-def-lab}. The side-condition on $\IE$
% ensures that these explicit type variables are bound by the closure operation.
% On the other hand, no {\sl other} explicit type variable occurring
% free in $\VE$ will become bound, since it must be in $\of{\IE}{\C}$, and
% is therefore excluded from closure by the definition of the closure operation
% (Section~\ref{closure-sec}, page~\pageref{clos-def-lab})
% since $\of{\IE}{\C}\subseteq\TyVarFcn\C$.
% \item{(\ref{datatypedec-rule}),(\ref{abstypedec-rule})}
% The side conditions
% express that the elaboration of each datatype binding
% generates new type names and that as many of these new names
% as possible admit equality.  Adding $\TE$ to the context on the left
% of the $\ts$ captures the recursive nature of the binding.
% %The side condition is
% %the formal way of expressing that the elaboration of each datatype binding
% %generates new type names.  Adding $\TE$ to the context on the left
% %of the $\ts$ captures the recursive nature of the binding. Recall that $\TE$
% %is assumed well-formed (as defined in Section~\ref{typeenv-wf-sec}). If
% %$\TyNamesFcn(\of{\E}{\C})\subseteq\of{\T}{\C}$ and the side condition is
% %satisfied then $\C\oplus\TE$ is well-formed.
% \item{(\ref{datatyperepdec-rule})}
% (18) Note that no new type name is generated (i.e., datatype replication is not generative). By the syntactic restriction in 
% Section~\ref{core-syntactic-restrictions} 
%  the two type variable sequences in the conclusion must be equal.
% % (cvr
% \item{(\ref{abstypedec-rule})}
% The $\Abs$ operation was defined in Section~\ref{typeenv-wf-sec}, page~\pageref{abs-lab}.
% % cvr)
% % (cvr
% % \item{(\ref{exceptiondec-rule})}
% % No closure operation is used here, since $\EE$ maps exception 
% % names to types rather than  to general type schemes.
% % Note that $\EE$ is also recorded in the {\VarEnv} component of
% % the resulting environment (see Section~\ref{stat-proj}, page~\pageref{stat-proj}).\index{29.0}
% \item{(\ref{exceptiondec-rule})}
% No closure operation is used here, since $\VE$ maps exception 
% names to types rather than  to general type schemes.
% % cvr)
% \end{description}
% cvr)
\comments
\begin{description}
\item{(\ref{valdec-rule})}
Here $\VE$ will contain types rather than general
type schemes. The closure of $\VE$  allows value identifiers to
be used polymorphically, via 
rule~\ref{longvidexp-rule}. 

The side-condition on $\{\alpha_1,\cdots,\alpha_k\}$
ensures that the type variables bound to \tyidseq\
are bound by the closure operation, if they occur in the range of \VE.

On the other hand, if the phrase \valdec\ occurs inside some larger
value binding $\VAL\ \tyidseq_0\ \valbind_0$
then no type variable $\alpha$ bound to a type identifier
listed in $\tyidseq_0$ will become bound by the 
$\cl{\C,\valbind}(\VE)$ operation; for 
$\alpha$ must be in $\of{\IE}{\C}$ and 
hence excluded from closure by the definition of the closure operation 
(Section~\ref{closure-sec}, page~\pageref{clos-def-lab})
since $\TyVarsFcn(\of{\IE}{\C})\subseteq\TyVarsFcn\C$.

\item{(\ref{datatypedec-rule}),(\ref{abstypedec-rule})}
The side conditions
express that the elaboration of each datatype binding
generates new type names and that as many of these new names
as possible admit equality.  Adding $\TE$ to the context on the left
of the $\ts$ captures the recursive nature of the binding.

\item{(\ref{datatyperepdec-rule})}
Note that no new type name is generated (i.e., datatype replication is not generative). 
\item{(\ref{abstypedec-rule})}
The $\Abs$ operation was defined in Section~\ref{typeenv-wf-sec}, page~\pageref{abs-lab}.
\item{(\ref{exceptiondec-rule})}
No closure operation is used here, as this would make the type system unsound.
Example: {\tt exception E of 'a; val it = (raise E 5) handle E f => f(2)}~.
%No closure operation is used here, since $\VE$ maps exception 
%names to types rather than  to general type schemes.
\end{description}
% cvr)

%                        Bindings
%
\rulesec{Value Bindings}{\C\ts\valbind\ra\VE}
%\vspace{6pt}
\begin{equation}	% value binding
\label{valbind-rule}
\frac{\C\ts\pat\ra(\VE,\tau)\qquad\C\ts\exp\ra\tau\qquad
      \langle\C\ts\valbind\ra\VE'\rangle }
     {\C\ts\longvalbind\ra\VE\ \langle +\ \VE'\rangle}\index{29.1}
\end{equation}

\begin{equation}	% recursive value binding
\label{recvalbind-rule}
\frac{\C+\VE\ts\valbind\ra\VE}
     {\C\ts\recvalbind\ra\VE}
\end{equation}
\comments
\begin{description}
\item{(\ref{valbind-rule})}
When the option is present we have $\Dom\VE\cap
\Dom\VE' = \emptyset$ by the syntactic restrictions.\index{29.2}
\item{(\ref{recvalbind-rule})}
Modifying $\C$ by $\VE$ on the left captures the 
recursive nature of the binding. From rule~\ref{valbind-rule} we see that any
type scheme occurring in $\VE$ will have to be a type. Thus each use of a
recursive function in its own body must be ascribed the same type.
% (cvr
Also note that C + VE may overwrite identifier status. For example, the program \verb+datatype t = f; val rec f = fn x => x;+ is legal.
% cvr)
\end{description}

\rulesec{Type Bindings}{\C\ts\typbind\ra\TE}
%\fbox{$\C\ts\typbind\ra\TE$}
\begin{equation}	% type binding
%\label{typbind-rule}
\frac{\begin{array}{lcr}
       \C\ts\tyidseq\ra(\alphak,{\IE}) &
       \C+\IE\ts\ty\ra\tau &
      \langle\C\ts\typbind\ra\TE\rangle
      \end{array}}
     {\begin{array}{c}
      \C\ts\longtypbind\ra\\
      \qquad\qquad\qquad
% (cvr
%      \{\tycon\mapsto(\typefcnk,\emptymap)\}\ \langle +\ \TE\rangle 
      \{\tycon\mapsto(\typetypefnc{\alphak}{\tau},\emptymap)\}\ 
             \langle +\ \TE\rangle 
% cvr)
      \end{array}
     }\index{29.3}
\end{equation}
\comment The syntactic restrictions ensure that the type function
% $\typefcnk$ satisfies the well-formedness constraints of  % (cvr)
$\typetypefnc{\alphak}{\tau}$ satisfies the well-formedness constraints of  % (cvr)
Section~\ref{tyfun-sec} and they ensure $tycon\notin\Dom\TE$.

\rulesec{Data Type Bindings}{\C\ts\datbind\ra\VE,\TE}
%\fbox{$\C\ts\datbind\ra\VE,\TE$}
% \begin{equation}	% datatype binding
% %\label{datbind-rule}
% \frac{\begin{array}{c}
%         \tyvarseq=\alphak\qquad\C,\alphakt\ts\constrs\ra\CE\\
%         \langle\C\ts\datbind\ra\VE,\TE\qquad
%         \forall(\t',\CE)\in\Ran\TE, \t\neq\t'\rangle
%       \end{array}
%      }
%      {\begin{array}{c}
%         \C\ts\longdatbind\ra\\
%         \qquad\qquad\qquad\cl{\C}{\CE}\langle +\ \VE\rangle,\
%         \{\tycon\mapsto(\t,\cl{\C}{\CE})\}\ \langle +\ \TE\rangle
%       \end{array}
%      }\index{30.1}
% \end{equation}
% \comment The syntactic restrictions ensure $\Dom\VE\cap\Dom\CE = \emptyset$
% and $\tycon\notin\Dom\TE$.

\begin{equation}	% datatype binding
%\label{datbind-rule}
\frac{\begin{array}{c}
       \C\ts\tyidseq\ra(\alphak,{\IE}) \\
       \C+\IE,\apptype{\alphak}{\t}\ts\constrs\ra\VE\\
        \langle\C\ts\datbind\ra\VE',\TE'\qquad
        \forall(\t',\VE'')\in\Ran\TE, \t\neq\t'\rangle
      \end{array}
     }
     {\begin{array}{c}
        \C\ts\longdatbind\ra\\
        \qquad\qquad\qquad\cl{\C}{\VE}\langle +\ \VE'\rangle,\
        \{\tycon\mapsto(\t,\cl{\C}{\VE})\}\ \langle +\ \TE'\rangle
      \end{array}
     }\index{30.1}
\end{equation}
\comment The syntactic restrictions ensure $\Dom\VE\cap\Dom\VE' = \emptyset$
and $\tycon\notin\Dom\TE'$.
% cvr)

% (cvr
%\rulesec{Constructor Bindings}{\C,\tau\ts\constrs\ra\CE}
%\fbox{$\C,\tau\ts\constrs\ra\CE$}
% \begin{equation}	% data constructors
% %\label{constrs-rule}
% \frac{\langle\C\ts\ty\ra\tau'\rangle\qquad
%       \langle\langle\C,\tau\ts\constrs\ra\CE\rangle\rangle }
%      {\begin{array}{c}
%       \C,\tau\ts\longerconstrs\ra\\
%       \qquad\qquad\qquad\{\con\mapsto\tau\}\
%      \langle +\ \{\con\mapsto\tau'\to\tau\}\ \rangle\
%       \langle\langle +\ \CE\rangle\rangle
%       \end{array}
%      }\index{30.2}
% \end{equation}
% \comment By the syntactic restrictions $\con\notin\Dom\CE$.

\rulesec{Constructor Bindings}{\C,\tau\ts\constrs\ra\VE}
 \begin{equation}	% data constructors
 %\label{constrs-rule}
 \frac{\langle\C\ts\ty\ra\tau'\rangle\qquad
       \langle\langle\C,\tau\ts\constrs\ra\VE\rangle\rangle }
      {\begin{array}{c}
       \C,\tau\ts\longerconstrs\ra\\
       \qquad\qquad\qquad\{\vid\mapsto(\tau,\cstatus)\}\
      \langle +\ \{\vid\mapsto(\tau'\to\tau,\cstatus)\}\ \rangle\
       \langle\langle +\ \VE\rangle\rangle
       \end{array}
      }\index{30.2}
 \end{equation}
 \comment By the syntactic restrictions $\vid\notin\Dom\VE$.
% cvr)

% (cvr
% \rulesec{Exception Bindings}{\C\ts\exnbind\ra\EE}
% %poly with polymorphic exceptions:
% \begin{equation}	% exception binding
% \label{exnbind1-rule}
% \frac{\langle\C\ts\ty\ra\tau\quad\mbox{$\tau$ is imperative}\rangle\qquad
%       \langle\langle\C\ts\exnbind\ra\EE\rangle\rangle }
%      {\begin{array}{c}
%       \C\ts\longexnbinda\ra\\
%       \qquad\qquad\qquad\{\exn\mapsto\EXCN\}\
%       \langle +\ \{\exn\mapsto\tau\rightarrow\EXCN\}\ \rangle\
%       \langle\langle +\ \EE\rangle\rangle
%       \end{array}
%      }\index{30.3}
% \end{equation}
\rulesec{Exception Bindings}{\C\ts\exnbind\ra\VE}
%poly with polymorphic exceptions:
\begin{equation}	% exception binding
\label{exnbind1-rule}
\frac{\langle\C\ts\ty\ra\tau\rangle\qquad
      \langle\langle\C\ts\exnbind\ra\VE\rangle\rangle }
     {\begin{array}{c}
      \C\ts\longexnbinda\ra\\
      \qquad\qquad\qquad\{\vid\mapsto(\EXCN,\estatus\}\
      \langle +\ \{\vid\mapsto(\tau\rightarrow\EXCN,\estatus)\}\ \rangle\
      \langle\langle +\ \VE\rangle\rangle
      \end{array}
     }\index{30.3}
\end{equation}
% cvr)

%with mono typed exceptions:
%\begin{equation}	% exception binding
%\label{exnbind1-rule}
%\frac{\langle\C\ts\ty\ra\tau\quad\TyVarFcn(\tau)=\emptyset\rangle\qquad
%      \langle\langle\C\ts\exnbind\ra\EE\rangle\rangle }
%     {\begin{array}{c}
%      \C\ts\longexnbinda\ra\\
%      \qquad\qquad\qquad\{\exn\mapsto\EXCN\}\
%      \langle +\ \{\exn\mapsto\tau\rightarrow\EXCN\}\ \rangle\
%      \langle\langle +\ \EE\rangle\rangle
%      \end{array}
%     }
%\end{equation}

\vspace*{4mm}
\begin{equation}	% exception binding
\label{exnbind2-rule}
\frac{\C\ts\longvid\ra(\tau,\estatus)\qquad 
      %\C\ts\vidpath\ra(\tau,\estatus)\qquad
      \langle\C\ts\exnbind\ra\VE\rangle }
      {\C\ts\longexnbindb\ra\{\vid\mapsto(\tau,\estatus)\}\ \langle +\ \VE\rangle}
%     {\begin{array}{c}
%      \C\ts\longexnbindb\ra\\
%      \qquad\qquad\qquad\{\exn\mapsto\tau\}\
%      \langle +\ \EE\rangle
%      \end{array}
%     }
\end{equation}
\comments
\begin{description}
\item{(\ref{exnbind1-rule})}
% (cvr
%  Notice that $\tau$ must not contain
% any applicative type variables.\index{30.35}
Notice that $\tau$ may contain type variables.
% cvr)
%with monotyped exceptions:
%\item{(\ref{exnbind1-rule})} Notice that $\tau$ must be a monotype
%(see also restriction~\ref{monotypes-res} in 
%Section~\ref{further-restrictions-sec}).
\item{(\ref{exnbind1-rule}),(\ref{exnbind2-rule})}
% (cvr
% There is a unique $\EE$, for each $\C$ and $\exnbind$,
% %No matter which of the options are present, given $\C$ and $\exnbind$ there
% %is at most one $\EE$ 
% such that $\C\ts\exnbind\ra\EE$.
% cvr)
For each $\C$ and $\exnbind$, there is at most one $\VE$ satisfying 
$\C\ts\exnbind\ra\VE$.
\end{description}

%\caption{Rules for Bindings}
%\end{figure}

%                        Atomic Patterns
%
\rulesec{Atomic Patterns}{\C\ts\atpat\ra(\VE,\tau)}
%\vspace{6pt}
%\fbox{$\C\ts\atpat\ra(\VE,\tau)$}
\begin{equation}	% wildcard pattern
%\label{wildcard-rule}
\frac{}
     {\C\ts\wildpat\ra (\emptymap,\tau)}\index{30.4}
\end{equation}

\begin{equation}	% special constant in pattern
\frac{}
     {\C\ts\scon\ra (\emptymap,\scontype(\scon))}\index{30.5}
\end{equation}

% (cvr
% \begin{equation}	% variable pattern
% \label{varpat-rule}
% \frac{}
%      {\C\ts\var\ra (\{\var\mapsto\tau\},\tau) }
% \end{equation}
\begin{equation}	% variable pattern
\label{varpat-rule}
\frac{\vid\not\in\Dom(\C)\ {\rm or}\ \of{\is}{\C(\vid)}=\vstatus}
     {\C\ts\vid\ra (\{\vid\mapsto(\tau,\vstatus\},\tau) }
\end{equation}
% cvr)


% (cvr
% \begin{equation}	% constant pattern
% %\label{constpat-rule}
% \frac{\C(\longcon)\succ\tauk\t }
%      {\C\ts\longcon\ra (\emptymap,\tauk\t)}
% \end{equation}

% \begin{equation}       % exception constant
% %\label{exconapat-rule}
% \frac{\C(\longexn)=\EXCN}
%      {\C\ts\longexn\ra (\emptymap,\EXCN)}
% \end{equation}

\begin{equation}	% constant pattern
 \label{constpat-rule}
 \frac{\begin{array}{lcr}
      \C\ts\longvid\ra(\tych,\is) &
      \is \neq \vstatus & 
      \tych \succ \apptype{\tauk}{\typeapp} 
      \end{array}}
     {\C\ts\longvid\ra (\emptymap,\apptype{\tauk}{\typeapp})}
 \end{equation}
% cvr)
\begin{equation}	% record pattern
%\label{recpat-rule}
\frac{\langle\C\ts\labpats\ra(\VE,\varrho)\rangle}
     {\C\ts\lttbrace\ \recpat\ \rttbrace\ra(\ \emptymap\langle +\ \VE\rangle,\ \emptymap
      \langle +\ \varrho\rangle\ \In\ \Type\ ) }\index{31.1}
\end{equation}

\begin{equation}	% parenthesised pattern
%\label{parpat-rule}
\frac{\C\ts\pat\ra(\VE,\tau)}
     {\C\ts\parpat\ra(\VE,\tau)}
\end{equation}
\comments
\begin{description}
% \item{(\ref{varpat-rule})} 
% Note that $\var$ can assume a type, not a general type scheme.
\item{(\ref{varpat-rule},\ref{constpat-rule})}
The context $\C$ determines which of these two rules applies. 
In rule~\ref{varpat-rule}, note
that $\vid$ can assume a type, not a general type scheme.
\end{description}

\rulesec{Pattern Rows}{\C\ts\labpats\ra(\VE,\varrho)}
%\fbox{$\C\ts\labpats\ra(\VE,\varrho)$}
\begin{equation}	% wildcard record
%\label{wildrec-rule}
\frac{}
     {\C\ts\wildrec\ra(\emptymap,\varrho)}\index{31.2}
\end{equation}

\begin{equation}	% record component
\label{longlab-rule}
\frac{\begin{array}{c}
      \C\ts\pat\ra(\VE,\tau)\qquad \\
      \langle\C\ts\labpats\ra(\VE',\varrho)\qquad
%     \Dom\VE \cap \Dom \VE' = \emptyset \qquad % (cvr)
      \lab\notin\Dom\varrho\rangle
      \end{array}
}
     {\C\ts\longlabpats\ra
     (\VE\langle +\ \VE'\rangle,\
      \{\lab\mapsto\tau\}\langle +\ \varrho\rangle) }
\end{equation}
% (cvr
% \comment 
% \begin{description}
% \item{(\ref{longlab-rule})} 
%  By the syntactic restrictions, $\Dom\VE\cap\Dom\VE' = \emptyset$.
% \end{description}
% cvr)
%                        Patterns
%
%\begin{figure}[h]
%\label{pat-rules}
\rulesec{Patterns}{\C\ts\pat\ra(\VE,\tau)}
\begin{equation}	% atomic pattern
%\label{atpat-rule}
\frac{\C\ts\atpat\ra (\VE,\tau)}
     {\C\ts\atpat\ra (\VE,\tau)}\index{31.3}
\end{equation}

% (cvr
% \begin{equation}	% construction pattern
% %\label{conpat-rule}
% \frac{\C(\longcon)\succ\tau'\to\tau\qquad\C\ts\atpat\ra(\VE,\tau')}
%      {\C\ts\conpat\ra (\VE,\tau)}
% \end{equation}

% \begin{equation}       %  exception construction pattern
% %\label{exconpat-rule}
% \frac{\C(\longexn)=\tau\rightarrow\EXCN\qquad
%       \C\ts\atpat\ra(\VE,\tau)}
%      {\C\ts\exconpat\ra(\VE,\EXCN)}
% \end{equation}


\begin{equation}	% construction pattern
\label{conpat-rule}
\frac{\begin{array}{lccr}
      \C\ts\longvid\ra(\tych,\is) &
      \is \neq \vstatus &
      \tych \succ \tau'\to\tau & 
      \C\ts\atpat\ra(\VE,\tau')      
      \end{array}}
     {\C\ts\conpat\ra (\VE,\tau)}
\end{equation}
% cvr)
\begin{equation}	% typed pattern
%\label{typedpat-rule}
\frac{\C\ts\pat\ra(\VE,\tau)\qquad\C\ts\ty\ra\tau}
     {\C\ts\typedpat\ra (\VE,\tau)}
\end{equation}


% \begin{equation}	% layered pattern
% \label{layeredpat-rule}
% \frac{\begin{array}{c}
%       \C\ts\var\ra(\VE,\tau)\qquad\langle\C\ts\ty\ra\tau\rangle\\
%       \C\ts\pat\ra(\VE',\tau)
% %\qquad\VE\sim\VE'
%       \end{array}
%      }
%      {\C\ts\layeredpat\ra(\plusmap{\VE}{\VE'},\tau)}
% \end{equation}
\begin{equation}	% layered pattern
\label{layeredpat-rule}
\frac{\begin{array}{c}
      \vid\not\in\Dom(\C)\ {\rm or}\ \of{\is}{\C(\vid)}=\vstatus\\
      \langle\C\ts\ty\ra\tau\rangle \qquad
      \C\ts\pat\ra(\VE,\tau) \qquad
      \vid \not \in \Dom \VE
      \end{array}
     }
     {\C\ts\layeredpat\ra(\plusmap{\{\vid\mapsto(\tau,\vstatus)\}}{\VE},\tau)}
\end{equation}


\rulesec{Long Type Constructors}{\C\ts\longtycon\ra(\typefnc[\k],\VE)}

\begin{equation}	% idlongtycon
\label{idlongtycon-rule}
\frac{\tycon\in\Dom\C}
     {\C\ts\idlongid{\tycon}\ra\C(\tycon)}
\end{equation}

\begin{equation}	% dotlongtycon
%\label{dotlongtycon-rule}
\frac{\begin{array}{lcr}
      \C\ts\longstrid\ra\RS &
      \S = \of\S\RS&
      \tycon\in\Dom\S
      \end{array}
      }
     {\C\ts\dotlongid{\longstrid}{\tycon}\ra\S(\tycon)}
\end{equation}

\rulesec{Type Constructor Paths}{\C\ts\tyconpath\ra(\typefnc[\k],\VE)}

\begin{equation}	% longtyconpath
\label{longtyconpath-rule}
\frac{\C\ts\longtycon\ra(\typefnc,\VE)}
     {\C\ts\longtyconpath\ra(\typefnc,\VE)}
\end{equation}

\begin{equation}	% anontyconpath
\label{anontyconpath-rule}
\frac{\begin{array}{l}
      \C\ts^\expectstr\modexp\ra\exmod{\T}{RS} \\
      \C+\{\strid\mapsto\RS\}\ts\longtyconpath\ra(\typefnc,\VE)\\
      \T\cap(\TyNamesFcn(\C) \cup \TyNamesFcn((\typefnc,\VE))) = \emptyset 
      \end{array}
      }
     {\C\ts\anontyconpath\ra(\typefnc,\VE)}
\end{equation}


%                        Type Identifier Sequences
\rulesec{Type Identifier Sequences}{\C\ts\tyidseq\ra(\alphak,\IE)}
\begin{equation}	% singleton
\label{tyidtyidseq-rule}
\frac{\begin{array}{lr}
       \mbox{$\alpha$ admits equality iff $\tyid \in \ETyId$} &
        \alpha \not\in(\TyVarsFcn\C) 
      \end{array}}
     {\C\ts\tyid\ra((\alpha),\{\tyid\mapsto(\alpha)\})}
\end{equation}

\begin{equation}	% tyidktyidseq
\label{emptytyidseq-rule}
\frac{ }
     {\C\ts\qquad\ra((),\emptymap)}
\end{equation}

\begin{equation}	% tyidktyidseq
\label{tyidktyidseq-rule}
\frac{\begin{array}{c}
      \mbox{$\alpha_i$ admits equality iff $\tyid_i \in \ETyId, i = 1..k$} \\
      \alpha_i \not\in(\TyVarsFcn\C) \cup \{\alpha_1, \ldots, \alpha_{(i-1)}\},
             i = 1..k
      \end{array}
     }
     {\C\ts\ml{(}\tyid_1\ml{,}\cdots\ml{,}\tyid_k\ml{)}\ra((\alpha_1,\cdots, \alpha_k),                                 \{\tyid_1\mapsto\alpha_1\} +
                                   \cdots +
                                   \{\tyid_k\mapsto\alpha_k\})}
\end{equation}


% (cvr
% \comments
% \begin{description}
% \item{(\ref{layeredpat-rule})}
% By the syntactic restrictions, $\Dom\VE\cap\Dom\VE' = \emptyset$.
% \end{description}
% cvr)


%                        Type Expressions
\rulesec{Type Expressions}{\C\ts\ty\ra\tau}
\begin{equation}	% atype variable
%\label{tyid-rule}
\frac{\tyid\in\Dom\ \C}
     {\C\ts\tyid\ra\C(\tyid)}\index{32.1}
\end{equation}

\begin{equation}	% record type
%\label{rectype-rule}
\frac{\langle\C\ts\labtys\ra\varrho\rangle}
     {\C\ts\lttbrace\ \rectype\ \rttbrace\ra\emptymap\langle +\ \varrho\rangle\ \In\ \Type}
\end{equation}

% (cvr
% \begin{equation}	% constructed type
% \label{constype-rule}
% \frac{\begin{array}{c}
%       \tyseq=\ty_1\cdots\ty_k\qquad\C\ts\ty_i\ra\tau_i\ (1\leq i\leq k)\\
%       \C(\longtycon)=(\theta,\CE)
%       \end{array}
%      }
%      {\C\ts\constype\ra\tauk\theta}
% \end{equation}

\begin{equation}	% constructed type
\label{constype-rule}
\frac{\begin{array}{c}
      \tyseq=\ty_1\cdots\ty_k\qquad\C\ts\ty_i\ra\tau_i\ (1\leq i\leq k)\\
      \C\ts\tyconpath\ra(\typefnc[\k],\VE)
      \end{array}
     }
     {\C\ts\constype\ra\apptype{\tauk}{\typefnc[\k]}}
\end{equation}

% cvr)
\begin{equation}	% function type
%\label{funtype-rule}
\frac{\C\ts\ty\ra\tau\qquad\C\ts\ty'\ra\tau'}
     {\C\ts\funtype\ra\tau\to\tau'}
\end{equation}

\begin{equation}	% package type
\label{packtype-rule}
\frac{\C\ts\sigexp\ra\sig{\T}{\M}}
     {\C\ts\packtype\ra\packagetype{\exmod{\T}{\M}}}
\end{equation}

\begin{equation}	% parenthesised type
%\label{packtype-rule}
\frac{\C\ts\ty\ra\tau}
     {\C\ts\partype\ra\tau}
\end{equation}



\comments
\begin{tabbing}
(\ref{constype-rule}) \= Recall that for
\apptype{\tauk}{\typefnc}\ to be defined, $\typefnc$
must have kind $k$.
\end{tabbing}

\rulesec{Type-expression Rows}{\C\ts\labtys\ra\varrho}
%\fbox{$\C\ts\labtys\ra\varrho$}
\begin{equation}	% record type components
%\label{longlabtys-rule}
\frac{\C\ts\ty\ra\tau\qquad\langle\C\ts\labtys\ra\varrho\rangle}
     {\C\ts\longlabtys\ra\{\lab\mapsto\tau\}\langle +\ \varrho\rangle}\index{32.15}
\end{equation}
\comment The syntactic constraints ensure $\lab\notin\Dom\varrho$.
%\caption{Rules for Types}
%\end{figure}

% \subsection{Further Restrictions}
% \label{further-restrictions-sec}
% There\index{32.2} are a few restrictions on programs which should be enforced by a
% compiler, but are better expressed apart from the preceding
% Inference Rules.  They are:
% \begin{enumerate}
% %poly
% %The following restriction has been removed from Version 1 because
% %of polymorphic references and exceptions
% %\item \label{monotypes-res}
% %The reference value constructor ~{\tt ref}~ may occur in patterns
% %with polymorphic type, but in an expression it must always elaborate to
% %a monotype, i.e. a type containing no type variables.  
% %Moreover, exception constructors can have monotypes only.
% %These restrictions
% %will be relaxed in future Versions, but some restrictions will always be
% %necessary to ensure soundness of the type discipline.
% \item For each occurrence of a record pattern containing a record wildcard,
% i.e. of the form
% %\begin{quote}
% \verb+{+${\it lab}_1$\ml{=}$\pat_1$\ml{,}$\cdots$\ml{,}${\it lab}_m$\ml{=}$\pat_m$\ml{,}\verb+...}+
% %\end{quote}
% the program context must determine uniquely the domain
% $\{{\it lab}_1,\cdots,{\it lab}_n\}$
% of its record type, where $m\leq n$; thus, the context must
% determine the labels \linebreak $\{{\it lab}_{m+1},\cdots,{\it lab}_n\}$ of the fields
% to be matched by the wildcard. For this purpose, an explicit type
% constraint may be needed. 

% % This restriction is necessary to ensure the existence of principal type schemes. % (cvr)

% \item In a match of the form ${\it pat}_1$ \ml{=>} $\exp_1$ \ml{|}$\;\cdots\;$
% \ml{|} ${\tt pat}_n$ \ml{=>} $\exp_n$ 
% the pattern sequence $\pat_1,\ldots,\pat_n$ should be {\sl irredundant};
% that is, each $\pat_j$ must match some value
% (of the right type) which is not matched by $\pat_i$ for any $i<j$.
% In the context {\fnexp}, the $\match$ must also be {\sl exhaustive}; that is,
% every value (of the right type) must be matched by some $\pat_i$.
% The compiler must give warning on violation of these restrictions, 
% but should still compile the match. 
% The restrictions are inherited by derived forms; in particular,
% this means that in the
% % (cvr
% % function binding\index{33.1}
% %  $\var\ \atpat_1\ \cdots\ \atpat_n\langle : \ty\rangle$\ \ml{=}\ $\exp$
%  function-value binding\index{33.1}
%   $\vid\ \atpat_1\ \cdots\ \atpat_n\langle : \ty\rangle$\ \ml{=}\ $\exp$
% % cvr)
% (consisting of one clause only), each separate $\atpat_i$ should be
% exhaustive by itself.
% %must be {\sl irredundant} and {\sl exhaustive}.  That is, each ${\it pat}_j$
% %must match {\sl some} value (of the right type) which is not matched by
% %${\it pat}_i$ for any $i <j$, and {\sl every} value (of the right type) must be
% %matched by some ${\it pat}_i$. The compiler must give a warning on violation
% %of this restriction, but should still compile the match.
% \end{enumerate}

\subsection{Further Restrictions}
\label{further-restrictions-sec}
There\index{32.2} are a few restrictions on programs which should be enforced by a
compiler, but are better expressed apart from the preceding
Inference Rules.  They are:
\begin{enumerate}
\item For each occurrence of a record pattern containing a record wildcard,
i.e. of the form
%\begin{quote}
\verb+{+${\it lab}_1$\ml{=}$\pat_1$\ml{,}$\cdots$\ml{,}${\it lab}_m$\ml{=}$\pat_m$\ml{,}\verb+...}+
%\end{quote}
the program context must determine uniquely the domain
$\{{\it lab}_1,\cdots,{\it lab}_n\}$
of its row type, where $m\leq n$; thus, the context must
determine the labels $\{{\it lab}_{m+1},\cdots,{\it lab}_n\}$ of the fields
to be matched by the wildcard. For this purpose, an explicit type
constraint may be needed.

\item In a match of the form 
${\it pat}_1$ \ml{=>} $\exp_1$\ml{|}$\;\cdots\;$\ml{|} ${\tt pat}_n$ \ml{=>} $\exp_n$ 
the pattern sequence $\pat_1,\ldots,\pat_n$ should be {\sl
irredundant}; that is, each $\pat_j$ must match some value (of the
right type) which is not matched by $\pat_i$ for any $i<j$.  In the
context {\fnexp}, the $\match$ must also be {\sl exhaustive}; that is,
every value (of the right type) must be matched by some $\pat_i$.  The
compiler must give warning on violation of these restrictions, but
should still compile the match.  The restrictions are inherited by
derived forms; in particular, this means that in the function-value
binding\index{33.1} {$\vid\ \atpat_1\ \cdots\ \atpat_n\langle :
\ty\rangle$\ \ml{=}\ $\exp$} (consisting of one clause only), each
separate $\atpat_i$ should be exhaustive by itself.

\item   For each value binding   $\pat\ \mbox{\ml{=}}\ \exp$
        the compiler must issue a report (but still compile) if $\pat$
        is not exhaustive.  This will detect a mistaken declaration
        like $\VAL\ \ml{nil}\ \mbox{\ml{=}}\ \exp$ in which the user
        expects to declare a new variable \ml{nil} (whereas the
        language dictates that \ml{nil} is here a constant pattern, so
        no variable gets declared).  However, this warning should not
        be given when the binding is a component of a top-level
        declaration $\valdec$; e.g.  $\VAL\ \mbox{\ml{x::l = }}\exp_1\
        \mbox{\ml{\AND\ y = }}\exp_2$ is not faulted by the compiler
        at top level, but may of course generate a \ml{Bind} exception
        (see Section~\ref{bas-exc}).
\end{enumerate}

% (cvr
% \subsection{Principal Environments}
% \label{principal-env-sec}
% The\index{33.15} notion of {\sl enrichment}, $\E\succ\E'$, between environments
% $\E=(\SE,\TE,\VE,\EE)$ and $\E'=(\SE',\TE',\VE',\EE')$ is defined
% in Section~\ref{enrichment-sec}. For the present section,  $\E\succ\E'$
% may be taken to mean $\SE=\SE'=\emptymap$, $\TE=\TE'$,
% $\EE=\EE'$, $\Dom\VE=\Dom\VE'$ and, for each $\id\in\Dom\VE$,
% $\VE(\id)\succ\VE'(\id)$.

% Let\index{33.2} $\C$ be a context, and suppose that $\C\ts\dec\ra\E$
% according to the preceding Inference Rules. Then $E$ is {\em principal}
% (for $\dec$ in the context $\C$) if, for all $\E'$ for
% which $\C\ts\dec\ra\E'$, we have $\E\succ\E'$. We claim that if
% $\dec$ elaborates to any environment in $\C$ then it elaborates to
% a principal environment in $\C$. Strictly, we must allow for the
% possibility that type names and imperative type variables
% which do not occur in $\C$ are chosen
% differently for $\E$ and $\E'$. 
% The stated claim is therefore made up to such variation.
% cvr)