diff options
author | Ryan Scott <ryan.gl.scott@gmail.com> | 2020-04-03 08:53:14 -0400 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-04-04 07:07:58 -0400 |
commit | bd75e5da0f1f05f107325733b570bf28b379d2f2 (patch) | |
tree | 3da9fb9c1427ea99205a08546126b6ee4e2d4411 /compiler | |
parent | 40a85563a46c682eaab5fdf970f7c46afca78cb3 (diff) | |
download | haskell-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.
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/typecheck/TcTyDecls.hs | 28 |
1 files changed, 28 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. -} |