\section{Conclusion}
\label{sect.conclusion}

We presented a specification for GADT inference in terms of
the language \SystemFAI. This language deviates from System F
in three ways: it has syntax to request an equality proof,
a lambda to take an equality proof as argument and bring it
in scope, and automatic coercions based on equality proofs
in scope.
In this language, we can express GADTs using the folklore
Church encoding for data types.

Compared to other approaches, our specification is a small
extension of a bare System F, which allows us to treat
data types and case expressions as syntactic sugar.
Furthermore, our specification describes what to do with
other forms of pattern matching and binding, exploiting
encodings as conventional System F terms.

As future work, it may be worthwhile to investigate if 
algorithms such as OutsideIn~\cite{DBLP:conf/icfp/SchrijversJSV09}
can be specified in a simpler way by taking an implicitly
typed variation on \SystemFAI{}
as a basis.


%if False
\subsection{Experiences with UHC}

  Crosscutting concerns played an important role regarding our
  implementation in UHC. Surprisingly, the code related to
  GADT resolving was affected by code related to context
  reduction (resolving of overloading). The underlying problem
  was that we were constructing equality proofs too early, and
  were faced with types that were not sufficiently known yet.

  Therefore, we decided to construct equality proofs at the
  end of inference for a binding group. We then only
  coerce between types that we do know sufficiently.
  This inspired us to specify GADT inference in terms of
  System F.

  In previous versions of this paper, we experimented
  with approaches where we allow coercions on types we do not
  know yet, which allows certain type annotations to be
  omitted. In our experience, however, the burden of
  annotating GADT matches is insignificant compared to
  the implementation and specification complexity of more
  flexible inference approaches.

  Also, because the abstract syntax of UHC
  is rich, we were forced to deal with various
  forms of pattern matches, from which it is not directly
  clear how these correspond to syntax in other specifications,
  and what challenges these introduce.
%endif