  Graded modal types systems and coeffects are becoming a standard formalism to
deal with context-dependent computations where code usage plays a central role.
The theory of program equivalence for modal and coeffectful languages, however,
is considerably underdeveloped if compared to the denotational and operational
semantics of such languages. This raises the question of how much of the theory
of ordinary program equivalence can be given in a modal scenario. In this work,
we show that coinductive equivalences can be extended to a modal setting, and
we do so by generalising Abramsky's applicative bisimilarity to coeffectful
behaviours. To achieve this goal, we develop a general theory of ternary
program relations based on the novel notion of a comonadic lax extension, on
top of which we define a modal extension of Abramsky's applicative bisimilarity
(which we dub modal applicative bisimilarity). We prove such a relation to be a
congruence, this way obtaining a compositional technique for reasoning about
modal and coeffectful behaviours. But this is not the end of the story: we also
establish a correspondence between modal program relations and program
distances. This correspondence shows that modal applicative bisimilarity and (a
properly extended) applicative bisimilarity distance coincide, this way
revealing that modal program equivalences and program distances are just two
sides of the same coin.
