Make SpecConstr deal with casts better

This patch does two things, to fix #23209:

* It improves SpecConstr so that it no longer quantifies over
  coercion variables.  See Note [SpecConstr and casts]

* It improves the rule matcher to deal nicely with the case where
  the rule does not quantify over coercion variables, but the the
  template has a cast in it.  See Note [Casts in the template]