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).