Skolems can escape in arrow notation, resulting in Core Lint errors

This issue looks quite similar to #20469, but its root cause is quite different. This is the offending program:

{-# LANGUAGE Arrows, GADTs #-}
module ArrowPanic where

data A where
  A :: a -> B a -> A
data B a where
  B :: B ()

foo :: A -> ()
foo = proc a -> case a of
  A x B -> id -< x

$ ghc -c -dcore-lint ArrowPanic.hs
*** Core Lint errors : in result of Desugar (before optimization) ***
ArrowPanic.hs:10:1: warning:
    The type variable @a_aHa is out of scope

After desugaring, the RHS of foo includes expressions that look roughly like this (simplified and abbreviated for clarity):

arr @A @a_aHa (\(A @a_aHa x (B co)) -> x)
--      ↑           ⬑ skolem bound here
--      └ skolem used here (out of scope!)

The root cause here appears to be threefold:

1. Metavariables are created to represent various intermediate types, but the creation of those metavariables isn’t wrapped in escapeArrowScope, so they can freely unify with skolems introduced in the current arrow scope.

2. Even if they were wrapped in escapeArrowScope, that currently wouldn’t help, because escapeArrowScope doesn’t reset tcl_tclvl. That means the level of the fresh metavariables would still be too deep.

3. Even if escapeArrowScope did reset tcl_tclvl, that wouldn’t catch all such issues, because expressions like this could still cause trouble:

   proc v -> case v of
     A (x :: a) B -> id -< id @a

   The problem is the id @a expression does appear in the arrow scope, so typechecking it won’t be wrapped in escapeArrowScope. However, the desugared expression still won’t be lexically nested inside the binding site for a, so the reference will be out of scope.

Points 1 and 2 are, I believe, unique to this issue, since they involve incorrect scoping of unification variables. Point 3 is somewhat similar to #20469, since threading coercions through the desugaring is a similar challenge to threading type variables. However, threading existentials around seems significantly more challenging to achieve than threading coercions, as they can’t simply be boxed and packed into the environment tuple.