existential typing question

[Hal Daume III]

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
> 
> _______________________________________________
> Haskell mailing list
> Haskell@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell
>