Inferring refinement types
You've stumbled on the fact that inference of static invariants for higher-order languages is quite difficult in practice, in addition to being undecidable in theory. I'm not sure what the definitive answer to your question is, but note several things:


Polymorphism and refinement types behave poorly together, as you have noted, in particular the notion of most general type is lost. A consequence of this is that analyses based on refinement types in the presence of polymorphism may need to chose between whole-program analysis (as opposed to compositional analysis) and the use of heuristics to decide which type you want to assign to your program.
There is a strong relationship between inferring refinement types and:


Computing the abstract interpretation of your program
Computing loop invariants in an imperative language.



With this in mind, here are a few disorganized references on the inference of refinement types. Note that there are many differing flavors of refinement types: I tend to be more interested in refinements of inductive datatypes, so this list may be skewed in that direction.


Start with the classics: Relational Abstract Interpretation of Higher-Order Functional Programs by Cousot &amp; Cousot. This explains how to extend abstract interpretation to higher-order programs using relational semantics.
Liquid Types by Rhondon, Kawaguchi and Jhala. This is very evolved work, that combines HM and a type of predicate refinement to infer security annotations (array bound checks for instance) for ML style programs. The inference proceeds in 2 steps; the first is HM inference of type annotations, which guide the choice of refinements to perform.
I should probably also mention the work by Fournet, Swarmy, Chen, Strub... on $F^*$, an extension of $F^\#$ which seems similar to the liquid types approach, but with the goal of verifying cryptographic protocols and algorithms for distributed computing. I'm not sure how much published work there is on the inference of annotations in this case.
There is a nice paper by Chin and Khoo on inference of a specific kind of refinement types: types with size annotations.
The ATS programming language is a system which allows various refinements and provides facilities for writing programs with them. However the annotations may be arbitrarily complex (and thus undecidable) and therefore may require user interaction. I believe that there is a form of inference for these types, I'm not sure which article to recommend however.
Last, but not least The Cartesian Product Algorithm, by Ole Agesen. While not mentioning refinement types explicitly, this seems to be the work closest to solving the problem you seem to have. Don't be fooled by the mention of parametric polymorphism in the abstract: they look to infer concrete types, which are just tuples of possible atomic types. Emphasis is given on efficiency. I recommend reading this article first to see if it solves your problem.


Side note: type inference in the presence of intersection types can be very undecidable: in the simplest form, $\lambda$-terms with intersection type are exactly the strongly normalizing terms. Tread softly around them :)