A type- and control-flow analysis is a program analysis that yields both type-flow information, approximating the types that may instantiate type variables, and control-flow information, approximating the values (especially lambda- and Lambda-expressions) that may be bound to variables. Moreover, each of the flows informs the other; control-flow establishes the types that may instantiate Lambda-bound type variables by determining the Lambda-expressions that flow to a type-application expression, while type-flow filters control-flow by rejecting the flow of values having static types that are incompatible (according to the type-flow information) with the static type of the receiving variable. In previous work [1,13,14], we introduced a (monovariant) type- and control-flow analysis for System F (with recursion). While System F has an expressive type system and has served as a useful core calculus in which to express interesting language features, it only allows abstraction over types and does not allow abstraction over type constructors. Increasingly, researchers are looking at System F-omega, with both term- and type-level abstraction over types of arbitrary kind, as a core calculus in which to explore advanced language features. Hence, we are motivated to define a type- and control-flow analysis for System F-omega that is able to analyze the rich structure of System F-omega types. In this work, we present a preliminary type- and control-flow analysis for System F-omega (with recursion). As in previous work, we give both a specification-based formulation of the analysis, used to prove soundness of the analysis, and a flow-graph-based formulation, used to guide the implementation of an algorithm. While the macro structure of the development for System F-omega follows that for System F, moving to System F-omega introduces subtle challenges that have left some unanswered questions about the meta-theory. In particular, the decidability of type compatibility defined in terms of System F-omega's definitional type equivalence remains an open question. In order to be computable, our flow-graph-based formulation uses a restricted form of definitional type equivalence and performs a 0CFA at the type-level, yielding an analysis result that is less precise than the "best" (but as of yet, uncomputable) analysis result accepted by the specification-based formulation. Our soundness results have been formalized in the Coq proof assistant. This work is based in part on the first author's MS thesis [53].
