Best How To :

I'm reading it as "given a term which requires l ~ r, return that term"

It's "given a term whose type contains l, return that term with all ls being substituted by rs in the type" (or in the other direction r -> l). It's a very neat trick, that allows you to delegate all cong, trans, subst and similar stuff to GHC.

Here is an example:

{-# LANGUAGE GADTs, DataKinds, PolyKinds, TypeFamilies, TypeOperators, RankNTypes #-}

data Nat = Z | S Nat

data Natty n where
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)

data Vec a n where
    Nil  :: Vec a Z
    Cons :: a -> Vec a n -> Vec a (S n)

type family (n :: Nat) :+ (m :: Nat) :: Nat where
    Z     :+ m = m
    (S n) :+ m = S (n :+ m)

assoc :: Natty n -> Natty m -> Natty p -> (((n :+ m) :+ p) ~ (n :+ (m :+ p)) => t) -> t
assoc  Zy     my py t = t
assoc (Sy ny) my py t = assoc ny my py t

coerce :: Natty n -> Natty m -> Natty p -> Vec a ((n :+ m) :+ p) -> Vec a (n :+ (m :+ p))
coerce ny my py xs = assoc ny my py xs

UPDATE

It's instructive to specialize assoc:

assoc' :: Natty n -> Natty m -> Natty p ->
            (((n :+ m) :+ p) ~ (n :+ (m :+ p)) => Vec a (n :+ (m :+ p)))
                                               -> Vec a (n :+ (m :+ p))
assoc'  Zy     my py t = t
assoc' (Sy ny) my py t = assoc ny my py t

coerce' :: Natty n -> Natty m -> Natty p -> Vec a ((n :+ m) :+ p) -> Vec a (n :+ (m :+ p))
coerce' ny my py xs = assoc' ny my py xs

Daniel Wagner explained what's going on in comments:

Or, to say it another way, you can read ((l ~ r) => t) -> t as, "given a term that is well typed assuming that l ~ r, return that same term from a context where we have proven l ~ r and discharged that assumption".

Let's elaborate the proving part.

In the assoc' Zy my py t = t case n is equal to Zy and hence we have

((Zy :+ m) :+ p) ~ (Zy :+ (m :+ p))

which reduces to

(m :+ p) ~ (m :+ p)

This is clearly identity and hence we can discharge that assumption and return t.

At each recursive step we maintain the

((n :+ m) :+ p) ~ (n :+ (m :+ p))

equation. So when assoc' (Sy ny) my py t = assoc ny my py t the equation becomes

((Sy n :+ m) :+ p) ~ (Sy n :+ (m :+ p))

which reduces to

 Sy ((n :+ m) :+ p) ~ Sy (n :+ (m :+ p))

due to the definition of (:+). And since constructors are injective

constructors_are_injective :: S n ~ S m => Vec a n -> Vec a m
constructors_are_injective xs = xs

the equation becomes

((n :+ m) :+ p) ~ (n :+ (m :+ p))

and we can call assoc' recursively.

Finally in the call of coerce' these two terms are unified:

 1. ((n :+ m) :+ p) ~ (n :+ (m :+ p)) => Vec a (n :+ (m :+ p))
 2.                                      Vec a ((n :+ m) :+ p)

Clearly Vec a ((n :+ m) :+ p) is Vec a (n :+ (m :+ p)) under the assumption that ((n :+ m) :+ p) ~ (n :+ (m :+ p)).