# unify a list of constraints:
#  - input = list of constraints of the form "lhs==rhs"
#  - output = list of constraints

# a unification is an assignment of values to variable that satisfies
# the constraints in the most general way. in our case, variables
# are the PolymorphicType guys, and values are any Types

def unify( constraints ):

    return [] if constraints is an empty list;

    (lhs,rhs) = shift constraints;

    ## if they are already equal, do nothing    
    if lhs = rhs then
        return unify(constraints);

    ## orient "variables" on the lhs
    if lhs is not a PolymorphicType, but rhs is, then
        (lhs,rhs) = (rhs,lhs);
        
    if lhs = PolymorphicType(id) then
        if PolymorphicType(id) occurs anywhere within constraints, then
            croak "you're asking for a recursive type!"
    
        constraints = map { replace each PolymorphicType(id)
                                with rhs } constraints;
                             
        ## output this assignment as part of the solution!   
        return "id:rhs" + unify(constraints);
   
    ## for 2 FuncTypes to be equal, their components must be equal,
    ## so add new constraints
    if lhs = FuncType(l1,l2) and rhs = FuncType(r1,r2) then
        return unify(constraints + "l1==r1" + "l2==r2");
    
    if lhs = ListType(l1) and rhs = ListType(r1) then
        return unify(constraints + "l1==r1");

    ## we get here if you try to constrain a ListType to equal a
    ## FuncType, or other such impossible feats
    else
        croak "unification impossible!";