Note [SpecConstr and casts]

Consider (#14270) a call like

    let f = e
    in ... f (K @(a |> cv)) ...

where 'cv' is a coercion variable not in scope at f's definition site.
If we aren't careful we'll get

    let $sf a cv = e (K @(a |> cv))
        RULE "SC:f" forall a cv.  f (K @(a |> cv)) = $sf a co
        f = e
    in ...

But alas, when we match the call we may fail to bind 'co', because the rule
matcher in GHC.Core.Rules cannot reliably bind coercion variables that appear
in casts (see Note [Casts in the template] in GHC.Core.Rules).

This seems intractable (see #23209). So:

* Key point: we /never/ quantify over coercion variables in a SpecConstr rule.
  If we would need to quantify over a coercion variable, we just discard the
  call pattern. See the test for `bad_covars` in callToPat.

* However (#14936) we /do/ still allow casts in call patterns. For example
     f ((e1,e2) |> sym co)
  where, say,
     f  :: Foo -> blah   -- Foo is a newtype
     f = f_rhs
     co :: Foo ~R (Int,Int)
  We want to specialise on that pair!

So for our function f, we might generate
  RULE forall x y.  f ((x,y) |> co) = $sf x y
  $sf x y = f_rhs ((x,y) |> co)

This works provided the free vars of `co` are either in-scope at the
definition of `f`, or quantified. For the latter, suppose `f` was polymorphic:

     f2  :: Foo2 a -> blah   -- Foo is a newtype
     f2 = f2_rhs
     co2 :: Foo a ~R (a,a)

Then it's fine for `co2` to mention `a`.  We'll get
  RULE forall a (x::a) (y::a).  f2 @a ((x,y) |> co2) = $sf2 a x y
  $sf2 @a x y = f2_rhs ((x,y) |> co2)