  Type classes are one of Haskell's most popular features and extend its type
system with ad-hoc polymorphism. Since their conception, there were useful
features that could not be offered because of the desire to offer two
correctness properties: coherence and global uniqueness of instances. Coherence
essentially guarantees that program semantics are independent from type-checker
internals. Global uniqueness of instances is relied upon by libraries for
enforcing, for example, that a single order relation is used for all
manipulations of an ordered binary tree.
  The features that could not be offered include explicit dictionary
application and local instances, which would be highly useful in practice. We
propose a new design for offering explicit dictionary application, without
compromising coherence and global uniqueness. We introduce a novel criterion
based on GHC's type argument roles to decide when a dictionary application is
safe with respect to global uniqueness of instances. We preserve coherence by
detecting potential sources of incoherence, and prove it formally. Moreover,
our solution makes it possible to use local dictionaries. In addition to
developing our ideas formally, we have implemented a working prototype in GHC.
  This report contains the full formalisation and coherence proof.
