\section{Related Work} \label{sect.relatedwork} Several approaches propose limitations to make inference for GADTs tractable. Many specifications and algorithms for GADTs consist of two components: a type information propagation component and a type conversion component. A type information propagation strategy determines what is known type information based on user-supplied type signatures, and what is inferred type information. A type conversion strategy deals with the construction of coercion terms. \subsection{Restricting Expressiveness for Tractable Inference} \citet{gadt-short} show that inference for \GADTs{} is undecidable without a helping hand from the programmer in the form of type annotations, and show that principal typing is lost. They present an inference algorithm that generates implication constraints, and apply a technique called Herbrand abduction~\citep{1079715} to solve these constraints. A solution to these constraints is a normalized constraint that implies the generated constraints. The authors define a notion of a sensible solution; under these conditions the resulting type is principal. These conditions are specified in terms of the algorithm. We are reluctant to adopt such an approach, because it requires programmers to think in terms of an algorithm. To discover why their program is (not) accepted by the type inferencer, the steps of the algorithm have to be performed by hand. \citet{DBLP:conf/icfp/SchrijversJSV09} recently presented two type systems for \GADTs, and the inference algorithm OutsideIn. The first type system is relatively simple, but inference for it is undecidable. The latter is more restricted, but has OutsideIn as a sound and complete inference algorithm. Both specification and inference algorithm are given in terms of implication constraints. When type inference is combined with coercion inference, additionally a coercion |ty1 =*= ty2| may be constructed when |ty1| unifies with |ty2| (the result then corresponds to the \TirName{refl} rule). The main idea of OutsideIn is that binding of variables during such a unification is not allowed on variables that are free in the environment (of the enclosing let-expression or case-branch). These are called the ``untouchable'' unification variables. Type checking proceeds as normal, except that a unification of a Skolem constant or with an untouchable requires a coercion to be constructed. The actual construction of these coercions is done after type checking is complete. The approach is presented as a general solution to inference for GADTs. Although this approach is sound and complete with respect to their specification, their specification still requires type annotations for most functions with GADT patterns. For example, with OutsideIn, a type signature is needed for the following code that uses GADTs in the typical way: \begin{code} data D a where C1 :: Int -> D Int C2 :: Bool -> D Bool -- needs: |f :: D alpha -> alpha| f x = case x of C1 y -> y C2 z -> z \end{code} The reason is that |alpha| is free in the environment, and thus not unified. This approach still lacks a good specification: it introduces ``suspended judgments'' to encode a two-phase typing of an expression, which is actually harder to comprehend than the algorithm itself. A problem here is that the untouchable variables do not appear explicitly in conventional type system specifications. They might be eliminated by unification during conventional type inference, and are notationally equal to the type the variable is unified with. Thus, such a specification requires a programmer to know how the algorithm is distributing its type variables over the program. \citet{pointwise} propose the Pointwise GADT type system. The notion pointwise comes from the correspondence between the range-type of a constructor and the type of the scrutinee in a GADT case expression. During inference in case branches, type information flows from and to such types. The authors identify two typical usage-patterns for GADTs, and make a case to restrict the use of GADTs to these patterns. \emph{Parametric instantiation} entails that each case branch assumes the same specific instance of a polymorphic data type. \emph{Type indexing} entails that each case branch assumes a different instance of a polymorphic data type. The authors propose a unification technique to restrict this bidirectional information flow. From an implementation point-of-view, this approach is promising: the authors performed several case studies of typical uses of GADTs and presented a mechanism that types many typical usages of GADT programs without explicit type annotations. However, it is not clear how this approach relates to the challenges we pointed out in Section~\ref{sect.motivation.inference}. Furthermore, the approach lacks a specification to serve as an explanation to the programmer. \subsection{Type Annotation Propagation Strategies} \label{sect.relatedwork.prop} \metacomment { \item "Stratified type inference for generalized algebraic data types." (Franc¸ois Pottier and Yann R´egis-Gianas) } \citet{pottier06} use shape inference. A shape represents known type information based on user-supplied signatures. These shapes are spread throughout the syntax tree in order to locate possible coercions. Their approach uses complex algorithms to spread the shapes as far as possible, iteratively. More iterations give rise to a better spread of annotations, at a cost of performance. The essential part concerning \GADTs{} is that incompatible shapes are normalized with respect to some equation system, which is not made explicit in their work. From an implementer's point of view, this description is a concrete description of the equation system, and it requires infrastructure for spreading shapes. \metacomment { \item "Simple unification-based type inference for \GADTs" (Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn) } Similarly, \citet{jones06,jones04} define a notion of wobbly types to combine type checking and type inference, which is based on earlier work on boxy types~\citep{vytiniotis06}. A rigid type represents known type information based on user-supplied type information, whereas a wobbly type is based on inferred information. The idea is then that type conversions are only applied on rigid types, for reasons of predictability and most-general typing. Aside from wobbly types, the authors use concepts such as ``fresh most general unifiers'' and lexically scoped type variables in their presentation. It is hard to distinguish which of these concepts are really required, and which of these concepts are actually related to other language features that are covered by their approach (such as type families). We incorporated a notion of wobbly and rigid types in our specification: in an explicitly typed \SystemF-variant, the skolemnized type constants are rigid types, and we only allow type conversions on those. \metacomment { \item propagation conclusion } The exact choice of propagation strategy is an orthogonal issue. By allowing type conversions only on known type information, a better propagation strategy just means that less explicit types have to be given by the programmer. This is the reason why we have chosen an explicitly typed source language in the first place. In fact, for our own implementation of this specification, we piggybacked on the infrastructure of the implementation of a higher-ranked impredicate type system. It has two propagation strategies, of which the advanced one has a concept of hard and soft type context, which can be compared to rigid and boxy types~\citep{dijkstra05phd}. \subsection{Type Conversion Strategies} \metacomment { \item "Simple unification-based type inference for \GADTs" (Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn) } \citet{jones06,jones04} use a unification-based strategy, where type conversion is called type refinement. A fixpoint substitution is constructed that, for each type equation introduced by pattern matching, contains a mapping for each (non-wobbly) type component of the left hand side of an equation, to the corresponding type component on the right hand side of an equation. The substitution is then used to normalize the types under consideration. The presentation is intertwined with the type propagation strategy, which makes it hard to separate these concepts. %% More recent continuation of this work by Sulzmann et al.~\cite{sulzmann07} puts the \GADT aspect in relative isolation. \metacomment { \item "Type inference and type error diagnosis for Hindly/Milner with extensions" \item no specific solver for \GADTs, complicated solver } \citet{wazny06} uses a constraint-based strategy. The GADT aspect of this strategy is covered separately by \citet{sulzmann06,stuckey05}. They also formulate the typing problems in terms of solving constraints with CHRs. The difference is that we restrict ourselves to equality constraints, and do not need the machinery required to solve implication constraints. Their typing/translation rules do not mention how to deal with existential data types, which may be transparent to the given approach, but is of interest to a reader because GADT examples often use them. In contrast to \citet{jones06}, restrictions on type conversions are not mentioned.