This was an interesting video by that covers how role annotations are important for enforcing data structure invariants in the presence of Data.Coercible:
Conversation
I find it interesting how similar issues pop up in type class mechanisms that allow for non-canonical instances. See section 4.3 of the Modular Implicits paper, where a solution (4.4) is to use an applicative functor: arxiv.org/pdf/1512.01895
read image description
ALT
Replying to
In dependent type systems (like Idris) you can avoid these issues by parameterising data structures with the instances that are critical for maintaining internal invariants.
1
Automated
