[Blaisorblade0]

Good point, but never seen typeclass coherence with dependent types (in either Coq or the various versions of the Agda design). Not sure for Isabelle.

[dllthomas]

I'm not sure I can name another language with coherence, dependant types or not. To be fair, even GHC is half-hearted about it.