stuck because overloading-by-typeclasses sucks

Using typeclasses for overloading clutters all users of the typeclass
with an extra layer of indirection that would need to be unfolded in all
proofs. Condemning all downstream Ltac to handling a new layer of
definitions that have no semantic dignificance is suboptimal design (and
encourages even worse design decisions like unfolding during rewriting).
Overloading should be fully resolved during type inference, the
resulting code must not be distinguishable from having the overloading
resolved manually before entering the code.

0 files changed, 0 insertions, 0 deletions