\section{A type system for \SystemF}
\label{sect.systemftypesystem}

The type system given in \Sect{sect.typesystem} is a GADT-extension of a type system for \SystemF. This appendix gives a bit of background information by giving a bit of explanation of the type system if we leave out support for GADTs.

First we give a full type system for \SystemF in \Fig{rules.F.decl.base}, \Fig{rules.F.expr.base}, \Fig{rules.F.pat.base}, \Fig{rules.F.kind.base}. These correspond to the typing rules given by Pierce~\cite{pierce02}. Bindings are collected in a separate local environment |envl| during pattern matches and merged with the global environment |env|, when passing them on to other judgements as |envl env|. The initial environment at the root of the expression contains the two signatures for each constructor and the name of each data type as type constructor.

\rulerCmdUse{rules.F.decl.base}
\rulerCmdUse{rules.F.expr.base}
\rulerCmdUse{rules.F.pat.base}
\rulerCmdUse{rules.F.kind.base}

Then we add existentials in \Fig{rules.FE.decl.base}, \Fig{rules.FE.expr.base}, \Fig{rules.FE.pat.base}, \Fig{rules.FE.kind.base}. An existential is opened by a pattern match that binds a name to the existential (as a skolumnized type variable). This name must be unique and may not be part of types that escape out the scope of the binding. The intersection of the free variables of the types and the local environments, gives us those variables mentioned by the bindings that are about to escape. Only the variables that are part of an outer scope |env| are allowed to escape. This we express formally as |ftv(ty) >< ftv(envl) <== ftv(env)| or equivalently |(ftv(ty) / ftv(env)) >< ftv(envl) = emptyset|.

\rulerCmdUse{rules.FE.decl.base}
\rulerCmdUse{rules.FE.expr.base}
\rulerCmdUse{rules.FE.pat.base}
\rulerCmdUse{rules.FE.kind.base}


\section{Semantics of the \SystemFC coercions}
\label{sect.systemfcsemantics}

Consult the \SystemFC paper for a semantics of the coercions. Alternatively, consider the following alternative specification of entailment in \Fig{rules.G.entails.alt}.

\rulerCmdUse{rules.G.entails.alt}