content: \documentclass[authoryear]{sigplanconf}
  
  %options ghci
  
  %include lhs2TeX.fmt
  %include lhs2TeX.sty
  
  \DeclareMathAlphabet{\mathkw}{OT1}{cmss}{bx}{n}
  %subst keyword a = "\mathkw{" a "}"
  %subst conid a = "\mathsf{" a "}"
  
  %format <-  = "\leftarrow "
  %format :-> = "\arrow "
  %format <>< = "<\!>\!< "
  %format <>> = "<\!>\!> "
  %format <+> = "\oplus "
  %format <*> = "\varoast "
  %format <$> = "<\!\!\$\!\!> "
  %format :$  = ":\!\!\$\ "
  %format ::: = "\asc "
  %format >=> = "\genarrow "
  %format <?  = "\in "
  %format ... = "\ldots "
  %format >-  = "\Yright "
  %format .   = "\,\circ\, "
  
  %format F0  = "\emptycontext"
  %format B0  = "\emptycontext"
  
  % %format Lam (x) (b) = "\lambda" x "." b
  % %format Let (x) (s) (t) = "\letIn{" x "}{" s "}{" t "} "
  %format LetGoal = "\letGoal "
  
  %format Hole = "? "
  %format Some = "!\!"
  
  %format alpha  = "\alpha"
  %format alpha0
  %format alpha1
  %format alpha'
  %format alphaD = "\alpha\!D"
  %format beta   = "\beta"
  %format beta0
  %format beta1
  %format gamma  = "\gamma"
  %format _Gamma  = "\Gamma"
  %format _Gamma0
  %format _Gamma1
  %format delta  = "\delta"
  %format delta0
  %format delta1
  %format nu     = "\nu"
  %format sigma  = "\sigma"
  %format sigma0
  %format sigma1
  %format sigma'
  %format tau    = "\tau"
  %format tau0
  %format tau1
  %format tau'
  %format rho = "\rho"
  %format upsilon = "\upsilon"
  %format upsilon0
  %format upsilon1
  %format chi = "\chi"
  %format _Xi = "\Xi"
  %format _Xi0
  %format _Xi1
  
  \newcommand{\ident}[1]{\mathsf{#1}}
  %format return          = "\ident{return}"
  %format put             = "\ident{put}"
  %format any             = "\ident{any}"
  %format fst             = "\ident{fst}"
  %format snd             = "\ident{snd}"
  %format get             = "\ident{get}"
  %format fmap            = "\ident{fmap}"
  %format gets            = "\ident{gets}"
  %format succ            = "\ident{succ}"
  %format fail            = "\ident{fail}"
  %format error           = "\ident{error}"
  %format otherwise       = "\ident{otherwise}"
  %format occurs          = "\ident{occurs}"
  %format fresh           = "\ident{fresh}"
  %format getContext      = "\ident{getContext}"
  %format putContext      = "\ident{putContext}"
  %format modifyContext   = "\ident{modifyContext}"
  %format onTop           = "\ident{onTop}"
  %format restore         = "\ident{restore}"
  %format replace         = "\ident{replace}"
  %format unify           = "\ident{unify}"
  %format solve           = "\ident{solve}"
  %format specialise      = "\ident{specialise}"
  %format unpack          = "\ident{unpack}"
  %format fromS           = "\ident{fromS}"
  %format generaliseOver  = "\ident{generaliseOver}"
  %format skimContext     = "\ident{skimContext}"
  %format find            = "\ident{find}"
  %format help            = "\ident{help}"
  %format extract         = "\ident{extract}"
  %format infer           = "\ident{infer}"
  %format bind            = "\ident{bind}"
  
  \usepackage{color}
  \definecolor{red}{rgb}{1.0,0.0,0.0}
  \newcommand{\TODO}[1]{\NotForPublication{\textcolor{red}{#1}}}
  \newcommand{\NotForPublication}[1]{#1}
  
  % Boxes and inference rules
  \newcommand{\mathframe}[1]{\framebox{\ensuremath{#1}}}
  \newcommand{\boxrule}[1]{\begin{center}\mathframe{#1}\end{center}}
  \newcommand{\boxrules}[2]{\begin{center}\mathframe{#1}\quad\mathframe{#2}\end{center}}
  \newcommand{\boxruless}[3]{\begin{center}\mathframe{#1}\quad\mathframe{#2}\quad\mathframe{#3}\end{center}}
  \newcommand{\name}[1]{\textsc{#1}}
  \newcommand{\namer}[1]{\ensuremath{\mathrm{\name{#1}} \;}}
  \newcommand{\side}[1]{\ensuremath{\; #1}}
  \newcommand{\br}[2]{\genfrac{}{}{0pt}{0}{#1}{#2}}
  \newcommand{\BigRule}[3]{\ensuremath{\Rule{\br{#1}{#2}}{#3}}}
  
  % Text
  \newcommand{\define}[1]{\emph{#1}}
  \newcommand{\scare}[1]{`#1'}
  \newcommand{\W}{\ensuremath{\mathcal{W}}}
  \newcommand{\AlgorithmW}{Algorithm~\W}
  \newcommand{\hindleymilner}{Hindley-Milner}
  \newcommand{\hindleymilnershort}{HM}
  
  % Definitions
  \newcommand{\defmap}{~\mapsto~}
  \newcommand{\centcolon}{\mathrel{\mathop:}}
  \newcommand{\defsyn}{\centcolon\centcolon=}
  
  % Substitutions
  \newcommand{\eqsubst}{\equiv}
  \newcommand{\compose}{\cdot}
  \newcommand{\subst}[3]{[#1/#2]#3}
  \newcommand{\restrict}[2]{#1 ||_{#2}}
  
  % Sets and sorts
  \newcommand{\V}{\mathcal{V}}
  \newcommand{\D}{\mathcal{D}}
  \newcommand{\Ss}{\mathcal{S}}
  \newcommand{\K}{\mathcal{K}}
  \newcommand{\TY}{\mathrm{\textsc{TY}}}
  \newcommand{\TM}{\mathrm{\textsc{TM}}}
  
  % Context bits
  \newcommand{\entails}{\ensuremath{\vdash}}
  \newcommand{\entailsN}{\ensuremath{\Vdash}}
  \newcommand{\emptycontext}{\ensuremath{\mathcal{E}}}
  \newcommand{\letGoal}{\ensuremath{\fatsemi}}
  \newcommand{\defn}{\ensuremath{\!\centcolon=\!}}
  \newcommand{\asc}{\ensuremath{\!::\!}}
  \newcommand{\hole}[1]{\ensuremath{#1 \!\centcolon= ?}}
  \newcommand{\decl}[2]{#1 #2}
  
  % Statements
  \newcommand{\type}{\ensuremath{~\mathbf{type}}}
  \newcommand{\scheme}{\ensuremath{~\mathbf{scheme}}}
  \newcommand{\valid}{\ensuremath{\mathbf{valid}}}
  \newcommand{\Sbind}[2]{#1 \Yright #2}
  \newcommand{\hasscheme}{\ensuremath{::}}
  \newcommand{\Pinf}[2]{#1 : #2}
  \newcommand{\Psch}[2]{#1 \hasscheme #2}
  \newcommand{\Puni}[2]{#1 \equiv #2}
  \newcommand{\sanity}{sanity condition}
  \newcommand{\Sanity}{Sanity condition}
  
  % Types, terms and schemes
  \newcommand{\arrow}{\ensuremath{\triangleright}}
  \newcommand{\letIn}[3]{\ensuremath{\mathrm{let}\; #1 \!\centcolon=\! #2 \;\mathrm{in}\; #3}}
  \newcommand{\letS}[3]{\ensuremath{(!#1 \!\centcolon=\! #2 ~\mathrm{in}~ #3)}}
  \newcommand{\genarrow}{\ensuremath{\Uparrow}}
  \newcommand{\gen}[2]{\ensuremath{(#1 \genarrow #2)}}
  \newcommand{\gendot}[1]{\ensuremath{.{#1}}}
  
  % Maps
  \newcommand{\tyvars}[1]{\ensuremath{\V_\TY(#1)}}
  \newcommand{\FTV}[1]{\ensuremath{\mathit{FTV}(#1)}}
  \newcommand{\sem}[1]{\ensuremath{\llbracket #1 \rrbracket}}
  \newcommand{\ok}{\ensuremath{~\mathbf{ok}}}
  \newcommand{\forget}[1]{\ensuremath{\lfloor #1 \rfloor}}
  \newcommand{\semidrop}{\downharpoonright}
  
  % Relations between contexts
  \newcommand{\lei}{\ensuremath{\preceq}}
  \newcommand{\LEI}{\ensuremath{~\hat\lei~}}
  \newcommand{\leiR}{\ensuremath{\sqsubseteq}}
  \newcommand{\LEIR}{\ensuremath{~\hat\sqsubseteq~}}
  \newcommand{\transto}{\ensuremath{\twoheadrightarrow}}
  
  \newcommand{\iRel}[4]{#1 #3 #4 \entails #2}
  \newcommand{\ioRel}[5]{#1 \circ #2 #3 #4 \bullet #5}
  
  \newcommand{\leiStmt}[3]{\iRel{#1}{#2}{\lei}{#3}}
  \newcommand{\leiRStmt}[3]{\iRel{#1}{#2}{\leiR}{#3}}
  \newcommand{\LEIStmt}[3]{\iRel{#1}{#2}{\LEI}{#3}}
  \newcommand{\LEIRStmt}[3]{\iRel{#1}{#2}{\LEIR}{#3}}
  \newcommand{\leiRParam}[4]{(#1, #2) \leiR (#3, #4)}
  \newcommand{\LEIProb}[4]{\ioRel{#1}{#2}{\LEI}{#3}{#4}}
  \newcommand{\LEIRProb}[4]{\ioRel{#1}{#2}{\LEIR}{#3}{#4}}
  \newcommand{\LEIUnify}[4]{\leiStmt{#1}{#2 \equiv #3}{#4}}
  \newcommand{\LEIRUnify}[4]{\leiRStmt{#1}{#2 \equiv #3}{#4}}
  \newcommand{\LEIInfer}[4]{\LEIProb{#1}{(#2 :)}{#4}{#3}}
  \newcommand{\LEIRInfer}[4]{\LEIRProb{#1}{(#2 :)}{#4}{#3}}
  \newcommand{\LEIInferScheme}[4]{\LEIProb{#1}{(#2 \hasscheme)}{#4}{#3}}
  \newcommand{\LEIRInferScheme}[4]{\LEIRProb{#1}{(#2 \hasscheme)}{#4}{#3}}
  
  \newcommand{\alg}[4]{\ioRel{#1}{#2}{\transto}{#3}{#4}}
  \newcommand{\ialg}[3]{\iRel{#1}{#2}{\transto}{#3}}
  \newcommand{\algUnify}[4]{\ialg{#1}{#2 \equiv #3}{#4}}
  \newcommand{\algInstantiate}[5]{\ialg{#1 ~||~ #4}{#2 \equiv #3}{#5}}
  \newcommand{\algInfer}[4]{\alg{#1}{(#2 :)}{#4}{#3}}
  \newcommand{\algInferScheme}[4]{\alg{#1}{(#2 \hasscheme)}{#4}{#3}}
  
  % Problem bits
  \newcommand{\iprobcond}[2]{#1\! [#2]}
  \newcommand{\iprobstmt}[3]{#1\! [#2]\, #3}
  \newcommand{\iprobsubst}[4]{(#1 (#2\! [#3]))\, #4}
  \newcommand{\probstmt}[2]{#1 #2}
  \newcommand{\probsubst}[3]{(#1 #2) #3}
  
  \newcommand{\leParam}[4]{#2 \entails #3 \subset_{#1} #4}
  \newcommand{\pconj}[3]{\Sigma #1 #3}
  \newcommand{\Qbind}[2]{#1 ~ \Yright #2}
  
  
  
  \usepackage{amsthm}
  \usepackage{amsmath}
  \usepackage{enumerate}
  \usepackage{eucal}
  \usepackage{natbib}
  \usepackage[T1]{fontenc}
  \usepackage{subfigure}
  % \usepackage[colorlinks,draft=true]{hyperref}
  
  \newcommand{\url}[1]{{\tt #1}}
  \newcommand{\phantomsection}{}
  
  \newcommand{\fixpars}{\setlength{\parskip}{5pt}\setlength{\parindent}{0pt}}
  \fixpars
  
  \newtheorem{lemma}{Lemma}
  \newcommand{\proofsux}{\vspace*{-0.2in}}
  
  \include{macros}
  \setlength{\rulevgap}{0.05in}
  
  \hyphenpenalty=5000
  \tolerance=1000
  
  
  %if showCode
  
  > {-# LANGUAGE  DeriveFunctor, DeriveFoldable,
  >               FlexibleInstances, TypeSynonymInstances,
  >               TypeFamilies, StandaloneDeriving, TypeOperators #-}
  
  > import Prelude hiding (any)
  > import Control.Monad.State (StateT, get, gets, put, runStateT)
  > import Data.Foldable (Foldable, any, foldMap)
  > import Data.Monoid (Monoid, mappend, mempty)
  
  %endif
  
  
  
  \begin{document}
  
  \conferenceinfo{MSFP'10,} {September 26, 2010, Baltimore, Maryland, USA.}
  \CopyrightYear{2010}
  \copyrightdata{978-1-4503-0251-7/10/09}
  
  \titlebanner{\NotForPublication{REVISED DRAFT}}
  
  \title{Type Inference in Context}
  \authorinfo{Adam Gundry\thanks{%%%Adam Gundry was supported 
                   Supported by the Microsoft Research PhD Scholarship Programme.} 
              \and Conor McBride}
             {University of Strathclyde, Glasgow}
             {\{adam.gundry,conor.mcbride\}@@cis.strath.ac.uk}
  \authorinfo{James McKinna\thanks{%%%James McKinna was supported 
                    Supported by the NWO cluster `\textsc{Diamant}'. }}
             {Radboud University, Nijmegen}
             {james.mckinna@@cs.ru.nl}
  
  \maketitle
  
  \begin{abstract}
  
  We consider the problems of first-order unification and type inference
  from a general perspective on problem-solving, namely that of
  information increase in the problem context.  This leads to a powerful
  technique for implementing type inference algorithms.  We describe a
  unification algorithm and illustrate the technique for the familiar
  Hindley-Milner type system, but it can be applied to more advanced
  type systems.  The algorithms depend on \emph{well-founded} contexts:
  type variable bindings and type-schemes for terms may depend only on
  earlier bindings.  We ensure that unification yields a most general
  unifier, and that type inference yields principal types, by advancing
  definitions earlier in the context only when necessary.
  
  \end{abstract}
  
  \category{F.3.3}{Logics and Meanings of Programs}{Studies of Program Constructs}[Type structure]
  % \category{D.3.3}{Programming Languages}{Language Constructs and Features}[Data types and structures]
  
  \terms
  Algorithms, Theory
  
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{Introduction\label{sec:intro}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  %%% \subsection{\AlgorithmW}
  
  \AlgorithmW\ is a well-known type inference algorithm for the \hindleymilner\
  (\hindleymilnershort)
  system \citep{milner_theory_1978, damas_principal_1982}, based on
  \citeauthor{robinson_machine-oriented_1965}'s Unification Algorithm
  \citeyearpar{robinson_machine-oriented_1965}. The system consists of
  simply-typed $\lambda$-calculus with \scare{let-expressions} for polymorphic
  definitions.
  For example, %%% the term
  $$\letIn{i}{\lambda x . x}{i\:i}$$
  is well-typed: $i$ is given a polymorphic type, which is instantiated in two
  different ways. The syntax of types is
  $$\tau \defsyn \alpha ~||~ \tau \arrow \tau.$$
  For simplicity, the function arrow $\arrow$ is our only type constructor.
  We let $\alpha$ and $\beta$ range over type variables and $\tau$ and $\upsilon$
  over types.
  
  Most presentations of \AlgorithmW\ have treated the underlying unification
  algorithm as a \scare{black box}, but by considering both together we can give a
  more elegant type inference algorithm.  In particular, the generalisation step
  (used when inferring the type of a let-expression) becomes straightforward
  (Section \ref{sec:tyinf}).
  
  \subsection{Motivating context}
  
  Why revisit \AlgorithmW? 
  %%%This is 
     As 
  a first step towards a longer-term goal:
  %%%to explain the elaboration of 
     explaining how to elaborate 
  high-level \emph{dependently typed} programs into fully explicit calculi. 
  Just as \W\ specialises polymorphic type schemes, 
  elaboration involves inferring \emph{implicit arguments} by solving constraints, but
  with fewer algorithmic guarantees. Pragmatically, 
     we need to account for
  stepwise progress in problem solving from states of partial knowledge.
  We 
  %%%wish to identify 
     seek  
  local correctness criteria for type inference 
     that guarantee 
  %%%guaranteeing 
  global correctness.
  
  
  In contrast to other presentations of unification and \hindleymilnershort\ type
  inference, our algorithm is based on contexts carrying variable definitions as
  well as declarations. This avoids the need to represent substitutions explicitly.
  (We use them to reason about the system.)
  
  This paper has been a long time brewing. 
     Its origins lie in a constraint
  %%%It originates in a con-straint
  engine cannibalised by McBride from an implementation of
  \citeauthor{miller:mixed}'s \scare{mixed prefix}
  unification~\citeyearpar{miller:mixed}, mutating the quantifier prefix into a
  context. \citeauthor{mcbride:thesis}'s thesis~\citeyearpar{mcbride:thesis} gives
  an early account of using typing contexts to represent the state of an
  interactive construction system, \scare{holes} in programs and proofs being 
  specially designated variables. Contexts carry an information order: increase of
  information preserves typing and equality judgments; proof tactics are
  admissible context validity rules which increase information; unification is
  specified as a tactic which increases information to make an equation hold, but
  its imple-mentation is not discussed. This view of construction underpinned the
  implementation of Epigram~\citep{mcbride.mckinna:view-from-the-left} and informed
  \citeauthor{norell:agda}'s 
  %%%implementation of Agda~\citeyearpar{norell:agda}. 
     Agda implementation~\citeyearpar{norell:agda}.
  It is high time we began to explain how it works and perhaps to understand it.
  
  We are grateful to an anonymous referee for pointing out the work of
  \citet{dunfield_polymorphism_2009} on polymorphism in a bidirectional type system.
  Dunfield uses well-founded contexts that contain existential type variables
  (amongst other things). These variables can be solved, and there is an informal
  notion of information increase between input and output contexts.
  %%% though this is used for different purposes. 
  However, our concerns are different: whilst Dunfield elaborates a
  particular approach to bidirectional polymorphic checking to a larger
  class of type theories, here we pursue a methodological understanding
  of the problem-solving strategy in \hindleymilner\ type inference.
  
  %%%\TODO{More crunchiness: forward pointers to claims and contributions}
  
  This paper is literate Haskell, with full source code available at
  \footnotesize\url{http://personal.cis.strath.ac.uk/{\(\sim\)}adam/type-inference/}\normalsize.
  
  \subsection{The occurs check}
  
  Testing whether a variable occurs in a term is used by both Robinson unification
  and \AlgorithmW. In unification, the check is (usually)
  necessary to ensure termination, let alone correctness: the equation
  $\alpha \equiv \alpha \arrow \beta$ has no (finite) solution because the
  right-hand side depends on the left, so it does not make a good definition.
  
  In \AlgorithmW, the occurs check is used to discover type dependencies just in
  time for generalisation. When inferring the type of the let-expression
  $\letIn{x}{e'}{e}$, the type of $e'$ must first be inferred, then
  quantified over \scare{generic} type variables, i.e.\ those involved with $e'$
  but not the enclosing bindings. 
  The rule in question, as presented by \citet{clment_simple_1986}, is:
  $$
  \Rule{A \entails e' : \tau'  \qquad  A_x \cup \{ x : \sigma \} \entails e : \tau}
       {A \entails \letIn{x}{e'}{e} : \tau}
  \side{\sigma = gen(A, \tau')}
  $$
  $$gen(A, \tau) = \begin{cases}
      \forall \vec{\alpha_i} . \tau  &
          (FV(\tau) \setminus FV(A) = \{ \alpha_1, \cdots, \alpha_n \})  \\
      \tau &
          (FV(\tau) \setminus FV(A) = \emptyset)
  \end{cases}.
  $$
  The context \(A\) is an unordered set of type scheme 
  %%%assignments, 
     bindings, 
  with \(A_x\) denoting 
  %%%`\(A\) with any \(x\) assignment removed': 
     `\(A\) minus any \(x\) binding ': such 
  contexts
  %%%are not designed to
     do not
  reflect lexical scope, so shadowing requires deletion and reinsertion.
  
  The `let' rule is the only real complexity in \AlgorithmW,
  and as \citet{milner_theory_1978} wrote, ``the
  reader may still feel that our rules are arbitrarily chosen and only partly
  supported by intuition.'' The rules are well-chosen
  indeed; perhaps we can recover the intuition.
  
  In both cases, the occurs check is used to detect dependencies between variables.
  Type variables are traditionally left floating in space and given meaning by
  substitution, but by exposing structure we can manage definitions and
  dependencies as we go. Recording type variables in the context is natural when
  dealing with dependent types, as there is no distinction between type and term
  variables, but it also works well in the simply-typed setting.
  
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{Unification over a context\label{sec:unif}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  We begin %%%our study of type inference 
  by revisiting unification for
  type expressions containing free variables. Let us equip ourselves to
  address the problem---solving equations---by explaining which types
  are considered equal, raising the question of which things a given
  context admits as types, and 
  %%%in turn, 
     hence, 
  which contexts make sense in the first place.
  
  \begin{figure}[ht]
  \[\begin{array}{c}
  \mathframe{\Gamma \entails \valid} \smallskip \\
  \Axiom{\emptycontext \entails \valid}
  \qquad
  \Rule{\Gamma \entails \valid}
       {\Gamma, \hole{\alpha} \entails \valid}
  \side{\alpha \notin \Gamma}
  \smallskip \\
  \Rule{\Gamma \entails \valid    \quad    \Gamma \entails \tau \type}
       {\Gamma, \alpha \defn \tau \entails \valid}
  \side{\alpha \notin \Gamma}
  
  \bigskip \\
  
  \mathframe{\Gamma \entails \tau \type} \smallskip \\
  \Rule{\Gamma, \alpha \defn \_, \Gamma' \entails \valid}
       {\Gamma, \alpha \defn \_, \Gamma' \entails \alpha \type}
  \qquad
  \Rule{\Gamma \entails \tau \type   \quad   \Gamma \entails \upsilon \type}
       {\Gamma \entails \tau \arrow \upsilon \type}.
  
  \bigskip \\
  
  \mathframe{\Gamma \entails \tau \equiv \upsilon} \smallskip \\
  \Rule{\Gamma, \alpha \defn \tau, \Gamma' \entails \valid}
       {\Gamma, \alpha \defn \tau, \Gamma' \entails \alpha \equiv \tau}
  \qquad
  \Rule{\Gamma \entails \tau \type}
       {\Gamma \entails \tau \equiv \tau}
  \qquad
  \Rule{\Gamma \entails \upsilon \equiv \tau}
       {\Gamma \entails \tau \equiv \upsilon}
  \smallskip \\
  \Rule{\Gamma \entails \tau_0 \equiv \upsilon_0
        \quad
        \Gamma \entails \tau_1 \equiv \upsilon_1}
       {\Gamma \entails \tau_0 \arrow \tau_1 \equiv \upsilon_0 \arrow \upsilon_1}
  \qquad
  \Rule{\Gamma \entails \tau_0 \equiv \tau_1
        \quad
        \Gamma \entails \tau_1 \equiv \tau_2}
       {\Gamma \entails \tau_0 \equiv \tau_2}
  \end{array}\]
  \caption{Rules for validity, types and type equivalence}
  \label{fig:oldRules}
  \end{figure}
  
  The rules in Figure~\ref{fig:oldRules} define a context as a left-to-right list
  of type variables, each of which may be declared 
  \define{unknown} (written $\hole{\alpha}$) or
  \define{defined} (written $\alpha \defn \tau$). 
  A context is \define{valid} if the type \(\tau\) in
  every definition makes sense in its preceding context.
  For example, the context
  $\hole{\alpha}, \hole{\beta}, \gamma \defn \alpha \arrow \beta$
  is valid, while %%%but the context
  $\alpha \defn \beta, \hole{\beta}$
  is not, because $\beta$ is not in scope for the definition of $\alpha$.
  This topological sorting of the dependency graph means that 
  entries on the right are harder to depend on, and correspondingly easier to
  generalise, just by discharging them as hypotheses in the usual way.
  
  Definitions in the context induce a nontrivial equational theory on types,
  starting with $\alpha \equiv \tau$ for every definition $\alpha \defn \tau$ in
  the context, then taking the congruence closure.
  Unification is the problem of making variable definitions (thus increasing
  information) 
  %%%to solve an equation. 
     in order to make an equation hold. 
  The idea is to decompose constraints on the syntactic structure of types
  until we reach variables, then move through the context and update it to solve
  the equation. 
  
  For example, we might start in context
  $\hole{\alpha}, \hole{\beta}, \gamma \defn \alpha \arrow \beta$
  aiming to solve the equation $\beta \arrow \alpha \equiv \gamma$.
  %
  % The definition of $\gamma$ tells us that we must
  % solve $\beta \arrow \alpha \equiv \alpha \arrow \beta$ over the context
  % $\hole{\alpha}, \hole{\beta}$. This constraint decomposes to
  % $\beta \equiv \alpha$ and $\alpha \equiv \beta$, which are easily solved by
  % defining $\beta \defn \alpha$, giving the final judgment
  %
  It suffices to define $\beta \defn \alpha$, giving as final judgment
  $\hole{\alpha}, \beta \defn \alpha, \gamma \defn \alpha \arrow \beta
      \entails \beta \arrow \alpha \equiv \gamma.$
  
  A context represents a substitution in `triangular form'~\cite{DBLP:books/el/RV01/BaaderS01}, 
  which can be applied on demand.
  % but that need not be all.
  As we proceed with the development,
  the context structure will evolve to hold a variety of information
  about variables of all sorts and some control markers, managing the
  generalisation process.
  
  \subsection{Implementation of unification}
  
  \begin{figure*}[p]
  
  \begin{minipage}[b]{0.5\linewidth}
  
  \subfigure[][Types, type variables, occurs check]{\frame{\parbox{\textwidth}{\fixpars\medskip
  
  > data Ty a  =  V a |  Ty a :-> Ty a
  >     deriving (Functor, Foldable)
  
  %if showCode
  
  > infixr 5 :->
  
  %endif
  
  > type TyName  = Integer
  > type Type    = Ty TyName
  
  
  > class FTV a where
  >     (<?) :: TyName -> a -> Bool
  
  > instance FTV TyName where
  >     (<?) = (==)
  
  > instance  (Foldable t, FTV a) => FTV (t a) where
  >     alpha <? t = any (alpha <?) t
  
  \label{subfig:typeCode}
  }}}
  
  \subfigure[][Contexts and suffixes]{\frame{\parbox{\textwidth}{\fixpars\medskip
  
  > data TyDecl   =  Some Type | {-"\;"-} Hole
  > data TyEntry  =  TyName := TyDecl
  
  > instance FTV TyEntry where
  >    alpha <? (_ := Some tau)  = alpha <? tau
  >    alpha <? (_ := Hole)      = False
  
  < data Entry    = TY TyEntry | ...
  < type Context  = Bwd Entry
  < type Suffix   = Fwd TyEntry
  
  %if False
  
  > -- so we can line up the two previous lines
  > type Context  = Bwd Entry
  > type Suffix   = Fwd TyEntry
  
  %endif
  
  > (<><) :: Context -> Suffix -> Context
  > _Gamma <>< F0                   = _Gamma
  > _Gamma <>< (alpha := d :> _Xi)  = _Gamma :< TY (alpha := d) <>< _Xi
  
  %if False
  
  > infixl 8 <><
  
  %endif
  
  \vspace{6pt}
  \label{subfig:contextCode}
  }}}
  
  \subfigure[][Context manipulation monad]{\frame{\parbox{\linewidth}{\fixpars\medskip
  
  > type Contextual  = StateT (TyName, Context) Maybe
  
  > fresh :: TyDecl -> Contextual TyName
  > fresh d = do   (beta, _Gamma) <- get
  >                put (succ beta, _Gamma :< TY (beta := d))
  >                return beta
  
  > getContext :: Contextual Context
  > getContext = gets snd
  >
  > putContext :: Context -> Contextual ()
  > putContext _Gamma = do  beta <- gets fst
  >                         put (beta, _Gamma)
  >
  > modifyContext :: (Context -> Context) -> Contextual ()
  > modifyContext f = getContext >>= putContext . f
  
  \label{subfig:monadCode}
  }}}
  
  \end{minipage}
  \hspace{\medskipamount}
  \begin{minipage}[b]{0.5\linewidth}
  
  \subfigure[][Processing the context]{\frame{\parbox{\linewidth}{\fixpars\medskip
  
  > data Extension = Restore | Replace Suffix
  
  > onTop ::  (TyEntry -> Contextual Extension)
  >             -> Contextual ()
  > onTop f = do
  >     _Gamma :< vD <- getContext
  >     putContext _Gamma
  >     case vD of
  >         TY alphaD    -> do  m <- f alphaD
  >                             case m of
  >                                 Replace _Xi  -> modifyContext (<>< _Xi)
  >                                 Restore      -> modifyContext (:< vD)
  >         _            -> onTop f >> modifyContext (:< vD)
  
  > restore :: Contextual Extension
  > restore = return Restore
  
  > replace :: Suffix -> Contextual Extension
  > replace = return . Replace
  
  \label{subfig:onTopCode}
  }}}
  
  \subfigure[][Unification]{\frame{\parbox{\linewidth}{\fixpars\medskip
  
  > unify :: Type -> Type -> Contextual ()
  > unify (tau0 :-> tau1)  (upsilon0 :-> upsilon1)  = unify tau0 upsilon0 >> unify tau1 upsilon1
  > unify (V alpha)        (V beta)                 = onTop $
  >   \ (gamma := d) -> case
  >           (gamma == alpha,  gamma == beta,  d         ) of
  >           (True,            True,           _         )  ->  restore                                 
  >           (True,            False,          Hole      )  ->  replace (alpha := Some (V beta) :> F0)  
  >           (False,           True,           Hole      )  ->  replace (beta := Some (V alpha) :> F0)  
  >           (True,            False,          Some tau  )  ->  unify (V beta)   tau       >> restore   
  >           (False,           True,           Some tau  )  ->  unify (V alpha)  tau       >> restore   
  >           (False,           False,          _         )  ->  unify (V alpha)  (V beta)  >> restore   
  > unify (V alpha)        tau                               =   solve alpha F0 tau
  > unify tau              (V alpha)                         =   solve alpha F0 tau    
  
  > solve :: TyName -> Suffix -> Type -> Contextual ()
  > solve alpha _Xi tau = onTop $
  >   \ (gamma := d) -> let occurs = gamma <? tau || gamma <? _Xi in case
  >     (gamma == alpha,  occurs,  d             ) of
  >     (True,            True,    _             )  ->  fail "Occurrence detected!"
  >     (True,            False,   Hole          )  ->  replace (_Xi <+> (alpha := Some tau :> F0))
  >     (True,            False,   Some upsilon  )  ->  modifyContext (<>< _Xi)
  >                                                 >>  unify upsilon tau
  >                                                 >>  restore
  >     (False,           True,    _             )  ->  solve alpha (gamma := d :> _Xi) tau
  >                                                 >>  replace F0   
  >     (False,           False,   _             )  ->  solve alpha _Xi tau
  >                                                 >>  restore
  
  \label{subfig:unifyCode}
  }}}
  
  \end{minipage}
  
  \caption{Haskell implementation of unification}
  \label{fig:unifyCode}
  \end{figure*}
  
  Figure~\ref{fig:unifyCode} renders our unification algorithm in Haskell. 
  %%%\citeauthor{NaraschewskiN-JAR} formally proved correctness of \AlgorithmW\ 
     \AlgorithmW\ has been formally verified 
  in Isabelle/HOL by \citet{NaraschewskiN-JAR}, using a counter for fresh 
  %%%variable 
     name 
  generation and a monad to propagate failure; 
  we use similar techniques here.
  
  Figure~\ref{subfig:typeCode} implements types as a functor
  parameterised by a type of variable names;  
     for simplicity, we use integers.
  We compute free type variables using the typeclass |FTV| with membership
  function |(<?)|. 
  The typeclass instances are derived
  using |Foldable|, 
  thanks to a language
  extension in GHC 6.12 \citep{ghc_team_glorious_2009}. 
  %%%Thanks to a language
  %%%extension in GHC 6.12 \citep{ghc_team_glorious_2009} we can simply
  %%%derive the required typeclass instances. 
  %%%For simplicity, we use integers as names.
  %%%We can find free type variables using the typeclass |FTV| with membership
  %%%function |(<?)|. We get most of the required instances for free using |Foldable|.
  
  Figure~\ref{subfig:contextCode} defines context entries, contexts and suffixes.
  The types |Bwd| and |Fwd|, whose definitions are omitted, are backwards and forwards lists
  with |B0| for 
  %%%both empty lists 
     the empty list 
  and |:<| and |:>| for snoc and cons respectively.
  Lists are monoids under concatenation |(<+>)|; the \scare{fish}
  operator |(<><)| appends a suffix to a context. We %%%will 
  later extend |Entry| to
  handle term variables, so this definition is incomplete.
  
  Figure~\ref{subfig:monadCode} defines the |Contextual| monad of computations which mutate
  the context or fail. The |TyName| component is the next fresh 
  %%%type variable name 
     name 
  to use; it is an implementation detail not mentioned in the typing
  rules. The |fresh| function generates a 
  %%%fresh variable name and appends a 
     fresh name and appends its
  declaration to the context. Our choice of |TyName| makes it easy to
  choose a name fresh with respect to a |Context|.
  
  Figure~\ref{subfig:onTopCode} implements |onTop|, which delivers the
  typical access pattern for contexts, locally bringing the top variable
  declaration into focus and working over the remainder.  The local
  operation \(f\), passed as an argument, may |restore| the previous entry, or
  it may return a context extension (containing at least as much
  information as the entry that has been removed) with which to
  |replace| it.
  
  Figure~\ref{subfig:unifyCode} gives the actual implementations of unification
  and solution. Unification proceeds structurally over types. If it reaches a pair
  of variables, it examines the context, using 
  %%%the operator |onTop| 
     |onTop| 
  to pick out
  a variable declaration to consider. Depending on the variables, it %%%will
  then either succeeds, restoring the old entry or replacing it with a new one, 
  or continues %%%unifying 
  with an updated constraint.
  
  The |solve| function is called 
  %%%when a variable must be unified 
     to unify a variable 
  with a non-variable type. 
  It works similarly to 
  %%%unification of variables, 
     |unify| on variables, 
  but must accumulate a list of
  the type's dependencies and push them left through the context. It also performs
  the occurs check and 
  %%%invokes the monadic failure command 
     calls the monadic |fail| 
  if an illegal occurrence
  (leading to an infinite type) is detected.
  
  As an example, consider the behaviour of the algorithm when |unify| is called
  to solve $\alpha \arrow \beta \equiv \alpha' \arrow (\gamma \arrow \gamma)$:
  %
  % in the context $\hole{\alpha}, \hole{\beta}, \alpha' \defn \beta, \hole{\gamma}$.
  % The first case matches, decomposing the constraint structurally and first
  % invoking unify on $\alpha$ and $\alpha'$. The algorithm then traverses the
  % context, ignoring $\gamma$, then moving past $\alpha'$ by unifying $\alpha$ and
  % $\beta$. This succeds by defining $\beta$ to be $\alpha$, giving the context
  % $\hole{\alpha}, \beta \defn \alpha, \alpha' \defn \beta, \hole{\gamma}$.
  %
  % The second part of the structural decomposition now unifies $\beta$ with
  % $\gamma \arrow \gamma$. This calls |solve|, which collects $\gamma$ in the
  % dependency suffix, ignores $\alpha'$ and moves past $\beta$ by unifying
  % $\alpha$ and $\gamma \arrow \gamma$. Again this succeeds, giving the context
  % $\hole{\gamma}, \alpha \defn \gamma \arrow \gamma, \beta \defn \alpha,
  % \alpha' \defn \beta$.
  %
  \newcommand{\grot}[1]{\multicolumn{2}{@@{}l@@{}}{\ensuremath{[#1]}}}
  \[\begin{array}{@@{}c@@{}l@@{\,}l@@{\,}l@@{\,}l@@{\,}ll}
           &\hole{\alpha},& \hole{\beta},& \alpha' \defn \beta,&
       \hole{\gamma}&                     &\textrm{initially}
  \smallskip\\
   &
    \hole{\alpha},& \hole{\beta},& \alpha' \defn \beta,& \hole{\gamma},&
       [\alpha\equiv\alpha'] \\
   &
    \hole{\alpha},& \hole{\beta},& \alpha' \defn \beta,&
       [\alpha\equiv\alpha'],& \hole{\gamma} \\
   &
    \hole{\alpha},& \hole{\beta},&
       [\alpha\equiv\beta],& \alpha' \defn \beta,& \hole{\gamma}
  \smallskip \\
  \transto~ &\hole{\alpha},&
      \multicolumn{2}{@@{}c@@{\,}}{\beta \defn \alpha,\;\;}&
      \alpha' \defn \beta,&
      \hole{\gamma}                       &\alpha \equiv \alpha'
  \smallskip \\
   &
    \hole{\alpha},& \beta\defn\alpha,& \alpha' \defn \beta,& \hole{\gamma},&
       [\beta\equiv\gamma\arrow\gamma] \\
   &
    \hole{\alpha},& \beta\defn\alpha,& \alpha' \defn \beta,&
       \grot{ \hole{\gamma} \mid \beta\equiv\gamma\arrow\gamma} \\
   &
    \hole{\alpha},& \beta\defn\alpha,&
       \grot{ \hole{\gamma} \mid \beta\equiv\gamma\arrow\gamma} &
       \alpha' \defn \beta \\
   &
    \hole{\alpha},&
       \grot{\hole{\gamma} \mid \alpha\equiv\gamma\arrow\gamma}, &
       \beta\defn\alpha,& \alpha' \defn \beta
  \smallskip \\
  \transto~ &\hole{\gamma},&
   \multicolumn{2}{@@{}c@@{\,}}{\alpha \defn \gamma \arrow \gamma,}&
   \beta \defn \alpha,& \alpha' \defn \beta   &\beta \equiv \gamma \arrow \gamma 
  \end{array}\]
  The constraint decomposes into two constraints on variables. The first ignores
  $\gamma$, moves past $\alpha'$ by updating the constraint to
  $\alpha \equiv \beta$, then defines $\beta \defn \alpha$.
  The second calls |solve|, which collects $\gamma$ in the dependency suffix,
  ignores $\alpha'$, moves past $\beta$ by updating the constraint to
  $\alpha \equiv \gamma \arrow \gamma$, then defines $\alpha$ after pasting in
  $\gamma$.
  
  
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{Modelling statements-in-context\label{sec:stmts}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  %%%Having seen an 
     Given this 
  implementation of unification, let us try to understand it.
  We would like 
  %%%to give 
  a general picture of \scare{statements-in-context} that
  allows us to view unification and type inference in a uniform setting.
  What is the common structure?
  
  A \define{context} is a list of \define{declarations} assigning
  \define{properties} to
  %%%variables (here, in particular, type variables). 
     names (in particular, those of type variables). 
  We let $\Gamma, \Delta, \Theta$ range over contexts.
  The empty context is written $\emptycontext$. 
  Let $\V_\TY$ be a set of type
  variables and $\D_\TY$ the properties 
  %%%that may be given to them
     assignable to them: 
  the 
  %%%\scare{unknown variable} 
     \scare{unknown} 
  property $\,\hole{}$ and 
  %%%\scare{defined variable} 
     \scare{defined}
  properties $\,\defn{\tau}$, one for each type $\tau$.
  
  Later we %%%will 
  introduce corresponding definitions for term variables. Where
  needed we let $K \in \{ \TY, \TM \}$ represent an arbitrary sort of variable.
  We write $\decl{x}{D}$ for an arbitrary property, with $x \in \V_K$ and
  $D \in \D_K$. The set of variables of $\Gamma$ with sort $K$ is written
  $\V_K(\Gamma)$.
  
  We will build a set $\Ss$ of \define{statements}, assertions that can be judged
  in contexts. For now, the grammar of statements will be
  $$S \defsyn~ \valid
      ~||~ \tau \type
      ~||~ \tau \equiv \upsilon
      ~||~ S \wedge S,$$
  meaning (respectively) that the context is valid, $\tau$ is a type, the types
  $\tau$ and $\upsilon$ are equivalent, and both conjuncts hold.
  %%%Note that $\valid$ and $\wedge$ give a unit and product for statements.
  
  A statement has zero or more
  \define{parameters}, each of which has an associated \define{\sanity}, 
  i.e.\ a statement whose truth is presupposed for the original statement to make sense.
  The $\valid$ statement has no parameter and hence no \sanity s.
  In $\tau \type$, the parameter $\tau$ has \sanity\  $\valid$.
  The type equivalence statement $\tau \equiv \upsilon$ has two 
  %%%parameters; the \sanity s are 
     parameters, with \sanity s 
  $\tau \type$ and $\upsilon \type$ respectively.
  Finally, $S \wedge S'$ has parameters (and \sanity s) taken from $S$ and
  $S'$.
  
  Each declaration in the context causes some statement to hold.
  We maintain a map $\sem{\cdot}_K : \V_K \times \D_K \rightarrow \Ss$
  from declarations to statements. (Typically we will omit the subscript $K$.)
  The idea is that $\sem{\decl{x}{D}}$ is the statement that holds by virtue of the
  declaration $\decl{x}{D}$ in the context. For type variables, we define
  \[\begin{array}{r@@{\,}l}
  \sem{\hole{\alpha}} &\defmap \alpha \type \\ 
  \sem{\alpha \defn \tau} &\defmap \alpha \type \wedge \alpha \equiv \tau.
  \end{array}\]
  
  We can inspect the context in derivations using the inference rule
  $$\namer{Lookup}
    \Rule{\decl{x}{D} \in \Gamma}
         {\Gamma \entailsN \sem{\decl{x}{D}}}.$$
  Note the different turnstile 
  %%%symbol 
  in the conclusion of this rule.
  We write the \define{normal judgment} $\Gamma \entails S$
  to mean that the declarations in $\Gamma$ support the statement 
  %%%$S \in \Ss$.  
     \(S\). 
  We write the \define{neutral judgment} $\Gamma \entailsN S$ to
  mean that $S$ follows directly from 
  %%%applying 
  a fact in $\Gamma$.
  Neutral judgments capture exactly the valid appeals to declarations
  in the context, just as \scare{neutral terms} in $\lambda$-calculus are
  %%%applied variables. Variables are the \scare{atoms} of terms, and 
     applied variables, the \scare{atoms} of terms. 
  %%%appeals to declarations in 
     Such appeals to 
  the context are the atoms of derivations.
  
  The \name{Lookup} rule is our only means to extract information from the
  context, so we omit contextual plumbing (almost) everywhere else.
  %%%
  For example, embedding neutral judgments into the normal:
  $$\namer{Neutral}
    \Rule{\entailsN S}
         {\entails S}.$$
  
  \subsection{Validity of contexts}
  
  It is not enough for contexts to be lists of declarations: they must
  be well-founded, that is, each declaration should make sense in
  \emph{its} context.  A context is \define{valid} if it declares each name
  at most once, and the assigned property \(D\) is meaningful in the
  preceding context. Rules for the context validity statement
  $\valid$ are given in Figure~\ref{fig:contextValidityRules}.
  
  \begin{figure}[ht]
  \[\begin{array}{c}
  \mathframe{\Gamma \entails \valid}
  \smallskip\\
  \Axiom{\emptycontext \entails \valid}
  \qquad
  \Rule{\Gamma \entails \valid    \quad    \Gamma \entails \ok_K D}
       {\Gamma, \decl{x}{D} \entails \valid}
  \side{x \in \V_K \setminus \V_K(\Gamma)}
  \end{array}\]
  \caption{Rules for context validity}
  \label{fig:contextValidityRules}
  \end{figure}
  
  The map $\ok_K : \D_K \rightarrow \Ss$, for each $K \in \K$, 
  associates the statement of being meaningful, \(\ok_{K} D\), to each \(D\). 
  %%%For type properties:
     For types: 
  \[\begin{array}{r@@{\,}l}
  \ok_\TY (\,\hole{}) &\defmap \valid \\
  \ok_\TY (\,\defn{\tau}) &\defmap \tau \type
  \end{array}\]
  %%%Now we can define the context validity statement
  %%%$\valid$ as shown in Figure~\ref{fig:contextValidityRules}.
  
  Henceforth we %%%implicitly 
  assume that all contexts treated are valid,
  and ensure we only construct valid ones. We typically ignore 
  %%%the issue of fresh names, 
     freshness issues, 
  as our simple counter implementation suffices for most
  purposes.
  
  %%%DONE: don't do this. \TODO{Relate to traditional presentation - give intuition.}
  
  \subsection{Rules for establishing statements}
  
  Figure~\ref{fig:statementRules} gives rules for establishing statements other than
  $\valid$.
  We deduce that variables are types by 
  %%%looking up 
     lookup in 
  the context, but we need
  a structural rule for the $\arrow$ type constructor.
  
  %%%DONE: use \mathframe. \TODO{Fix rule box sizes.}
  
  \begin{figure}[ht]
  \[\begin{array}{c}
  \mathframe{\tau \type}\qquad\mathframe{\tau \equiv \upsilon}\qquad\mathframe{S \wedge S'}
  \smallskip\\
  \Rule{\tau \type   \quad   \upsilon \type}
       {\tau \arrow \upsilon \type}
  \qquad
  \Rule{\tau \type}
       {\tau \equiv \tau}
  \quad
  \Rule{\upsilon \equiv \tau}
       {\tau \equiv \upsilon}
  \quad
  \Rule{\tau_0 \equiv \tau_1
        \quad
        \tau_1 \equiv \tau_2}
       {\tau_0 \equiv \tau_2}
  \\
  \Rule{\tau_0 \equiv \upsilon_0
        \quad
        \tau_1 \equiv \upsilon_1}
       {\tau_0 \arrow \tau_1 \equiv \upsilon_0 \arrow \upsilon_1}
  \qquad
  \Rule{S \quad S'} {S \wedge S'}
    \quad
    \Rule{\entailsN S \wedge S'}
         {\entailsN S}
    \quad
    \Rule{\entailsN S \wedge S'}
         {\entailsN S'}
  \end{array}\]
  \caption{Rules for types, equivalence and conjunction}
  \label{fig:statementRules}
  \end{figure}
  
  Statement conjunction $S \wedge S'$ allows us to package multiple facts
  about a single variable, with a normal introduction rule (pairing) and neutral
  elimination rules (projections).
  This is but one instance of a general pattern: we add \emph{normal} introduction
  rules for composite forms, but supply
  eliminators only for statements 
  %%%which ultimately rest 
     ultimately resting 
  on (composite) hypotheses,
  obtained by \name{Lookup}. This forces
  derivations to be cut-free, facilitating reasoning by induction on
  derivations.
  Adding the corresponding projections for \emph{normal} judgments 
  would hamper us in obtaining a syntax-directed rule system. In any case, we shall
  ensure that the corresponding elimination rules are admissible, as is clearly
  the case for conjunction.
  
  
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{An information order for contexts\label{sec:stab}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  %%% \subsection{Information order}
  
  The transition from $\hole{\alpha}$ to $\alpha \defn \tau$ intuitively cannot
  falsify any existing equations.
  More generally, if we rely on the context to tell us what we may
  deduce about variables, then making contexts more informative must preserve
  %%%deductions. 
     derivability of judgments. 
  
  Let $\Gamma$ and $\Delta$ be contexts.
  A \define{substitution from $\Gamma$ to $\Delta$} is a map \(\delta\) from
  $\tyvars{\Gamma}$ to $\{ \tau ~||~ \Delta \entails \tau \type \}$.
  We could also substitute for term variables, and give a more general
  definition, but we omit this for simplicity.
  Substitutions act on types and statements as usual. 
  Composition of substitutions \(\theta, \delta\) is given by
  $(\theta \compose \delta) (\alpha) = \theta (\delta \alpha)$.
     The identity substitution is written \(\iota\). 
  %%%We write $\subst{\tau}{\alpha}{}$ for the substitution that maps 
     The substitution $\subst{\tau}{\alpha}{}$ maps 
  $\alpha$ to $\tau$ and 
  %%%other variables to themselves. 
     otherwise acts as \(\iota\). 
  
  Given $\delta$ from $\Gamma$ to $\Delta$, we 
  write the \define{information increase} 
     relation 
  $\delta : \Gamma \lei \Delta$ 
  and 
  say \define{$\Delta$ is more informative than $\Gamma$} 
  if for all $\decl{x}{D} \in \Gamma$, we have 
  $\Delta \entails \delta \sem{\decl{x}{D}}$. 
  That is, $\Delta$ supports the statements arising from declarations
  in $\Gamma$.
  We write $\Gamma \lei \Delta$ if 
  %%%$\iota : \Gamma \lei \Delta$, where  $\iota$ is the identity substitution. 
     $\iota : \Gamma \lei \Delta$.
  If $\delta : \Gamma, \Gamma' \lei \Theta$ we write $\restrict{\delta}{\Gamma}$
  for the restriction of $\delta$ to 
  %%%the type variables in $\Gamma$.
     \(\V_\TY(\Gamma)\). 
  
  We write $\delta \eqsubst \theta : \Gamma \lei \Delta$ if
  $\delta : \Gamma \lei \Delta$, $\theta : \Gamma \lei \Delta$
  and for all $\alpha \in \tyvars{\Gamma}$,
  $\Delta \entails \delta\alpha \equiv \theta\alpha$.
  We will sometimes just write $\delta \equiv \theta$ if the contexts involved
  are obvious.
  It is straightforward to verify that $\eqsubst$ is an equivalence relation
  for fixed contexts $\Gamma$ and $\Delta$, and that if
  $\delta \eqsubst \theta$ then
  $\Delta \entails \delta\tau \equiv \theta\tau$ for any $\Gamma$-type $\tau$.
  
  %%%This partial order on contexts suffices to ensure stability, as described
  %%%%%%in the following section, 
  %%%   below, 
  %Lemma~\ref{lei:preorder} below shows that 
  %\(\lei\) indeed defines a preorder under suitable stability assumptions, 
  %but in practice the algorithm works with a more constrained subrelation:  
  %we give up some freedom to achieve a more comprehensible
  %algorithm, which always uses \(\iota\). %%%the identity substitution.
  
  
  
  
  \subsection{Stable statements}
  
  A statement $S$ is \define{stable} if information
  increase preserves it, i.e., if
  $$\Gamma \entails S  \quad \mathrm{and}  \quad  \delta : \Gamma \lei \Delta
      \quad \Rightarrow \quad  \Delta \entails \delta S.$$
  That is, we can extend a simultaneous substitution on syntax to 
  %%%a simultaneous substitution on derivations. 
     one on derivations.
  Since we only consider valid contexts, the statement $\valid$ always holds,
  is invariant under substitution, hence is stable.
  
  We observe that neutral derivations always ensure stability:
  \begin{lemma}\label{lem:neutrality}
  If $\Gamma \entailsN S$ and $\delta : \Gamma \lei \Delta$ then
  $\Delta \entails \delta S$.
  \end{lemma}
  \proofsux\begin{proof}
  By 
  %%%structural induction on derivations. If the proof is by \name{Lookup}, then the result 
     induction on derivations. In the case of \name{Lookup}, it 
  holds by definition of information increase. Otherwise, the proof is
  by a neutral elimination rule, so the result follows by induction, and
  admissibility of the corresponding normal elimination rule.
  \end{proof}
  
  We have a standard way, effective by construction,  
  to prove stability of most 
  %%%statements. In each case we proceed by induction on 
     statements: we proceed by induction on
  %%%the structure of derivations. Where the \name{Neutral} rule is applied, 
     derivations. In the \name{Neutral} case, 
  stability holds by 
  Lemma~\ref{lem:neutrality}. Otherwise, we check the non-recursive hypotheses
  are stable and that recursive hypotheses occur in strictly positive positions,
  %%%hence are stable by induction. Applying this method shows that both 
     so are stable by induction. In this way we see that 
  $\tau \type$ and $\tau \equiv \upsilon$ are stable.
  
  \begin{lemma}[Conjunction preserves stability]\label{lem:stab-pres-conj}
  If $S$ and $S'$ are stable then $S \wedge S'$ is stable.
  \end{lemma}
  \proofsux\begin{proof}
  Suppose $S, S'$ are stable,  $\Gamma \entails S \wedge S'$, 
  and $\delta \!:\! \Gamma \lei \Delta$. In the \name{Neutral} case, 
  $\Delta \entails \delta (S \wedge S')$ by Lemma~\ref{lem:neutrality}.
  Otherwise $\Gamma \entails S$ and $\Gamma \entails S'$. 
  By stability, $\Delta \entails \delta S$ and $\Delta \entails \delta S'$,   
  so $\Delta \entails \delta (S \wedge S')$.
  \end{proof}
  %%%
  %%Thanks to stability, our information order is reasonable:
  We shall exploit the preorder structure of $\lei$, induced by stability.
  \begin{lemma}\label{lei:preorder}
  If $\sem{\decl{x}{D}}$ is stable for every declaration $\decl{x}{D}$, then
  the $\lei$ relation is a preorder, with reflexivity witnessed by
  the identity substitution $\iota : \Gamma \lei \Gamma$, and transitivity by
  composition:
  $$\delta : \Gamma \lei \Delta  ~~\text{and}~~  \theta : \Delta \lei \Theta
    \quad \Rightarrow \quad  \theta \compose \delta : \Gamma \lei \Theta.$$
  \end{lemma}
  \proofsux\begin{proof}
  Reflexivity follows immediately by applying the \name{Lookup} and
  \name{Neutral} rules.
  For transitivity, suppose that $\decl{x}{D} \in \Gamma$,
  then $\Delta \entails \delta \sem{\decl{x}{D}}$ since
  $\delta : \Gamma \lei \Delta$.
  Now by stability applied to $\delta \sem{\decl{x}{D}}$ using $\theta$, we have
  $\Theta \entails \theta\delta \sem{\decl{x}{D}}$ as required.
  \end{proof}
  
  %%\TODO{How do we use the following lemma?}
  %%\begin{lemma}
  %%\label{lem:composePreservesEquivSubst}
  %%If $\delta_0 \eqsubst \delta_1 : \Gamma \lei \Delta$
  %%and $\theta_0 \eqsubst \theta_1 : \Delta \lei \Theta$
  %%then $\theta_0 \compose \delta_0  \eqsubst  \theta_1 \compose \delta_1 :
  %%         \Gamma \lei \Theta$.
  %%\end{lemma}
  %%\proofsux\begin{proof}
  %%Fix $\alpha \in \tyvars{\Gamma}$. By definition of $\eqsubst$,
  %%$\Delta \entails \delta_0\alpha \equiv \delta_1\alpha$,
  %%so by stability,
  %%$\Theta \entails \theta_0\delta_0\alpha \equiv \theta_0\delta_1\alpha$.
  %%Moreover
  %%$\Theta \entails \theta_0\delta_1\alpha \equiv \theta_1\delta_1\alpha$,
  %%and hence
  %%$\Theta \entails \theta_0\delta_0\alpha \equiv \theta_1\delta_1\alpha$
  %%by transitivity.
  %%\end{proof}
  
  
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{Constraints: problems at ground mode\label{sec:constrs}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  We define a \define{constraint problem} to be a pair of a context $\Gamma$ and a statement
  $P$, where
  the \sanity s on the parameters of $P$ hold in $\Gamma$, but $P$ itself
  may not. A \define{solution} to such a problem is then an information increase 
  $\delta : \Gamma \lei \Delta$ such that
  $\Delta \entails \delta P$. 
     In this setting, the \define{unification} problem \((\Gamma, \tau \equiv \upsilon)\) 
  %%%is given $\Gamma$, $\tau$ and $\upsilon$ such that
     stipulates that 
  $\Gamma \entails \tau \type \wedge \upsilon \type$, and 
     a solution to the problem (a \define{unifier}) is given by 
  %%%must find 
  $\delta : \Gamma \lei \Delta$ such that
  $\Delta \entails \delta \tau \equiv \delta \upsilon$.
  
  We are interested in algorithms to solve problems, preferably in as
  general a way as possible (that is, by making the smallest information increase
  necessary to find a solution). 
     For the unification problem, this 
  corresponds to finding a most general
  unifier. We say
  the solution $\delta : \Gamma \lei \Delta$ is \define{minimal} if, for
  any other solution $\theta: \Gamma \lei \Theta$, there exists a
  substitution $\zeta : \Delta \lei \Theta$ such that
  $\theta \eqsubst \zeta \compose \delta$ (we say $\theta$ \emph{factors through}
  $\delta$ with \emph{cofactor} $\zeta$).
  
  Variables can become more informative either by definition or by substitution.
  Our algorithms exploit only the former, always choosing solutions of the form
  $\iota : \Gamma \lei \Delta$, but we show these minimal with respect to
  arbitrary information increase. Correspondingly,
  we write $\LEIStmt{\Gamma}{P}{\Delta}$ to mean that $(\Gamma, P)$ is a
  problem with minimal solution $\iota : \Gamma \lei \Delta$.
  
  Unsurprisingly, stability permits \emph{sound} sequential problem solving:
  $$\Rule{\iota:\leiStmt{\Gamma}{P}{\Delta}
         \quad  \iota:\leiStmt{\Delta}{Q}{\Theta}}
         {\iota:\leiStmt{\Gamma}{P \wedge Q}{\Theta}}.$$
  If $\Delta$ solves $P$ then any more
  informative context $\Theta$ also solves $P$. More surprisingly, composite
  problems acquire \emph{minimal} solutions similarly,
  allowing a \scare{greedy}  strategy.
  %
  % We can now state the following \scare{greedy} approach to finding minimal
  % solutions to such composite problems: find a minimal solution of problem $P$,
  % then extend it to (minimally) solve $Q$:
  %
  \begin{lemma}[The Optimist's lemma]
  \label{lem:optimist}
  The following is admissible:
  $$\Rule{\LEIStmt{\Gamma}{P}{\Delta}
         \quad  \LEIStmt{\Delta}{Q}{\Theta}}
         {\LEIStmt{\Gamma}{P \wedge Q}{\Theta}}.$$
  \end{lemma}
  
  \proofsux\begin{proof}[Sketch]
  Any solution $\phi : \Gamma \lei \Phi$ to $(\Gamma, P \wedge Q)$ must solve
  $(\Gamma, P)$, and hence factor through $\iota : \Gamma \lei \Delta$. But its
  cofactor solves $(\Delta, Q)$, and hence factors through
  $\iota : \Delta \lei \Theta$. For the detailed proof of a
  more general result, see Lemma~\ref{lem:optimistInference}.
  \end{proof}
  
  This sequential approach to problem solving is not the only decomposition
  justified by stability. \citeauthor{mcadam_unification_1998}'s account of
  unification \citeyearpar{mcadam_unification_1998} amounts to a concurrent,
  transactional decomposition of problems. The same context is extended via
  multiple different substitutions, which are then unified to produce a single
  substitution.
  
  
  
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{The unification algorithm, formally\label{sec:unif-formal}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  We now present the algorithm formally. The structural rule ensures that
  rigid problems, with $\arrow$ on each side, decompose
  into subproblems: by the Optimist's lemma, these we solve
  sequentially. Otherwise, we have either two variables, or a variable
  and a type. In each case, we ask how the rightmost type
  variable in the context helps us, and either solve
  the problem or continue leftward in the context with an updated constraint.
  When solving a variable with a type, we must accumulate
  the type's dependencies as we find them, performing the occurs check to
  ensure a solution exists.
  
  The rules in Figure~\ref{fig:unifyRules} define our unification algorithm. 
  The 
     \define{unify} 
  judgment $\algUnify{\Gamma}{\tau}{\upsilon}{\Delta}$ means that given inputs
  $\Gamma$, $\tau$ and $\upsilon$, 
     satisfying the input \sanity\ 
  $\Gamma \entails \tau \type \wedge \upsilon \type$, 
  unification succeeds, yielding output context $\Delta$. 
  %%%This is subject to the input \sanity\ 
  %%%$\Gamma \entails \tau \type \wedge \upsilon \type$.
  
  \newpage
  The 
     \define{solve} 
  judgment $\algInstantiate{\Gamma}{\alpha}{\tau}{\Xi}{\Delta}$
  means that given inputs $\Gamma$, $\Xi$, $\alpha$ and $\tau$,
  solving $\alpha$ with $\tau$ succeeds,  
  yielding output context $\Delta$. The idea is that the bar $(||)$ represents
  %%%progress through the context, 
     progress in examining context elements in order, 
  %%%and $\Xi$ contains dependencies of $\tau$ (which
  %%%must be placed before $\tau$ for it to be well-defined). 
     and $\Xi$ contains exactly those declarations on which $\tau$ depends.  
  Formally, the inputs 
  must satisfy \((\dag)\):
  
  \hspace*{0.1in}$\alpha \in \tyvars{\Gamma}$, ~
  $\tau$ is not a variable, \\ {}
  \hspace*{0.1in}$\Gamma, \Xi \entails \tau \type$, ~ 
  $\Xi$ contains only type variable declarations \\ {}
  \hspace*{0.1in}$\beta \in \tyvars{\Xi} \Rightarrow \beta \in \FTV{\tau, \Xi}$.
  
  %%%\TODO{Fix FTV!} 
  The set \(\FTV{\tau}\) records those variables occurring free in type \(\tau\); the notation extends to (sub-)contexts \(\FTV\Xi\) and composite objects \FTV{\tau, \Xi} in the obvious way. 
  Some context entries have no bearing on the problem at hand.
  We write $x \!\perp\! X$ ($x$ is orthogonal to set $X$ of type variables)
  if $x$ is not a type variable or not in $X$.
  
  The rules \name{Define} and \name{Expand} have
  symmetric counterparts, identical apart from interchanging the equated
  terms in the conclusion. Usually we will ignore these without loss of generality.
  
  \begin{figure}[ht]
  \[\begin{array}{c}
  \mathframe{\algUnify{\Gamma}{\tau}{\upsilon}{\Delta}}
  
  \smallskip\\
  \namer{Decompose}
  \Rule{\algUnify{\Gamma}{\tau_0}{\upsilon_0}{\Delta_0}
        \quad
        \algUnify{\Delta_0}{\tau_1}{\upsilon_1}{\Delta}}
      {\algUnify{\Gamma}{\tau_0 \arrow \tau_1}{\upsilon_0 \arrow \upsilon_1}{\Delta}}
  
  \smallskip\\
  
  \namer{Idle}
  % \Rule{\Gamma \entails \alpha \type}
  \Axiom{\algUnify{\Gamma, \alpha D}{\alpha}{\alpha}{\Gamma, \alpha D}}
  
  \smallskip\\ 
  
  \namer{Define}
  %\Rule{\Gamma \entails \beta \type}
  \Axiom{\algUnify{\Gamma, \hole{\alpha}}{\alpha}{\beta}{\Gamma, \alpha \defn \beta}}
  \side{\alpha \neq \beta}
  
  \smallskip\\ 
  
  \namer{Ignore}
  \Rule{\algUnify{\Gamma}{\alpha}{\beta}{\Delta}}
       {\algUnify{\Gamma, \decl{x}{D}}{\alpha}{\beta}{\Delta, \decl{x}{D}}}
  \side{x \perp \{\alpha, \beta\} }
  
  \smallskip\\ 
  
  \namer{Expand}
  \Rule{\algUnify{\Gamma}{\tau}{\beta}{\Delta}}
       {\algUnify{\Gamma, \alpha \defn \tau}{\alpha}{\beta}{\Delta, \alpha \defn \tau}}
  \side{\alpha \neq \beta}
  
  \smallskip\\ 
  
  \namer{Solve}
  \Rule{\algInstantiate{\Gamma}{\alpha}{\tau}{\emptycontext}{\Delta}}
       {\algUnify{\Gamma}{\alpha}{\tau}{\Delta}}
  %% \side{\tau \neq \alpha}
  \side{\tau \mathrm{~not~variable}}
  
  \bigskip\\
  
  \mathframe{\algInstantiate{\Gamma}{\alpha}{\tau}{\Xi}{\Delta}}
  
  \smallskip\\
  \namer{DefineS}
  % \Rule{\Gamma, \Xi \entails \tau \type}
  \Axiom{\algInstantiate{\Gamma, \hole{\alpha}}{\alpha}{\tau}{\Xi}
                     {\Gamma, \Xi, \alpha \defn \tau}}
  \side{\alpha \notin \FTV{\tau, \Xi}}
  
  \smallskip\\ 
  
  \namer{IgnoreS}
  \Rule{\algInstantiate{\Gamma}{\alpha}{\tau}{\Xi}{\Delta}}
       {\algInstantiate{\Gamma, \decl{x}{D}}{\alpha}{\tau}{\Xi}{\Delta, \decl{x}{D}}}
  \side{x \perp \FTV{\alpha, \tau, \Xi}}
  
  \smallskip\\
  
  \namer{ExpandS}
  \Rule{\algUnify{\Gamma, \Xi}{\upsilon}{\tau}{\Delta}}
       {\algInstantiate{\Gamma, \alpha \defn \upsilon}{\alpha}{\tau}{\Xi}
                     {\Delta, \alpha \defn \upsilon}}
  \side{\alpha \notin \FTV{\tau, \Xi}}
  
  \smallskip\\
  
  \namer{DependS}
  \Rule{\algInstantiate{\Gamma}{\alpha}{\tau}{\beta D, \Xi}{\Delta}}
       {\algInstantiate{\Gamma, \beta D}{\alpha}{\tau}{\Xi}{\Delta}}
  \side{\alpha \neq \beta, \beta \in \FTV{\tau, \Xi}}
  
  \end{array}\]
  \caption{Algorithmic rules for unification}
  \label{fig:unifyRules}
  \end{figure}
  
  Observe that no rule applies in the case \((\ddag)\) 
  $$\algInstantiate{\Gamma, \alpha D}{\alpha}{\tau}{\Xi}{\Delta}
  \mathrm{~with~} \alpha \in \FTV{\tau, \Xi},$$
  %%%so the algorithm fails in this case. 
     where the algorithm fails. 
  This is an occurs check failure: $\alpha$ and $\tau$ cannot unify 
  if $\alpha$ occurs in
  $\tau$ or in an entry that $\tau$ depends on, and $\tau$ is not a variable.
  Given the single type constructor symbol (the function arrow $\arrow$),
  there are no failures due to rigid-rigid mismatch. 
  To add these would not significantly complicate matters.
  
  The idea of assertions producing a resulting context goes back at least to
  \citet{pollack_implicit_1990}. \citet{Nipkow-Prehofer-JFP95} use (unordered)
  input and output contexts to pass information about \scare{sorts} for Haskell
  typeclass inference, alongside a conventional substitution-based presentation
  of unification.
  
  By exposing the contextual structure underlying unification we make
  termination of the algorithm evident. Each recursive appeal to
  unification (directly or via the solving process) either shortens the context
  left of the bar, shortens the overall
  context, or preserves the context and decomposes
  types~\citep{mcbride:unification}. We are correspondingly entitled to
  reason about the total correctness of unification by induction on the
  algorithmic rules.
  
  \subsection{Soundness and completeness}
  
  At present, order in the context is unimportant (providing dependencies are
  respected) but we will see in Section~\ref{sec:genloc} that the algorithm does
  keep entries as far right as possible, which will be necessary for generality
  of type inference.
  
  \begin{lemma}[Soundness and generality of unification]
  \label{lem:unifySound} ~
  \vspace*{-0.1in}\begin{enumerate}[(a)]
  \item Suppose $\algUnify{\Gamma}{\tau}{\upsilon}{\Delta}$. Then 
  $\tyvars{\Gamma} = \tyvars{\Delta}$ \\ and
  $\LEIStmt{\Gamma}{\tau \equiv \upsilon}{\Delta}$.
  \item Suppose 
  $\algInstantiate{\Gamma}{\alpha}{\tau}{\Xi}{\Delta}$. Then 
  $\tyvars{\Gamma, \Xi} = \tyvars{\Delta}$ and
  $\LEIStmt{\Gamma, \Xi}{\alpha \equiv \tau}{\Delta}$.
  \end{enumerate}
  
  \end{lemma}
  \proofsux\begin{proof}
  By induction on the structure of derivations.
  For each rule, we verify that it preserves the set of type variables and
  that $\Gamma \lei \Delta$.
  
  For minimality, it suffices to take some
  $\theta : \Gamma \lei \Theta$ such that
  $\Theta \entails \theta\tau \equiv \theta\upsilon$, and show
  $\theta : \Delta \lei \Theta$. As the type variables of $\Gamma$ are
  the same as $\Delta$, we simply note that definitions in $\Delta$ hold as
  equations in $\Theta$ for each rule that rewrites or solves the problem.
  
  The only rule not in this form is \name{Decompose}, but solutions to
  $\tau_0 \arrow \tau_1 \equiv \upsilon_0 \arrow \upsilon_1$ are exactly those
  that solve $\tau_0 \equiv \upsilon_0 \wedge \tau_1 \equiv \upsilon_1$,
  so it gives a minimal solution by the Optimist's lemma.
  \end{proof}
  
  We prove a straightforward lemma about the occurs check, and hence show
  completeness of unification.
  
  \begin{lemma}[Occurs check]
  \label{lem:occursCheck}
  Let $\alpha$ be a variable and $\tau$ a non-variable type such that
  $\alpha \in \FTV{\tau}$. There is no context $\Theta$ and substitution
  $\theta$ such that $\Theta \entails \theta\alpha \equiv \theta\tau$ or
  $\Theta \entails \theta\tau \equiv \theta\alpha$.
  \end{lemma}
  \proofsux\begin{proof}
  Suppose otherwise. Moreover, let $\Theta$ contain no definitions
  (by extending $\theta$ to substitute them out). Now,
  $\theta\alpha\equiv\theta\tau$ ensures $\theta\alpha=\theta\tau$,
  but as $\alpha \in \FTV{\tau}$ and $\tau$ is not $\alpha$, $\theta\tau$
  must be a proper subterm of itself, which is impossible.
  \end{proof}
  
  \begin{lemma}[Completeness of unification]
  \label{lem:unifyComplete}
  \begin{enumerate}[(a)]
  \item If 
  $\theta : \Gamma \lei \Theta$, \\
  $\Gamma \entails \upsilon \type \wedge \tau \type$  
  and
  $\Theta \entails \theta\upsilon \equiv \theta\tau$, then
  there is some context $\Delta$ such that
  $\algUnify{\Gamma}{\upsilon}{\tau}{\Delta}$.
  
  % with
  % $\theta : \Delta \lei \Theta$. That is, if a unifier for $\tau$ and $\upsilon$
  % exists, then the algorithm succeeds and delivers a most general unifier.
  
  \item Moreover, if $\theta : \Gamma, \Xi \lei \Theta$ is such that
  $\Theta \entails \theta\alpha \equiv \theta\tau$ and
  the input conditions \((\dag)\) are satisfied,
  then there is some context $\Delta$ such that
  $\algInstantiate{\Gamma}{\alpha}{\tau}{\Xi}{\Delta}$.
  \end{enumerate}
  \end{lemma}
  
  \proofsux\begin{proof} It suffices to show that the algorithm succeeds
  for every well-formed input in which a solution can exist. As the
  algorithm terminates, we proceed by induction on its call graph. Each
  step preserves solutions: if the equation in a conclusion can be
  solved, so can those in its hypothesis.
  
  The only case the rules omit is the case \((\ddag)\) where an illegal occurrence
  of a type variable is rejected. In this case, we are seeking to solve the
  problem $\alpha \equiv \tau$ in the context
  $\Gamma, \decl{\alpha}{D} ~||~ \Xi$ and we have $\alpha \in \FTV{\tau, \Xi}$.
  Substituting out the definitions in $\Xi$ from $\tau$, we obtain a type
  $\upsilon$ such that $\alpha \in \FTV{\upsilon}$, $\upsilon$ is not a variable
  and $\Gamma, \decl{\alpha}{D}, \Xi \entails \upsilon \equiv \tau$.
  Now the problem $\alpha \equiv \upsilon$ has the same solutions as
  $\alpha \equiv \tau$, but by Lemma~\ref{lem:occursCheck}, there are 
  %%%none. 
     no such. 
  \end{proof}
  
  
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{Specifying type inference\label{sec:spec-tyinf}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  We aim to implement type inference for the \hindleymilner\ system, so we need to
  introduce type schemes and the term language. We extend the grammar of statements
  to express additions to the context (binding statements), well-formed schemes,
  type assignment and scheme assignment. The final grammar will be:
  \[\begin{array}{r@@{\,}l}
  S \defsyn~ \valid
      &~||~ \tau \type
      ~||~ \tau \equiv \upsilon
      ~||~ S \wedge S \\
      &~||~ \Sbind{\decl{x}{D}}{S}
      ~||~ \sigma \scheme
      ~||~ t : \tau
      ~||~ s \hasscheme \sigma.
  \end{array}\]
  
  \subsection{Binding statements}
  
  To account for schemes and type assignment, we need a controlled way
  to extend the context.
  %%%If $S$ is a statement and $\decl{x}{D}$ is a declaration, then we define the 
     Given statement $S$ and declaration $\decl{x}{D}$, then we define the
  %%%binding statement $\Sbind{\decl{x}{D}}{S}$. 
     statement $\Sbind{\decl{x}{D}}{S}$, binding \(x\) in \(S\), subject to \(D\). 
  
  We give a generic introduction rule,
  but we make use of neutral elimination only for type variables.
  \[\begin{array}{c}
  \Rule{\Gamma \entails \ok_K D    \quad    \Gamma, \decl{y}{D} \entails \subst{y}{x} S}
       {\Gamma \entails \Sbind{\decl{x}{D}}{S}}
  \side{y \in \V_K \setminus \V_K(\Gamma)}
  \smallskip\\
  \Rule{\entailsN \Sbind{\alpha D}{S}
        \quad
        \entails \subst{\tau}{\alpha}{\sem{\decl{\alpha}{D}}}}
       {\entailsN \subst{\tau}{\alpha}{S}}
  \side{D \in \D_\TY}
  \end{array}\]
  The corresponding normal rule is admissible. If
  $\Gamma \entails \Sbind{\decl{\alpha}{D}}{S}$ by the introduction rule, then
  $\Gamma, \decl{\beta}{D} \entails \subst{\beta}{\alpha} S$ where $\beta$ is fresh.
  But $\Gamma \entails \subst{\tau}{\alpha}{\sem{\decl{\alpha}{D}}}$ implies
  $\Gamma \entails \subst{\tau}{\beta}{\sem{\decl{\beta}{D}}}$ and hence
  we can obtain a proof of $\Gamma \entails \subst{\tau}{\alpha} S$ by replacing
  every appeal to \name{Lookup} $\beta$ in the proof of 
  $\Gamma, \decl{\beta}{D} \entails \subst{\beta}{\alpha} S$
  with the proof of
  $\Gamma \entails \subst{\tau}{\beta}{\sem{\decl{\beta}{D}}}$.
  As a consequence, Lemma~\ref{lem:neutrality} still holds.
  
  While the introduction rule allows renaming to ensure freshness, in practice we
  will ignore this and assume that the bound variable name is always fresh for the
  context.
  
  \begin{lemma}[Binding preserves stability]\label{lem:stab-pres-bind}
  If $\decl{x}{D}$ is a declaration and both $\ok_K D$ and $S$ are stable, then
  $\Sbind{\decl{x}{D}}{S}$ is stable.
  \end{lemma}
  \proofsux\begin{proof}
  Suppose $S$ is stable, $\delta : \Gamma \lei \Delta$, $x$ chosen
  fresh for $\Gamma$ and $\Delta$, and 
  $\Gamma \entails \Sbind{\decl{x}{D}}{S}$.  
  %%%If the proof is by \name{Neutral} then 
     In the \name{Neutral} case,  
  the result follows by Lemma~\ref{lem:neutrality}.
  Otherwise, $\Gamma \entails \ok_K D$ and 
  %%%$\Gamma, \decl{y}{D} \entails \subst{y}{x}S$ for fresh $y$.
     $\Gamma, \decl{x}{D} \entails S$.
  By stability and inductive hypothesis, $\Delta \entails \delta (\!\ok_K D)$.
  % Let $\delta' = \subst{x}{x}{\delta}$, then
  Now we have $\delta : \Gamma, \decl{x}{D} \lei \Delta, \decl{x}{(\delta D)}$
  %(with $y$ mapped to itself)
  so we also have $\Delta, \decl{x}{(\delta D)} \entails \delta S$ by stability of $S$.
  Hence $\Delta \entails \Sbind{\decl{x}{(\delta D)}}{\delta S}$
  and so $\Delta \entails \delta (\Sbind{\decl{x}{D}}{S})$.
  \end{proof}
  
  We 
  %%%write 
     extend the binding notation to 
  $\Sbind{\Xi}{S}$, where $\Xi$ is a list of declarations, 
  %%%defining 
     by:  
  $\Sbind{\emptycontext}{S} \defmap S$ and
  $\Sbind{(\Xi, \decl{x}{D})}{S} \defmap \Sbind{\Xi}{(\Sbind{\decl{x}{D}}{S})}$.
  
  If $S$ is a statement and $C$ is a sanity condition for one of its parameters,
  the statement $\Sbind{x D}{S}$ has sanity condition $\Sbind{x D}{C}$ for the
  corresponding parameter.
  
  \subsection{Type schemes}
  
  To handle let-polymorphism, the context must assign type schemes to term
  variables, rather than monomorphic types.
  A \define{type scheme} $\sigma$ is a type wrapped in one or more $\forall$
  quantifiers or $\letS{\cdot}{\cdot}{\cdot}$ bindings, with the syntax
  $$\sigma \defsyn \gendot{\tau} ~||~ \forall\alpha~\sigma ~||~ \letS{\alpha}{\tau}{\sigma}.$$
  We use explicit definitions in type schemes to avoid the need for substitution
  in the type inference algorithm. 
  
  Schemes arise by discharging a context suffix (a list of type variable
  declarations) over a type, and any scheme can be viewed in this way. We write
  $\gen{\Xi}{\tau}$ for the generalisation of the type $\tau$ over the suffix of
  type variable declarations $\Xi$, defined by
  %\begin{align*}
  %\emptycontext         &\genarrow \tau = \gendot{\tau}  \\
  %\hole{\alpha}, \Xi    &\genarrow \tau = \forall\alpha~\gen{\Xi}{\tau}  \\
  %\alpha \defn \upsilon, \Xi &\genarrow \tau = \letS{\alpha}{\upsilon}{\gen{\Xi}{\tau}}
  %\end{align*}
  \[
  \begin{array}{r@@{\,}l}
  \emptycontext         &\genarrow \tau \defmap \gendot{\tau}  \\
  \hole{\alpha}, \Xi    &\genarrow \tau \defmap \forall\alpha~\gen{\Xi}{\tau}  \\
  \alpha \defn \upsilon, \Xi &\genarrow \tau \defmap \letS{\alpha}{\upsilon}{\gen{\Xi}{\tau}}
  \end{array}
  \]
  
  The statement $\sigma \scheme$ is then defined by
  $$\gen{\Xi}{\tau} \scheme \defmap \Sbind{\Xi}{\tau \type}.$$
  The \sanity\  is just $\valid$, as for $\tau \type$.
  
  \subsection{Terms and type assignment}
  
  Now we are in a position to reuse the framework already
  introduced, defining the sort $\TM$, with 
  $\V_\TM$ a set of term variables and $x$ ranging over $\V_\TM$.
  Term variable properties $\D_\TM$ are scheme assignments of the form
  $\,\asc \sigma$, with
  $\ok_\TM (\,\asc \sigma) = \sigma \scheme$.
  
  Let $s$, $t$, $w$ range over the set of terms with syntax 
  $$t \defsyn x ~||~ t~t ~||~ \lambda x . t ~||~ \letIn{x}{t}{t}.$$
  
  The type assignment statement $t : \tau$ is established by the
  rules in Figure~\ref{fig:typeAssignmentRules}. It has two parameters $t$ and
  $\tau$ with \sanity s $\valid$ and $\tau \type$ respectively.
  We overload notation to define the scheme assignment statement
  $t \hasscheme \sigma$ by
  $$t \hasscheme \gen{\Xi}{\tau} \defmap \Sbind{\Xi}{t : \tau}.$$
  Note this gives the parameters $t$ and $\sigma$ \sanity s
  $\valid$ and $\sigma \scheme$ as one might expect.
  This overloading is 
  reasonable because the meaning of $\hasscheme$ is clear from
  the context, and the interpretation of declarations embeds them in
  statements:
  $$\sem{x \asc \sigma}_\TM \defmap x \hasscheme \sigma.$$
  
  \begin{figure}[ht]
  \[\begin{array}{c}
  \mathframe{t : \tau}
  
  \smallskip\\
  \Rule{\Sbind{x \asc \gendot{\upsilon}}{t : \tau}}
       {\lambda x.t : \upsilon \arrow \tau}
  \qquad
  \Rule{f : \upsilon \arrow \tau
        \quad
        a : \upsilon}
       {f a : \tau}
  
  \smallskip\\
  
  \Rule{
        s \hasscheme \sigma
        \quad
        \Sbind{x \asc \sigma}{w : \tau}
       }
       {\letIn{x}{s}{w} : \tau}
  \qquad
  \Rule{t : \tau
        \quad
        \tau \equiv \upsilon}
       {t : \upsilon}
  \end{array}\]
  \caption{Declarative rules for type assignment}
  \label{fig:typeAssignmentRules}
  \end{figure}
  
  The definition of
  $\Gamma \lei \Delta$ requires $\Delta$ to assign a term variable all the types
  that $\Gamma$ assigns it, but allows $x$ to become more polymorphic
  and acquire new types.  This notion certainly retains stability:
  every variable lookup can be simulated in the more general context.
  However, it allows arbitrary generalisation of the schemes assigned to term
  variables which are incompatible with the known and intended value of
  those variables.
  
  As \citet{wells_principal_typings_2002} points out, \hindleymilnershort\ 
  type inference is not in this respect compositional. He carefully
  distinguishes principal \emph{typings}, given the right to demand more
  polymorphism, from Milner's principal \emph{type schemes} and analyses
  how the language of types must be extended to express principal
  typings.
  
  We, too, note this distinction. We cannot hope to find principal types
  with respect to $\lei$, so we will define a subrelation $\leiR$ to capture
  Milner's compromise, requiring that, for \(\delta : \Gamma \lei \Delta\), 
  $$x \asc \sigma \in \Gamma ~\Rightarrow~ x \asc \delta\sigma \in \Delta.$$
  If $\Gamma \leiR \Delta$, then
  $\Delta$ assigns the \emph{same} type schemes to term variables as $\Gamma$
  does (modulo substitution). Since the unification algorithm ignores term
  variables, it must preserve this property.
  % all the previous results hold if we
  % replace $\lei$ with $\leiR$ throughout.
  This is not the full story, however; we need to extend the notion of
  context to complete the definition of the $\leiR$ relation.
  
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{Generalising \emph{local} type variables\label{sec:genloc}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  %%%\subsection{Preserving order in the context}
  
  We have previously observed, but not yet exploited, the importance of
  declaration order in the context, and that we move declarations left as
  little as possible. Thus rightmost entries are those most local to the problem
  we are solving. This will be useful when we come to implement type inference
  for the `let' construct, as we want to generalise over \scare{local} type
  variables but not \scare{global} variables.
  
  In order to keep track of locality in the context, we need another kind of
  context entry: the $\fatsemi$ separator. We add a new validity rule 
  $$
  \Rule{\Gamma \entails \valid}
       {\Gamma \fatsemi \entails \valid}.
  $$
  
  %%%The $\leiR$ relation must be defined to respect the $\fatsemi$ divisions. 
     We must then refine the $\leiR$ relation to respect these $\fatsemi$ divisions.
  Let $\semidrop$ be the partial function from contexts $\Gamma$ and natural numbers $n$ which truncates $\Gamma$ after $n$
  $\fatsemi$ separators, provided $\Gamma$ contains at least $n$ such: 
  \[\begin{array}{r@@{\,}l}
  \Xi \semidrop 0 &\defmap \Xi  \\
  \Xi \fatsemi \Gamma \semidrop 0 &\defmap \Xi  \\
  \Xi \fatsemi \Gamma \semidrop n+1 &\defmap \Xi \fatsemi (\Gamma \semidrop n)  \\
  \Xi \semidrop n+1 &~\mathrm{undefined}
  \end{array}\]
  %
  We write $\delta : \Gamma \leiR \Delta$ if $\delta$ is a substitution from
  $\Gamma$ to $\Delta$ such that, for all
  $\decl{x}{D} \in \Gamma \!\semidrop\! n$, we have that
  $\Delta \!\semidrop\! n$ is defined,
  $\Delta \!\semidrop\! n \entails \delta \sem{\decl{x}{D}}$ and
  $$x \asc \sigma \in \Gamma ~\Rightarrow~ x \asc \delta\sigma \in \Delta.$$
  We thus make the $\fatsemi$-separated sections of $\Gamma$ and
  $\Delta$ correspond, so that declarations in the first $n$ sections of
  $\Gamma$ can be interpreted over the first $n$ sections of $\Delta$. As
  a consequence, \scare{moving left of \(\fatsemi\)} is an irrevocable
  commitment. In particular, we note that
  \[
  \iota : \Gamma\fatsemi\hole{\alpha},\Delta
     \leiR \Gamma,\hole{\alpha}\fatsemi\Delta
  \;\;\mbox{but}\;\;
  \iota : \Gamma,\hole{\alpha}\fatsemi\Delta
     \not\leiR \Gamma\fatsemi\hole{\alpha},\Delta
  \]
  
  Note also that if $\delta : \Gamma \fatsemi \Gamma' \leiR \Delta \fatsemi \Delta'$,
  where $\Gamma$ and $\Delta$ contain the same number of $\fatsemi$ separators,
  then $\restrict{\delta}{\Gamma} : \Gamma \leiR \Delta$.
  
  % It is fairly straightforward to verify that the previous results for $\lei$ 
  % hold for its sub-relation $\leiR$.
  
  When the contexts contain only type variables, the two relations $\lei$ and
  $\leiR$ coincide; the latter is a proper subrelation if the contexts also 
  contain term variables.
  Hence, most of the previous results hold if we replace $\lei$ with $\leiR$
  throughout.
  
  
  \subsection{Amending the unification algorithm}
  
  Replacing $\lei$ with $\leiR$ makes extra work only in the unification
  algorithm, because it acts structurally on contexts, which may now contain
  $\fatsemi$ separators. We complete the algorithmic rules:
  \[\begin{array}{c}
  \namer{Skip}
  \Rule{\algUnify{\Gamma}{\alpha}{\beta}{\Delta}}
       {\algUnify{\Gamma \fatsemi}{\alpha}{\beta}{\Delta \fatsemi}}
  \smallskip\\
  \namer{Repossess}
  \Rule{\algInstantiate{\Gamma}{\alpha}{\tau}{\Xi}{\Delta}}
       {\algInstantiate{\Gamma \fatsemi}{\alpha}{\tau}{\Xi}{\Delta \fatsemi}}
  \end{array}\]
  
  We must correspondingly update the induction in Lemma~\ref{lem:unifySound} to
  show that adding the new rules preserves soundness and generality. For the
  \name{Skip} rule, correctness follows immediately from this lemma:
  
  \begin{lemma}
  If $\LEIRStmt{\Gamma}{S}{\Delta}$ then $\LEIRStmt{\Gamma \! \fatsemi}{S}{\Delta \fatsemi}$.
  \end{lemma}
  \proofsux\begin{proof}
  If $\Gamma \leiR \Delta$ then $\Gamma \fatsemi \leiR \Delta \fatsemi$ by
  definition. If $\Delta \entails S$ then $\Delta \fatsemi \entails S$ since the
  \name{Lookup} rule is the only one that extracts information from the context,
  and it ignores the $\fatsemi$.
  
  Now let $\theta : \Gamma \fatsemi \leiR \Theta \fatsemi \Xi$ be such that
  $\Theta \fatsemi \Xi \entails S$. By definition of $\leiR$, we must have
  $\theta : \Gamma \leiR \Theta$, so by minimality there exists
  $\zeta : \Delta \leiR \Theta$ with $\theta \eqsubst \zeta \compose \iota$.
  Then $\zeta : \Delta \fatsemi \leiR \Theta \fatsemi \Xi$ and we are done.
  \end{proof}
  
  The \name{Repossess} rule is so named because it moves
  declarations in $\Xi$ to the left of the $\fatsemi$ separator,
  thereby \scare{repossessing} them. To guarantee a solution
  most general with respect to \(\leiR\),
  we show that $\Xi$'s leftward journey is really necessary.
  
  \begin{lemma}[Soundness and generality of the \name{Repossess} rule]
  Suppose $\algInstantiate{\Gamma \fatsemi}{\alpha}{\tau}{\Xi}{\Delta \fatsemi}$. 
  Then $\tyvars{\Gamma \fatsemi \Xi} = \tyvars{\Delta \fatsemi}$ and
  $\LEIRUnify{\Gamma \fatsemi \Xi}{\alpha}{\tau}{\Delta \fatsemi}$.
  \end{lemma}
  \proofsux\begin{proof}
  We extend the structural induction in Lemma~\ref{lem:unifySound} with an extra
  case. The only proof of
  $\algInstantiate{\Gamma \! \fatsemi}{\alpha}{\tau}{\Xi}{\Delta \fatsemi}$
  is by \name{Repossess}, so inversion gives
  $\algInstantiate{\Gamma}{\alpha}{\tau}{\Xi}{\Delta}$.
  By induction, $\tyvars{\Gamma, \Xi} = \tyvars{\Delta}$ and
  $\LEIRUnify{\Gamma, \Xi}{\alpha}{\tau}{\Delta}$.
  
  We immediately observe that $\Gamma \fatsemi \Xi \leiR \Delta \fatsemi$,
  \, 
  $\Delta \fatsemi \entails \alpha \equiv \tau$ and
  $$\tyvars{\Gamma \fatsemi \Xi} = \tyvars{\Gamma, \Xi} = \tyvars{\Delta}
      = \tyvars{\Delta \fatsemi}.$$
  
  For minimality, suppose
  $\theta : \Gamma \fatsemi \Xi \leiR \Theta \fatsemi \Phi$
  and $\Theta \fatsemi \Phi \entails \theta\alpha \equiv \theta\tau$.
  Observe that  $\alpha \in \tyvars{\Gamma}$ and
  $\beta \in \tyvars{\Xi}  \Rightarrow  \beta \in \FTV{\tau, \Xi}$
  by the conditions for the algorithmic judgment.
  Now $\theta\alpha$ is a $\Theta$-type and $\theta\tau$ is equal to it,
  so the only declarations in $\Phi$ that $\theta\tau$ (hereditarily) depends on
  must be definitions over $\Theta$. But all the variables declared in $\Xi$ are
  used in $\tau$, so there is a substitution
  $\psi : \Gamma \fatsemi \Xi \leiR \Theta \fatsemi$
  that agrees with $\theta$ on $\Gamma$ and maps variables in $\Xi$ to their
  definitions in $\Theta$.
  
  Hence $\psi : \Gamma, \Xi \leiR \Theta$ and
  $\Theta \entails \psi\alpha \equiv \psi\tau$, so by hypothesis there exists
  $\zeta : \Delta \leiR \Theta$ such that
  $\psi \eqsubst \zeta \compose \iota : \Gamma, \Xi \leiR \Theta$.
  Note that $\psi \eqsubst \theta : \Gamma \fatsemi \Xi \leiR \Theta \fatsemi \Phi$.
  Then $\zeta : \Delta \fatsemi \leiR \Theta \fatsemi \Phi$
  and
  $\psi \eqsubst \zeta \compose \iota :
      \Gamma \fatsemi \Xi \leiR \Theta \fatsemi \Phi$,
  so
  $\theta \eqsubst \zeta \compose \iota :
      \Gamma \fatsemi \Xi \leiR \Theta \fatsemi \Phi$.
  \end{proof}
  
  
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{Type inference problems and their solutions\label{sec:tyinf}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  Type inference involves making the statement $t : \tau$ hold, but
  unlike unification, the type should
  be an \emph{output} of problem-solving along with the solution context. We need
  a more liberal definition than that of constraint problems.
  We associate a \define{mode} with each parameter in a statement: either
  \scare{input} or \scare{output}. For simplicity, assume statements always have
  one parameter of each mode (which may be trivial or composite).
  We now extend the apparatus of minimal solutions to problems with outputs.
  
  What can outputs be, and how can we compare them?
  An \define{output set} is a set $B$ closed under
  substitution, such that every context $\Gamma$ induces a preorder
  $\leParam{}{\Gamma}{\cdot}{\cdot}$ on $B$ which is congruent
  with respect to the definitional equality, i.e.\ if
  $\Gamma \entails \alpha \equiv \tau \wedge \beta \equiv \upsilon$, then
  $\leParam{}{\Gamma}{b}{c}$ if and only if 
  $\leParam{}{\Gamma}{\subst{\tau}{\alpha} b}{\subst{\upsilon}{\beta} c}$.
  This is easily verified for each preorder we use.
  %% \TODO{Other conditions?}
  
  We need subsequent problems to depend on the results of earlier problems,
  threading the output from one into the input of the next. Thus we must index
  problems to determine the input parameters. 
  
  Let $A$ be an output set.
  An \define{$A$-indexed problem family $Q$ for $B$} is an output set $B$ and a
  family of input parameters for a statement, indexed by elements of $A$, such
  that the \define{simplicity condition} holds:
  for all $a, a' \in A$, contexts $\Gamma$ and output parameter values $b \in B$,
  $$\leParam{}{\Gamma}{a}{a'} ~\wedge~ \Gamma \entails \iprobstmt{Q}{a'}{b}
      \quad\Rightarrow\quad  \Gamma \entails \iprobstmt{Q}{a}{b}.$$
  We write $\iprobstmt{Q}{a}{b}$ for the statement with input at index $a$ and
  output value $b$, and $\iprobcond{Q}{a}$ for the \sanity s on the input
  parameters at index $a$.
  We use $\leParam{Q}{\Gamma}{\cdot}{\cdot}$ for the preorder on the output set.
  The idea behind this contravariant condition is that the preorder
  represents specialisation of solutions, so if a problem can be solved with an
  input $a'$ then it can be solved with the more general $a$.
  
  Now we can generalise the notion of constraint problem and its solution.
  An \define{inference problem} consists of a context $\Gamma$, an $A$-indexed
  problem family $Q$ and an index $a \in A$ such that
  $\Gamma \entails \iprobcond{Q}{a}$.
  A \define{solution} of it consists of an information increase
  $\delta : \Gamma \leiR \Delta$ and a value for the output parameter $b \in B$
  such that $\Delta \entails \iprobsubst{\delta}{Q}{a}{b}$.
  
  The preorder on outputs induces a
  preorder on context-output pairs, with $\delta : \leiRParam{\Gamma}{a}{\Delta}{b}$ if
  $\delta : \Gamma \leiR \Delta$ and $\leParam{}{\Delta}{\delta a}{b}$.
  We will look for minimal solutions with respect to this preorder,
  and write $\LEIRProb{\Gamma}{Q[a]}{\Delta}{b}$ if
  $(\iota : \Gamma \leiR \Delta, b)$ is a solution (i.e.\ $\Delta \entails \iprobstmt{Q}{a}{b}$)
  and for all solutions $(\theta : \Gamma \leiR \Theta, c)$ we have
  $\zeta : \leiRParam{\Delta}{b}{\Theta}{c}$ for some $\zeta$ such that
  $\theta \eqsubst \zeta \compose \iota$.
  As with unification, we only use the identity substitution
  but are minimal with respect to any solution.
  
  A \define{problem $P$ for $B$} is a problem family indexed by the 
  unit set with the trivial preorder. We simply omit the index in this case.
  
  \subsection{The Optimist's lemma}
  
  Let $P$ be a problem for $A$ and let $Q$ be an $A$-indexed family for $B$.
  Then the conjunction $\pconj{P}{x}{Q}$ is a problem for $A \times B$
  with statement
  $$\probstmt{(\pconj{P}{x}{Q})}{(a, b)} \defmap \probstmt{P}{a} \wedge \iprobstmt{Q}{a}{b}$$
  and the preorder defined pointwise.
  This \scare{dependent} generalisation of $P \wedge Q$
  allows the output of $P$ to be threaded into $Q$.
  The Optimist's lemma correspondingly generalises:
  
  \begin{lemma}[The Optimist's lemma for inference problems]
  \label{lem:optimistInference}
  %The following inference rule is admissible:
  $$\Rule{\LEIRProb{\Gamma}{P}{\Delta}{b}
         \quad  \LEIRProb{\Delta}{Q[b]}{\Theta}{c}}
         {\LEIRProb{\Gamma}{(\pconj{P}{x}{Q})}{\Theta}{(b, c)}}.$$
  \end{lemma}
  \proofsux\begin{proof}
  Since $\Gamma \leiR \Delta$ and $\Delta \leiR \Theta$,
  we have $\Gamma \leiR \Theta$ by (updating) Lemma~\ref{lei:preorder}.
  Furthermore, $\Theta \entails \probstmt{(\pconj{P}{x}{Q})}{(b, c)}$ since
  $\Theta \entails \iprobstmt{Q}{b}{c}$ by assumption
  and $\Delta \entails \probstmt{P}{b}$ so
  stability gives $\Theta \entails \probstmt{P}{b}$.
  
  For minimality, suppose there is a solution
  $(\phi : \Gamma \leiR \Phi, (b', c'))$, so
  $\Phi \entails \probsubst{\phi}{P}{b'}$ and
  $\Phi \entails \iprobstmt{(\phi Q)}{b'}{c'}$.
  Since $\LEIRProb{\Gamma}{P}{\Delta}{b}$, there exists
  $\zeta : \Delta \leiR \Phi$
  with $\leParam{}{\Phi}{\zeta b}{b'}$ and $\phi \eqsubst \zeta \compose \iota$.
  By the simplicity condition,
  $\Phi \entails \iprobstmt{(\phi Q)}{\zeta b}{c'}$
  and hence $\Phi \entails \iprobsubst{\zeta}{Q}{b}{c'}$.
  But $\LEIRProb{\Delta}{Q[b]}{\Theta}{c}$, so there exists
  $\xi : \Theta \leiR \Phi$ such that $\leParam{}{\Phi}{\xi c}{c'}$
  and $\zeta \eqsubst \xi \compose \iota$.
  Hence $\leParam{}{\Phi}{\xi (b, c)}{(b', c')}$
  so $\xi : \leiRParam{\Theta}{(b, c)}{\Phi}{(b', c')}$, and
  $\phi \eqsubst \zeta \compose \iota
        \eqsubst (\xi \compose \iota) \compose \iota
        \eqsubst \xi \compose \iota$.
  \end{proof}
  
  
  
  \subsection{The Generalist's lemma}
  
  We have considered problems with abstract inputs and outputs, but
  which 
  %sets of
  concrete values do we actually use? We want to
  solve type inference problems, so we are interested in types and
  type schemes.
  
  The statement $t \hasscheme \sigma$ defines 
  a problem for the set of schemes with preorder given by
  $\leParam{\hasscheme}{\Gamma}{\gen{\Xi}{\tau}}{\gen{\Psi}{\upsilon}}$
  if there is some $\psi : \Gamma \fatsemi \Xi \leiR \Gamma \fatsemi \Psi$
  such that $\Gamma \fatsemi \Psi \entails \psi \tau \equiv \upsilon$
  and $\restrict{\psi}{\Gamma} \eqsubst \iota$. That is,
  $\leParam{\hasscheme}{\Gamma}{\sigma}{\sigma'}$
  if $\sigma$ is a more general type scheme than $\sigma'$.
  
  Since types are just schemes with no quantifiers, we instantiate the above
  definition with $\Xi = \emptycontext = \Psi$, to get a preorder on types:
  $\leParam{:}{\Gamma}{\tau}{\upsilon}$
  if $\Gamma \entails \tau \equiv \upsilon$.
  
  Thus the type inference problem is given by a context $\Gamma$ and a term
  parameter $t$ as input to the type assignment statement. Following the
  definitions, a solution is an information increase
  $\delta : \Gamma \leiR \Delta$ and a type $\tau$ such that
  $\Delta \entails \tau \type \wedge t : \tau$. A solution with output $\tau$ is
  minimal if, given any other solution, we can find a substitution that unifies $\tau$
  and the other type: that is, $\tau$ is a principal type.
  
  In the type inference algorithm, we will use $\fatsemi$ to determine what can be
  generalised, based on the following lemma.
  
  \begin{lemma}[The Generalist's lemma]
  \label{lem:generalist}
  This rule is admissible:
  $$
  \Rule{\LEIRInfer{(\Gamma \fatsemi)}{t}{\tau}{(\Delta \fatsemi \Xi)}}
       {\LEIRInferScheme{\Gamma}{t}{\gen{\Xi}{\tau}}{\Delta}}.
  $$
  \end{lemma}
  \proofsux\begin{proof}
  If $\Gamma \fatsemi \leiR \Delta \!\fatsemi\! \Xi$ then $\Gamma \leiR \Delta$ by
  definition. Furthermore,
  $\Delta \entails t \hasscheme \gen{\Xi}{\tau}$ is defined to be
  $\Delta \entails \Sbind{\Xi}{t : \tau}$, which holds iff
  $\Delta \fatsemi \Xi \entails t : \tau$.
  
  For minimality, suppose $\theta : \Gamma \leiR \Theta$ is an information
  increase and $\gen{\Psi}{\upsilon}$ is a scheme such that
  $\Theta \entails t \hasscheme \gen{\Psi}{\upsilon}$.
  Then $\Theta, \Psi \entails t~:~\upsilon$. Now
  $\theta : \Gamma \fatsemi \leiR \Theta \fatsemi \Psi$
  and $\Theta \fatsemi \Psi \entails t : \upsilon$,
  so by minimality of the hypothesis there is a substitution
  $\zeta : \Delta \fatsemi \Xi \leiR \Theta \fatsemi \Psi$ such that
  $\theta \equiv \zeta \compose \iota$ and
  $\Theta \fatsemi \Psi \entails \zeta\tau \equiv \upsilon$.
  Then by definition
  $\restrict{\zeta}{\Delta} : \leiRParam{\Delta}{\gen{\Xi}{\tau}}{\Theta}{\gen{\Psi}{\upsilon}}$
  and
  $\theta \eqsubst \restrict{\zeta}{\Delta} \compose \iota : \Gamma \leiR \Theta$.
  \end{proof}
  
  
  \subsection{The binding lemmas}
  
  Just as we have a general notion of conjunction problems, so we can regard
  binding statements as problems. There are two ways to do so, depending on the
  mode of the bound property. Each has a corresponding minimality result.
  % corresponding to the Optimist's lemma and Generalist's lemma.
  
  First, if $Q$ is a problem for $A$, then $\Sbind{x \asc \sigma}{Q}$
  is also a problem for $A$ where we regard $\sigma$ as an input. It has statement
  $$(\Sbind{x \asc \sigma}{Q}) a \defmap \Sbind{x \asc \sigma}{Q a}$$
  and preorder given by $\leParam{(\Sbind{x \asc \sigma}{Q})}{\Gamma}{a}{b}$ if
  $\leParam{Q}{\Gamma, x \asc \sigma}{a}{b}$.
  Minimal solutions are found by bringing $x$ into scope temporarily.
  
  \begin{lemma}
  \label{lem:bindVariableProblem}
  If $\Xi$ does not contain any $\fatsemi$ separators, then we have:
  $$\Rule{\LEIRProb{(\Gamma, x \asc \sigma)}{Q}{(\Delta, x \asc \sigma, \Xi)}{a}}
         {\LEIRProb{\Gamma}{(\Sbind{x \asc \sigma}{Q})}{(\Delta, \Xi)}{a}}.$$
  \end{lemma}
  \proofsux\begin{proof}
  If $\Gamma, x \asc \sigma \leiR \Delta, x \asc \sigma, \Xi$ then
  $\Gamma \leiR \Delta, \Xi$ since nothing in $\Xi$ can depend on $x$.
  If $\Delta, x \asc \sigma, \Xi \entails Q a$ then
  $\Delta, \Xi, x \asc \sigma \entails Q a$ (permuting the context) and hence
  $\Delta, \Xi \entails \Sbind{x \asc \sigma}{Q a}$.
  
  If $\theta : \Gamma \leiR \Theta$ is such that
  $\Theta \entails \Sbind{x \asc \theta\sigma}{(\theta Q) a'}$, then by inversion,
  $\Theta, x \asc \theta\sigma \entails (\theta Q) a'$.
  By minimality of the hypothesis, there is
  $\zeta : \Delta, x \asc \sigma, \Xi \leiR \Theta, x \asc \theta\sigma$ such that
  $\leParam{Q}{\Theta, x \asc \theta\sigma}{\theta a}{a'}$ and
  $\theta \eqsubst \zeta \compose \iota$.
  Hence $\zeta : \Delta, \Xi \leiR \Theta$ and
  $\leParam{(\Sbind{x \asc \sigma}{Q})}{\Theta}{\theta a}{a'}$.
  \end{proof}
  
  
  Alternatively, we can regard a type variable binding as being
  initially unknown, and obtain the problem $\Qbind{\alpha}{Q}$ whose output is
  a pair of a type and a value in $A$. The corresponding statement is
  $$(\Qbind{\alpha}{Q}) (\tau, b) \defmap \subst{\tau}{\alpha}(\probstmt{Q}{b})$$
  and the output preorder is given by
  $\leParam{(\Qbind{\alpha}{Q})}{\Gamma}{(\tau, a)}{(\upsilon, b)}$ if
  $\Gamma \entails \tau \equiv \upsilon$ and
  $\leParam{Q}{\Gamma}{\subst{\tau}{\alpha} a}{\subst{\upsilon}{\alpha} b}$.
  Minimal solutions arise by adding an unknown to the context and returning it
  as the output:
  
  \begin{lemma}
  \label{lem:inventVariableProblem}
  \raisebox{-0.1in}{\qquad\qquad\(
  \Rule{\LEIRProb{(\Gamma, \hole{\alpha})}{Q}{\Delta}{b}}
         {\LEIRProb{\Gamma}{(\Qbind{\alpha}{Q})}{\Delta}{(\alpha, b)}}
  \)}
  \end{lemma}
  \proofsux\begin{proof}
  By hypothesis, $\Delta \entails \probstmt{Q}{b}$ so clearly
  $\Delta \entails \subst{\alpha}{\alpha}(\probstmt{Q}{b})$.
  Moreover, $\Gamma, \hole{\alpha} \leiR \Delta$ so $\Gamma \leiR \Delta$.
  If $\theta : \Gamma \leiR \Theta$ is such that
  $\Theta \entails \subst{\upsilon}{\alpha}(\probsubst{\theta}{Q}{c})$, then
  $\Theta \entails \probstmt{(\subst{\upsilon}{\alpha} \theta Q)}{(\subst{\upsilon}{\alpha} c)}$.
  By minimality of the hypothesis
  with the substitution
  $\subst{\upsilon}{\alpha} \compose \theta : \Gamma, \hole{\alpha} \leiR \Theta$,
  there is some $\zeta : \Delta \leiR \Theta$ such that
  $\leParam{Q}{\Theta}{\zeta b}{(\subst{\upsilon}{\alpha} c)}$ and
  $\subst{\upsilon}{\alpha} \compose \theta \eqsubst \zeta \compose \iota$.
  Hence
  $\zeta : \leiRParam{\Delta}{(\alpha, b)}{\Theta}{(\upsilon, c)}$.
  \end{proof}
  
  
  
  \subsection{Transforming type assignment into type inference}
  
  To transform a rule into an algorithmic form, we proceed clockwise starting from
  the conclusion. For each hypothesis, we must ensure that the problem is fully
  specified, inserting variables to stand for unknown problem inputs. Moreover, we
  cannot pattern match on problem outputs, so we ensure there are schematic
  variables in output positions, fixing things up with appeals to unification. 
  
  Figure~\ref{fig:transformedRules} shows the transformed version of the
  declarative rule system. The 
  %%%rule for $\lambda$-abstractions 
     $\lambda$-rule 
  now binds a fresh name for the argument type, which 
  %%%we will replace 
     gets replaced 
  with an unknown in the algorithm. The rule for application assigns
  types to the function and argument separately, then inserts an
  equation with a fresh name for the codomain type.
  
  \begin{figure}[ht]
  \[\begin{array}{c}
  \mathframe{t : \tau}
  \smallskip\\
  \Rule{\Sbind{\beta \defn \upsilon, x \asc \gendot{\beta}}{\Pinf{t}{\tau}}}
         {\Pinf{\lambda x . t}{\upsilon \arrow \tau}}
  \qquad
  \Rule{\Pinf{f}{\chi}
          \quad
          \Pinf{a}{\upsilon}
          \quad
          \Sbind{\beta \defn \tau}{\Puni{\chi}{\upsilon \arrow \beta}}
         }
         {\Pinf{f a}{\tau}}
  
  \smallskip\\
  
  \Rule{
        s \hasscheme \sigma
        \quad
        \Sbind{x \asc \sigma}{\Pinf{w}{\tau}}
       }
       {\Pinf{\letIn{x}{s}{w}}{\tau}}
  \qquad
  \Rule{t : \tau
        \quad
        \tau \equiv \upsilon}
       {t : \upsilon}
  
  \end{array}\]
  \caption{Transformed rules for type assignment}
  \label{fig:transformedRules}
  \end{figure}
  
  We must verify that the rule systems in Figures~\ref{fig:typeAssignmentRules}
  and \ref{fig:transformedRules} are equivalent. This is mostly straightforward,
  as 
  %%%the fresh variable bindings 
     fresh name bindings 
  can be substituted out.
  The only difficulty is in the application rule, where an equation 
  %%%has been
     is 
  introduced. If an application has a type in the old system, it can be assigned
  the same type in the new system with 
  %%%the equation being reflexive. 
     using a reflexive equation. 
  Conversely,
  if an application has a type in the new system, then using the conversion
  with the equation allows the same type to be assigned in the old system.
  
  
  Given the transformed rules, we construct the algorithm to match.
  We establish the type inference assertion $\algInfer{\Gamma}{t}{\tau}{\Delta}$ 
  and the scheme inference assertion $\algInferScheme{\Gamma}{s}{\sigma}{\Delta}$ 
  by the rules in Figure~\ref{fig:inferRules}.
  As they are structural on terms, they 
  yield a terminating algorithm, 
  and hence the implementation in 
  Subsection~\ref{sec:inferImplementation}.
  The Optimist's lemma
  permits sequential solution of problems and the binding lemmas
  let us interpret binding statements as problems.
  
  \begin{figure}[ht]
  \[\begin{array}{c}
  \mathframe{\algInferScheme{\Gamma}{s}{\sigma}{\Delta}}
  
  \smallskip\\
  \namer{Gen}
  \Rule{\algInfer{(\Gamma \fatsemi)}{s}{\upsilon}{(\Delta \fatsemi \Xi)}}
       {\algInferScheme{\Gamma}{s}{\gen{\Xi}{\upsilon}}{\Delta}}
  \bigskip\\ 
  
  \mathframe{\algInfer{\Gamma}{t}{\tau}{\Delta}}
  
  \smallskip\\
  \namer{Var}
  \Rule{x \asc \gen{\Xi}{\upsilon} \in \Gamma}
       {\algInfer{\Gamma}{x}{\upsilon}{(\Gamma, \Xi)}}
  
  \smallskip\\
  
  \namer{Abs}
  \Rule{\algInfer{(\Gamma, \hole{\alpha}, x \asc \gendot{\alpha})}{w}{\upsilon}
            {(\Delta, x \asc \gendot{\alpha}, \Xi)}}
       {\algInfer{\Gamma}{\lambda x.w}{(\alpha \arrow \upsilon)}{(\Delta, \Xi)}}
  \side{\alpha \notin \tyvars{\Gamma}}
  
  \smallskip\\
  
  \namer{App}
  \BigRule{\algInfer{\Gamma}{f}{\chi}{\Delta_0}
           \quad
           \algInfer{\Delta_0}{a}{\upsilon}{\Delta_1}}
          {\algUnify{\Delta_1, \hole{\beta}}{\chi}{\upsilon \arrow \beta}{\Delta}}
          {\algInfer{\Gamma}{f a}{\beta}{\Delta}}
  \side{\beta \notin \tyvars{\Delta_1}}
  
  \smallskip\\ 
  
  \namer{Let}
  \BigRule%%%{\algInfer{\Gamma \fatsemi}{s}{\upsilon}{\Delta_0 \fatsemi \Xi_0}}
          %%%{\algInfer{\Delta_0, x \asc \gen{\Xi_0}{\upsilon}}{w}{\chi}
          %%%       {\Delta_1, x \asc \gen{\Xi_0}{\upsilon}, \Xi_1}}
          %%%{\algInfer{\Gamma}{\letIn{x}{s}{w}}{\chi}{\Delta_1, \Xi_1}}
          {\algInferScheme{\Gamma}{s}{\sigma}{\Delta_0}}
          {\algInfer{(\Delta_0, x \asc \sigma)}{w}{\chi}
                 {(\Delta, x \asc \sigma, \Xi)}}
          {\algInfer{\Gamma}{\letIn{x}{s}{w}}{\chi}{(\Delta, \Xi)}}
  
  \end{array}\]
  \caption{Algorithmic rules for type inference}
  \label{fig:inferRules}
  \end{figure}
  
  
  \subsection{Soundness and completeness}
  
  %% Corresponding to $\leiParam{\Gamma}{a}{\Delta}{b}$, we write
  %% $\delta : \leiRParam{\Gamma}{a}{\Delta}{b}$
  %% if $\delta : \Gamma \leiR \Delta$ and $\leParam{\Delta}{\delta a}{b}$.
  %% 
  %% Corresponding to $\LEIProb{\Gamma}{P}{\Delta}{a}$, we write
  %% $\LEIRProb{\Gamma}{P}{\Delta}{a}$ if $\Gamma \leiR \Delta \entails P a$, and for any
  %% $\theta : \Gamma \leiR \Theta$ such that $\Theta \entails (\theta P) b$ we have
  %% $\zeta : \leiRParam{\Delta}{a}{\Theta}{b}$ for some $\zeta$ such that
  %% $\theta \eqsubst \zeta \compose \iota$.
  
  Since the algorithmic rules correspond directly to the transformed declarative
  system in Figure~\ref{fig:transformedRules}, we can easily prove soundness,
  completeness and generality of type inference with respect to this system.
  Each proof is by induction on 
  derivations, observing that each
  algorithmic rule maintains the appropriate properties.
  
  Recall that a type inference problem $(\Gamma, P)$ has statement
  $t : \tau$ where $t$ is a term and $\tau$ is the output type.
  A scheme inference problem has statement $t \hasscheme \sigma$
  where $\sigma$ is the output scheme.
  
  \begin{lemma}[Soundness of type inference]
  \label{lem:inferSound}
  If $(\Gamma, P)$ is a type or scheme inference problem, and $\alg{\Gamma}{P}{\Delta}{a}$,
  then $\Gamma \leiR\Delta$ and $\Delta \entails P a$.
  \end{lemma}
  \proofsux\begin{proof}
  We maintain this property as an invariant in all the rules.
  \end{proof}
  
  To prove generality, we use the admissible rules in the Optimist's, Generalist's
  and binding lemmas. The algorithmic rules map to compositions of these,
  with multiple hypotheses corresponding to conjunctions of problems.
  To apply the Optimist's lemma, we must check that the problem on the right
  satisfies the \scare{simplicity condition}. For \name{Let}, this means we need
  $$\leParam{\hasscheme}{\Gamma}{\sigma}{\sigma'}
       ~\wedge~ \Gamma, x \asc \sigma' \entails w : \chi
       \quad\Rightarrow\quad \Gamma, x \asc \sigma \entails w : \chi,$$
  which says that if a solution can be found with $x$ having a given type scheme
  then one can be found with it having a more general scheme.
  The \name{App} case is even more straightforward.
  
  \begin{lemma}[Generality of type inference]
  \label{lem:inferGeneral}
  If $(\Gamma, P)$ is a type or scheme inference problem, and $\alg{\Gamma}{P}{\Delta}{a}$,
  then $\LEIRProb{\Gamma}{P}{\Delta}{a}$.
  \end{lemma}
  \proofsux\begin{proof}
  Given soundness (Lemma~\ref{lem:inferSound}), it remains to show 
  generality, i.e.\ that each algorithmic rule becomes
  admissible in the transformed declarative system if we replace
  $\transto$ with $\LEIR$.
  
  For the \name{Var} rule, suppose $\theta : \Gamma \leiR \Theta$ and
  $\Theta \entails x : \tau$. By inversion, the proof must consist of
  the \name{Lookup} rule followed by eliminating 
  $\Theta \entailsN x \hasscheme \gen{\theta\,\Xi}{\theta\upsilon}$
  with some $\Theta$-types. Hence it determines a map from the unbound type variables
  of $\Xi$ to types over $\Theta$, i.e.\ a substitution
  $\zeta : \Gamma, \Xi \leiR \Theta$ that agrees with $\theta$ on $\Gamma$ and
  maps type variables in $\Xi$ to their definitions in $\Theta$.
  
  All the remaining cases are covered by the previous lemmas.
  The Generalist's lemma proves exactly the property required for the \name{Gen}
  rule. 
  The \name{Abs} rule is minimal by Lemmas~\ref{lem:bindVariableProblem} and
  \ref{lem:inventVariableProblem}.
  The \name{App} rule is minimal by two uses of the Optimist's lemma,
  Lemma~\ref{lem:inventVariableProblem} and minimality of unification.
  The \name{Let} rule is minimal by the Optimist's lemma and
  Lemma~\ref{lem:bindVariableProblem}.
  \end{proof}
  
  \begin{lemma}[Completeness of type inference]
  \label{lem:inferComplete}
  If $(\Gamma, P)$ is a type or scheme inference problem, and
  there exist $\theta : \Gamma \leiR \Theta$ and $a'$ such that
  $\Theta \entails (\theta P) a'$, then $\alg{\Gamma}{P}{\Delta}{a}$
  for some context $\Delta$ and output $a$.
  \end{lemma}
  \proofsux\begin{proof}
  We proceed by induction on the derivation of $\Theta \entails (\theta P) a'$.
  Every case in the transformed declarative system (excluding the conversion rule)
  is covered by the algorithm, and it reduces the problem to an equivalent form,
  thereby preserving solutions. Thus if a solution exists, then the algorithm
  will succeed.
  \end{proof}
  
  
  \subsection{Implementation of type inference}
  \label{sec:inferImplementation}
  
  \begin{figure*}[p]
  
  \begin{minipage}[b]{0.5\linewidth}
  
  \subfigure[][Type schemes]{\frame{\parbox{\textwidth}{\fixpars\medskip
  
  > data Index a = Z | S a deriving (Functor, Foldable)
  >
  > data Schm a  =  Type (Ty a) 
  >              |  All (Schm (Index a))
  >              |  LetS (Ty a) (Schm (Index a))
  >     deriving (Functor, Foldable)
  >
  > type Scheme  = Schm TyName
  
  \label{subfig:schemeCode}
  }}}
  
  \subfigure[][Specialisation]{\frame{\parbox{\textwidth}{\fixpars\medskip
  
  > specialise :: Scheme -> Contextual Type
  > specialise (Type tau) = return tau
  > specialise sigma = do
  >     let (d, sigma') = unpack sigma
  >     beta <- fresh d
  >     specialise (fmap (fromS beta) sigma')
  >   where
  >     unpack :: Scheme -> (TyDecl, Schm (Index TyName))
  >     unpack (All sigma')       = (Hole      , sigma')
  >     unpack (LetS tau sigma')  = (Some tau  , sigma')
  >
  >     fromS :: TyName -> Index TyName -> TyName
  >     fromS beta  Z          = beta
  >     fromS beta  (S alpha)  = alpha
  
  \label{subfig:specialiseCode}
  }}}
  
  \subfigure[][Generalisation]{\frame{\parbox{\textwidth}{\fixpars\medskip
  
  > bind :: TyName -> Scheme -> Schm (Index TyName)
  > bind alpha = fmap help
  >   where
  >     help :: TyName -> Index TyName
  >     help beta  | alpha == beta  = Z
  >                | otherwise      = S beta
  
  > (>=>) :: Suffix -> Type -> Scheme
  > F0                               >=> tau = Type tau
  > (alpha := Hole          :> _Xi)  >=> tau = All (bind alpha (_Xi >=> tau))
  > (alpha := Some upsilon  :> _Xi)  >=> tau = LetS upsilon (bind alpha (_Xi >=> tau))
  
  > generaliseOver ::  Contextual Type -> Contextual Scheme
  > generaliseOver mt = do
  >     modifyContext (:< LetGoal)
  >     tau <- mt
  >     _Xi <- skimContext F0
  >     return (_Xi >=> tau)
  >   where
  >     skimContext :: Suffix -> Contextual Suffix
  >     skimContext _Xi = do
  >         _Gamma :< vD <- getContext
  >         putContext _Gamma
  >         case vD of
  >             LetGoal    -> return _Xi
  >             TY alphaD  -> skimContext (alphaD :> _Xi)
  >             TM _       -> error "Unexpected TM variable!"
  
  \vspace{1pt}
  
  \label{subfig:generaliseCode}
  }}}
  
  \end{minipage}
  \hspace{\medskipamount}
  \begin{minipage}[b]{0.5\linewidth}
  
  
  \subfigure[][Terms and context entries]{\frame{\parbox{\textwidth}{\fixpars\medskip
  
  > data Tm a  =  X a
  >            |  Tm a :$ Tm a 
  >            |  Lam a (Tm a)
  >            |  Let a (Tm a) (Tm a)
  >     deriving (Functor, Foldable)
  
  > type TmName   = String
  > type Term     = Tm TmName
  
  > data TmEntry  = TmName ::: Scheme
  > data Entry    = TY TyEntry | TM TmEntry | LetGoal
  
  > find :: TmName -> Contextual Scheme
  > find x = getContext >>= help
  >   where
  >     help :: Context -> Contextual Scheme
  >     help (_Gamma :< TM (y ::: sigma)) | x == y  = return sigma
  >     help (_Gamma :< _)                          = help _Gamma
  >     help B0                                     = fail "Missing var!"
  
  \label{subfig:termCode}
  }}}
  
  \subfigure[][Bringing term variables into scope]{\frame{\parbox{\textwidth}{\fixpars\medskip
  
  > (>-) :: TmEntry -> Contextual a -> Contextual a
  > x ::: sigma >- ma = do
  >     modifyContext (:< TM (x ::: sigma))
  >     a <- ma
  >     modifyContext extract
  >     return a 
  >   where          
  >     extract ::  Context -> Context
  >     extract (_Gamma :< TM (y ::: _)) | x == y = _Gamma
  >     extract (_Gamma :< TY xD) = (extract _Gamma) :< TY xD
  >     extract (_Gamma :< _)  = error "Bad context entry!"
  >     extract B0             = error "Missing TM variable!"
  
  \label{subfig:termScopeCode}
  }}}
  
  \subfigure[][Type inference]{\frame{\parbox{\textwidth}{\fixpars\medskip
  
  > infer :: Term -> Contextual Type
  >
  > infer (X x) = find x >>= specialise
  >
  > infer (Lam x w) = do
  >     alpha    <- fresh Hole
  >     upsilon  <- x ::: Type (V alpha) >- infer w
  >     return (V alpha :-> upsilon)
  >
  > infer (f :$ a) = do
  >     chi      <- infer f
  >     upsilon  <- infer a
  >     beta     <- fresh Hole
  >     unify chi (upsilon :-> V beta)
  >     return (V beta)
  >
  > infer (Let x s w) = do
  >     sigma <- generaliseOver (infer s)
  >     x ::: sigma >- infer w
  
  \label{subfig:inferCode}
  }}}
  
  \end{minipage}
  
  \caption{Haskell implementation of type inference}
  \label{fig:inferCode}
  \end{figure*}
  
  Figure~\ref{fig:inferCode} shows the Haskell implementation of our
  type inference algorithm. Note that the monadic |fail| is called if 
  scope checking fails, whereas |error| signals violation of an
  algorithmic invariant.
  
  Figure~\ref{subfig:schemeCode} implements type schemes.
  It is convenient to represent bound variables by de Bruijn indices and free
  variables (in the context) by names
  \citep{mcbride_mckinna_not_number_2004}.
  We use
  Haskell's type system to prevent some incorrect manipulations of indices by
  defining a \scare{successor} type |Index|,
  where the outermost bound variable is represented by |Z| and other variables
  are wrapped in the |S| constructor
  \citep{bird_paterson_nested_1999, bellegarde_hook_substitution_1994}.
  
  Figures~\ref{subfig:specialiseCode} and~\ref{subfig:generaliseCode} implement
  specialisation and generalisation of type schemes. The former unpacks a %%%type
  scheme with fresh names; the latter \scare{skims} 
  %%%type variables 
     entries 
  off the top of the context to the |LetGoal| marker.
  
  Figure~\ref{subfig:termCode} implements the data type of terms, and gives the
  final definition of |Entry| including type and term variable declarations and
  |LetGoal| markers. It implements the |find| function to look up a term variable
  in the context and return its scheme.
  
  Figure~\ref{subfig:termScopeCode} implements the |(>-)| operator to evaluate
  |Contextual| code in the scope of a term variable, then remove it afterwards.
  This is necessary for dealing with $\lambda$-abstractions and let-bindings.
  
  Finally, Figure~\ref{subfig:inferCode} implements the type inference algorithm
  itself. It proceeds structurally over the term,
  % adding term variables to the
  % context and looking them up later, calling |unify|
  %to check applications.
  following the rules in Figure~\ref{fig:inferRules}
  and using the monadic operations.
  
  
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{Discussion\label{sec:conc}}  %%% Concussion?
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  We have arrived at an implementation of \hindleymilner\ type inference
  which involves all the same steps as \AlgorithmW, but not
  necessarily in the same order. In particular, the dependency panic
  which seizes \W\ in the let-rule here becomes
  an invariant that the underlying unification algorithm
  maintain a well-founded context.
  
  Our algorithm is presented as a problem transformation system locally
  preserving all possible solutions, hence finding a most general
  global solution if any at all. Accumulating solutions to decomposed
  problems is justified simply by stability of solutions on information
  increase. We have established a discipline of problem solving, happily
  complete for Hindley-Milner type inference, but in any case coupling
  soundness with generality.
  
  Maintain context validity, make definitions anywhere and only where
  there is no choice, so the solutions you find will be general and
  generalisable locally: this is a key design principle for
  elaboration of high-level code in systems like Epigram and Agda; bugs
  arise from its transgression. Our disciplined account of
  \scare{current information} in terms of contexts and their information
  ordering provides a principled means to investigate and repair
  these troubles.
  
  We are, however, missing yet more context. Our task was greatly
  simplified by studying a structural type inference process for
  \scare{finished} expressions in a setting where unification is
  complete. Each subproblem is either solved or rejected on first
  inspection---there is never a need for a \scare{later, perhaps} outcome. As
  a result, \scare{direct style} 
  recursive programming is adequate to the task. If problems could get
  stuck, how might we abandon them and return to them later? By storing
  their \emph{context}, of course!
  
  Here, we have combined the \emph{linguistic} contexts for various sorts
  of variable; our next acquisition is the
  \emph{syntactic} context of the target term, interspersing variable
  declarations with pieces of its
  \emph{zipper}~\citep{huet:zipper}. We thus enable a flexible traversal
  strategy, refocusing wherever progress can be
  made. The tree-like proof states of McBride's thesis evolved into
  exactly such \scare{zippers with binding} in the implementation of Epigram.
  
  As we have seen, `information increase' is really the
  elaboration of simultaneous substitution from variables-and-terms to
  declarations-and-derivations. Our analysis of role
  declaration plays in derivation shows that stability is endemic---an
  action of hereditary substitution on \scare{cut-free} derivations.
  And that is just what it should be. We have rationalised
  Hindley-Milner type inference, adapting a discipline for
  incremental term construction in dependent types
  to manage unknowns for incremental problem solving.
  The analysis can only become clearer, the technology
  simpler, as we identify these two kinds of construction,
  mediating \emph{problems as types}.
  
  %As we have seen, an information increase is nothing other than the
  %extension of a simultaneous substitution from variables and terms to
  %declarations and derivations. Our generic analysis of the role of
  %declarations in derivations shows that stability is endemic, amounting
  %to the action of hereditary substitution on \scare{cut-free} derivations.
  %And that is exactly what it should be. We have rationalised
  %Hindley-Milner type inference by adapting a discipline for
  %interactively constructing inhabitants of dependent types as the means
  %to manage unknowns when incrementally constructing solutions to
  %problems. The analysis can only become clearer, the technology
  %simpler, as we bring these two kinds of construction together,
  %mediating \emph{problems as types}.
  
  
  \phantomsection
  \addcontentsline{toc}{section}{References}
  \bibliographystyle{plainnat}
  \bibliography{lib-short}
  
  
  
  %if showCode
  
  \appendix
  
  \subsection{Lists}
  
  We define our own types of forward (|Fwd|) and backward (|Bwd|) lists,
  which are foldable functors and monoids.
  
  > data Fwd a = F0 | a :> Fwd a
  >     deriving (Eq, Functor, Foldable, Show)
  
  > data Bwd a = B0 | Bwd a :< a
  >     deriving (Eq, Functor, Foldable, Show)
  
  > infixr 8 :>
  > infixl 8 :<
  
  > instance Monoid (Fwd a) where
  >     mempty = F0
  >     F0         `mappend` ys = ys
  >     (x :> xs)  `mappend` ys = x :> (xs `mappend` ys)
  
  > (<+>) :: Monoid a => a -> a -> a
  > (<+>) = mappend
  
  The fish operator |(<><)| combines a backward and a forward list to
  produce a backward list. Similarly, the |(<>>)| operator (chips?)
  produces a forward list.
  
  % > (<><) :: Context -> Suffix -> Context
  % > infixl 8 <><
  % > xs <>< F0 = xs
  % > xs <>< (alpha := d :> ys) = (xs :< TY (alpha := d) ) <>< ys
  
  > (<>>) :: Bwd a -> Fwd a -> Fwd a
  > infixl 8 <>>
  > B0 <>> ys         = ys
  > (xs :< x) <>> ys  = xs <>> (x :> ys)
  
  
  \section{Tests}
  
  The |findType| function looks up a type variable in the context and returns its binding,
  or |Nothing| if it is unbound or missing from the context.
  
  > findType :: Context -> TyName -> Maybe Type
  > findType B0              _                      = Nothing
  > findType (_ :< TY (y := Some tau))  x | x == y  = Just tau
  > findType (_ :< TY (y := Hole))      x | x == y  = Nothing
  > findType (c :< _)        x                      = findType c x
  
  
  The |normalise| function returns the normal form (i.e.\ with all type variables expanded as far
  as possible) of the given type within the given context. Laziness means that every
  variable in the context is normalised at most once and only if necessary.
  
  > normalise :: Context -> Type -> Type
  > normalise _Gamma tau = normalStep (normaliseContext B0 (_Gamma <>> F0)) tau
  >     where
  >         normalStep :: Context -> Type -> Type
  >         normalStep c (s :-> t) = (normalStep c s) :-> (normalStep c t)
  >         normalStep c (V x) = case findType c x of
  >             Just t   -> t
  >             Nothing  -> (V x)
  >
  >         normaliseContext :: Context -> Fwd Entry -> Context
  >         normaliseContext c F0 = c
  >         normaliseContext c (TY (x := Some t) :> es) = 
  >             normaliseContext (c :< TY (x := Some (normalStep c t))) es
  >         normaliseContext c (e :> es) = normaliseContext (c :< e) es
  
  
  |inferType| is a convenience method for inferring the type of a term in the empty context.
  
  > inferType :: Term -> Maybe (Type, (TyName, Context))
  > inferType t = runStateT (infer t) (0, B0)
  
  
  A collection of very simple unit tests follows. These allow the unifier and
  type inference algorithm to be tested with
  
  < main
  
  Note that equality of types is syntactic (it does not perform renaming) so
  changing the algorithm may sometimes cause spurious failures as the fresh
  variable numbers may be different.
  
  > main :: IO ()
  > main = unifyTest unifyTests >> inferTest inferTests
  
  > alpha *= d = TY (alpha := d)
  
  > unifyTests :: [(Type, Type, Context, Maybe Context)]
  > unifyTests = [
  >     (V 0, V 1,
  >         B0 :< 0 *= Hole :< 1 *= Hole,
  >         Just (B0 :< 0 *= Hole :< 1 *= Some (V 0))),
  >     (V 0, V 1 :-> V 2, 
  >         B0 :< 0 *= Hole :< 1 *= Hole :< 2 *= Hole,
  >         Just (B0 :< 1 *= Hole :< 2 *= Hole :< 0 *= Some (V 1 :-> V 2))),
  >     (V 0, V 1 :-> V 2,
  >         B0 :< 0 *= Hole :< 2 *= Some (V 0) :< 1 *= Some (V 0),
  >         Nothing),
  >     (V 0 :-> V 0, V 1 :-> V 1,
  >         B0 :< 1 *= Hole :< 0 *= Hole,
  >         Just (B0 :< 1 *= Hole :< 0 *= Some (V 1))),
  >     (V 0, V 1 :-> V 2,
  >        B0 :< 1 *= Hole :< 0 *= Some (V 1 :-> V 1) :< 2 *= Hole,
  >        Just (B0 :< 1 *= Hole :< 2 *= Some (V 1) :< 0 *= Some (V 1 :-> V 1))),
  >     (V 0 :-> V 1, V 1 :-> V 0,
  >        B0 :< 0 *= Hole :< 1 *= Hole,
  >        Just (B0 :< 0 *= Hole :< 1 *= Some (V 0))),
  >     (V 0 :-> V 1 :-> V 2, V 1 :-> V 0 :-> V 0,
  >        B0 :< 2 *= Hole :< 0 *= Hole :< 1 *= Hole,
  >        Just (B0 :< 2 *= Hole :< 0 *= Some (V 2) :< 1 *= Some (V 0)))
  >     ]
  
  > unifyTest :: [(Type, Type, Context, Maybe Context)] -> IO ()
  > unifyTest [] = return ()
  > unifyTest ((sigma, tau, c0, mc):xs) =
  >     do case runStateT (unify sigma tau) (0, c0) of
  >          Just ((), (_, c1)) ->
  >              if Just c1 == mc
  >              then putStrLn "OKAY" -- ++ (show sigma) ++ " == " ++ (show tau) ++ " in " ++ (show c1))
  >              else putStrLn ("\nFAIL: " ++ (show sigma) ++ " == " 
  >                                 ++ (show tau) ++ " in " ++ (show c1))
  >          Nothing -> 
  >              if mc == Nothing
  >              then putStrLn "OKAY" -- ++ show sigma ++ " /= " ++ show tau)
  >              else putStrLn ("\nFAIL: " ++ show sigma ++ " /= " ++ show tau)
  >        unifyTest xs
  
  
  > inferTests :: [(Term, Maybe Type)]
  > inferTests = [
  >     (X "u", 
  >          Nothing),
  >     (Lam "x" (X "x"),
  >          Just (V 0 :-> V 0)),
  >     (Lam "x" (X "x" :$ X "x"),
  >          Nothing),
  >     (Lam "x" (Lam "y" (X "y")),
  >          Just (V 0 :-> V 1 :-> V 1)),
  >     (Lam "x" (Lam "y" (X "x")),
  >          Just (V 0 :-> V 1 :-> V 0)),
  >     (Lam "x" ((Lam "y" (X "y")) :$ X "x"),
  >          Just (V 0 :-> V 0)),
  >     (Lam "x" ((Lam "y" (X "x")) :$ X "x"),
  >          Just (V 0 :-> V 0)),
  >     (Let "m" (Lam "a" (X "a")) (X "m" :$ X "m"),
  >          Just (V 2 :-> V 2)),
  >     (Let "s" (Let "m" (Lam "a" (X "a")) (X "m" :$ X "m")) (X "s"), 
  >          Just (V 4 :-> V 4)),
  >     (Lam "x" (Lam "y" (X "x")),
  >          Just (V 0 :-> (V 1 :-> V 0))),
  >     (Lam "x" (Lam "y" (X "x" :$ X "y")),
  >          Just ((V 1 :-> V 2) :-> (V 1 :-> V 2))),
  >     (Let "I" (Lam "x" (X "x")) (X "I"),
  >          Just (V 1 :-> V 1))
  >   ]
  
  > inferTest :: [(Term, Maybe Type)] -> IO ()
  > inferTest [] = return ()
  > inferTest ((t, expected):tes) =
  >     do case inferType t of
  >          Just (tau, (_, c)) ->
  >              let tau' = normalise c tau
  >              in
  >                  if Just tau' == expected
  >                  then putStrLn "OKAY" -- ++ (show t) ++ " : " ++ (show tau') ++ " in " ++ (show c))
  >                  else putStrLn ("\nFAIL: " ++ (show t) ++ " : " 
  >                                 ++ (show tau') ++ " /= " ++ (show expected)
  >                                 ++ " in " ++ (show c))
  >          Nothing -> 
  >              if expected == Nothing
  >              then putStrLn "OKAY" -- ++ (show t) ++ " does not type")
  >              else putStrLn ("\nFAIL: " ++ (show t) ++ " should type to " ++ (show expected))
  >        inferTest tes
  
  
  We need some |Eq| and |Show| instances for testing purposes:
  
  > deriving instance Eq a => Eq (Ty a)
  > deriving instance Show a => Show (Ty a)
  > deriving instance Eq Entry
  > deriving instance Show Entry
  > deriving instance Show Term
  > deriving instance Eq a => Eq (Schm a)
  > deriving instance Show a => Show (Schm a)
  > deriving instance Eq a => Eq (Index a)
  > deriving instance Show a => Show (Index a)
  
  > deriving instance Eq TyDecl
  > deriving instance Show TyDecl
  
  > deriving instance Eq TyEntry
  > deriving instance Show TyEntry
  > deriving instance Eq TmEntry
  > deriving instance Show TmEntry
  
  %endif
  
  
  
  \end{document}
  