Type indexed types?

[Jim Farrand <jim@farrand.net>]

Hi,

This is what I need to do:

Given a type, u, and a collection of types, ts, find a type t such that:
  * t is a member of ts
  * t can be unified with u
  * There is no type v in ts, which unifies with u and is more general
    than t.

(In other words, find the most specific type in ts that is still equal
to or a generalisation of u.)

For example:

ts = list int, int, list 'a, 'a

For u = list int, the result would be list int.  For u = list string,
the result would be list 'a, and for u = string the result would be 'a.

Note that I already have a function which can compute if type a is a
specialisation of type b.

I think that in theory, I could do a brute force approach:
  * Grab all types in ts that are generalisations of u.
  * Order the results according to how specific they are.
  * Arbitrarily choose one of the most specific.

But there must be a smarter way!  Eg, I think that I should be able to
start with the type u, and incrementally generalise it until I find a
match.  It is tricky to find a method of generalisation that will cover
the entire search space, and find the most specific type first.

I am sure there must be papers on this, but I am having trouble coming
up with the right search terms - references appreciated! :)

Thanks in advance,
Jim

-- 
Jim Farrand