Solved: Typing problems with polymorphic recursion and typeclasses

[oleg@pobox.com]

Martin SULZMANN wrote:

> Here's a simplified version. 

> h :: (Show ha) => t -> ha
> h b = g (h b)
>  > > g:: (Show ga) => ga -> gb
>  > > g = undefined

In an attempt to discover the type signature of h, let us lift it:

> g:: (Show ga,Show gb) => ga -> gb
> g = undefined

> class (Show ha) => H t ha where
>     h:: t->ha
>     h b = g (h b)


gives us an error:

    Could not deduce (H t ha1) from the context (H t ha)
    Probable fix:
        Add (H t ha1) to the class or instance method `h'
    arising from use of `h' at /tmp/e.hs:10
    In the first argument of `g', namely `(h b)'
    In the definition of `h': g (h b)

However, if we change the class H into

> class (Show ha) => H t ha | t->ha where
>     h:: t->ha
>     h b = g (h b)

everything typechecks. It seems very hard for me to avoid the thought
that the type of the original h should be
	forall t ha. (Show ha) => t -> ha | t -> ha

or, to re-write it into valid Haskell,
	forall t ha. (H t ha) => t -> ha

That might answer my previous question...

Regarding your observation:

> g:: (Show ga) => ga -> gb
> g = undefined
> h :: (Show ha) => t -> ha
> h b = g (h b)

> Same problem occurs. Though this is strange.

> Consider type inference for 

> h b = g (h b)

> We generate the following constraints:

> th = tb -> ga, Show ga  -- results from g (h b)
> th = tb -> gb           -- taking into account h b = g (h b)

> In case of 

> h :: (Show ha) => t -> ha
> h b = g (h b)

> we additionally generate

> th = t -> ha, Show ha

> Overall, we find

>  th = tb -> ga, Show ga 
>  th = tb -> gb,
>  th = t -> ha, Show ha

> as my above calculation shows there shouldn't be a problem in the
> first place.

I think I can see the problem: if we have a function
	foo:: t1 -> t2
then GHC definitely knows that foo relates t1 and t2 by a functional
dependency -- indeed, foo is a function.

However, when presented with a type signature
	bar:: (C t3) => t3 -> t4
the compiler doesn't know if bar is a regular function, or if it is a
method in the class C. In either case, the signature is just the
same. If bar is a bona fide function, then t3 and t4 are related by a
functional dependency. If bar is a method of C, things are not so
clear. Well, they are clear for the single-parameter class C without
overlapping instances (which GHC actually allows). However, for
	baz:: (D t5 t6 t7) => t6 -> t8
there could conceivably be instances of baz which relate the same t6
to two different t8. That's why we have to explicitly specify the
functional dependency.

I guess this might probably answer the original question Levent Erkok
posed three years ago.