Applicative Do should go via HsExpansion Route

See also

• #26516 (closed)
• #26517

Summary

Impredicativity does not play well with do-blocks expanding under ApplicativeDo Language pragma due to ill-designed 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: [GHC-91028]
    • 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: [GHC-46956]
    • 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