Ken Shan wrote:
I think the rule you're looking for is the following: Don't equate a type variable with something that contains that type variable. This is known as the "occurs check". This rule prohibits "equi-recursive" types like "b" above, but not "iso-recursive" types like
data List a = Nil | Cons a (List a)
because the type "List a" is merely isomorphic to something containing "List a", but not equal to it.
Thanks, this is great. I understand (more or less) about equi- vs. iso-recursion from Pierce. The point (I assume) is that there is a natural distinction between the two cases, so that the restriction on infinite types (but not all recursive types) falls out fairly naturally from the Hindley-Milner analysis. (Thanks to everybody who responded.) Regards, Jeff Scofield Seattle