QualifiedDo causes Core lint error (with my typechecker plugin)

Summary

I'm trying to develop a plugin that automatically solves transitivity of a type class that I've defined myself:

type (<=) :: (Type -> Type) -> (Type -> Type) -> Constraint
class f <= g where
  inj :: f x -> g x

-- These are overlapping, but our plugin will resolve the overlap.

instance f <= f where
  inj = id

instance forall f g h. (f <= g, g <= h) => f <= h where
  inj = inj @g @h . inj @f @g

However, I'm running into an error that I cannot explain.

The error occurs in the hsapply function which is defined like this:

hsapply :: Free MySig u (a -> b) -> Free MySig u a -> Free MySig u b
hsapply x y = Main.do
  x' <- x
  y' <- injfree y
  Free (HsApply (inj x') y' (coerce Pure))

But the error disappears if I manually use my own >>=:

hsapply :: Free MySig u (a -> b) -> Free MySig u a -> Free MySig u b
hsapply x y =
  x Main.>>= \x' ->
  injfree y Main.>>= \y' -> 
  Free (HsApply (inj x') y' (coerce Pure))

The type of my bind is:

(>>=) :: UFunctor f => Free f u a -> (forall u'. (u <= u') => u' a -> Free f u' b) -> Free f u b

Steps to reproduce

1. Clone https://github.com/noughtmare/transitive-constraint-plugin
2. Check out this problematic commit: git checkout bb7f4cfec371f6053bb3f4d33130bc7a67166596
3. Try to build the 'Free' example: cabal build exe:free-example

This produces a core lint error:

    Out of scope: $d<=_a1fj :: u_a1eN <= u'_a1eW
                  [LclId]

The relevant snippet of Core is:

               >>=
                 @MySig
                 @u'_a1eW
                 @a_a1eO
                 @b_a1eP
                 $dUFunctor_a1f9
                 (injfree @u_a1eN @u'_a1eW @a_a1eO $d<=_a1fj y_aXB)
                 (\ (@(u'_a1fa :: * -> *)) ($d<=_a1fb :: u'_a1eW <= u'_a1fa) ->
                    let {
                      $d<=_a1fj :: u_a1eN <= u'_a1eW
                      [LclId]
                      $d<=_a1fj = $d<=_a1eX } in

Note how the $d<=_a1fj is referenced outside the let it is bound in.

But my plugin does not produce that reference as far as I can tell. My tracing (source) shows that it only touches that name once and in that case it produces a contradiction:

contradiction: [W] $d<=_a1fj {0}:: u_a1eN[sk:1] <= u'_a1eW[sk:2] (CDictCan)

Expected behavior

The Free.hs example should compile without issues.

Environment

• GHC version used: 9.6.3