Note [Casts in the template]

This Note concerns `matchTemplateCast`.  Consider the definition
  f x = e,
and SpecConstr on call pattern
  f ((e1,e2) |> co)

The danger is that We'll make a RULE
   RULE forall a,b,g.  f ((a,b)|> g) = $sf a b g
   $sf a b g = e[ ((a,b)|> g) / x ]

This requires the rule-matcher to bind the coercion variable `g`.
That is Very Deeply Suspicious:

* It would be unreasonable to match on a structured coercion in a pattern,
  such as    RULE   forall g.  f (x |> Sym g) = ...
  because the strucure of a coercion is arbitrary and may change -- it's their
  /type/ that matters.

* We considered insisting that in a template, in a cast (e |> co), the the cast
  `co` is always a /variable/ cv.  That looks a bit more plausible, but #23209
  (and related tickets) shows that it's very fragile.  For example suppose `e`
  is a variable `f`, and the simplifier has an unconditional substitution
     [f :-> g |> co2]
  Now the rule LHS becomes (f |> (co2 ; cv)); not a coercion variable any more!

In short, it is Very Deeply Suspicious for a rule to quantify over a coercion
variable.  And SpecConstr no longer does so: see Note [SpecConstr and casts] in
SpecConstr.

Wrinkles:

(CT0) It is, however, OK for a cast to appear in a template provided the cast mentions
  none of the template variables.  For example
      newtype N a = MkN (a,a)    -- Axiom ax:N a :: (a,a) ~R N a
      f :: N a -> bah
      RULE forall b x:b y:b. f @b ((x,y) |> (axN @b)) = ...
  When matching we can just move these casts to the other side:
      match (tmpl |> co) tgt  -->   match tmpl (tgt |> sym co)
  See matchTemplateCast.

(CT1) We need to be careful about scoping, and to match left-to-right, so that we
  know the substitution [a :-> b] before we meet (co :: (a,a) ~R N a), and so we
  can apply that substitition

(CT2) Annoyingly, we still want support one case in which the RULE quantifies
  over a coercion variable: the dreaded map/coerce RULE.
  See Note [Getting the map/coerce RULE to work] in GHC.Core.SimpleOpt.

  Since that can happen, matchTemplateCast laboriously checks whether the
  coercion mentions a template coercion variable; and if so does the Very Deeply
  Suspicious `match_co` instead.  It works fine for map/coerce, where the
  coercion is always a variable and will (robustly) remain so.

See also
* Note [Coercion arguments]
* Note [Matching coercion variables] in GHC.Core.Unify.
* Note [Cast swizzling on rule LHSs] in GHC.Core.Opt.Simplify.Utils:
  sm_cast_swizzle is switched off in the template of a RULE