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

We described a translation of \GADTs to an explicitly typed system with qualified types (\Sect{sect.translation}) with equality constraints as qualifiers. The type system comes basically for free, since dealing with assumptions and insertion of evidence is already done by the system for qualified types. Adding \GADTs to such a language boils down to implementing an entailment relation on equality constraints. To prevent having entailment rules for each construct in the type language, we used an auxiliary relation to construct coercions based on the structure of types.

To validate our work, we added support for \GADTs to the Essential Haskell compiler~\cite{dijkstra04}, using Constraint Handling Rules~\cite{chr98} to implement the entailment rules. The EH language has a rich type system (higher ranked types, impredicative types, existential types, many type class extensions, scoped instances, polymorphic kinds, extensible records). The implementation is orthogonal to all these extensions.


\subsection{Future work}

The obvious future work is to describe our implementation in terms of this specification. Second to that, we can now describe implementation issues separately, such as the propagation of type information, and the implementation of entailment. For example, the following issues can now be described without having to give an implementation for other aspects of a GADT implementation:

The construction of equality proofs can be expensive, especially when big types with many variables are involved. There are two potential directions for optimization. The solver uses a trie-structure to select candidate CHRs and is optimized to deal with a great number of very specific CHR rules. By generating many but specialized versions of the CHR rules based on the \GADT declarations, we hope to reduce the time it takes to select the next applicable rule. Furthermore, there can be several applicable rules to choose from during a solve step. At the moment, the choice is non-deterministic, but more advanced heuristics are definable in the CHR framework (for example, to make the symmetry rule the least attractive choice). These optimizations can speed up the time it takes to construct an equality proof considerably.

A succeeding pattern match witnesses that the type equalities hold. However, in the presence of irrefutable patterns, the pattern match may not have taken place. One way to deal with this is to only assume the additional type equalities when the pattern match is not inside an irrefutable pattern. This approach is taken by the Haskell compiler GHC for example. However, since we formulated \GADTs in terms of qualified types and have the facilities for evidence generation at our disposal, we can do better: generate coercion functions that force evaluation of the irrefutable pattern when a coerced value is evaluated which needed the corresponding assumption. Proper heuristics need to be defined to minimize the forcing of evaluations.

\paragraph{Acknowledgements}
We thank the anonymous referees for their comments; the student paper feedback report in particular. Special thanks to Luc\'{i}lia Camarao from Universidade Federal de Ouro Preto, Brazil, for her support just before the first submission deadline. 

This work was supported in part by Microsoft Research through its European PhD Scholarship Programme.