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