summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRyan Scott <ryan.gl.scott@gmail.com>2020-04-03 08:53:14 -0400
committerMarge Bot <ben+marge-bot@smart-cactus.org>2020-04-04 07:07:58 -0400
commitbd75e5da0f1f05f107325733b570bf28b379d2f2 (patch)
tree3da9fb9c1427ea99205a08546126b6ee4e2d4411
parent40a85563a46c682eaab5fdf970f7c46afca78cb3 (diff)
downloadhaskell-bd75e5da0f1f05f107325733b570bf28b379d2f2.tar.gz
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.
-rw-r--r--compiler/typecheck/TcTyDecls.hs28
-rw-r--r--testsuite/tests/typecheck/should_compile/T18005.hs30
-rw-r--r--testsuite/tests/typecheck/should_compile/all.T1
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, [''])