[clean-list] a local function typing question in function composition

[Edsko de Vries]

Hi Philip,

> So, going back to the  original example
>      f :: a -> a
>      f x = y
>          where
>              y :: a
>              y = x
> 
>      Start = f 5
> 
> Here the error really is that the compiler cannot unify the type of  
> "y" in the expression "f x = y" with the type of "y" from the type  
> declaration "y :: a", because the "a"s are actually different type  
> variables. They are different type variables, but they need to be the  
> same in order to type check the function.
> 
> Am I correct?

No, not quite, but close :-) Let me illustrate with a slightly modified
example:

module t

undefined :: z
undefined = undefined

f :: a -> a
f x = y
    where
        y :: a
        y = undefined

Start = f 5

I'm declaring a term "undefined", which is simply defined to be itself. The
point is that "undefined" has every type. That's what the type annotation says
for undefined: the type of undefined is "z" *for every z*.

This definition of f (which is identical to the previous, except that I defined
y to be "undefined" rather than "x") is accepted by the compiler. Why? 

The annotation of "y" says that y has type a *for every a*. It checks
the definition of y, and finds that it is defined to be "undefined"; it
looks up the type of undefined, finds that undefined has type x *for
every x* and thus accepts the type annotation. 

Then when it checks the body of f ("y"), it must check that y has type "a",
where "a" is the type of the argument passed in (x). This is indeed a different
a, BUT "y" has type "a" *for every a*, so that doesn't matter! We could just as
well have written: 

f :: a -> a
f x = y
    where
        y :: b
        y = undefined

and nothing would change. Now when we go back to the original example,

f :: a -> a
f x = y
    where
        y :: a
        y = x

the type error is *not* in the body of, but in the body of y. The body of y
says that y must have type a *for every a*, but in fact, y only has one type,
that is, the type of the argument passed in (x). Unfortunately, since Clean
doesn't have scoped type variables, we cannot write that down, but internally
the typechecker will have assigned a type variable "T" to correspond to the
type of x. Because y is defined to be x, Y will also have type "T". The type
annotation of "y" says that y has every type you want it to have, but that's
not the case (it has type T, and only type T).

Again, this program is *exactly* the same program as

f :: a -> a
f x = y
    where
        y :: b
        y = x

which is rejected for the same reason (now y has type b *for every b*, but that
is of course the same type as type a *for every a* -- although perhaps it is
easier to see that this program is wrong).

Does that help?

Edsko