Type applications break function matching

[ilyakooo0]

running the rule

forall a b. foo a b = foo b a

on the following file would succeed:

main = foo x y

while adding type applications to a function call would break matching the function and the rewrite would not be applied:

main = foo @Int x y

[xich]

Matching is syntactic, so this is expected. Does the rule forall t a b. foo @t a b = foo @t b a work? (@ not strictly necessary, but would distinguish from a term-level variable)

I'm not sure how we could spot this is the general case since we don't have access to the type of foo (retrie only parses).

[ilyakooo0]

No, it would not work. Type applications are not supported at all in rules. It will give an error.

[ilyakooo0]

I think ignoring type applications when matching would be far preferable to not matching at all. Right now if the codebase supports type applications, there is no reliable way of applying a rule to the codebase.