\section{Algorithm}
\label{sect.algorithm}

We briefly discuss an inference algorithm for \SystemFAI.

\paragraph{Scopes.}
We keep track of equality assumptions and equality obligations per scope.
If an expression |let x = e1 in e2| is in a scope |s1|, then |e1| is in
a scope |s2| (a subscope of |s1|), and |e2| is in scope |s1|.

For an implicit |v|, we emit an equality obligation, written |s : Prv (v =*= ty)|,
when we unify |v| with some type |ty| in a scope |s|.
Similarly, we emit an equality assumption, written |s : Ass(v =*= ty)|, when we
introduce these through a GADT pattern match.

\paragraph{Proof obligations.}
For a scope |s|, we try to prove the equality obligations |overline(Prv)| given the assumptions |(overline(Ass))| in |s| or the parent scopes of |s|.
We apply a certain constraint solving algorithm~\cite{geest07}. This algorithm applies the inference
rules of Figure~\ref{fig.type.equal} exhaustively. The outcome is the largest set of equality assumptions
|Overline(Ass')| that:
\begin{itemize}
\item solve the original proof obligations, i.e. |(overline(Ass)) (overline(Ass')) ::- (overline(Prv))|.
\item are not implied by the original assumptions, i.e. |(overline(Ass)) ::/- (overline(Ass'))|.
\item consist only of types that were encountered during exhaustive application of the inference rules.
\item the left-hand side of all the rules is a skolem constant.
\end{itemize}
The result set consists of two possible assumptions:
\begin{itemize}
\item |s : Ass(v =*= v')| with |v'| an implicit. We emit a proof obligation |s : Prv(v =*= v')|.
\item |s : Ass(v =*= rho)|, and |rho| not an implicit. We substitute |v| with |rho|, if
      |rho| does not conflict with assumptions and prove obligations on |v|. Otherwise,
      the result is a type error. Effectively, this means that |v| was introduced through the
      use of the \TirName{impl.expo} rule of Figure~\ref{fig.type.expr}, and we may not generalize over |v|.
\end{itemize}

\paragraph{Plausible obligation and generalization.}
We keep track of a \emph{plausible obligation} for |v|.
For all assumptions |s : Ass(v =*= rho)| in a scope |s| with |rho = D (overline ty)|, and the plausible obligations of
the subscopes of |s|, we compute the most general unifier |substi = mgu (overline rho)|.
If this unifier exists, we use this unifier applied to one of the assumptions as plausible obligation
for |v| in scope |s|.
Such a plausible obligation becomes the qualifier for |v| when generalizing a let-binding, if it exists. For example,
in the expression:
\begin{code}
eval = \(e :: Expr v) ->  case e of
                            Num i            -> i       :: v
                            (Tuple p q) a b  -> (p, q)  :: v
\end{code}
If the second case alternative was not written, we obtain the assumption |v ~ Int| as plausible obligation
for |v|. Otherwise, there is no plausible obligation for |v|.

Finally, we determine which occurrences of |v| in types are in the context of the plausible obligation.
For all occurrences |v1 ... (sub' v n)|, we temporarily substitute |v'| for |v| and check that all
occurrences of |v'| in the types mentioned by rule \TirName{valid} are in a context where the plausible
obligation hold. If not, we revert the substitution, otherwise we keep it.
For example, in:
\begin{code}
eval = \(e :: Expr v) ->  case e of
                            Num i -> i :: v 
\end{code}
We cannot proof |v =*= Int| for the scope that |e :: Expr v| is in. We can prove this for |i :: v|.
Thus, we end up with the type |Expr v -> v'|, and quantify it to |impl (v : v' =*= Int) dot Expr v -> v'|.

\paragraph{Discussion.}
We implemented an earlier version of the algorithm in UHC~\cite{uhc},
and evaluated the performance on a complex GADT example~\cite{DBLP:conf/tldi/BaarsSV09}.
Roughly all time was spent in exhaustively applying the equality rules on large types.
We expect that part of the algorithm can be optimized severely by using the solving algorithms
for implication constraints~\cite{gadt-short,DBLP:conf/icfp/SchrijversJSV09}.