Solved: Typing problems with polymorphic recursion and typeclasses

[Martin SULZMANN]

 > First, let us distill the problem to the following few lines:
 > 
 > > f:: (Show fa) => fb -> fa
 > > f = undefined
 > >
 > > g:: (Show ga) => ga -> gb
 > > g = undefined
 > >
 > > -- h:: (Show fa) => t -> fa
 > > h b = f (g (h b))
 > 

Here's a simplified version. 

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

(*) 


Note that this implies ga=ha, gb=ha

The error message 

    Ambiguous type variable(s) `ha' in the constraint `Show ha'
    arising from use of `g' at HaskellMay03.hs:16
    In the definition of `h'': g (h' b)

suggests that ghc does not apply the unifier ha=ga.
I suspect the type computed out of the constraints from (*) is 
as follows:

(Show ga, Show ha) => t -> ha

Indeed hugs says

ERROR HaskellMay03.hs:13 - Cannot justify constraints in explicitly typed binding
*** Expression    : h
*** Type          : Show a => b -> a
*** Given context : Show a
*** Constraints   : Show c

That is, the type (Show ga, Show ha) => t -> ha does not conform
to the annotation (Show ha) => t -> ha.


In case we use scoped type variables

h2:: (Show t2) => t1 -> t2
h2 b :: g1a
  = g ((h2 b)::g1a)

we impose some additional constraints (ga=g1a, ha=g1a). This seems to 
resolve the problem, though, as my above calculation shows there
shouldn't be a problem in the first place.

E.g. Chameleon accepts without problem

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

or

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

This is the Chameleon equivalent to h2. Scoped type variables in
Chameleon refer to type annotations.

You can try this out by calling

chameleon -d HaskellMay03.hs

where

HaskellMay03.hs =

hconstraint Show  -- Chameleon does not know the Prelude.
                  -- We have to introduce type class constraints
                  -- explicitely 

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

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

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


Martin