Fundeps and quantified constructors

anatoli [email protected]
Thu, 8 Feb 2001 00:29:11 -0800 (PST)


--- Tom Pledger <[email protected]> wrote:
> anatoli writes:
>  :
>  | The same error message is given for
>  | 
>  | > data Foo a = (Eq b) => MkFoo b
> 
> Since the type variable a is orphaned, how about reducing it to this?
> 
> > data Foo = forall b . Eq b => MkFoo b

This is possible (the semantics is different of course).
What I want to do is, given a multi-parameter context,
orphan one type variable leaving the other intact,
and that's not possible now. I can only orphan all or preserve 
all.

> 
> so that  MkFoo :: Eq b => b -> Foo
> 
>  | I don't know whether this is intended behaviour; IMHO
>  | it should be treated identically to
>  | 
>  | > data Foo a = MkFoo (Eq a => a)
> 
> Isn't the Foo-ed a hidden by the Eq-ed a in this example too?  i.e.
> 
> > data Foo = MkFoo (forall a . Eq a => a)

It appears that both examples are wrong, or at least Hugs thinks so.
The first MkFoo happily accepts any type, not just of class Eq:

Main> :t MkFoo head
MkFoo head :: Foo ([a] -> a)

The second accepts nothing of interest:
Main> :t MkFoo 'a' 
ERROR: Inferred type is not general enough
*** Expression    : 'a'
*** Expected type : Eq a => a
*** Inferred type : Eq Char => Char

Hm... The more I experiment with this, the less I understand.

It seems that the only correct place to put the quantifier
is before the data constructor, and the context may go either
before the type constructor or after the quantifier. This is 
very unfortunate. How can I correctly write something to this
effect:

> data Quick a = Eq  a => Unsorted [a]
>              | Ord a => Sorted (Tree a)

???

Regards
-- 
anatoli

__________________________________________________
Do You Yahoo!?
Get personalized email addresses from Yahoo! Mail - only $35 
a year!  http://personal.mail.yahoo.com/