\documentclass[preprint]{sigplanconf}
  
%\usepackage[british]{babel}
\usepackage{version}
\usepackage{ifthen}
\usepackage{amsmath}
\usepackage{amsfonts,amssymb}
\usepackage{haskell}
\usepackage{url}
\usepackage{verbatim}

%\renewcommand{\textfraction}{0.4}
%\renewcommand{\topfraction}{1}
%\renewcommand{\dbltopfraction}{1}
%\renewcommand{\floatpagefraction}{0.7}
%\renewcommand{\dblfloatpagefraction}{0.9}

% version control
%
\includeversion{DRAFT}
%\excludeversion{DRAFT}

\def\Version{\relax}
\begin{DRAFT}%
{
  \gdef\Version{%
    \\[1ex]
    \textbf{--- DRAFT [\today] ---}\\[1ex]
%    \ttfamily\scriptsize
%    $\relax$Id: at-syns.tex,v 1.65 2005/07/11 11:29:25 chak Exp $\relax$%
    \ignorespaces}
  }
\end{DRAFT}

% Put figures in boxes
\usepackage{float}
\floatstyle{boxed}
\restylefloat{figure}

%\setlength{\parskip}{0.5\baselineskip plus 0.2\baselineskip minus 0.1\baselineskip}
%\setlength{\parsep}{\parskip}

% fonts
%
\DeclareMathAlphabet{\mathsfsbc}{T1}{cmss}{sbc}{n}

% Haskell style
%
%\hsmargin.5\leftmargini
%\hsmargin0pt
\renewcommand{\hsstr}[1]{\texttt{"#1"}}               % strings literals

% Names
\newcommand{\FC}{\ensuremath{\mathrm{F}_{\mathrm{C}}}}

% Flush left function heads in align environments
%
\newcommand{\flushlefteqn}[1]{\omit\(#1\)\hfil}

% Syntax for programs
%
\newcommand{\data}{\mathbf{data}}
\newcommand{\type}{\mathbf{type}}
\newcommand{\newtype}{\mathbf{newtype}}
\newcommand{\class}{\mathbf{class}}
\newcommand{\instance}{\mathbf{instance}}
\newcommand{\where}{\mathbf{where}}
\newcommand{\letkwd}{\mathbf{let}}
\newcommand{\inkwd}{\mathbf{in}}
\newcommand{\coercion}{\mathbf{coercion}}

% Syntax for FC
%
\newcommand{\eqc}[2]{{#1}\doteq{#2}}                  % Equality constraint
\newcommand{\cast}[2]{{#1}\blacktriangleright{#2}}    % Term casting
% Constant coerctions: refl, sym etc
%\newcommand{\refl}[1]{\operatorname{refl}~{#1}}
\newcommand{\dleft}[1]{\operatorname{left}~{#1}} 
\newcommand{\dright}[1]{\operatorname{right}~{#1}}
\newcommand{\sym}[1]{\operatorname{sym}~{#1}}
\newcommand{\inst}[2]{\operatorname{inst}~{#1}~{#2}}
\newcommand{\trans}[2]{{#1}\rhd{#2}}
% \newcommand{\trans}[2]{\operatorname{trans}~{#1}~{#2}}
\newcommand{\evkind}{\diamond}   % The kind of evidence
%\newcommand{\comp}[2]{\operatorname{comp}~{#1}~{#2}}
\newcommand{\comp}[2]{{#1}\icomp{#2}}
%\newcommand{\scomp}[2][S]{\operatorname{comp}_{#1}~{#2}}
\newcommand{\scomp}[2][S]{{#1}\icomp{#2}}
\newcommand{\icomp}{\mathop{\odot}}

% Syntax for type system
%
\newcommand{\ruleform}[1]{\fbox{\Large $#1$}}
\newcommand{\ruleformsm}[1]{\fbox{\large $#1$}}
\newcommand{\To}{\Rightarrow}

% \bvar{x}{t} expands to    x:t
% Used for bound variables
\newcommand{\bvar}[2]{{#1}{:}{#2}}
\newcommand{\bstar}[1]{\bvar{#1}\star}

\newcommand{\rulename}[1]{$(\mathit{#1})$}

\newcommand{\typing}[3][\Theta\mid\Gamma]{{#1}\vdash{#2 : #3}}
\newcommand{\kinding}[3][\Gamma]{{#1}\vdash{#2}:{#3}}
\newcommand{\pikinding}[2][\Gamma]{{#1}\vdash{#2}}
\newcommand{\wfpi}[2][\Theta]{{#1}\vdash{#2}}
\newcommand{\tyeq}[3][\Theta]{{#1}\Vdash{{#2}={#3}}}

% \ttyping{env}{e}{e'}{t} expands to     env |- e --> e' : t
% used for terms
\newcommand{\ttyping}[4][\Theta\mid\Gamma]{%
  {#1}\vdash{{#2}\leadsto{#3}:{#4}}%
}
\newcommand{\tkinding}[4][\Gamma]{{#1}\vdash{#2}\leadsto{#3}:{#4}}
\newcommand{\tpikinding}[3][\Gamma]{{#1}\vdash{#2}\leadsto{#3}}

\newcommand{\ttyeq}[4][\Theta]{{#1}\Vdash{{#2}={#3}}\leadsto{#4}}

% \tdecl{env}{d}{d':G} expands to     env |- d --> d' : G
% used for terms
\newcommand{\tdecl}[3][\Theta\mid\Gamma]{%
  {#1} \vdash {#2} \leadsto {#3}%
}

% \rtype[env]{t}{u}     expands to     env |- t --> u
% \rtypen[env]{n}{t}{u} expands to the same, with a bar over t-->u

\newcommand{\rtype}[3][\Gamma]{{#1}\vdash{{#2}\leadsto{#3}}}
\newcommand{\rtypen}[4][\Gamma]{{#2}\vdash{\tupn{#2}{{#3}\leadsto{#4}}}}

\newcommand{\teq}[3][\Pi]{{#1}\vdash{#2\eqeq#3}}
\newcommand{\entails}[2][\Theta]{{#1}\Vdash{#2}}

\newcommand{\tentails}[3][\Theta]{{#1}\Vdash{#2}\leadsto{#3}}

% \tentailsT{theta}{w}{t}  expands to   p ||- theta --> w
\newcommand{\tentailsT}[3][\Omega\mid\Delta]{{#1}\Vdash{#3 \leadsto #2}}

% \rpiE{pi}{ts}{t}  expands to   p |- pi --> ts
\newcommand{\rpiE}[3][\Omega]{{#1}\vdash{#3 \leadsto #2}}
\newcommand{\rpiEn}[4][\Omega]{{#1}\vdash{\tupn{#2}{#4 \leadsto #3}}}

% \rpiI{pi}{alpha}{tau}{taus}  expands to   omega |- pi --> alpha, tau, taus
\newcommand{\rpiI}[5][\Omega]{{#1}\vdash{#2 \leadsto (#4\leadsto#3),\;#5}}
\newcommand{\rpiIn}[6][\Omega]{
  {#1}\vdash{\tupn{#2}{#3 \leadsto (#5\leadsto#4),\;#6}}}

\newcommand{\simplifies}{\leadsto}
\newcommand{\simplifiesS}{\leadsto^{*}}
\newcommand{\simplifiesto}{\leadsto^{!}}

\newcommand{\Wdash}{%
  \mathrel{\vdash^{\!\!\!\raisebox{.3em}{\scriptsize W}}}}
\newcommand{\tinf}[3][\Theta,U\mid{T}\Gamma]{{#1}\Wdash{#2:#3}}
\newcommand{\tunify}[4][!*NEVER USED ARGUMENT*!]{%
  \ifthenelse{\equal{#1}{!*NEVER USED ARGUMENT*!}}{%
    {#2\mathrel{=_{#3}}#4}
  }{%
    {#2\mathrel{\overset{#1}=_{#3}}#4}
  }%
}
\newcommand{\unifsimpl}[3][\Theta,U]{\Theta\Vdash_U{#2}\simplifies{#3}}
\newcommand{\unifsimplS}[3][\Theta,U]{\Theta\Vdash_U{#2}\simplifiesS{#3}}
\newcommand{\unifsimplto}[3][\Theta_P]{#1\Vdash_U{#2}\simplifiesto{#3}}
\newcommand{\entailsimpl}[3][\Theta,P]{\Theta\Vdash_E{#2}\simplifies{#3}}
\newcommand{\entailsimplS}[3][\Theta,P]{\Theta\Vdash_E{#2}\simplifiesS{#3}}
\newcommand{\entailsimplto}[3][\Theta_P]{#1\Vdash_E{#2}\simplifiesto{#3}}
\newcommand{\normal}[3][\Theta]{\Theta\Vdash{#2}\Downarrow{#3}}
\newcommand{\tred}[3][\Theta]{#1\Vdash{#2}\leadsto{#3}}
\newcommand{\Gen}[2]{\mathop{\operatorname{Gen}}(#1;#2)}
\newcommand{\subsumes}[3][\Theta_P]{{#1}\Vdash{#2}\leq{#3}}
\newcommand{\Impr}[1]{\mathop{\operatorname{Impr}_\Phi}#1}
\newcommand{\impr}[1]{\mathop{\operatorname{impr}_\Phi}#1}
\newcommand{\Simp}[1]{\mathop{\operatorname{Simp}_\Phi}#1}
\newcommand{\simp}[1]{\mathop{\operatorname{simp}_\Phi}#1}
\newcommand{\norm}{{\downarrow}}
\newcommand{\Class}{\mathop{\operatorname{Class}}}
\newcommand{\Rules}{\mathop{\operatorname{Rules}}}

\newcommand{\vdashF}{\vdash_{F}}

% Syntax for expressions
%
\newcommand{\letin}[3]{\letkwd\;{#1=#2}\mathrel{\inkwd}{#3}}
\newcommand{\caseof}[2]{\mathbf{case}\;{#1}\mathrel{\mathbf{of}}{#2}}

% Misc. classes of symbols
%
\newcommand{\meta}[1]{\mathit{#1}}      % meta-level variables
\newcommand{\defconst}[1]{\mathsf{#1}}  % defined constant
\newcommand{\mathname}[1]{%             % multi-character name in math mode
  \mathord{\mathit{#1}}}

\newcommand{\tup}[1]{\overline{#1}}     % tuple
\newcommand{\tupn}[2]{\overline{#2}^{#1}}     

\newcommand{\inform}[1]{\ensuremath{\langle\text{#1}\rangle}}

% Operators
%
\newcommand{\Fv}{\operatorname{Fv}}
\newcommand{\Fixv}{\operatorname{Fixv}}

% Inference rules
%
\newcommand{\Inf}[3][!*NEVER USED ARGUMENT*!]{%
  \ifthenelse{\equal{#1}{!*NEVER USED ARGUMENT*!}}{%
    \dfrac{#2}{#3}
  }{%
    \dfrac{#2}{#3}(#1)
  }%
}

% Theorems
%
% Theorems
%
\newtheorem{definition}{Definition}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{corollary}{Corollary}

% Syntactic identity modulo an equational theory
%
\newcommand{\eqeq}{\doteq}


% TODO's
%
%\newcommand{\todo}[2]{\emph{\textbf{Review #1}: #2}}
\newcommand{\TODO}[1]{\emph{\textbf{TODO:} #1}}
\newcommand{\simon}[1]{\emph{\textbf{SLPJ:} #1}}
\newcommand{\martin}[1]{\emph{\textbf{MS:} #1}}
\newcommand{\manuel}[1]{\emph{\textbf{MMTC:} #1}}


\begin{document}

\toappear{\LARGE--- DRAFT---}

\makeatletter
\title{Beyond Associated Types
  \Version}
\makeatother
\authorinfo{
  Manuel M. T. Chakravarty\and Simon Peyton Jones\and Martin Sulzmann
}{
  % where
}{
  % \url{email}
}
\maketitle

\begin{abstract}
  Type inference for toplevel type-indexed type synonyms and data types as
  well as their translation to \FC.
\end{abstract}

\category{D.3.3}{Programming Languages}{Language Constructs and Features}
\terms
Design, Languages, Theory
\keywords
Type classes; Type functions; Associated types; Type inference; Generic
programming


\section{Introduction}
\label{sec:intro}

Plan:
%
\begin{itemize}
\item Definition of top-level abstract type constructors (in the \FC\ sense)
\item Definition of type functions and type-indexed data types
\item Associated types as a special case of the former
\item Type inference in the presence of type functions
\item Translation to \FC
\end{itemize}


\section{Examples}
\label{sec:examples}

\subsection{Disassociating associated types}

\manuel{These are just examples showing that associated types are simply sugar
  for disassociated types, and hence, we don't need cover the former in the
  formal part of the paper.}

Consider the following class involving an associated type synonym:%
%
\begin{haskell}
  \hsclass{Collects c}{%
    \hsnoalign{\type Elem c\qquad\qquad\hscom{Associated type synonym}}
    empty  &:: c\\
    insert &:: Elem c \to c \to c\\
    toList &:: c \to [Elem c]
  }
\end{haskell}
%
It corresponds to the following declaration where the associated synonym is
disassociated:
%
\begin{haskell}
  \type Elem c \qquad\qquad\hscom{Non-injective disassociated type}\\
  \hsclass{Collects c}{
    empty  &:: c\\
    insert &:: Elem c \to c \to c\\
    toList &:: c \to [Elem c]
  }
\end{haskell}

We proceed similarly with instance declarations.  Instead of
%
\begin{haskell}
  \instance Eq e \To Collects [e] \where 
  \\ ~~~~~~ \{\type Elem [e] = e; \ldots\}\\
  \instance Collects BitSet \where
  \\ ~~~~~~ \{\type Elem BitSet = Char; \ldots\}\\
  \instance (Collects c, Hashable (Elem c)) \\ 
  ~~~~~~~~~~~\To~Collects (Array Int c)  \where
  \\ ~~~~~~ \{\type Elem (Array Int c) = Elem c; \ldots\}
\end{haskell}
%
we simply write
%
\begin{haskell}
  \type Elem [e] = e\\
  \instance Eq e \To Collects [e] \where \{\ldots\}\\
  \type Elem BitSet = Char \ldots\\
  \instance Collects BitSet \where \{\ldots\}\\
  \type Elem (Array Int c) = Elem c \\
  \instance (Collects c, Hashable (Elem c)) \\ 
  ~~~~~~~~~~~\To~Collects (Array Int c) \where \{\ldots\}
\end{haskell}

We can treat associated data types in a similar way by using injective
disassociated types.  For example, rather than
%
\begin{haskell}
  \hsclass{ArrayElem e}{
    \data Array e\\
    index :: Array e \to Int \to e
  }
\end{haskell}
%
we can write
%
\begin{haskell}
  \type Array e :> \star \qquad\qquad\hscom{Injective disassociated type}\\
  \hsclass{ArrayElem e}{
    index :: Array e \to Int \to e
  }
\end{haskell}

For the instance declarations we need to do a bit more work.  Instead of
%
\begin{haskell}
  \hsinstance{ArrayElem Int}{
    \data Array Int = IntArray UIntArr\\
    index (IntArray ar) i = indexUIntArr ar i
  }
  \hskip0pt\\
  \hsinstance{(ArrayElem a, ArrayElem b) \To\\
    \qquad{}ArrayElem (a, b)}{
    \data Array (a, b) = PairArray (Array a) (Array b)\\
    index (PairArray ar br) i = (index ar i, index br i)
  }
\end{haskell}
%
we write
%
\begin{haskell}
  \data ArrayInt = IntArray UIntArr\\
  \type Array Int = ArrayInt\\
  \hsinstance{ArrayElem Int}{
    index (IntArray ar) i = indexUIntArr ar i
  }
  \hskip0pt\\
  \data ArrayPair a b = PairArray (Array a) (Array b)\\
  \type Array (a, b) = ArrayPair a b\\
  \hsinstance{(ArrayElem a, ArrayElem b) \To\\
    \qquad{}ArrayElem (a, b)}{
    index (PairArray ar br) i = (index ar i, index br i)
  }
\end{haskell}

The nice thing is that we can handle associated type synonyms and associated
data types with just a single, more primitive mechanism.


\section{Details of the Language Extension}
\label{sec:informal}

\subsection{Defining disassociated types}

We declare the signature of an disassociated type either with the form
%
\begin{haskell}
  \type S a_1 \cdots a_n :: \kappa
\end{haskell}
%
or with the form
%
\begin{haskell}
  \type R a_1 \cdots a_n :> \kappa
\end{haskell}
%
where we require that the arity \(n\geq 1\) and $\kappa$ be a kind.  The
arguments $a_i$ may have kind annotations as well.  $S$ is a non-injective and
$R$ an injective disassociated type.  Injective disassociated types allow to
conclude that all \<t_i=t_i'\> if \<R t_1 \cdots t_n = R t_1' \cdots t_n'\>,
whereas this reasoning is unsound for non-injective disassociated types.  All
applications of both injective and non-injective disassociated types need to
be saturated.

Type equations for disassociated types take the form
%
\begin{haskell}
  \type S \tau_1 \cdots \tau_n = \tau
\end{haskell}
%
where the arity and the kinds of the $\tau_i$ and $\tau$ have to match the
siganture of $S$.  The arguments $\tau_i$ may only contain regular type
variables and type constructors; disassociated types are not permitted.  All
type equations for a type $S$ must be \emph{consistent.}  Two equations
\<S\hsap \tau_1 \cdots \tau_n = \tau\> and \<S\hsap \tau'_1 \cdots \tau'_n =
\tau'\> are consistent iff for every substitution $R$ with \<R(S \tau_1 \cdots
\tau_n) = R(S \tau'_1 \cdots \tau'_n)\>, we have \<R\tau = R\tau'\> (this is
semantic equality, not just syntactic; extension of Herbrand equality).  For
injective types we also require the converse; i.e., for every substitution $R$
such that \<R\tau = R\tau'\>, we need to have \<R(S \tau_1 \cdots \tau_n) =
R(S \tau'_1 \cdots \tau'_n)\>.

\manuel{In general, we cannot decide consistency and injectivity locally.
  Right-hand sides can contain disassociated types and we cannot decide
  whether \<S a = S' a\> without knowing all equations of $S$ and $S'$ in all
  modules every linked with this one.  So, we need to approximate.  To decide
  consistency, the crudest criterion would be to require syntactical identity
  of right-hand sides.  However, it may be convenient to relax this to
  syntactical identity after reducing both types as far as possible.  For
  injectivity, we may require that the outermost constructors of both
  right-hand sides are different regular type constructors---then, the
  right-hand sides never overlap.}

Note that disassociated types subsume the conventional notion of type synonyms
in Haskell.

\subsection{Type equalities}

Type equalities in signatures need to have the form \<S \tau_1\cdots\tau_n =
\tau\>.  They may not be (mutually) recursive.

\manuel{Do we want to restrict this to equalities where the arity of $S$ is
  exactly $n$, or allow $S$ to have an arity smaller then $n$.  I don't think
  there is a difference in expressiveness, maybe there is one in convenience.}

\manuel{I think, occurrences of non-injective DTs are ok in the $\tau_i$, but
  we will need to verify this.}

\manuel{What constraints do we impose on type equalities in class and instance
  heads?} 

\subsection{Functional dependencies}

\TODO{Maybe describe the translation of functional dependencies into
  disassociated types}


\section{The Type System}
\label{sec:typing}

In this section, we formalise a type system for a lambda calculus including
type classes and types functions.  Our treatment of type classes is based
on Jones' \emph{Overloaded ML
  (OML)}~\cite{jones:improving-qualified-types,jones:constr-class} and that of
type functions builds on our earlier work on associated
types~\cite{chak-etal:ATs,chak-etal:at-syns}.  In this section, we give the
declarative type system.  We extend this to a type-directed translation
targeting System \FC~\cite{sulzmann-etal:FC} in the following section, and
then go on to discuss type inference.

\subsection{Syntax}

\begin{figure}[tbp]
% \small
% \begin{minipage}{.605\textwidth}
  \[
%  \begin{array}{@{}l@{}}
  \begin{array}{l}
    %
    \begin{array}{@{}lcl}
      \multicolumn{3}{@{}l}{\textbf{Symbol Classes}} \\
      \alpha,\beta,\gamma 
                & \rightarrow & \inform{type variable} \\
      T         & \rightarrow & \inform{type constructor} \\
      S^k_\iota,
      R^k_\iota & \rightarrow & 
        \inform{type function, arity $k$, injectivity $\iota$} \\
      C         & \rightarrow & \inform{type class} \\
%      C        & \rightarrow & \inform{data constructor} \\
      x,f       & \rightarrow & \inform{term variable} \\
    \end{array} \\ \\
    %
    \begin{array}{@{}lcll}
      \multicolumn{4}{@{}l}{\textbf{Source declarations}} \\
      pgm & \rightarrow & \tup{tdec}; ~ \tup{\mathit{tdef}}; ~ \tup{cls}; 
                           ~ \tup{inst}; ~ \tup{val}
      & (\text{whole program}) \\
      cls  & \rightarrow & 
        \multicolumn{2}{l}{%
          \class~\forall\tup{\bvar\alpha\kappa}.
            \tup{\pi^\circ}\To C~\tup\alpha~\where
          \quad (\text{class decl})%
        } \\
                        && \quad\tup{vsig} \\
      inst  & \rightarrow & \instance~\forall\tup{\bvar\alpha\kappa}.\phi~\where
      & (\text{instance declaration}) \\
                         && \quad\tup{val} \\
      vsig & \rightarrow & x :: \sigma & (\text{method signature}) \\
      val  & \rightarrow & x ~=~ e  & (\text{value binding}) \\
      tdec & \rightarrow & \type~S^{k}_{{:}{:}}~\tupn{k}\alpha :: \kappa
           & (\text{non-injective type}) \\
           & \mid        & \type~S^{k}_{{:}{>}}~\tupn{k}\alpha :> \kappa
           & (\text{injective type}) \\
      \mathbin{tdef} 
           & \rightarrow & \type~\forall\tup{\bvar\alpha\kappa}.\,
                             S^{k}_\iota~\tupn{k}\tau~=~\xi 
           & (\text{type equation}) \\
    \end{array} \\ \\
    %
    \begin{array}{@{}lcll}
      \multicolumn{3}{@{}l}{\textbf{Source terms}} \\
      e & \rightarrow & x ~|~ e_1 ~ e_2 ~|~ \lambda{}x.e  
        ~|~ \letin{x}{e_1}{e_2} ~|~ e::\sigma \\
    \end{array}  \\ \\
    %
    \begin{array}{@{}lcl}
      \multicolumn{3}{@{}l}{\textbf{Kinds}} \\
      \kappa & \rightarrow & \star ~|~ \kappa_1 \to \kappa_2
    \end{array} \\ \\
    %
    \begin{array}{@{}lcll}
     \multicolumn{4}{@{}l}{\textbf{Source types}} \\
     \tau,
     \xi  & \rightarrow & T  ~|~ \alpha  ~|~ \tau_1 ~ \tau_2 ~|~ \eta 
       & (\text{monotype})\\
     \eta & \rightarrow & S^{k}_\iota~\tupn{k}\tau
       & (\text{type function application}) \\
     \rho& \rightarrow & \tup\pi\To\tau
       & (\text{qualified type})\\
     \sigma & \rightarrow & \forall\tup{\bvar\alpha\kappa}.\rho
       & (\text{type scheme})\\
   \end{array}  \\ \\
   %
   \begin{array}{@{}lcll}
     \multicolumn{4}{@{}l}{\textbf{Constraints}} \\
     \pi_c & \rightarrow & C~\tup\tau
       & (\text{class constraint})\\
     \pi_= & \rightarrow & \eta=\tau
       & (\text{oriented equality constraint})\\
     \pi & \rightarrow & \pi_C \mid \pi_= \\
     \pi^\circ& \rightarrow & C~\tup\alpha 
              ~|~ S^{k}_\iota~\tupn{k}\alpha=\beta\\
     \phi& \rightarrow & \tup\pi \To \pi_c
       & (\text{qualified constraint})\\
     \theta & \rightarrow & \forall\tup{\bvar\alpha\kappa}.\phi 
            ~|~ \forall\tup{\bvar\alpha\kappa}.\pi_=
       & (\text{constraint scheme})\\
   \end{array} \\ \\

   \begin{array}{@{}lcll}
       \multicolumn{4}{@{}l}{\textbf{Environments}} \\
       \Gamma & \rightarrow & \epsilon \mid \Gamma,\bvar{x}{\sigma}
         & (\text{type and}) \\
              & \mid        & \Gamma,\bvar{T}{\kappa}
                              \mid \Gamma,\bvar{C}{\kappa}
                              \mid \Gamma,\bvar{\alpha}{\kappa}
         & (\text{kind environment}) \\
       \Theta & \rightarrow & \tup{\theta}      
         & (\text{predicate environment}) \\
       U & \rightarrow & \tup{\tau_1=\tau_2}    
         & (\text{set of equalities}) \\
   \end{array}
 \end{array}
  \]
% \end{minipage}
  \caption{Syntax of expressions and types}
  \label{fig:syntax}
\end{figure}
%
The syntax of the source language is given in Figure~\ref{fig:syntax}.  
%
We use overbar notation extensively. The notation $\tupn{n}{\alpha}$ means the
sequence $\alpha_1 \cdots \alpha_n$; the ``$n$'' may be omitted when it is
unimportant.  Moreover, we use comma to mean sequence extension as follows:
$\tupn{n}{a},a_{n+1} \triangleq \tupn{n+1}{a}$.  Although we give the syntax
of qualified and quantified types and constraints in an uncurried way, we also
sometimes use equivalent curried notation, thus:
\[
\begin{array}{rcl}
\tupn{n}{\pi}\To\tau & \equiv & \pi_1 \To \cdots \To \pi_n \To \tau \\
\tupn{n}{\tau}\to\xi & \equiv & \tau_1 \to \cdots \to \tau_n \to \xi \\
\forall \tupn{n}{\bvar\alpha\kappa}.\rho & \equiv & 
  \forall \bvar{\alpha_1}{\kappa_1} \cdots \forall \bvar{\alpha_n}{\kappa_n}.
  \rho \\
\lambda \tupn{n}x.e & \equiv &   \lambda{x_1} \cdots \lambda{x_n}. e
\end{array}
\]
We accommodate function types $\tau_1 \to \tau_2$ by regarding them as the
curried application of the function type constructor to two arguments, thus
$(\to)~\tau_1~\tau_2$.  We use \<(\Fv x)\> to denote the free variables of a
structure $x$, which maybe an expression, type term, or environment.

The unusual features of the source language all concern type functions.  The
type constructors of type functions are syntactically distinguished: $S$ is a
distinguished type constructor, while $T$ is a regular type constructor (such
as lists or pairs).  We have declarations and type equations for type
functions on the toplevel.  Declarations appear in two flavours: as
non-injective types (using the usual \<::\>) and as injective types (using
\<:>\>).  Moreover, the number of type variables in a type function
declaration determines its \emph{arity}.  The arity is given by a superscript
to the constructor name, but we drop it when it is clear from the context.
Similarily, the injectivity is indicated by a subscript, which we also drop
when it is clear or irrelevant.

The syntax of types $\tau$ includes $\eta$, the saturated application of a
type function.  Note that such a saturated application can be of higher
kind, if the result kind $\kappa$ in the defining $tdec$ is not $\star$.
Finally, in addition to conventional class constraints, constraints can be
equalities whose right-hand side is the application of a type function.

In the formal syntax, all classes have excatly one method.  This notational
simplification saves a considerable number of overbars.

\subsection{Well-formed programs}

We require that
%
\begin{itemize}
\item Type equations are consistent.
\item Type equations are terminating.
\item Toplevel type equations don't have occurences of disassociated types in
  their type patterns.
\item Class heads \ldots and instance heads \ldots.
\end{itemize}
%
\manuel{We could probably say that type equations are confluent, instead of
  consistent---this is assuming they are terminating.}

\manuel{We may allow overlapping instances, but it may make some of the rules
  more messy (as we would have to specify best fit, but maybe that's not much
  of an issue as we describe the translation using the declarative system).}

\subsection{Type checking}

% ---------------------------- Typing rules (no translation) ----------
\begin{figure*}[tbp]
\small
  \centering
  \renewcommand{\arraystretch}{3}
  \ruleform{\typing{e}{\sigma}} \\
  \begin{gather*}
    \Inf[\mathit{var}]{
      (x:\sigma)\in\Gamma
    }{
      \typing{x}{\sigma}
    }
    \qquad
    \Inf[\mathit{let}]{
      \typing[\Theta_1\mid\Gamma]{e_1}{\sigma_1} 
      \qquad 
      \typing[\Theta_2\mid\Gamma{[x:\sigma_1]}]{e_2}{\sigma_2}
    }{
      \typing[\Theta_1,\Theta_2\mid\Gamma]{\letin{x}{e_1}{e_2}}{\sigma_2}
    }
    \qquad
    \Inf[\mathit{conv}]{
      \typing{e}{\tau_1}
      \qquad 
      \tyeq{\tau_1}{\tau_2}
    }{
      \typing{e}{\tau_2}
    }
    \\[2ex]
    %
    \Inf[{\to}I]{
      \typing[\Theta \mid \Gamma{[\bvar{x}{\tau_1}]}]{e_2}{\tau_2} 
      \qquad 
      \kinding{\tau_1}\star
    }{
      \typing{\lambda x.e_2}{\tau_1\to\tau_2}
    }
    \qquad
    \Inf[{\to}E]{
      \typing{e_1}{\tau_2\to\tau_1} \qquad \typing{e_2}{\tau_2}
    }{
      \typing{e_1~e_2}{\tau_1}
    }
    \\[2ex]
    %
    \Inf[{\To}I]{
      \typing[\Theta,\pi\mid\Gamma]{e}{\rho}
    }{
      \typing{e}{\pi \To \rho}
    }
    \qquad
    \Inf[{\To}E]{
      \typing{e}{\pi\To\rho} 
      \qquad 
      \entails[\Theta]{\pi}
    }{
      \typing{e}{\rho}
    }
    \\[2ex]
    %
    \Inf[{\forall}I]{
      \typing[\Theta\mid\Gamma,\alpha:\kappa]{e}{\sigma} 
      \qquad 
      \alpha\not\in\Fv\Theta\cup\Fv\Gamma
    }{
      \typing{e}{\forall{\bvar\alpha\kappa}.\sigma}
    }
    \qquad
    \Inf[{\forall}E]{
      \typing{e}{\forall\bvar\alpha\kappa.\sigma} 
      \qquad 
      \kinding{\tau}\kappa
    }{
      \typing{e}{[\tau/\alpha]\sigma}
    }
\qquad
    \Inf[\mathit{sig}]{
      \typing{e}{\sigma}
      \qquad
      \Fv\sigma=\emptyset
    }{
      \typing{(e::\sigma)}{\sigma}
    }
  \end{gather*} \\[2ex]

  \ruleform{\kinding\sigma\kappa} \\
  \begin{gather*}
  \Inf[\mathit{tcon}]{
    (T:\kappa)\in\Gamma
  }{
    \kinding{T}\kappa
  } 
  \qquad
  \Inf[\mathit{tvar}]{
    (\alpha:\kappa)\in\Gamma
  }{
    \kinding{\alpha}\kappa
  } 
  \qquad
  \Inf[\mathit{tapp}]{
    \kinding{\tau_1}{\kappa_2\to\kappa_1}
    \qquad
    \kinding{\tau_2}{\kappa_2}
  }{
    \kinding{\tau_1~\tau_2}{\kappa_1}
  }
  \qquad
  \Inf[\mathit{dt}]{
    \tupn{k}{\kinding\tau\kappa}
    \qquad
    (S^k:\tupn{k}\kappa\to\kappa')\in\Gamma
  }{
    \kinding{S^k~\tupn{k}\tau}{\kappa'}
  } 
  \\[2ex]
  \Inf[\mathit{timpl}]{
    \pikinding{\pi}
    \qquad
    \kinding\rho\star
  }{
    \kinding{\pi\To\rho}\star
  }
  \qquad
  \Inf[\mathit{tall}]{
    \kinding[\Gamma,\bvar\alpha{\kappa}]{\sigma}\star
    \qquad
    \alpha\not\in\Fv\Gamma
  }{
    \kinding{\forall\bvar\alpha{\kappa}.\sigma}\star
  } 
  \end{gather*}
  \\[2ex]

  \ruleform{\pikinding\pi} \\
  \begin{gather*}
     \Inf[\mathit{pred}]{
       \tupn{k}{\kinding\tau\kappa}
       \qquad
       (C:\tupn{k}\kappa\to\star)\in\Gamma
     }{
       \pikinding{C~\tupn{k}\tau}
     } 
     \qquad
     \Inf[\mathit{eq}]{
       \kinding{\tau_1}\kappa
       \qquad
       \kinding{\tau_2}\kappa
     }{
       \pikinding{\tau_1=\tau_2}
     } 
  \end{gather*}
  \\[2ex]

  \ruleform{\entails{\theta}} \\
  \begin{gather*}
    \Inf[\mathit{mono}]{
      \theta \in \Theta
    }{
      \entails{\theta}
    }
    \qquad
    \Inf[\mathit{param}]{
      \entails{\forall\bvar\alpha\kappa.\theta}
      \qquad
      \kinding{\tau}\kappa
    }{
      \entails{[\tau/\alpha]\theta}
    }
    \qquad
    \Inf[\mathit{mp}]{
      \entails{\pi \To \phi} \qquad \entails{\pi}
    }{
      \entails{\phi}
    }
    \qquad
    \Inf[\mathit{pcomp}]{
      \entails{C~\tup\tau}
      \qquad
      \tup{\entails{\tau=\tau'}}
    }{
      \entails{C~\tup{\tau'}}
    }    
    % -- equality axioms
    \\[2ex]
    \Inf[\mathit{eq_{refl}}]{
    }{
      \entails{\tau=\tau}
    }    
    \qquad
    \Inf[\mathit{eq_{symm}}]{
      \entails{\tau_2=\tau_1}
    }{
      \entails{\tau_1=\tau_2}
    }    
    \qquad
    \Inf[\mathit{eq_{trans}}]{
      \entails{\tau_1=\tau_2}\qquad\entails{\tau_2=\tau_3}
    }{
      \entails{\tau_1=\tau_3}
    }    
    \\[2ex]
    \Inf[\mathit{eq_{comp}}]{
      \entails{\tau_1=\tau_1'}
      \qquad
      \entails{\tau_2=\tau_2'}
    }{
      \entails{\tau_1~\tau_2=\tau_1'~\tau_2'}
    }    
    \qquad
    \Inf[\mathit{eq_{scomp}}]{
      \tup{\entails{\tau=\tau'}}
    }{
      \entails{S~\tup\tau=S~\tup{\tau'}}
    }    
  \end{gather*}

  \caption{Typing rules for expressions}
  \label{fig:typing}
\end{figure*}
%
\begin{figure*}[tpb]
  \centering
  %
  \ruleform{\typing[\Gamma]{cls}{\Theta,\Gamma}} \\
  \begin{gather*}
    \Inf[\mathit{cls}]{
      \Gamma'=\Gamma,\tup{\bvar\alpha\kappa}
      \qquad
      \tupn{n}{\pikinding[\Gamma']\pi}
      \qquad
      \kinding[\Gamma']\sigma\star
      \qquad
      \tup\alpha\supseteq\Fv\tup\pi
    }{
      \typing{
        \begin{array}{@{}l@{}}
          \class~\forall\tup{\bvar\alpha\kappa}.\tupn{n}{\pi}\To C~\tup\alpha~
          \where\\
          \quad{f::\sigma}
        \end{array}
      }{
        [\tupn{n}{\forall\tup{\bvar\alpha\kappa}.C~\tup\alpha\To\pi}],
        [C:\tup\kappa\to\star, 
         f:\forall\tup{\bvar\alpha\kappa}.C~\tup\alpha\To\sigma]
      }
    }
  \end{gather*}
  \\[2ex]
  %
  \ruleform{\typing[\Theta_t,\Theta_c,\Theta_i\mid\Gamma]{inst}{\Theta}} \\
  \begin{gather*}
    \Inf[\mathit{inst}]{
      \renewcommand{\arraystretch}{1.5}
      \begin{array}{c}
        \text{for each $\pi'$ where }
        (\forall\tup{\bvar\gamma{\kappa'}}.C~\tup\gamma\To\pi')
          \in\Theta_c\text{, we have }
        \entails[\Theta_t,\Theta_c,\Theta_i,\forall\tup{\bvar\alpha\kappa}.\tup\pi]{
          \forall\tup{\bvar\alpha\kappa}.[\tup\tau/\tup\gamma]\pi'}
        \\
        (C:\tup{\kappa'}\to\star)\in\Gamma
        \qquad
        \tup{\kinding\tau{\kappa'}}
        \\
        (f:\forall\tup{\bvar\beta{\kappa'}}.C~\tup\beta\To\sigma)\in\Gamma
        \qquad
        \typing[\Theta_t,\Theta_c,\Theta_i,\tup\pi\mid\Gamma,\tup{\alpha:\kappa}]{e}{
          [\tup\tau/\tup\beta]\sigma}
        \qquad
        \tup\alpha=\Fv\tup\tau\supseteq\Fv\tup\pi
      \end{array}
    }{
      \typing[\Theta_t,\Theta_c,\Theta_i\mid\Gamma]{
        \begin{array}{@{}l@{}}
          \instance~\forall\tup{\bvar\alpha\kappa}.\tup\pi\To C~\tup\tau~\where\\
          \quad{f=e}
        \end{array}
      }{
        [\forall\tup{\bvar\alpha\kappa}.\tup\pi\To C~\tup\tau]
      }
    }
  \end{gather*}
  \\[2ex]
  %
  \begin{gather*}
    \ruleform{\typing[\relax]{\mathit{tdec}}{\Gamma}} \\[2ex]
    \Inf[\mathit{tdec_{::}}]{
    }{
      \typing{
        (\type~S^k_{::}~\tupn{k}{\bvar\alpha{\kappa}} :: \kappa')
      }{
        [S^k_{::}:\tupn{k}\kappa\to\kappa']
      }
    }
    \qquad
    \Inf[\mathit{tdec_{:>}}]{
    }{
      \typing{
        (\type~S^k_{:>}~\tupn{k}{\bvar\alpha{\kappa}} :> \kappa')
      }{
        [S^k_{:>}:\tupn{k}\kappa\to\kappa']
      }
    }
  \end{gather*}
  \\[2ex]
  %
  \[
  \begin{matrix}
    \begin{gathered}
    \ruleform{\typing[\Gamma]{\mathit{tdef}}{\Theta}} \\[2ex]
    \Inf[\mathit{tdef}]{
      (S^k_\iota:\tupn{k}{\kappa_a}\to\kappa_r)\in\Gamma
      \qquad
      \tupn{k}{\kinding\tau{\kappa_a}}
      \qquad
      \kinding\xi{\kappa_r}
      \qquad
      \tup\alpha=\Fv\tupn{k}\tau\supseteq\Fv\xi
    }{
      \typing[\Gamma]{
        (\type~\forall\tup{\bvar\alpha\kappa}.S^k_\iota~\tupn{k}\tau=\xi)
      }{
        [\forall\tup{\bvar\alpha\kappa}.S^k_\iota~\tupn{k}\tau=\xi]
      }
    }
    \end{gathered}
    &\quad&
    \begin{gathered}
    \ruleform{\typing{\mathit{val}}{\Gamma}} \\[2ex]
    \Inf[\mathit{val}]{
      \typing{e}\sigma
    }{
      \typing{(x=e)}{[x:\sigma]}
    }
    \end{gathered}
  \end{matrix}
  \]
  \\[2ex]
  %
  \begin{gather*}
    \ruleform{\vdash{pgm}} \\[2ex]
    \Inf{
      \begin{array}{c}
        \Theta=\Theta_t,\Theta_c,\Theta_i
        \qquad
        \Gamma=\Gamma_t,\Gamma_c,\Gamma_v
        \\[.5ex]
        \tup{\typing[\relax]{\mathit{tdec}}{\Gamma_t}}
        \qquad
        \tup{\typing[\Gamma]{\mathit{tdef}}{\Theta_t}}
        \qquad
        \tup{\typing[\Gamma]{\mathit{cls}}{\Theta_c,\Gamma_c}}
        \qquad
        \tup{\typing[\Theta_t,\Theta_c,\Theta_i\mid\Gamma]{
            \mathit{inst}}{\Theta_i}}
        \qquad
        \tup{\typing{\mathit{val}}{\Gamma_v}}
      \end{array}
    }{
      \vdash \tup{\mathit{tdec}}; \tup{\mathit{tdef}}; \tup{\mathit{cls}}; 
      \tup{\mathit{inst}}; \tup{\mathit{val}}
    }
  \end{gather*}

  \caption{Typing rules for declarations}
  \label{fig:decl-typing}
\end{figure*}
%
Figures~\ref{fig:typing} and \ref{fig:decl-typing} present the typing rules
for our type system. Our formalisation is similar to
\cite{hall-etal:class-haskell} in that we maintain the context reduction rules
as part of the instance environment.  The main judgement has the conventional
form \(\typing{e}{\sigma}\) meaning ``in type environment $\Gamma$, and
instance environment $\Theta$, the term $e$ has type $\sigma$''.  Declarations
are typed by Figure~\ref{fig:decl-typing}, where all the rules are standard
for Haskell, except for the Rules~\rulename{tdec_{::}},~\rulename{tdec_{:>}},
and~\rulename{tdef}.

The instance environment $\Theta$ is a set of \emph{constraint schemes}
$\theta$ that hold in $e$.  A constraint scheme $\theta$ takes one of two
forms (Figure~\ref{fig:syntax}): it is either a \emph{class constraint scheme}
$\forall\tup\alpha.\phi$, or an \emph{equality scheme}
$\forall\tup\alpha.\pi_=$.  The instance environment is populated firstly by
class and instance declarations, which generate constraint schemes using the
rules of Figure~\ref{fig:decl-typing}; and secondly by moving underneath a
qualified type (Rule~\rulename{{\To}I} of Figure~\ref{fig:typing}).  The
latter adds only a \emph{simple constraint} $\pi$, which can be a \emph{class
  constraint} $\pi_c$ or an \emph{equality constraint} $\pi_=$; these simple
constraints are special cases of the two forms described earlier\footnote{Rule
  \rulename{{\To}I}, and the syntax of types, does not allow one to quantify
  over constraint \emph{schemes}, an orthogonal and interesting possible
  extension\cite{hinze-peyton-jones:deriv-class}.}.

The expression typing and constraint entailment rules of
Figures~\ref{fig:typing} are almost as for vanilla Haskell 98, with two major
differences.  The first is the addition of the Rule~\rulename{conv} that
enables typing an expression $e$ for which we derive a type $\tau_1$ also as
any other type $\tau_2$ for which we can derive that \(\tau_1=\tau_2\) from
the instance environment $\Theta$.  Intuitively, this means that we can
convert between $\tau_1$ and $\tau_2$ by using the equations defining type
functions as rewrite rules.

The second major difference is in the addition of the four
Rules~\rulename{eq_{refl}},~\rulename{eq_{symm}},~\rulename{eq_{trans}},
and~\rulename{eq_{subst}} in the constraint entailment judgement
\(\entails\theta\).  These rules are standard equality axioms used to derive
the type equalities used in the Rule~\rulename{conv} we just discussed.  The
last of the four rules allows equal types to be wrapped in an arbitrary
context: for example, if $\tau_2 = \tau_3$, then \<Tree\hsap (List\hsap
\tau_2) = Tree (List \tau_3)\>.

It is worthwhile to note that Rule~\rulename{sig} does not contain
well-formedness judgement, although it mentions a user-supplied type.  This
type is also produced by the typing judgement in the hypothesis, and the
judgement always produces well-formed types.  So, the rule will never apply to
a malformed type.

Much of this is standard for extensions of the Hindley-Milner system
with non-syntactic type
equality~\cite{remy:ml-eq-theory,neubauer-etal:funlog-overloading,
neuerbauer-thiemann:tc-ho-poly,odersky-etal:HMX,
xi-etal:guarded-datatypes,cheney-hinze:1st-class-phantom}.
Novel in our system is the integration of entailment of type class predicates
with type equalities.  In particular, our system allows equality schemes, such
as
%
\begin{haskell}
  \forall{}a. Sprintf (I a) = Int \to Sprintf a
\end{haskell}
%
in the constraint context $\Theta$ of the typing rules.  Equality schemes are
introduced by Rule~\rulename{tdef} of the declaration typing rules from
Figure~\ref{fig:decl-typing}.  This rule turns the definitions of type
equations into equality schemes, such as the \<Sprintf\> scheme above, which
are used in the inference rules of judgement \(\entails{\theta}\) from
Figure~\ref{fig:typing}.  Moreover, user-supplied signatures, as well as those
signatures inferred in Section~\ref{sec:inference}, can contain equalities in
constraint contexts.


\section{Type Preserving Translation}
\label{sec:translation}

% ---------------------------- Translation rules ----------
\begin{figure*}[tbp]
\small
  \centering
  \renewcommand{\arraystretch}{3}
  \ruleform{\ttyping{e}w{\sigma}} \\
  \begin{gather*}
    \Inf[\mathit{var}]{
      (x:\sigma)\in\Gamma
    }{
      \ttyping{x}x{\sigma}
    }
    \qquad
    \Inf[\mathit{conv}]{
      \ttyping{e}w{\tau_1}
      \qquad 
      \ttyeq{\tau_1}{\tau_2}{\gamma}
    }{
      \ttyping{e}{(\cast{w}{\gamma})}{\tau_2}
    }
    \\[2ex]
    %
    \Inf[\mathit{let}]{
      \ttyping[\Theta_1\mid\Gamma]{e_1}{w_1}{\sigma_1} 
      \qquad 
      \ttyping[\Theta_2\mid\Gamma{[x:\sigma_1]}]{e_2}{w_2}{\sigma_2}
      \qquad
      \tkinding{\sigma_1}{\nu_1}\star
    }{
      \ttyping[\Theta_1,\Theta_2\mid\Gamma]{(\letin{x}{e_1}{e_2})}{%
        (\letin{\bvar{x}{\nu_1}}{w_1}{w_2})
      }{\sigma_2}
    }
    \\[2ex]
    %
    \Inf[{\to}I]{
      \ttyping[\Theta\mid\Gamma,x:\tau_1]{e_2}{w_2}{\tau_2} 
      \qquad 
      \tkinding{\tau_1}{\nu_1}\star
    }{
      \ttyping{\lambda x.e_2}{\lambda\bvar{x}{\nu_1}.w_2}{\tau_1\to\tau_2}
    }
    \qquad
    \Inf[{\to}E]{
      \ttyping{e_1}{w_1}{\tau_2\to\tau_1} 
      \qquad 
      \ttyping{e_2}{w_2}{\tau_2}
    }{
      \ttyping{e_1~e_2}{w_1~w_2}{\tau_1}
    }
    \\[2ex]
    %
    \Inf[{\To}I_c]{
      \ttyping[\Theta,d:C~\tup\tau\mid\Gamma]{e}w{\rho}
      \qquad
      \tpikinding{C~\tup\tau}\nu
    }{
      \ttyping{e}{\lambda\bvar{d}\nu.w}{C~\tup\tau\To\rho}
    }
    \qquad
    \Inf[{\To}E_c]{
      \ttyping{e}{w_1}{C~\tup\tau\To\rho} 
      \qquad 
      \tentails{C~\tup\tau}{w_2}
    }{
      \ttyping{e}{w_1~w_2}{\rho}
    }
    \\[2ex]
    %
    \Inf[{\To}I_=]{
      \ttyping[\Theta,c:(\tau_1=\tau_2)\mid\Gamma]{e}w{\rho}
      \qquad
      \tpikinding{\tau_1=\tau_2}{\kappa}
    }{
      \ttyping{e}{\Lambda\bvar{c}\kappa.w}{(\tau_1=\tau_2)\To\rho}
    }
    \qquad
    \Inf[{\To}E_=]{
      \ttyping{e}{w}{(\tau_1=\tau_2)\To\rho} 
      \qquad 
      \tentails{\tau_1=\tau_2}\gamma
    }{
      \ttyping{e}{w~\gamma}{\rho}
    }
    \\[2ex]
    %
    \Inf[{\forall}I]{
      \ttyping[\Theta\mid\Gamma,\bvar\alpha\kappa]{e}w{\sigma} 
      \qquad 
      \alpha\not\in\Fv\Theta\cup\Fv\Gamma
    }{
      \ttyping{e}{\Lambda\bvar\alpha\kappa.w}{\forall\bvar\alpha\kappa.\sigma}
    }
    \qquad
    \Inf[{\forall}E]{
      \ttyping{e}w{\forall\bvar\alpha\kappa.\sigma} 
      \qquad 
      \tkinding{\tau}\nu\kappa
    }{
      \ttyping{e}{w~\nu}{[\tau/\alpha]\sigma}
    }
    \\[2ex]
    %
    \Inf[\mathit{sig}]{
      \ttyping{e}w{\sigma}
      \qquad
      \Fv\sigma=\emptyset
    }{
      \ttyping{(e::\sigma)}w{\sigma}
    }
  \end{gather*} \\[3ex]

  \ruleform{\tkinding\sigma\nu\kappa} \\
  \begin{gather*}
  \Inf[\mathit{tcon}]{
    (T:\kappa)\in\Gamma
  }{
    \tkinding{T}T\kappa
  } 
  \qquad
  \Inf[\mathit{tvar}]{
    (\alpha:\kappa)\in\Gamma
  }{
    \tkinding{\alpha}\alpha\kappa
  } 
  \qquad
  \Inf[\mathit{tapp}]{
    \tkinding{\tau_1}{\nu_1}{\kappa_2\to\kappa_1}
    \qquad
    \tkinding{\tau_2}{\nu_2}{\kappa_2}
  }{
    \tkinding{\tau_1~\tau_2}{\nu_1~\nu_2}{\kappa_1}
  }
  \\[2ex]
  \Inf[\mathit{dt}]{
    \tupn{k}{\tkinding\tau\nu\kappa}
    \qquad
    (S^k:\tupn{k}\kappa\to\kappa')\in\Gamma
  }{
    \tkinding{S^k~\tupn{k}\tau}{S^k~\tupn{k}\nu}{\kappa'}
  } 
  \qquad
  \Inf[\mathit{timpl}]{
    \tpikinding{\pi}{\nu_1}
    \qquad
    \tkinding\rho{\nu_2}\star
  }{
    \tkinding{\pi\To\rho}{\nu_1\to\nu_2}\star
  }
  \qquad
  \Inf[\mathit{tall}]{
    \tkinding[\Gamma,\bvar\alpha{\kappa}]{\sigma}\nu\star
    \qquad
    \alpha\not\in\Fv\Gamma
  }{
    \tkinding{\forall\bvar\alpha{\kappa}.\sigma}{%
      \forall\bvar\alpha{\kappa}.\nu}\star
  } 
  \end{gather*}
  \\[3ex]

  \[
  \begin{matrix}
  \begin{gathered}
     \ruleform{\tpikinding{\pi_c}\nu} \\
     \Inf[\mathit{pred}]{
       \tupn{k}{\tkinding\tau\nu\kappa}
       \qquad
       (C:\tupn{k}\kappa\to\star)\in\Gamma
     }{
       \tpikinding{C~\tupn{k}\tau}{C~\tupn{k}\nu}
     } 
   \end{gathered}
   &\qquad&
   \begin{gathered}
     \ruleform{\tpikinding{\pi_=}\kappa} \\
     \Inf[\mathit{eq}]{
       \tkinding{\tau_1}{\nu_1}\kappa
       \qquad
       \tkinding{\tau_2}{\nu_2}\kappa
     }{
       \tpikinding{\tau_1=\tau_2}{\eqc{\nu_1}{\nu_2}}
     } 
  \end{gathered}
  \end{matrix}
  \]
  \\[3ex]

  \ruleform{\tentails{(\forall\tup{\bvar\alpha\kappa}.\,\phi)}w} \\
  \begin{gather*}
    \Inf[\mathit{mono}]{
      (d:\theta)\in\Theta
    }{
      \tentails{\theta}d
    }
    \qquad
    \Inf[\mathit{param}]{
      \tentails{\forall\bvar\alpha\kappa.\theta}w
      \qquad
      \tkinding{\tau}\nu\kappa
    }{
      \tentails{[\tau/\alpha]\theta}{w~\nu}
    }
    \qquad
    \Inf[\mathit{mp}]{
      \tentails{\pi \To \phi}{w_1} 
      \qquad 
      \tentails{\pi}{w_2}
    }{
      \tentails{\phi}{w_1~w_2}
    }
    \\[2ex]
    \Inf[\mathit{subst}]{
      \tentails{C~\tup\tau}w
      \qquad
      \tup{\tentails{\tau=\tau'}\gamma}
    }{
      \tentails{C~\tup{\tau'}}{(\cast{w}{C~\tup\gamma})}
    }    
  \end{gather*}
  \\[3ex]

  \ruleform{\tentails{(\forall\tup{\bvar\alpha\kappa}.\,\pi_=)}\gamma}
  \\
  \begin{gather*}
    \Inf[\mathit{eq_{mono}}]{
      (c:\theta)\in\Theta
    }{
      \tentails{\theta}c
    }
    \qquad
    \Inf[\mathit{eq_{param}}]{
      \tentails{\forall\bvar\alpha\kappa.\theta}\gamma
      \qquad
      \tkinding{\tau}\nu\kappa
    }{
      \tentails{[\tau/\alpha]\theta}{\inst\gamma\nu}
    }
    \\[2ex]
    \Inf[\mathit{eq_{refl}}]{
    }{
      \tentails{\tau=\tau}{\tau}
    }    
    \qquad
    \Inf[\mathit{eq_{symm}}]{
      \tentails{\tau_2=\tau_1}\gamma
    }{
      \tentails{\tau_1=\tau_2}{\sym\gamma}
    }    
    \qquad
    \Inf[\mathit{eq_{trans}}]{
      \tentails{\tau_1=\tau_2}{\gamma_1}
      \qquad
      \tentails{\tau_2=\tau_3}{\gamma_2}
    }{
      \tentails{\tau_1=\tau_3}{\trans{\gamma_1}{\gamma_2}}
    }    
    \\[2ex]
    \Inf[\mathit{eq_{comp}}]{
      \tentails{\tau_1=\tau_1'}{\gamma_1}
      \qquad
      \tentails{\tau_2=\tau_2'}{\gamma_2}
    }{
      \tentails{\tau_1~\tau_2=\tau_1'~\tau_2'}{\gamma_1~\gamma_2}
    }
    \qquad
    \Inf[\mathit{eq_{scomp}}]{
      \tup{\tentails{\tau=\tau'}{\gamma}}
    }{
      \tentails{S~\tup\tau=S~\tup{\tau'}}{S_n~\tup\gamma}
    }    
  \end{gather*}

  \caption{Translation rules for expressions and types}
  \label{fig:expr-trans}
\end{figure*}
%
\begin{figure*}[tpb]
  \centering
  %
  \ruleform{\ttyping[\Gamma]{\mathit{cls}}{\mathit{td}}{\Theta,\Gamma}} \\
  \begin{gather*}
    \Inf[\mathit{cls}]{
      \Gamma'=\Gamma,\tup{\bvar\alpha\kappa}
      \qquad
      \tupn{n}{\pikinding[\Gamma']\pi}
      \qquad
      \tkinding[\Gamma']\sigma\nu\star
      \qquad
      \tup\alpha\supseteq\Fv\tup\pi
    }{
      \ttyping{
        \begin{array}{@{}l@{}}
          \class~\forall\tup{\bvar\alpha\kappa}.\tupn{n}{\pi}\To C~\tup\alpha~
          \where\\
          \quad{}f::\sigma
        \end{array}
      }{
        \begin{array}{@{}l@{}}
          \data~C:\tup\kappa\to\star~
          \where\\
          \quad{}K_C:\forall\tup{\bvar\alpha\kappa}.\nu\to C~\tup\alpha
          \\[.7ex]
          f:(\forall\tup{\bvar\alpha\kappa}.C~\tup\alpha\to\nu) =\\
          \quad\Lambda\tup{\bvar\alpha\kappa}.\lambda\bvar{x}{C~\tup\alpha}.\\
          \qquad\caseof{x}{K_C~f_0 \to f_0}
        \end{array}
      }{
        [\tupn{n}{\forall\tup{\bvar\alpha\kappa}.C~\tup\alpha\To\pi}],
        [C:\tup\kappa\to\star, 
         f:\forall\tup{\bvar\alpha\kappa}.C~\tup\alpha\To\sigma]
      }
    }
  \end{gather*}
  \\[2ex]
  %
  \ruleform{\ttyping[\Theta_t,\Theta_c,\Theta_i\mid\Gamma]{%
      \mathit{inst}}{\mathit{td}}{\Theta}} \\
  \begin{gather*}
    \Inf[\mathit{inst}]{
      \renewcommand{\arraystretch}{1.5}
      \begin{array}{c}
        \text{for each $\pi'$ where }
        (\forall\tup{\bvar\gamma{\kappa'}}.C~\tup\gamma\To\pi)
          \in\Theta_c\text{, we have }
        \entails[\Theta_t,\Theta_c,\Theta_i,%
          \forall\tupn{k}{\bvar\alpha\kappa}.\tup{\pi_=},%
          \forall\tupn{k}{\bvar\alpha\kappa}.\tup{\pi_c}]{
          \forall\tupn{k}{\bvar\alpha\kappa}.
            [\tup\tau/\tup\gamma]\pi}
        \\
        (C:\tup{\kappa'}\to\star)\in\Gamma
        \qquad
        \tup{\tkinding\tau\nu{\kappa'}}
        \qquad
        \tup{\tpikinding{\pi_=}{\kappa_=}}
        \qquad
        \tup{\tpikinding{\pi_c}\upsilon}
        \qquad
        \tup\alpha=\Fv\tup\tau\supseteq\Fv\tupn{n}\pi
        \\
        (f:\forall\tup{\bvar\beta{\kappa'}}.C~\tup\beta\To\sigma)\in\Gamma
        \qquad
         \ttyping[\Theta_t,\Theta_c,\Theta_i,\tup{c:\pi_=},\tup{d_c:\pi_c}%
           \mid\Gamma,\tupn{k}{\alpha:\kappa}]{e}w{%
           [\tup\tau/\tup\beta]\sigma}
%         \ttyping[\Theta_t,\Theta_c,\Theta_i\mid\Gamma]{e}{(\tupn{k+n}\Pi).w}{%
%           (\forall\tupn{k}{\bvar\alpha\kappa}.\tupn{n}\pi\To
%           [\tup\tau/\tup\beta]\sigma)}
%         \ttyping[\Theta_t,\Theta_c,\Theta_i\mid\Gamma]{e}{%
%           (\Lambda\tupn{k}{\bvar\alpha\kappa}.
%           \Lambda\tupn{n_1}{\bvar{c}\upsilon}.
%           \lambda\tupn{n_2}{\bvar{d}\upsilon}.w)}{%
%           (\forall\tupn{k}{\bvar\alpha\kappa}.\tupn{n}\pi\To
%           [\tup\tau/\tup\beta]\sigma)}
        \qquad
        d\text{ fresh}
      \end{array}
    }{
      \ttyping[\Theta_t,\Theta_c,\Theta_i\mid\Gamma]{
        \begin{array}{@{}l@{}}
          \instance~\forall\tupn{k}{\bvar\alpha\kappa}.
          (\tup{\pi_=},\tup{\pi_c}) \To C~\tup\tau~
          \where\\
          \quad{f=e}
        \end{array}
      }{
        \begin{array}{@{}l@{}}
          d : 
            (\forall\tupn{k}{\bvar\alpha\kappa}.
              \tup{\kappa_=}\To\tup\upsilon\to C~\tup\nu) =\\
            \quad
            \Lambda\tupn{k}{\bvar\alpha\kappa}.
            \Lambda\tup{\bvar{c}{\kappa_=}}.
            \lambda\tup{\bvar{d_c}\upsilon}.
%            (\tupn{k+n}\Pi).
            K_C~\tup\nu~w
        \end{array}
      }{
        [d:\forall\tupn{k}{\bvar\alpha\kappa}.(\tup{\pi_=},\tup{\pi_c})\To 
          C~\tup\tau]
      }
    }
  \end{gather*}
  \\[2ex]
  %
  \begin{gather*}
    \ruleform{\ttyping[\relax]{\mathit{tdec}}{\mathit{td}}{\Gamma}}
    \\[2ex]
    \Inf[\mathit{tdec_{::}}]{
    }{
      \ttyping{
        (\type~S^k_{::}~\tupn{k}{\bvar\alpha{\kappa}} :: \kappa')
      }{
        (\type~S^k_{::}:\tupn{k}\kappa\to\kappa')
      }{
        [S^k_{::}:\tupn{k}\kappa\to\kappa']
      }
    }
    \\[2ex]
    %
    \Inf[\mathit{tdec_{:>}}]{
    }{
      \ttyping{
        (\type~S^k_{:>}~\tupn{k}{\bvar\alpha{\kappa}} :> \kappa')
      }{
        (\type~S^k_{:>}:\tupn{k}\kappa\to\kappa')
      }{
        [S^k_{:>}:\tupn{k}\kappa\to\kappa']
      }
    }
  \end{gather*}
  \\[2ex]
  %
  \begin{gather*}
    \ruleform{\ttyping[\Gamma]{\mathit{tdef}}{\mathit{td}}{\Theta}} 
    \\[2ex]
    \Inf[\mathit{tdef}]{
      (S^k_\iota:\tupn{k}{\kappa_a}\to\kappa_r)\in\Gamma
      \qquad
      \tupn{k}{\tkinding\tau\nu{\kappa_a}}
      \qquad
      \tkinding\xi\upsilon{\kappa_r}
      \qquad
      \tup\alpha=\Fv\tupn{k}\tau\supseteq\Fv\xi
      \qquad
      k\text{ fresh}
    }{
      \ttyping[\Gamma]{
        (\type~\forall\tup{\bvar\alpha\kappa}.S^k_\iota~\tupn{k}\tau=\xi)
      }{
        (\coercion~k:
          \eqc{(\forall\tup{\bvar\alpha\kappa}.S^k_\iota~\tupn{k}\nu)}{%
            (\forall\tup{\bvar\alpha\kappa}.\upsilon)})
      }{
        [k:\forall\tup{\bvar\alpha\kappa}.S^k_\iota~\tupn{k}\tau=\xi]
      }
    }
  \end{gather*}
  \\[2ex]
  %
  \begin{gather*}
    \ruleform{\ttyping{\mathit{val}}{\mathit{td}}{\Gamma}} \\[2ex]
    \Inf[\mathit{val}]{
      \ttyping{e}w\sigma
      \qquad
      \tkinding\sigma\nu\star
    }{
      \ttyping{(x=e)}{(x:\nu=w)}{[x:\sigma]}
    }
  \end{gather*}
  \\[2ex]
  %
  \begin{gather*}
    \ruleform{\vdash\mathit{pgm}\leadsto\tup{\mathit{td}}} \\[2ex]
    \Inf{
      \begin{array}{c}
        \Theta=\Theta_t,\Theta_c,\Theta_i
        \quad
        \Gamma=\Gamma_t,\Gamma_c,\Gamma_v
        \\[.5ex]
        \tup{\ttyping[\relax]{\mathit{tdec}}{d_t}{\Gamma_t}}
        \quad
        \tup{\ttyping[\Gamma]{\mathit{tdef}}{d_o}{\Theta_t}}
        \quad
        \tup{\ttyping[\Gamma]{\mathit{cls}}{d_c}{\Theta_c,\Gamma_c}}
        \quad
        \tup{\ttyping[\Theta_t,\Theta_c,\Theta_i\mid\Gamma]{
            \mathit{inst}}{d_i}{\Theta_i}}
        \quad
        \tup{\ttyping{\mathit{val}}{d_v}{\Gamma_v}}
      \end{array}
    }{
      \vdash \tup{\mathit{tdec}}; \tup{\mathit{tdef}}; \tup{\mathit{cls}}; 
      \tup{\mathit{inst}}; \tup{\mathit{val}} 
      \leadsto \tup{d_c}; \tup{d_i}; \tup{d_t}; \tup{d_o}; \tup{d_v}
    }
  \end{gather*}

  \caption{Translation rules for declarations}
  \label{fig:decl-trans}
\end{figure*}
%
\TODO{Need to introduce \FC\ somewhere.}  The translation of source types,
expressions, and declarations into \FC\ is type-directed, and hence, realised
by augmenting the typing rules, as shown in Figures~\ref{fig:expr-trans}
and~\ref{fig:decl-trans}.  The bulk of the translation follows the standard
approach for Haskell, as for example explained by Hall et
al.~\cite{hall-etal:class-haskell}.  

\TODO{Need some examples with the following explanations.}

\subsection{Translation of types and expressions}

The translation of type functions adds to this standard scheme for expressions
and types (Figure~\ref{fig:expr-trans}) in three interesting ways.  Firstly,
the translated term in the conversion rule~\rulename{conv} includes a cast of
the form \<\cast{e}\gamma\> where the witnessing coercion $\gamma$ is produced
by a translating variant of constraint entailment for equalities
\(\ttyeq{\tau_1}{\tau_2}{\gamma}\), which leads to the second difference.

Secondly, the judgement \(\entails\theta\) from Figure~\ref{fig:typing} splits
into two judgements: one to generate witnesses for class predicates
\(\tentails{(\forall\tup{\bvar\alpha\kappa}.\,\phi)}w\) and one to generate
witnesses for equalities
\(\tentails{(\forall\tup{\bvar\alpha\kappa}.\,\pi_=)}\gamma\).  This
distinction is fundamental as witnesses for class predicates, often called
\emph{class dictionaries}, are computational \FC\ terms, whereas witnesses for
equalities are \FC\ coercions; i.e., types of a particular kind.  Intuitively,
we can justify this setup by observing that class dictionaries influence the
dynamic semantics of the generated program, whereas coercions merely serve to
enable decidable type checking of \FC\ programs---hence, they are a purely
static artifact with now runtime effect whatsoever.  We get a similar split
for the constraint well-formedness judgement \(\pikinding\pi\).

Thirdly, that class predicates translate to computational \FC\ terms realising
class dictionaries and equalities translate to \FC\ coercions, requires to
split the constraint context introduction and elimination
rules~\rulename{{\To}I} and~\rulename{{\To}E} into two rules each; one for
each flavour of constraint.  In particular, the translated terms need to use
value abstraction and application for class predicates and type abstraction
and application for equalities.

\subsection{Translation of declarations}

The translation of class declarations by Rule~\rulename{cls} is identical to
the case of vanilla type classes.  More interesting is the translation of
instance declarations by Rule~\rulename{inst}.  It gets more involved by the
presence of equalities \(\tup{\pi_=}\) in instance contexts.  These equalities
translate to coercion kinds \(\tup{\kappa_=}\) that require additional type
abstractions in the dictionary function $d$.  To simplify the notation,
Rule~\rulename{inst} assume w.l.o.g. that the instance context has all
equalities first, followed by the class predicates.  Otherwise, the rule
follows that of vanilla type classes.

The second addition to declaration translation is the translation of type
function declarations and type equation definitions.  Both translate into the
quite closely corresponding declarations of abstract type constructors and
toplevel coercions in \FC.


\section{Type Inference}
\label{sec:inference}

The presence of the typing rule~\rulename{conv} and related extensions of
constraint entailment with equality axioms has a significant impact on type
inference.  Firstly, we need to normalise type terms involving type functions
according to the available type equations.  Secondly, as type terms involving
type variables often cannot be fully normalised until some type variables are
further instantiated, we need to extend the standard definition of unification
in the Hindley-Milner system to return partially-solved equality constraints
in addition to a substitution.

To illustrate this, reconsider the definition of the class \<Collects\> with
type function \<Elem\> from Section~\ref{sec:intro}.  The unification problem
\<(Int, a) = (Elem c, Bool)\> implies the substitution \([Bool/a]\), but also
the additional constraint \<Int = Elem\hsap c\>.  We cannot decide whether the
latter constraint is valid without knowing more about \(c\), so we call such
constraints \emph{pending equality constraints.}  In the presence of general
type functions, the type inference algorithm has to maintain pending equality
constraints together with class predicates.

In this section, after fixing some constraints on source programs, we will
first discuss a variant of Hindley-Milner type inference with predicates,
based on our earlier work~\cite{chak-etal:at-syns}.  The inference algorithm
depends on a unification procedure that includes type normalisation
(Section~\ref{sect:unification}).  Afterwards, we will use the unification
procedure to test the subsumption relation of type schemes
(Section~\ref{sect:subsumption}).  We conclude the section with some formal
properties of our inference system with type functions.

\subsection{Well-formed programs}

To achieve \emph{decidable} type inference, we impose the following
restrictions on source programs:
%
\begin{itemize}
\item Instance heads must be constructor-based---i.e., type arguments may only
  contain variables and data constructors, type functions are not permitted.
\item Instance contexts must be decreasing---i.e., (a) no variable has more
  occurrences in the context than in the head and (b) the context has fewer
  constructors and variables (taken together and counting repetitions) than
  the head.
\item The left-hand sides of all type equations must be constructors-based.
  Furthermore, the right-hand sides of injective type equations must be
  constructor-based.
\item Type equations must be non-overlapping.  That is, for any two equations
  \<S\hsap \tau_1 \cdots \tau_n = \tau\> and \<S\hsap \tau'_1 \cdots \tau'_n =
  \tau'\>, there may be no substitution $R$ with \<R(S \tau_1 \cdots \tau_n) =
  R(S \tau'_1 \cdots \tau'_n)\>.  Furthermore, if $R$ is injective, there may
  be no substitution $R$ with \<R\tau = R\tau'\>.  \manuel{We could relax this
    to allow overlap, if the rhses (resp.\ lhses) coincide under the
    substitution $R$, possibly after reducing all type applications as far as
    possible.}
\end{itemize}
%
Strictly speaking, these restrictions are tighter than required to achieve
decidable type inference.  This is so that it is easy for both the compiler
and programmer to check whether a program obeys the restrictions.

A program that meets all of the listed constraints is \emph{well-formed}.  The
declaration typing rules of Figure~\ref{fig:decl-typing} determine, for a
given program, the validity of a \emph{program context} $\Theta_P$ and typing
environment $\Gamma$.  Both are inputs to type inference for expressions and,
if they are without superfluous elements, we call them well-formed.

For the rest of the paper, we confine ourselves to well-formed programs and
program contexts.  This in particular means that the rewrite system implied by
the equality schemes in a program context $\Theta_P$ is confluent and
terminating.

\iffalse
\TODO{This is still old!!!}

\subsection{Type inference}

\begin{figure*}[tbp]
  \centering
  \renewcommand{\arraystretch}{3}
  \ruleform{\tinf[\Theta,U\mid{T}\Gamma]{e}{\tau}} \\
  \begin{gather*}
    \Inf[\mathit{var}_W]{
      (x:\forall\tup{\alpha}.\tup\pi\To\tau)\in\Gamma 
      \qquad 
      \tup{\beta}\text{ fresh}
    }{
      \tinf[{[\tup{\beta}/\tup{\alpha}]}\tup\pi\mid\Gamma]{x}{%
        [\tup{\beta}/\tup{\alpha}]\tau}
    }
    \\[2ex]
    %
    \Inf[{\to}E_W]{
      \tinf[\Theta_1,U_1\mid{T_1}\Gamma]{e_1}{\tau_1}
      \qquad 
      \tinf[\Theta_2,U_2\mid{T_2}(T_1\Gamma)]{e_2}{\tau_2}
      \qquad\mskip-6mu
      \begin{gathered}[b]
        \alpha\text{ fresh}
        \\[-1ex]
        \unifsimplto[\Theta_P]{%
          U_1,U_2,(\tunify{T_2\tau_1}\relax{\tau_2\to\alpha})}{U;R}
      \end{gathered}
    }{
      \tinf[R(T_2\Theta_1,\Theta_2),U\mid(RT_2T_1)\Gamma]{e_1~e_2}{R\alpha}
    }
    \\[2ex]
    %
    \Inf[{\to}I_W]{
      \tinf[\Theta,U\mid{T}\Gamma{[x:\alpha]}]{e}\tau 
      \qquad 
      \alpha\text{ fresh}
    }{
      \tinf{\lambda x.e}{T\alpha\to\tau}
    }
    \\[2ex]
    %
    \Inf[\mathit{let}_W]{
      \tinf[\Theta_1,U_1\mid{T_1}\Gamma]{e_1}{\tau_1}
      \qquad
      \tinf[\Theta_2,U_2\mid{T_2}({T_1}\Gamma{[x:\sigma]})]{e_2}{\tau_2}
      \qquad
      \sigma=\Gen{T_1\Gamma}{(\Theta_1,U_1)\To\tau_1}
%      \qquad
%      T_2U_1\cup U_2\simplifiesto UR
    }{
      \tinf[\Theta_2,U_2\mid{(T_2T_1)}\Gamma]{(\letin{x}{e_1}{e_2})}{\tau_2}
    }
    \\[2ex]
    %
    \Inf[\mathit{sig}_W]{
      \tinf{e}{\tau_1}
      \qquad
      \sigma=\Gen{T\Gamma}{(\Theta,U)\To\tau_1}
      \qquad 
      \subsumes\sigma{(\forall\tup\alpha.\tup\pi\To\tau_2)}
      \qquad\mskip-20mu
      \begin{gathered}[b]
        \tup\beta\text{ fresh}
        \\[-1ex]
        \Fv{(\tup\pi\To\tau_2)}\subseteq\tup\alpha
      \end{gathered}
    }{
      \tinf[{[\tup\beta/\tup\alpha]}\tup\pi\mid{T\Gamma}]{%
        (e::\forall\tup\alpha.\tup\pi\To\tau_2)
      }{%
        [\tup\beta/\tup\alpha]\tau_2
      }
    }
    \\[5ex]
    %
    \Gen{\Gamma}{\rho}=\forall\tup\alpha.\rho
    \qquad\text{, where }
    \begin{aligned}[t]
      \tup\alpha&=\Fv\rho\setminus\Fv\Gamma
    \end{aligned}
  \end{gather*}
  \caption{Type inference rules}
  \label{fig:inference}
\end{figure*}
%
We begin with type inference for type classes with associated types.
Figure~\ref{fig:inference} displays the rules for the inference judgement
\(\tinf{e}\tau\).  Given a type environment $\Gamma$ and an expression $e$ as
inputs, it computes the following outputs (1) a set of class constraints
$\Theta$, (2) a set of pending equality constraints $U$, (3) a substitution
$T$, and (4) a monotype $\tau$.  The judgement implicitly also depends on the
program context $\Theta_P$, 
initially populated by the instance declarations and remains constant
thereafter.  Because $\class$ and $\instance$ declarations are, in effect,
explicitly typed, their type inference rules are extremely similar to those in
Figure~\ref{fig:decl-typing}; so, we do not give them separately here.

Our inference rules generalise the standard rules for Haskell in two ways:
(1) the inference rules maintain a set of equality constraints
$U$ and (2) unification produces a set of pending equality constraints in
addition to a substitution.  Let us look at both aspects in some more detail.

Type inference for Haskell needs to maintain a set of $\Theta$ of constraints,
called the \emph{constraint context.}  In Haskell 98, the constraint context
is a set of type class predicates.  We extend the context to also include
equality constraints, just as in the typing rules.  However, as we need to
treat these two kinds of constraints differently during the inference process,
we partition the overall context into the two subsets $\Theta$ and $U$
denoting the class constraints and equality constraints, respectively.  Hence,
the phrase \(\Theta,U\) to the left of the vertical bar in the inference
judgement captures the whole context.  In particular, Rules~\rulename{var_W}
and~\rulename{sig_W} result in contexts \([\tup\beta/\tup\alpha]\tup\pi\),
which are implicitly partitioned into the two components $\Theta$ and $U$ in
the hypotheses of other inference rules.  During generalisation by the
function \(\Gen\Gamma\rho\) in Rule~\rulename{let_W} and~\rulename{sig_W},
both class and equality constraints are moved into the signature context of
the produced signature.

In Rule~\rulename{{\to}E_W}, the two sets of equality constraints $U_1$ and
$U_2$ are both extracted out of the constraint context, to be fed to the
unification process in conjunction with the new equality constraint
\(T_2\tau_1 = \tau_2\to\alpha\).  Unification simplifies the equalities as far
as possible, producing, in addition to a substitution $R$, a set of pending
equality constraints $U$.  This set is used in the conclusion of the inference
rule.

Rules~\rulename{{\to}E_W} and~\rulename{sig_W} make use of two auxiliary
judgements for unification and subsumption, respectively.  Both of these
judgements depend on the program context $\Theta_P$ and are the subject of the
following two subsections.

\subsection{Unification} \label{sect:unification}

\begin{figure*}[tbp]
  \centering
  \renewcommand{\arraystretch}{3}
  %
% Old style
%  \ruleform{\normal{\tau_1}{\tau_2}}
%  \begin{gather*}
%    \Inf[\meta{con}_R]{}{
%      \normal[\cdot]TT
%    }
%    \qquad
%    \Inf[\meta{var}_R]{}{
%      \normal[\cdot]\alpha\alpha
%    }
%    \qquad
%    \Inf[\meta{app}_R]{
%      \normal[\Theta_i]{\tau_i}{\tau_i'}
%    }{
%      \normal[\Theta_1,\Theta_2]{\tau_1~\tau_2}{\tau_1'~\tau_2'}
%    }
%    \\[2ex]
%% Big step semantics:
%%    \Inf[\meta{syn}_R]{
%%      \tup{\normal[\Theta_1]{\tau}{[\tup\alpha/\tup\xi]\tau'}}
%%      \qquad
%%      (\forall\tup\alpha.S~\tup{\tau'}=\tau)\in\Theta
%%      \qquad
%%      \normal[\Theta_2]{[\tup\alpha/\tup\xi]\tau}{\tau'}
%%    }{
%%      \normal[\tup{\Theta_1},\Theta_2,{[\tup\alpha/\tup\xi]}\tup\pi]{
%%        (S~\tup\tau)
%%      }{
%%        \tau'
%%      }
%%    }
%    \Inf[\meta{arg}_R]{
%      \tup{\normal{\tau}{\tau'}}
%    }{
%      \normal[\tup\Theta]{S~\tup\tau}{S~\tup{\tau'}}
%    }
%    \qquad
%    \Inf[\meta{red}_R]{
%      (\forall\tup\alpha.\tup\pi\To(\eta=\tau))\in\Theta_P
%    }{
%      \normal[{[\tup\alpha/\tup\xi]}\tup\pi]{
%        [\tup\alpha/\tup\xi]\eta
%      }{
%        [\tup\alpha/\tup\xi]\tau
%      }
%    }
%  \end{gather*}
  %
  \ruleform{\tred{\tau}{\tau'}}
  \begin{gather*}
    \Inf[\meta{lapp}_R]{
      \tred{\tau_1}{\tau_1'}
    }{
      \tred{\tau_1~\tau_2}{\tau_1'~\tau_2}
    }
    \qquad
    \Inf[\meta{rapp}_R]{
      \tred{\tau_2}{\tau_2'}
    }{
      \tred{\tau_1~\tau_2}{\tau_1~\tau_2'}
    }
    \\[2ex]
    \Inf[\meta{arg}_R]{
      1\leq i\leq k
      \qquad
      \tred{\tau_i}{\tau'_i}
      \qquad
      \tau_j'=\tau_j, \forall j\neq i
    }{
      \tred{S^k~\tupn{k}\tau}{S^k~\tupn{k}{\tau'}}
    }
    \qquad
    \Inf[\meta{syn}_R]{
      (\forall\tup\alpha.\eta=\tau)\in\Theta
    }{
      \tred{
        [\tup\xi/\tup\alpha]\eta
      }{
        [\tup\xi/\tup\alpha]\tau
      }
    }
  \end{gather*}

  \medskip
  \ruleform{\unifsimpl{\tau_1=\tau_2}{U;R}}\\
  \begin{gather*}
    \Inf[\mathit{refl}_U]{}{
      \unifsimpl{\tau=\tau}{\bullet;\bullet}
    }
    \qquad
    \Inf[\mathit{symm}_U]{
      \unifsimpl{\tau_2=\tau_1}{U;R}
    }{
      \unifsimpl{\tau_1=\tau_2}{U;R}
    }
    \qquad
    \Inf[\mathit{var}_U]{
      \alpha\not\in\Fv\tau
    }{
      \unifsimpl{\alpha=\tau}{\bullet;[\tau/\alpha]}
    }
    \\[2ex]
    \Inf[\mathit{app}_U]{}{
      \unifsimpl{\tau_1~\tau_2=\tau_1'~\tau_2'}{%
        \{\tau_1=\tau_1',\tau_2=\tau_2'\};\bullet}
    }
    \qquad
    \Inf[\mathit{red}_U]{
      \tred{\eta}{\tau_2}
    }{
      \unifsimpl{\eta=\tau_1}{\{\tau_2=\tau_1\};\bullet}
    }
  \end{gather*}
  
  \medskip
  \ruleform{\unifsimplS{U}{U';R}}\\
  \begin{gather*}
    \Inf{}{%
      \unifsimplS{U}{U;\bullet}
    }
    \qquad
    \Inf{%
      \unifsimpl{\tau_1=\tau_2}{U';R'} 
      \qquad 
      \unifsimplS{R'U,U'}{U'';R''}
    }{%
      \unifsimplS{U,\tau_1=\tau_2}{U'';R''R'}
    }
  \end{gather*}
  \caption{Unification in the presence of type functions}
  \label{fig:unification}
\end{figure*}
%
Associated type synonyms extend Haskell 98's purely syntactic type equality;
e.g, \<Elem BitSet = Char\> holds under the definitions for the class
\<Collects\> discussed before.  To handle non-syntactic equalities during
unification, we exploit the properties of well-formed programs.  In
particular, the type functions in well-formed programs are confluent and
terminating; i.e., type terms have unique normal forms.  Hence, we can
determine whether two type terms are equal by syntactically comparing their
normal forms.

The judgement \(\tred\tau{\tau'}\), whose inference rules are given by
Figure~\ref{fig:unification}, defines a \emph{one-step reduction relation} on
type terms under a constraint environment $\Theta$.  The reduction relation on
types is used by the \emph{one-step unification judgement}
\(\unifsimpl{\tau_1=\tau_2}{U;R}\).  This judgement holds for an equality
\(\tau_1=\tau_2\) iff the corresponding unification problem can be reduced to a
simpler unification problem in the form of a set of equality constraints $U$
and a substitution $R$.  The symbol $\bullet$ in the inference rules
represents an empty set of equality constraints and the identity substitution,
respectively.  The repeated application of one-step unification, as performed
by the reflexive and transitive closure \(\unifsimplS{U}{U';R}\), reduces a
set of equality constraints $U$ to a set of pending equality constraints $U'$
and a substitution $R$.  If $U'$ cannot be reduced any further, we also write
\(\unifsimplto[\Theta]{U}{U';R}\), hence turning the transitive closure of
one-step unification into a deterministic function.  Note that, due to the
syntactic restrictions on $\tau$, 
Rule~\rulename{\mathit{app}_U}  and \rulename{\mathit{red}_U} are not overlapping.

Unification is performed
under a constraint environment $\Theta$ only because this environment is
required by associate type synonym expansion.  It is easy to see that, where
two types $\tau_1$ and $\tau_2$ are free of associated synonyms, the relation
\(\unifsimplto[\bullet]{\{\tau_1=\tau_2\}}{\bullet;R}\) coincides with
standard syntactic unification as employed in type inference for vanilla
Haskell 98.

Just like Jones~\cite{jones:constr-class}, we only need first-order
unification despite the presence of higher-kinded variables, as we require all
applications of associated type synonyms to be saturated.

\paragraph{Soundness of unification.}  
%
The judgements of Figure~\ref{fig:unification} enjoy the following properties.

\begin{lemma}[Soundness of type reduction]
  Given a well-formed constraint environment $\Theta$ and a type $\tau$ with
  \(\wfpi\tau\), we have that \(\tred\tau{\tau'}\) implies
  \(\entails{\tau=\tau'}\).
\end{lemma}
%
\begin{lemma}[Soundness of one-step unification]
  Given a well-formed constraint environment $\Theta$, the judgement
  \(\unifsimpl{\tau_1=\tau_2}{U;R}\) implies that
  \(\entails{R(\tau_1=\tau_2)}\) iff \(\entails{U}\).
\end{lemma}
%
\begin{theorem}[Soundness of unification]\label{thm:sound-unif}
  Given a well-formed constraint environment $\Theta$ and a set of equalities
  $U$, then \(\unifsimplS{U}{U';R}\) implies that \(\entails{RU}\) iff
  \(\entails{U'}\). 
\end{theorem}
%
The proofs proceed by rule induction.  Moreover, Theorem~\ref{thm:sound-unif}
requires that ``\(\entails{R\theta_1}\) iff \(\entails{R\theta_2}\)'' follows
from ``\(\entails{\theta_1}\) iff \(\entails{\theta_2}\)'' for any substitution
$R$, which is a basic property of constraint entailment.

\subsection{Subsumption} 
\label{sect:subsumption}

\manuel{We must talk about that, while internally equalities can be cyclic, we
  do not support cyclic equalities in \textbf{user-provided} signatures.  I
  think that we don't have to do anything extra to the formal system to
  achieve that, but we need to explain it with an example and we need to
  define completeness such that it excludes cyclic equalities in user-supplied
  type annotations a priori.}

\begin{figure*}[tbp]
  \centering
  \renewcommand{\arraystretch}{3}
  \ruleform{\entailsimpl{\pi}{P;R}}\\
  \begin{gather*}
    \Inf[\mathit{bchain}_E]{
      (\forall\tup\alpha.\tup\pi\To D~\tau)\in\Theta
    }{
      \entailsimpl{[\tup\xi/\tup\alpha]D~\tau}{%
        [\tup\xi/\tup\alpha]\tup\pi;\bullet}
    }
    \qquad
    \Inf[\mathit{red}_E]{
      \tred{\tau}{\tau'}
    }{
      \entailsimpl{D~\tau}{\{D~\tau'\};\bullet}
    }
    \qquad
    \Inf[\mathit{eq}_E]{
      \unifsimpl{\tau_1=\tau_2}{U;R}
    }{
      \entailsimpl{\tau_1=\tau_2}{U;R}
    }
  \end{gather*}
  
  \medskip
  \ruleform{\entailsimplS{P}{P';R}}\\
  \begin{gather*}
    \Inf{}{%
      \entailsimplS{P}{P;\bullet}
    }
    \qquad
    \Inf{%
      \entailsimpl{\pi}{P';R'} 
      \qquad 
      \entailsimplS{R'P,P'}{P'';R''}
    }{%
      \entailsimplS{P,\pi}{P'';R''R'}
    }
  \end{gather*}
  \caption{Constraint entailment with equality constraints}
  \label{fig:entailment}
\end{figure*}
%
To handle type annotations, such as in expressions of the form \(e::\sigma\),
during type inference, we need to have an algorithm deciding type subsumption.
We say a type scheme $\sigma_1$ \emph{subsumes} $\sigma_2$, written
\(\sigma_1\leq\sigma_2\) iff any expression that can be typed as $\sigma_1$
can also be typed as $\sigma_2$.

The subsumption check can be formulated as a constraint entailment problem in
the presence of equality constraints.  If we want to check
\[
(\forall\tup{\alpha_1}.\tup{\pi_1}\To\tau_1)
\leq
(\forall\tup{\alpha_2}.\tup{\pi_2}\To\tau_2),
\]
in the context of a program context $\Theta_P$, we need to demonstrate that,
given a set of new type constructors \(\tup{T}\) of the appropriate kind,
there exists a substitution \(R=[\tup\xi/\tup{\alpha_1}]\), such that
\[
\entails[{\Theta_P,[\tup{T}/\tup{\alpha_2}]\tup{\pi_2}}]{%
  R\tup{\pi_1},R\tau_1=[\tup{T}/\tup{\alpha_2}]\tau_2}
\]
where we define the entailment of a set of predicates \(\entails{\tup\theta}\)
as the conjunction of all \(\entails{\theta_i}\).

Given that we implement the entailment of equalities by unification during
type inference, it is not surprising that we can implement subsumption via a
combination of unification and the usual backchaining approach to entailment;
a process called \emph{context reduction} when used to simplify type class
contexts.  In Figure~\ref{fig:entailment}, we define the procedure computing
entailment using the same structure as we used for the unification procedure:
Firstly, we define a one-step entailment judgement \(\entailsimpl\pi{P;R}\)
that reduces a constraint $\pi$ (which may be a class constraint or equality
constraint) to a simpler set of constraints $P$ and a substitution $R$.
Rule~\rulename{bchain_E} formalises standard backchaining,
Rule~\rulename{red_E} enables the reduction of associated type synonyms in
class parameters, and Rule~\rulename{eq_E} invokes one-step unification for
equality constraints.  Secondly, we define the reflexive and transitive
closure \(\entailsimplS{P}{P';R}\).  Finally, we turn the closure into a
deterministic function by requiring that for \(\entailsimplto{P}{P';R}\), the
resulting set of constraints $P'$ cannot be reduced further.

Now, we can define subsumption as follows:
\[
\Inf[\leq]{{\begin{array}{c}
  \entailsimplto[{\Theta_P,[\tup{T}/\tup{\alpha_2}]\tup{\pi_2}}]{
    \{\tup{\pi_1},\tau_1=[\tup{T}/\tup{\alpha_2}]\tau_2\}}{\bullet;R}
  \\
  \tup{T}\text{ new type constructors}
  \end{array}}
  }{
    \subsumes{
      (\forall\tup{\alpha_1}.\tup{\pi_1}\To\tau_1)
    }{
      (\forall\tup{\alpha_2}.\tup{\pi_2}\To\tau_2)
    }
  }
\]
In other words, subsumption succeeds if context reduction can resolve the
constraint set entirely.

\paragraph{Soundness of subsumption.}
%
The subsumption rule enjoys the following property.

\begin{lemma}[Soundness of subsumption]\label{lem:sub-sound}
  Let $\Theta_P$ be a well-formed constraint environment, and
  \(\sigma_1=\forall\tup{\alpha_1}.\tup{\pi_1}\To\tau_1\) and 
  \(\sigma_2=\forall\tup{\alpha_2}.\tup{\pi_2}\To\tau_2\) signatures with
  \(\entails[\Theta_P]{\sigma_1}\) and \(\entails[\Theta_P]{\sigma_2}\), where
  $\sigma_2$ is closed.  Then, \(\subsumes{\sigma_1}{\sigma_2}\) implies that,
  given a set of new type constructors \(\tup{T}\) of the appropriate kind,
  there exists a substitution \(R=[\tup\xi/\tup{\alpha_1}]\), such
  that \(\entails[{\Theta_P,[\tup{T}/\tup{\alpha_2}]\tup{\pi_2}}]{%
    R\tup{\pi_1},R\tau_1=[\tup{T}/\tup{\alpha_2}]\tau_2}\).
\end{lemma}
%
The lemma is an immediate consequence of Theorem~\ref{thm:sound-unif}.

\subsection{Formal properties of type inference}

\begin{theorem}[Soundness of type inference]
  Assume a well-formed program context $\Theta_P$, typing environment
  $\Gamma$, and expression $e$.  If \(\tinf{e}\tau\), then
  \(\typing[(\Theta_P,\Theta,U)\mid{T\Gamma}]{e}\tau\). 
\end{theorem}
%
In proving this theorem, we followed Jones~\cite{jones:qual-types} who
introduces a \emph{syntax-directed system} as a bridge between the declarative
typing rules and the algorithmic inference rules, as first suggested by
Cl{\'e}ment at al.~\cite{clement-etal:mini-ml}.  The tricky bit is to define
the inference rule for function elimination in the syntax-directed system such
that a correspondence to the inference system can be established.  We define
the rule as follows:
\[
\Inf[{\to}E_S]{{\begin{array}{c}
  \typing[\Theta\mid\Gamma]{e_1}{\tau_1}
  \qquad
  \typing[\Theta\mid\Gamma]{e_2}{\tau_2}
  \\
  \entails[\Theta_P,\Theta]{\tau_1=\tau_2\to\tau_1'}
  \end{array}}
}{
  \typing[\Theta\mid\Gamma]{e_1~e_2}{\tau_1'}
}
\]
In addition, we need to use Theorem~\ref{thm:sound-unif} and
Lemma~\ref{lem:sub-sound}.

\subsection{Completeness.}

\TODO{How to handle ambigious programs?}

We believe that our inference algorithm is complete and that we can obtain
principal types by performing a further generalisation step on its outputs.
However, we leave the proof to further work---which we plan to do by again
following Jones' scheme for qualified types.
\fi

\section{Related work}
\label{sec:related}


\section{Conclusions}


\bibliographystyle{plain}
\bibliography{at-ng}

\end{document}

% Local IspellDict: british

% Local Variables:
% TeX-auto-untabify: nil
% End:
