Notes: need a example of delayed reflexivity coercion

As discussed at !12947 (comment 578145), when checking, for the sake of linearity, that a coercion is reflexivity, we have to delay the check until the desugarer. This is a purely empirical fact: when we only do checks on the fly, some things which should typecheck don't. But I believe that nobody has an intuitive understanding of why.

The goal of this issue is to come up with a small example, and add it to Note [Coercions returned from tcSubMult] in GHC.Tc.Utils.Unify (I'm leaving a dedicated TODO there).