Design of tyepclasses
- As noted in #136, we currently have instances of tyepclasses that take in nontypeclass parameters.
- Typeclass inference in Coq can not infer these instances.
- One of the currently approaches (as noted in #136) is to restate these instances at the top of the file.
- However, in some files such as https://prosa.mpi-sws.org/branches/master/pretty/prosa.results.rs.fp.fully_preemptive.html these definitions are not restated.
- In these files, one or more lemmas that are used (along with
eauto
) silently ties the results of the lemma to specific definitions of the typeclass instances. - These is bad design in my opinion. Such proofs will become hard to maintain and change.
- The code is also not readable to developers.
- We need to find a better way of handling these tyepclass instances.
- In our concrete case, I don't think it make sense to put the nontypeclass parameters inside typeclasses.
- Then we can either make it a rule to state definitions with nontypeclass parameters fed at the top of file or explore using canonical instances instead of typeclasses
Edited by Sergey Bozhko