[clean-list] Typing polymorphic CAFs

[John van Groningen]

Vag wrote:

>module c
>import StdEnv ; Start = testcafI ; testcafI :: Int ; testcafI = testcaf1
>class minValue a :: a
>instance minValue Int where minValue = 0x80000000 /* we are using
>INT32 machines for now */
>minValueOf :: a -> a | minValue a
>minValueOf _ = minValue
>minValueOf2 = minValueOf testcaf2
>minValueOf1 = minValueOf testcaf1
>// ------------------------------
>
>testcaf1 = if (minValueOf testcaf1 == zero) one (one + one)
>
>testcaf2 = if (minValueOf2 == zero) one (one + one)
>
>//testcaf3 = if (minValueOf2 == zero) one (one + one)
>
>1. testcaf1 is ok, but testcaf2 and testcaf3 contain overloading
>ambiguities. Compiler complains only about testcaf3 (testcaf2 compiled
>ok). Why?

'testcaf2' and 'minValueOf2' are mutually recursive:

>testcaf2 = if (minValueOf2 == zero) one (one + one)
>minValueOf2 = minValueOf testcaf2

therefore the type checker infers the types for these functions
together and all occurences of the functions 'testcaf2' and 'minValueOf2'
(inside these functions) will get the same type. Because of this
restriction the ambiguity disappears.

>2. If inferred type for testcaf1 (testcaf1 :: a | + a & one a & == a &
>zero a & minValue a) or for testcaf2 (testcaf2 :: a | + a & one a & ==
>a & zero a & minValue a) is inserted, compiler gives "internal
>overloading could not be solved" for both.

If the type of 'testcaf2' is specified, the compiler no longer has
to type the functions 'testcaf2' and 'minValueOf2' together. Instead
it can now first type 'minValueOf2' using the specified type for
'testcaf2', and then type 'testcaf2' using the inferred type of
'minValueOf2' that was just inferred. This enables more polymorphism.

In this case the extra polymorphism causes ambiguity, and overloading
cannot be resolved. This happens because the recursive call of 'testcaf2'
that occurs after calling 'minValueOf' from the first call of 'testcaf2'
no longer has to have the same type as the first call of 'testcaf2'.

Similarly the call of 'testcaf1' in 'testcaf1' no longer has to have
to same type as the first call.

>Why compiler does not eat types inferred by itself?

By specifying the type more polymorphism is allowed, which allows more
programs to be type checked. Unfortunately this may cause ambiguity
in overloading, causing an overloading error that doesn't occur
if the type is not specified.

By the way, a CAF must be defined with =:, otherwise it a function.

Kind regards,

John van Groningen