Various reasons for doing this:
- Most of the time we are interested in
oFunctor_car
, so it's really confusing thatoFunctor_diag
is a coercion - The coercion doesn't work well with the
Cofe
type class argument (see !257 (merged))---an underscore_
is needed when applying the coercion. - The coercion is very little used, so better to be explicit, especially in light of #240 (closed).
/cc @iris-users This is a breaking change.
This MR closes issue #240 (closed).