Applicative Do should go via HsExpansion Route
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
Edited by sheaf