To my last message:
> Jeffrey R. Lewis" <[EMAIL PROTECTED]> writes:
> >
> > foo :<= C a => a -> b roughly equiv to foo :: C _a => _a -> _b
> >
> > I can easily imagine that you might want some variables to be a bound, and
> > others to be exact, as in
> >
> > foo :: C a => a -> _b
> >
> > I don't think the above can be expressed with Claus' proposal.
> >
>
> You could, by being more explicit than usual:
>
> > foo :<= forall b => C a => a -> b
>
I forgot to add:
and this is exactly where problems begin,
since, besides harmless cases like
> foo :: forall b => C int => int -> b
you also want to allow instantiations such as
> foo :: forall b => C [b] => [b] -> b
Therefore
* either the ``metavariables'' approach makes sense,
where metavariables are context holes, and
we allow context substitution
* or we allow second order substitution.
In this second case, we have to distinguish between
> foo1 :<= forall b => C a => a -> b
which allows
> foo1 :: forall b => C int => int -> b
but not
> foo1 :: forall b => C [b] => [b] -> b
and
> foo2 :<= forall b => C (a b) => (a b) -> b
which allows both of
> foo2 :: forall b => C int => int -> b
and
> foo2 :: forall b => C [b] => [b] -> b
This second approach seems to be preferrable to me.
Wolfram
