> >> {rules Num a=> x::a, y::[a] ==>
> x+y = [x]+y}
> >> instance Num a => Num [a] where ...
> >> one could expect for x :: Num b=>b the casting
> >> x + [x,y] -->
> [x] + [x,y]
> > Provided the two sides of the rules have the same overall type,
> > GHC will be happy. But since there are no side condition, your
> > rule will rewrite *every* x+y to [x]+y, which isn't what you
> > want I guess.
> > [..]
>
> Why? This rule contains the x::a, y::[a] condition,
> so 1+1 does not fit the rule, and 1+[1] does.
Hmm. That's true. My current matching algorithm doesn't compare
types when matching a pattern variable against a term, but perhaps
it should. It *does* match types when they occur in type applications;
e.g. length [True,False]
actually expands (after type checking) to
length Bool (True : False : nil)
The 'Bool' argument to length matches the 'forall' in length's type.
And the matching algorithm does match these type args.
Now I think about it, it is perhaps inconsistent not to match the
type of non-polymorphic variables too. I'll think some more about
that one.
Simon