Polymorphic Recursion / Rank-2 Confusion

[Frank Atanassow]

On maandag, sep 22, 2003, at 00:07 Europe/Amsterdam, Brandon Michael 
Moore wrote:
> Can anyone tell me what's wrong with the following derivation?

Without going through your derivation completely, the problem is almost 
certainly polymorphic recursion. Vector is a nested datatype---its 
definition calls itself with different type arguments---and so, although

   collect :: (v -> [a]) -> (w -> [a]) -> Vector v w -> [a]

the recursive call to collect in, for example, the second clause, has a 
different type, namely:

   collect :: (v -> [a]) -> ((w,w) -> [a]) -> Vector v w -> [a]

However, in the absence of an explicit type signature, Haskell will 
assume that the types of the top-level and recursive occurrences of 
collect are equal, which they are not, so you'll get a type error.

Indeed, the error messages Dominic posted:

 > ERROR "Test1.hs":23 - Type error in function binding
 > *** Term           : coal_
 > *** Type           : (a -> b) -> (c -> [d]) -> Vector_ a e -> b
 > *** Does not match : (a -> b) -> ((c,c) -> [d]) -> Vector_ a (e,e) -> 
b
 > *** Because        : unification would give infinite type
 >
 > Test1.hs:25:
 >     Occurs check: cannot construct the infinite type: t = (t, t1)
 >         Expected type: (t, t1)
 >         Inferred type: t
 >     In the first argument of `coalw', namely `w1'
 >     In the first argument of `(++)', namely `(coalw w1)'

corroborate this argument.

Or, are you asking instead why it is that type inference does not work 
for polymorphic-recursive functions?

Regards,
Frank