There is an easy design choice - which Haskell didn't take - which would allow us to have transparent Identity functors, associative Compose and many others: Add a conversion rule to your language and don't eagerly expand definitions at the type level.
For example, in Coq you would write
Definition Identity a := a.
Definition Compose F G a := F (G a).
Instance: Functor Identity. Proof[...]
and so on. This works, since explicit conversion during type checking allows you to associate type classes to otherwise transparent definitions.
Of course, this is no silver bullet and complicates other things. Everything works out beautifully though, if you combine conversion with bidirectional type checking, at the expense of less powerful type inference.
For example, in Coq you would write
and so on. This works, since explicit conversion during type checking allows you to associate type classes to otherwise transparent definitions.Of course, this is no silver bullet and complicates other things. Everything works out beautifully though, if you combine conversion with bidirectional type checking, at the expense of less powerful type inference.