existential typing question

[Dean Herington]

Consider:

class RT r t where rt :: r -> t

data D t = Dt t | forall r. RT r t => Dr r

f1 :: D t -> D t
f1 (Dr r) = Dt (rt r)

f2 :: D t -> D t
f2 = g
 where g :: D t -> D t
       g (Dr r) = Dt (rt r)

Your explanation well justifies the need for `f1`'s type declaration.  But I
still don't understand why `g` needs the same declaration.  Why doesn't
`f2`'s declaration suffice to specify that `g`'s input and output have the
same type?

By the way, I can't use the fundep approach to avoid the need for a type
declaration, because the two instances you mention are both possible.
Fortunately, it's not a problem to include the type declaration.

-- Dean


Hal Daume III wrote:

> Because you could have an instance:
>
>   instance RT r t1
>
> and another instance for a t2 /= t1:
>
>   instance RT r t2
>
> then when you say:
>
>   g (Dr r) = Dt (r t)
>
> then, 'r t' could either have type t1 or t2, thus giving the result value
> type 'Dt t1' or 'Dt t2'.
>
> If your class had fundeps 'r -> t', then this probably wouldn't be
> necessary.
>
> --
> Hal Daume III
>
>  "Computer science is no more about computers    | hdaume@isi.edu
>   than astronomy is about telescopes." -Dijkstra | www.isi.edu/~hdaume
>
> On Mon, 27 Jan 2003, Dean Herington wrote:
>
> > Can someone explain why the type declaration for `g` is required in the
> > following?
> >
> >
> > class RT r t where rt :: r -> t
> >
> > data D t = Dt t | forall r. RT r t => Dr r
> >
> > f :: D t -> D t
> > f = g
> >  where -- g :: D t -> D t
> >        g (Dr r) = Dt (rt r)
> >
> >
> > As given above, the program evokes these error messages:
> >
> > with GHC 5.04.2:
> > Bug4.hs:10:
> >     Could not deduce (RT r t1) from the context (RT r t)
> >     Probable fix:
> >         Add (RT r t1) to the existential context of a data constructor
> >     arising from use of `rt' at Bug4.hs:10
> >     In the first argument of `Dt', namely `(rt r)'
> >     In the definition of `g': Dt (rt r)
> >
> > with Hugs:
> > ERROR "Bug4.hs":6 - Cannot justify constraints in explicitly typed
> > binding
> > *** Expression    : f
> > *** Type          : D a -> D a
> > *** Given context : ()
> > *** Constraints   : RT _6 a
> >
> >
> > -- Dean