Although I'd read the restriction in advance, I nevertheless unwittingly
contrived to try and write a binding-group style pattern-match against
an existentially quantified data constructor. Oops. (Actually, I did
it twice, what's worse...) I can imagine this is indeed an irksome
thing to TC, but OTOH, it's not a very natural language restriction
either. What's worse, one is of course not able to use 'selectors' in
these cases, as they're immediately ill-typed. One saving grace was
that one _can_ use pattern guards, but since that's a non-standard
feature too, I feel I'm multiplying heterodoxy upon heteredoxy when I do
this.
What's worse, in the other caes, when I replaced the let-binding with an
auxiliary function call (pattern guards no use in this case), I ran into
_another_ restriction: mutually recursive functions needing to have the
same contexts. I believe, at least at first wink, that in the presence
of existentials this is _not_ an entirely sensible restriction, since if
one is 'unfolding' and 'folding' an existentially-typed DC, then chunks
of the context can disappear and reappear accordingly. (That is if one
has a group like f (EDC x) = ... f' x ...; f' x = ... f (EDC x) ...)
Comments, O implementors and designers?
Cheers,
Alex.
