Coerce for functions and path types

[valis]

Suppose that A coerces to B. Then it's not true that C -> A coerces to C -> B. We can fix that. Similarly, we can make a = {A} a' coerce to a = {B} a'.