Skip to content

Something related to ImpredicativeTypes breaks due to "involving polytypes" preventing GHC.Exts.inline application from type-checking

The below fails, but very similar examples, e.g., without the r, succeed. This is rather important, because it breaks GHC.Exts.inline f for functions f like that in my (almost) real life code.

GHCi, version 9.3.20220316: https://www.haskell.org/ghc/  :? for help
ghci> :set -XImpredicativeTypes
ghci> f :: forall r. (forall a. Either a r -> Either a r) -> (); f _ = ()
ghci> id f

<interactive>:3:4: error:
    • Couldn't match expected type ‘a’
                  with actual type ‘(forall a. Either a r0 -> Either a r0) -> ()’
    • Cannot equate type variable ‘a’
      with a type involving polytypes:
        (forall a1. Either a1 r0 -> Either a1 r0) -> ()
      ‘a’ is a rigid type variable bound by
        the inferred type of it :: a
        at <interactive>:3:1-4
    • In the first argument of ‘id’, namely ‘f’
      In the expression: id f
      In an equation for ‘it’: it = id f
    • Relevant bindings include it :: a (bound at <interactive>:3:1)
ghci> (\x -> id x) (\x -> f x)

<interactive>:4:23: error:
    • Couldn't match expected type ‘Either a r0 -> Either a r0’
                  with actual type ‘p’
      ‘p’ is a rigid type variable bound by
        the inferred type of it :: p -> ()
        at <interactive>:4:1-24
    • In the first argument of ‘f’, namely ‘x’
      In the expression: f x
      In the first argument of ‘\ x -> id x’, namely ‘(\ x -> f x)’
    • Relevant bindings include
        x :: p (bound at <interactive>:4:16)
        it :: p -> () (bound at <interactive>:4:1)
Edited by Mikolaj Konarski
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information