Hi Mark, Thanks for the references you provided! Mark P Jones wrote:
My instinct (which perhaps somebody will prove incorrect) is that this will not help. Suppose, for example, that you needed to unify ([a],[b]) with f c as part of the type inference process. How would you solve this problem? Alas, there are several different, and incompatible ways:
([a], [b]) = (/\a. ([a],[b])) a = (/\b. ([a],[b])) b = (/\c. (c, [b])) [a] = (/\d. ([a], d)) [b] = (/\e. e) ([a], [b])
Note that the /\-terms in each of these examples satisfies your restriction. So I don't think you'll be able to obtain most general unifiers or principal types with this restriction.
Let's put your example into the context of type classes: class T f c where method :: f c Now when we want to use method as a ([a],[b]), ambiguity arises, as you suggested. However, I think this just means we should allow *at most one* of the following instances to be declared: instance T (/\a. ([a],[b])) a instance T (/\b. ([a],[b])) b instance T (/\c. (c, [b])) [a] instance T (/\d. ([a], d)) [b] instance T (/\e. e) ([a], [b]) In other words, the above instances are considered overlapping. ____________________________________________________ | As long as we only have one of these instances | | in the program, there is no ambiguity. | ---------------------------------------------------- I'm sure there must be other ramifications (e.g. maybe now whether two instances are overlapping becomes undecidable -- I haven't thought over it yet), but it seems worth further investigation. -- Zhanyong