Impredicative instantiation of application fails under guarded positions
Consider the following declarations.
{-# LANGUAGE ImpredicativeTypes #-}
-- typechecks with signature, without signature, and inlining "test"
f1 = test
where
ids :: [forall a. a -> a]
ids = take 5 (repeat id)
test = ids ++ ids
-- typechecks with or without signature
f2 = Just test
where
ids :: [forall a. a -> a]
ids = take 5 (repeat id)
test = ids ++ ids
-- only typechecks with a signature
f3 = Just (ids ++ ids)
where
ids :: [forall a. a -> a]
ids = take 5 (repeat id)
test = ids ++ ids
I think all of these should typecheck.
Here is the error message I get for f3:
/Users/artin/Programming/projects/playground/src/PatBind.hs:32:12-21: error: [GHC-91028]
• Couldn't match expected type ‘a’
with actual type ‘[forall a. a -> a]’
Cannot equate type variable ‘a’
with a type involving polytypes: [forall a1. a1 -> a1]
‘a’ is a rigid type variable bound by
the inferred type of f3 :: Maybe a
at /Users/artin/Programming/projects/playground/src/PatBind.hs:(32,1)-(36,21)
• In the first argument of ‘Just’, namely ‘(ids ++ ids)’
In the expression: Just (ids ++ ids)
In an equation for ‘f3’:
f3
= Just (ids ++ ids)
where
ids :: [forall a. a -> a]
ids = take 5 (repeat id)
test = ids ++ ids
• Relevant bindings include
f3 :: Maybe a
(bound at /Users/artin/Programming/projects/playground/src/PatBind.hs:32:1)
|
32 | f3 = Just (ids ++ ids)
GHC version used: latest nightly. 9.11.20240412