Excerpts from André Batista Martins's message of Sat Oct 09 17:45:05 -0400 2010:
Hello, exists any algorithm to determine how terms can be changed to safisty the type of one function?
Your terminology is a little off: in particular, your example doesn't include any "terms" (which are understood to be the things to the right of the =, not the double-colon). The term you are actually looking for is "unification". One way of looking at this is that you have two types that are the same type, but due to their structure they impose various constraints on each other. Solve all of the constraints and you have a unified type (indeed, the "best" such type in many type systems--the correct term is principal type), and if you can't solve them then you have a type error. Cheers, Edward