Skip to content

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)

@simonpj

@int-index

GHC version used: latest nightly. 9.11.20240412

Edited by Artin Ghasivand
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information