diff options
Diffstat (limited to 'compiler/GHC/Core')
48 files changed, 1771 insertions, 543 deletions
diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs index e89709929b..6b28adf371 100644 --- a/compiler/GHC/Core/Coercion.hs +++ b/compiler/GHC/Core/Coercion.hs @@ -112,6 +112,8 @@ module GHC.Core.Coercion ( -- * Other promoteCoercion, buildCoercion, + multToCo, + simplifyArgsWorker, badCoercionHole, badCoercionHoleCo @@ -147,6 +149,7 @@ import GHC.Builtin.Types.Prim import GHC.Data.List.SetOps import GHC.Data.Maybe import GHC.Types.Unique.FM +import GHC.Core.Multiplicity import Control.Monad (foldM, zipWithM) import Data.Function ( on ) @@ -298,9 +301,9 @@ whose `RuntimeRep' arguments are intentionally marked inferred to avoid type application. Hence - FunCo r co1 co2 :: (s1->t1) ~r (s2->t2) + FunCo r mult co1 co2 :: (s1->t1) ~r (s2->t2) is short for - TyConAppCo (->) co_rep1 co_rep2 co1 co2 + TyConAppCo (->) mult co_rep1 co_rep2 co1 co2 where co_rep1, co_rep2 are the coercions on the representations. -} @@ -321,12 +324,12 @@ decomposeCo arity co rs decomposeFunCo :: HasDebugCallStack => Role -- Role of the input coercion -> Coercion -- Input coercion - -> (Coercion, Coercion) + -> (CoercionN, Coercion, Coercion) -- Expects co :: (s1 -> t1) ~ (s2 -> t2) -- Returns (co1 :: s1~s2, co2 :: t1~t2) --- See Note [Function coercions] for the "2" and "3" +-- See Note [Function coercions] for the "3" and "4" decomposeFunCo r co = ASSERT2( all_ok, ppr co ) - (mkNthCo r 2 co, mkNthCo r 3 co) + (mkNthCo Nominal 0 co, mkNthCo r 3 co, mkNthCo r 4 co) where Pair s1t1 s2t2 = coercionKind co all_ok = isFunTy s1t1 && isFunTy s2t2 @@ -401,7 +404,9 @@ decomposePiCos orig_co (Pair orig_k1 orig_k2) orig_args -- ty :: s2 -- need arg_co :: s2 ~ s1 -- res_co :: t1 ~ t2 - = let (sym_arg_co, res_co) = decomposeFunCo Nominal co + = let (_, sym_arg_co, res_co) = decomposeFunCo Nominal co + -- It should be fine to ignore the multiplicity bit of the coercion + -- for a Nominal coercion. arg_co = mkSymCo sym_arg_co in go (arg_co : acc_arg_cos) (subst1,t1) res_co (subst2,t2) tys @@ -430,10 +435,13 @@ splitTyConAppCo_maybe co ; let args = zipWith mkReflCo (tyConRolesX r tc) tys ; return (tc, args) } splitTyConAppCo_maybe (TyConAppCo _ tc cos) = Just (tc, cos) -splitTyConAppCo_maybe (FunCo _ arg res) = Just (funTyCon, cos) - where cos = [mkRuntimeRepCo arg, mkRuntimeRepCo res, arg, res] +splitTyConAppCo_maybe (FunCo _ w arg res) = Just (funTyCon, cos) + where cos = [w, mkRuntimeRepCo arg, mkRuntimeRepCo res, arg, res] splitTyConAppCo_maybe _ = Nothing +multToCo :: Mult -> Coercion +multToCo r = mkNomReflCo r + -- first result has role equal to input; third result is Nominal splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion) -- ^ Attempt to take a coercion application apart. @@ -457,8 +465,9 @@ splitAppCo_maybe co = Just (mkReflCo r ty1, mkNomReflCo ty2) splitAppCo_maybe _ = Nothing +-- Only used in specialise/Rules splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion) -splitFunCo_maybe (FunCo _ arg res) = Just (arg, res) +splitFunCo_maybe (FunCo _ _ arg res) = Just (arg, res) splitFunCo_maybe _ = Nothing splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, Coercion, Coercion) @@ -682,12 +691,12 @@ mkNomReflCo = Refl -- caller's responsibility to get the roles correct on argument coercions. mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion mkTyConAppCo r tc cos - | tc `hasKey` funTyConKey - , [_rep1, _rep2, co1, co2] <- cos -- See Note [Function coercions] + | [w, _rep1, _rep2, co1, co2] <- cos -- See Note [Function coercions] + , isFunTyCon tc = -- (a :: TYPE ra) -> (b :: TYPE rb) ~ (c :: TYPE rc) -> (d :: TYPE rd) -- rep1 :: ra ~ rc rep2 :: rb ~ rd -- co1 :: a ~ c co2 :: b ~ d - mkFunCo r co1 co2 + mkFunCo r w co1 co2 -- Expand type synonyms | Just (tv_co_prs, rhs_ty, leftover_cos) <- expandSynTyCon_maybe tc cos @@ -701,13 +710,14 @@ mkTyConAppCo r tc cos -- | Build a function 'Coercion' from two other 'Coercion's. That is, -- given @co1 :: a ~ b@ and @co2 :: x ~ y@ produce @co :: (a -> x) ~ (b -> y)@. -mkFunCo :: Role -> Coercion -> Coercion -> Coercion -mkFunCo r co1 co2 +mkFunCo :: Role -> CoercionN -> Coercion -> Coercion -> Coercion +mkFunCo r w co1 co2 -- See Note [Refl invariant] | Just (ty1, _) <- isReflCo_maybe co1 , Just (ty2, _) <- isReflCo_maybe co2 - = mkReflCo r (mkVisFunTy ty1 ty2) - | otherwise = FunCo r co1 co2 + , Just (w, _) <- isReflCo_maybe w + = mkReflCo r (mkVisFunTy w ty1 ty2) + | otherwise = FunCo r w co1 co2 -- | Apply a 'Coercion' to another 'Coercion'. -- The second coercion must be Nominal, unless the first is Phantom. @@ -810,7 +820,8 @@ mkForAllCo_NoRefl v kind_co co , ASSERT( not (isReflCo co)) True , isCoVar v , not (v `elemVarSet` tyCoVarsOfCo co) - = FunCo (coercionRole co) kind_co co + = FunCo (coercionRole co) (multToCo Many) kind_co co + -- Functions from coercions are always unrestricted | otherwise = ForAllCo v kind_co co @@ -1024,21 +1035,22 @@ mkNthCo r n co -- If co :: (forall a1:t1 ~ t2. t1) ~ (forall a2:t3 ~ t4. t2) -- then (nth 0 co :: (t1 ~ t2) ~N (t3 ~ t4)) - go r n co@(FunCo r0 arg res) + go r n co@(FunCo r0 w arg res) -- See Note [Function coercions] - -- If FunCo _ arg_co res_co :: (s1:TYPE sk1 -> s2:TYPE sk2) - -- ~ (t1:TYPE tk1 -> t2:TYPE tk2) + -- If FunCo _ mult arg_co res_co :: (s1:TYPE sk1 :mult-> s2:TYPE sk2) + -- ~ (t1:TYPE tk1 :mult-> t2:TYPE tk2) -- Then we want to behave as if co was - -- TyConAppCo argk_co resk_co arg_co res_co + -- TyConAppCo mult argk_co resk_co arg_co res_co -- where -- argk_co :: sk1 ~ tk1 = mkNthCo 0 (mkKindCo arg_co) -- resk_co :: sk2 ~ tk2 = mkNthCo 0 (mkKindCo res_co) -- i.e. mkRuntimeRepCo = case n of - 0 -> ASSERT( r == Nominal ) mkRuntimeRepCo arg - 1 -> ASSERT( r == Nominal ) mkRuntimeRepCo res - 2 -> ASSERT( r == r0 ) arg - 3 -> ASSERT( r == r0 ) res + 0 -> ASSERT( r == Nominal ) w + 1 -> ASSERT( r == Nominal ) mkRuntimeRepCo arg + 2 -> ASSERT( r == Nominal ) mkRuntimeRepCo res + 3 -> ASSERT( r == r0 ) arg + 4 -> ASSERT( r == r0 ) res _ -> pprPanic "mkNthCo(FunCo)" (ppr n $$ ppr co) go r n (TyConAppCo r0 tc arg_cos) = ASSERT2( r == nthRole r0 tc n @@ -1186,8 +1198,8 @@ mkSubCo (Refl ty) = GRefl Representational ty MRefl mkSubCo (GRefl Nominal ty co) = GRefl Representational ty co mkSubCo (TyConAppCo Nominal tc cos) = TyConAppCo Representational tc (applyRoles tc cos) -mkSubCo (FunCo Nominal arg res) - = FunCo Representational +mkSubCo (FunCo Nominal w arg res) + = FunCo Representational w (downgradeRole Representational Nominal arg) (downgradeRole Representational Nominal res) mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) ) @@ -1259,10 +1271,10 @@ setNominalRole_maybe r co setNominalRole_maybe_helper (TyConAppCo Representational tc cos) = do { cos' <- zipWithM setNominalRole_maybe (tyConRolesX Representational tc) cos ; return $ TyConAppCo Nominal tc cos' } - setNominalRole_maybe_helper (FunCo Representational co1 co2) + setNominalRole_maybe_helper (FunCo Representational w co1 co2) = do { co1' <- setNominalRole_maybe Representational co1 ; co2' <- setNominalRole_maybe Representational co2 - ; return $ FunCo Nominal co1' co2' + ; return $ FunCo Nominal w co1' co2' } setNominalRole_maybe_helper (SymCo co) = SymCo <$> setNominalRole_maybe_helper co @@ -1376,7 +1388,7 @@ promoteCoercion co = case co of mkNomReflCo liftedTypeKind -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep - FunCo _ _ _ + FunCo _ _ _ _ -> ASSERT( False ) mkNomReflCo liftedTypeKind @@ -1508,8 +1520,8 @@ mkPiCo r v co | isTyVar v = mkHomoForAllCos [v] co -- want it to be r. It is only called in 'mkPiCos', which is -- only used in GHC.Core.Opt.Simplify.Utils, where we are sure for -- now (Aug 2018) v won't occur in co. - mkFunCo r (mkReflCo r (varType v)) co - | otherwise = mkFunCo r (mkReflCo r (varType v)) co + mkFunCo r (multToCo (varMult v)) (mkReflCo r (varType v)) co + | otherwise = mkFunCo r (multToCo (varMult v)) (mkReflCo r (varType v)) co -- mkCoCast (c :: s1 ~?r t1) (g :: (s1 ~?r t1) ~#R (s2 ~?r t2)) :: s2 ~?r t2 -- The first coercion might be lifted or unlifted; thus the ~? above @@ -1888,7 +1900,7 @@ ty_co_subst lc role ty liftCoSubstTyVar lc r tv go r (AppTy ty1 ty2) = mkAppCo (go r ty1) (go Nominal ty2) go r (TyConApp tc tys) = mkTyConAppCo r tc (zipWith go (tyConRolesX r tc) tys) - go r (FunTy _ ty1 ty2) = mkFunCo r (go r ty1) (go r ty2) + go r (FunTy _ w ty1 ty2) = mkFunCo r (go Nominal w) (go r ty1) (go r ty2) go r t@(ForAllTy (Bndr v _) ty) = let (lc', v', h) = liftCoSubstVarBndr lc v body_co = ty_co_subst lc' r ty in @@ -2125,7 +2137,7 @@ seqCo (TyConAppCo r tc cos) = r `seq` tc `seq` seqCos cos seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2 seqCo (ForAllCo tv k co) = seqType (varType tv) `seq` seqCo k `seq` seqCo co -seqCo (FunCo r co1 co2) = r `seq` seqCo co1 `seq` seqCo co2 +seqCo (FunCo r w co1 co2) = r `seq` seqCo w `seq` seqCo co1 `seq` seqCo co2 seqCo (CoVarCo cv) = cv `seq` () seqCo (HoleCo h) = coHoleCoVar h `seq` () seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos @@ -2188,7 +2200,7 @@ coercionLKind co go (TyConAppCo _ tc cos) = mkTyConApp tc (map go cos) go (AppCo co1 co2) = mkAppTy (go co1) (go co2) go (ForAllCo tv1 _ co1) = mkTyCoInvForAllTy tv1 (go co1) - go (FunCo _ co1 co2) = mkFunctionType (go co1) (go co2) + go (FunCo _ w co1 co2) = mkFunctionType (go w) (go co1) (go co2) go (CoVarCo cv) = coVarLType cv go (HoleCo h) = coVarLType (coHoleCoVar h) go (UnivCo _ _ ty1 _) = ty1 @@ -2245,7 +2257,7 @@ coercionRKind co go (AppCo co1 co2) = mkAppTy (go co1) (go co2) go (CoVarCo cv) = coVarRType cv go (HoleCo h) = coVarRType (coHoleCoVar h) - go (FunCo _ co1 co2) = mkFunctionType (go co1) (go co2) + go (FunCo _ w co1 co2) = mkFunctionType (go w) (go co1) (go co2) go (UnivCo _ _ _ ty2) = ty2 go (SymCo co) = coercionLKind co go (TransCo _ co2) = go co2 @@ -2348,7 +2360,7 @@ coercionRole = go go (TyConAppCo r _ _) = r go (AppCo co1 _) = go co1 go (ForAllCo _ _ co) = go co - go (FunCo r _ _) = r + go (FunCo r _ _ _) = r go (CoVarCo cv) = coVarRole cv go (HoleCo h) = coVarRole (coHoleCoVar h) go (AxiomInstCo ax _ _) = coAxiomRole ax @@ -2454,9 +2466,9 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2 ; _ -> False } ) mkNomReflCo ty1 - go (FunTy { ft_arg = arg1, ft_res = res1 }) - (FunTy { ft_arg = arg2, ft_res = res2 }) - = mkFunCo Nominal (go arg1 arg2) (go res1 res2) + go (FunTy { ft_mult = w1, ft_arg = arg1, ft_res = res1 }) + (FunTy { ft_mult = w2, ft_arg = arg2, ft_res = res2 }) + = mkFunCo Nominal (go w1 w2) (go arg1 arg2) (go res1 res2) go (TyConApp tc1 args1) (TyConApp tc2 args2) = ASSERT( tc1 == tc2 ) diff --git a/compiler/GHC/Core/Coercion.hs-boot b/compiler/GHC/Core/Coercion.hs-boot index eaf0180bef..7a92a84eb6 100644 --- a/compiler/GHC/Core/Coercion.hs-boot +++ b/compiler/GHC/Core/Coercion.hs-boot @@ -17,7 +17,7 @@ mkReflCo :: Role -> Type -> Coercion mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion mkAppCo :: Coercion -> Coercion -> Coercion mkForAllCo :: TyCoVar -> Coercion -> Coercion -> Coercion -mkFunCo :: Role -> Coercion -> Coercion -> Coercion +mkFunCo :: Role -> CoercionN -> Coercion -> Coercion -> Coercion mkCoVarCo :: CoVar -> Coercion mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion mkPhantomCo :: Coercion -> Type -> Type -> Coercion diff --git a/compiler/GHC/Core/Coercion/Axiom.hs b/compiler/GHC/Core/Coercion/Axiom.hs index 6a8ac41650..4ecbb6cc3d 100644 --- a/compiler/GHC/Core/Coercion/Axiom.hs +++ b/compiler/GHC/Core/Coercion/Axiom.hs @@ -26,7 +26,7 @@ module GHC.Core.Coercion.Axiom ( Role(..), fsFromRole, CoAxiomRule(..), TypeEqn, - BuiltInSynFamily(..) + BuiltInSynFamily(..), trivialBuiltInFamily ) where import GHC.Prelude @@ -579,3 +579,11 @@ data BuiltInSynFamily = BuiltInSynFamily , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn] } + +-- Provides default implementations that do nothing. +trivialBuiltInFamily :: BuiltInSynFamily +trivialBuiltInFamily = BuiltInSynFamily + { sfMatchFam = \_ -> Nothing + , sfInteractTop = \_ _ -> [] + , sfInteractInert = \_ _ _ _ -> [] + } diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs index 18cb98767f..bb99f93ac6 100644 --- a/compiler/GHC/Core/Coercion/Opt.hs +++ b/compiler/GHC/Core/Coercion/Opt.hs @@ -251,14 +251,15 @@ opt_co4 env sym rep r (ForAllCo tv k_co co) opt_co4_wrap env' sym rep r co -- Use the "mk" functions to check for nested Refls -opt_co4 env sym rep r (FunCo _r co1 co2) +opt_co4 env sym rep r (FunCo _r cow co1 co2) = ASSERT( r == _r ) if rep - then mkFunCo Representational co1' co2' - else mkFunCo r co1' co2' + then mkFunCo Representational cow' co1' co2' + else mkFunCo r cow' co1' co2' where co1' = opt_co4_wrap env sym rep r co1 co2' = opt_co4_wrap env sym rep r co2 + cow' = opt_co1 env sym cow opt_co4 env sym rep r (CoVarCo cv) | Just co <- lookupCoVar (lcTCvSubst env) cv @@ -648,10 +649,10 @@ opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2 fireTransRule "PushTyConApp" in_co1 in_co2 $ mkTyConAppCo r1 tc1 (opt_transList is cos1 cos2) -opt_trans_rule is in_co1@(FunCo r1 co1a co1b) in_co2@(FunCo r2 co2a co2b) - = ASSERT( r1 == r2 ) -- Just like the TyConAppCo/TyConAppCo case +opt_trans_rule is in_co1@(FunCo r1 w1 co1a co1b) in_co2@(FunCo r2 w2 co2a co2b) + = ASSERT( r1 == r2) -- Just like the TyConAppCo/TyConAppCo case fireTransRule "PushFun" in_co1 in_co2 $ - mkFunCo r1 (opt_trans is co1a co2a) (opt_trans is co1b co2b) + mkFunCo r1 (opt_trans is w1 w2) (opt_trans is co1a co2a) (opt_trans is co1b co2b) opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b) -- Must call opt_trans_rule_app; see Note [EtaAppCo] diff --git a/compiler/GHC/Core/ConLike.hs b/compiler/GHC/Core/ConLike.hs index c7f8f494eb..efe29f608f 100644 --- a/compiler/GHC/Core/ConLike.hs +++ b/compiler/GHC/Core/ConLike.hs @@ -39,6 +39,7 @@ import GHC.Types.Basic import GHC.Core.TyCo.Rep (Type, ThetaType) import GHC.Types.Var import GHC.Core.Type(mkTyConApp) +import GHC.Core.Multiplicity import qualified Data.Data as Data @@ -108,11 +109,11 @@ conLikeFieldLabels (PatSynCon pat_syn) = patSynFieldLabels pat_syn -- | Returns just the instantiated /value/ argument types of a 'ConLike', -- (excluding dictionary args) -conLikeInstOrigArgTys :: ConLike -> [Type] -> [Type] +conLikeInstOrigArgTys :: ConLike -> [Type] -> [Scaled Type] conLikeInstOrigArgTys (RealDataCon data_con) tys = dataConInstOrigArgTys data_con tys conLikeInstOrigArgTys (PatSynCon pat_syn) tys = - patSynInstArgTys pat_syn tys + map unrestricted $ patSynInstArgTys pat_syn tys -- | 'TyVarBinder's for the type variables of the 'ConLike'. For pattern -- synonyms, this will always consist of the universally quantified variables @@ -181,7 +182,7 @@ conLikeFullSig :: ConLike -> ([TyVar], [TyCoVar], [EqSpec] -- Why tyvars for universal but tycovars for existential? -- See Note [Existential coercion variables] in GHC.Core.DataCon - , ThetaType, ThetaType, [Type], Type) + , ThetaType, ThetaType, [Scaled Type], Type) conLikeFullSig (RealDataCon con) = let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, res_ty) = dataConFullSig con -- Required theta is empty as normal data cons require no additional diff --git a/compiler/GHC/Core/DataCon.hs b/compiler/GHC/Core/DataCon.hs index ca486863a5..e6f3d39690 100644 --- a/compiler/GHC/Core/DataCon.hs +++ b/compiler/GHC/Core/DataCon.hs @@ -30,11 +30,14 @@ module GHC.Core.DataCon ( dataConRepType, dataConInstSig, dataConFullSig, dataConName, dataConIdentity, dataConTag, dataConTagZ, dataConTyCon, dataConOrigTyCon, - dataConUserType, + dataConWrapperType, + dataConNonlinearType, + dataConDisplayType, dataConUnivTyVars, dataConExTyCoVars, dataConUnivAndExTyCoVars, dataConUserTyVars, dataConUserTyVarBinders, dataConEqSpec, dataConTheta, dataConStupidTheta, + dataConOtherTheta, dataConInstArgTys, dataConOrigArgTys, dataConOrigResTy, dataConInstOrigArgTys, dataConRepArgTys, dataConFieldLabels, dataConFieldType, dataConFieldType_maybe, @@ -68,6 +71,7 @@ import GHC.Core.Type as Type import GHC.Core.Coercion import GHC.Core.Unify import GHC.Core.TyCon +import GHC.Core.Multiplicity import GHC.Types.FieldLabel import GHC.Core.Class import GHC.Types.Name @@ -83,6 +87,9 @@ import GHC.Utils.Binary import GHC.Types.Unique.Set import GHC.Types.Unique( mkAlphaTyVarUnique ) +import GHC.Driver.Session +import GHC.LanguageExtensions as LangExt + import Data.ByteString (ByteString) import qualified Data.ByteString.Builder as BSB import qualified Data.ByteString.Lazy as LBS @@ -188,7 +195,7 @@ Note [Data constructor workers and wrappers] * Neither_ the worker _nor_ the wrapper take the dcStupidTheta dicts as arguments -* The wrapper (if it exists) takes dcOrigArgTys as its arguments +* The wrapper (if it exists) takes dcOrigArgTys as its arguments. The worker takes dataConRepArgTys as its arguments If the worker is absent, dataConRepArgTys is the same as dcOrigArgTys @@ -412,7 +419,7 @@ data DataCon -- the wrapper Id, because that makes it harder to use the wrap-id -- to rebuild values after record selection or in generics. - dcOrigArgTys :: [Type], -- Original argument types + dcOrigArgTys :: [Scaled Type], -- Original argument types -- (before unboxing and flattening of strict fields) dcOrigResTy :: Type, -- Original result type, as seen by the user -- NB: for a data instance, the original user result type may @@ -595,7 +602,7 @@ sometimes refer to this as "the dcUserTyVarBinders invariant". dcUserTyVarBinders, as the name suggests, is the one that users will see most of the time. It's used when computing the type signature of a data constructor (see -dataConUserType), and as a result, it's what matters from a TypeApplications +dataConWrapperType), and as a result, it's what matters from a TypeApplications perspective. Note [The dcEqSpec domain invariant] @@ -640,9 +647,9 @@ data DataConRep , dcr_boxer :: DataConBoxer - , dcr_arg_tys :: [Type] -- Final, representation argument types, - -- after unboxing and flattening, - -- and *including* all evidence args + , dcr_arg_tys :: [Scaled Type] -- Final, representation argument types, + -- after unboxing and flattening, + -- and *including* all evidence args , dcr_stricts :: [StrictnessMark] -- 1-1 with dcr_arg_tys -- See also Note [Data-con worker strictness] @@ -944,7 +951,7 @@ mkDataCon :: Name -- See @Note [TyVarBinders in DataCons]@ -> [EqSpec] -- ^ GADT equalities -> KnotTied ThetaType -- ^ Theta-type occurring before the arguments proper - -> [KnotTied Type] -- ^ Original argument types + -> [KnotTied (Scaled Type)] -- ^ Original argument types -> KnotTied Type -- ^ Original result type -> RuntimeRepInfo -- ^ See comments on 'TyCon.RuntimeRepInfo' -> KnotTied TyCon -- ^ Representation type constructor @@ -1002,8 +1009,8 @@ mkDataCon name declared_infix prom_info rep_ty = case rep of -- If the DataCon has no wrapper, then the worker's type *is* the - -- user-facing type, so we can simply use dataConUserType. - NoDataConRep -> dataConUserType con + -- user-facing type, so we can simply use dataConWrapperType. + NoDataConRep -> dataConWrapperType con -- If the DataCon has a wrapper, then the worker's type is never seen -- by the user. The visibilities we pick do not matter here. DCR{} -> mkInfForAllTys univ_tvs $ mkTyCoInvForAllTys ex_tvs $ @@ -1021,7 +1028,7 @@ mkDataCon name declared_infix prom_info prom_theta_bndrs = [ mkAnonTyConBinder InvisArg (mkTyVar n t) {- Invisible -} | (n,t) <- fresh_names `zip` theta ] prom_arg_bndrs = [ mkAnonTyConBinder VisArg (mkTyVar n t) - {- Visible -} | (n,t) <- dropList theta fresh_names `zip` orig_arg_tys ] + {- Visible -} | (n,t) <- dropList theta fresh_names `zip` map scaledThing orig_arg_tys ] prom_bndrs = prom_tv_bndrs ++ prom_theta_bndrs ++ prom_arg_bndrs prom_res_kind = orig_res_ty promoted = mkPromotedDataCon con name prom_info prom_bndrs @@ -1029,7 +1036,7 @@ mkDataCon name declared_infix prom_info roles = map (\tv -> if isTyVar tv then Nominal else Phantom) (univ_tvs ++ ex_tvs) - ++ map (const Representational) (theta ++ orig_arg_tys) + ++ map (const Representational) (theta ++ map scaledThing orig_arg_tys) freshNames :: [Name] -> [Name] -- Make an infinite list of Names whose Uniques and OccNames @@ -1206,7 +1213,7 @@ dataConFieldType con label = case dataConFieldType_maybe con label of dataConFieldType_maybe :: DataCon -> FieldLabelString -> Maybe (FieldLabel, Type) dataConFieldType_maybe con label - = find ((== label) . flLabel . fst) (dcFields con `zip` dcOrigArgTys con) + = find ((== label) . flLabel . fst) (dcFields con `zip` (scaledThing <$> dcOrigArgTys con)) -- | Strictness/unpack annotations, from user; or, for imported -- DataCons, from the interface file @@ -1270,7 +1277,7 @@ dataConInstSig con@(MkData { dcUnivTyVars = univ_tvs, dcExTyCoVars = ex_tvs univ_tys = ( ex_tvs' , substTheta subst (dataConTheta con) - , substTys subst arg_tys) + , substTys subst (map scaledThing arg_tys)) where univ_subst = zipTvSubst univ_tvs univ_tys (subst, ex_tvs') = Type.substVarBndrs univ_subst ex_tvs @@ -1290,11 +1297,12 @@ dataConInstSig con@(MkData { dcUnivTyVars = univ_tvs, dcExTyCoVars = ex_tvs -- equalities -- -- 5) The original argument types to the 'DataCon' (i.e. before --- any change of the representation of the type) +-- any change of the representation of the type) with linearity +-- annotations -- -- 6) The original result type of the 'DataCon' dataConFullSig :: DataCon - -> ([TyVar], [TyCoVar], [EqSpec], ThetaType, [Type], Type) + -> ([TyVar], [TyCoVar], [EqSpec], ThetaType, [Scaled Type], Type) dataConFullSig (MkData {dcUnivTyVars = univ_tvs, dcExTyCoVars = ex_tvs, dcEqSpec = eq_spec, dcOtherTheta = theta, dcOrigArgTys = arg_tys, dcOrigResTy = res_ty}) @@ -1309,7 +1317,41 @@ dataConOrigResTy dc = dcOrigResTy dc dataConStupidTheta :: DataCon -> ThetaType dataConStupidTheta dc = dcStupidTheta dc -dataConUserType :: DataCon -> Type +{- +Note [Displaying linear fields] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A constructor with a linear field can be written either as +MkT :: a #-> T a (with -XLinearTypes) +or +MkT :: a -> T a (with -XNoLinearTypes) + +There are two different methods to retrieve a type of a datacon. +They differ in how linear fields are handled. + +1. dataConWrapperType: +The type of the wrapper in Core. +For example, dataConWrapperType for Maybe is a #-> Just a. + +2. dataConNonlinearType: +The type of the constructor, with linear arrows replaced by unrestricted ones. +Used when we don't want to introduce linear types to user (in holes +and in types in hie used by haddock). + +3. dataConDisplayType (depends on DynFlags): +The type we'd like to show in error messages, :info and -ddump-types. +Ideally, it should reflect the type written by the user; +the function returns a type with arrows that would be required +to write this constructor under the current setting of -XLinearTypes. +In principle, this type can be different from the user's source code +when the value of -XLinearTypes has changed, but we don't +expect this to cause much trouble. + +Due to internal plumbing in checkValidDataCon, we can't just return a Doc. +The multiplicity of arrows returned by dataConDisplayType and +dataConDisplayType is used only for pretty-printing. +-} + +dataConWrapperType :: DataCon -> Type -- ^ The user-declared type of the data constructor -- in the nice-to-read form: -- @@ -1324,14 +1366,30 @@ dataConUserType :: DataCon -> Type -- -- NB: If the constructor is part of a data instance, the result type -- mentions the family tycon, not the internal one. -dataConUserType (MkData { dcUserTyVarBinders = user_tvbs, - dcOtherTheta = theta, dcOrigArgTys = arg_tys, - dcOrigResTy = res_ty }) +dataConWrapperType (MkData { dcUserTyVarBinders = user_tvbs, + dcOtherTheta = theta, dcOrigArgTys = arg_tys, + dcOrigResTy = res_ty }) = mkInvisForAllTys user_tvbs $ - mkInvisFunTys theta $ + mkInvisFunTysMany theta $ mkVisFunTys arg_tys $ res_ty +dataConNonlinearType :: DataCon -> Type +dataConNonlinearType (MkData { dcUserTyVarBinders = user_tvbs, + dcOtherTheta = theta, dcOrigArgTys = arg_tys, + dcOrigResTy = res_ty }) + = let arg_tys' = map (\(Scaled w t) -> Scaled (case w of One -> Many; _ -> w) t) arg_tys + in mkInvisForAllTys user_tvbs $ + mkInvisFunTysMany theta $ + mkVisFunTys arg_tys' $ + res_ty + +dataConDisplayType :: DynFlags -> DataCon -> Type +dataConDisplayType dflags dc + = if xopt LangExt.LinearTypes dflags + then dataConWrapperType dc + else dataConNonlinearType dc + -- | Finds the instantiated types of the arguments required to construct a -- 'DataCon' representation -- NB: these INCLUDE any dictionary args @@ -1341,13 +1399,13 @@ dataConInstArgTys :: DataCon -- ^ A datacon with no existentials or equality -- However, it can have a dcTheta (notably it can be a -- class dictionary, with superclasses) -> [Type] -- ^ Instantiated at these types - -> [Type] + -> [Scaled Type] dataConInstArgTys dc@(MkData {dcUnivTyVars = univ_tvs, dcExTyCoVars = ex_tvs}) inst_tys = ASSERT2( univ_tvs `equalLength` inst_tys , text "dataConInstArgTys" <+> ppr dc $$ ppr univ_tvs $$ ppr inst_tys) ASSERT2( null ex_tvs, ppr dc ) - map (substTyWith univ_tvs inst_tys) (dataConRepArgTys dc) + map (mapScaledType (substTyWith univ_tvs inst_tys)) (dataConRepArgTys dc) -- | Returns just the instantiated /value/ argument types of a 'DataCon', -- (excluding dictionary args) @@ -1355,7 +1413,7 @@ dataConInstOrigArgTys :: DataCon -- Works for any DataCon -> [Type] -- Includes existential tyvar args, but NOT -- equality constraints or dicts - -> [Type] + -> [Scaled Type] -- For vanilla datacons, it's all quite straightforward -- But for the call in GHC.HsToCore.Match.Constructor, we really do want just -- the value args @@ -1364,26 +1422,30 @@ dataConInstOrigArgTys dc@(MkData {dcOrigArgTys = arg_tys, dcExTyCoVars = ex_tvs}) inst_tys = ASSERT2( tyvars `equalLength` inst_tys , text "dataConInstOrigArgTys" <+> ppr dc $$ ppr tyvars $$ ppr inst_tys ) - map (substTy subst) arg_tys + substScaledTys subst arg_tys where tyvars = univ_tvs ++ ex_tvs subst = zipTCvSubst tyvars inst_tys -- | Returns the argument types of the wrapper, excluding all dictionary arguments -- and without substituting for any type variables -dataConOrigArgTys :: DataCon -> [Type] +dataConOrigArgTys :: DataCon -> [Scaled Type] dataConOrigArgTys dc = dcOrigArgTys dc +-- | Returns constraints in the wrapper type, other than those in the dataConEqSpec +dataConOtherTheta :: DataCon -> ThetaType +dataConOtherTheta dc = dcOtherTheta dc + -- | Returns the arg types of the worker, including *all* non-dependent -- evidence, after any flattening has been done and without substituting for -- any type variables -dataConRepArgTys :: DataCon -> [Type] +dataConRepArgTys :: DataCon -> [Scaled Type] dataConRepArgTys (MkData { dcRep = rep , dcEqSpec = eq_spec , dcOtherTheta = theta , dcOrigArgTys = orig_arg_tys }) = case rep of - NoDataConRep -> ASSERT( null eq_spec ) theta ++ orig_arg_tys + NoDataConRep -> ASSERT( null eq_spec ) (map unrestricted theta) ++ orig_arg_tys DCR { dcr_arg_tys = arg_tys } -> arg_tys -- | The string @package:module.name@ identifying a constructor, which is attached @@ -1502,7 +1564,7 @@ splitDataProductType_maybe -> Maybe (TyCon, -- The type constructor [Type], -- Type args of the tycon DataCon, -- The data constructor - [Type]) -- Its /representation/ arg types + [Scaled Type]) -- Its /representation/ arg types -- Rejecting existentials is conservative. Maybe some things -- could be made to work with them, but I'm not going to sweat diff --git a/compiler/GHC/Core/DataCon.hs-boot b/compiler/GHC/Core/DataCon.hs-boot index 6520abbbe7..70c8328da1 100644 --- a/compiler/GHC/Core/DataCon.hs-boot +++ b/compiler/GHC/Core/DataCon.hs-boot @@ -9,6 +9,7 @@ import GHC.Types.Unique ( Uniquable ) import GHC.Utils.Outputable ( Outputable, OutputableBndr ) import GHC.Types.Basic (Arity) import {-# SOURCE #-} GHC.Core.TyCo.Rep ( Type, ThetaType ) +import GHC.Core.Multiplicity (Scaled) data DataCon data DataConRep @@ -21,10 +22,10 @@ dataConUserTyVars :: DataCon -> [TyVar] dataConUserTyVarBinders :: DataCon -> [InvisTVBinder] dataConSourceArity :: DataCon -> Arity dataConFieldLabels :: DataCon -> [FieldLabel] -dataConInstOrigArgTys :: DataCon -> [Type] -> [Type] +dataConInstOrigArgTys :: DataCon -> [Type] -> [Scaled Type] dataConStupidTheta :: DataCon -> ThetaType dataConFullSig :: DataCon - -> ([TyVar], [TyCoVar], [EqSpec], ThetaType, [Type], Type) + -> ([TyVar], [TyCoVar], [EqSpec], ThetaType, [Scaled Type], Type) isUnboxedSumCon :: DataCon -> Bool instance Eq DataCon diff --git a/compiler/GHC/Core/FVs.hs b/compiler/GHC/Core/FVs.hs index b562ffc38b..5d65eec042 100644 --- a/compiler/GHC/Core/FVs.hs +++ b/compiler/GHC/Core/FVs.hs @@ -76,6 +76,8 @@ import GHC.Core.TyCo.FVs import GHC.Core.TyCon import GHC.Core.Coercion.Axiom import GHC.Core.FamInstEnv +import GHC.Core.Multiplicity +import GHC.Builtin.Types( unrestrictedFunTyConName ) import GHC.Builtin.Types.Prim( funTyConName ) import GHC.Data.Maybe( orElse ) import GHC.Utils.Misc @@ -350,11 +352,17 @@ orphNamesOfType ty | Just ty' <- coreView ty = orphNamesOfType ty' -- Look through type synonyms (#4912) orphNamesOfType (TyVarTy _) = emptyNameSet orphNamesOfType (LitTy {}) = emptyNameSet -orphNamesOfType (TyConApp tycon tys) = orphNamesOfTyCon tycon +orphNamesOfType (TyConApp tycon tys) = func + `unionNameSet` orphNamesOfTyCon tycon `unionNameSet` orphNamesOfTypes tys + where func = case tys of + arg:_ | tycon == funTyCon -> orph_names_of_fun_ty_con arg + _ -> emptyNameSet orphNamesOfType (ForAllTy bndr res) = orphNamesOfType (binderType bndr) `unionNameSet` orphNamesOfType res -orphNamesOfType (FunTy _ arg res) = unitNameSet funTyConName -- NB! See #8535 +orphNamesOfType (FunTy _ w arg res) = orph_names_of_fun_ty_con w + `unionNameSet` unitNameSet funTyConName + `unionNameSet` orphNamesOfType w `unionNameSet` orphNamesOfType arg `unionNameSet` orphNamesOfType res orphNamesOfType (AppTy fun arg) = orphNamesOfType fun `unionNameSet` orphNamesOfType arg @@ -378,7 +386,7 @@ orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` or orphNamesOfCo (AppCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2 orphNamesOfCo (ForAllCo _ kind_co co) = orphNamesOfCo kind_co `unionNameSet` orphNamesOfCo co -orphNamesOfCo (FunCo _ co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2 +orphNamesOfCo (FunCo _ co_mult co1 co2) = orphNamesOfCo co_mult `unionNameSet` orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2 orphNamesOfCo (CoVarCo _) = emptyNameSet orphNamesOfCo (AxiomInstCo con _ cos) = orphNamesOfCoCon con `unionNameSet` orphNamesOfCos cos orphNamesOfCo (UnivCo p _ t1 t2) = orphNamesOfProv p `unionNameSet` orphNamesOfType t1 `unionNameSet` orphNamesOfType t2 @@ -428,6 +436,12 @@ orphNamesOfCoAxBranch (CoAxBranch { cab_lhs = lhs, cab_rhs = rhs }) orphNamesOfFamInst :: FamInst -> NameSet orphNamesOfFamInst fam_inst = orphNamesOfAxiom (famInstAxiom fam_inst) +-- Detect FUN 'Many as an application of (->), so that :i (->) works as expected +-- (see #8535) Issue #16475 describes a more robust solution +orph_names_of_fun_ty_con :: Mult -> NameSet +orph_names_of_fun_ty_con Many = unitNameSet unrestrictedFunTyConName +orph_names_of_fun_ty_con _ = emptyNameSet + {- ************************************************************************ * * @@ -716,9 +730,10 @@ freeVars = go where go :: CoreExpr -> CoreExprWithFVs go (Var v) - | isLocalVar v = (aFreeVar v `unionFVs` ty_fvs, AnnVar v) + | isLocalVar v = (aFreeVar v `unionFVs` ty_fvs `unionFVs` mult_vars, AnnVar v) | otherwise = (emptyDVarSet, AnnVar v) where + mult_vars = tyCoVarsOfTypeDSet (varMult v) ty_fvs = dVarTypeTyCoVars v -- See Note [The FVAnn invariant] diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs index 9d2c5c2f79..81221c25ed 100644 --- a/compiler/GHC/Core/FamInstEnv.hs +++ b/compiler/GHC/Core/FamInstEnv.hs @@ -1413,14 +1413,14 @@ normalise_type ty go (TyConApp tc tys) = normalise_tc_app tc tys go ty@(LitTy {}) = do { r <- getRole ; return (mkReflCo r ty, ty) } - go (AppTy ty1 ty2) = go_app_tys ty1 [ty2] - go ty@(FunTy { ft_arg = ty1, ft_res = ty2 }) + go ty@(FunTy { ft_mult = w, ft_arg = ty1, ft_res = ty2 }) = do { (co1, nty1) <- go ty1 ; (co2, nty2) <- go ty2 + ; (wco, wty) <- go w ; r <- getRole - ; return (mkFunCo r co1 co2, ty { ft_arg = nty1, ft_res = nty2 }) } + ; return (mkFunCo r wco co1 co2, ty { ft_mult = wty, ft_arg = nty1, ft_res = nty2 }) } go (ForAllTy (Bndr tcvar vis) ty) = do { (lc', tv', h, ki') <- normalise_var_bndr tcvar ; (co, nty) <- withLC lc' $ normalise_type ty @@ -1749,10 +1749,11 @@ coreFlattenTy subst = go = let (env', tys') = coreFlattenTys subst env tys in (env', mkTyConApp tc tys') - go env ty@(FunTy { ft_arg = ty1, ft_res = ty2 }) + go env ty@(FunTy { ft_mult = mult, ft_arg = ty1, ft_res = ty2 }) = let (env1, ty1') = go env ty1 - (env2, ty2') = go env1 ty2 in - (env2, ty { ft_arg = ty1', ft_res = ty2' }) + (env2, ty2') = go env1 ty2 + (env3, mult') = go env2 mult in + (env3, ty { ft_mult = mult', ft_arg = ty1', ft_res = ty2' }) go env (ForAllTy (Bndr tv vis) ty) = let (env1, subst', tv') = coreFlattenVarBndr subst env tv @@ -1770,6 +1771,7 @@ coreFlattenTy subst = go = let (env', co') = coreFlattenCo subst env co in (env', CoercionTy co') + -- when flattening, we don't care about the contents of coercions. -- so, just return a fresh variable of the right (flattened) type coreFlattenCo :: TvSubstEnv -> FlattenEnv diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs index 314f9d0319..43c93595df 100644 --- a/compiler/GHC/Core/Lint.hs +++ b/compiler/GHC/Core/Lint.hs @@ -8,6 +8,7 @@ See Note [Core Lint guarantee]. -} {-# LANGUAGE CPP #-} +{-# LANGUAGE ViewPatterns #-} {-# LANGUAGE ScopedTypeVariables, DeriveFunctor #-} module GHC.Core.Lint ( @@ -34,12 +35,14 @@ import GHC.Data.Bag import GHC.Types.Literal import GHC.Core.DataCon import GHC.Builtin.Types.Prim +import GHC.Builtin.Types ( multiplicityTy ) import GHC.Tc.Utils.TcType ( isFloatingTy ) import GHC.Types.Var as Var import GHC.Types.Var.Env import GHC.Types.Var.Set import GHC.Types.Unique.Set( nonDetEltsUniqSet ) import GHC.Types.Name +import GHC.Types.Name.Env import GHC.Types.Id import GHC.Types.Id.Info import GHC.Core.Ppr @@ -47,6 +50,8 @@ import GHC.Utils.Error import GHC.Core.Coercion import GHC.Types.SrcLoc import GHC.Core.Type as Type +import GHC.Core.Multiplicity +import GHC.Core.UsageEnv import GHC.Types.RepType import GHC.Core.TyCo.Rep -- checks validity of types/coercions import GHC.Core.TyCo.Subst @@ -66,7 +71,7 @@ import GHC.Core.Coercion.Opt ( checkAxInstCo ) import GHC.Core.Opt.Arity ( typeArity ) import GHC.Types.Demand ( splitStrictSig, isDeadEndDiv ) -import GHC.Driver.Types +import GHC.Driver.Types hiding (Usage) import GHC.Driver.Session import Control.Monad import GHC.Utils.Monad @@ -471,7 +476,7 @@ lintCoreBindings dflags pass local_in_scope binds -- into use 'unexpectedly'; see Note [Glomming] in "GHC.Core.Opt.OccurAnal" binders = map fst all_pairs - flags = defaultLintFlags + flags = (defaultLintFlags dflags) { lf_check_global_ids = check_globals , lf_check_inline_loop_breakers = check_lbs , lf_check_static_ptrs = check_static_ptrs } @@ -541,7 +546,7 @@ lintUnfolding is_compulsory dflags locn var_set expr | otherwise = Just (pprMessageBag errs) where vars = nonDetEltsUniqSet var_set - (_warns, errs) = initL dflags defaultLintFlags vars $ + (_warns, errs) = initL dflags (defaultLintFlags dflags) vars $ if is_compulsory -- See Note [Checking for levity polymorphism] then noLPChecks linter @@ -558,7 +563,7 @@ lintExpr dflags vars expr | isEmptyBag errs = Nothing | otherwise = Just (pprMessageBag errs) where - (_warns, errs) = initL dflags defaultLintFlags vars linter + (_warns, errs) = initL dflags (defaultLintFlags dflags) vars linter linter = addLoc TopLevelBindings $ lintCoreExpr expr @@ -572,24 +577,29 @@ lintExpr dflags vars expr Check a core binding, returning the list of variables bound. -} +-- Returns a UsageEnv because this function is called in lintCoreExpr for +-- Let + lintRecBindings :: TopLevelFlag -> [(Id, CoreExpr)] - -> ([LintedId] -> LintM a) -> LintM a + -> ([LintedId] -> LintM a) -> LintM (a, [UsageEnv]) lintRecBindings top_lvl pairs thing_inside = lintIdBndrs top_lvl bndrs $ \ bndrs' -> - do { zipWithM_ lint_pair bndrs' rhss - ; thing_inside bndrs' } + do { ues <- zipWithM lint_pair bndrs' rhss + ; a <- thing_inside bndrs' + ; return (a, ues) } where (bndrs, rhss) = unzip pairs lint_pair bndr' rhs = addLoc (RhsOf bndr') $ - do { rhs_ty <- lintRhs bndr' rhs -- Check the rhs - ; lintLetBind top_lvl Recursive bndr' rhs rhs_ty } + do { (rhs_ty, ue) <- lintRhs bndr' rhs -- Check the rhs + ; lintLetBind top_lvl Recursive bndr' rhs rhs_ty + ; return ue } -lintLetBody :: [LintedId] -> CoreExpr -> LintM LintedType +lintLetBody :: [LintedId] -> CoreExpr -> LintM (LintedType, UsageEnv) lintLetBody bndrs body - = do { body_ty <- addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) + = do { (body_ty, body_ue) <- addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) ; mapM_ (lintJoinBndrType body_ty) bndrs - ; return body_ty } + ; return (body_ty, body_ue) } lintLetBind :: TopLevelFlag -> RecFlag -> LintedId -> CoreExpr -> LintedType -> LintM () @@ -668,7 +678,8 @@ lintLetBind top_lvl rec_flag binder rhs rhs_ty ; addLoc (RuleOf binder) $ mapM_ (lintCoreRule binder binder_ty) (idCoreRules binder) ; addLoc (UnfoldingOf binder) $ - lintIdUnfolding binder binder_ty (idUnfolding binder) } + lintIdUnfolding binder binder_ty (idUnfolding binder) + ; return () } -- We should check the unfolding, if any, but this is tricky because -- the unfolding is a SimplifiableCoreExpr. Give up for now. @@ -680,7 +691,7 @@ lintLetBind top_lvl rec_flag binder rhs rhs_ty -- join point. -- -- See Note [Checking StaticPtrs]. -lintRhs :: Id -> CoreExpr -> LintM LintedType +lintRhs :: Id -> CoreExpr -> LintM (LintedType, UsageEnv) -- NB: the Id can be Linted or not -- it's only used for -- its OccInfo and join-pointer-hood lintRhs bndr rhs @@ -695,6 +706,7 @@ lintRhs _bndr rhs = fmap lf_check_static_ptrs getLintFlags >>= go where -- Allow occurrences of 'makeStatic' at the top-level but produce errors -- otherwise. + go :: StaticPtrCheck -> LintM (OutType, UsageEnv) go AllowAtTopLevel | (binders0, rhs') <- collectTyBinders rhs , Just (fun, t, info, e) <- collectMakeStaticArgs rhs' @@ -703,15 +715,15 @@ lintRhs _bndr rhs = fmap lf_check_static_ptrs getLintFlags >>= go -- imitate @lintCoreExpr (Lam ...)@ lintLambda -- imitate @lintCoreExpr (App ...)@ - (do fun_ty <- lintCoreExpr fun - lintCoreArgs fun_ty [Type t, info, e] + (do fun_ty_ue <- lintCoreExpr fun + lintCoreArgs fun_ty_ue [Type t, info, e] ) binders0 go _ = markAllJoinsBad $ lintCoreExpr rhs -- | Lint the RHS of a join point with expected join arity of @n@ (see Note -- [Join points] in GHC.Core). -lintJoinLams :: JoinArity -> Maybe Id -> CoreExpr -> LintM LintedType +lintJoinLams :: JoinArity -> Maybe Id -> CoreExpr -> LintM (LintedType, UsageEnv) lintJoinLams join_arity enforce rhs = go join_arity rhs where @@ -729,10 +741,10 @@ lintIdUnfolding :: Id -> Type -> Unfolding -> LintM () lintIdUnfolding bndr bndr_ty uf | isStableUnfolding uf , Just rhs <- maybeUnfoldingTemplate uf - = do { ty <- if isCompulsoryUnfolding uf - then noLPChecks $ lintRhs bndr rhs - -- See Note [Checking for levity polymorphism] - else lintRhs bndr rhs + = do { ty <- fst <$> (if isCompulsoryUnfolding uf + then noLPChecks $ lintRhs bndr rhs + -- See Note [Checking for levity polymorphism] + else lintRhs bndr rhs) ; ensureEqTys bndr_ty ty (mkRhsMsg bndr (text "unfolding") ty) } lintIdUnfolding _ _ _ = return () -- Do not Lint unstable unfoldings, because that leads @@ -825,7 +837,7 @@ lintCastExpr expr expr_ty co ; ensureEqTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty) ; return to_ty } -lintCoreExpr :: CoreExpr -> LintM LintedType +lintCoreExpr :: CoreExpr -> LintM (LintedType, UsageEnv) -- The returned type has the substitution from the monad -- already applied to it: -- lintCoreExpr e subst = exprType (subst e) @@ -839,11 +851,12 @@ lintCoreExpr (Var var) = lintIdOcc var 0 lintCoreExpr (Lit lit) - = return (literalType lit) + = return (literalType lit, zeroUE) lintCoreExpr (Cast expr co) - = do expr_ty <- markAllJoinsBad $ lintCoreExpr expr - lintCastExpr expr expr_ty co + = do (expr_ty, ue) <- markAllJoinsBad $ lintCoreExpr expr + to_ty <- lintCastExpr expr expr_ty co + return (to_ty, ue) lintCoreExpr (Tick tickish expr) = do case tickish of @@ -875,12 +888,13 @@ lintCoreExpr (Let (NonRec tv (Type ty)) body) lintCoreExpr (Let (NonRec bndr rhs) body) | isId bndr = do { -- First Lint the RHS, before bringing the binder into scope - rhs_ty <- lintRhs bndr rhs + (rhs_ty, let_ue) <- lintRhs bndr rhs + -- See Note [Multiplicity of let binders] in Var -- Now lint the binder ; lintBinder LetBind bndr $ \bndr' -> do { lintLetBind NotTopLevel NonRecursive bndr' rhs rhs_ty - ; lintLetBody [bndr'] body } } + ; addAliasUE bndr let_ue (lintLetBody [bndr'] body) } } | otherwise = failWithL (mkLetErr bndr rhs) -- Not quite accurate @@ -897,8 +911,11 @@ lintCoreExpr e@(Let (Rec pairs) body) ; checkL (all isJoinId bndrs || all (not . isJoinId) bndrs) $ mkInconsistentRecMsg bndrs - ; lintRecBindings NotTopLevel pairs $ \ bndrs' -> - lintLetBody bndrs' body } + -- See Note [Multiplicity of let binders] in Var + ; ((body_type, body_ue), ues) <- + lintRecBindings NotTopLevel pairs $ \ bndrs' -> + lintLetBody bndrs' body + ; return (body_type, body_ue `addUE` scaleUE Many (foldr1 addUE ues)) } where bndrs = map fst pairs @@ -908,19 +925,20 @@ lintCoreExpr e@(App _ _) -- N.B. we may have an over-saturated application of the form: -- runRW (\s -> \x -> ...) y , arg_ty1 : arg_ty2 : arg3 : rest <- args - = do { fun_ty1 <- lintCoreArg (idType fun) arg_ty1 - ; fun_ty2 <- lintCoreArg fun_ty1 arg_ty2 + = do { fun_pair1 <- lintCoreArg (idType fun, zeroUE) arg_ty1 + ; (fun_ty2, ue2) <- lintCoreArg fun_pair1 arg_ty2 -- See Note [Linting of runRW#] - ; let lintRunRWCont :: CoreArg -> LintM LintedType + ; let lintRunRWCont :: CoreArg -> LintM (LintedType, UsageEnv) lintRunRWCont (Cast expr co) = do - ty <- lintRunRWCont expr - lintCastExpr expr ty co + (ty, ue) <- lintRunRWCont expr + new_ty <- lintCastExpr expr ty co + return (new_ty, ue) lintRunRWCont expr@(Lam _ _) = do lintJoinLams 1 (Just fun) expr lintRunRWCont other = markAllJoinsBad $ lintCoreExpr other -- TODO: Look through ticks? - ; arg3_ty <- lintRunRWCont arg3 - ; app_ty <- lintValApp arg3 fun_ty2 arg3_ty + ; (arg3_ty, ue3) <- lintRunRWCont arg3 + ; app_ty <- lintValApp arg3 fun_ty2 arg3_ty ue2 ue3 ; lintCoreArgs app_ty rest } | Var fun <- fun @@ -928,8 +946,8 @@ lintCoreExpr e@(App _ _) = failWithL (text "Invalid runRW# application") | otherwise - = do { fun_ty <- lintCoreFun fun (length args) - ; lintCoreArgs fun_ty args } + = do { pair <- lintCoreFun fun (length args) + ; lintCoreArgs pair args } where (fun, args) = collectArgs e @@ -948,11 +966,11 @@ lintCoreExpr (Type ty) lintCoreExpr (Coercion co) = do { co' <- addLoc (InCo co) $ lintCoercion co - ; return (coercionType co') } + ; return (coercionType co', zeroUE) } ---------------------- lintIdOcc :: Var -> Int -- Number of arguments (type or value) being passed - -> LintM LintedType -- returns type of the *variable* + -> LintM (LintedType, UsageEnv) -- returns type of the *variable* lintIdOcc var nargs = addLoc (OccOf var) $ do { checkL (isNonCoVarId var) @@ -986,11 +1004,13 @@ lintIdOcc var nargs ; checkDeadIdOcc var ; checkJoinOcc var nargs - ; return linted_bndr_ty } + ; usage <- varCallSiteUsage var + + ; return (linted_bndr_ty, usage) } lintCoreFun :: CoreExpr - -> Int -- Number of arguments (type or val) being passed - -> LintM LintedType -- Returns type of the *function* + -> Int -- Number of arguments (type or val) being passed + -> LintM (LintedType, UsageEnv) -- Returns type of the *function* lintCoreFun (Var var) nargs = lintIdOcc var nargs @@ -1005,12 +1025,13 @@ lintCoreFun expr nargs -- See Note [Join points are less general than the paper] lintCoreExpr expr ------------------ -lintLambda :: Var -> LintM Type -> LintM Type +lintLambda :: Var -> LintM (Type, UsageEnv) -> LintM (Type, UsageEnv) lintLambda var lintBody = addLoc (LambdaBodyOf var) $ lintBinder LambdaBind var $ \ var' -> - do { body_ty <- lintBody - ; return (mkLamType var' body_ty) } + do { (body_ty, ue) <- lintBody + ; ue' <- checkLinearity ue var' + ; return (mkLamType var' body_ty, ue') } ------------------ checkDeadIdOcc :: Id -> LintM () -- Occurrences of an Id should never be dead.... @@ -1068,6 +1089,19 @@ checkJoinOcc var n_args | otherwise = return () +-- Check that the usage of var is consistent with var itself, and pop the var +-- from the usage environment (this is important because of shadowing). +checkLinearity :: UsageEnv -> Var -> LintM UsageEnv +checkLinearity body_ue lam_var = + case varMultMaybe lam_var of + Just mult -> do ensureSubUsage lhs mult (err_msg mult) + return $ deleteUE body_ue lam_var + Nothing -> return body_ue -- A type variable + where + lhs = lookupUE body_ue lam_var + err_msg mult = text "Linearity failure in lambda:" <+> ppr lam_var + $$ ppr lhs <+> text "⊈" <+> ppr mult + {- Note [No alternatives lint check] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1150,19 +1184,20 @@ subtype of the required type, as one would expect. -} -lintCoreArgs :: LintedType -> [CoreArg] -> LintM LintedType -lintCoreArgs fun_ty args = foldM lintCoreArg fun_ty args +lintCoreArgs :: (LintedType, UsageEnv) -> [CoreArg] -> LintM (LintedType, UsageEnv) +lintCoreArgs (fun_ty, fun_ue) args = foldM lintCoreArg (fun_ty, fun_ue) args -lintCoreArg :: LintedType -> CoreArg -> LintM LintedType -lintCoreArg fun_ty (Type arg_ty) +lintCoreArg :: (LintedType, UsageEnv) -> CoreArg -> LintM (LintedType, UsageEnv) +lintCoreArg (fun_ty, ue) (Type arg_ty) = do { checkL (not (isCoercionTy arg_ty)) (text "Unnecessary coercion-to-type injection:" <+> ppr arg_ty) ; arg_ty' <- lintType arg_ty - ; lintTyApp fun_ty arg_ty' } + ; res <- lintTyApp fun_ty arg_ty' + ; return (res, ue) } -lintCoreArg fun_ty arg - = do { arg_ty <- markAllJoinsBad $ lintCoreExpr arg +lintCoreArg (fun_ty, fun_ue) arg + = do { (arg_ty, arg_ue) <- markAllJoinsBad $ lintCoreExpr arg -- See Note [Levity polymorphism invariants] in GHC.Core ; flags <- getLintFlags ; lintL (not (lf_check_levity_poly flags) || not (isTypeLevPoly arg_ty)) @@ -1173,24 +1208,53 @@ lintCoreArg fun_ty arg ; checkL (not (isUnliftedType arg_ty) || exprOkForSpeculation arg) (mkLetAppMsg arg) - ; lintValApp arg fun_ty arg_ty } + ; lintValApp arg fun_ty arg_ty fun_ue arg_ue } ----------------- -lintAltBinders :: LintedType -- Scrutinee type +lintAltBinders :: UsageEnv + -> Var -- Case binder + -> LintedType -- Scrutinee type -> LintedType -- Constructor type - -> [OutVar] -- Binders - -> LintM () + -> [(Mult, OutVar)] -- Binders + -> LintM UsageEnv -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] -lintAltBinders scrut_ty con_ty [] - = ensureEqTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty) -lintAltBinders scrut_ty con_ty (bndr:bndrs) +lintAltBinders rhs_ue _case_bndr scrut_ty con_ty [] + = do { ensureEqTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty) + ; return rhs_ue } +lintAltBinders rhs_ue case_bndr scrut_ty con_ty ((var_w, bndr):bndrs) | isTyVar bndr = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr) - ; lintAltBinders scrut_ty con_ty' bndrs } + ; lintAltBinders rhs_ue case_bndr scrut_ty con_ty' bndrs } | otherwise - = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr) - ; lintAltBinders scrut_ty con_ty' bndrs } + = do { (con_ty', _) <- lintValApp (Var bndr) con_ty (idType bndr) zeroUE zeroUE + -- We can pass zeroUE to lintValApp because we ignore its usage + -- calculation and compute it in the call for checkCaseLinearity below. + ; rhs_ue' <- checkCaseLinearity rhs_ue case_bndr var_w bndr + ; lintAltBinders rhs_ue' case_bndr scrut_ty con_ty' bndrs } + +-- | Implements the case rules for linearity +checkCaseLinearity :: UsageEnv -> Var -> Mult -> Var -> LintM UsageEnv +checkCaseLinearity ue case_bndr var_w bndr = do + ensureSubUsage lhs rhs err_msg + lintLinearBinder (ppr bndr) (case_bndr_w `mkMultMul` var_w) (varMult bndr) + return $ deleteUE ue bndr + where + lhs = bndr_usage `addUsage` (var_w `scaleUsage` case_bndr_usage) + rhs = case_bndr_w `mkMultMul` var_w + err_msg = (text "Linearity failure in variable:" <+> ppr bndr + $$ ppr lhs <+> text "⊈" <+> ppr rhs + $$ text "Computed by:" + <+> text "LHS:" <+> lhs_formula + <+> text "RHS:" <+> rhs_formula) + lhs_formula = ppr bndr_usage <+> text "+" + <+> parens (ppr case_bndr_usage <+> text "*" <+> ppr var_w) + rhs_formula = ppr case_bndr_w <+> text "*" <+> ppr var_w + case_bndr_w = varMult case_bndr + case_bndr_usage = lookupUE ue case_bndr + bndr_usage = lookupUE ue bndr + + ----------------- lintTyApp :: LintedType -> LintedType -> LintM LintedType @@ -1211,11 +1275,12 @@ lintTyApp fun_ty arg_ty -- | @lintValApp arg fun_ty arg_ty@ lints an application of @fun arg@ -- where @fun :: fun_ty@ and @arg :: arg_ty@, returning the type of the -- application. -lintValApp :: CoreExpr -> LintedType -> LintedType -> LintM LintedType -lintValApp arg fun_ty arg_ty - | Just (arg_ty', res_ty') <- splitFunTy_maybe fun_ty +lintValApp :: CoreExpr -> LintedType -> LintedType -> UsageEnv -> UsageEnv -> LintM (LintedType, UsageEnv) +lintValApp arg fun_ty arg_ty fun_ue arg_ue + | Just (Scaled w arg_ty', res_ty') <- splitFunTy_maybe fun_ty = do { ensureEqTys arg_ty' arg_ty err1 - ; return res_ty' } + ; let app_ue = addUE fun_ue (scaleUE w arg_ue) + ; return (res_ty', app_ue) } | otherwise = failWithL err2 where @@ -1242,14 +1307,15 @@ lintTyKind tyvar arg_ty ************************************************************************ -} -lintCaseExpr :: CoreExpr -> Id -> Type -> [CoreAlt] -> LintM LintedType +lintCaseExpr :: CoreExpr -> Id -> Type -> [CoreAlt] -> LintM (LintedType, UsageEnv) lintCaseExpr scrut var alt_ty alts = do { let e = Case scrut var alt_ty alts -- Just for error messages -- Check the scrutinee - ; scrut_ty <- markAllJoinsBad $ lintCoreExpr scrut + ; (scrut_ty, scrut_ue) <- markAllJoinsBad $ lintCoreExpr scrut -- See Note [Join points are less general than the paper] -- in GHC.Core + ; let scrut_mult = varMult var ; alt_ty <- addLoc (CaseTy scrut) $ lintValueType alt_ty @@ -1292,9 +1358,10 @@ lintCaseExpr scrut var alt_ty alts = ; lintBinder CaseBind var $ \_ -> do { -- Check the alternatives - mapM_ (lintCoreAlt scrut_ty alt_ty) alts + ; alt_ues <- mapM (lintCoreAlt var scrut_ty scrut_mult alt_ty) alts + ; let case_ue = (scaleUE scrut_mult scrut_ue) `addUE` supUEs alt_ues ; checkCaseAlts e scrut_ty alts - ; return alt_ty } } + ; return (alt_ty, case_ue) } } checkCaseAlts :: CoreExpr -> LintedType -> [CoreAlt] -> LintM () -- a) Check that the alts are non-empty @@ -1336,23 +1403,26 @@ checkCaseAlts e ty alts = Nothing -> False Just tycon -> isPrimTyCon tycon -lintAltExpr :: CoreExpr -> LintedType -> LintM () +lintAltExpr :: CoreExpr -> LintedType -> LintM UsageEnv lintAltExpr expr ann_ty - = do { actual_ty <- lintCoreExpr expr - ; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) } + = do { (actual_ty, ue) <- lintCoreExpr expr + ; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) + ; return ue } -- See GHC.Core Note [Case expression invariants] item (6) -lintCoreAlt :: LintedType -- Type of scrutinee - -> LintedType -- Type of the alternative +lintCoreAlt :: Var -- Case binder + -> LintedType -- Type of scrutinee + -> Mult -- Multiplicity of scrutinee + -> LintedType -- Type of the alternative -> CoreAlt - -> LintM () + -> LintM UsageEnv -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] -lintCoreAlt _ alt_ty (DEFAULT, args, rhs) = +lintCoreAlt _ _ _ alt_ty (DEFAULT, args, rhs) = do { lintL (null args) (mkDefaultArgsMsg args) ; lintAltExpr rhs alt_ty } -lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs) +lintCoreAlt _case_bndr scrut_ty _ alt_ty (LitAlt lit, args, rhs) | litIsLifted lit = failWithL integerScrutinisedMsg | otherwise @@ -1362,24 +1432,51 @@ lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs) where lit_ty = literalType lit -lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs) +lintCoreAlt case_bndr scrut_ty _scrut_mult alt_ty alt@(DataAlt con, args, rhs) | isNewTyCon (dataConTyCon con) - = addErrL (mkNewTyDataConAltMsg scrut_ty alt) + = zeroUE <$ addErrL (mkNewTyDataConAltMsg scrut_ty alt) | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty = addLoc (CaseAlt alt) $ do { -- First instantiate the universally quantified -- type variables of the data constructor -- We've already check lintL (tycon == dataConTyCon con) (mkBadConMsg tycon con) - ; let con_payload_ty = piResultTys (dataConRepType con) tycon_arg_tys + ; let { con_payload_ty = piResultTys (dataConRepType con) tycon_arg_tys + ; ex_tvs_n = length (dataConExTyCoVars con) + -- See Note [Alt arg multiplicities] + ; multiplicities = replicate ex_tvs_n Many ++ + map scaledMult (dataConRepArgTys con) } -- And now bring the new binders into scope ; lintBinders CasePatBind args $ \ args' -> do - { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args') - ; lintAltExpr rhs alt_ty } } + { + rhs_ue <- lintAltExpr rhs alt_ty + ; rhs_ue' <- addLoc (CasePat alt) (lintAltBinders rhs_ue case_bndr scrut_ty con_payload_ty (zipEqual "lintCoreAlt" multiplicities args')) + ; return $ deleteUE rhs_ue' case_bndr + } + } | otherwise -- Scrut-ty is wrong shape - = addErrL (mkBadAltMsg scrut_ty alt) + = zeroUE <$ addErrL (mkBadAltMsg scrut_ty alt) + +lintLinearBinder :: SDoc -> Mult -> Mult -> LintM () +lintLinearBinder doc actual_usage described_usage + = ensureSubMult actual_usage described_usage err_msg + where + err_msg = (text "Multiplicity of variable does not agree with its context" + $$ doc + $$ ppr actual_usage + $$ text "Annotation:" <+> ppr described_usage) + +{- +Note [Alt arg multiplicities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +It is necessary to use `dataConRepArgTys` so you get the arg tys from +the wrapper if there is one. + +You also need to add the existential ty vars as they are passed are arguments +but not returned by `dataConRepArgTys`. Without this the test `GADT1` fails. +-} {- ************************************************************************ @@ -1498,7 +1595,7 @@ lintTypes dflags vars tys | isEmptyBag errs = Nothing | otherwise = Just (pprMessageBag errs) where - (_warns, errs) = initL dflags defaultLintFlags vars linter + (_warns, errs) = initL dflags (defaultLintFlags dflags) vars linter linter = lintBinders LambdaBind vars $ \_ -> mapM_ lintType tys @@ -1559,7 +1656,7 @@ lintType ty@(TyConApp tc tys) ; lintTySynFamApp report_unsat ty tc tys } | isFunTyCon tc - , tys `lengthIs` 4 + , tys `lengthIs` 5 -- We should never see a saturated application of funTyCon; such -- applications should be represented with the FunTy constructor. -- See Note [Linting function types] and @@ -1574,11 +1671,12 @@ lintType ty@(TyConApp tc tys) -- arrows can related *unlifted* kinds, so this has to be separate from -- a dependent forall. -lintType ty@(FunTy af t1 t2) +lintType ty@(FunTy af tw t1 t2) = do { t1' <- lintType t1 ; t2' <- lintType t2 - ; lintArrow (text "type or kind" <+> quotes (ppr ty)) t1' t2' - ; return (FunTy af t1' t2') } + ; tw' <- lintType tw + ; lintArrow (text "type or kind" <+> quotes (ppr ty)) t1' t2' tw' + ; return (FunTy af tw' t1' t2') } lintType ty@(ForAllTy (Bndr tcv vis) body_ty) | not (isTyCoVar tcv) @@ -1673,16 +1771,18 @@ checkValueType ty doc kind = typeKind ty ----------------- -lintArrow :: SDoc -> LintedType -> LintedType -> LintM () +lintArrow :: SDoc -> LintedType -> LintedType -> LintedType -> LintM () -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] -lintArrow what t1 t2 -- Eg lintArrow "type or kind `blah'" k1 k2 - -- or lintArrow "coercion `blah'" k1 k2 +lintArrow what t1 t2 tw -- Eg lintArrow "type or kind `blah'" k1 k2 kw + -- or lintArrow "coercion `blah'" k1 k2 kw = do { unless (classifiesTypeWithValues k1) (addErrL (msg (text "argument") k1)) - ; unless (classifiesTypeWithValues k2) (addErrL (msg (text "result") k2)) } + ; unless (classifiesTypeWithValues k2) (addErrL (msg (text "result") k2)) + ; unless (isMultiplicityTy kw) (addErrL (msg (text "multiplicity") kw)) } where k1 = typeKind t1 k2 = typeKind t2 + kw = typeKind tw msg ar k = vcat [ hang (text "Ill-kinded" <+> ar) 2 (text "in" <+> what) @@ -1729,7 +1829,7 @@ lint_app doc kfn arg_tys | Just kfn' <- coreView kfn = go_app in_scope kfn' ta - go_app _ fun_kind@(FunTy _ kfa kfb) ta + go_app _ fun_kind@(FunTy _ _ kfa kfb) ta = do { let ka = typeKind ta ; unless (ka `eqType` kfa) $ addErrL (fail_msg (text "Fun:" <+> (ppr fun_kind $$ ppr ta <+> dcolon <+> ppr ka))) @@ -1759,8 +1859,8 @@ lintCoreRule _ _ (BuiltinRule {}) lintCoreRule fun fun_ty rule@(Rule { ru_name = name, ru_bndrs = bndrs , ru_args = args, ru_rhs = rhs }) = lintBinders LambdaBind bndrs $ \ _ -> - do { lhs_ty <- lintCoreArgs fun_ty args - ; rhs_ty <- case isJoinId_maybe fun of + do { (lhs_ty, _) <- lintCoreArgs (fun_ty, zeroUE) args + ; (rhs_ty, _) <- case isJoinId_maybe fun of Just join_arity -> do { checkL (args `lengthIs` join_arity) $ mkBadJoinPointRuleMsg fun join_arity rule @@ -1923,7 +2023,7 @@ lintCoercion (GRefl r ty (MCo co)) lintCoercion co@(TyConAppCo r tc cos) | tc `hasKey` funTyConKey - , [_rep1,_rep2,_co1,_co2] <- cos + , [_w, _rep1,_rep2,_co1,_co2] <- cos = failWithL (text "Saturated TyConAppCo (->):" <+> ppr co) -- All saturated TyConAppCos should be FunCos @@ -1990,16 +2090,24 @@ lintCoercion co@(ForAllCo tcv kind_co body_co) ; return (ForAllCo tcv' kind_co' body_co') } } -lintCoercion co@(FunCo r co1 co2) +lintCoercion co@(FunCo r cow co1 co2) = do { co1' <- lintCoercion co1 ; co2' <- lintCoercion co2 + ; cow' <- lintCoercion cow ; let Pair lt1 rt1 = coercionKind co1 Pair lt2 rt2 = coercionKind co2 - ; lintArrow (text "coercion" <+> quotes (ppr co)) lt1 lt2 - ; lintArrow (text "coercion" <+> quotes (ppr co)) rt1 rt2 + Pair ltw rtw = coercionKind cow + ; lintArrow (text "coercion" <+> quotes (ppr co)) lt1 lt2 ltw + ; lintArrow (text "coercion" <+> quotes (ppr co)) rt1 rt2 rtw ; lintRole co1 r (coercionRole co1) ; lintRole co2 r (coercionRole co2) - ; return (FunCo r co1' co2') } + ; ensureEqTys (typeKind ltw) multiplicityTy (text "coercion" <> quotes (ppr co)) + ; ensureEqTys (typeKind rtw) multiplicityTy (text "coercion" <> quotes (ppr co)) + ; let expected_mult_role = case r of + Phantom -> Phantom + _ -> Nominal + ; lintRole cow expected_mult_role (coercionRole cow) + ; return (FunCo r cow' co1' co2') } -- See Note [Bad unsafe coercion] lintCoercion co@(UnivCo prov r ty1 ty2) @@ -2269,6 +2377,9 @@ data LintEnv -- See Note [Join points] , le_dynflags :: DynFlags -- DynamicFlags + , le_ue_aliases :: NameEnv UsageEnv -- Assigns usage environments to the + -- alias-like binders, as found in + -- non-recursive lets. } data LintFlags @@ -2276,6 +2387,7 @@ data LintFlags , lf_check_inline_loop_breakers :: Bool -- See Note [Checking for INLINE loop breakers] , lf_check_static_ptrs :: StaticPtrCheck -- ^ See Note [Checking StaticPtrs] , lf_report_unsat_syns :: Bool -- ^ See Note [Linting type synonym applications] + , lf_check_linearity :: Bool -- ^ See Note [Linting linearity] , lf_check_levity_poly :: Bool -- See Note [Checking for levity polymorphism] } @@ -2289,13 +2401,14 @@ data StaticPtrCheck -- ^ Reject any 'makeStatic' occurrence. deriving Eq -defaultLintFlags :: LintFlags -defaultLintFlags = LF { lf_check_global_ids = False - , lf_check_inline_loop_breakers = True - , lf_check_static_ptrs = AllowAnywhere - , lf_report_unsat_syns = True - , lf_check_levity_poly = True - } +defaultLintFlags :: DynFlags -> LintFlags +defaultLintFlags dflags = LF { lf_check_global_ids = False + , lf_check_inline_loop_breakers = True + , lf_check_static_ptrs = AllowAnywhere + , lf_check_linearity = gopt Opt_DoLinearCoreLinting dflags + , lf_report_unsat_syns = True + , lf_check_levity_poly = True + } newtype LintM a = LintM { unLintM :: @@ -2371,6 +2484,25 @@ we behave as follows (#15057, #T15664): * If lf_report_unsat_syns is on, expand the synonym application and lint the result. Reason: want to check that synonyms are saturated when the type is expanded. + +Note [Linting linearity] +~~~~~~~~~~~~~~~~~~~~~~~~ +There are two known optimisations that have not yet been updated +to work with Linear Lint: + +* Lambda-bound variables with unfoldings + (see Note [Case binders and join points] and ticket #17530) +* Optimisations can create a letrec which uses a variable linearly, e.g. + letrec f True = f False + f False = x + in f True + uses 'x' linearly, but this is not seen by the linter. + Plan: make let-bound variables remember the usage environment. + See test LinearLetRec and https://github.com/tweag/ghc/issues/405. + +We plan to fix both of the issues in the very near future. +For now, linear Lint is disabled by default and +has to be enabled manually with -dlinear-core-lint. -} instance Applicative LintM where @@ -2423,7 +2555,8 @@ initL dflags flags vars m , le_ids = mkVarEnv [(id, (id,idType id)) | id <- ids] , le_joins = emptyVarSet , le_loc = [] - , le_dynflags = dflags } + , le_dynflags = dflags + , le_ue_aliases = emptyNameEnv } setReportUnsat :: Bool -> LintM a -> LintM a -- Switch off lf_report_unsat_syns @@ -2536,6 +2669,9 @@ getValidJoins = LintM (\ env errs -> (Just (le_joins env), errs)) getTCvSubst :: LintM TCvSubst getTCvSubst = LintM (\ env errs -> (Just (le_subst env), errs)) +getUEAliases :: LintM (NameEnv UsageEnv) +getUEAliases = LintM (\ env errs -> (Just (le_ue_aliases env), errs)) + getInScope :: LintM InScopeSet getInScope = LintM (\ env errs -> (Just (getTCvInScope $ le_subst env), errs)) @@ -2577,12 +2713,48 @@ lookupJoinId id Just id' -> return (isJoinId_maybe id') Nothing -> return Nothing } +addAliasUE :: Id -> UsageEnv -> LintM a -> LintM a +addAliasUE id ue thing_inside = LintM $ \ env errs -> + let new_ue_aliases = + extendNameEnv (le_ue_aliases env) (getName id) ue + in + unLintM thing_inside (env { le_ue_aliases = new_ue_aliases }) errs + +varCallSiteUsage :: Id -> LintM UsageEnv +varCallSiteUsage id = + do m <- getUEAliases + return $ case lookupNameEnv m (getName id) of + Nothing -> unitUE id One + Just id_ue -> id_ue + ensureEqTys :: LintedType -> LintedType -> MsgDoc -> LintM () -- check ty2 is subtype of ty1 (ie, has same structure but usage -- annotations need only be consistent, not equal) -- Assumes ty1,ty2 are have already had the substitution applied ensureEqTys ty1 ty2 msg = lintL (ty1 `eqType` ty2) msg +ensureSubUsage :: Usage -> Mult -> SDoc -> LintM () +ensureSubUsage Bottom _ _ = return () +ensureSubUsage Zero described_mult err_msg = ensureSubMult Many described_mult err_msg +ensureSubUsage (MUsage m) described_mult err_msg = ensureSubMult m described_mult err_msg + +ensureSubMult :: Mult -> Mult -> SDoc -> LintM () +ensureSubMult actual_usage described_usage err_msg = do + flags <- getLintFlags + when (lf_check_linearity flags) $ case actual_usage' `submult` described_usage' of + Submult -> return () + Unknown -> case actual_usage' of + MultMul m1 m2 -> ensureSubMult m1 described_usage' err_msg >> + ensureSubMult m2 described_usage' err_msg + _ -> when (not (actual_usage' `eqType` described_usage')) (addErrL err_msg) + + where actual_usage' = normalize actual_usage + described_usage' = normalize described_usage + + normalize :: Mult -> Mult + normalize (MultMul m1 m2) = mkMultMul (normalize m1) (normalize m2) + normalize m = m + lintRole :: Outputable thing => thing -- where the role appeared -> Role -- expected diff --git a/compiler/GHC/Core/Make.hs b/compiler/GHC/Core/Make.hs index 2156ce70ce..9ea1ed85e0 100644 --- a/compiler/GHC/Core/Make.hs +++ b/compiler/GHC/Core/Make.hs @@ -72,6 +72,7 @@ import GHC.Hs.Utils ( mkChunkified, chunkify ) import GHC.Core.Type import GHC.Core.Coercion ( isCoVar ) import GHC.Core.DataCon ( DataCon, dataConWorkId ) +import GHC.Core.Multiplicity import GHC.Builtin.Types.Prim import GHC.Types.Id.Info import GHC.Types.Demand @@ -168,16 +169,16 @@ mkCoreAppTyped d (fun, fun_ty) arg where (arg_ty, res_ty) = splitFunTy fun_ty -mkValApp :: CoreExpr -> CoreExpr -> Type -> Type -> CoreExpr +mkValApp :: CoreExpr -> CoreExpr -> Scaled Type -> Type -> CoreExpr -- Build an application (e1 e2), -- or a strict binding (case e2 of x -> e1 x) -- using the latter when necessary to respect the let/app invariant -- See Note [Core let/app invariant] in GHC.Core -mkValApp fun arg arg_ty res_ty +mkValApp fun arg (Scaled w arg_ty) res_ty | not (needsCaseBinding arg_ty arg) = App fun arg -- The vastly common case | otherwise - = mkStrictApp fun arg arg_ty res_ty + = mkStrictApp fun arg (Scaled w arg_ty) res_ty {- ********************************************************************* * * @@ -186,33 +187,33 @@ mkValApp fun arg arg_ty res_ty ********************************************************************* -} mkWildEvBinder :: PredType -> EvVar -mkWildEvBinder pred = mkWildValBinder pred +mkWildEvBinder pred = mkWildValBinder Many pred -- | Make a /wildcard binder/. This is typically used when you need a binder -- that you expect to use only at a *binding* site. Do not use it at -- occurrence sites because it has a single, fixed unique, and it's very -- easy to get into difficulties with shadowing. That's why it is used so little. -- See Note [WildCard binders] in GHC.Core.Opt.Simplify.Env -mkWildValBinder :: Type -> Id -mkWildValBinder ty = mkLocalIdOrCoVar wildCardName ty +mkWildValBinder :: Mult -> Type -> Id +mkWildValBinder w ty = mkLocalIdOrCoVar wildCardName w ty -- "OrCoVar" since a coercion can be a scrutinee with -fdefer-type-errors -- (e.g. see test T15695). Ticket #17291 covers fixing this problem. -mkWildCase :: CoreExpr -> Type -> Type -> [CoreAlt] -> CoreExpr +mkWildCase :: CoreExpr -> Scaled Type -> Type -> [CoreAlt] -> CoreExpr -- Make a case expression whose case binder is unused -- The alts and res_ty should not have any occurrences of WildId -mkWildCase scrut scrut_ty res_ty alts - = Case scrut (mkWildValBinder scrut_ty) res_ty alts +mkWildCase scrut (Scaled w scrut_ty) res_ty alts + = Case scrut (mkWildValBinder w scrut_ty) res_ty alts -mkStrictApp :: CoreExpr -> CoreExpr -> Type -> Type -> CoreExpr +mkStrictApp :: CoreExpr -> CoreExpr -> Scaled Type -> Type -> CoreExpr -- Build a strict application (case e2 of x -> e1 x) -mkStrictApp fun arg arg_ty res_ty +mkStrictApp fun arg (Scaled w arg_ty) res_ty = Case arg arg_id res_ty [(DEFAULT,[],App fun (Var arg_id))] -- mkDefaultCase looks attractive here, and would be sound. -- But it uses (exprType alt_rhs) to compute the result type, -- whereas here we already know that the result type is res_ty where - arg_id = mkWildValBinder arg_ty + arg_id = mkWildValBinder w arg_ty -- Lots of shadowing, but it doesn't matter, -- because 'fun' and 'res_ty' should not have a free wild-id -- @@ -226,7 +227,7 @@ mkStrictApp fun arg arg_ty res_ty mkIfThenElse :: CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr mkIfThenElse guard then_expr else_expr -- Not going to be refining, so okay to take the type of the "then" clause - = mkWildCase guard boolTy (exprType then_expr) + = mkWildCase guard (linear boolTy) (exprType then_expr) [ (DataAlt falseDataCon, [], else_expr), -- Increasing order of tag! (DataAlt trueDataCon, [], then_expr) ] @@ -236,7 +237,7 @@ castBottomExpr :: CoreExpr -> Type -> CoreExpr -- See Note [Empty case alternatives] in GHC.Core castBottomExpr e res_ty | e_ty `eqType` res_ty = e - | otherwise = Case e (mkWildValBinder e_ty) res_ty [] + | otherwise = Case e (mkWildValBinder One e_ty) res_ty [] where e_ty = exprType e @@ -448,6 +449,10 @@ unitExpr = Var unitDataConId -- just the identity. -- -- If necessary, we pattern match on a \"big\" tuple. +-- +-- A tuple selector is not linear in its argument. Consequently, the case +-- expression built by `mkTupleSelector` must consume its scrutinee 'Many' +-- times. And all the argument variables must have multiplicity 'Many'. mkTupleSelector, mkTupleSelector1 :: [Id] -- ^ The 'Id's to pattern match the tuple against -> Id -- ^ The 'Id' to select @@ -542,7 +547,7 @@ mkTupleCase uniqs vars body scrut_var scrut one_tuple_case chunk_vars (us, vs, body) = let (uniq, us') = takeUniqFromSupply us - scrut_var = mkSysLocal (fsLit "ds") uniq + scrut_var = mkSysLocal (fsLit "ds") uniq Many (mkBoxedTupleTy (map idType chunk_vars)) body' = mkSmallTupleCase chunk_vars body scrut_var (Var scrut_var) in (us', scrut_var:vs, body') @@ -648,8 +653,8 @@ mkBuildExpr :: (MonadFail m, MonadThings m, MonadUnique m) mkBuildExpr elt_ty mk_build_inside = do n_tyvar <- newTyVar alphaTyVar let n_ty = mkTyVarTy n_tyvar - c_ty = mkVisFunTys [elt_ty, n_ty] n_ty - [c, n] <- sequence [mkSysLocalM (fsLit "c") c_ty, mkSysLocalM (fsLit "n") n_ty] + c_ty = mkVisFunTysMany [elt_ty, n_ty] n_ty + [c, n] <- sequence [mkSysLocalM (fsLit "c") Many c_ty, mkSysLocalM (fsLit "n") Many n_ty] build_inside <- mk_build_inside (c, c_ty) (n, n_ty) @@ -874,7 +879,7 @@ runtimeErrorTy :: Type -- forall (rr :: RuntimeRep) (a :: rr). Addr# -> a -- See Note [Error and friends have an "open-tyvar" forall] runtimeErrorTy = mkSpecForAllTys [runtimeRep1TyVar, openAlphaTyVar] - (mkVisFunTy addrPrimTy openAlphaTy) + (mkVisFunTyMany addrPrimTy openAlphaTy) {- Note [Error and friends have an "open-tyvar" forall] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -964,7 +969,7 @@ be relying on anything from it. aBSENT_ERROR_ID = mkVanillaGlobalWithInfo absentErrorName absent_ty arity_info where - absent_ty = mkSpecForAllTys [alphaTyVar] (mkVisFunTy addrPrimTy alphaTy) + absent_ty = mkSpecForAllTys [alphaTyVar] (mkVisFunTyMany addrPrimTy alphaTy) -- Not runtime-rep polymorphic. aBSENT_ERROR_ID is only used for -- lifted-type things; see Note [Absent errors] in GHC.Core.Opt.WorkWrap.Utils arity_info = vanillaIdInfo `setArityInfo` 1 diff --git a/compiler/GHC/Core/Map.hs b/compiler/GHC/Core/Map.hs index 6fc041887d..f8304d0d25 100644 --- a/compiler/GHC/Core/Map.hs +++ b/compiler/GHC/Core/Map.hs @@ -10,6 +10,7 @@ {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} module GHC.Core.Map ( -- * Maps over Core expressions @@ -179,7 +180,8 @@ data CoreMapX a instance Eq (DeBruijn CoreExpr) where D env1 e1 == D env2 e2 = go e1 e2 where - go (Var v1) (Var v2) = case (lookupCME env1 v1, lookupCME env2 v2) of + go (Var v1) (Var v2) + = case (lookupCME env1 v1, lookupCME env2 v2) of (Just b1, Just b2) -> b1 == b2 (Nothing, Nothing) -> v1 == v2 _ -> False @@ -193,6 +195,7 @@ instance Eq (DeBruijn CoreExpr) where go (Lam b1 e1) (Lam b2 e2) = D env1 (varType b1) == D env2 (varType b2) + && D env1 (varMultMaybe b1) == D env2 (varMultMaybe b2) && D (extendCME env1 b1) e1 == D (extendCME env2 b2) e2 go (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2) @@ -520,8 +523,8 @@ instance Eq (DeBruijn Type) where -> D env t1 == D env' t1' && D env t2 == D env' t2' (s, AppTy t1' t2') | Just (t1, t2) <- repSplitAppTy_maybe s -> D env t1 == D env' t1' && D env t2 == D env' t2' - (FunTy _ t1 t2, FunTy _ t1' t2') - -> D env t1 == D env' t1' && D env t2 == D env' t2' + (FunTy _ w1 t1 t2, FunTy _ w1' t1' t2') + -> D env w1 == D env w1' && D env t1 == D env' t1' && D env t2 == D env' t2' (TyConApp tc tys, TyConApp tc' tys') -> tc == tc' && D env tys == D env' tys' (LitTy l, LitTy l') @@ -745,6 +748,11 @@ instance Eq (DeBruijn a) => Eq (DeBruijn [a]) where D env xs == D env' xs' _ == _ = False +instance Eq (DeBruijn a) => Eq (DeBruijn (Maybe a)) where + D _ Nothing == D _ Nothing = True + D env (Just x) == D env' (Just x') = D env x == D env' x' + _ == _ = False + --------- Variable binders ------------- -- | A 'BndrMap' is a 'TypeMapG' which allows us to distinguish between @@ -753,7 +761,26 @@ instance Eq (DeBruijn a) => Eq (DeBruijn [a]) where -- not pick up an entry in the 'TrieMap' for @\(x :: Bool) -> ()@: -- we can disambiguate this by matching on the type (or kind, if this -- a binder in a type) of the binder. -type BndrMap = TypeMapG +-- +-- We also need to do the same for multiplicity! Which, since multiplicities are +-- encoded simply as a 'Type', amounts to have a Trie for a pair of types. Tries +-- of pairs are composition. +data BndrMap a = BndrMap (TypeMapG (MaybeMap TypeMapG a)) + +instance TrieMap BndrMap where + type Key BndrMap = Var + emptyTM = BndrMap emptyTM + lookupTM = lkBndr emptyCME + alterTM = xtBndr emptyCME + foldTM = fdBndrMap + mapTM = mapBndrMap + +mapBndrMap :: (a -> b) -> BndrMap a -> BndrMap b +mapBndrMap f (BndrMap tm) = BndrMap (mapTM (mapTM f) tm) + +fdBndrMap :: (a -> b -> b) -> BndrMap a -> b -> b +fdBndrMap f (BndrMap tm) = foldTM (foldTM f) tm + -- Note [Binders] -- ~~~~~~~~~~~~~~ @@ -761,10 +788,15 @@ type BndrMap = TypeMapG -- of these data types have binding forms. lkBndr :: CmEnv -> Var -> BndrMap a -> Maybe a -lkBndr env v m = lkG (D env (varType v)) m +lkBndr env v (BndrMap tymap) = do + multmap <- lkG (D env (varType v)) tymap + lookupTM (D env <$> varMultMaybe v) multmap + + +xtBndr :: forall a . CmEnv -> Var -> XT a -> BndrMap a -> BndrMap a +xtBndr env v xt (BndrMap tymap) = + BndrMap (tymap |> xtG (D env (varType v)) |>> (alterTM (D env <$> varMultMaybe v) xt)) -xtBndr :: CmEnv -> Var -> XT a -> BndrMap a -> BndrMap a -xtBndr env v f = xtG (D env (varType v)) f --------- Variable occurrence ------------- data VarMap a = VM { vm_bvar :: BoundVarMap a -- Bound variable diff --git a/compiler/GHC/Core/Multiplicity.hs b/compiler/GHC/Core/Multiplicity.hs new file mode 100644 index 0000000000..a4203fa6e0 --- /dev/null +++ b/compiler/GHC/Core/Multiplicity.hs @@ -0,0 +1,410 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE PatternSynonyms, ViewPatterns #-} + +{-| +This module defines the semi-ring of multiplicities, and associated functions. +Multiplicities annotate arrow types to indicate the linearity of the +arrow (in the sense of linear types). + +Mult is a type synonym for Type, used only when its kind is Multiplicity. +To simplify dealing with multiplicities, functions such as +mkMultMul perform simplifications such as Many * x = Many on the fly. +-} +module GHC.Core.Multiplicity + ( Mult + , pattern One + , pattern Many + , pattern MultMul + , mkMultAdd + , mkMultMul + , mkMultSup + , Scaled(..) + , scaledMult + , scaledThing + , unrestricted + , linear + , tymult + , irrelevantMult + , mkScaled + , scaledSet + , scaleScaled + , IsSubmult(..) + , submult + , mapScaledType) where + +import GHC.Prelude + +import Data.Data +import GHC.Utils.Outputable +import {-# SOURCE #-} GHC.Core.TyCo.Rep (Type) +import {-# SOURCE #-} GHC.Builtin.Types ( oneDataConTy, manyDataConTy, multMulTyCon ) +import {-# SOURCE #-} GHC.Core.Type( eqType, splitTyConApp_maybe, mkTyConApp ) +import GHC.Builtin.Names (multMulTyConKey) +import GHC.Types.Unique (hasKey) + +{- +Note [Linear types] +~~~~~~~~~~~~~~~~~~~ +This module is the entry point for linear types. + +The detailed design is in the _Linear Haskell_ article +[https://arxiv.org/abs/1710.09756]. Other important resources in the linear +types implementation wiki page +[https://gitlab.haskell.org/ghc/ghc/wikis/linear-types/implementation], and the +proposal [https://github.com/ghc-proposals/ghc-proposals/pull/111] which +describes the concrete design at length. + +For the busy developer, though, here is a high-level view of linear types is the following: + +- Function arrows are annotated with a multiplicity (as defined by type `Mult` + and its smart constructors in this module) + - Because, as a type constructor, the type of function now has an extra + argument, the notation (->) is no longer suitable. We named the function + type constructor `FUN`. + - (->) retains its backward compatible meaning: `(->) a b = a -> b`. To + achieve this, `(->)` is defined as a type synonym to `FUN Many` (see + below). +- Multiplicities can be reified in Haskell as types of kind + `GHC.Types.Multiplicity` +- Ground multiplicity (that is, without a variable) can be `One` or `Many` + (`Many` is generally rendered as ω in the scientific literature). + Functions whose type is annotated with `One` are linear functions, functions whose + type is annotated with `Many` are regular functions, often called “unrestricted” + to contrast them with linear functions. +- A linear function is defined as a function such that *if* its result is + consumed exactly once, *then* its argument is consumed exactly once. You can + think of “consuming exactly once” as evaluating a value in normal form exactly + once (though not necessarily in one go). The _Linear Haskell_ article (see + infra) has a more precise definition of “consuming exactly once”. +- Data types can have unrestricted fields (the canonical example being the + `Unrestricted` data type), then these don't need to be consumed for a value to + be consumed exactly once. So consuming a value of type `Unrestricted` exactly + once means forcing it at least once. +- Why “at least once”? Because if `case u of { C x y -> f (C x y) }` is linear + (provided `f` is a linear function). So we might as well have done `case u of + { !z -> f z }`. So, we can observe constructors as many times as we want, and + we are actually allowed to force the same thing several times because laziness + means that we are really forcing a the value once, and observing its + constructor several times. The type checker and the linter recognise some (but + not all) of these multiple forces as indeed linear. Mostly just enough to + support variable patterns. +- Multiplicities form a semiring. +- Multiplicities can also be variables and we can universally quantify over + these variables. This is referred to as “multiplicity + polymorphism”. Furthermore, multiplicity can be formal semiring expressions + combining variables. +- Contrary to the paper, the sum of two multiplicities is always `Many`. This + will have to change, however, if we want to add a multiplicity for 0. Whether + we want to is still debated. +- Case expressions have a multiplicity annotation too. A case expression with + multiplicity `One`, consumes its scrutinee exactly once (provided the entire + case expression is consumed exactly once); whereas a case expression with + multiplicity `Many` can consume its scrutinee as many time as it wishes (no + matter how much the case expression is consumed). + +Note [Usages] +~~~~~~~~~~~~~ +In the _Linear Haskell_ paper, you'll find typing rules such as these: + + Γ ⊢ f : A #π-> B Δ ⊢ u : A + --------------------------- + Γ + kΔ ⊢ f u : B + +If you read this as a type-checking algorithm going from the bottom up, this +reads as: the algorithm has to find a split of some input context Ξ into an +appropriate Γ and a Δ such as Ξ = Γ + kΔ, *and the multiplicities are chosen to +make f and u typecheck*. + +This could be achieved by letting the typechecking of `f` use exactly the +variable it needs, then passing the remainder, as `Delta` to the typechecking of +u. But what does that mean if `x` is bound with multiplicity `p` (a variable) +and `f` consumes `x` once? `Delta` would have to contain `x` with multiplicity +`p-1`. It's not really clear how to make that works. In summary: bottom-up +multiplicity checking forgoes addition and multiplication in favour of +subtraction and division. And variables make the latter hard. + +The alternative is to read multiplicities from the top down: as an *output* from +the typechecking algorithm, rather than an input. We call these output +multiplicities Usages, to distinguish them from the multiplicities which come, +as input, from the types of functions. Usages are checked for compatibility with +multiplicity annotations using an ordering relation. In other words, the usage +of x in the expression u is the smallest multiplicity which can be ascribed to x +for u to typecheck. + +Usages are usually group in a UsageEnv, as defined in the UsageEnv module. + +So, in our function application example, the typechecking algorithm would +receive usage environements f_ue from the typechecking of f, and u_ue from the +typechecking of u. Then the output would be f_ue + (k * u_ue). Addition and +scaling of usage environment is the pointwise extension of the semiring +operations on multiplicities. + +Note [Zero as a usage] +~~~~~~~~~~~~~~~~~~~~~~ +In the current presentation usages are not exactly multiplicities, because they +can contain 0, and multiplicities can't. + +Why do we need a 0 usage? A function which doesn't use its argument will be +required to annotate it with `Many`: + + \(x # Many) -> 0 + +However, we cannot replace absence with Many when computing usages +compositionally: in + + (x, True) + +We expect x to have usage 1. But when computing the usage of x in True we would +find that x is absent, hence has multiplicity Many. The final multiplicity would +be One+Many = Many. Oops! + +Hence there is a usage Zero for absent variables. Zero is characterised by being +the neutral element to usage addition. + +We may decide to add Zero as a multiplicity in the future. In which case, this +distinction will go away. + +Note [Joining usages] +~~~~~~~~~~~~~~~~~~~~~ +The usage of a variable is defined, in Note [Usages], as the minimum usage which +can be ascribed to a variable. + +So what is the usage of x in + + case … of + { p1 -> u -- usage env: u_ue + ; p2 -> v } -- usage env: v_ue + +It must be the least upper bound, or _join_, of u_ue(x) and v_ue(x). + +So, contrary to a declarative presentation where the correct usage of x can be +conjured out of thin air, we need to be able to compute the join of two +multiplicities. Join is extended pointwise on usage environments. + +Note [Bottom as a usage] +~~~~~~~~~~~~~~~~~~~~~~ +What is the usage of x in + + case … of {} + +Per usual linear logic, as well as the _Linear Haskell_ article, x can have +every multiplicity. + +So we need a minimum usage _bottom_, which is also the neutral element for join. + +In fact, this is not such as nice solution, because it is not clear how to +define sum and multiplication with bottom. We give reasonable definitions, but +they are not complete (they don't respect the semiring laws, and it's possible +to come up with examples of Core transformation which are not well-typed) + +A better solution would probably be to annotate case expressions with a usage +environment, just like they are annotated with a type. Which, probably not +coincidentally, is also primarily for empty cases. + +A side benefit of this approach is that the linter would not need to join +multiplicities, anymore; hence would be closer to the presentation in the +article. That's because it could use the annotation as the multiplicity for each +branch. + +Note [Data constructors are linear by default] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Data constructors defined without -XLinearTypes (as well as data constructors +defined with the Haskell 98 in all circumstances) have all their fields linear. + +That is, in + + data Maybe a = Nothing | Just a + +We have + + Just :: a #-> Just a + +The goal is to maximise reuse of types between linear code and traditional +code. This is argued at length in the proposal and the article (links in Note +[Linear Types]). + +Note [Polymorphisation of linear fields] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The choice in Note [Data constructors are linear by default] has an impact on +backwards compatibility. Consider + + map Just + +We have + + map :: (a -> b) -> f a -> f b + Just :: a #-> Just a + +Types don't match, we should get a type error. But this is legal Haskell 98 +code! Bad! Bad! Bad! + +It could be solved with subtyping, but subtyping doesn't combine well with +polymorphism. + +Instead, we generalise the type of Just, when used as term: + + Just :: forall {p}. a #p-> Just a + +This is solely a concern for higher-order code like this: when called fully +applied linear constructors are more general than constructors with unrestricted +fields. In particular, linear constructors can always be eta-expanded to their +Haskell 98 type. This is explained in the paper (but there, we had a different +strategy to resolve this type mismatch in higher-order code. It turned out to be +insufficient, which is explained in the wiki page as well as the proposal). + +We only generalise linear fields this way: fields with multiplicity Many, or +other multiplicity expressions are exclusive to -XLinearTypes, hence don't have +backward compatibility implications. + +The implementation is described in Note [Linear fields generalization]. + +More details in the proposal. +-} + +{- +Note [Adding new multiplicities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +To add a new multiplicity, you need to: +* Add the new type with Multiplicity kind +* Update cases in mkMultAdd, mkMultMul, mkMultSup, submult, tcSubMult +* Check supUE function that computes sup of a multiplicity + and Zero +-} + +-- +-- * Core properties of multiplicities +-- + +{- +Note [Mult is type] +~~~~~~~~~~~~~~~~~~~ +Mult is a type alias for Type. + +Mult must contain Type because multiplicity variables are mere type variables +(of kind Multiplicity) in Haskell. So the simplest implementation is to make +Mult be Type. + +Multiplicities can be formed with: +- One: GHC.Types.One (= oneDataCon) +- Many: GHC.Types.Many (= manyDataCon) +- Multiplication: GHC.Types.MultMul (= multMulTyCon) + +So that Mult feels a bit more structured, we provide pattern synonyms and smart +constructors for these. +-} +type Mult = Type + +pattern One :: Mult +pattern One <- (eqType oneDataConTy -> True) + where One = oneDataConTy + +pattern Many :: Mult +pattern Many <- (eqType manyDataConTy -> True) + where Many = manyDataConTy + +isMultMul :: Mult -> Maybe (Mult, Mult) +isMultMul ty | Just (tc, [x, y]) <- splitTyConApp_maybe ty + , tc `hasKey` multMulTyConKey = Just (x, y) + | otherwise = Nothing + +pattern MultMul :: Mult -> Mult -> Mult +pattern MultMul p q <- (isMultMul -> Just (p,q)) + +{- +Note [Overapproximating multiplicities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The functions mkMultAdd, mkMultMul, mkMultSup perform operations +on multiplicities. They can return overapproximations: their result +is merely guaranteed to be a submultiplicity of the actual value. + +They should be used only when an upper bound is acceptable. +In most cases, they are used in usage environments (UsageEnv); +in usage environments, replacing a usage with a larger one can only +cause more programs to fail to typecheck. + +In future work, instead of approximating we might add type families +and allow users to write types involving operations on multiplicities. +In this case, we could enforce more invariants in Mult, for example, +enforce that that it is in the form of a sum of products, and even +that the sumands and factors are ordered somehow, to have more equalities. +-} + +-- With only two multiplicities One and Many, we can always replace +-- p + q by Many. See Note [Overapproximating multiplicities]. +mkMultAdd :: Mult -> Mult -> Mult +mkMultAdd _ _ = Many + +mkMultMul :: Mult -> Mult -> Mult +mkMultMul One p = p +mkMultMul p One = p +mkMultMul Many _ = Many +mkMultMul _ Many = Many +mkMultMul p q = mkTyConApp multMulTyCon [p, q] + +-- See Note [Joining usages] +-- | @mkMultSup w1 w2@ returns a multiplicity such that @mkMultSup w1 +-- w2 >= w1@ and @mkMultSup w1 w2 >= w2@. See Note [Overapproximating multiplicities]. +mkMultSup :: Mult -> Mult -> Mult +mkMultSup = mkMultMul +-- Note: If you are changing this logic, check 'supUE' in UsageEnv as well. + +-- +-- * Multiplicity ordering +-- + +data IsSubmult = Submult -- Definitely a submult + | Unknown -- Could be a submult, need to ask the typechecker + deriving (Show, Eq) + +instance Outputable IsSubmult where + ppr = text . show + +-- | @submult w1 w2@ check whether a value of multiplicity @w1@ is allowed where a +-- value of multiplicity @w2@ is expected. This is a partial order. + +submult :: Mult -> Mult -> IsSubmult +submult _ Many = Submult +submult One One = Submult +-- The 1 <= p rule +submult One _ = Submult +submult _ _ = Unknown + +-- +-- * Utilities +-- + +-- | A shorthand for data with an attached 'Mult' element (the multiplicity). +data Scaled a = Scaled Mult a + deriving (Data) + +scaledMult :: Scaled a -> Mult +scaledMult (Scaled m _) = m + +scaledThing :: Scaled a -> a +scaledThing (Scaled _ t) = t + +unrestricted, linear, tymult :: a -> Scaled a +unrestricted = Scaled Many +linear = Scaled One + +-- Used for type arguments in core +tymult = Scaled Many + +irrelevantMult :: Scaled a -> a +irrelevantMult = scaledThing + +mkScaled :: Mult -> a -> Scaled a +mkScaled = Scaled + +instance (Outputable a) => Outputable (Scaled a) where + ppr (Scaled _cnt t) = ppr t + -- Do not print the multiplicity here because it tends to be too verbose + +scaledSet :: Scaled a -> b -> Scaled b +scaledSet (Scaled m _) b = Scaled m b + +scaleScaled :: Mult -> Scaled a -> Scaled a +scaleScaled m' (Scaled m t) = Scaled (m' `mkMultMul` m) t + +mapScaledType :: (Type -> Type) -> Scaled Type -> Scaled Type +mapScaledType f (Scaled m t) = Scaled (f m) (f t) diff --git a/compiler/GHC/Core/Opt/Arity.hs b/compiler/GHC/Core/Opt/Arity.hs index 17acd5dbfe..44505ef0b6 100644 --- a/compiler/GHC/Core/Opt/Arity.hs +++ b/compiler/GHC/Core/Opt/Arity.hs @@ -35,6 +35,7 @@ import GHC.Core.Type as Type import GHC.Core.TyCon ( initRecTc, checkRecTc ) import GHC.Core.Predicate ( isDictTy ) import GHC.Core.Coercion as Coercion +import GHC.Core.Multiplicity import GHC.Types.Basic import GHC.Types.Unique import GHC.Driver.Session ( DynFlags, GeneralFlag(..), gopt ) @@ -125,7 +126,7 @@ typeArity ty = go rec_nts ty' | Just (arg,res) <- splitFunTy_maybe ty - = typeOneShot arg : go rec_nts res + = typeOneShot (scaledThing arg) : go rec_nts res | Just (tc,tys) <- splitTyConApp_maybe ty , Just (ty', _) <- instNewTyCon_maybe tc tys @@ -1089,13 +1090,13 @@ mkEtaWW orig_n ppr_orig_expr in_scope orig_ty -- lambda \co:ty. e co. In this case we generate a new variable -- of the coercion type, update the scope, and reduce n by 1. | isTyVar tcv = ((subst', tcv'), n) - | otherwise = (freshEtaId n subst' (varType tcv'), n-1) + | otherwise = (freshEtaId n subst' (varScaledType tcv'), n-1) -- Avoid free vars of the original expression in go n_n n_subst ty' (EtaVar n_tcv : eis) ----------- Function types (t1 -> t2) | Just (arg_ty, res_ty) <- splitFunTy_maybe ty - , not (isTypeLevPoly arg_ty) + , not (isTypeLevPoly (scaledThing arg_ty)) -- See Note [Levity polymorphism invariants] in GHC.Core -- See also test case typecheck/should_run/EtaExpandLevPoly @@ -1192,7 +1193,7 @@ etaBodyForJoinPoint need_args body init_subst e = mkEmptyTCvSubst (mkInScopeSet (exprFreeVars e)) -------------- -freshEtaId :: Int -> TCvSubst -> Type -> (TCvSubst, Id) +freshEtaId :: Int -> TCvSubst -> Scaled Type -> (TCvSubst, Id) -- Make a fresh Id, with specified type (after applying substitution) -- It should be "fresh" in the sense that it's not in the in-scope set -- of the TvSubstEnv; and it should itself then be added to the in-scope @@ -1203,9 +1204,9 @@ freshEtaId :: Int -> TCvSubst -> Type -> (TCvSubst, Id) freshEtaId n subst ty = (subst', eta_id') where - ty' = Type.substTyUnchecked subst ty + Scaled mult' ty' = Type.substScaledTyUnchecked subst ty eta_id' = uniqAway (getTCvInScope subst) $ - mkSysLocalOrCoVar (fsLit "eta") (mkBuiltinUnique n) ty' + mkSysLocalOrCoVar (fsLit "eta") (mkBuiltinUnique n) mult' ty' -- "OrCoVar" since this can be used to eta-expand -- coercion abstractions subst' = extendTCvInScope subst eta_id' diff --git a/compiler/GHC/Core/Opt/CSE.hs b/compiler/GHC/Core/Opt/CSE.hs index d6f37f6eb5..16a0137a4c 100644 --- a/compiler/GHC/Core/Opt/CSE.hs +++ b/compiler/GHC/Core/Opt/CSE.hs @@ -16,7 +16,7 @@ module GHC.Core.Opt.CSE (cseProgram, cseOneExpr) where import GHC.Prelude import GHC.Core.Subst -import GHC.Types.Var ( Var ) +import GHC.Types.Var ( Var, varMultMaybe ) import GHC.Types.Var.Env ( mkInScopeSet ) import GHC.Types.Id ( Id, idType, idHasRules , idInlineActivation, setInlineActivation @@ -33,6 +33,7 @@ import GHC.Types.Basic import GHC.Core.Map import GHC.Utils.Misc ( filterOut, equalLength, debugIsOn ) import Data.List ( mapAccumL ) +import GHC.Core.Multiplicity {- Simple common sub-expression @@ -449,8 +450,34 @@ noCSE id = not (isAlwaysActive (idInlineActivation id)) && -- See Note [CSE for INLINE and NOINLINE] || isAnyInlinePragma (idInlinePragma id) -- See Note [CSE for stable unfoldings] + || not (multiplicityOkForCSE id) || isJoinId id -- See Note [CSE for join points?] + where + -- It doesn't make sense to do CSE for a binding which can't be freely + -- shared or dropped. In particular linear bindings, but this is true for + -- any binding whose multiplicity contains a variable. + -- + -- This shows up, in particular, when performing a substitution + -- + -- CSE[let x # 'One = y in x] + -- ==> let x # 'One = y in CSE[x[x\y]] + -- ==> let x # 'One = y in y + -- + -- Here @x@ doesn't appear in the body, but it is required by linearity! + -- Also @y@ appears shared, while we expect it to be a linear variable. + -- + -- This is usually not a problem with let-binders because they are aliases. + -- But we don't have such luxury for case binders. Still, substitution of + -- the case binder by the scrutinee happens routinely in CSE to discover + -- more CSE opportunities (see Note [CSE for case expressions]). + -- + -- It's alright, though! Because there is never a need to share linear + -- definitions. + multiplicityOkForCSE v = case varMultMaybe v of + Just Many -> True + Just _ -> False + Nothing -> True {- Note [Take care with literal strings] diff --git a/compiler/GHC/Core/Opt/ConstantFold.hs b/compiler/GHC/Core/Opt/ConstantFold.hs index 5ae5fa693c..6ca8efce2e 100644 --- a/compiler/GHC/Core/Opt/ConstantFold.hs +++ b/compiler/GHC/Core/Opt/ConstantFold.hs @@ -46,6 +46,7 @@ import GHC.Core.DataCon ( dataConTagZ, dataConTyCon, dataConWrapId, dataConWorkI import GHC.Core.Utils ( eqExpr, cheapEqExpr, exprIsHNF, exprType , stripTicksTop, stripTicksTopT, mkTicks ) import GHC.Core.Unfold ( exprIsConApp_maybe ) +import GHC.Core.Multiplicity import GHC.Core.FVs import GHC.Core.Type import GHC.Types.Var.Set @@ -549,7 +550,7 @@ litEq is_eq = msum where do_lit_eq platform lit expr = do guard (not (litIsLifted lit)) - return (mkWildCase expr (literalType lit) intPrimTy + return (mkWildCase expr (unrestricted $ literalType lit) intPrimTy [(DEFAULT, [], val_if_neq), (LitAlt lit, [], val_if_eq)]) where @@ -1557,8 +1558,8 @@ match_inline _ = Nothing match_magicDict :: [Expr CoreBndr] -> Maybe (Expr CoreBndr) match_magicDict [Type _, Var wrap `App` Type a `App` Type _ `App` f, x, y ] | Just (fieldTy, _) <- splitFunTy_maybe $ dropForAlls $ idType wrap - , Just (dictTy, _) <- splitFunTy_maybe fieldTy - , Just dictTc <- tyConAppTyCon_maybe dictTy + , Just (dictTy, _) <- splitFunTy_maybe (scaledThing fieldTy) + , Just dictTc <- tyConAppTyCon_maybe (scaledThing dictTy) , Just (_,_,co) <- unwrapNewTyCon_maybe dictTc = Just $ f `App` Cast x (mkSymCo (mkUnbranchedAxInstCo Representational co [a] [])) diff --git a/compiler/GHC/Core/Opt/DmdAnal.hs b/compiler/GHC/Core/Opt/DmdAnal.hs index 29fa61a5fc..e5d9c9a0d9 100644 --- a/compiler/GHC/Core/Opt/DmdAnal.hs +++ b/compiler/GHC/Core/Opt/DmdAnal.hs @@ -19,6 +19,7 @@ import GHC.Driver.Session import GHC.Core.Opt.WorkWrap.Utils import GHC.Types.Demand -- All of it import GHC.Core +import GHC.Core.Multiplicity ( scaledThing ) import GHC.Core.Seq ( seqBinds ) import GHC.Utils.Outputable import GHC.Types.Var.Env @@ -358,7 +359,7 @@ forcesRealWorld fam_envs ty | Just DataConAppContext{ dcac_dc = dc, dcac_arg_tys = field_tys } <- deepSplitProductType_maybe fam_envs ty , isUnboxedTupleCon dc - = any (\(ty,_) -> ty `eqType` realWorldStatePrimTy) field_tys + = any (\(ty,_) -> scaledThing ty `eqType` realWorldStatePrimTy) field_tys | otherwise = False diff --git a/compiler/GHC/Core/Opt/Exitify.hs b/compiler/GHC/Core/Opt/Exitify.hs index d903185c1d..5aa893e7b6 100644 --- a/compiler/GHC/Core/Opt/Exitify.hs +++ b/compiler/GHC/Core/Opt/Exitify.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE PatternSynonyms #-} + module GHC.Core.Opt.Exitify ( exitifyProgram ) where {- @@ -48,6 +50,7 @@ import GHC.Types.Var.Env import GHC.Core.FVs import GHC.Data.FastString import GHC.Core.Type +import GHC.Core.Multiplicity ( pattern Many ) import GHC.Utils.Misc( mapSnd ) import Data.Bifunctor @@ -265,7 +268,7 @@ mkExitJoinId in_scope ty join_arity = do `extendInScopeSet` exit_id_tmpl -- just cosmetics return (uniqAway avoid exit_id_tmpl) where - exit_id_tmpl = mkSysLocal (fsLit "exit") initExitJoinUnique ty + exit_id_tmpl = mkSysLocal (fsLit "exit") initExitJoinUnique Many ty `asJoinId` join_arity addExit :: InScopeSet -> JoinArity -> CoreExpr -> ExitifyM JoinId diff --git a/compiler/GHC/Core/Opt/FloatIn.hs b/compiler/GHC/Core/Opt/FloatIn.hs index ff63540ed1..03a84b872c 100644 --- a/compiler/GHC/Core/Opt/FloatIn.hs +++ b/compiler/GHC/Core/Opt/FloatIn.hs @@ -38,6 +38,7 @@ import GHC.Driver.Session import GHC.Utils.Outputable -- import Data.List ( mapAccumL ) import GHC.Types.Basic ( RecFlag(..), isRec ) +import GHC.Core.Multiplicity {- Top-level interface function, @floatInwards@. Note that we do not @@ -201,7 +202,7 @@ fiExpr platform to_drop ann_expr@(_,AnnApp {}) = (piResultTy fun_ty ty, extra_fvs) add_arg (fun_ty, extra_fvs) (arg_fvs, arg) - | noFloatIntoArg arg arg_ty + | noFloatIntoArg arg (irrelevantMult arg_ty) = (res_ty, extra_fvs `unionDVarSet` arg_fvs) | otherwise = (res_ty, extra_fvs) diff --git a/compiler/GHC/Core/Opt/OccurAnal.hs b/compiler/GHC/Core/Opt/OccurAnal.hs index af0e6aa5d6..156cb3df99 100644 --- a/compiler/GHC/Core/Opt/OccurAnal.hs +++ b/compiler/GHC/Core/Opt/OccurAnal.hs @@ -2066,7 +2066,8 @@ occAnalLamOrRhs env binders body env1 = env `addInScope` binders (env_body, binders') = oneShotGroup env1 binders -occAnalAlt :: OccEnv -> CoreAlt -> (UsageDetails, Alt IdWithOccInfo) +occAnalAlt :: OccEnv + -> CoreAlt -> (UsageDetails, Alt IdWithOccInfo) occAnalAlt env (con, bndrs, rhs) = case occAnal (env `addInScope` bndrs) rhs of { (rhs_usage1, rhs1) -> let @@ -2074,7 +2075,6 @@ occAnalAlt env (con, bndrs, rhs) in -- See Note [Binders in case alternatives] (alt_usg, (con, tagged_bndrs, rhs1)) } - {- ************************************************************************ * * diff --git a/compiler/GHC/Core/Opt/SetLevels.hs b/compiler/GHC/Core/Opt/SetLevels.hs index beecd424b6..bdd28d6a2f 100644 --- a/compiler/GHC/Core/Opt/SetLevels.hs +++ b/compiler/GHC/Core/Opt/SetLevels.hs @@ -47,9 +47,20 @@ The simplifier tries to get rid of occurrences of x, in favour of wild, in the hope that there will only be one remaining occurrence of x, namely the scrutinee of the case, and we can inline it. + + This can only work if @wild@ is an unrestricted binder. Indeed, even with the + extended typing rule (in the linter) for case expressions, if + case x of wild # 1 { p -> e} + is well-typed, then + case x of wild # 1 { p -> e[wild\x] } + is only well-typed if @e[wild\x] = e@ (that is, if @wild@ is not used in @e@ + at all). In which case, it is, of course, pointless to do the substitution + anyway. So for a linear binder (and really anything which isn't unrestricted), + doing this substitution would either produce ill-typed terms or be the + identity. -} -{-# LANGUAGE CPP, MultiWayIf #-} +{-# LANGUAGE CPP, MultiWayIf, PatternSynonyms #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module GHC.Core.Opt.SetLevels ( @@ -94,6 +105,7 @@ import GHC.Types.Name.Occurrence ( occNameString ) import GHC.Types.Unique ( hasKey ) import GHC.Core.Type ( Type, mkLamTypes, splitTyConApp_maybe, tyCoVarsOfType , mightBeUnliftedType, closeOverKindsDSet ) +import GHC.Core.Multiplicity ( pattern Many ) import GHC.Types.Basic ( Arity, RecFlag(..), isRec ) import GHC.Core.DataCon ( dataConOrigResTy ) import GHC.Builtin.Types @@ -477,6 +489,7 @@ lvlCase env scrut_fvs scrut' case_bndr ty alts , exprIsHNF (deTagExpr scrut') -- See Note [Check the output scrutinee for exprIsHNF] , not (isTopLvl dest_lvl) -- Can't have top-level cases , not (floatTopLvlOnly env) -- Can float anywhere + , Many <- idMult case_bndr -- See Note [Floating linear case] = -- Always float the case if possible -- Unlike lets we don't insist that it escapes a value lambda do { (env1, (case_bndr' : bs')) <- cloneCaseBndrs env dest_lvl (case_bndr : bs) @@ -548,6 +561,18 @@ Things to note: * We only do this with a single-alternative case +Note [Floating linear case] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Linear case can't be floated past case branches: + case u of { p1 -> case[1] v of { C x -> ...x...}; p2 -> ... } +Is well typed, but + case[1] v of { C x -> case u of { p1 -> ...x...; p2 -> ... }} +Will not be, because of how `x` is used in one alternative but not the other. + +It is not easy to float this linear cases precisely, so, instead, we elect, for +the moment, to simply not float linear case. + + Note [Setting levels when floating single-alternative cases] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Handling level-setting when floating a single-alternative case binding @@ -1579,6 +1604,7 @@ extendCaseBndrEnv :: LevelEnv -> LevelEnv extendCaseBndrEnv le@(LE { le_subst = subst, le_env = id_env }) case_bndr (Var scrut_var) + | Many <- varMult case_bndr = le { le_subst = extendSubstWithVar subst case_bndr scrut_var , le_env = add_id id_env (case_bndr, scrut_var) } extendCaseBndrEnv env _ _ = env @@ -1682,7 +1708,7 @@ newPolyBndrs dest_lvl mk_poly_bndr bndr uniq = transferPolyIdInfo bndr abs_vars $ -- Note [transferPolyIdInfo] in GHC.Types.Id transfer_join_info bndr $ - mkSysLocal (mkFastString str) uniq poly_ty + mkSysLocal (mkFastString str) uniq (idMult bndr) poly_ty where str = "poly_" ++ occNameString (getOccName bndr) poly_ty = mkLamTypes abs_vars (GHC.Core.Subst.substTy subst (idType bndr)) @@ -1717,7 +1743,7 @@ newLvlVar lvld_rhs join_arity_maybe is_mk_static = mkExportedVanillaId (mkSystemVarName uniq (mkFastString "static_ptr")) rhs_ty | otherwise - = mkSysLocal (mkFastString "lvl") uniq rhs_ty + = mkSysLocal (mkFastString "lvl") uniq Many rhs_ty -- | Clone the binders bound by a single-alternative case. cloneCaseBndrs :: LevelEnv -> Level -> [Var] -> LvlM (LevelEnv, [Var]) diff --git a/compiler/GHC/Core/Opt/Simplify.hs b/compiler/GHC/Core/Opt/Simplify.hs index 73f941c332..bf75a9de38 100644 --- a/compiler/GHC/Core/Opt/Simplify.hs +++ b/compiler/GHC/Core/Opt/Simplify.hs @@ -54,13 +54,15 @@ import GHC.Core.Rules ( lookupRule, getRules ) import GHC.Types.Basic import GHC.Utils.Monad ( mapAccumLM, liftIO ) import GHC.Types.Var ( isTyCoVar ) -import GHC.Data.Maybe ( orElse ) +import GHC.Data.Maybe ( orElse, fromMaybe ) import Control.Monad import GHC.Utils.Outputable import GHC.Data.FastString import GHC.Utils.Misc import GHC.Utils.Error import GHC.Unit.Module ( moduleName, pprModuleName ) +import GHC.Core.Multiplicity +import GHC.Core.TyCo.Rep ( TyCoBinder(..) ) import GHC.Builtin.PrimOps ( PrimOp (SeqOp) ) @@ -358,8 +360,44 @@ simplJoinBind :: SimplEnv simplJoinBind env cont old_bndr new_bndr rhs rhs_se = do { let rhs_env = rhs_se `setInScopeFromE` env ; rhs' <- simplJoinRhs rhs_env old_bndr rhs cont - ; completeBind env NotTopLevel (Just cont) old_bndr new_bndr rhs' } + ; let mult = contHoleScaling cont + arity = fromMaybe (pprPanic "simplJoinBind" (ppr new_bndr)) $ + isJoinIdDetails_maybe (idDetails new_bndr) + new_type = scaleJoinPointType mult arity (varType new_bndr) + new_bndr' = setIdType new_bndr new_type + ; completeBind env NotTopLevel (Just cont) old_bndr new_bndr' rhs' } +{- +Note [Scaling join point arguments] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider a join point which is linear in its variable, in some context E: + +E[join j :: a #-> a + j x = x + in case v of + A -> j 'x' + B -> <blah>] + +The simplifier changes to: + +join j :: a #-> a + j x = E[x] +in case v of + A -> j 'x' + B -> E[<blah>] + +If E uses its argument in a nonlinear way (e.g. a case['Many]), then +this is wrong: the join point has to change its type to a -> a. +Otherwise, we'd get a linearity error. + +See also Note [Return type for join points] and Note [Join points and case-of-case]. +-} +scaleJoinPointType :: Mult -> Int -> Type -> Type +scaleJoinPointType mult arity ty | arity == 0 = ty + | otherwise = case splitPiTy ty of + (binder, ty') -> mkPiTy (scaleBinder binder) (scaleJoinPointType mult (arity-1) ty') + where scaleBinder (Anon af t) = Anon af (scaleScaled mult t) + scaleBinder b@(Named _) = b -------------------------- simplNonRecX :: SimplEnv -> InId -- Old binder; not a JoinId @@ -664,7 +702,7 @@ makeTrivialBinding mode top_lvl occ_fs info expr expr_ty = do { (floats, expr1) <- prepareRhs mode top_lvl occ_fs expr ; uniq <- getUniqueM ; let name = mkSystemVarName uniq occ_fs - var = mkLocalIdWithInfo name expr_ty info + var = mkLocalIdWithInfo name Many expr_ty info -- Now something very like completeBind, -- but without the postInlineUnconditionally part @@ -968,8 +1006,8 @@ simplExprF env e cont simplExprF1 :: SimplEnv -> InExpr -> SimplCont -> SimplM (SimplFloats, OutExpr) -simplExprF1 _ (Type ty) _ - = pprPanic "simplExprF: type" (ppr ty) +simplExprF1 _ (Type ty) cont + = pprPanic "simplExprF: type" (ppr ty <+> text"cont: " <+> ppr cont) -- simplExprF does only with term-valued expressions -- The (Type ty) case is handled separately by simplExpr -- and by the other callers of simplExprF @@ -996,10 +1034,14 @@ simplExprF1 env (App fun arg) cont ApplyToTy { sc_arg_ty = arg' , sc_hole_ty = hole' , sc_cont = cont } } - _ -> simplExprF env fun $ + _ -> + let fun_ty = exprType fun + (Scaled m _, _) = splitFunTy fun_ty + in + simplExprF env fun $ ApplyToVal { sc_arg = arg, sc_env = env , sc_hole_ty = substTy env (exprType fun) - , sc_dup = NoDup, sc_cont = cont } + , sc_dup = NoDup, sc_cont = cont, sc_mult = m } simplExprF1 env expr@(Lam {}) cont = {-#SCC "simplExprF1-Lam" #-} @@ -1105,7 +1147,8 @@ simplJoinRhs :: SimplEnv -> InId -> InExpr -> SimplCont simplJoinRhs env bndr expr cont | Just arity <- isJoinId_maybe bndr = do { let (join_bndrs, join_body) = collectNBinders arity expr - ; (env', join_bndrs') <- simplLamBndrs env join_bndrs + mult = contHoleScaling cont + ; (env', join_bndrs') <- simplLamBndrs env (map (scaleIdBy mult) join_bndrs) ; join_body' <- simplExprC env' join_body cont ; return $ mkLams join_bndrs' join_body' } @@ -1303,8 +1346,8 @@ rebuild env expr cont Select { sc_bndr = bndr, sc_alts = alts, sc_env = se, sc_cont = cont } -> rebuildCase (se `setInScopeFromE` env) expr bndr alts cont - StrictArg { sc_fun = fun, sc_cont = cont, sc_fun_ty = fun_ty } - -> rebuildCall env (addValArgTo fun expr fun_ty ) cont + StrictArg { sc_fun = fun, sc_cont = cont, sc_fun_ty = fun_ty, sc_mult = m } + -> rebuildCall env (addValArgTo fun (m, expr) fun_ty ) cont StrictBind { sc_bndr = b, sc_bndrs = bs, sc_body = body , sc_env = se, sc_cont = cont } -> do { (floats1, env') <- simplNonRecX (se `setInScopeFromE` env) b expr @@ -1396,7 +1439,7 @@ simplCast env body co0 cont0 -- co1 :: t1 ~ s1 -- co2 :: s2 ~ t2 addCoerce co cont@(ApplyToVal { sc_arg = arg, sc_env = arg_se - , sc_dup = dup, sc_cont = tail }) + , sc_dup = dup, sc_cont = tail, sc_mult = m }) | Just (co1, m_co2) <- pushCoValArg co , let new_ty = coercionRKind co1 , not (isTypeLevPoly new_ty) -- Without this check, we get a lev-poly arg @@ -1419,7 +1462,8 @@ simplCast env body co0 cont0 , sc_env = arg_se' , sc_dup = dup' , sc_cont = tail' - , sc_hole_ty = coercionLKind co }) } } + , sc_hole_ty = coercionLKind co + , sc_mult = m }) } } addCoerce co cont | isReflexiveCo co = return cont -- Having this at the end makes a huge @@ -1953,16 +1997,17 @@ rebuildCall env info (ApplyToTy { sc_arg_ty = arg_ty, sc_hole_ty = hole_ty, sc_c -- runRW# :: forall (r :: RuntimeRep) (o :: TYPE r). (State# RealWorld -> o) -> o -- K[ runRW# rr ty body ] --> runRW rr' ty' (\s. K[ body s ]) rebuildCall env (ArgInfo { ai_fun = fun, ai_args = rev_args }) - (ApplyToVal { sc_arg = arg, sc_env = arg_se, sc_cont = cont }) + (ApplyToVal { sc_arg = arg, sc_env = arg_se, sc_cont = cont, sc_mult = m }) | fun `hasKey` runRWKey , not (contIsStop cont) -- Don't fiddle around if the continuation is boring , [ TyArg {}, TyArg {} ] <- rev_args - = do { s <- newId (fsLit "s") realWorldStatePrimTy + = do { s <- newId (fsLit "s") Many realWorldStatePrimTy ; let env' = (arg_se `setInScopeFromE` env) `addNewInScopeIds` [s] ty' = contResultType cont cont' = ApplyToVal { sc_dup = Simplified, sc_arg = Var s , sc_env = env', sc_cont = cont - , sc_hole_ty = mkVisFunTy realWorldStatePrimTy ty' } + , sc_hole_ty = mkVisFunTy m realWorldStatePrimTy ty' + , sc_mult = m } -- cont' applies to s, then K ; body' <- simplExprC env' arg cont' ; let arg' = Lam s body' @@ -1974,10 +2019,10 @@ rebuildCall env info@(ArgInfo { ai_encl = encl_rules , ai_strs = str:strs, ai_discs = disc:discs }) (ApplyToVal { sc_arg = arg, sc_env = arg_se , sc_dup = dup_flag, sc_hole_ty = fun_ty - , sc_cont = cont }) + , sc_cont = cont, sc_mult = m }) -- Argument is already simplified | isSimplified dup_flag -- See Note [Avoid redundant simplification] - = rebuildCall env (addValArgTo info' arg fun_ty) cont + = rebuildCall env (addValArgTo info' (m, arg) fun_ty) cont -- Strict arguments | str @@ -1986,7 +2031,7 @@ rebuildCall env info@(ArgInfo { ai_encl = encl_rules simplExprF (arg_se `setInScopeFromE` env) arg (StrictArg { sc_fun = info', sc_cci = cci_strict , sc_dup = Simplified, sc_fun_ty = fun_ty - , sc_cont = cont }) + , sc_cont = cont, sc_mult = m }) -- Note [Shadowing] -- Lazy arguments @@ -1997,7 +2042,7 @@ rebuildCall env info@(ArgInfo { ai_encl = encl_rules -- floating a demanded let. = do { arg' <- simplExprC (arg_se `setInScopeFromE` env) arg (mkLazyArgStop arg_ty cci_lazy) - ; rebuildCall env (addValArgTo info' arg' fun_ty) cont } + ; rebuildCall env (addValArgTo info' (m, arg') fun_ty) cont } where info' = info { ai_strs = strs, ai_discs = discs } arg_ty = funArgTy fun_ty @@ -2219,10 +2264,25 @@ trySeqRules in_env scrut rhs cont , TyArg { as_arg_ty = rhs_ty , as_hole_ty = res2_ty } , ValArg { as_arg = no_cast_scrut - , as_hole_ty = res3_ty } ] + , as_hole_ty = res3_ty + , as_mult = Many } ] + -- The multiplicity of the scrutiny above is Many because the type + -- of seq requires that its first argument is unrestricted. The + -- typing rule of case also guarantees it though. In a more + -- general world, where the first argument of seq would have + -- affine multiplicity, then we could use the multiplicity of + -- the case (held in the case binder) instead. rule_cont = ApplyToVal { sc_dup = NoDup, sc_arg = rhs , sc_env = in_env, sc_cont = cont - , sc_hole_ty = res4_ty } + , sc_hole_ty = res4_ty, sc_mult = Many } + -- The multiplicity in sc_mult above is the + -- multiplicity of the second argument of seq. Since + -- seq's type, as it stands, imposes that its second + -- argument be unrestricted, so is + -- sc_mult. However, a more precise typing rule, + -- for seq, would be to have it be linear. In which + -- case, sc_mult should be 1. + -- Lazily evaluated, so we don't do most of this drop_casts (Cast e _) = drop_casts e @@ -2575,13 +2635,14 @@ rebuildCase env scrut case_bndr alts cont -- as well as when it's an explicit constructor application , let env0 = setInScopeSet env in_scope' = do { tick (KnownBranch case_bndr) + ; let scaled_wfloats = map scale_float wfloats ; case findAlt (DataAlt con) alts of Nothing -> missingAlt env0 case_bndr alts cont Just (DEFAULT, bs, rhs) -> let con_app = Var (dataConWorkId con) `mkTyApps` ty_args `mkApps` other_args - in simple_rhs env0 wfloats con_app bs rhs - Just (_, bs, rhs) -> knownCon env0 scrut wfloats con ty_args other_args + in simple_rhs env0 scaled_wfloats con_app bs rhs + Just (_, bs, rhs) -> knownCon env0 scrut scaled_wfloats con ty_args other_args case_bndr bs rhs cont } where @@ -2599,6 +2660,31 @@ rebuildCase env scrut case_bndr alts cont GHC.Core.Make.wrapFloats wfloats $ wrapFloats (floats1 `addFloats` floats2) expr' )} + -- This scales case floats by the multiplicity of the continuation hole (see + -- Note [Scaling in case-of-case]). Let floats are _not_ scaled, because + -- they are aliases anyway. + scale_float (GHC.Core.Make.FloatCase scrut case_bndr con vars) = + let + scale_id id = scaleIdBy holeScaling id + in + GHC.Core.Make.FloatCase scrut (scale_id case_bndr) con (map scale_id vars) + scale_float f = f + + holeScaling = contHoleScaling cont `mkMultMul` idMult case_bndr + -- We are in the following situation + -- case[p] case[q] u of { D x -> C v } of { C x -> w } + -- And we are producing case[??] u of { D x -> w[x\v]} + -- + -- What should the multiplicity `??` be? In order to preserve the usage of + -- variables in `u`, it needs to be `pq`. + -- + -- As an illustration, consider the following + -- case[Many] case[1] of { C x -> C x } of { C x -> (x, x) } + -- Where C :: A #-> T is linear + -- If we were to produce a case[1], like the inner case, we would get + -- case[1] of { C x -> (x, x) } + -- Which is ill-typed with respect to linearity. So it needs to be a + -- case[Many]. -------------------------------------------------- -- 2. Eliminate the case if scrutinee is evaluated @@ -2680,8 +2766,11 @@ reallyRebuildCase env scrut case_bndr alts cont | otherwise = do { (floats, cont') <- mkDupableCaseCont env alts cont ; case_expr <- simplAlts (env `setInScopeFromF` floats) - scrut case_bndr alts cont' + scrut (scaleIdBy holeScaling case_bndr) (scaleAltsBy holeScaling alts) cont' ; return (floats, case_expr) } + where + holeScaling = contHoleScaling cont + -- Note [Scaling in case-of-case] {- simplCaseBinder checks whether the scrutinee is a variable, v. If so, @@ -2760,6 +2849,39 @@ taking advantage of the `seq`. At one point I did transformation in LiberateCase, but it's more robust here. (Otherwise, there's a danger that we'll simply drop the 'seq' altogether, before LiberateCase gets to see it.) + +Note [Scaling in case-of-case] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +When two cases commute, if done naively, the multiplicities will be wrong: + + case (case u of w[1] { (x[1], y[1]) } -> f x y) of w'[Many] + { (z[Many], t[Many]) -> z + } + +The multiplicities here, are correct, but if I perform a case of case: + + case u of w[1] + { (x[1], y[1]) -> case f x y of w'[Many] of { (z[Many], t[Many]) -> z } + } + +This is wrong! Using `f x y` inside a `case … of w'[Many]` means that `x` and +`y` must have multiplicities `Many` not `1`! The correct solution is to make +all the `1`-s be `Many`-s instead: + + case u of w[Many] + { (x[Many], y[Many]) -> case f x y of w'[Many] of { (z[Many], t[Many]) -> z } + } + +In general, when commuting two cases, the rule has to be: + + case (case … of x[p] {…}) of y[q] { … } + ===> case … of x[p*q] { … case … of y[q] { … } } + +This is materialised, in the simplifier, by the fact that every time we simplify +case alternatives with a continuation (the surrounded case (or more!)), we must +scale the entire case we are simplifying, by a scaling factor which can be +computed in the continuation (with function `contHoleScaling`). -} simplAlts :: SimplEnv @@ -2802,7 +2924,7 @@ improveSeq :: (FamInstEnv, FamInstEnv) -> SimplEnv -- Note [Improving seq] improveSeq fam_envs env scrut case_bndr case_bndr1 [(DEFAULT,_,_)] | Just (co, ty2) <- topNormaliseType_maybe fam_envs (idType case_bndr1) - = do { case_bndr2 <- newId (fsLit "nt") ty2 + = do { case_bndr2 <- newId (fsLit "nt") Many ty2 ; let rhs = DoneEx (Var case_bndr2 `Cast` mkSymCo co) Nothing env2 = extendIdSubst env case_bndr rhs ; return (env2, scrut `Cast` co, case_bndr2) } @@ -2924,11 +3046,12 @@ addAltUnfoldings env scrut case_bndr con_app env1 = addBinderUnfolding env case_bndr con_app_unf -- See Note [Add unfolding for scrutinee] - env2 = case scrut of + env2 | Many <- idMult case_bndr = case scrut of Just (Var v) -> addBinderUnfolding env1 v con_app_unf Just (Cast (Var v) co) -> addBinderUnfolding env1 v $ mk_simple_unf (Cast con_app (mkSymCo co)) _ -> env1 + | otherwise = env1 ; traceSmpl "addAltUnf" (vcat [ppr case_bndr <+> ppr scrut, ppr con_app]) ; return env2 } @@ -3003,6 +3126,9 @@ piece of information. So instead we add the unfolding x -> Just a, and x -> Nothing in the respective RHSs. +Since this transformation is tantamount to a binder swap, the same caveat as in +Note [Suppressing binder-swaps on linear case] in OccurAnal apply. + ************************************************************************ * * @@ -3213,7 +3339,7 @@ mkDupableCont env (StrictBind { sc_bndr = bndr, sc_bndrs = bndrs , sc_cont = mkBoringStop res_ty } ) } mkDupableCont env (StrictArg { sc_fun = info, sc_cci = cci - , sc_cont = cont, sc_fun_ty = fun_ty }) + , sc_cont = cont, sc_fun_ty = fun_ty, sc_mult = m }) -- See Note [Duplicating StrictArg] -- NB: sc_dup /= OkToDup; that is caught earlier by contIsDupable = do { (floats1, cont') <- mkDupableCont env cont @@ -3224,6 +3350,7 @@ mkDupableCont env (StrictArg { sc_fun = info, sc_cci = cci , sc_cont = cont' , sc_cci = cci , sc_fun_ty = fun_ty + , sc_mult = m , sc_dup = OkToDup} ) } mkDupableCont env (ApplyToTy { sc_cont = cont @@ -3234,7 +3361,7 @@ mkDupableCont env (ApplyToTy { sc_cont = cont mkDupableCont env (ApplyToVal { sc_arg = arg, sc_dup = dup , sc_env = se, sc_cont = cont - , sc_hole_ty = hole_ty }) + , sc_hole_ty = hole_ty, sc_mult = mult }) = -- e.g. [...hole...] (...arg...) -- ==> -- let a = ...arg... @@ -3253,7 +3380,7 @@ mkDupableCont env (ApplyToVal { sc_arg = arg, sc_dup = dup -- has turned arg'' into a fresh variable -- See Note [StaticEnv invariant] in GHC.Core.Opt.Simplify.Utils , sc_dup = OkToDup, sc_cont = cont' - , sc_hole_ty = hole_ty }) } + , sc_hole_ty = hole_ty, sc_mult = mult }) } mkDupableCont env (Select { sc_bndr = case_bndr, sc_alts = alts , sc_env = se, sc_cont = cont }) @@ -3269,8 +3396,10 @@ mkDupableCont env (Select { sc_bndr = case_bndr, sc_alts = alts -- And this is important: see Note [Fusing case continuations] ; let alt_env = se `setInScopeFromF` floats - ; (alt_env', case_bndr') <- simplBinder alt_env case_bndr - ; alts' <- mapM (simplAlt alt_env' Nothing [] case_bndr' alt_cont) alts + ; let cont_scaling = contHoleScaling cont + -- See Note [Scaling in case-of-case] + ; (alt_env', case_bndr') <- simplBinder alt_env (scaleIdBy cont_scaling case_bndr) + ; alts' <- mapM (simplAlt alt_env' Nothing [] case_bndr' alt_cont) (scaleAltsBy cont_scaling alts) -- Safe to say that there are no handled-cons for the DEFAULT case -- NB: simplBinder does not zap deadness occ-info, so -- a dead case_bndr' will still advertise its deadness diff --git a/compiler/GHC/Core/Opt/Simplify/Env.hs b/compiler/GHC/Core/Opt/Simplify/Env.hs index 4a749e8951..5c8e0f21c2 100644 --- a/compiler/GHC/Core/Opt/Simplify/Env.hs +++ b/compiler/GHC/Core/Opt/Simplify/Env.hs @@ -63,6 +63,7 @@ import qualified GHC.Core.Type as Type import GHC.Core.Type hiding ( substTy, substTyVar, substTyVarBndr, extendTvSubst, extendCvSubst ) import qualified GHC.Core.Coercion as Coercion import GHC.Core.Coercion hiding ( substCo, substCoVar, substCoVarBndr ) +import GHC.Core.Multiplicity import GHC.Types.Basic import GHC.Utils.Monad import GHC.Utils.Outputable @@ -276,7 +277,7 @@ mkSimplEnv mode -- The top level "enclosing CC" is "SUBSUMED". init_in_scope :: InScopeSet -init_in_scope = mkInScopeSet (unitVarSet (mkWildValBinder unitTy)) +init_in_scope = mkInScopeSet (unitVarSet (mkWildValBinder Many unitTy)) -- See Note [WildCard binders] {- @@ -724,6 +725,8 @@ changed!! That's why we pass res_ty into simplNonRecJoinBndr, and substIdBndr takes a (Just res_ty) argument so that it knows to do the type-changing thing. + +See also Note [Scaling join point arguments]. -} simplBinders :: SimplEnv -> [InBndr] -> SimplM (SimplEnv, [OutBndr]) @@ -927,12 +930,15 @@ substCo env co = Coercion.substCo (getTCvSubst env) co ------------------ substIdType :: SimplEnv -> Id -> Id substIdType (SimplEnv { seInScope = in_scope, seTvSubst = tv_env, seCvSubst = cv_env }) id - | (isEmptyVarEnv tv_env && isEmptyVarEnv cv_env) - || noFreeVarsOfType old_ty + | (isEmptyVarEnv tv_env && isEmptyVarEnv cv_env) + || no_free_vars = id - | otherwise = Id.setIdType id (Type.substTy (TCvSubst in_scope tv_env cv_env) old_ty) + | otherwise = Id.updateIdTypeAndMult (Type.substTyUnchecked subst) id -- The tyCoVarsOfType is cheaper than it looks -- because we cache the free tyvars of the type -- in a Note in the id's type itself where + no_free_vars = noFreeVarsOfType old_ty && noFreeVarsOfType old_w + subst = TCvSubst in_scope tv_env cv_env old_ty = idType id + old_w = varMult id diff --git a/compiler/GHC/Core/Opt/Simplify/Monad.hs b/compiler/GHC/Core/Opt/Simplify/Monad.hs index d0096e1a7e..b84ed1028f 100644 --- a/compiler/GHC/Core/Opt/Simplify/Monad.hs +++ b/compiler/GHC/Core/Opt/Simplify/Monad.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE PatternSynonyms #-} {- (c) The AQUA Project, Glasgow University, 1993-1998 @@ -26,7 +27,7 @@ import GHC.Types.Var ( Var, isId, mkLocalVar ) import GHC.Types.Name ( mkSystemVarName ) import GHC.Types.Id ( Id, mkSysLocalOrCoVar ) import GHC.Types.Id.Info ( IdDetails(..), vanillaIdInfo, setArityInfo ) -import GHC.Core.Type ( Type, mkLamTypes ) +import GHC.Core.Type ( Type, mkLamTypes, Mult ) import GHC.Core.FamInstEnv ( FamInstEnv ) import GHC.Core ( RuleEnv(..) ) import GHC.Types.Unique.Supply @@ -40,6 +41,7 @@ import GHC.Utils.Misc ( count ) import GHC.Utils.Panic (throwGhcExceptionIO, GhcException (..)) import GHC.Types.Basic ( IntWithInf, treatZeroAsInf, mkIntWithInf ) import Control.Monad ( ap ) +import GHC.Core.Multiplicity ( pattern Many ) {- ************************************************************************ @@ -180,9 +182,9 @@ getSimplRules = SM (\st_env us sc -> return (st_rules st_env, us, sc)) getFamEnvs :: SimplM (FamInstEnv, FamInstEnv) getFamEnvs = SM (\st_env us sc -> return (st_fams st_env, us, sc)) -newId :: FastString -> Type -> SimplM Id -newId fs ty = do uniq <- getUniqueM - return (mkSysLocalOrCoVar fs uniq ty) +newId :: FastString -> Mult -> Type -> SimplM Id +newId fs w ty = do uniq <- getUniqueM + return (mkSysLocalOrCoVar fs uniq w ty) newJoinId :: [Var] -> Type -> SimplM Id newJoinId bndrs body_ty @@ -196,7 +198,7 @@ newJoinId bndrs body_ty id_info = vanillaIdInfo `setArityInfo` arity -- `setOccInfo` strongLoopBreaker - ; return (mkLocalVar details name join_id_ty id_info) } + ; return (mkLocalVar details name Many join_id_ty id_info) } {- ************************************************************************ diff --git a/compiler/GHC/Core/Opt/Simplify/Utils.hs b/compiler/GHC/Core/Opt/Simplify/Utils.hs index 5878445d44..c1cb4c9f3f 100644 --- a/compiler/GHC/Core/Opt/Simplify/Utils.hs +++ b/compiler/GHC/Core/Opt/Simplify/Utils.hs @@ -19,7 +19,7 @@ module GHC.Core.Opt.Simplify.Utils ( -- The continuation type SimplCont(..), DupFlag(..), StaticEnv, isSimplified, contIsStop, - contIsDupable, contResultType, contHoleType, + contIsDupable, contResultType, contHoleType, contHoleScaling, contIsTrivial, contArgs, countArgs, mkBoringStop, mkRhsStop, mkLazyArgStop, contIsRhsOrArg, @@ -62,6 +62,7 @@ import GHC.Core.Opt.Simplify.Monad import GHC.Core.Type hiding( substTy ) import GHC.Core.Coercion hiding( substCo ) import GHC.Core.DataCon ( dataConWorkId, isNullaryRepDataCon ) +import GHC.Core.Multiplicity import GHC.Utils.Misc import GHC.Data.OrdList ( isNilOL ) import GHC.Utils.Monad @@ -123,7 +124,8 @@ data SimplCont -- See Note [The hole type in ApplyToTy/Val] , sc_arg :: InExpr -- The argument, , sc_env :: StaticEnv -- see Note [StaticEnv invariant] - , sc_cont :: SimplCont } + , sc_cont :: SimplCont + , sc_mult :: Mult } | ApplyToTy -- (ApplyToTy ty K)[e] = K[ e ty ] { sc_arg_ty :: OutType -- Argument type @@ -156,7 +158,8 @@ data SimplCont , sc_fun_ty :: OutType -- Type of the function (f e1 .. en), -- presumably (arg_ty -> res_ty) -- where res_ty is expected by sc_cont - , sc_cont :: SimplCont } + , sc_cont :: SimplCont + , sc_mult :: Mult } | TickIt -- (TickIt t K)[e] = K[ tick t e ] (Tickish Id) -- Tick tickish <hole> @@ -274,22 +277,23 @@ data ArgInfo } data ArgSpec - = ValArg { as_arg :: OutExpr -- Apply to this (coercion or value); c.f. ApplyToVal + = ValArg { as_mult :: Mult + , as_arg :: OutExpr -- Apply to this (coercion or value); c.f. ApplyToVal , as_hole_ty :: OutType } -- Type of the function (presumably t1 -> t2) | TyArg { as_arg_ty :: OutType -- Apply to this type; c.f. ApplyToTy , as_hole_ty :: OutType } -- Type of the function (presumably forall a. blah) | CastBy OutCoercion -- Cast by this; c.f. CastIt instance Outputable ArgSpec where - ppr (ValArg { as_arg = arg }) = text "ValArg" <+> ppr arg + ppr (ValArg { as_mult = mult, as_arg = arg }) = text "ValArg" <+> ppr mult <+> ppr arg ppr (TyArg { as_arg_ty = ty }) = text "TyArg" <+> ppr ty ppr (CastBy c) = text "CastBy" <+> ppr c -addValArgTo :: ArgInfo -> OutExpr -> OutType -> ArgInfo -addValArgTo ai arg hole_ty = ai { ai_args = arg_spec : ai_args ai - , ai_rules = decRules (ai_rules ai) } +addValArgTo :: ArgInfo -> (Mult, OutExpr) -> OutType -> ArgInfo +addValArgTo ai (w, arg) hole_ty = ai { ai_args = arg_spec : ai_args ai + , ai_rules = decRules (ai_rules ai) } where - arg_spec = ValArg { as_arg = arg, as_hole_ty = hole_ty } + arg_spec = ValArg { as_arg = arg, as_hole_ty = hole_ty, as_mult = w } addTyArgTo :: ArgInfo -> OutType -> OutType -> ArgInfo addTyArgTo ai arg_ty hole_ty = ai { ai_args = arg_spec : ai_args ai @@ -312,9 +316,9 @@ pushSimplifiedArgs env (arg : args) k = case arg of TyArg { as_arg_ty = arg_ty, as_hole_ty = hole_ty } -> ApplyToTy { sc_arg_ty = arg_ty, sc_hole_ty = hole_ty, sc_cont = rest } - ValArg { as_arg = arg, as_hole_ty = hole_ty } + ValArg { as_arg = arg, as_hole_ty = hole_ty, as_mult = w } -> ApplyToVal { sc_arg = arg, sc_env = env, sc_dup = Simplified - , sc_hole_ty = hole_ty, sc_cont = rest } + , sc_hole_ty = hole_ty, sc_cont = rest, sc_mult = w } CastBy c -> CastIt c rest where rest = pushSimplifiedArgs env args k @@ -413,12 +417,33 @@ contHoleType (TickIt _ k) = contHoleType k contHoleType (CastIt co _) = coercionLKind co contHoleType (StrictBind { sc_bndr = b, sc_dup = dup, sc_env = se }) = perhapsSubstTy dup se (idType b) -contHoleType (StrictArg { sc_fun_ty = ty }) = funArgTy ty -contHoleType (ApplyToTy { sc_hole_ty = ty }) = ty -- See Note [The hole type in ApplyToTy/Val] +contHoleType (StrictArg { sc_fun_ty = ty, sc_mult = _m }) = funArgTy ty +contHoleType (ApplyToTy { sc_hole_ty = ty }) = ty -- See Note [The hole type in ApplyToTy] contHoleType (ApplyToVal { sc_hole_ty = ty }) = ty -- See Note [The hole type in ApplyToTy/Val] contHoleType (Select { sc_dup = d, sc_bndr = b, sc_env = se }) = perhapsSubstTy d se (idType b) + +-- Computes the multiplicity scaling factor at the hole. That is, in (case [] of +-- x ::(p) _ { … }) (respectively for arguments of functions), the scaling +-- factor is p. And in E[G[]], the scaling factor is the product of the scaling +-- factor of E and that of G. +-- +-- The scaling factor at the hole of E[] is used to determine how a binder +-- should be scaled if it commutes with E. This appears, in particular, in the +-- case-of-case transformation. +contHoleScaling :: SimplCont -> Mult +contHoleScaling (Stop _ _) = One +contHoleScaling (CastIt _ k) = contHoleScaling k +contHoleScaling (StrictBind { sc_bndr = id, sc_cont = k }) = + (idMult id) `mkMultMul` contHoleScaling k +contHoleScaling (StrictArg { sc_mult = w, sc_cont = k }) = + w `mkMultMul` contHoleScaling k +contHoleScaling (Select { sc_bndr = id, sc_cont = k }) = + (idMult id) `mkMultMul` contHoleScaling k +contHoleScaling (ApplyToTy { sc_cont = k }) = contHoleScaling k +contHoleScaling (ApplyToVal { sc_cont = k }) = contHoleScaling k +contHoleScaling (TickIt _ k) = contHoleScaling k ------------------- countArgs :: SimplCont -> Int -- Count all arguments, including types, coercions, and other values @@ -521,7 +546,7 @@ mkArgInfo env fun rules n_val_args call_cont add_type_str _ [] = [] add_type_str fun_ty all_strs@(str:strs) - | Just (arg_ty, fun_ty') <- splitFunTy_maybe fun_ty -- Add strict-type info + | Just (Scaled _ arg_ty, fun_ty') <- splitFunTy_maybe fun_ty -- Add strict-type info = (str || Just False == isLiftedType_maybe arg_ty) : add_type_str fun_ty' strs -- If the type is levity-polymorphic, we can't know whether it's @@ -1831,7 +1856,7 @@ abstractFloats dflags top_lvl main_tvs floats body ; let poly_name = setNameUnique (idName var) uniq -- Keep same name poly_ty = mkInfForAllTys tvs_here (idType var) -- But new type of course poly_id = transferPolyIdInfo var tvs_here $ -- Note [transferPolyIdInfo] in GHC.Types.Id - mkLocalId poly_name poly_ty + mkLocalId poly_name (idMult var) poly_ty ; return (poly_id, mkTyApps (Var poly_id) (mkTyVarTys tvs_here)) } -- In the olden days, it was crucial to copy the occInfo of the original var, -- because we were looking at occurrence-analysed but as yet unsimplified code! @@ -1953,7 +1978,10 @@ prepareAlts scrut case_bndr' alts -- Test simpl013 is an example = do { us <- getUniquesM ; let (idcs1, alts1) = filterAlts tc tys imposs_cons alts - (yes2, alts2) = refineDefaultAlt us tc tys idcs1 alts1 + (yes2, alts2) = refineDefaultAlt us (idMult case_bndr') tc tys idcs1 alts1 + -- the multiplicity on case_bndr's is the multiplicity of the + -- case expression The newly introduced patterns in + -- refineDefaultAlt must be scaled by this multiplicity (yes3, idcs3, alts3) = combineIdenticalAlts idcs1 alts2 -- "idcs" stands for "impossible default data constructors" -- i.e. the constructors that can't match the default case @@ -2184,7 +2212,7 @@ mkCase2 dflags scrut bndr alts_ty alts _ -> True , gopt Opt_CaseFolding dflags , Just (scrut', tx_con, mk_orig) <- caseRules (targetPlatform dflags) scrut - = do { bndr' <- newId (fsLit "lwild") (exprType scrut') + = do { bndr' <- newId (fsLit "lwild") Many (exprType scrut') ; alts' <- mapMaybeM (tx_alt tx_con mk_orig bndr') alts -- mapMaybeM: discard unreachable alternatives @@ -2235,7 +2263,7 @@ mkCase2 dflags scrut bndr alts_ty alts = -- For non-nullary data cons we must invent some fake binders -- See Note [caseRules for dataToTag] in GHC.Core.Opt.ConstantFold do { us <- getUniquesM - ; let (ex_tvs, arg_ids) = dataConRepInstPat us dc + ; let (ex_tvs, arg_ids) = dataConRepInstPat us (idMult new_bndr) dc (tyConAppArgs (idType new_bndr)) ; return (ex_tvs ++ arg_ids) } mk_new_bndrs _ _ = return [] diff --git a/compiler/GHC/Core/Opt/SpecConstr.hs b/compiler/GHC/Core/Opt/SpecConstr.hs index da8aaa3447..c3135de28f 100644 --- a/compiler/GHC/Core/Opt/SpecConstr.hs +++ b/compiler/GHC/Core/Opt/SpecConstr.hs @@ -32,6 +32,7 @@ import GHC.Core.Coercion hiding( substCo ) import GHC.Core.Rules import GHC.Core.Type hiding ( substTy ) import GHC.Core.TyCon ( tyConName ) +import GHC.Core.Multiplicity import GHC.Types.Id import GHC.Core.Ppr ( pprParendExpr ) import GHC.Core.Make ( mkImpossibleExpr ) @@ -969,7 +970,7 @@ forceSpecBndr :: ScEnv -> Var -> Bool forceSpecBndr env var = forceSpecFunTy env . snd . splitForAllTys . varType $ var forceSpecFunTy :: ScEnv -> Type -> Bool -forceSpecFunTy env = any (forceSpecArgTy env) . fst . splitFunTys +forceSpecFunTy env = any (forceSpecArgTy env) . map scaledThing . fst . splitFunTys forceSpecArgTy :: ScEnv -> Type -> Bool forceSpecArgTy env ty @@ -1675,7 +1676,7 @@ spec_one env fn arg_bndrs body (call_pat@(qvars, pats), rule_number) spec_join_arity | isJoinId fn = Just (length spec_lam_args) | otherwise = Nothing - spec_id = mkLocalId spec_name + spec_id = mkLocalId spec_name Many (mkLamTypes spec_lam_args body_ty) -- See Note [Transfer strictness] `setIdStrictness` spec_str @@ -2052,7 +2053,7 @@ callToPats env bndr_occs call@(Call _ args con_env) -- The kind of a type variable may mention a kind variable -- and the type of a term variable may mention a type variable - sanitise id = id `setIdType` expandTypeSynonyms (idType id) + sanitise id = updateIdTypeAndMult expandTypeSynonyms id -- See Note [Free type variables of the qvar types] -- Bad coercion variables: see Note [SpecConstr and casts] @@ -2212,7 +2213,7 @@ argToPat _env _in_scope _val_env arg _arg_occ wildCardPat :: Type -> UniqSM (Bool, CoreArg) wildCardPat ty = do { uniq <- getUniqueM - ; let id = mkSysLocalOrCoVar (fsLit "sc") uniq ty + ; let id = mkSysLocalOrCoVar (fsLit "sc") uniq Many ty ; return (False, varToCoreExpr id) } argsToPats :: ScEnv -> InScopeSet -> ValueEnv diff --git a/compiler/GHC/Core/Opt/Specialise.hs b/compiler/GHC/Core/Opt/Specialise.hs index 44cfc460dd..ae3d1cb287 100644 --- a/compiler/GHC/Core/Opt/Specialise.hs +++ b/compiler/GHC/Core/Opt/Specialise.hs @@ -5,6 +5,7 @@ -} {-# LANGUAGE CPP #-} +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE ViewPatterns #-} @@ -18,6 +19,7 @@ import GHC.Prelude import GHC.Types.Id import GHC.Tc.Utils.TcType hiding( substTy ) import GHC.Core.Type hiding( substTy, extendTvSubstList ) +import GHC.Core.Multiplicity import GHC.Core.Predicate import GHC.Unit.Module( Module, HasModule(..) ) import GHC.Core.Coercion( Coercion ) @@ -1130,9 +1132,10 @@ specCase env scrut' case_bndr [(con, args, rhs)] sc_args' = filter is_flt_sc_arg args' clone_me bndr = do { uniq <- getUniqueM - ; return (mkUserLocalOrCoVar occ uniq ty loc) } + ; return (mkUserLocalOrCoVar occ uniq wght ty loc) } where name = idName bndr + wght = idMult bndr ty = idType bndr occ = nameOccName name loc = getSrcSpan name @@ -1423,7 +1426,7 @@ specCalls mb_mod env existing_rules calls_for_me fn rhs (spec_bndrs, spec_rhs, spec_fn_ty) | add_void_arg = ( voidPrimId : spec_bndrs1 , Lam voidArgId spec_rhs1 - , mkVisFunTy voidPrimTy spec_fn_ty1) + , mkVisFunTyMany voidPrimTy spec_fn_ty1) | otherwise = (spec_bndrs1, spec_rhs1, spec_fn_ty1) join_arity_decr = length rule_lhs_args - length spec_bndrs @@ -2504,7 +2507,7 @@ mkCallUDs' env f args -- we decide on a case by case basis if we want to specialise -- on this argument; if so, SpecDict, if not UnspecArg mk_spec_arg arg (Anon InvisArg pred) - | type_determines_value pred + | type_determines_value (scaledThing pred) , interestingDict env arg -- Note [Interesting dictionary arguments] = SpecDict arg | otherwise = UnspecArg @@ -2890,7 +2893,7 @@ newDictBndr :: SpecEnv -> CoreBndr -> SpecM CoreBndr newDictBndr env b = do { uniq <- getUniqueM ; let n = idName b ty' = substTy env (idType b) - ; return (mkUserLocal (nameOccName n) uniq ty' (getSrcSpan n)) } + ; return (mkUserLocal (nameOccName n) uniq Many ty' (getSrcSpan n)) } newSpecIdSM :: Id -> Type -> Maybe JoinArity -> SpecM Id -- Give the new Id a similar occurrence name to the old one @@ -2898,7 +2901,7 @@ newSpecIdSM old_id new_ty join_arity_maybe = do { uniq <- getUniqueM ; let name = idName old_id new_occ = mkSpecOcc (nameOccName name) - new_id = mkUserLocal new_occ uniq new_ty (getSrcSpan name) + new_id = mkUserLocal new_occ uniq Many new_ty (getSrcSpan name) `asJoinId_maybe` join_arity_maybe ; return new_id } diff --git a/compiler/GHC/Core/Opt/StaticArgs.hs b/compiler/GHC/Core/Opt/StaticArgs.hs index 827a3e90a5..dd015924e3 100644 --- a/compiler/GHC/Core/Opt/StaticArgs.hs +++ b/compiler/GHC/Core/Opt/StaticArgs.hs @@ -48,7 +48,7 @@ The previous patch, to fix polymorphic floatout demand signatures, is essential to make this work well! -} -{-# LANGUAGE CPP #-} +{-# LANGUAGE CPP, PatternSynonyms #-} module GHC.Core.Opt.StaticArgs ( doStaticArgs ) where import GHC.Prelude @@ -56,6 +56,7 @@ import GHC.Prelude import GHC.Types.Var import GHC.Core import GHC.Core.Utils +import GHC.Core.Multiplicity ( pattern Many ) import GHC.Core.Type import GHC.Core.Coercion import GHC.Types.Id @@ -420,12 +421,13 @@ saTransform binder arg_staticness rhs_binders rhs_body shadow_rhs = mkLams shadow_lam_bndrs local_body -- nonrec_rhs = \alpha' beta' c n xs -> sat_worker xs - rec_body_bndr = mkSysLocal (fsLit "sat_worker") uniq (exprType rec_body) + rec_body_bndr = mkSysLocal (fsLit "sat_worker") uniq Many (exprType rec_body) -- rec_body_bndr = sat_worker -- See Note [Shadow binding]; make a SysLocal shadow_bndr = mkSysLocal (occNameFS (getOccName binder)) (idUnique binder) + Many (exprType shadow_rhs) isStaticValue :: Staticness App -> Bool diff --git a/compiler/GHC/Core/Opt/WorkWrap/Utils.hs b/compiler/GHC/Core/Opt/WorkWrap/Utils.hs index 4c4a5ced8a..9da3065bed 100644 --- a/compiler/GHC/Core/Opt/WorkWrap/Utils.hs +++ b/compiler/GHC/Core/Opt/WorkWrap/Utils.hs @@ -34,6 +34,7 @@ import GHC.Types.Literal ( absentLiteralOf, rubbishLit ) import GHC.Types.Var.Env ( mkInScopeSet ) import GHC.Types.Var.Set ( VarSet ) import GHC.Core.Type +import GHC.Core.Multiplicity import GHC.Core.Predicate ( isClassPred ) import GHC.Types.RepType ( isVoidTy, typePrimRep ) import GHC.Core.Coercion @@ -185,7 +186,7 @@ mkWwBodies dflags fam_envs rhs_fvs fun_id demands cpr_info -- Note [Do not split void functions] only_one_void_argument | [d] <- demands - , Just (arg_ty1, _) <- splitFunTy_maybe fun_ty + , Just (Scaled _ arg_ty1, _) <- splitFunTy_maybe fun_ty , isAbsDmd d && isVoidTy arg_ty1 = True | otherwise @@ -423,7 +424,7 @@ mkWWargs subst fun_ty demands | (dmd:demands') <- demands , Just (arg_ty, fun_ty') <- splitFunTy_maybe fun_ty = do { uniq <- getUniqueM - ; let arg_ty' = substTy subst arg_ty + ; let arg_ty' = substScaledTy subst arg_ty id = mk_wrap_arg uniq arg_ty' dmd ; (wrap_args, wrap_fn_args, work_fn_args, res_ty) <- mkWWargs subst fun_ty' demands' @@ -472,9 +473,9 @@ mkWWargs subst fun_ty demands applyToVars :: [Var] -> CoreExpr -> CoreExpr applyToVars vars fn = mkVarApps fn vars -mk_wrap_arg :: Unique -> Type -> Demand -> Id -mk_wrap_arg uniq ty dmd - = mkSysLocalOrCoVar (fsLit "w") uniq ty +mk_wrap_arg :: Unique -> Scaled Type -> Demand -> Id +mk_wrap_arg uniq (Scaled w ty) dmd + = mkSysLocalOrCoVar (fsLit "w") uniq w ty `setIdDemandInfo` dmd {- Note [Freshen WW arguments] @@ -635,10 +636,12 @@ unbox_one dflags fam_envs arg cs , dcac_arg_tys = inst_con_arg_tys , dcac_co = co } = do { (uniq1:uniqs) <- getUniquesM - ; let -- See Note [Add demands for strict constructors] + ; let scale = scaleScaled (idMult arg) + scaled_inst_con_arg_tys = map (\(t,s) -> (scale t, s)) inst_con_arg_tys + -- See Note [Add demands for strict constructors] cs' = addDataConStrictness data_con cs - unpk_args = zipWith3 mk_ww_arg uniqs inst_con_arg_tys cs' - unbox_fn = mkUnpackCase (Var arg) co uniq1 + unpk_args = zipWith3 mk_ww_arg uniqs scaled_inst_con_arg_tys cs' + unbox_fn = mkUnpackCase (Var arg) co (idMult arg) uniq1 data_con unpk_args arg_no_unf = zapStableUnfolding arg -- See Note [Zap unfolding when beta-reducing] @@ -949,7 +952,7 @@ data DataConAppContext = DataConAppContext { dcac_dc :: !DataCon , dcac_tys :: ![Type] - , dcac_arg_tys :: ![(Type, StrictnessMark)] + , dcac_arg_tys :: ![(Scaled Type, StrictnessMark)] , dcac_co :: !Coercion } @@ -990,12 +993,22 @@ deepSplitCprType_maybe fam_envs con_tag ty , let con = cons `getNth` (con_tag - fIRST_TAG) arg_tys = dataConInstArgTys con tc_args strict_marks = dataConRepStrictness con + , all isLinear arg_tys + -- Deactivates CPR worker/wrapper splits on constructors with non-linear + -- arguments, for the moment, because they require unboxed tuple with variable + -- multiplicity fields. = Just DataConAppContext { dcac_dc = con , dcac_tys = tc_args , dcac_arg_tys = zipEqual "dspt" arg_tys strict_marks , dcac_co = co } deepSplitCprType_maybe _ _ _ = Nothing +isLinear :: Scaled a -> Bool +isLinear (Scaled w _ ) = + case w of + One -> True + _ -> False + findTypeShape :: FamInstEnvs -> Type -> TypeShape -- Uncover the arrow and product shape of a type -- The data type TypeShape is defined in GHC.Types.Demand @@ -1018,7 +1031,7 @@ findTypeShape fam_envs ty else checkRecTc rec_tc tc -- We treat tuples specially because they can't cause loops. -- Maybe we should do so in checkRecTc. - = TsProd (map (go rec_tc) (dataConInstArgTys con tc_args)) + = TsProd (map (go rec_tc . scaledThing) (dataConInstArgTys con tc_args)) | Just (_, ty') <- splitForAllTy_maybe ty = go rec_tc ty' @@ -1075,8 +1088,9 @@ mkWWcpr_help :: DataConAppContext mkWWcpr_help (DataConAppContext { dcac_dc = data_con, dcac_tys = inst_tys , dcac_arg_tys = arg_tys, dcac_co = co }) | [arg1@(arg_ty1, _)] <- arg_tys - , isUnliftedType arg_ty1 - -- Special case when there is a single result of unlifted type + , isUnliftedType (scaledThing arg_ty1) + , isLinear arg_ty1 + -- Special case when there is a single result of unlifted, linear, type -- -- Wrapper: case (..call worker..) of x -> C x -- Worker: case ( ..body.. ) of C x -> x @@ -1086,42 +1100,50 @@ mkWWcpr_help (DataConAppContext { dcac_dc = data_con, dcac_tys = inst_tys ; return ( True , \ wkr_call -> mkDefaultCase wkr_call arg con_app - , \ body -> mkUnpackCase body co work_uniq data_con [arg] (varToCoreExpr arg) + , \ body -> mkUnpackCase body co One work_uniq data_con [arg] (varToCoreExpr arg) -- varToCoreExpr important here: arg can be a coercion -- Lacking this caused #10658 - , arg_ty1 ) } + , scaledThing arg_ty1 ) } | otherwise -- The general case -- Wrapper: case (..call worker..) of (# a, b #) -> C a b -- Worker: case ( ...body... ) of C a b -> (# a, b #) + -- + -- Remark on linearity: in both the case of the wrapper and the worker, + -- we build a linear case. All the multiplicity information is kept in + -- the constructors (both C and (#, #)). In particular (#,#) is + -- parametrised by the multiplicity of its fields. Specifically, in this + -- instance, the multiplicity of the fields of (#,#) is chosen to be the + -- same as those of C. = do { (work_uniq : wild_uniq : uniqs) <- getUniquesM - ; let wrap_wild = mk_ww_local wild_uniq (ubx_tup_ty,MarkedStrict) + ; let wrap_wild = mk_ww_local wild_uniq (linear ubx_tup_ty,MarkedStrict) args = zipWith mk_ww_local uniqs arg_tys ubx_tup_ty = exprType ubx_tup_app - ubx_tup_app = mkCoreUbxTup (map fst arg_tys) (map varToCoreExpr args) + ubx_tup_app = mkCoreUbxTup (map (scaledThing . fst) arg_tys) (map varToCoreExpr args) con_app = mkConApp2 data_con inst_tys args `mkCast` mkSymCo co tup_con = tupleDataCon Unboxed (length arg_tys) ; return (True , \ wkr_call -> mkSingleAltCase wkr_call wrap_wild (DataAlt tup_con) args con_app - , \ body -> mkUnpackCase body co work_uniq data_con args ubx_tup_app + , \ body -> mkUnpackCase body co One work_uniq data_con args ubx_tup_app , ubx_tup_ty ) } -mkUnpackCase :: CoreExpr -> Coercion -> Unique -> DataCon -> [Id] -> CoreExpr -> CoreExpr +mkUnpackCase :: CoreExpr -> Coercion -> Mult -> Unique -> DataCon -> [Id] -> CoreExpr -> CoreExpr -- (mkUnpackCase e co uniq Con args body) -- returns -- case e |> co of bndr { Con args -> body } -mkUnpackCase (Tick tickish e) co uniq con args body -- See Note [Profiling and unpacking] - = Tick tickish (mkUnpackCase e co uniq con args body) -mkUnpackCase scrut co uniq boxing_con unpk_args body +mkUnpackCase (Tick tickish e) co mult uniq con args body -- See Note [Profiling and unpacking] + = Tick tickish (mkUnpackCase e co mult uniq con args body) +mkUnpackCase scrut co mult uniq boxing_con unpk_args body = mkSingleAltCase casted_scrut bndr (DataAlt boxing_con) unpk_args body where casted_scrut = scrut `mkCast` co - bndr = mk_ww_local uniq (exprType casted_scrut, MarkedStrict) - + bndr = mk_ww_local uniq (Scaled mult (exprType casted_scrut), MarkedStrict) + -- An unpacking case can always be chosen linear, because the variables + -- are always passed to a constructor. This limits the {- Note [non-algebraic or open body type warning] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1257,10 +1279,10 @@ mk_absent_let dflags fam_envs arg -- See also Note [Unique Determinism] in GHC.Types.Unique unlifted_rhs = mkTyApps (Lit rubbishLit) [arg_ty] -mk_ww_local :: Unique -> (Type, StrictnessMark) -> Id +mk_ww_local :: Unique -> (Scaled Type, StrictnessMark) -> Id -- The StrictnessMark comes form the data constructor and says -- whether this field is strict -- See Note [Record evaluated-ness in worker/wrapper] -mk_ww_local uniq (ty,str) +mk_ww_local uniq (Scaled w ty,str) = setCaseBndrEvald str $ - mkSysLocalOrCoVar (fsLit "ww") uniq ty + mkSysLocalOrCoVar (fsLit "ww") uniq w ty diff --git a/compiler/GHC/Core/PatSyn.hs b/compiler/GHC/Core/PatSyn.hs index c518a6c94e..6f88fd897d 100644 --- a/compiler/GHC/Core/PatSyn.hs +++ b/compiler/GHC/Core/PatSyn.hs @@ -33,6 +33,7 @@ import GHC.Types.Name import GHC.Utils.Outputable import GHC.Types.Unique import GHC.Utils.Misc +import GHC.Core.Multiplicity import GHC.Types.Basic import GHC.Types.Var import GHC.Types.FieldLabel @@ -421,13 +422,13 @@ patSynExTyVars ps = binderVars (psExTyVars ps) patSynExTyVarBinders :: PatSyn -> [InvisTVBinder] patSynExTyVarBinders = psExTyVars -patSynSigBndr :: PatSyn -> ([InvisTVBinder], ThetaType, [InvisTVBinder], ThetaType, [Type], Type) +patSynSigBndr :: PatSyn -> ([InvisTVBinder], ThetaType, [InvisTVBinder], ThetaType, [Scaled Type], Type) patSynSigBndr (MkPatSyn { psUnivTyVars = univ_tvs, psExTyVars = ex_tvs - , psProvTheta = prov, psReqTheta = req - , psArgs = arg_tys, psResultTy = res_ty }) - = (univ_tvs, req, ex_tvs, prov, arg_tys, res_ty) + , psProvTheta = prov, psReqTheta = req + , psArgs = arg_tys, psResultTy = res_ty }) + = (univ_tvs, req, ex_tvs, prov, map unrestricted arg_tys, res_ty) -patSynSig :: PatSyn -> ([TyVar], ThetaType, [TyVar], ThetaType, [Type], Type) +patSynSig :: PatSyn -> ([TyVar], ThetaType, [TyVar], ThetaType, [Scaled Type], Type) patSynSig ps = let (u_tvs, req, e_tvs, prov, arg_tys, res_ty) = patSynSigBndr ps in (binderVars u_tvs, req, binderVars e_tvs, prov, arg_tys, res_ty) @@ -484,6 +485,6 @@ pprPatSynType (MkPatSyn { psUnivTyVars = univ_tvs, psReqTheta = req_theta , pprType sigma_ty ] where sigma_ty = mkInvisForAllTys ex_tvs $ - mkInvisFunTys prov_theta $ - mkVisFunTys orig_args orig_res_ty + mkInvisFunTysMany prov_theta $ + mkVisFunTysMany orig_args orig_res_ty insert_empty_ctxt = null req_theta && not (null prov_theta && null ex_tvs) diff --git a/compiler/GHC/Core/Ppr/TyThing.hs b/compiler/GHC/Core/Ppr/TyThing.hs index 628d13ad7f..873c6ac199 100644 --- a/compiler/GHC/Core/Ppr/TyThing.hs +++ b/compiler/GHC/Core/Ppr/TyThing.hs @@ -166,7 +166,7 @@ pprTyThing :: ShowSub -> TyThing -> SDoc -- We pretty-print 'TyThing' via 'IfaceDecl' -- See Note [Pretty-printing TyThings] pprTyThing ss ty_thing - = pprIfaceDecl ss' (tyThingToIfaceDecl ty_thing) + = sdocWithDynFlags (\dflags -> pprIfaceDecl ss' (tyThingToIfaceDecl dflags ty_thing)) where ss' = case ss_how_much ss of ShowHeader (AltPpr Nothing) -> ss { ss_how_much = ShowHeader ppr' } diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs index 9f0eefef30..dda9e24db2 100644 --- a/compiler/GHC/Core/Predicate.hs +++ b/compiler/GHC/Core/Predicate.hs @@ -41,6 +41,7 @@ import GHC.Builtin.Names import GHC.Data.FastString import GHC.Utils.Outputable import GHC.Utils.Misc +import GHC.Core.Multiplicity ( scaledThing ) import Control.Monad ( guard ) @@ -70,7 +71,7 @@ classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of _ | (tvs, rho) <- splitForAllTys ev_ty , (theta, pred) <- splitFunTys rho , not (null tvs && null theta) - -> ForAllPred tvs theta pred + -> ForAllPred tvs (map scaledThing theta) pred | otherwise -> IrredPred ev_ty diff --git a/compiler/GHC/Core/SimpleOpt.hs b/compiler/GHC/Core/SimpleOpt.hs index 216c30d8fc..b0b6416c0b 100644 --- a/compiler/GHC/Core/SimpleOpt.hs +++ b/compiler/GHC/Core/SimpleOpt.hs @@ -45,6 +45,7 @@ import GHC.Core.Type hiding ( substTy, extendTvSubst, extendCvSubst, extendTvSub , isInScope, substTyVarBndr, cloneTyVarBndr ) import GHC.Core.Coercion hiding ( substCo, substCoVarBndr ) import GHC.Core.TyCon ( tyConArity ) +import GHC.Core.Multiplicity import GHC.Builtin.Types import GHC.Builtin.Names import GHC.Types.Basic @@ -377,7 +378,7 @@ simple_bind_pair env@(SOE { soe_inl = inl_env, soe_subst = subst }) top_level | Type ty <- in_rhs -- let a::* = TYPE ty in <body> , let out_ty = substTy (soe_subst rhs_env) ty - = ASSERT( isTyVar in_bndr ) + = ASSERT2( isTyVar in_bndr, ppr in_bndr $$ ppr in_rhs ) (env { soe_subst = extendTvSubst subst in_bndr out_ty }, Nothing) | Coercion co <- in_rhs @@ -435,7 +436,7 @@ simple_out_bind :: TopLevelFlag -> (SimpleOptEnv, Maybe (OutVar, OutExpr)) simple_out_bind top_level env@(SOE { soe_subst = subst }) (in_bndr, out_rhs) | Type out_ty <- out_rhs - = ASSERT( isTyVar in_bndr ) + = ASSERT2( isTyVar in_bndr, ppr in_bndr $$ ppr out_ty $$ ppr out_rhs ) (env { soe_subst = extendTvSubst subst in_bndr out_ty }, Nothing) | Coercion out_co <- out_rhs @@ -588,7 +589,7 @@ subst_opt_id_bndr env@(SOE { soe_subst = subst, soe_inl = inl }) old_id Subst in_scope id_subst tv_subst cv_subst = subst id1 = uniqAway in_scope old_id - id2 = setIdType id1 (substTy subst (idType old_id)) + id2 = updateIdTypeAndMult (substTy subst) id1 new_id = zapFragileIdInfo id2 -- Zaps rules, unfolding, and fragile OccInfo -- The unfolding and rules will get added back later, by add_info @@ -1399,7 +1400,14 @@ pushCoValArg co = Just (mkRepReflCo arg, MRefl) | isFunTy tyL - , (co1, co2) <- decomposeFunCo Representational co + , (co_mult, co1, co2) <- decomposeFunCo Representational co + , isReflexiveCo co_mult + -- We can't push the coercion in the case where co_mult isn't reflexivity: + -- it could be an unsafe axiom, and losing this information could yield + -- ill-typed terms. For instance (fun x ::(1) Int -> (fun _ -> () |> co) x) + -- with co :: (Int -> ()) ~ (Int #-> ()), would reduce to (fun x ::(1) Int + -- -> (fun _ ::(Many) Int -> ()) x) which is ill-typed + -- If co :: (tyL1 -> tyL2) ~ (tyR1 -> tyR2) -- then co1 :: tyL1 ~ tyR1 -- co2 :: tyL2 ~ tyR2 @@ -1422,11 +1430,15 @@ pushCoercionIntoLambda in_scope x e co | ASSERT(not (isTyVar x) && not (isCoVar x)) True , Pair s1s2 t1t2 <- coercionKind co , Just (_s1,_s2) <- splitFunTy_maybe s1s2 - , Just (t1,_t2) <- splitFunTy_maybe t1t2 - = let (co1, co2) = decomposeFunCo Representational co + , Just (Scaled w1 t1,_t2) <- splitFunTy_maybe t1t2 + , (co_mult, co1, co2) <- decomposeFunCo Representational co + , isReflexiveCo co_mult + -- We can't push the coercion in the case where co_mult isn't + -- reflexivity. See pushCoValArg for more details. + = let -- Should we optimize the coercions here? -- Otherwise they might not match too well - x' = x `setIdType` t1 + x' = x `setIdType` t1 `setIdMult` w1 in_scope' = in_scope `extendInScopeSet` x' subst = extendIdSubst (mkEmptySubst in_scope') x @@ -1478,14 +1490,15 @@ pushCoDataCon dc dc_args co (map exprToType ex_args) -- Cast the value arguments (which include dictionaries) - new_val_args = zipWith cast_arg arg_tys val_args + new_val_args = zipWith cast_arg (map scaledThing arg_tys) val_args cast_arg arg_ty arg = mkCast arg (psi_subst arg_ty) to_ex_args = map Type to_ex_arg_tys dump_doc = vcat [ppr dc, ppr dc_univ_tyvars, ppr dc_ex_tcvars, ppr arg_tys, ppr dc_args, - ppr ex_args, ppr val_args, ppr co, ppr from_ty, ppr to_ty, ppr to_tc ] + ppr ex_args, ppr val_args, ppr co, ppr from_ty, ppr to_ty, ppr to_tc + , ppr $ mkTyConApp to_tc (map exprToType $ takeList dc_univ_tyvars dc_args) ] in ASSERT2( eqType from_ty (mkTyConApp to_tc (map exprToType $ takeList dc_univ_tyvars dc_args)), dump_doc ) ASSERT2( equalLength val_args arg_tys, dump_doc ) @@ -1545,7 +1558,8 @@ collectBindersPushingCo e | isId b , let Pair tyL tyR = coercionKind co , ASSERT( isFunTy tyL) isFunTy tyR - , (co_arg, co_res) <- decomposeFunCo Representational co + , (co_mult, co_arg, co_res) <- decomposeFunCo Representational co + , isReflCo co_mult -- See Note [collectBindersPushingCo] , isReflCo co_arg -- See Note [collectBindersPushingCo] = go_c (b:bs) e co_res @@ -1556,7 +1570,7 @@ collectBindersPushingCo e Note [collectBindersPushingCo] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We just look for coercions of form - <type> -> blah + <type> # w -> blah (and similarly for foralls) to keep this function simple. We could do more elaborate stuff, but it'd involve substitution etc. diff --git a/compiler/GHC/Core/Subst.hs b/compiler/GHC/Core/Subst.hs index ddb5b61f7b..f2b25e17e5 100644 --- a/compiler/GHC/Core/Subst.hs +++ b/compiler/GHC/Core/Subst.hs @@ -476,11 +476,12 @@ substIdBndr _doc rec_subst subst@(Subst in_scope env tvs cvs) old_id where id1 = uniqAway in_scope old_id -- id1 is cloned if necessary id2 | no_type_change = id1 - | otherwise = setIdType id1 (substTy subst old_ty) + | otherwise = updateIdTypeAndMult (substTy subst) id1 old_ty = idType old_id + old_w = idMult old_id no_type_change = (isEmptyVarEnv tvs && isEmptyVarEnv cvs) || - noFreeVarsOfType old_ty + (noFreeVarsOfType old_ty && noFreeVarsOfType old_w) -- new_id has the right IdInfo -- The lazy-set is because we're in a loop here, with @@ -600,13 +601,16 @@ substCo subst co = Coercion.substCo (getTCvSubst subst) co substIdType :: Subst -> Id -> Id substIdType subst@(Subst _ _ tv_env cv_env) id - | (isEmptyVarEnv tv_env && isEmptyVarEnv cv_env) || noFreeVarsOfType old_ty = id - | otherwise = setIdType id (substTy subst old_ty) - -- The tyCoVarsOfType is cheaper than it looks - -- because we cache the free tyvars of the type - -- in a Note in the id's type itself + | (isEmptyVarEnv tv_env && isEmptyVarEnv cv_env) + || (noFreeVarsOfType old_ty && noFreeVarsOfType old_w) = id + | otherwise = + updateIdTypeAndMult (substTy subst) id + -- The tyCoVarsOfType is cheaper than it looks + -- because we cache the free tyvars of the type + -- in a Note in the id's type itself where old_ty = idType id + old_w = varMult id ------------------ -- | Substitute into some 'IdInfo' with regard to the supplied new 'Id'. diff --git a/compiler/GHC/Core/Tidy.hs b/compiler/GHC/Core/Tidy.hs index c31b58f6ed..246da2be54 100644 --- a/compiler/GHC/Core/Tidy.hs +++ b/compiler/GHC/Core/Tidy.hs @@ -149,8 +149,9 @@ tidyIdBndr env@(tidy_env, var_env) id -- though we could extract it from the Id -- ty' = tidyType env (idType id) + mult' = tidyType env (idMult id) name' = mkInternalName (idUnique id) occ' noSrcSpan - id' = mkLocalIdWithInfo name' ty' new_info + id' = mkLocalIdWithInfo name' mult' ty' new_info var_env' = extendVarEnv var_env id id' -- Note [Tidy IdInfo] @@ -174,9 +175,10 @@ tidyLetBndr rec_tidy_env env@(tidy_env, var_env) id = case tidyOccName tidy_env (getOccName id) of { (tidy_env', occ') -> let ty' = tidyType env (idType id) + mult' = tidyType env (idMult id) name' = mkInternalName (idUnique id) occ' noSrcSpan details = idDetails id - id' = mkLocalVar details name' ty' new_info + id' = mkLocalVar details name' mult' ty' new_info var_env' = extendVarEnv var_env id id' -- Note [Tidy IdInfo] diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs index e6083eb521..0d7e1cb47c 100644 --- a/compiler/GHC/Core/TyCo/FVs.hs +++ b/compiler/GHC/Core/TyCo/FVs.hs @@ -570,7 +570,7 @@ tyCoFVsOfType (TyVarTy v) f bound_vars (acc_list, acc_set) tyCoFVsOfType (TyConApp _ tys) f bound_vars acc = tyCoFVsOfTypes tys f bound_vars acc tyCoFVsOfType (LitTy {}) f bound_vars acc = emptyFV f bound_vars acc tyCoFVsOfType (AppTy fun arg) f bound_vars acc = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) f bound_vars acc -tyCoFVsOfType (FunTy _ arg res) f bound_vars acc = (tyCoFVsOfType arg `unionFV` tyCoFVsOfType res) f bound_vars acc +tyCoFVsOfType (FunTy _ w arg res) f bound_vars acc = (tyCoFVsOfType w `unionFV` tyCoFVsOfType arg `unionFV` tyCoFVsOfType res) f bound_vars acc tyCoFVsOfType (ForAllTy bndr ty) f bound_vars acc = tyCoFVsBndr bndr (tyCoFVsOfType ty) f bound_vars acc tyCoFVsOfType (CastTy ty co) f bound_vars acc = (tyCoFVsOfType ty `unionFV` tyCoFVsOfCo co) f bound_vars acc tyCoFVsOfType (CoercionTy co) f bound_vars acc = tyCoFVsOfCo co f bound_vars acc @@ -617,8 +617,8 @@ tyCoFVsOfCo (AppCo co arg) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc tyCoFVsOfCo (ForAllCo tv kind_co co) fv_cand in_scope acc = (tyCoFVsVarBndr tv (tyCoFVsOfCo co) `unionFV` tyCoFVsOfCo kind_co) fv_cand in_scope acc -tyCoFVsOfCo (FunCo _ co1 co2) fv_cand in_scope acc - = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc +tyCoFVsOfCo (FunCo _ w co1 co2) fv_cand in_scope acc + = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2 `unionFV` tyCoFVsOfCo w) fv_cand in_scope acc tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc = tyCoFVsOfCoVar v fv_cand in_scope acc tyCoFVsOfCo (HoleCo h) fv_cand in_scope acc @@ -672,8 +672,9 @@ almost_devoid_co_var_of_co (AppCo co arg) cv almost_devoid_co_var_of_co (ForAllCo v kind_co co) cv = almost_devoid_co_var_of_co kind_co cv && (v == cv || almost_devoid_co_var_of_co co cv) -almost_devoid_co_var_of_co (FunCo _ co1 co2) cv - = almost_devoid_co_var_of_co co1 cv +almost_devoid_co_var_of_co (FunCo _ w co1 co2) cv + = almost_devoid_co_var_of_co w cv + && almost_devoid_co_var_of_co co1 cv && almost_devoid_co_var_of_co co2 cv almost_devoid_co_var_of_co (CoVarCo v) cv = v /= cv almost_devoid_co_var_of_co (HoleCo h) cv = (coHoleCoVar h) /= cv @@ -723,8 +724,9 @@ almost_devoid_co_var_of_type (LitTy {}) _ = True almost_devoid_co_var_of_type (AppTy fun arg) cv = almost_devoid_co_var_of_type fun cv && almost_devoid_co_var_of_type arg cv -almost_devoid_co_var_of_type (FunTy _ arg res) cv - = almost_devoid_co_var_of_type arg cv +almost_devoid_co_var_of_type (FunTy _ w arg res) cv + = almost_devoid_co_var_of_type w cv + && almost_devoid_co_var_of_type arg cv && almost_devoid_co_var_of_type res cv almost_devoid_co_var_of_type (ForAllTy (Bndr v _) ty) cv = almost_devoid_co_var_of_type (varType v) cv @@ -779,12 +781,12 @@ injectiveVarsOfType :: Bool -- ^ Should we look under injective type families? -> Type -> FV injectiveVarsOfType look_under_tfs = go where - go ty | Just ty' <- coreView ty - = go ty' - go (TyVarTy v) = unitFV v `unionFV` go (tyVarKind v) - go (AppTy f a) = go f `unionFV` go a - go (FunTy _ ty1 ty2) = go ty1 `unionFV` go ty2 - go (TyConApp tc tys) = + go ty | Just ty' <- coreView ty + = go ty' + go (TyVarTy v) = unitFV v `unionFV` go (tyVarKind v) + go (AppTy f a) = go f `unionFV` go a + go (FunTy _ w ty1 ty2) = go w `unionFV` go ty1 `unionFV` go ty2 + go (TyConApp tc tys) = case tyConInjectivityInfo tc of Injective inj | look_under_tfs || not (isTypeFamilyTyCon tc) @@ -837,7 +839,7 @@ invisibleVarsOfType = go = go ty' go (TyVarTy v) = go (tyVarKind v) go (AppTy f a) = go f `unionFV` go a - go (FunTy _ ty1 ty2) = go ty1 `unionFV` go ty2 + go (FunTy _ w ty1 ty2) = go w `unionFV` go ty1 `unionFV` go ty2 go (TyConApp tc tys) = tyCoFVsOfTypes invisibles `unionFV` invisibleVarsOfTypes visibles where (invisibles, visibles) = partitionInvisibleTypes tc tys diff --git a/compiler/GHC/Core/TyCo/Ppr.hs b/compiler/GHC/Core/TyCo/Ppr.hs index 40f901dc53..c6bf57e6d2 100644 --- a/compiler/GHC/Core/TyCo/Ppr.hs +++ b/compiler/GHC/Core/TyCo/Ppr.hs @@ -34,6 +34,7 @@ import {-# SOURCE #-} GHC.CoreToIface import {-# SOURCE #-} GHC.Core.DataCon ( dataConFullSig , dataConUserTyVarBinders , DataCon ) +import GHC.Core.Multiplicity import {-# SOURCE #-} GHC.Core.Type ( isLiftedTypeKind ) @@ -213,13 +214,18 @@ debug_ppr_ty _ (LitTy l) debug_ppr_ty _ (TyVarTy tv) = ppr tv -- With -dppr-debug we get (tv :: kind) -debug_ppr_ty prec (FunTy { ft_af = af, ft_arg = arg, ft_res = res }) +debug_ppr_ty prec ty@(FunTy { ft_af = af, ft_mult = mult, ft_arg = arg, ft_res = res }) = maybeParen prec funPrec $ - sep [debug_ppr_ty funPrec arg, arrow <+> debug_ppr_ty prec res] + sep [debug_ppr_ty funPrec arg, arr <+> debug_ppr_ty prec res] where - arrow = case af of - VisArg -> text "->" - InvisArg -> text "=>" + arr = case af of + VisArg -> case mult of + One -> lollipop + Many -> arrow + w -> mulArrow (ppr w) + InvisArg -> case mult of + Many -> darrow + _ -> pprPanic "unexpected multiplicity" (ppr ty) debug_ppr_ty prec (TyConApp tc tys) | null tys = ppr tc @@ -286,7 +292,7 @@ pprDataConWithArgs dc = sep [forAllDoc, thetaDoc, ppr dc <+> argsDoc] user_bndrs = tyVarSpecToBinders $ dataConUserTyVarBinders dc forAllDoc = pprUserForAll user_bndrs thetaDoc = pprThetaArrowTy theta - argsDoc = hsep (fmap pprParendType arg_tys) + argsDoc = hsep (fmap pprParendType (map scaledThing arg_tys)) pprTypeApp :: TyCon -> [Type] -> SDoc diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs index 684854045e..e201dcfea3 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs +++ b/compiler/GHC/Core/TyCo/Rep.hs @@ -27,7 +27,7 @@ module GHC.Core.TyCo.Rep ( -- * Types Type( TyVarTy, AppTy, TyConApp, ForAllTy , LitTy, CastTy, CoercionTy - , FunTy, ft_arg, ft_res, ft_af + , FunTy, ft_mult, ft_arg, ft_res, ft_af ), -- Export the type synonym FunTy too TyLit(..), @@ -46,9 +46,13 @@ module GHC.Core.TyCo.Rep ( -- * Functions over types mkTyConTy, mkTyVarTy, mkTyVarTys, mkTyCoVarTy, mkTyCoVarTys, - mkFunTy, mkVisFunTy, mkInvisFunTy, mkVisFunTys, mkInvisFunTys, + mkFunTy, mkVisFunTy, mkInvisFunTy, mkVisFunTys, mkForAllTy, mkForAllTys, mkInvisForAllTys, mkPiTy, mkPiTys, + mkFunTyMany, + mkScaledFunTy, + mkVisFunTyMany, mkVisFunTysMany, + mkInvisFunTyMany, mkInvisFunTysMany, -- * Functions over binders TyCoBinder(..), TyCoVarBinder, TyBinder, @@ -83,6 +87,7 @@ import GHC.Iface.Type import GHC.Types.Var import GHC.Types.Var.Set import GHC.Types.Name hiding ( varName ) +import GHC.Core.Multiplicity import GHC.Core.TyCon import GHC.Core.Coercion.Axiom @@ -210,9 +215,10 @@ data Type -- be mentioned in the Type. See -- Note [Unused coercion variable in ForAllTy] - | FunTy -- ^ t1 -> t2 Very common, so an important special case + | FunTy -- ^ FUN m t1 t2 Very common, so an important special case -- See Note [Function types] - { ft_af :: AnonArgFlag -- Is this (->) or (=>)? + { ft_af :: AnonArgFlag -- Is this (->) or (=>)? + , ft_mult :: Mult -- Multiplicity , ft_arg :: Type -- Argument type , ft_res :: Type } -- Result type @@ -680,8 +686,8 @@ type KnotTied ty = ty -- not. See Note [TyCoBinders] data TyCoBinder = Named TyCoVarBinder -- A type-lambda binder - | Anon AnonArgFlag Type -- A term-lambda binder. Type here can be CoercionTy. - -- Visibility is determined by the AnonArgFlag + | Anon AnonArgFlag (Scaled Type) -- A term-lambda binder. Type here can be CoercionTy. + -- Visibility is determined by the AnonArgFlag deriving Data.Data instance Outputable TyCoBinder where @@ -980,19 +986,41 @@ mkTyCoVarTy v mkTyCoVarTys :: [TyCoVar] -> [Type] mkTyCoVarTys = map mkTyCoVarTy -infixr 3 `mkFunTy`, `mkVisFunTy`, `mkInvisFunTy` -- Associates to the right +infixr 3 `mkFunTy`, `mkVisFunTy`, `mkInvisFunTy`, `mkVisFunTyMany`, + `mkInvisFunTyMany` -- Associates to the right -mkFunTy :: AnonArgFlag -> Type -> Type -> Type -mkFunTy af arg res = FunTy { ft_af = af, ft_arg = arg, ft_res = res } +mkFunTy :: AnonArgFlag -> Mult -> Type -> Type -> Type +mkFunTy af mult arg res = FunTy { ft_af = af + , ft_mult = mult + , ft_arg = arg + , ft_res = res } -mkVisFunTy, mkInvisFunTy :: Type -> Type -> Type +mkScaledFunTy :: AnonArgFlag -> Scaled Type -> Type -> Type +mkScaledFunTy af (Scaled mult arg) res = mkFunTy af mult arg res + +mkVisFunTy, mkInvisFunTy :: Mult -> Type -> Type -> Type mkVisFunTy = mkFunTy VisArg mkInvisFunTy = mkFunTy InvisArg +mkFunTyMany :: AnonArgFlag -> Type -> Type -> Type +mkFunTyMany af = mkFunTy af Many + +-- | Special, common, case: Arrow type with mult Many +mkVisFunTyMany :: Type -> Type -> Type +mkVisFunTyMany = mkVisFunTy Many + +mkInvisFunTyMany :: Type -> Type -> Type +mkInvisFunTyMany = mkInvisFunTy Many + -- | Make nested arrow types -mkVisFunTys, mkInvisFunTys :: [Type] -> Type -> Type -mkVisFunTys tys ty = foldr mkVisFunTy ty tys -mkInvisFunTys tys ty = foldr mkInvisFunTy ty tys +mkVisFunTys :: [Scaled Type] -> Type -> Type +mkVisFunTys tys ty = foldr (mkScaledFunTy VisArg) ty tys + +mkVisFunTysMany :: [Type] -> Type -> Type +mkVisFunTysMany tys ty = foldr mkVisFunTyMany ty tys + +mkInvisFunTysMany :: [Type] -> Type -> Type +mkInvisFunTysMany tys ty = foldr mkInvisFunTyMany ty tys -- | Like 'mkTyCoForAllTy', but does not check the occurrence of the binder -- See Note [Unused coercion variable in ForAllTy] @@ -1007,8 +1035,8 @@ mkForAllTys tyvars ty = foldr ForAllTy ty tyvars mkInvisForAllTys :: [InvisTVBinder] -> Type -> Type mkInvisForAllTys tyvars ty = foldr ForAllTy ty $ tyVarSpecToBinders tyvars -mkPiTy:: TyCoBinder -> Type -> Type -mkPiTy (Anon af ty1) ty2 = FunTy { ft_af = af, ft_arg = ty1, ft_res = ty2 } +mkPiTy :: TyCoBinder -> Type -> Type +mkPiTy (Anon af ty1) ty2 = mkScaledFunTy af ty1 ty2 mkPiTy (Named (Bndr tv vis)) ty = mkForAllTy tv vis ty mkPiTys :: [TyCoBinder] -> Type -> Type @@ -1079,8 +1107,8 @@ data Coercion | ForAllCo TyCoVar KindCoercion Coercion -- ForAllCo :: _ -> N -> e -> e - | FunCo Role Coercion Coercion -- lift FunTy - -- FunCo :: "e" -> e -> e -> e + | FunCo Role CoercionN Coercion Coercion -- lift FunTy + -- FunCo :: "e" -> N -> e -> e -> e -- Note: why doesn't FunCo have a AnonArgFlag, like FunTy? -- Because the AnonArgFlag has no impact on Core; it is only -- there to guide implicit instantiation of Haskell source @@ -1825,7 +1853,7 @@ foldTyCo (TyCoFolder { tcf_view = view go_ty _ (LitTy {}) = mempty go_ty env (CastTy ty co) = go_ty env ty `mappend` go_co env co go_ty env (CoercionTy co) = go_co env co - go_ty env (FunTy _ arg res) = go_ty env arg `mappend` go_ty env res + go_ty env (FunTy _ w arg res) = go_ty env w `mappend` go_ty env arg `mappend` go_ty env res go_ty env (TyConApp _ tys) = go_tys env tys go_ty env (ForAllTy (Bndr tv vis) inner) = let !env' = tycobinder env tv vis -- Avoid building a thunk here @@ -1845,7 +1873,9 @@ foldTyCo (TyCoFolder { tcf_view = view go_co env (GRefl _ ty (MCo co)) = go_ty env ty `mappend` go_co env co go_co env (TyConAppCo _ _ args) = go_cos env args go_co env (AppCo c1 c2) = go_co env c1 `mappend` go_co env c2 - go_co env (FunCo _ c1 c2) = go_co env c1 `mappend` go_co env c2 + go_co env (FunCo _ cw c1 c2) = go_co env cw `mappend` + go_co env c1 `mappend` + go_co env c2 go_co env (CoVarCo cv) = covar env cv go_co env (AxiomInstCo _ _ args) = go_cos env args go_co env (HoleCo hole) = cohole env hole @@ -1892,7 +1922,7 @@ typeSize :: Type -> Int typeSize (LitTy {}) = 1 typeSize (TyVarTy {}) = 1 typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2 -typeSize (FunTy _ t1 t2) = typeSize t1 + typeSize t2 +typeSize (FunTy _ _ t1 t2) = typeSize t1 + typeSize t2 typeSize (ForAllTy (Bndr tv _) t) = typeSize (varType tv) + typeSize t typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts) typeSize (CastTy ty co) = typeSize ty + coercionSize co @@ -1905,7 +1935,8 @@ coercionSize (GRefl _ ty (MCo co)) = 1 + typeSize ty + coercionSize co coercionSize (TyConAppCo _ _ args) = 1 + sum (map coercionSize args) coercionSize (AppCo co arg) = coercionSize co + coercionSize arg coercionSize (ForAllCo _ h co) = 1 + coercionSize co + coercionSize h -coercionSize (FunCo _ co1 co2) = 1 + coercionSize co1 + coercionSize co2 +coercionSize (FunCo _ w co1 co2) = 1 + coercionSize co1 + coercionSize co2 + + coercionSize w coercionSize (CoVarCo _) = 1 coercionSize (HoleCo _) = 1 coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args) diff --git a/compiler/GHC/Core/TyCo/Rep.hs-boot b/compiler/GHC/Core/TyCo/Rep.hs-boot index c7ce05f0a6..25a22435cf 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs-boot +++ b/compiler/GHC/Core/TyCo/Rep.hs-boot @@ -1,5 +1,6 @@ module GHC.Core.TyCo.Rep where +import GHC.Utils.Outputable ( Outputable ) import Data.Data ( Data ) import {-# SOURCE #-} GHC.Types.Var( Var, ArgFlag, AnonArgFlag ) @@ -17,7 +18,8 @@ type ThetaType = [PredType] type CoercionN = Coercion type MCoercionN = MCoercion -mkFunTy :: AnonArgFlag -> Type -> Type -> Type +mkFunTyMany :: AnonArgFlag -> Type -> Type -> Type mkForAllTy :: Var -> ArgFlag -> Type -> Type instance Data Type -- To support Data instances in GHC.Core.Coercion.Axiom +instance Outputable Type diff --git a/compiler/GHC/Core/TyCo/Subst.hs b/compiler/GHC/Core/TyCo/Subst.hs index 0c8f77dfd8..88799c2414 100644 --- a/compiler/GHC/Core/TyCo/Subst.hs +++ b/compiler/GHC/Core/TyCo/Subst.hs @@ -33,12 +33,12 @@ module GHC.Core.TyCo.Subst substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars, substCoWith, - substTy, substTyAddInScope, - substTyUnchecked, substTysUnchecked, substThetaUnchecked, - substTyWithUnchecked, + substTy, substTyAddInScope, substScaledTy, + substTyUnchecked, substTysUnchecked, substScaledTysUnchecked, substThetaUnchecked, + substTyWithUnchecked, substScaledTyUnchecked, substCoUnchecked, substCoWithUnchecked, substTyWithInScope, - substTys, substTheta, + substTys, substScaledTys, substTheta, lookupTyVar, substCo, substCos, substCoVar, substCoVars, lookupCoVar, cloneTyVarBndr, cloneTyVarBndrs, @@ -69,6 +69,7 @@ import {-# SOURCE #-} GHC.Core.Coercion import GHC.Core.TyCo.Rep import GHC.Core.TyCo.FVs import GHC.Core.TyCo.Ppr +import GHC.Core.Multiplicity import GHC.Types.Var import GHC.Types.Var.Set @@ -673,6 +674,12 @@ substTyUnchecked subst ty | isEmptyTCvSubst subst = ty | otherwise = subst_ty subst ty +substScaledTy :: HasCallStack => TCvSubst -> Scaled Type -> Scaled Type +substScaledTy subst scaled_ty = mapScaledType (substTy subst) scaled_ty + +substScaledTyUnchecked :: HasCallStack => TCvSubst -> Scaled Type -> Scaled Type +substScaledTyUnchecked subst scaled_ty = mapScaledType (substTyUnchecked subst) scaled_ty + -- | Substitute within several 'Type's -- The substitution has to satisfy the invariants described in -- Note [The substitution invariant]. @@ -681,6 +688,12 @@ substTys subst tys | isEmptyTCvSubst subst = tys | otherwise = checkValidSubst subst tys [] $ map (subst_ty subst) tys +substScaledTys :: HasCallStack => TCvSubst -> [Scaled Type] -> [Scaled Type] +substScaledTys subst scaled_tys + | isEmptyTCvSubst subst = scaled_tys + | otherwise = checkValidSubst subst (map scaledMult scaled_tys ++ map scaledThing scaled_tys) [] $ + map (mapScaledType (subst_ty subst)) scaled_tys + -- | Substitute within several 'Type's disabling the sanity checks. -- The problems that the sanity checks in substTys catch are described in -- Note [The substitution invariant]. @@ -691,6 +704,11 @@ substTysUnchecked subst tys | isEmptyTCvSubst subst = tys | otherwise = map (subst_ty subst) tys +substScaledTysUnchecked :: TCvSubst -> [Scaled Type] -> [Scaled Type] +substScaledTysUnchecked subst tys + | isEmptyTCvSubst subst = tys + | otherwise = map (mapScaledType (subst_ty subst)) tys + -- | Substitute within a 'ThetaType' -- The substitution has to satisfy the invariants described in -- Note [The substitution invariant]. @@ -721,10 +739,11 @@ subst_ty subst ty -- by [Int], represented with TyConApp go (TyConApp tc tys) = let args = map go tys in args `seqList` TyConApp tc args - go ty@(FunTy { ft_arg = arg, ft_res = res }) - = let !arg' = go arg + go ty@(FunTy { ft_mult = mult, ft_arg = arg, ft_res = res }) + = let !mult' = go mult + !arg' = go arg !res' = go res - in ty { ft_arg = arg', ft_res = res' } + in ty { ft_mult = mult', ft_arg = arg', ft_res = res' } go (ForAllTy (Bndr tv vis) ty) = case substVarBndrUnchecked subst tv of (subst', tv') -> @@ -805,7 +824,7 @@ subst_co subst co = case substForAllCoBndrUnchecked subst tv kind_co of (subst', tv', kind_co') -> ((mkForAllCo $! tv') $! kind_co') $! subst_co subst' co - go (FunCo r co1 co2) = (mkFunCo r $! go co1) $! go co2 + go (FunCo r w co1 co2) = ((mkFunCo r $! go w) $! go co1) $! go co2 go (CoVarCo cv) = substCoVar subst cv go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos go (UnivCo p r t1 t2) = (((mkUnivCo $! go_prov p) $! r) $! @@ -827,7 +846,7 @@ subst_co subst co -- See Note [Substituting in a coercion hole] go_hole h@(CoercionHole { ch_co_var = cv }) - = h { ch_co_var = updateVarType go_ty cv } + = h { ch_co_var = updateVarTypeAndMult go_ty cv } substForAllCoBndr :: TCvSubst -> TyCoVar -> KindCoercion -> (TCvSubst, TyCoVar, Coercion) diff --git a/compiler/GHC/Core/TyCo/Tidy.hs b/compiler/GHC/Core/TyCo/Tidy.hs index 6cfce74790..bc586d77c8 100644 --- a/compiler/GHC/Core/TyCo/Tidy.hs +++ b/compiler/GHC/Core/TyCo/Tidy.hs @@ -52,8 +52,7 @@ tidyVarBndr tidy_env@(occ_env, subst) var (occ_env', occ') -> ((occ_env', subst'), var') where subst' = extendVarEnv subst var var' - var' = setVarType (setVarName var name') type' - type' = tidyType tidy_env (varType var) + var' = updateVarTypeAndMult (tidyType tidy_env) (setVarName var name') name' = tidyNameOcc name occ' name = varName var @@ -120,7 +119,7 @@ tidyOpenTyCoVar env@(_, subst) tyvar tidyTyCoVarOcc :: TidyEnv -> TyCoVar -> TyCoVar tidyTyCoVarOcc env@(_, subst) tv = case lookupVarEnv subst tv of - Nothing -> updateVarType (tidyType env) tv + Nothing -> updateVarTypeAndMult (tidyType env) tv Just tv' -> tv' --------------- @@ -134,9 +133,10 @@ tidyType env (TyVarTy tv) = TyVarTy (tidyTyCoVarOcc env tv) tidyType env (TyConApp tycon tys) = let args = tidyTypes env tys in args `seqList` TyConApp tycon args tidyType env (AppTy fun arg) = (AppTy $! (tidyType env fun)) $! (tidyType env arg) -tidyType env ty@(FunTy _ arg res) = let { !arg' = tidyType env arg - ; !res' = tidyType env res } - in ty { ft_arg = arg', ft_res = res' } +tidyType env ty@(FunTy _ w arg res) = let { !w' = tidyType env w + ; !arg' = tidyType env arg + ; !res' = tidyType env res } + in ty { ft_mult = w', ft_arg = arg', ft_res = res' } tidyType env (ty@(ForAllTy{})) = mkForAllTys' (zip tvs' vis) $! tidyType env' body_ty where (tvs, vis, body_ty) = splitForAllTys' ty @@ -208,7 +208,7 @@ tidyCo env@(_, subst) co where (envp, tvp) = tidyVarBndr env tv -- the case above duplicates a bit of work in tidying h and the kind -- of tv. But the alternative is to use coercionKind, which seems worse. - go (FunCo r co1 co2) = (FunCo r $! go co1) $! go co2 + go (FunCo r w co1 co2) = ((FunCo r $! go w) $! go co1) $! go co2 go (CoVarCo cv) = case lookupVarEnv subst cv of Nothing -> CoVarCo cv Just cv' -> CoVarCo cv' diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs index 80b4500685..eac2d8b109 100644 --- a/compiler/GHC/Core/TyCon.hs +++ b/compiler/GHC/Core/TyCon.hs @@ -138,11 +138,12 @@ import GHC.Prelude import GHC.Platform import {-# SOURCE #-} GHC.Core.TyCo.Rep - ( Kind, Type, PredType, mkForAllTy, mkFunTy ) + ( Kind, Type, PredType, mkForAllTy, mkFunTyMany ) import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprType ) import {-# SOURCE #-} GHC.Builtin.Types ( runtimeRepTyCon, constraintKind + , multiplicityTyCon , vecCountTyCon, vecElemTyCon, liftedTypeKind ) import {-# SOURCE #-} GHC.Core.DataCon ( DataCon, dataConExTyCoVars, dataConFieldLabels @@ -489,7 +490,7 @@ mkTyConKind :: [TyConBinder] -> Kind -> Kind mkTyConKind bndrs res_kind = foldr mk res_kind bndrs where mk :: TyConBinder -> Kind -> Kind - mk (Bndr tv (AnonTCB af)) k = mkFunTy af (varType tv) k + mk (Bndr tv (AnonTCB af)) k = mkFunTyMany af (varType tv) k mk (Bndr tv (NamedTCB vis)) k = mkForAllTy tv vis k tyConInvisTVBinders :: [TyConBinder] -- From the TyCon @@ -2213,6 +2214,7 @@ kindTyConKeys :: UniqSet Unique kindTyConKeys = unionManyUniqSets ( mkUniqSet [ liftedTypeKindTyConKey, constraintKindTyConKey, tYPETyConKey ] : map (mkUniqSet . tycon_with_datacons) [ runtimeRepTyCon + , multiplicityTyCon , vecCountTyCon, vecElemTyCon ] ) where tycon_with_datacons tc = getUnique tc : map getUnique (tyConDataCons tc) @@ -2410,7 +2412,7 @@ tyConRoles :: TyCon -> [Role] -- See also Note [TyCon Role signatures] tyConRoles tc = case tc of - { FunTyCon {} -> [Nominal, Nominal, Representational, Representational] + { FunTyCon {} -> [Nominal, Nominal, Nominal, Representational, Representational] ; AlgTyCon { tcRoles = roles } -> roles ; SynonymTyCon { tcRoles = roles } -> roles ; FamilyTyCon {} -> const_role Nominal diff --git a/compiler/GHC/Core/TyCon.hs-boot b/compiler/GHC/Core/TyCon.hs-boot index 1081249d19..c561da08f9 100644 --- a/compiler/GHC/Core/TyCon.hs-boot +++ b/compiler/GHC/Core/TyCon.hs-boot @@ -1,9 +1,12 @@ module GHC.Core.TyCon where import GHC.Prelude +import GHC.Types.Unique ( Uniquable ) data TyCon +instance Uniquable TyCon + isTupleTyCon :: TyCon -> Bool isUnboxedTupleTyCon :: TyCon -> Bool isFunTyCon :: TyCon -> Bool diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index a183308526..bdf9ba21da 100644 --- a/compiler/GHC/Core/Type.hs +++ b/compiler/GHC/Core/Type.hs @@ -19,6 +19,7 @@ module GHC.Core.Type ( Specificity(..), KindOrType, PredType, ThetaType, Var, TyVar, isTyVar, TyCoVar, TyCoBinder, TyCoVarBinder, TyVarBinder, + Mult, Scaled, KnotTied, -- ** Constructing and deconstructing types @@ -28,7 +29,10 @@ module GHC.Core.Type ( mkAppTy, mkAppTys, splitAppTy, splitAppTys, repSplitAppTys, splitAppTy_maybe, repSplitAppTy_maybe, tcRepSplitAppTy_maybe, - mkVisFunTy, mkInvisFunTy, mkVisFunTys, mkInvisFunTys, + mkVisFunTy, mkInvisFunTy, + mkVisFunTys, + mkVisFunTyMany, mkInvisFunTyMany, + mkVisFunTysMany, mkInvisFunTysMany, splitFunTy, splitFunTy_maybe, splitFunTys, funResultTy, funArgTy, @@ -93,7 +97,7 @@ module GHC.Core.Type ( -- ** Binders sameVis, mkTyCoVarBinder, mkTyCoVarBinders, - mkTyVarBinders, + mkTyVarBinder, mkTyVarBinders, tyVarSpecToBinders, mkAnonBinder, isAnonTyCoBinder, @@ -106,7 +110,7 @@ module GHC.Core.Type ( tyConBindersTyCoBinders, -- ** Common type constructors - funTyCon, + funTyCon, unrestrictedFunTyCon, -- ** Predicates on types isTyVarTy, isFunTy, isCoercionTy, @@ -129,6 +133,11 @@ module GHC.Core.Type ( dropRuntimeRepArgs, getRuntimeRep, + -- Multiplicity + + isMultiplicityTy, isMultiplicityVar, + isLinearType, + -- * Main data types representing Kinds Kind, @@ -196,10 +205,10 @@ module GHC.Core.Type ( isEmptyTCvSubst, unionTCvSubst, -- ** Performing substitution on types and kinds - substTy, substTys, substTyWith, substTysWith, substTheta, + substTy, substTys, substScaledTy, substScaledTys, substTyWith, substTysWith, substTheta, substTyAddInScope, - substTyUnchecked, substTysUnchecked, substThetaUnchecked, - substTyWithUnchecked, + substTyUnchecked, substTysUnchecked, substScaledTyUnchecked, substScaledTysUnchecked, + substThetaUnchecked, substTyWithUnchecked, substCoUnchecked, substCoWithUnchecked, substTyVarBndr, substTyVarBndrs, substTyVar, substTyVars, substVarBndr, substVarBndrs, @@ -235,6 +244,7 @@ import GHC.Core.TyCo.Rep import GHC.Core.TyCo.Subst import GHC.Core.TyCo.Tidy import GHC.Core.TyCo.FVs +import GHC.Core.Multiplicity -- friends: import GHC.Types.Var @@ -248,7 +258,8 @@ import {-# SOURCE #-} GHC.Builtin.Types ( listTyCon, typeNatKind , typeSymbolKind, liftedTypeKind , liftedTypeKindTyCon - , constraintKind ) + , constraintKind + , unrestrictedFunTyCon ) import GHC.Types.Name( Name ) import GHC.Builtin.Names import GHC.Core.Coercion.Axiom @@ -425,8 +436,8 @@ expandTypeSynonyms ty go _ (LitTy l) = LitTy l go subst (TyVarTy tv) = substTyVar subst tv go subst (AppTy t1 t2) = mkAppTy (go subst t1) (go subst t2) - go subst ty@(FunTy _ arg res) - = ty { ft_arg = go subst arg, ft_res = go subst res } + go subst ty@(FunTy _ mult arg res) + = ty { ft_mult = go subst mult, ft_arg = go subst arg, ft_res = go subst res } go subst (ForAllTy (Bndr tv vis) t) = let (subst', tv') = substVarBndrUsing go subst tv in ForAllTy (Bndr tv' vis) (go subst' t) @@ -448,8 +459,8 @@ expandTypeSynonyms ty go_co subst (ForAllCo tv kind_co co) = let (subst', tv', kind_co') = go_cobndr subst tv kind_co in mkForAllCo tv' kind_co' (go_co subst' co) - go_co subst (FunCo r co1 co2) - = mkFunCo r (go_co subst co1) (go_co subst co2) + go_co subst (FunCo r w co1 co2) + = mkFunCo r (go_co subst w) (go_co subst co1) (go_co subst co2) go_co subst (CoVarCo cv) = substCoVar subst cv go_co subst (AxiomInstCo ax ind args) @@ -559,6 +570,28 @@ isRuntimeRepTy _ = False isRuntimeRepVar :: TyVar -> Bool isRuntimeRepVar = isRuntimeRepTy . tyVarKind +-- | Is this the type 'Multiplicity'? +isMultiplicityTy :: Type -> Bool +isMultiplicityTy ty | Just ty' <- coreView ty = isMultiplicityTy ty' +isMultiplicityTy (TyConApp tc []) = tc `hasKey` multiplicityTyConKey +isMultiplicityTy _ = False + +-- | Is a tyvar of type 'Multiplicity'? +isMultiplicityVar :: TyVar -> Bool +isMultiplicityVar = isMultiplicityTy . tyVarKind + +isLinearType :: Type -> Bool +-- ^ @isLinear t@ returns @True@ of a if @t@ is a type of (curried) function +-- where at least one argument is linear (or otherwise non-unrestricted). We use +-- this function to check whether it is safe to eta reduce an Id in CorePrep. It +-- is always safe to return 'True', because 'True' deactivates the optimisation. +isLinearType ty = case ty of + FunTy _ Many _ res -> isLinearType res + FunTy _ _ _ _ -> True + ForAllTy _ res -> isLinearType res + _ + | Just ty' <- coreView ty -> isLinearType ty' + | otherwise -> False {- ********************************************************************* * * @@ -655,9 +688,9 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar go_ty env (CastTy ty co) = mkCastTy <$> go_ty env ty <*> go_co env co go_ty env (CoercionTy co) = CoercionTy <$> go_co env co - go_ty env ty@(FunTy _ arg res) - = do { arg' <- go_ty env arg; res' <- go_ty env res - ; return (ty { ft_arg = arg', ft_res = res' }) } + go_ty env ty@(FunTy _ w arg res) + = do { w' <- go_ty env w; arg' <- go_ty env arg; res' <- go_ty env res + ; return (ty { ft_mult = w', ft_arg = arg', ft_res = res' }) } go_ty env ty@(TyConApp tc tys) | isTcTyCon tc @@ -685,7 +718,7 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar go_co env (Refl ty) = Refl <$> go_ty env ty go_co env (GRefl r ty mco) = mkGReflCo r <$> go_ty env ty <*> go_mco env mco go_co env (AppCo c1 c2) = mkAppCo <$> go_co env c1 <*> go_co env c2 - go_co env (FunCo r c1 c2) = mkFunCo r <$> go_co env c1 <*> go_co env c2 + go_co env (FunCo r cw c1 c2) = mkFunCo r <$> go_co env cw <*> go_co env c1 <*> go_co env c2 go_co env (CoVarCo cv) = covar env cv go_co env (HoleCo hole) = cohole env hole go_co env (UnivCo p r t1 t2) = mkUnivCo <$> go_prov env p <*> pure r @@ -844,8 +877,8 @@ splitAppTy_maybe ty = repSplitAppTy_maybe ty repSplitAppTy_maybe :: HasDebugCallStack => Type -> Maybe (Type,Type) -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that -- any Core view stuff is already done -repSplitAppTy_maybe (FunTy _ ty1 ty2) - = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2) +repSplitAppTy_maybe (FunTy _ w ty1 ty2) + = Just (TyConApp funTyCon [w, rep1, rep2, ty1], ty2) where rep1 = getRuntimeRep ty1 rep2 = getRuntimeRep ty2 @@ -866,12 +899,11 @@ repSplitAppTy_maybe _other = Nothing tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type) -- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that -- any coreView stuff is already done. Refuses to look through (c => t) -tcRepSplitAppTy_maybe (FunTy { ft_af = af, ft_arg = ty1, ft_res = ty2 }) +tcRepSplitAppTy_maybe (FunTy { ft_af = af, ft_mult = w, ft_arg = ty1, ft_res = ty2 }) | InvisArg <- af = Nothing -- See Note [Decomposing fat arrow c=>t] - | otherwise - = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2) + = Just (TyConApp funTyCon [w, rep1, rep2, ty1], ty2) where rep1 = getRuntimeRep ty1 rep2 = getRuntimeRep ty2 @@ -907,9 +939,9 @@ splitAppTys ty = split ty ty [] (tc_args1, tc_args2) = splitAt n tc_args in (TyConApp tc tc_args1, tc_args2 ++ args) - split _ (FunTy _ ty1 ty2) args + split _ (FunTy _ w ty1 ty2) args = ASSERT( null args ) - (TyConApp funTyCon [], [rep1, rep2, ty1, ty2]) + (TyConApp funTyCon [], [w, rep1, rep2, ty1, ty2]) where rep1 = getRuntimeRep ty1 rep2 = getRuntimeRep ty2 @@ -927,9 +959,9 @@ repSplitAppTys ty = split ty [] (tc_args1, tc_args2) = splitAt n tc_args in (TyConApp tc tc_args1, tc_args2 ++ args) - split (FunTy _ ty1 ty2) args + split (FunTy _ w ty1 ty2) args = ASSERT( null args ) - (TyConApp funTyCon [], [rep1, rep2, ty1, ty2]) + (TyConApp funTyCon [], [w, rep1, rep2, ty1, ty2]) where rep1 = getRuntimeRep ty1 rep2 = getRuntimeRep ty2 @@ -1041,25 +1073,25 @@ In the compiler we maintain the invariant that all saturated applications of See #11714. -} -splitFunTy :: Type -> (Type, Type) +splitFunTy :: Type -> (Scaled Type, Type) -- ^ Attempts to extract the argument and result types from a type, and -- panics if that is not possible. See also 'splitFunTy_maybe' splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty' -splitFunTy (FunTy _ arg res) = (arg, res) -splitFunTy other = pprPanic "splitFunTy" (ppr other) +splitFunTy (FunTy _ w arg res) = (Scaled w arg, res) +splitFunTy other = pprPanic "splitFunTy" (ppr other) -splitFunTy_maybe :: Type -> Maybe (Type, Type) +splitFunTy_maybe :: Type -> Maybe (Scaled Type, Type) -- ^ Attempts to extract the argument and result types from a type splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty' -splitFunTy_maybe (FunTy _ arg res) = Just (arg, res) -splitFunTy_maybe _ = Nothing +splitFunTy_maybe (FunTy _ w arg res) = Just (Scaled w arg, res) +splitFunTy_maybe _ = Nothing -splitFunTys :: Type -> ([Type], Type) +splitFunTys :: Type -> ([Scaled Type], Type) splitFunTys ty = split [] ty ty where split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty' - split args _ (FunTy _ arg res) = split (arg:args) res res - split args orig_ty _ = (reverse args, orig_ty) + split args _ (FunTy _ w arg res) = split ((Scaled w arg):args) res res + split args orig_ty _ = (reverse args, orig_ty) funResultTy :: Type -> Type -- ^ Extract the function result type and panic if that is not possible @@ -1237,9 +1269,10 @@ compilation. In order to avoid a potentially expensive series of checks in mkTyConApp :: TyCon -> [Type] -> Type mkTyConApp tycon tys | isFunTyCon tycon - , [_rep1,_rep2,ty1,ty2] <- tys + , [w, _rep1,_rep2,ty1,ty2] <- tys -- The FunTyCon (->) is always a visible one - = FunTy { ft_af = VisArg, ft_arg = ty1, ft_res = ty2 } + = FunTy { ft_af = VisArg, ft_mult = w, ft_arg = ty1, ft_res = ty2 } + -- Note [mkTyConApp and Type] | tycon == liftedTypeKindTyCon = ASSERT2( null tys, ppr tycon $$ ppr tys ) @@ -1279,10 +1312,10 @@ tyConAppTyCon ty = tyConAppTyCon_maybe ty `orElse` pprPanic "tyConAppTyCon" (ppr tyConAppArgs_maybe :: Type -> Maybe [Type] tyConAppArgs_maybe ty | Just ty' <- coreView ty = tyConAppArgs_maybe ty' tyConAppArgs_maybe (TyConApp _ tys) = Just tys -tyConAppArgs_maybe (FunTy _ arg res) +tyConAppArgs_maybe (FunTy _ w arg res) | Just rep1 <- getRuntimeRep_maybe arg , Just rep2 <- getRuntimeRep_maybe res - = Just [rep1, rep2, arg, res] + = Just [w, rep1, rep2, arg, res] tyConAppArgs_maybe _ = Nothing tyConAppArgs :: Type -> [Type] @@ -1333,10 +1366,10 @@ repSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type]) -- see Note [FunTy and decomposing tycon applications] in GHC.Tc.Solver.Canonical -- repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys) -repSplitTyConApp_maybe (FunTy _ arg res) +repSplitTyConApp_maybe (FunTy _ w arg res) | Just arg_rep <- getRuntimeRep_maybe arg , Just res_rep <- getRuntimeRep_maybe res - = Just (funTyCon, [arg_rep, res_rep, arg, res]) + = Just (funTyCon, [w, arg_rep, res_rep, arg, res]) repSplitTyConApp_maybe _ = Nothing ------------------- @@ -1404,7 +1437,7 @@ tyConBindersTyCoBinders :: [TyConBinder] -> [TyCoBinder] tyConBindersTyCoBinders = map to_tyb where to_tyb (Bndr tv (NamedTCB vis)) = Named (Bndr tv vis) - to_tyb (Bndr tv (AnonTCB af)) = Anon af (varType tv) + to_tyb (Bndr tv (AnonTCB af)) = Anon af (tymult (varType tv)) -- | Drop the cast on a type, if any. If there is no -- cast, just return the original type. This is rarely what @@ -1474,7 +1507,7 @@ mkTyCoInvForAllTy :: TyCoVar -> Type -> Type mkTyCoInvForAllTy tv ty | isCoVar tv , not (tv `elemVarSet` tyCoVarsOfType ty) - = mkVisFunTy (varType tv) ty + = mkVisFunTyMany (varType tv) ty | otherwise = ForAllTy (Bndr tv Inferred) ty @@ -1529,18 +1562,21 @@ mkLamType v body_ty = ForAllTy (Bndr v Required) body_ty | otherwise - = mkFunctionType (varType v) body_ty + = mkFunctionType arg_mult arg_ty body_ty + where + Scaled arg_mult arg_ty = varScaledType v -mkFunctionType :: Type -> Type -> Type +mkFunctionType :: Mult -> Type -> Type -> Type -- This one works out the AnonArgFlag from the argument type -- See GHC.Types.Var Note [AnonArgFlag] -mkFunctionType arg_ty res_ty +mkFunctionType mult arg_ty res_ty | isPredTy arg_ty -- See GHC.Types.Var Note [AnonArgFlag] - = mkInvisFunTy arg_ty res_ty + = ASSERT(eqType mult Many) + mkInvisFunTy mult arg_ty res_ty | otherwise - = mkVisFunTy arg_ty res_ty + = mkVisFunTy mult arg_ty res_ty -- | Given a list of type-level vars and the free vars of a result kind, -- makes TyCoBinders, preferring anonymous binders @@ -1705,8 +1741,8 @@ splitPiTy_maybe ty = go ty where go ty | Just ty' <- coreView ty = go ty' go (ForAllTy bndr ty) = Just (Named bndr, ty) - go (FunTy { ft_af = af, ft_arg = arg, ft_res = res}) - = Just (Anon af arg, res) + go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res}) + = Just (Anon af (mkScaled w arg), res) go _ = Nothing -- | Takes a forall type apart, or panics @@ -1722,8 +1758,8 @@ splitPiTys ty = split ty ty [] where split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs split _ (ForAllTy b res) bs = split res res (Named b : bs) - split _ (FunTy { ft_af = af, ft_arg = arg, ft_res = res }) bs - = split res res (Anon af arg : bs) + split _ (FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res }) bs + = split res res (Anon af (Scaled w arg) : bs) split orig_ty _ bs = (reverse bs, orig_ty) -- | Like 'splitPiTys' but split off only /named/ binders @@ -1753,8 +1789,8 @@ splitPiTysInvisible ty = split ty ty [] split _ (ForAllTy b res) bs | Bndr _ vis <- b , isInvisibleArgFlag vis = split res res (Named b : bs) - split _ (FunTy { ft_af = InvisArg, ft_arg = arg, ft_res = res }) bs - = split res res (Anon InvisArg arg : bs) + split _ (FunTy { ft_af = InvisArg, ft_mult = mult, ft_arg = arg, ft_res = res }) bs + = split res res (Anon InvisArg (mkScaled mult arg) : bs) split orig_ty _ bs = (reverse bs, orig_ty) splitPiTysInvisibleN :: Int -> Type -> ([TyCoBinder], Type) @@ -1769,8 +1805,8 @@ splitPiTysInvisibleN n ty = split n ty ty [] | ForAllTy b res <- ty , Bndr _ vis <- b , isInvisibleArgFlag vis = split (n-1) res res (Named b : bs) - | FunTy { ft_af = InvisArg, ft_arg = arg, ft_res = res } <- ty - = split (n-1) res res (Anon InvisArg arg : bs) + | FunTy { ft_af = InvisArg, ft_mult = mult, ft_arg = arg, ft_res = res } <- ty + = split (n-1) res res (Anon InvisArg (Scaled mult arg) : bs) | otherwise = (reverse bs, orig_ty) -- | Given a 'TyCon' and a list of argument types, filter out any invisible @@ -1875,9 +1911,9 @@ isTauTy (TyVarTy _) = True isTauTy (LitTy {}) = True isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc isTauTy (AppTy a b) = isTauTy a && isTauTy b -isTauTy (FunTy af a b) = case af of - InvisArg -> False -- e.g., Eq a => b - VisArg -> isTauTy a && isTauTy b -- e.g., a -> b +isTauTy (FunTy af w a b) = case af of + InvisArg -> False -- e.g., Eq a => b + VisArg -> isTauTy w && isTauTy a && isTauTy b -- e.g., a -> b isTauTy (ForAllTy {}) = False isTauTy (CastTy ty _) = isTauTy ty isTauTy (CoercionTy _) = False -- Not sure about this @@ -1905,7 +1941,7 @@ isAtomicTy _ = False -} -- | Make an anonymous binder -mkAnonBinder :: AnonArgFlag -> Type -> TyCoBinder +mkAnonBinder :: AnonArgFlag -> Scaled Type -> TyCoBinder mkAnonBinder = Anon -- | Does this binder bind a variable that is /not/ erased? Returns @@ -1920,18 +1956,18 @@ tyCoBinderVar_maybe _ = Nothing tyCoBinderType :: TyCoBinder -> Type tyCoBinderType (Named tvb) = binderType tvb -tyCoBinderType (Anon _ ty) = ty +tyCoBinderType (Anon _ ty) = scaledThing ty tyBinderType :: TyBinder -> Type tyBinderType (Named (Bndr tv _)) = ASSERT( isTyVar tv ) tyVarKind tv -tyBinderType (Anon _ ty) = ty +tyBinderType (Anon _ ty) = scaledThing ty -- | Extract a relevant type, if there is one. binderRelevantType_maybe :: TyCoBinder -> Maybe Type -binderRelevantType_maybe (Named {}) = Nothing -binderRelevantType_maybe (Anon _ ty) = Just ty +binderRelevantType_maybe (Named {}) = Nothing +binderRelevantType_maybe (Anon _ ty) = Just (scaledThing ty) {- ************************************************************************ @@ -1972,7 +2008,7 @@ isFamFreeTy (TyVarTy _) = True isFamFreeTy (LitTy {}) = True isFamFreeTy (TyConApp tc tys) = all isFamFreeTy tys && isFamFreeTyCon tc isFamFreeTy (AppTy a b) = isFamFreeTy a && isFamFreeTy b -isFamFreeTy (FunTy _ a b) = isFamFreeTy a && isFamFreeTy b +isFamFreeTy (FunTy _ w a b) = isFamFreeTy w && isFamFreeTy a && isFamFreeTy b isFamFreeTy (ForAllTy _ ty) = isFamFreeTy ty isFamFreeTy (CastTy ty _) = isFamFreeTy ty isFamFreeTy (CoercionTy _) = False -- Not sure about this @@ -2192,7 +2228,7 @@ seqType :: Type -> () seqType (LitTy n) = n `seq` () seqType (TyVarTy tv) = tv `seq` () seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2 -seqType (FunTy _ t1 t2) = seqType t1 `seq` seqType t2 +seqType (FunTy _ w t1 t2) = seqType w `seq` seqType t1 `seq` seqType t2 seqType (TyConApp tc tys) = tc `seq` seqTypes tys seqType (ForAllTy (Bndr tv _) ty) = seqType (varType tv) `seq` seqType ty seqType (CastTy ty co) = seqType ty `seq` seqCo co @@ -2345,8 +2381,9 @@ nonDetCmpTypeX env orig_t1 orig_t2 = go env ty1 (AppTy s2 t2) | Just (s1, t1) <- repSplitAppTy_maybe ty1 = go env s1 s2 `thenCmpTy` go env t1 t2 - go env (FunTy _ s1 t1) (FunTy _ s2 t2) - = go env s1 s2 `thenCmpTy` go env t1 t2 + go env (FunTy _ w1 s1 t1) (FunTy _ w2 s2 t2) + = go env w1 w2 `thenCmpTy` + go env s1 s2 `thenCmpTy` go env t1 t2 go env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = liftOrdering (tc1 `nonDetCmpTc` tc2) `thenCmpTy` gos env tys1 tys2 go _ (LitTy l1) (LitTy l2) = liftOrdering (compare l1 l2) @@ -2707,10 +2744,11 @@ occCheckExpand vs_to_avoid ty go cxt (AppTy ty1 ty2) = do { ty1' <- go cxt ty1 ; ty2' <- go cxt ty2 ; return (mkAppTy ty1' ty2') } - go cxt ty@(FunTy _ ty1 ty2) - = do { ty1' <- go cxt ty1 + go cxt ty@(FunTy _ w ty1 ty2) + = do { w' <- go cxt w + ; ty1' <- go cxt ty1 ; ty2' <- go cxt ty2 - ; return (ty { ft_arg = ty1', ft_res = ty2' }) } + ; return (ty { ft_mult = w', ft_arg = ty1', ft_res = ty2' }) } go cxt@(as, env) (ForAllTy (Bndr tv vis) body_ty) = do { ki' <- go cxt (varType tv) ; let tv' = setVarType tv ki' @@ -2737,8 +2775,7 @@ occCheckExpand vs_to_avoid ty ; return (mkCoercionTy co') } ------------------ - go_var cxt v = do { k' <- go cxt (varType v) - ; return (setVarType v k') } + go_var cxt v = updateVarTypeAndMultM (go cxt) v -- Works for TyVar and CoVar -- See Note [Occurrence checking: look inside kinds] @@ -2766,9 +2803,10 @@ occCheckExpand vs_to_avoid ty as' = as `delVarSet` tv ; body' <- go_co (as', env') body_co ; return (ForAllCo tv' kind_co' body') } - go_co cxt (FunCo r co1 co2) = do { co1' <- go_co cxt co1 + go_co cxt (FunCo r w co1 co2) = do { co1' <- go_co cxt co1 ; co2' <- go_co cxt co2 - ; return (mkFunCo r co1' co2') } + ; w' <- go_co cxt w + ; return (mkFunCo r w' co1' co2') } go_co cxt@(as,env) (CoVarCo c) | c `elemVarSet` as = Nothing | Just c' <- lookupVarEnv env c = return (mkCoVarCo c') @@ -2828,7 +2866,8 @@ tyConsOfType ty go (LitTy {}) = emptyUniqSet go (TyConApp tc tys) = go_tc tc `unionUniqSets` go_s tys go (AppTy a b) = go a `unionUniqSets` go b - go (FunTy _ a b) = go a `unionUniqSets` go b `unionUniqSets` go_tc funTyCon + go (FunTy _ w a b) = go w `unionUniqSets` + go a `unionUniqSets` go b `unionUniqSets` go_tc funTyCon go (ForAllTy (Bndr tv _) ty) = go ty `unionUniqSets` go (varType tv) go (CastTy ty co) = go ty `unionUniqSets` go_co co go (CoercionTy co) = go_co co @@ -2838,7 +2877,7 @@ tyConsOfType ty go_co (TyConAppCo _ tc args) = go_tc tc `unionUniqSets` go_cos args go_co (AppCo co arg) = go_co co `unionUniqSets` go_co arg go_co (ForAllCo _ kind_co co) = go_co kind_co `unionUniqSets` go_co co - go_co (FunCo _ co1 co2) = go_co co1 `unionUniqSets` go_co co2 + go_co (FunCo _ co_mult co1 co2) = go_co co_mult `unionUniqSets` go_co co1 `unionUniqSets` go_co co2 go_co (AxiomInstCo ax _ args) = go_ax ax `unionUniqSets` go_cos args go_co (UnivCo p _ t1 t2) = go_prov p `unionUniqSets` go t1 `unionUniqSets` go t2 go_co (CoVarCo {}) = emptyUniqSet @@ -2886,7 +2925,7 @@ splitVisVarsOfType orig_ty = Pair invis_vars vis_vars go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv) go (AppTy t1 t2) = go t1 `mappend` go t2 go (TyConApp tc tys) = go_tc tc tys - go (FunTy _ t1 t2) = go t1 `mappend` go t2 + go (FunTy _ w t1 t2) = go w `mappend` go t1 `mappend` go t2 go (ForAllTy (Bndr tv _) ty) = ((`delVarSet` tv) <$> go ty) `mappend` (invisible (tyCoVarsOfType $ varType tv)) @@ -2971,7 +3010,7 @@ isKindLevPoly k = ASSERT2( isLiftedTypeKind k || _is_type, ppr k ) go AppTy{} = True -- it can't be a TyConApp go (TyConApp tc tys) = isFamilyTyCon tc || any go tys go ForAllTy{} = True - go (FunTy _ t1 t2) = go t1 || go t2 + go (FunTy _ w t1 t2) = go w || go t1 || go t2 go LitTy{} = False go CastTy{} = True go CoercionTy{} = True diff --git a/compiler/GHC/Core/Type.hs-boot b/compiler/GHC/Core/Type.hs-boot index 08efbf608d..1faf4304ab 100644 --- a/compiler/GHC/Core/Type.hs-boot +++ b/compiler/GHC/Core/Type.hs-boot @@ -3,7 +3,7 @@ module GHC.Core.Type where import GHC.Prelude -import GHC.Core.TyCon +import {-# SOURCE #-} GHC.Core.TyCon import {-# SOURCE #-} GHC.Core.TyCo.Rep( Type, Coercion ) import GHC.Utils.Misc @@ -19,8 +19,11 @@ eqType :: Type -> Type -> Bool coreView :: Type -> Maybe Type tcView :: Type -> Maybe Type isRuntimeRepTy :: Type -> Bool +isMultiplicityTy :: Type -> Bool isLiftedTypeKind :: Type -> Bool splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type]) +mkTyConApp :: TyCon -> [Type] -> Type + partitionInvisibleTypes :: TyCon -> [Type] -> ([Type], [Type]) diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs index 8eac3fbf63..84aa76d573 100644 --- a/compiler/GHC/Core/Unify.hs +++ b/compiler/GHC/Core/Unify.hs @@ -1041,7 +1041,9 @@ unify_ty env (CoercionTy co1) (CoercionTy co2) kco , not (cv `elemVarEnv` c_subst) , BindMe <- tvBindFlag env cv -> do { checkRnEnv env (tyCoVarsOfCo co2) - ; let (co_l, co_r) = decomposeFunCo Nominal kco + ; let (_, co_l, co_r) = decomposeFunCo Nominal kco + -- Because the coercion is nominal, it should be safe to + -- ignore the multiplicity coercion. -- cv :: t1 ~ t2 -- co2 :: s1 ~ s2 -- co_l :: t1 ~ s1 @@ -1463,15 +1465,15 @@ ty_co_match menv subst ty1 (AppCo co2 arg2) _lkco _rkco ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo _ tc2 cos) _lkco _rkco = ty_co_match_tc menv subst tc1 tys tc2 cos -ty_co_match menv subst (FunTy _ ty1 ty2) co _lkco _rkco - -- Despite the fact that (->) is polymorphic in four type variables (two - -- runtime rep and two types), we shouldn't need to explicitly unify the - -- runtime reps here; unifying the types themselves should be sufficient. - -- See Note [Representation of function types]. - | Just (tc, [_,_,co1,co2]) <- splitTyConAppCo_maybe co +ty_co_match menv subst (FunTy _ w ty1 ty2) co _lkco _rkco + -- Despite the fact that (->) is polymorphic in five type variables (two + -- runtime rep, a multiplicity and two types), we shouldn't need to + -- explicitly unify the runtime reps here; unifying the types themselves + -- should be sufficient. See Note [Representation of function types]. + | Just (tc, [co_mult, _,_,co1,co2]) <- splitTyConAppCo_maybe co , tc == funTyCon - = let Pair lkcos rkcos = traverse (fmap mkNomReflCo . coercionKind) [co1,co2] - in ty_co_match_args menv subst [ty1, ty2] [co1, co2] lkcos rkcos + = let Pair lkcos rkcos = traverse (fmap mkNomReflCo . coercionKind) [co_mult,co1,co2] + in ty_co_match_args menv subst [w, ty1, ty2] [co_mult, co1, co2] lkcos rkcos ty_co_match menv subst (ForAllTy (Bndr tv1 _) ty1) (ForAllCo tv2 kind_co2 co2) @@ -1575,10 +1577,10 @@ pushRefl co = case (isReflCo_maybe co) of Just (AppTy ty1 ty2, Nominal) -> Just (AppCo (mkReflCo Nominal ty1) (mkNomReflCo ty2)) - Just (FunTy _ ty1 ty2, r) + Just (FunTy _ w ty1 ty2, r) | Just rep1 <- getRuntimeRep_maybe ty1 , Just rep2 <- getRuntimeRep_maybe ty2 - -> Just (TyConAppCo r funTyCon [ mkReflCo r rep1, mkReflCo r rep2 + -> Just (TyConAppCo r funTyCon [ multToCo w, mkReflCo r rep1, mkReflCo r rep2 , mkReflCo r ty1, mkReflCo r ty2 ]) Just (TyConApp tc tys, r) -> Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys)) diff --git a/compiler/GHC/Core/UsageEnv.hs b/compiler/GHC/Core/UsageEnv.hs new file mode 100644 index 0000000000..a03343ee9f --- /dev/null +++ b/compiler/GHC/Core/UsageEnv.hs @@ -0,0 +1,90 @@ +{-# LANGUAGE ViewPatterns #-} +module GHC.Core.UsageEnv (UsageEnv, addUsage, scaleUsage, zeroUE, + lookupUE, scaleUE, deleteUE, addUE, Usage(..), unitUE, + supUE, supUEs) where + +import Data.Foldable +import GHC.Prelude +import GHC.Core.Multiplicity +import GHC.Types.Name +import GHC.Types.Name.Env +import GHC.Utils.Outputable + +-- +-- * Usage environments +-- + +-- The typechecker and the linter output usage environments. See Note [Usages] +-- in Multiplicity. Every absent name being considered to map to 'Zero' of +-- 'Bottom' depending on a flag. See Note [Zero as a usage] in Multiplicity, see +-- Note [Bottom as a usage] in Multiplicity. + +data Usage = Zero | Bottom | MUsage Mult + +instance Outputable Usage where + ppr Zero = text "0" + ppr Bottom = text "Bottom" + ppr (MUsage x) = ppr x + +addUsage :: Usage -> Usage -> Usage +addUsage Zero x = x +addUsage x Zero = x +addUsage Bottom x = x +addUsage x Bottom = x +addUsage (MUsage x) (MUsage y) = MUsage $ mkMultAdd x y + +scaleUsage :: Mult -> Usage -> Usage +scaleUsage One Bottom = Bottom +scaleUsage _ Zero = Zero +scaleUsage x Bottom = MUsage x +scaleUsage x (MUsage y) = MUsage $ mkMultMul x y + +-- For now, we use extra multiplicity Bottom for empty case. +data UsageEnv = UsageEnv (NameEnv Mult) Bool + +unitUE :: NamedThing n => n -> Mult -> UsageEnv +unitUE x w = UsageEnv (unitNameEnv (getName x) w) False + +zeroUE, bottomUE :: UsageEnv +zeroUE = UsageEnv emptyNameEnv False + +bottomUE = UsageEnv emptyNameEnv True + +addUE :: UsageEnv -> UsageEnv -> UsageEnv +addUE (UsageEnv e1 b1) (UsageEnv e2 b2) = + UsageEnv (plusNameEnv_C mkMultAdd e1 e2) (b1 || b2) + +scaleUE :: Mult -> UsageEnv -> UsageEnv +scaleUE One ue = ue +scaleUE w (UsageEnv e _) = + UsageEnv (mapNameEnv (mkMultMul w) e) False + +supUE :: UsageEnv -> UsageEnv -> UsageEnv +supUE (UsageEnv e1 False) (UsageEnv e2 False) = + UsageEnv (plusNameEnv_CD mkMultSup e1 Many e2 Many) False +supUE (UsageEnv e1 b1) (UsageEnv e2 b2) = UsageEnv (plusNameEnv_CD2 combineUsage e1 e2) (b1 && b2) + where combineUsage (Just x) (Just y) = mkMultSup x y + combineUsage Nothing (Just x) | b1 = x + | otherwise = Many + combineUsage (Just x) Nothing | b2 = x + | otherwise = Many + combineUsage Nothing Nothing = pprPanic "supUE" (ppr e1 <+> ppr e2) +-- Note: If you are changing this logic, check 'mkMultSup' in Multiplicity as well. + +supUEs :: [UsageEnv] -> UsageEnv +supUEs = foldr supUE bottomUE + + +deleteUE :: NamedThing n => UsageEnv -> n -> UsageEnv +deleteUE (UsageEnv e b) x = UsageEnv (delFromNameEnv e (getName x)) b + +-- | |lookupUE x env| returns the multiplicity assigned to |x| in |env|, if |x| is not +-- bound in |env|, then returns |Zero| or |Bottom|. +lookupUE :: NamedThing n => UsageEnv -> n -> Usage +lookupUE (UsageEnv e has_bottom) x = + case lookupNameEnv e (getName x) of + Just w -> MUsage w + Nothing -> if has_bottom then Bottom else Zero + +instance Outputable UsageEnv where + ppr (UsageEnv ne b) = text "UsageEnv:" <+> ppr ne <+> ppr b diff --git a/compiler/GHC/Core/Utils.hs b/compiler/GHC/Core/Utils.hs index 700ab14b1e..9748dd2753 100644 --- a/compiler/GHC/Core/Utils.hs +++ b/compiler/GHC/Core/Utils.hs @@ -20,6 +20,7 @@ module GHC.Core.Utils ( findDefault, addDefault, findAlt, isDefaultAlt, mergeAlts, trimConArgs, filterAlts, combineIdenticalAlts, refineDefaultAlt, + scaleAltsBy, -- * Properties of expressions exprType, coreAltType, coreAltsType, isExprLevPoly, @@ -88,6 +89,7 @@ import GHC.Core.Predicate import GHC.Core.TyCo.Rep( TyCoBinder(..), TyBinder ) import GHC.Core.Coercion import GHC.Core.TyCon +import GHC.Core.Multiplicity import GHC.Types.Unique import GHC.Utils.Outputable import GHC.Builtin.Types.Prim @@ -237,7 +239,7 @@ applyTypeToArgs e op_ty args go op_ty (Coercion co : args) = go_ty_args op_ty [mkCoercionTy co] args go op_ty (_ : args) | Just (_, res_ty) <- splitFunTy_maybe op_ty = go res_ty args - go _ _ = pprPanic "applyTypeToArgs" panic_msg + go _ args = pprPanic "applyTypeToArgs" (panic_msg args) -- go_ty_args: accumulate type arguments so we can -- instantiate all at once with piResultTys @@ -248,9 +250,10 @@ applyTypeToArgs e op_ty args go_ty_args op_ty rev_tys args = go (piResultTys op_ty (reverse rev_tys)) args - panic_msg = vcat [ text "Expression:" <+> pprCoreExpr e + panic_msg as = vcat [ text "Expression:" <+> pprCoreExpr e , text "Type:" <+> ppr op_ty - , text "Args:" <+> ppr args ] + , text "Args:" <+> ppr args + , text "Args':" <+> ppr as ] {- @@ -295,7 +298,8 @@ mkCast expr co WARN( not (from_ty `eqType` exprType expr), text "Trying to coerce" <+> text "(" <> ppr expr $$ text "::" <+> ppr (exprType expr) <> text ")" - $$ ppr co $$ ppr (coercionType co) ) + $$ ppr co $$ ppr (coercionType co) + $$ callStackDoc ) (Cast expr co) -- | Wraps the given expression in the source annotation, dropping the @@ -701,12 +705,13 @@ filterAlts _tycon inst_tys imposs_cons alts -- | Refine the default alternative to a 'DataAlt', if there is a unique way to do so. -- See Note [Refine DEFAULT case alternatives] refineDefaultAlt :: [Unique] -- ^ Uniques for constructing new binders + -> Mult -- ^ Multiplicity annotation of the case expression -> TyCon -- ^ Type constructor of scrutinee's type -> [Type] -- ^ Type arguments of scrutinee's type -> [AltCon] -- ^ Constructors that cannot match the DEFAULT (if any) -> [CoreAlt] -> (Bool, [CoreAlt]) -- ^ 'True', if a default alt was replaced with a 'DataAlt' -refineDefaultAlt us tycon tys imposs_deflt_cons all_alts +refineDefaultAlt us mult tycon tys imposs_deflt_cons all_alts | (DEFAULT,_,rhs) : rest_alts <- all_alts , isAlgTyCon tycon -- It's a data type, tuple, or unboxed tuples. , not (isNewTyCon tycon) -- We can have a newtype, if we are just doing an eval: @@ -727,7 +732,7 @@ refineDefaultAlt us tycon tys imposs_deflt_cons all_alts [con] -> (True, mergeAlts rest_alts [(DataAlt con, ex_tvs ++ arg_ids, rhs)]) -- We need the mergeAlts to keep the alternatives in the right order where - (ex_tvs, arg_ids) = dataConRepInstPat us con tys + (ex_tvs, arg_ids) = dataConRepInstPat us mult con tys -- It matches more than one, so do nothing _ -> (False, all_alts) @@ -930,6 +935,18 @@ combineIdenticalAlts imposs_deflt_cons ((con1,bndrs1,rhs1) : rest_alts) combineIdenticalAlts imposs_cons alts = (False, imposs_cons, alts) +-- Scales the multiplicity of the binders of a list of case alternatives. That +-- is, in [C x1…xn -> u], the multiplicity of x1…xn is scaled. +scaleAltsBy :: Mult -> [CoreAlt] -> [CoreAlt] +scaleAltsBy w alts = map scaleAlt alts + where + scaleAlt :: CoreAlt -> CoreAlt + scaleAlt (con, bndrs, rhs) = (con, map scaleBndr bndrs, rhs) + + scaleBndr :: CoreBndr -> CoreBndr + scaleBndr = scaleVarBy w + + {- ********************************************************************* * * exprIsTrivial @@ -1608,7 +1625,7 @@ app_ok primop_ok fun args primop_arg_ok :: TyBinder -> CoreExpr -> Bool primop_arg_ok (Named _) _ = True -- A type argument primop_arg_ok (Anon _ ty) arg -- A term argument - | isUnliftedType ty = expr_ok primop_ok arg + | isUnliftedType (scaledThing ty) = expr_ok primop_ok arg | otherwise = True -- See Note [Primops with lifted arguments] ----------------------------- @@ -1941,18 +1958,19 @@ exprIsTickedString_maybe _ = Nothing These InstPat functions go here to avoid circularity between DataCon and Id -} -dataConRepInstPat :: [Unique] -> DataCon -> [Type] -> ([TyCoVar], [Id]) -dataConRepFSInstPat :: [FastString] -> [Unique] -> DataCon -> [Type] -> ([TyCoVar], [Id]) +dataConRepInstPat :: [Unique] -> Mult -> DataCon -> [Type] -> ([TyCoVar], [Id]) +dataConRepFSInstPat :: [FastString] -> [Unique] -> Mult -> DataCon -> [Type] -> ([TyCoVar], [Id]) dataConRepInstPat = dataConInstPat (repeat ((fsLit "ipv"))) dataConRepFSInstPat = dataConInstPat dataConInstPat :: [FastString] -- A long enough list of FSs to use for names -> [Unique] -- An equally long list of uniques, at least one for each binder + -> Mult -- The multiplicity annotation of the case expression: scales the multiplicity of variables -> DataCon -> [Type] -- Types to instantiate the universally quantified tyvars -> ([TyCoVar], [Id]) -- Return instantiated variables --- dataConInstPat arg_fun fss us con inst_tys returns a tuple +-- dataConInstPat arg_fun fss us mult con inst_tys returns a tuple -- (ex_tvs, arg_ids), -- -- ex_tvs are intended to be used as binders for existential type args @@ -1979,7 +1997,7 @@ dataConInstPat :: [FastString] -- A long enough list of FSs to use for -- -- where the double-primed variables are created with the FastStrings and -- Uniques given as fss and us -dataConInstPat fss uniqs con inst_tys +dataConInstPat fss uniqs mult con inst_tys = ASSERT( univ_tvs `equalLength` inst_tys ) (ex_bndrs, arg_ids) where @@ -2013,9 +2031,9 @@ dataConInstPat fss uniqs con inst_tys -- Make value vars, instantiating types arg_ids = zipWith4 mk_id_var id_uniqs id_fss arg_tys arg_strs - mk_id_var uniq fs ty str + mk_id_var uniq fs (Scaled m ty) str = setCaseBndrEvald str $ -- See Note [Mark evaluated arguments] - mkLocalIdOrCoVar name (Type.substTy full_subst ty) + mkLocalIdOrCoVar name (mult `mkMultMul` m) (Type.substTy full_subst ty) where name = mkInternalName uniq (mkVarOccFS fs) noSrcSpan @@ -2299,6 +2317,14 @@ There are some particularly delicate points here: So it's important to do the right thing. +* With linear types, eta-reduction can break type-checking: + f :: A ⊸ B + g :: A -> B + g = \x. f x + + The above is correct, but eta-reducing g would yield g=f, the linter will + complain that g and f don't have the same type. + * Note [Arity care]: we need to be careful if we just look at f's arity. Currently (Dec07), f's arity is visible in its own RHS (see Note [Arity robustness] in GHC.Core.Opt.Simplify.Env) so we must *not* trust the @@ -2382,7 +2408,7 @@ tryEtaReduce bndrs body -- Float app ticks: \x -> Tick t (e x) ==> Tick t e go (b : bs) (App fun arg) co - | Just (co', ticks) <- ok_arg b arg co + | Just (co', ticks) <- ok_arg b arg co (exprType fun) = fmap (flip (foldr mkTick) ticks) $ go bs fun co' -- Float arg ticks: \x -> e (Tick t x) ==> Tick t e @@ -2417,27 +2443,34 @@ tryEtaReduce bndrs body ok_arg :: Var -- Of type bndr_t -> CoreExpr -- Of type arg_t -> Coercion -- Of kind (t1~t2) + -> Type -- Type of the function to which the argument is applied -> Maybe (Coercion -- Of type (arg_t -> t1 ~ bndr_t -> t2) -- (and similarly for tyvars, coercion args) , [Tickish Var]) -- See Note [Eta reduction with casted arguments] - ok_arg bndr (Type ty) co + ok_arg bndr (Type ty) co _ | Just tv <- getTyVar_maybe ty , bndr == tv = Just (mkHomoForAllCos [tv] co, []) - ok_arg bndr (Var v) co - | bndr == v = let reflCo = mkRepReflCo (idType bndr) - in Just (mkFunCo Representational reflCo co, []) - ok_arg bndr (Cast e co_arg) co + ok_arg bndr (Var v) co fun_ty + | bndr == v + , let mult = idMult bndr + , Just (Scaled fun_mult _, _) <- splitFunTy_maybe fun_ty + , mult `eqType` fun_mult -- There is no change in multiplicity, otherwise we must abort + = let reflCo = mkRepReflCo (idType bndr) + in Just (mkFunCo Representational (multToCo mult) reflCo co, []) + ok_arg bndr (Cast e co_arg) co fun_ty | (ticks, Var v) <- stripTicksTop tickishFloatable e + , Just (Scaled fun_mult _, _) <- splitFunTy_maybe fun_ty , bndr == v - = Just (mkFunCo Representational (mkSymCo co_arg) co, ticks) + , fun_mult `eqType` idMult bndr + = Just (mkFunCo Representational (multToCo fun_mult) (mkSymCo co_arg) co, ticks) -- The simplifier combines multiple casts into one, -- so we can have a simple-minded pattern match here - ok_arg bndr (Tick t arg) co - | tickishFloatable t, Just (co', ticks) <- ok_arg bndr arg co + ok_arg bndr (Tick t arg) co fun_ty + | tickishFloatable t, Just (co', ticks) <- ok_arg bndr arg co fun_ty = Just (co', t:ticks) - ok_arg _ _ _ = Nothing + ok_arg _ _ _ _ = Nothing {- Note [Eta reduction of an eval'd function] |