[Git][ghc/ghc][wip/torsten.schmits/16468] Relax defaulting of RuntimeRep/Levity when printing

Torsten Schmits (@torsten.schmits) gitlab at gitlab.haskell.org
Mon Jun 26 20:28:11 UTC 2023



Torsten Schmits pushed to branch wip/torsten.schmits/16468 at Glasgow Haskell Compiler / GHC


Commits:
5305ee3f by Torsten Schmits at 2023-06-26T22:28:03+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
=====================================
@@ -821,7 +821,7 @@ pprIfaceLamBndr (b, IfaceNoOneShot) = ppr b
 pprIfaceLamBndr (b, IfaceOneShot)   = ppr b <> text "[OneShot]"
 
 pprIfaceIdBndr :: IfaceIdBndr -> SDoc
-pprIfaceIdBndr (w, name, ty) = parens (ppr name <> brackets (ppr w) <+> dcolon <+> ppr ty)
+pprIfaceIdBndr (w, name, ty) = parens (ppr name <> brackets (ppr_ty_nested w) <+> dcolon <+> ppr_ty_nested ty)
 
 {- Note [Suppressing binder signatures]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -881,7 +881,7 @@ pprIfaceTvBndr :: IfaceTvBndr -> SuppressBndrSig -> UseBndrParens -> SDoc
 pprIfaceTvBndr (tv, ki) (SuppressBndrSig suppress_sig) (UseBndrParens use_parens)
   | suppress_sig             = ppr tv
   | isIfaceLiftedTypeKind ki = ppr tv
-  | otherwise                = maybe_parens (ppr tv <+> dcolon <+> ppr ki)
+  | otherwise                = maybe_parens (ppr tv <+> dcolon <+> ppr_ty_nested ki)
   where
     maybe_parens | use_parens = parens
                  | otherwise  = id
@@ -933,9 +933,13 @@ instance Binary IfaceOneShot where
 instance Outputable IfaceType where
   ppr ty = pprIfaceType ty
 
-pprIfaceType, pprParendIfaceType :: IfaceType -> SDoc
+-- The purpose of 'ppr_ty_nested' is to distinguish calls that should not
+-- trigger 'hideNonStandardTypes', see Note [Defaulting RuntimeRep variables]
+-- wrinkle (W2).
+pprIfaceType, pprParendIfaceType, ppr_ty_nested :: IfaceType -> SDoc
 pprIfaceType       = pprPrecIfaceType topPrec
 pprParendIfaceType = pprPrecIfaceType appPrec
+ppr_ty_nested = ppr_ty topPrec
 
 pprPrecIfaceType :: PprPrec -> IfaceType -> SDoc
 -- We still need `hideNonStandardTypes`, since the `pprPrecIfaceType` may be
@@ -987,7 +991,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_nested other_ty]
 
 ppr_ty ctxt_prec (IfaceAppTy t ts)
   = if_print_coercions
@@ -1044,9 +1048,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 +1079,32 @@ 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 (r1 :: RuntimeRep) . (∀ (r2 :: RuntimeRep) . p r2) -> p r1
+     We want to default 'r1', but not 'r2'.
+     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 'r2'.
+
+(W2) 'defaultIfaceTyVarsOfKind' ought to be called only once when printing a
+     type.
+     A few components of the printing machinery used to invoke 'ppr' on types
+     nested in secondary structures like IfaceBndr, which would repeat the
+     defaulting process, but treating the type as if it were top-level, causing
+     unwanted defaulting.
+     In order to prevent future developers from using 'ppr' again or being
+     confused that @ppr_ty topPrec@ is used, we introduced a marker function,
+     'ppr_ty_nested'.
 -}
 
 -- | Default 'RuntimeRep' variables to 'LiftedRep',
@@ -1097,28 +1129,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?
        -> IfaceType
        -> IfaceType
-    go subs (IfaceForAllTy (Bndr (IfaceTvBndr (var, var_kind)) argf) ty)
+    go subs True (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
       = 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' True ty
 
-    go subs (IfaceForAllTy bndr ty)
-      = IfaceForAllTy (go_ifacebndr subs bndr) (go subs ty)
+    go subs rank1 (IfaceForAllTy bndr ty)
+      = IfaceForAllTy (go_ifacebndr subs 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,34 +1171,34 @@ defaultIfaceTyVarsOfKind def_rep def_mult ty = go emptyFsEnv ty
       | otherwise
       = ty
 
-    go subs (IfaceTyConApp tc tc_args)
+    go subs _ (IfaceTyConApp tc tc_args)
       = IfaceTyConApp tc (go_args subs tc_args)
 
-    go subs (IfaceTupleTy sort is_prom tc_args)
+    go subs _ (IfaceTupleTy sort is_prom tc_args)
       = IfaceTupleTy sort is_prom (go_args subs 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 False w) (go subs False arg) (go subs rank1 res)
 
-    go subs (IfaceAppTy t ts)
-      = IfaceAppTy (go subs t) (go_args subs ts)
+    go subs _ (IfaceAppTy t ts)
+      = IfaceAppTy (go subs False t) (go_args subs 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
+      = Bndr (IfaceIdBndr (w, n, go subs False t)) argf
     go_ifacebndr subs (Bndr (IfaceTvBndr (n, t)) argf)
-      = Bndr (IfaceTvBndr (n, go subs t)) argf
+      = Bndr (IfaceTvBndr (n, go subs False 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)
+      = IA_Arg (go subs False ty) argf (go_args subs args)
 
     check_substitution :: IfaceType -> Maybe IfaceType
     check_substitution (IfaceTyConApp tc _)
@@ -1236,7 +1269,7 @@ ppr_app_arg ctx_prec (t, argf) =
        Specified |  print_kinds
                  -> char '@' <> ppr_ty appPrec t
        Inferred  |  print_kinds
-                 -> char '@' <> braces (ppr_ty topPrec t)
+                 -> char '@' <> braces (ppr_ty_nested t)
        _         -> empty
 
 -------------------
@@ -1367,7 +1400,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_nested 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,52 @@
+:set -XLinearTypes -XImpredicativeTypes
+import GHC.Types (RuntimeRep (..), Levity (..), TYPE, Multiplicity, Type, LiftedRep)
+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
+class C a where l :: forall (r :: RuntimeRep) (b :: TYPE r). a -> b
+m :: (forall (m :: Multiplicity). Int %m -> Int) -> Int; m x = x 5
+n :: forall (m :: Multiplicity). Int %m -> Int; n a = a
+o :: Maybe (forall (r :: RuntimeRep). Proxy r); o = Nothing
+p :: (forall (r :: RuntimeRep). Proxy r, Int); p = undefined
+q :: p (forall (r :: RuntimeRep). Proxy r); q = undefined
+r :: forall (a :: (forall (r :: RuntimeRep). TYPE r)) (p :: (forall (r :: RuntimeRep). TYPE r) -> Type). p a; r = r
+
+:set -XNoLinearTypes
+
+:type f
+:type g
+:type g'
+:type h
+:type i
+:type j
+:type k
+:type l
+:type m
+:type n
+:type o
+:type p
+:type q
+:type r
+
+:set -fprint-explicit-runtime-reps
+:set -XLinearTypes
+:type f
+:type g
+:type g'
+:type h
+:type i
+:type j
+:type k
+:type l
+:type m
+:type n
+:type o
+:type p
+:type q
+:type r


=====================================
testsuite/tests/ghci/scripts/T16468.stdout
=====================================
@@ -0,0 +1,34 @@
+f :: (forall (r :: RuntimeRep). Int -> p r) -> p LiftedRep
+g :: Int -> p LiftedRep
+g' :: Int -> forall (p :: RuntimeRep -> *). p LiftedRep
+h :: Int -> *
+i :: Int -> *
+j :: Eq (p LiftedRep) => Int -> p LiftedRep
+k :: Eq (p LiftedRep) =>
+     (forall (r :: RuntimeRep). Eq (p r) => Int -> p r) -> p LiftedRep
+l :: C a => a -> b
+m :: (forall (m :: Multiplicity). Int %m -> Int) -> Int
+n :: Int -> Int
+o :: Maybe (forall (r :: RuntimeRep). Proxy r)
+p :: (Proxy LiftedRep, Int)
+q :: p (forall (r :: RuntimeRep). Proxy r)
+r :: forall (a :: forall (r :: RuntimeRep). TYPE r)
+            (p :: (forall (r :: RuntimeRep). TYPE r) -> *).
+     p a
+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 LiftedRep) => Int -> forall (r :: RuntimeRep). p r
+k :: Eq (p r') =>
+     (forall (r :: RuntimeRep). Eq (p r) => Int -> p r) -> p r'
+l :: forall a (r :: RuntimeRep) (b :: TYPE r). C a => a -> b
+m :: (forall (m :: Multiplicity). Int %m -> Int) -> Int
+n :: Int %m -> Int
+o :: Maybe (forall (r :: RuntimeRep). Proxy r)
+p :: (forall (r :: RuntimeRep). Proxy r, Int)
+q :: p (forall (r :: RuntimeRep). Proxy r)
+r :: forall (a :: forall (r :: RuntimeRep). TYPE r)
+            (p :: (forall (r :: RuntimeRep). TYPE r) -> *).
+     p a


=====================================
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/5305ee3f1147fce7d4846341e4d9f19d055cba00

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5305ee3f1147fce7d4846341e4d9f19d055cba00
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/20230626/1e712136/attachment-0001.html>


More information about the ghc-commits mailing list