Enable ImpredicativeTypes internally when typechecking selector bindings

This is necessary for certain record selectors with higher-rank
types, such as the examples in #18005. See
`Note [Impredicative record selectors]` in `TcTyDecls`.

Fixes #18005.

3 files changed, 59 insertions, 0 deletions

diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs
index cd06e79b2d..cff4f3ed00 100644
--- a/compiler/typecheck/TcTyDecls.hs
+++ b/compiler/typecheck/TcTyDecls.hs
@@ -67,6 +67,7 @@ import Bag
 import FastString
 import FV
 import GHC.Types.Module
+import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad
 
@@ -831,6 +832,8 @@ tcRecSelBinds :: [(Id, LHsBind GhcRn)] -> TcM TcGblEnv
 tcRecSelBinds sel_bind_prs
   = tcExtendGlobalValEnv [sel_id | (L _ (IdSig _ sel_id)) <- sigs] $
     do { (rec_sel_binds, tcg_env) <- discardWarnings $
+                                     -- See Note [Impredicative record selectors]
+                                     setXOptM LangExt.ImpredicativeTypes $
                                      tcValBinds TopLevel binds sigs getGblEnv
        ; return (tcg_env `addTypecheckedBinds` map snd rec_sel_binds) }
   where
@@ -1029,4 +1032,29 @@ The selector we want for fld looks like this:
 The scrutinee of the case has type :R7T (Maybe b), which can be
 gotten by applying the eq_spec to the univ_tvs of the data con.
 
+Note [Impredicative record selectors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There are situations where generating code for record selectors requires the
+use of ImpredicativeTypes. Here is one example (adapted from #18005):
+
+  type S = (forall b. b -> b) -> Int
+  data T = MkT {unT :: S}
+         | Dummy
+
+We want to generate HsBinds for unT that look something like this:
+
+  unT :: 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 `(forall b. b -> b) -> Int`, which is impredicative.
+To make sure that GHC is OK with this, we enable ImpredicativeTypes interally
+when typechecking these HsBinds so that the user does not have to.
+
+Although ImpredicativeTypes is somewhat fragile and unpredictable in GHC right
+now, it will become robust when Quick Look impredicativity is implemented. In
+the meantime, using ImpredicativeTypes to instantiate the `a` type variable in
+recSelError's type does actually work, so its use here is benign.
 -}
diff --git a/testsuite/tests/typecheck/should_compile/T18005.hs b/testsuite/tests/typecheck/should_compile/T18005.hs
new file mode 100644
index 0000000000..9b4ddbd366
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18005.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ViewPatterns #-}
+module T18005 where
+
+type S1 = Int -> (forall a. a -> a) -> Int
+
+data T1a = MkT1a {unT1a :: S1}
+         | Dummy1
+
+newtype T1b = MkT1b S1
+
+unT1b' :: T1b -> S1
+unT1b' (MkT1b x) = x
+
+pattern MkT1b' :: S1 -> T1b
+pattern MkT1b' {unT1b} <- (unT1b' -> unT1b)
+
+type S2 = Int -> forall a. a -> a
+
+data T2a = MkT2a {unT2a :: S2}
+         | Dummy2
+
+newtype T2b = MkT2b S2
+
+unT2b' :: T2b -> S2
+unT2b' (MkT2b x) = x
+
+pattern MkT2b' :: S2 -> T2b
+pattern MkT2b' {unT2b} <- (unT2b' -> unT2b)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index dd416ad2de..9b60c6cfb0 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -701,3 +701,4 @@ test('T17710', normal, compile, [''])
 test('T17792', normal, compile, [''])
 test('T17024', normal, compile, [''])
 test('T17021a', normal, compile, [''])
+test('T18005', normal, compile, [''])