[Git][ghc/ghc][wip/T18005] Enable ImpredicativeTypes internally when typechecking selector bindings

[Ryan Scott]

Ryan Scott pushed to branch wip/T18005 at Glasgow Haskell Compiler / GHC


Commits:
2e0f90b7 by Ryan Scott at 2020-04-03T10:44:05-04:00
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 changed files:

- compiler/typecheck/TcTyDecls.hs
- + testsuite/tests/typecheck/should_compile/T18005.hs
- testsuite/tests/typecheck/should_compile/all.T


Changes:

=====================================
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.
 -}


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


=====================================
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, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2e0f90b7084052aa9473a326b14b9247b3fde4cc

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2e0f90b7084052aa9473a326b14b9247b3fde4cc
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200403/2654d96e/attachment-0001.html>