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
Replying to
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
2
2
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