[Note to the Haskell list.  The question this thread is discussing
is whether the H98 rule that all the functions in a mutually 
recursive group must have the same context, is a show stopper.]

| Oeer.  Come to think of it, if f is getting the dictionary 
| (in the real world
| example) from the context, rather than from the existential 
| type, I fear it may be getting the wrong dictionary, and will 
| crash badly when I try to run the code.  

No I don't think that can happen. But I have thought of a test
case

data T = forall a. Eq a => MkT a a T
         | Nil

f :: T -> Bool
f Nil = True
f (MkT x y t) = g x y t

g  :: Eq b => b -> b -> T -> Bool
g x y t = (x==y) && f t


Notice that
  (a) f and g are mutually recursive
  (b) They have different contexts in their type sig
  (c)  If they were made the same, f would get an
        ambiguous type  f :: Eq a => T -> Bool
  (d) Haskell's polymorphic recursion is essential here;
        each call to g may be at a different type

So it looks to me that, in the presence of existentials, the H98
rule goes from being moot to being throughly awkward. 

Mark's THIH paper shows that there's no real need for the rule,
because one can type-check the bindings without type sigs as
a group, and then the ones with type sigs one by one.  

But what happens for pattern-bindings that bind more than
one variable.  Must all those variables have the same context?
(I hope so.)

Needless to say, I'm not proposing any changes in H98!  But
I thought the example would be of interest.  Maybe it's well known,
but it wasn't to me.

Simon

_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Reply via email to