Coercion logic

[David Feuer]

At present, any time we write a function with a `Coercible`
constraint, we must take great care to choose `Coercible a b` or
`Coercible b a` depending on which will ultimately lead to fewer silly
conversions. This is particularly sad because the whole Coercible
mechanism guarantees that these have exactly the same run-time
representation, and because People Wiser Than Me believe Coercible
should *always* remain symmetric. My (admittedly reptilian) brain
wonders what it would take to tell the type checker that

forall a b . Coercible a b ~ Coercible b a

and have it over with.

David Feuer