Sufficiently higher-rank record selectors fail to typecheck

There are certain situations where record selectors with higher-rank types will fail to typecheck unless the user enables ImpredicativeTypes. Here is one example, adapted from !2600 (comment 257654):

{-# LANGUAGE RankNTypes #-}
module Bug where

type S = Int -> (forall a. a -> a) -> Int

data T = MkT {unT :: S}
       | Dummy

This will fail to compile on GHC 8.0.2 or later:

$ /opt/ghc/8.10.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:6:15: error:
    • Cannot instantiate unification variable ‘a0’
      with a type involving polytypes: Int -> (forall a. a -> a) -> Int
        GHC doesn't yet support impredicative polymorphism
    • In the expression: Control.Exception.Base.recSelError "unT"#
      In a case alternative:
          _ -> Control.Exception.Base.recSelError "unT"#
  |
6 | data T = MkT {unT :: S}
  |               ^^^

Here is a similar example involving PatternSynonyms, adapted from !2600 (comment 255078):

{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}
module Bug where

type S = Int -> (forall a. a -> a) -> Int

newtype T = MkT S

unT' :: T -> S
unT' (MkT x) = x

pattern MkT' :: S -> T
pattern MkT' {unT} <- (unT' -> unT)

$ /opt/ghc/8.10.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:14:15: error:
    • Cannot instantiate unification variable ‘a0’
      with a type involving polytypes: Int -> (forall a. a -> a) -> Int
        GHC doesn't yet support impredicative polymorphism
    • In the expression: Control.Exception.Base.recSelError "unT"#
      In a case alternative:
          _ -> Control.Exception.Base.recSelError "unT"#
      In the declaration for pattern synonym ‘MkT'’
   |
14 | pattern MkT' {unT} <- (unT' -> unT)
   |               ^^^

The underlying cause behind both of these failures is the same. GHC generates HsBinds for unT that look roughly like this:

unT :: T -> S
unT (MkT x) = x
unT _       = recSelError "unT'"#

Note that the type of recSelError is forall r (a :: TYPE r). Addr# -> a. Therefore, when used in the right-hand side of unT, GHC attempts to instantiate a with Int -> (forall a. a -> a) -> Int. But this requires ImpredicativeTypes, so GHC rejects it.

There's no real reason why a user should have to explicitly enable ImpredicativeTypes in order to make this program typecheck, however. GHC could just as well generate the following HsBinds:

unT :: T -> S
unT (MkT x) = x
unT _       = recSelError @_ @S "unT"#

And then GHC could enable ImpredicativeTypes (and RankNTypes) internally when typechecking unT. This is very similar to a trick that is used in TcDeriv—see Note [Newtype-deriving instances].

Fixing this is a prerequisite for #17775 (closed), since simplified subsumption makes this bug even more likely to occur than it does currently. See the discussion beginning at !2600 (comment 255078).