Applicative Do should go via HsExpansion Route
Summary
Impredicativity does not play well with do
blocks expanding under ApplicativeDo
Language pragma due to illdesigned tcSyntaxOp
(c.f. issues documented in wiki page)
Steps to reproduce
 test.hs
{# LANGUAGE ImpredicativeTypes, ApplicativeDo #}
module T where
t :: IO (forall a. a > a)
t = return id
p :: (forall a. a > a) > (Bool, Int)
p f = (f True, f 3)
 This typechecks (with QL)
foo1 = t >>= \x > return (p x)
 But this does *not* type check:
foo2 = do { x < t ; return (p x) }
$ ghc test.hs
Error:
test.hs:14:18: error: [GHC91028]
• Couldn't match type ‘a0’ with ‘forall a. a > a’
Expected: IO a0
Actual: IO (forall a. a > a)
Cannot instantiate unification variable ‘a0’
with a type involving polytypes: forall a. a > a
• In a stmt of a 'do' block: x < t
In the expression:
do x < t
return (p x)
In an equation for ‘foo2’:
foo2
= do x < t
return (p x)

14  foo2 = do { x < t ; return (p x) }
 ^
test.hs:14:32: error: [GHC46956]
• Couldn't match expected type ‘a > a’ with actual type ‘a0’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context:
forall a. a > a
at test.hs:14:32
• In the first argument of ‘p’, namely ‘x’
In a stmt of a 'do' block: return (p x)
In the expression:
do x < t
return (p x)
• Relevant bindings include x :: a0 (bound at test.hs:14:13)

14  foo2 = do { x < t ; return (p x) }
Expected behavior
It should type check and execute as expected
Environment
 GHC version used: 9.6, 9.9