Many synthesizers implicitly benefit from using polymorphic types, since parametric polymorphism reduces the search space. Additional synthesis constraints may interfere with \emph{parametricity}. In particular, a polymorphic type may cause otherwise feasible input-output examples to contradict each other. We present \textsc{Taxi} (\textbf{t}ype-\textbf{a}nd-e\textbf{x}ample based \textbf{i}nferencer), a tool for efficiently reasoning about the feasibility of polymorphic programs specified by input-output examples, and \textsc{Driver}, a tactic language for top-down program synthesis that uses feasibility reasoning to prune the search space. \textsc{Taxi} guarantees that every search state corresponds to a correct (albeit possibly partial) implementation. In addition, it allows for shortcutting the synthesis when a subspecification covers all cases. We show that these techniques have the potential to speed up top-down enumerative type-and-example driven synthesizers.