Static semantics v0.1

doc/definition/static-semantics.tex

+\subsection*{Field lookup}
+
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \\
+          \fieldDecl{x}{\tau} \in \many{\mathit{ce}}
+        }
+        {\fieldLookup{\Phi}{\TApp{C}{\tau_0, \ldots, \tau_n}}{x}{\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\tau}}
+        }
+
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \quad x \notin \many{\mathit{ce}} \\
+         \fieldLookup{\Phi}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{x}{\tau}
+        }
+        {\fieldLookup{\Phi}{\TApp{C}{\tau_0, \ldots, \tau_n}}{x}{\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\tau}}
+        }
+
+
+\subsection*{Method lookup}
+
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \\
+          \methodDecl{m}{\tau}{\sigma} \in \many{\mathit{ce}}
+        }
+        {\methodLookup{\Phi}
+          {\TApp{C}{\tau_0, \ldots, \tau_n}}{m}
+          {\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\tau}}
+          {\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\sigma}}
+        }
+
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \quad m \notin \many{\mathit{ce}} \\
+         \methodLookup{\Phi}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{m}{\tau}{\sigma}
+        }
+        {\methodLookup{\Phi}{\TApp{C}{\tau_0, \ldots, \tau_n}}{m}
+          {\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\tau}}
+          {\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\sigma}}
+        }
+
+\subsection*{Method and field absence}
+
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \quad x \notin \many{\mathit{ce}} \\
+         \fieldAbsent{\Phi}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{x}
+        }
+        {\fieldAbsent{\Phi}{\TApp{C}{\tau_0, \ldots, \tau_n}}{x}
+        }
+
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \quad m \notin \many{\mathit{ce}} \\
+         \methodAbsent{\Phi}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{m}{\tau}{\sigma}
+        }
+        {\methodAbsent{\Phi}{\TApp{C}{\tau_0, \ldots, \tau_n}}{m}
+        }
+
+\iftrans{
+
+\subsection*{Type translation}
+
+To translate covariant generics, we essentially want to treat all contravariant
+occurrences of type variables as $\Dynamic$.  The type translation
+$\down{\tau}$ implements this.  It is defined in terms of the dual operator
+$\up{\tau}$ which translates positive occurences of type variables as $\Dynamic$.
+
+\begin{eqnarray*}
+  \down{T} & = & T \\
+  \down{\Arrow[k]{\tau_0, \ldots, \tau_n}{\tau_r}} & = & 
+     \Arrow[k]{\up{\tau_0}, \ldots, \up{\tau_n}}{\down{\tau_r}} \\
+  \down{\TApp{C}{\tau_0, \ldots, \tau_n}} & = & \TApp{C}{\down{\tau_0}, \ldots, \down{\tau_n}} \\
+  \down{\tau} & = & \tau\ \mbox{otherwise}
+\end{eqnarray*}
+
+\begin{eqnarray*}
+  \up{T} & = & \Dynamic \\
+  \up{\Arrow[k]{\tau_0, \ldots, \tau_n}{\tau_r}} & = & 
+     \Arrow[k]{\down{\tau_0}, \ldots, \down{\tau_n}}{\up{\tau_r}} \\
+  \up{\TApp{C}{\tau_0, \ldots, \tau_n}} & = & \TApp{C}{\up{\tau_0}, \ldots, \up{\tau_n}} \\
+  \up{\tau} & = & \tau\ \mbox{if $\tau$ is base type.}
+\end{eqnarray*}
+
+
+}
 \subsection*{Expression typing: $\yieldsOk{\Phi, \Delta, \Gamma}{e}{\opt{\tau}}{e'}{\tau'}$} 
 \hrulefill\\
 
 
 \sstext{ Expression typing is a relation between typing contexts, a term ($e$),
   an optional type ($\opt{\tau}$), and a type ($\tau'$).  The general idea is
   that we are typechecking a term ($e$) and want to know if it is well-typed.
   The term appears in a context, which may (or may not) impose a type constraint
   on the term.  For example, in $\dvar{x:\tau}{e}$, $e$ appears in a context
   which requires it to be a subtype of $\tau$, or to be coercable to $\tau$.
@@ skipping 70 matching lines @@
 declared types.  
 }{
 
 A fully annotated function elaborates to a function with an elaborated body.
 The rest of the function elaboration rules fill in the reified type using
 contextual information if present and applicable, or $\Dynamic$ otherwise.
 
 }
 
 \infrule{\Gamma' = \extends{\Gamma}{\many{x}}{\many{\tau}} \quad\quad 
-         \yieldsOk{\Phi, \Delta, \Gamma'}{e}{\sigma}{e'}{\sigma'}
+         \stmtOk{\Phi, \Delta, \Gamma'}{s}{\sigma}{s'}{\Gamma'}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{\many{x:\tau}}{\sigma}{e}}
+                  {\elambda{\many{x:\tau}}{\sigma}{s}}
                   {\_}
-                  {\elambda{\many{x:\tau}}{\sigma}{e'}}
+                  {\elambda{\many{x:\tau}}{\sigma}{s'}}
                   {\Arrow[-]{\many{\tau}}{\sigma}}
         } 
 
 \sstext{A function with a missing argument type is well-typed if it is well-typed with
 the argument type replaced with $\Dynamic$.}
 {}
 
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\Dynamic, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{e}}
+                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\Dynamic, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{s}}
                   {\opt{\tau}}
                   {e_f}
                   {\tau_f}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\_, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{e}}
+                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\_, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{s}}
                   {\opt{\tau}}
                   {e_f}
                   {\tau_f}
         } 
 
 \sstext{A function with a missing argument type is well-typed if it is well-typed with
 the argument type replaced with the corresponding argument type from the context
 type.  Note that this rule overlaps with the previous: the formal presentation
 leaves this as a non-deterministic choice.}{}
 
 \infrule{\tau_c = \Arrow[k]{\upsilon_0, \ldots, \upsilon_n}{\upsilon_r} \\
          \yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\upsilon_i, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{e}}
+                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\upsilon_i, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{s}}
                   {\tau_c}
                   {e_f}
                   {\tau_f}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\_, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{e}}
+                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\_, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{s}}
                   {\tau_c}
                   {e_f}
                   {\tau_f}
         } 
 
 \sstext{A function with a missing return type is well-typed if it is well-typed with
 the return type replaced with $\Dynamic$.}{}
 
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{\many{x:\opt{\tau}}}{\Dynamic}{e}}
+                  {\elambda{\many{x:\opt{\tau}}}{\Dynamic}{s}}
                   {\opt{\tau_c}}
                   {e_f}
                   {\tau_f}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{\many{x:\opt{\tau}}}{\_}{e}}
+                  {\elambda{\many{x:\opt{\tau}}}{\_}{s}}
                   {\opt{\tau_c}}
                   {e_f}
                   {\tau_f}
         } 
 
 \sstext{A function with a missing return type is well-typed if it is well-typed with
 the return type replaced with the corresponding return type from the context
 type.  Note that this rule overlaps with the previous: the formal presentation
 leaves this as a non-deterministic choice.  }{}
 
 \infrule{\tau_c = \Arrow[k]{\upsilon_0, \ldots, \upsilon_n}{\upsilon_r} \\
          \yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{\many{x:\opt{\tau}}}{\upsilon_r}{e}}
+                  {\elambda{\many{x:\opt{\tau}}}{\upsilon_r}{s}}
                   {\tau_c}
                   {e_f}
                   {\tau_f}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{\many{x:\opt{\tau}}}{\_}{e}}
+                  {\elambda{\many{x:\opt{\tau}}}{\_}{s}}
                   {\tau_c}
                   {e_f}
                   {\tau_f}
         } 
 
 
 \sstext{Instance creation creates an instance of the appropriate type.}{}
 
 % FIXME(leafp): inference
 % FIXME(leafp): deal with bounds
@@ skipping 72 matching lines @@
                   {e_a'}
                   {\tau_a'} \quad \mbox{for}\ e_a \in \many{e_a}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\ecall{e}{\many{e_a}}}
                   {\_}
                   {\edcall{e'}{\many{e_a'}}}
                   {\Dynamic}
         } 
 
+\iftrans{
 \sstext{A dynamic call expression is well-typed so long as the applicand and the
 arguments are well-typed at any type.}{}
 
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}
                   {e}
                   {\Dynamic}
                   {e'}
                   {\tau} \\
          \yieldsOk{\Phi, \Delta, \Gamma}
                   {e_a}
                   {\_}
                   {e_a'}
                   {\tau_a} \quad \mbox{for}\ e_a \in \many{e_a}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\edcall{e}{\many{e_a}}}
                   {\_}
                   {\edcall{e'}{\many{e_a'}}}
                   {\Dynamic}
         }
 
+}
+
 \sstext{A method load is well-typed if the term is well-typed, and the method name is
 present in the type of the term.}{}
 
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}
                   {e}
                   {\_}
                   {e'}
                   {\sigma} \quad\quad
-         \methodLookup{\Phi}{\sigma}{m}{\tau}
+         \methodLookup{\Phi}{\sigma}{m}{\sigma}{\tau}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\eload{e}{m}}
                   {\_}
                   {\eload{e'}{m}}
                   {\tau}
         }
 
 \sstext{A method load from a term of type $\Dynamic$ is well-typed if the term is
 well-typed.}
@@ skipping 10 matching lines @@
                   {e'}
                   {\tau} 
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\eload{e}{m}}
                   {\_}
                   {\edload{e'}{m}}
                   {\Dynamic}
         }
 
+\iftrans{
 \sstext{A dynamic method load is well typed so long as the term is well-typed.}{}
 
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}
                   {e}
                   {\Dynamic}
                   {e'}
                   {\tau} 
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\edload{e}{m}}
                   {\_}
                   {\edload{e'}{m}}
                   {\Dynamic}
         }
 
+}
+
 \sstext{A field load from $\ethis$ is well-typed if the field name is present in the
 type of $\ethis$.}{}
 
 \infrule{\Gamma = \Gamma_\tau & \fieldLookup{\Phi}{\tau}{x}{\sigma}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\eload{\ethis}{x}}
                   {\_}
                   {\eload{\ethis}{x}}
                   {\sigma}
@@ skipping 46 matching lines @@
                   {\ethrow}
                   {\_}
                   {\ethrow}
                   {\sigma}
         } 
 
 \sstext{A cast expression is well-typed so long as the term being cast is well-typed.
 The synthesized type is the cast-to type.  We require that the cast-to type be a
 ground type.}{}
 
-\comment{TODO(leafp): specify ground types}
-
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\sigma} \quad\quad \mbox{$\tau$ is ground}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\eas{e}{\tau}}
                   {\_}
                   {\eas{e'}{\tau}}
                   {\tau}
         } 
 
 \sstext{An instance check expression is well-typed if the term being checked is
 well-typed. We require that the cast to-type be a ground type.}{}
 
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\sigma} \quad\quad \mbox{$\tau$ is ground}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\eis{e}{\tau}}
                   {\_}
                   {\eis{e'}{\tau}}
                   {\Bool}
         } 
 
+\iftrans{
+
 \sstext{A check expression is well-typed so long as the term being checked is
 well-typed.  The synthesized type is the target type of the check.}{}
 
 
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\sigma}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\echeck{e}{\tau}}
                   {\_}
                   {\echeck{e'}{\tau}}
                   {\tau}
         } 
 
+}
+
 \subsection*{Declaration typing: $\declOk[d]{\Phi, \Delta, \Gamma}{\mathit{vd}}{\mathit{vd'}}{\Gamma'}$}
 \hrulefill\\
 
 \sstext{
 Variable declaration typing checks the well-formedness of the components, and
 produces an output context $\Gamma'$ which contains the binding introduced by
 the declaration.
 
 A simple variable declaration with a declared type is well-typed if the
 initializer for the declaration is well-typed at the declared type.  The output
@@ skipping 102 matching lines @@
 \sstext{A sequence statement is well-typed if the first component is well-typed, and the
 second component is well-typed with the output context of the first component as
 its input context.  The final output context is the output context of the second
 component.}{}
 
 \infrule{\stmtOk{\Phi, \Delta, \Gamma}{s_1}{\tau_r}{s_1'}{\Gamma'} \quad\quad
          \stmtOk{\Phi, \Delta, \Gamma'}{s_2}{\tau_r}{s_2'}{\Gamma''}
         }
         {\stmtOk{\Phi, \Delta, \Gamma}{s_1;s_2}{\tau_r}{s_1';s_2'}{\Gamma''}
         }
+
+\subsection*{Class member typing:  $\declOk[ce]{\Phi, \Delta, \Gamma}{\mathit{vd} : \mathit{ce}}{\mathit{vd}'}{\Gamma'}$}
+\hrulefill\\
+
+\sstext{ 
+
+A class member is well-typed with a given signature ($\mathit{ce}$) taken from
+the class hierarchy if the signature type matches the type on the definition,
+and if the definition is well-typed.
+
+}
+{
+
+Elaborating class members is done with respect to a signature.  The field
+translation simply translates the field as a variable declaration.
+
+}
+
+
+\infrule{
+          \declOk[d]{\Phi, \Delta, \Gamma}
+                 {\dvar{x:\opt{\tau}}{e}}
+                 {\mathit{vd'}}
+                 {\Gamma'}
+        }
+        {
+          \declOk[ce]{\Phi, \Delta, \Gamma}
+                 {\dvar{x:\opt{\tau}}{e} : \fieldDecl{x}{\opt{\tau}}}
+                 {\mathit{vd'}}
+                 {\Gamma'}
+        }
+
+
+\iftrans{
+
+Translating methods requires introducing guard expressions.  The signature
+provides an internal and an external type for the method.  The external type is
+the original declared type of the method, and is the signature which the method
+presents to external clients.  Because we implement covariant generics, clients
+may see an instantiation of this signature which will allow them to violate the
+contract expected by the implementation.  To handle this, we rewrite the method
+to match an internal signature which is in fact soundly covariant in the type
+parameters (that is, all contravariant type parameters are replaced with
+$\Dynamic$, and hence all remaining type parameters occur in properly covariant
+positions).  This property is enforced in the override checking relation: from
+the perspective of this relation, there is simply another internal type which
+defines how to wrap the method with guards.
+
+The translation insists that the internal and external types be function types
+of the appropriate arity, and that the external type is equal to the type of the
+declaration.  The declaration is translated using the underlying function
+definition translation, but is then wrapped with guards to enforce the type
+contract, producing a valid function of the internal (covariant) type.  The
+original body of the function is wrapped in a lambda function, which is applied
+using a dynamic call which checks that the arguments (which may have negative
+occurrences of type variables which are treated as $\Dynamic$ in the internal
+type) are appropriate for the actual body.  The original function returns a type
+$\tau_r$ which may be a super-type of the internal type (since negative
+occurrences of type variables must be treated as dynamic), and so we insert a
+check expression to guard against runtime type mismatches here.
+
+This is a very simplistic translation for now.  We could choose, in the case
+that the body returns a lambda, to push the checking down into the lambda
+(essentially wrapping it in place).  
+
+}
+
+\infrule{ \mathit{vd} = \dfun{\tau_r}{f}{x_0:\tau_0, \ldots, x_n:\tau_n}{s} \\
+          \sigma_e = \Arrow[+]{\tau_0, \ldots, \tau_n}{\tau_r} 
+\iftrans{\quad\quad 
+                 \sigma_i = \Arrow{\upsilon_0, \ldots, \upsilon_n}{\upsilon_r}
+} \\
+          \declOk[d]{\Phi, \Delta, \Gamma}
+                 {\mathit{vd}}
+                 {\dfun{\tau_r}{f}{x_0:\tau_0, \ldots, x_n:\tau_n}{s'}}
+                 {\Gamma'}
+\iftrans{\\
+                 e_g = \elambda{x_0:\tau_0, \ldots, x_n:\tau_n}{\tau_r}{s'}\\
+                 s_g = \sreturn{(\echeck{\edcall{e_g}{x_0 , \ldots, x_n}}{\upsilon_r})} \\
+                 \mathit{vd}_g = \dfun{\upsilon_r}{f}{x_0:\upsilon_0, \ldots, x_n:\upsilon_n}{s_g} 
+}
+        }
+        {
+          \declOk[ce]{\Phi, \Delta, \Gamma}
+                 {\mathit{vd} : \methodDecl{f}{\sigma_i}{\sigma_e}}
+                 {\mathit{vd}_g}
+                 {\Gamma'}
+        }
+
+\subsection*{Class declaration typing:  $\declOk[c]{\Phi, \Gamma}{\mathit{cd}}{\mathit{cd'}}{\Gamma'}$}
+\hrulefill\\
+
+\sstext{ 
+
+A class declaration is well-typed with a given signature ($\Sig$) taken from the
+class hierarchy if the signature matches the definition, and if each member of
+the class is well-typed with the corresponding signature from the class
+signature.  The members are checked with the generic type parameters bound in
+the type context, and with the type of the current class set as the type of
+$\ethis$ on the term context $\Gamma$.
+
+}
+{
+
+Elaboration of a class requires that the class hierarchy $\Phi$ have a matching
+signature for the class declaration.  Each class member in the class is
+elaborated using the corresponding class element from the signature.
+
+}
+
+
+\infrule{\mathit{cd} = \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{\tau}}}{\mathit{vd}_0, \ldots, \mathit{vd}_n} \\
+         (C : \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{\tau}}}{\mathit{ce}_0, \ldots, \many{ce}_n}) \in \Phi \\ 
+         \Delta = \many{T} \quad 
+         \Gamma_i = 
+         \begin{cases}
+           \Gamma_{\TApp{C}{\many{T}}} & \mbox{if $\mathit{vd}_i$ is a method} \\
+           \Gamma & \mbox{if $\mathit{vd}_i$ is a field} \\
+         \end{cases}\\
+
+         \declOk[ce]{\Phi, \Delta, \Gamma_i}{\mathit{vd}_i : \mathit{ce}_i}{\mathit{vd}'_i}{\Gamma'_i} \quad\quad
+         \mbox{for}\ i \in 0, \ldots, n 
+\iftrans{\\
+         \mathit{cd'} = \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{\tau}}}{\many{\mathit{vd'}}}
+}
+        }
+        {\declOk[c]{\Phi, \Gamma}
+                   {\mathit{cd}}
+                   {\mathit{cd'}}{\Gamma'}
+        }
+
+\subsection*{Override checking:\\  \quad\quad$\overrideOk{\Phi}
+                                             {\TApp{C}{T_0, \ldots, T_n}}
+                                             {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                                             {\mathit{ce}}$}
+\hrulefill\\
+
+\sstext{
+
+The override checking relation is the primary relation that checks the
+consistency of the class hierarchy.  We assume a non-cyclic class hierarchy as a
+syntactic pre-condition.  The override check relation checks that in a class
+declaration $\TApp{C}{T_0, \ldots, T_n}$ which extends $\TApp{G}{\tau_0, \ldots,
+  \tau_k}$, the definition of an element with signature $\mathit{ce}$ is valid.  
+
+}{
+
+Override checking remains largely the same, with the exception of additional
+consistency constraints on the internal signatures for methods.
+
+}
+
+\sstext{
+
+A field with the type elided is a valid override if the same field with type
+$\Dynamic$ is valid.
+
+}{
+
+}
+
+\infrule{
+           \overrideOk{\Phi}
+                 {\TApp{C}{T_0, \ldots, T_n}}
+                 {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                 {\fieldDecl{x}{\Dynamic}}
+
+        }
+        {
+         \overrideOk{\Phi}
+                 {\TApp{C}{T_0, \ldots, T_n}}
+                 {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                 {\fieldDecl{x}{\_}}
+        }
+
+\sstext{
+
+A field with a type $\tau$ is a valid override if it appears in the super type
+with the same type.
+
+}{
+
+}
+
+\infrule{\fieldLookup{\Phi}{\TApp{G}{\tau_0, \ldots, \tau_k}}{x}{\tau}
+        }
+        {
+         \overrideOk{\Phi}
+                 {\TApp{C}{T_0, \ldots, T_n}}
+                 {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                 {\fieldDecl{x}{\tau}}
+        }
+
+\sstext{
+
+A field with a type $\tau$ is a valid override if it does not appear in the super type.
+
+}{
+
+}
+
+\infrule{\fieldAbsent{\Phi}{\TApp{G}{\tau_0, \ldots, \tau_k}}{x}
+        }
+        {
+         \overrideOk{\Phi}
+                 {\TApp{C}{T_0, \ldots, T_n}}
+                 {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                 {\fieldDecl{x}{\tau}}
+        }
+
+\sstext{
+
+A method with a type $\sigma$ is a valid override if it does not appear in the super type.
+
+}{
+
+For a non-override method, we require that the internal type $\tau$ be a subtype
+of $\down{\sigma}$ where $\sigma$ is the declared type.  Essentially, this
+enforces the property that the initial declaration of a method in the hierarchy
+has a covariant internal type.
+
+}
+
+\infrule{
+\iftrans{
+      \Delta = T_0, \ldots, T_n \quad\quad
+      \subtypeOf{\Phi, \Delta}{\tau}{\down{\sigma}}\ \\
+}
+      \methodAbsent{\Phi}{\TApp{G}{\tau_0, \ldots, \tau_k}}{f}
+    }
+    {
+      \overrideOk{\Phi}
+                 {\TApp{C}{T_0, \ldots, T_n}}
+                 {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                 {\methodDecl{f}{\tau}{\sigma}}
+    }
+
+\sstext{
+
+A method with a type $\sigma$ is a valid override if it appears in the super
+type, and $\sigma$ is a subtype of the type of the method in the super class.
+
+}{
+
+For a method override, we require two coherence conditions.  As before, we
+require that the internal type $\tau$ be a subtype of the $\down{\sigma}$ where
+$\sigma$ is the external type.  Moreover, we also insist that the external type
+$\sigma$ be a subtype of the external type of the method in the superclass, and
+that the internal type $\tau$ be a subtype of the internal type in the
+superclass.  Note that it this last consistency property that ensures that
+covariant generics are ``poisonous'' in the sense that non-generic subclasses of
+generic classes must still have additional checks.  For example, a superclass
+with a method of external type $\sigma_s = \Arrow{T}{T}$ will have internal type
+$\tau_s = \Arrow{\Dynamic}{T}$.  A subclass of an instantiation of this class
+with $\Num$ can validly override this method with one of external type $\sigma =
+\Arrow{\Num}{\Num}$.  This is unsound in general since the argument occurrence
+of $T$ in $\sigma_s$ is contra-variant.  However, the additional consistency
+requirement is that the internal type of the subclass method must be a subtype
+of $\subst{\Num}{T}{\tau_s} = \Arrow{\Dynamic}{\Num}$.  This enforces the
+property that the overridden method must expect to be used at type
+$\Arrow{\Dynamic}{\Num}$, and hence must check its arguments (and potentially
+its return value as well in the higher-order case).  This checking code is
+inserted during the elaboration of class members above.
+
+  }
+
+\infrule{
+\iftrans{
+      \Delta = T_0, \ldots, T_n \quad\quad 
+      \subtypeOf{\Phi, \Delta}{\tau}{\down{\sigma}}\ \\
+}
+      \methodLookup{\Phi}{\TApp{G}{\tau_0, \ldots, \tau_k}}{f}{\tau_s}{\sigma_s} \\
+\iftrans{
+      \subtypeOf{\Phi, \Delta}{\tau}{\tau_s}\quad\quad 
+}
+      \subtypeOf{\Phi, \Delta}{\sigma}{\sigma_s}
+    }
+    {
+      \overrideOk{\Phi}
+                 {\TApp{C}{T_0, \ldots, T_n}}
+                 {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                 {\methodDecl{f}{\tau}{\sigma}}
+    }
+
+\subsection*{Toplevel declaration typing:  $\declOk[t]{\Phi, \Gamma}{\mathit{td}}{\mathit{td'}}{\Gamma'}$}
+\hrulefill\\
+
+\sstext{
+
+Top level variable declarations are well-typed if they are well-typed according
+to their respective specific typing relations.
+
+}{
+
+Top level declaration elaboration falls through to the underlying variable and
+class declaration code.
+
+}
+
+\infrule
+    {\declOk[d]{\Phi, \epsilon, \Gamma}{\mathit{vd}}{\mathit{vd'}}{\Gamma'}
+      
+    }
+    {\declOk[t]{\Phi, \Gamma}{\mathit{vd}}{\mathit{vd'}}{\Gamma'}
+    }
+
+\infrule
+    {\declOk[c]{\Phi, \Gamma}{\mathit{cd}}{\mathit{cd'}}{\Gamma'}
+      
+    }
+    {\declOk[t]{\Phi, \Gamma}{\mathit{cd}}{\mathit{cd'}}{\Gamma'}
+    }
+
+
+\subsection*{Well-formed class signature:  $\ok{\Phi}{\Sig}$}
+\hrulefill\\
+
+\sstext{
+
+The well-formed class signature relation checks whether a class signature is
+well-formed with respect to a given class hierarchy $\Phi$.
+
+}{
+
+}
+
+\sstext{
+
+The $\Object$ signature is always well-formed.
+
+}{
+
+}
+
+\axiom{\ok{\Phi}{\Object}
+      }
+
+\sstext{
+
+A signature for a class $C$ is well-formed if its super-class signature is
+well-formed, and if every element in its signature is a valid override of the
+super-class.
+
+}{
+
+}
+
+\infrule{\Sig = \dclass{\TApp{C}{\many{T}}}
+                              {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                              {\mathit{ce}_0, \ldots, \mathit{ce}_n} \\
+        (G : \Sig') \in \Phi \quad\quad \ok{\Phi}{\Sig'} \\
+        \overrideOk{\Phi}{\TApp{C}{\many{T}}}{\TApp{G}{\tau_0, \ldots, \tau_k}}{\mathit{ce}_i} 
+        \quad\quad
+        \mbox{for}\ \mathit{ce}_i \in \mathit{ce}_0, \ldots, \mathit{ce}_n 
+        }
+        {\ok{\Phi}{\Sig}
+        }
+
+\subsection*{Well-formed class hierarchy:  $\ok{}{\Phi}$}
+\hrulefill\\
+
+\sstext{
+
+A class hierarchy is well-formed if all of the signatures in it are well-formed
+with respect to it.
+
+}{
+
+}
+
+\infrule{\ok{\Phi}{\Sig}\ \mbox{for}\, \Sig\, \in \Phi
+        }
+        {\ok{}{\Phi}
+        }
+
+\subsection*{Program typing:  $\programOk{\Phi}{P}{P'}$}
+\hrulefill\\
+
+%%Definitions:
+%%
+%% \begin{eqnarray*}
+%% \sigof{\mathit{vd}} & = &
+%%   \begin{cases}
+%%     \fieldDecl{x}{\tau} & \mbox{if}\ \mathit{vd} = \dvar{x:\tau}{e}\\
+%%     \fieldDecl{x}{\Dynamic} & \mbox{if}\ \mathit{vd} = \dvar{x:\_}{e}\\
+%%     \methodDecl{f}{\tau_f}{\Arrow[+]{\many{\tau}}{\sigma}} & \mbox{if}\ \mathit{vd} = \dfun{\sigma}{f}{\many{x:\tau}}{s}
+%% \end{cases}\\
+%% \sigof{\mathit{cd}} & = & C\, : \, \dclass{\TApp{C}{\many{T}}}
+%%                                          {\TApp{G}{\tau_0, \ldots, \tau_k}}
+%%                                          {\mathit{ce}_0, \ldots, \mathit{ce}_n} \\
+%% \mbox{where} && 
+%%          \mathit{cd} = \dclass{\TApp{C}{\many{T}}}
+%%                               {\TApp{G}{\tau_0, \ldots, \tau_k}}
+%%                               {\mathit{vd}_0, \ldots, \mathit{vd}_n} \\
+%% \mbox{and} &&
+%%         \mathit{ce}_i = \sigof{vd_i} \quad \mbox{for}\ i \in 0, \ldots, n 
+%%\end{eqnarray*}
+
+\sstext{
+
+Program well-formedness is defined with respect to a class hierarchy $\Phi$.  It
+is not specified how $\Phi$ is produced, but the well-formedness constraints in
+the various judgments should constrain it appropriately.  A program is
+well-formed if each of the top level declarations in the program is well-formed
+in a context in which all of the previous variable declarations have been
+checked and inserted in the context, and if the body of the program is
+well-formed in the final context.  We allow classes to refer to each other in
+any order, since $\Phi$ is pre-specified, but do not model out of order
+definitions of top level variables and functions.  We assume as a syntactic
+property that the class hierarchy $\Phi$ is acyclic.
+
+}{
+
+}
+
+\infrule{  \Gamma_0 = \epsilon \quad\quad
+           \declOk[t]{\Phi, \Gamma_i}{\mathit{td}_i}{\mathit{td}'_i}{\Gamma_{i+1}} \quad 
+           \mbox{for}\ i \in 0,\ldots,n\\
+           \stmtOk{\Phi, \epsilon, \Gamma_{n+1}}{s}{\tau}{s'}{\Gamma_{n+1}'}
+        }
+        { \programOk{\Phi}{\program{\mathit{td}_0, \ldots, \mathit{td}_n}{s}}
+          {\program{\mathit{td}'_0, \ldots, \mathit{td}'_n}{s'}}
+        }