Note [Lambdas in the template]

If we match
   Template:   (\x. blah_template)
   Target:     (\y. blah_target)
then we want to match inside the lambdas, using rv_lcl to match up
x and y.

But what about this?
   Template   (\x. (blah1 |> cv))
   Target     (\y. blah2) |> co

This happens quite readily, because the Simplifier generally moves
casts outside lambdas: see Note [Casts and lambdas] in
GHC.Core.Opt.Simplify.Utils. So, tiresomely, we want to push `co`
back inside, which is what `exprIsLambda_maybe` does.  But we've
stripped off that cast, so now we need to put it back, hence mkCastMCo.

Unlike the target, where we attempt eta-reduction, we do not attempt
to eta-reduce the template, and may therefore fail on
  Template:   \x. f True x
  Target      f True

It's not especially easy to deal with eta reducing the template,
and never happens, because no one write eta-expanded left-hand-sides.