[Git][ghc/ghc][wip/torsten.schmits/16468] Relax defaulting of RuntimeRep/Levity when printing
Torsten Schmits (@torsten.schmits)
gitlab at gitlab.haskell.org
Fri Jun 23 12:22:37 UTC 2023
Torsten Schmits pushed to branch wip/torsten.schmits/16468 at Glasgow Haskell Compiler / GHC
Commits:
a9bab5b3 by Torsten Schmits at 2023-06-23T14:22:30+02:00
Relax defaulting of RuntimeRep/Levity when printing
Fixes #16468
MR: !10702
Only default RuntimeRep to LiftedRep when variables are bound by the toplevel forall
- - - - -
5 changed files:
- compiler/GHC/Iface/Type.hs
- compiler/GHC/Types/Unique/DFM.hs
- + testsuite/tests/ghci/scripts/T16468.script
- + testsuite/tests/ghci/scripts/T16468.stdout
- testsuite/tests/ghci/scripts/all.T
Changes:
=====================================
compiler/GHC/Iface/Type.hs
=====================================
@@ -987,7 +987,7 @@ ppr_ty ctxt_prec ty@(IfaceFunTy af w ty1 ty2) -- Should be a visible argument
| isVisibleFunArg af
= (pprTypeArrow af wthis <+> ppr_ty funPrec ty1) : ppr_fun_tail wnext ty2
ppr_fun_tail wthis other_ty
- = [pprTypeArrow af wthis <+> pprIfaceType other_ty]
+ = [pprTypeArrow af wthis <+> ppr_ty topPrec other_ty]
ppr_ty ctxt_prec (IfaceAppTy t ts)
= if_print_coercions
@@ -1044,9 +1044,11 @@ Haskell programs, so it makes little sense to make all users pay this
syntactic overhead.
For this reason it was decided that we would hide RuntimeRep variables
-for now (see #11549). We do this by defaulting all type variables of
-kind RuntimeRep to LiftedRep.
-Likewise, we default all Multiplicity variables to Many.
+for now (see #11549). We do this right in the pretty-printer, by pre-processing
+the type we are about to print, to default any type variables of kind RuntimeRep
+that are bound by toplevel invisible quantification to LiftedRep.
+Likewise, we default Multiplicity variables to Many and Levity variables to
+Lifted.
This is done in a pass right before pretty-printing
(defaultIfaceTyVarsOfKind, controlled by
@@ -1073,6 +1075,22 @@ metavariables are converted, skolem variables are not.
There's one exception though: TyVarTv metavariables should not be defaulted,
as they appear during kind-checking of "newtype T :: TYPE r where..."
(test T18357a). Therefore, we additionally test for isTyConableTyVar.
+
+Wrinkles:
+
+(W1) The loop 'go' in 'defaultIfaceTyVarsOfKind' passes a Bool flag, 'rank1',
+ around that indicates whether we haven't yet descended into the arguments
+ of a function type.
+ This is used to decide whether newly bound variables are eligible for
+ defaulting – we do not want contravariant foralls to be defaulted because
+ that would result in an incorrect, rather than specialized, type.
+ For example:
+ ∀ p (r :: RuntimeRep) . (∀ (r' :: RuntimeRep) . p r') -> p r
+ We want to default @r@, but not @r'@.
+ When examining the first forall, 'rank1' is True.
+ The toplevel function type is matched as IfaceFunTy, where we recurse into
+ 'go' by passing False for 'rank1'.
+ The forall in the first argument then skips adding a substitution for 'r''.
-}
-- | Default 'RuntimeRep' variables to 'LiftedRep',
@@ -1097,28 +1115,29 @@ as they appear during kind-checking of "newtype T :: TYPE r where..."
defaultIfaceTyVarsOfKind :: Bool -- ^ default 'RuntimeRep'/'Levity' variables?
-> Bool -- ^ default 'Multiplicity' variables?
-> IfaceType -> IfaceType
-defaultIfaceTyVarsOfKind def_rep def_mult ty = go emptyFsEnv ty
+defaultIfaceTyVarsOfKind def_rep def_mult ty = go emptyFsEnv True ty
where
go :: FastStringEnv IfaceType -- Set of enclosing forall-ed RuntimeRep/Levity/Multiplicity variables
+ -> Bool -- Are we in a toplevel forall, where defaulting is allowed for RR/L?
-> IfaceType
-> IfaceType
- go subs (IfaceForAllTy (Bndr (IfaceTvBndr (var, var_kind)) argf) ty)
+ go subs rank1 (IfaceForAllTy (Bndr (IfaceTvBndr (var, var_kind)) argf) ty)
| isInvisibleForAllTyFlag argf -- Don't default *visible* quantification
-- or we get the mess in #13963
- , Just substituted_ty <- check_substitution var_kind
+ , Just substituted_ty <- check_substitution rank1 var_kind
= let subs' = extendFsEnv subs var substituted_ty
-- Record that we should replace it with LiftedRep/Lifted/Many,
-- and recurse, discarding the forall
- in go subs' ty
+ in go subs' rank1 ty
- go subs (IfaceForAllTy bndr ty)
- = IfaceForAllTy (go_ifacebndr subs bndr) (go subs ty)
+ go subs rank1 (IfaceForAllTy bndr ty)
+ = IfaceForAllTy (go_ifacebndr subs rank1 bndr) (go subs rank1 ty)
- go subs ty@(IfaceTyVar tv) = case lookupFsEnv subs tv of
+ go subs _ ty@(IfaceTyVar tv) = case lookupFsEnv subs tv of
Just s -> s
Nothing -> ty
- go _ ty@(IfaceFreeTyVar tv)
+ go _ _ ty@(IfaceFreeTyVar tv)
-- See Note [Defaulting RuntimeRep variables], about free vars
| def_rep
, GHC.Core.Type.isRuntimeRepTy (tyVarKind tv)
@@ -1138,47 +1157,49 @@ defaultIfaceTyVarsOfKind def_rep def_mult ty = go emptyFsEnv ty
| otherwise
= ty
- go subs (IfaceTyConApp tc tc_args)
- = IfaceTyConApp tc (go_args subs tc_args)
+ go subs rank1 (IfaceTyConApp tc tc_args)
+ = IfaceTyConApp tc (go_args subs rank1 tc_args)
- go subs (IfaceTupleTy sort is_prom tc_args)
- = IfaceTupleTy sort is_prom (go_args subs tc_args)
+ go subs rank1 (IfaceTupleTy sort is_prom tc_args)
+ = IfaceTupleTy sort is_prom (go_args subs rank1 tc_args)
- go subs (IfaceFunTy af w arg res)
- = IfaceFunTy af (go subs w) (go subs arg) (go subs res)
+ go subs rank1 (IfaceFunTy af w arg res)
+ = IfaceFunTy af (go subs rank1 w) (go subs False arg) (go subs False res)
- go subs (IfaceAppTy t ts)
- = IfaceAppTy (go subs t) (go_args subs ts)
+ go subs rank1 (IfaceAppTy t ts)
+ = IfaceAppTy (go subs rank1 t) (go_args subs rank1 ts)
- go subs (IfaceCastTy x co)
- = IfaceCastTy (go subs x) co
+ go subs rank1 (IfaceCastTy x co)
+ = IfaceCastTy (go subs rank1 x) co
- go _ ty@(IfaceLitTy {}) = ty
- go _ ty@(IfaceCoercionTy {}) = ty
+ go _ _ ty@(IfaceLitTy {}) = ty
+ go _ _ ty@(IfaceCoercionTy {}) = ty
- go_ifacebndr :: FastStringEnv IfaceType -> IfaceForAllBndr -> IfaceForAllBndr
- go_ifacebndr subs (Bndr (IfaceIdBndr (w, n, t)) argf)
- = Bndr (IfaceIdBndr (w, n, go subs t)) argf
- go_ifacebndr subs (Bndr (IfaceTvBndr (n, t)) argf)
- = Bndr (IfaceTvBndr (n, go subs t)) argf
+ go_ifacebndr :: FastStringEnv IfaceType -> Bool -> IfaceForAllBndr -> IfaceForAllBndr
+ go_ifacebndr subs rank1 (Bndr (IfaceIdBndr (w, n, t)) argf)
+ = Bndr (IfaceIdBndr (w, n, go subs rank1 t)) argf
+ go_ifacebndr subs rank1 (Bndr (IfaceTvBndr (n, t)) argf)
+ = Bndr (IfaceTvBndr (n, go subs rank1 t)) argf
- go_args :: FastStringEnv IfaceType -> IfaceAppArgs -> IfaceAppArgs
- go_args _ IA_Nil = IA_Nil
- go_args subs (IA_Arg ty argf args)
- = IA_Arg (go subs ty) argf (go_args subs args)
+ go_args :: FastStringEnv IfaceType -> Bool -> IfaceAppArgs -> IfaceAppArgs
+ go_args _ _ IA_Nil = IA_Nil
+ go_args subs rank1 (IA_Arg ty argf args)
+ = IA_Arg (go subs rank1 ty) argf (go_args subs rank1 args)
- check_substitution :: IfaceType -> Maybe IfaceType
- check_substitution (IfaceTyConApp tc _)
+ check_substitution :: Bool -> IfaceType -> Maybe IfaceType
+ check_substitution rank1 (IfaceTyConApp tc _)
| def_rep
, tc `ifaceTyConHasKey` runtimeRepTyConKey
+ , rank1
= Just liftedRep_ty
| def_rep
, tc `ifaceTyConHasKey` levityTyConKey
+ , rank1
= Just lifted_ty
| def_mult
, tc `ifaceTyConHasKey` multiplicityTyConKey
= Just many_ty
- check_substitution _ = Nothing
+ check_substitution _ _ = Nothing
-- | The type ('BoxedRep 'Lifted), also known as LiftedRep.
liftedRep_ty :: IfaceType
@@ -1367,7 +1388,7 @@ ppr_sigma show_forall ctxt_prec iface_ty
-- Then it could handle both invisible and required binders, and
-- splitIfaceReqForallTy wouldn't be necessary here.
in ppr_iface_forall_part show_forall invis_tvs theta $
- sep [pprIfaceForAll req_tvs, ppr tau']
+ sep [pprIfaceForAll req_tvs, ppr_ty topPrec tau']
pprUserIfaceForAll :: [IfaceForAllBndr] -> SDoc
pprUserIfaceForAll tvs
=====================================
compiler/GHC/Types/Unique/DFM.hs
=====================================
@@ -94,7 +94,7 @@ import qualified Data.IntSet as I
-- order then `udfmToList` returns them in deterministic order.
--
-- There is an implementation cost: each element is given a serial number
--- as it is added, and `udfmToList` sorts it's result by this serial
+-- as it is added, and `udfmToList` sorts its result by this serial
-- number. So you should only use `UniqDFM` if you need the deterministic
-- property.
--
=====================================
testsuite/tests/ghci/scripts/T16468.script
=====================================
@@ -0,0 +1,27 @@
+import GHC.Types (RuntimeRep (..), Levity (..), TYPE)
+import Data.Proxy
+
+f :: forall p (r' :: RuntimeRep). (forall (r :: RuntimeRep). Int -> p r) -> p r'; f x = x 5
+g :: forall p. Int -> forall (r :: RuntimeRep). p r; g _ = undefined
+g' :: Int -> forall p (r :: RuntimeRep). p r; g' _ = undefined
+h :: Int -> forall (r :: RuntimeRep). TYPE r; h _ = undefined
+i :: forall (r :: RuntimeRep). Int -> TYPE r; i _ = undefined
+j :: forall p. Eq (p ('BoxedRep 'Lifted)) => Int -> forall (r :: RuntimeRep). p r; j _ = undefined
+k :: forall p (r' :: RuntimeRep). Eq (p r') => (forall (r :: RuntimeRep). Eq (p r) => Int -> p r) -> p r'; k x = x 5
+
+:type f
+:type g
+:type g'
+:type h
+:type i
+:type j
+:type k
+
+:set -fprint-explicit-runtime-reps
+:type f
+:type g
+:type g'
+:type h
+:type i
+:type j
+:type k
=====================================
testsuite/tests/ghci/scripts/T16468.stdout
=====================================
@@ -0,0 +1,20 @@
+f :: (forall (r :: RuntimeRep). Int -> p r)
+ -> p GHC.Types.LiftedRep
+g :: Int -> forall (r :: RuntimeRep). p r
+g' :: Int -> forall (p :: RuntimeRep -> *) (r :: RuntimeRep). p r
+h :: Int -> forall (r :: RuntimeRep). TYPE r
+i :: Int -> *
+j :: Eq (p GHC.Types.LiftedRep) =>
+ Int -> forall (r :: RuntimeRep). p r
+k :: Eq (p GHC.Types.LiftedRep) =>
+ (forall (r :: RuntimeRep). Eq (p r) => Int -> p r)
+ -> p GHC.Types.LiftedRep
+f :: (forall (r :: RuntimeRep). Int -> p r) -> p r'
+g :: Int -> forall (r :: RuntimeRep). p r
+g' :: Int -> forall (p :: RuntimeRep -> *) (r :: RuntimeRep). p r
+h :: Int -> forall (r :: RuntimeRep). TYPE r
+i :: Int -> TYPE r
+j :: Eq (p GHC.Types.LiftedRep) =>
+ Int -> forall (r :: RuntimeRep). p r
+k :: Eq (p r') =>
+ (forall (r :: RuntimeRep). Eq (p r) => Int -> p r) -> p r'
=====================================
testsuite/tests/ghci/scripts/all.T
=====================================
@@ -375,3 +375,4 @@ test('T22695', normal, ghci_script, ['T22695.script'])
test('T22817', normal, ghci_script, ['T22817.script'])
test('T22908', normal, ghci_script, ['T22908.script'])
test('T23062', normal, ghci_script, ['T23062.script'])
+test('T16468', normal, ghci_script, ['T16468.script'])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a9bab5b3d4c8dc041502d47e54dfe40f928c021c
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a9bab5b3d4c8dc041502d47e54dfe40f928c021c
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/20230623/ca0abce1/attachment-0001.html>
More information about the ghc-commits
mailing list