We take one of the first steps towards developing a practical, statically-typed, functional, aspect-oriented programming language by showing how to integrate polymorphism and type analysis with aspect-oriented programming features. In particular, we demonstrate how to define type-safe polymorphic advice using pointcuts that unify a collection of polymorphic join points. We also introduce a new mechanism for specifying context-sensitive advice that involves pattern matching against the current stack of activation records, and meshes well with functional programming idioms. We give our language meaning via type-directed translation into an expressive, but fairly simple, type-safe intermediate language. Many complexities of the source language are elminated in this translation, leading to a modular specification of its semantics. One of the novelties of the intermediate language is the definition of polymorphic labels for marking control-flow points. These labels are organized in a tree structure such that a parent in the tree serves as a representative for the collection of all its children. Type safety requires that the type of each child is a generic instance of the type of the polymorphic parent. Similarly, when a set of labels is assembled as a pointcut, the type of each label is an instance of the type of the pointcut.