...

It is quite similar in spirit to the concept of principal type in Hindley-Milner type systems. An expression can have many types but only one "best" (most general) type in that system.

Now, I'm not any kind of expert on this, but isn't the most general HM type one that encompasses the others, and *not* one out of a set of ambigous (and mutually exclusive) types?

In a sense. You define a partial order on types by a < a' (a more general than a') if there is a substitution s of type variables such that a' = sa. The interesting property of HM type systems is that for each term t and all type judgements t:a that can be derived, there is a type judgement t:a' such that a' < a. a' is called the most general type of t. What I suggested was to define a different relation between types, measuring "relative liftedness". We can call it "<<". Now, if it is the case that for all judgements t -> t':a in the type system I sketch, there is a judgement t -> t'':a' where a' << a, the we can select the transformation to be t -> t''. t'' will then have a "most general type" among the possible transformed terms, but wrt << rather than <. Ambiguity between types depends on the ordering between types that you consider! Björn Lisper