diff options
Diffstat (limited to 'compiler/GHC/Tc/Utils')
| -rw-r--r-- | compiler/GHC/Tc/Utils/Backpack.hs | 3 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Env.hs | 28 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Instantiate.hs | 5 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Monad.hs | 48 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcMType.hs | 39 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 66 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs | 97 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs-boot | 7 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Zonk.hs | 43 |
9 files changed, 241 insertions, 95 deletions
diff --git a/compiler/GHC/Tc/Utils/Backpack.hs b/compiler/GHC/Tc/Utils/Backpack.hs index 1f6090c7b7..72a1aee55d 100644 --- a/compiler/GHC/Tc/Utils/Backpack.hs +++ b/compiler/GHC/Tc/Utils/Backpack.hs @@ -50,6 +50,7 @@ import GHC.Types.SrcLoc import GHC.Driver.Types import GHC.Utils.Outputable import GHC.Core.Type +import GHC.Core.Multiplicity import GHC.Data.FastString import GHC.Rename.Fixity ( lookupFixityRn ) import GHC.Data.Maybe @@ -216,7 +217,7 @@ check_inst sig_inst = do (substTy skol_subst pred) givens <- forM theta $ \given -> do loc <- getCtLocM origin (Just TypeLevel) - let given_pred = substTy skol_subst given + let given_pred = substTy skol_subst (scaledThing given) new_ev <- newEvVar given_pred return CtGiven { ctev_pred = given_pred -- Doesn't matter, make something up diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs index 2563ff7348..55c0ad4e67 100644 --- a/compiler/GHC/Tc/Utils/Env.hs +++ b/compiler/GHC/Tc/Utils/Env.hs @@ -34,6 +34,7 @@ module GHC.Tc.Utils.Env( tcExtendIdEnv, tcExtendIdEnv1, tcExtendIdEnv2, tcExtendBinderStack, tcExtendLocalTypeEnv, isTypeClosedLetBndr, + tcCheckUsage, tcLookup, tcLookupLocated, tcLookupLocalIds, tcLookupId, tcLookupIdMaybe, tcLookupTyVar, @@ -78,6 +79,10 @@ import GHC.Iface.Env import GHC.Tc.Utils.Monad import GHC.Tc.Utils.TcMType import GHC.Tc.Utils.TcType +import GHC.Core.UsageEnv +import GHC.Tc.Types.Evidence (HsWrapper, idHsWrapper) +import {-# SOURCE #-} GHC.Tc.Utils.Unify ( tcSubMult ) +import GHC.Tc.Types.Origin ( CtOrigin(UsageEnvironmentOf) ) import GHC.Iface.Load import GHC.Builtin.Names import GHC.Builtin.Types @@ -108,6 +113,7 @@ import GHC.Data.Bag import GHC.Data.List.SetOps import GHC.Utils.Error import GHC.Data.Maybe( MaybeErr(..), orElse ) +import GHC.Core.Multiplicity import qualified GHC.LanguageExtensions as LangExt import GHC.Utils.Misc ( HasDebugCallStack ) @@ -621,6 +627,28 @@ tcExtendLocalTypeEnv :: TcLclEnv -> [(Name, TcTyThing)] -> TcLclEnv tcExtendLocalTypeEnv lcl_env@(TcLclEnv { tcl_env = lcl_type_env }) tc_ty_things = lcl_env { tcl_env = extendNameEnvList lcl_type_env tc_ty_things } +-- | @tcCheckUsage name mult thing_inside@ runs @thing_inside@, checks that the +-- usage of @name@ is a submultiplicity of @mult@, and removes @name@ from the +-- usage environment. See also Note [tcSubMult's wrapper] in TcUnify. +tcCheckUsage :: Name -> Mult -> TcM a -> TcM (a, HsWrapper) +tcCheckUsage name id_mult thing_inside + = do { (local_usage, result) <- tcCollectingUsage thing_inside + ; wrapper <- check_then_add_usage local_usage + ; return (result, wrapper) } + where + check_then_add_usage :: UsageEnv -> TcM HsWrapper + -- Checks that the usage of the newly introduced binder is compatible with + -- its multiplicity, and combines the usage of non-new binders to |uenv| + check_then_add_usage uenv + = do { let actual_u = lookupUE uenv name + ; traceTc "check_then_add_usage" (ppr id_mult $$ ppr actual_u) + ; wrapper <- case actual_u of + Bottom -> return idHsWrapper + Zero -> tcSubMult (UsageEnvironmentOf name) Many id_mult + MUsage m -> tcSubMult (UsageEnvironmentOf name) m id_mult + ; tcEmitBindingUsage (deleteUE uenv name) + ; return wrapper } + {- ********************************************************************* * * The TcBinderStack diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs index df9cf982ee..d027209d04 100644 --- a/compiler/GHC/Tc/Utils/Instantiate.hs +++ b/compiler/GHC/Tc/Utils/Instantiate.hs @@ -53,6 +53,7 @@ import GHC.Core ( isOrphan ) import GHC.Tc.Instance.FunDeps import GHC.Tc.Utils.TcMType import GHC.Core.Type +import GHC.Core.Multiplicity import GHC.Core.TyCo.Rep import GHC.Core.TyCo.Ppr ( debugPprType ) import GHC.Tc.Utils.TcType @@ -393,7 +394,7 @@ tcInstInvisibleTyBinder subst (Named (Bndr tv _)) ; return (subst', mkTyVarTy tv') } tcInstInvisibleTyBinder subst (Anon af ty) - | Just (mk, k1, k2) <- get_eq_tys_maybe (substTy subst ty) + | Just (mk, k1, k2) <- get_eq_tys_maybe (substTy subst (scaledThing ty)) -- Equality is the *only* constraint currently handled in types. -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep = ASSERT( af == InvisArg ) @@ -500,7 +501,7 @@ newNonTrivialOverloadedLit orig ; let lit_ty = hsLitType hs_lit ; (_, fi') <- tcSyntaxOp orig (mkRnSyntaxExpr meth_name) [synKnownType lit_ty] res_ty $ - \_ -> return () + \_ _ -> return () ; let L _ witness = nlHsSyntaxApps fi' [nlHsLit hs_lit] ; res_ty <- readExpType res_ty ; return (lit { ol_witness = witness diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs index ca85a087b6..e485b667af 100644 --- a/compiler/GHC/Tc/Utils/Monad.hs +++ b/compiler/GHC/Tc/Utils/Monad.hs @@ -69,6 +69,9 @@ module GHC.Tc.Utils.Monad( addMessages, discardWarnings, + -- * Usage environment + tcCollectingUsage, tcScalingUsage, tcEmitBindingUsage, + -- * Shared error message stuff: renamer and typechecker mkLongErrAt, mkErrDocAt, addLongErrAt, reportErrors, reportError, reportWarning, recoverM, mapAndRecoverM, mapAndReportM, foldAndRecoverM, @@ -157,6 +160,8 @@ import GHC.Driver.Types import GHC.Unit import GHC.Types.Name.Reader import GHC.Types.Name +import GHC.Core.UsageEnv +import GHC.Core.Multiplicity import GHC.Core.Type import GHC.Tc.Utils.TcType @@ -332,6 +337,7 @@ initTcWithGbl :: HscEnv initTcWithGbl hsc_env gbl_env loc do_this = do { lie_var <- newIORef emptyWC ; errs_var <- newIORef (emptyBag, emptyBag) + ; usage_var <- newIORef zeroUE ; let lcl_env = TcLclEnv { tcl_errs = errs_var, tcl_loc = loc, -- Should be over-ridden very soon! @@ -341,6 +347,7 @@ initTcWithGbl hsc_env gbl_env loc do_this tcl_th_bndrs = emptyNameEnv, tcl_arrow_ctxt = NoArrowCtxt, tcl_env = emptyNameEnv, + tcl_usage = usage_var, tcl_bndrs = [], tcl_lie = lie_var, tcl_tclvl = topTcLevel @@ -625,15 +632,16 @@ newSysName occ = do { uniq <- newUnique ; return (mkSystemName uniq occ) } -newSysLocalId :: FastString -> TcType -> TcRnIf gbl lcl TcId -newSysLocalId fs ty +newSysLocalId :: FastString -> Mult -> TcType -> TcRnIf gbl lcl TcId +newSysLocalId fs w ty = do { u <- newUnique - ; return (mkSysLocal fs u ty) } + ; return (mkSysLocal fs u w ty) } -newSysLocalIds :: FastString -> [TcType] -> TcRnIf gbl lcl [TcId] +newSysLocalIds :: FastString -> [Scaled TcType] -> TcRnIf gbl lcl [TcId] newSysLocalIds fs tys = do { us <- newUniqueSupply - ; return (zipWith (mkSysLocal fs) (uniqsFromSupply us) tys) } + ; let mkId' n (Scaled w t) = mkSysLocal fs n w t + ; return (zipWith mkId' (uniqsFromSupply us) tys) } instance MonadUnique (IOEnv (Env gbl lcl)) where getUniqueM = newUnique @@ -1191,6 +1199,36 @@ captureConstraints thing_inside Just res -> return (res, lie) } ----------------------- +-- | @tcCollectingUsage thing_inside@ runs @thing_inside@ and returns the usage +-- information which was collected as part of the execution of +-- @thing_inside@. Careful: @tcCollectingUsage thing_inside@ itself does not +-- report any usage information, it's up to the caller to incorporate the +-- returned usage information into the larger context appropriately. +tcCollectingUsage :: TcM a -> TcM (UsageEnv,a) +tcCollectingUsage thing_inside + = do { env0 <- getLclEnv + ; local_usage_ref <- newTcRef zeroUE + ; let env1 = env0 { tcl_usage = local_usage_ref } + ; result <- setLclEnv env1 thing_inside + ; local_usage <- readTcRef local_usage_ref + ; return (local_usage,result) } + +-- | @tcScalingUsage mult thing_inside@ runs @thing_inside@ and scales all the +-- usage information by @mult@. +tcScalingUsage :: Mult -> TcM a -> TcM a +tcScalingUsage mult thing_inside + = do { (usage, result) <- tcCollectingUsage thing_inside + ; traceTc "tcScalingUsage" (ppr mult) + ; tcEmitBindingUsage $ scaleUE mult usage + ; return result } + +tcEmitBindingUsage :: UsageEnv -> TcM () +tcEmitBindingUsage ue + = do { lcl_env <- getLclEnv + ; let usage = tcl_usage lcl_env + ; updTcRef usage (addUE ue) } + +----------------------- attemptM :: TcRn r -> TcRn (Maybe r) -- (attemptM thing_inside) runs thing_inside -- If thing_inside succeeds, returning r, diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index cc8ac8f737..c33c335ac7 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -4,7 +4,7 @@ -} -{-# LANGUAGE CPP, TupleSections, MultiWayIf #-} +{-# LANGUAGE CPP, TupleSections, MultiWayIf, PatternSynonyms #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} @@ -26,6 +26,7 @@ module GHC.Tc.Utils.TcMType ( cloneMetaTyVar, newFmvTyVar, newFskTyVar, + newMultiplicityVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef, newTauTvDetailsAtLevel, newMetaDetails, newMetaTyVarName, isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar, @@ -126,6 +127,7 @@ import GHC.Data.FastString import GHC.Data.Bag import GHC.Data.Pair import GHC.Types.Unique.Set +import GHC.Core.Multiplicity import GHC.Driver.Session import qualified GHC.LanguageExtensions as LangExt import GHC.Types.Basic ( TypeOrKind(..) ) @@ -173,7 +175,7 @@ newEvVars theta = mapM newEvVar theta newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar -- Creates new *rigid* variables for predicates newEvVar ty = do { name <- newSysName (predTypeOccName ty) - ; return (mkLocalIdOrCoVar name ty) } + ; return (mkLocalIdOrCoVar name Many ty) } newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence -- Deals with both equality and non-equality predicates @@ -286,7 +288,7 @@ emitNewExprHole occ ev_id ty newDict :: Class -> [TcType] -> TcM DictId newDict cls tys = do { name <- newSysName (mkDictOcc (getOccName cls)) - ; return (mkLocalId name (mkClassPred cls tys)) } + ; return (mkLocalId name Many (mkClassPred cls tys)) } predTypeOccName :: PredType -> OccName predTypeOccName ty = case classifyPredType ty of @@ -925,6 +927,7 @@ writeMetaTyVarRef tyvar ref ty -- Check for level OK -- See Note [Level check when unifying] ; MASSERT2( level_check_ok, level_check_msg ) + -- another level check problem, see #97 -- Check Kinds ok ; MASSERT2( kind_check_ok, kind_msg ) @@ -982,6 +985,9 @@ that can't ever appear in user code, so we're safe! -} +newMultiplicityVar :: TcM TcType +newMultiplicityVar = newFlexiTyVarTy multiplicityTy + newFlexiTyVar :: Kind -> TcM TcTyVar newFlexiTyVar kind = newAnonMetaTyVar TauTv kind @@ -1320,9 +1326,9 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty ----------------- go :: CandidatesQTvs -> TcType -> TcM CandidatesQTvs -- Uses accumulating-parameter style - go dv (AppTy t1 t2) = foldlM go dv [t1, t2] - go dv (TyConApp _ tys) = foldlM go dv tys - go dv (FunTy _ arg res) = foldlM go dv [arg, res] + go dv (AppTy t1 t2) = foldlM go dv [t1, t2] + go dv (TyConApp _ tys) = foldlM go dv tys + go dv (FunTy _ w arg res) = foldlM go dv [w, arg, res] go dv (LitTy {}) = return dv go dv (CastTy ty co) = do dv1 <- go dv ty collect_cand_qtvs_co orig_ty bound dv1 co @@ -1393,7 +1399,7 @@ collect_cand_qtvs_co orig_ty bound = go_co go_mco dv1 mco go_co dv (TyConAppCo _ _ cos) = foldlM go_co dv cos go_co dv (AppCo co1 co2) = foldlM go_co dv [co1, co2] - go_co dv (FunCo _ co1 co2) = foldlM go_co dv [co1, co2] + go_co dv (FunCo _ w co1 co2) = foldlM go_co dv [w, co1, co2] go_co dv (AxiomInstCo _ _ cos) = foldlM go_co dv cos go_co dv (AxiomRuleCo _ cos) = foldlM go_co dv cos go_co dv (UnivCo prov _ t1 t2) = do dv1 <- go_prov dv prov @@ -1725,6 +1731,10 @@ defaultTyVar default_kind tv = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv) ; writeMetaTyVar tv liftedRepTy ; return True } + | isMultiplicityVar tv + = do { traceTc "Defaulting a Multiplicty var to Many" (ppr tv) + ; writeMetaTyVar tv manyDataConTy + ; return True } | default_kind -- -XNoPolyKinds and this is a kind var = default_kind_var tv -- so default it to * if possible @@ -2030,8 +2040,7 @@ zonkImplication implic@(Implic { ic_skols = skols , ic_info = info' }) } zonkEvVar :: EvVar -> TcM EvVar -zonkEvVar var = do { ty' <- zonkTcType (varType var) - ; return (setVarType var ty') } +zonkEvVar var = updateVarTypeAndMultM zonkTcType var zonkWC :: WantedConstraints -> TcM WantedConstraints @@ -2218,9 +2227,7 @@ zonkInvisTVBinder (Bndr tv spec) = do { tv' <- zonkTcTyVarToTyVar tv -- zonkId is used *during* typechecking just to zonk the Id's type zonkId :: TcId -> TcM TcId -zonkId id - = do { ty' <- zonkTcType (idType id) - ; return (Id.setIdType id ty') } +zonkId id = Id.updateIdTypeAndMultM zonkTcType id zonkCoVar :: CoVar -> TcM CoVar zonkCoVar = zonkId @@ -2308,7 +2315,7 @@ tidyHole env h@(Hole { hole_ty = ty }) = h { hole_ty = tidyType env ty } ---------------- tidyEvVar :: TidyEnv -> EvVar -> EvVar -tidyEvVar env var = setVarType var (tidyType env (varType var)) +tidyEvVar env var = updateVarTypeAndMult (tidyType env) var ---------------- tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo @@ -2333,8 +2340,10 @@ tidySigSkol env cx ty tv_prs where (env', tv') = tidy_tv_bndr env tv - tidy_ty env ty@(FunTy InvisArg arg res) -- Look under c => t - = ty { ft_arg = tidyType env arg, ft_res = tidy_ty env res } + tidy_ty env ty@(FunTy InvisArg w arg res) -- Look under c => t + = ty { ft_mult = tidy_ty env w, + ft_arg = tidyType env arg, + ft_res = tidy_ty env res } tidy_ty env ty = tidyType env ty diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 9cc1d79df9..f06cdd7d31 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -134,7 +134,8 @@ module GHC.Tc.Utils.TcType ( mkForAllTy, mkForAllTys, mkInvisForAllTys, mkTyCoInvForAllTys, mkSpecForAllTys, mkTyCoInvForAllTy, mkInfForAllTy, mkInfForAllTys, - mkVisFunTy, mkVisFunTys, mkInvisFunTy, mkInvisFunTys, + mkVisFunTy, mkVisFunTys, mkInvisFunTy, mkInvisFunTyMany, + mkVisFunTyMany, mkVisFunTysMany, mkInvisFunTysMany, mkTyConApp, mkAppTy, mkAppTys, mkTyConTy, mkTyVarTy, mkTyVarTys, mkTyCoVarTy, mkTyCoVarTys, @@ -155,9 +156,10 @@ module GHC.Tc.Utils.TcType ( Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr, Type.extendTvSubst, isInScope, mkTCvSubst, mkTvSubst, zipTyEnv, zipCoEnv, - Type.substTy, substTys, substTyWith, substTyWithCoVars, + Type.substTy, substTys, substScaledTys, substTyWith, substTyWithCoVars, substTyAddInScope, - substTyUnchecked, substTysUnchecked, substThetaUnchecked, + substTyUnchecked, substTysUnchecked, substScaledTyUnchecked, + substThetaUnchecked, substTyWithUnchecked, substCoUnchecked, substCoWithUnchecked, substTheta, @@ -198,6 +200,7 @@ import GHC.Core.TyCo.Subst ( mkTvSubst, substTyWithCoVars ) import GHC.Core.TyCo.FVs import GHC.Core.TyCo.Ppr import GHC.Core.Class +import GHC.Core.Multiplicity import GHC.Types.Var import GHC.Types.ForeignCall import GHC.Types.Var.Set @@ -411,6 +414,9 @@ mkCheckExpType = Check -- for the 'SynType', because you've said positively that it should be an -- Int, and so it shall be. -- +-- You'll also get three multiplicities back: one for each function arrow. See +-- also Note [Linear types] in Multiplicity. +-- -- This is defined here to avoid defining it in GHC.Tc.Gen.Expr boot file. data SyntaxOpType = SynAny -- ^ Any type @@ -804,7 +810,8 @@ tcTyFamInstsAndVisX = go go _ (LitTy {}) = [] go is_invis_arg (ForAllTy bndr ty) = go is_invis_arg (binderType bndr) ++ go is_invis_arg ty - go is_invis_arg (FunTy _ ty1 ty2) = go is_invis_arg ty1 + go is_invis_arg (FunTy _ w ty1 ty2) = go is_invis_arg w + ++ go is_invis_arg ty1 ++ go is_invis_arg ty2 go is_invis_arg ty@(AppTy _ _) = let (ty_head, ty_args) = splitAppTys ty @@ -861,8 +868,8 @@ anyRewritableTyVar ignore_cos role pred ty go _ _ (LitTy {}) = False go rl bvs (TyConApp tc tys) = go_tc rl bvs tc tys go rl bvs (AppTy fun arg) = go rl bvs fun || go NomEq bvs arg - go rl bvs (FunTy _ arg res) = go NomEq bvs arg_rep || go NomEq bvs res_rep || - go rl bvs arg || go rl bvs res + go rl bvs (FunTy _ w arg res) = go NomEq bvs arg_rep || go NomEq bvs res_rep || + go rl bvs arg || go rl bvs res || go rl bvs w where arg_rep = getRuntimeRep arg -- forgetting these causes #17024 res_rep = getRuntimeRep res go rl bvs (ForAllTy tv ty) = go rl (bvs `extendVarSet` binderVar tv) ty @@ -1133,7 +1140,7 @@ mkSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type mkSpecSigmaTy tyvars preds ty = mkSigmaTy (mkTyCoVarBinders Specified tyvars) preds ty mkPhiTy :: [PredType] -> Type -> Type -mkPhiTy = mkInvisFunTys +mkPhiTy = mkInvisFunTysMany --------------- getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to @@ -1329,18 +1336,18 @@ tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of Nothing -> pprPanic "tcSplitTyConApp" (pprType ty) ----------------------- -tcSplitFunTys :: Type -> ([Type], Type) +tcSplitFunTys :: Type -> ([Scaled Type], Type) tcSplitFunTys ty = case tcSplitFunTy_maybe ty of Nothing -> ([], ty) Just (arg,res) -> (arg:args, res') where (args,res') = tcSplitFunTys res -tcSplitFunTy_maybe :: Type -> Maybe (Type, Type) +tcSplitFunTy_maybe :: Type -> Maybe (Scaled Type, Type) tcSplitFunTy_maybe ty | Just ty' <- tcView ty = tcSplitFunTy_maybe ty' -tcSplitFunTy_maybe (FunTy { ft_af = af, ft_arg = arg, ft_res = res }) - | VisArg <- af = Just (arg, res) +tcSplitFunTy_maybe (FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res }) + | VisArg <- af = Just (Scaled w arg, res) tcSplitFunTy_maybe _ = Nothing -- Note the VisArg guard -- Consider (?x::Int) => Bool @@ -1353,7 +1360,7 @@ tcSplitFunTy_maybe _ = Nothing tcSplitFunTysN :: Arity -- n: Number of desired args -> TcRhoType -> Either Arity -- Number of missing arrows - ([TcSigmaType], -- Arg types (always N types) + ([Scaled TcSigmaType],-- Arg types (always N types) TcSigmaType) -- The rest of the type -- ^ Split off exactly the specified number argument types -- Returns @@ -1369,10 +1376,10 @@ tcSplitFunTysN n ty | otherwise = Left n -tcSplitFunTy :: Type -> (Type, Type) +tcSplitFunTy :: Type -> (Scaled Type, Type) tcSplitFunTy ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty) -tcFunArgTy :: Type -> Type +tcFunArgTy :: Type -> Scaled Type tcFunArgTy ty = fst (tcSplitFunTy ty) tcFunResultTy :: Type -> Type @@ -1452,7 +1459,7 @@ tcSplitDFunTy ty = case tcSplitForAllTys ty of { (tvs, rho) -> case splitFunTys rho of { (theta, tau) -> case tcSplitDFunHead tau of { (clas, tys) -> - (tvs, theta, clas, tys) }}} + (tvs, map scaledThing theta, clas, tys) }}} tcSplitDFunHead :: Type -> (Class, [Type]) tcSplitDFunHead = getClassPredTys @@ -1544,10 +1551,10 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2 -- Make sure we handle all FunTy cases since falling through to the -- AppTy case means that tcRepSplitAppTy_maybe may see an unzonked -- kind variable, which causes things to blow up. - go env (FunTy _ arg1 res1) (FunTy _ arg2 res2) - = go env arg1 arg2 && go env res1 res2 - go env ty (FunTy _ arg res) = eqFunTy env arg res ty - go env (FunTy _ arg res) ty = eqFunTy env arg res ty + go env (FunTy _ w1 arg1 res1) (FunTy _ w2 arg2 res2) + = go env w1 w2 && go env arg1 arg2 && go env res1 res2 + go env ty (FunTy _ w arg res) = eqFunTy env w arg res ty + go env (FunTy _ w arg res) ty = eqFunTy env w arg res ty -- See Note [Equality on AppTys] in GHC.Core.Type go env (AppTy s1 t1) ty2 @@ -1582,25 +1589,25 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2 orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2] - -- @eqFunTy arg res ty@ is True when @ty@ equals @FunTy arg res@. This is + -- @eqFunTy w arg res ty@ is True when @ty@ equals @FunTy w arg res@. This is -- sometimes hard to know directly because @ty@ might have some casts -- obscuring the FunTy. And 'splitAppTy' is difficult because we can't -- always extract a RuntimeRep (see Note [xyz]) if the kind of the arg or -- res is unzonked/unflattened. Thus this function, which handles this -- corner case. - eqFunTy :: RnEnv2 -> Type -> Type -> Type -> Bool + eqFunTy :: RnEnv2 -> Mult -> Type -> Type -> Type -> Bool -- Last arg is /not/ FunTy - eqFunTy env arg res ty@(AppTy{}) = get_args ty [] + eqFunTy env w arg res ty@(AppTy{}) = get_args ty [] where get_args :: Type -> [Type] -> Bool get_args (AppTy f x) args = get_args f (x:args) get_args (CastTy t _) args = get_args t args get_args (TyConApp tc tys) args | tc == funTyCon - , [_, _, arg', res'] <- tys ++ args - = go env arg arg' && go env res res' + , [w', _, _, arg', res'] <- tys ++ args + = go env w w' && go env arg arg' && go env res res' get_args _ _ = False - eqFunTy _ _ _ _ = False + eqFunTy _ _ _ _ _ = False {- ********************************************************************* * * @@ -1850,7 +1857,7 @@ isInsolubleOccursCheck eq_rel tv ty go (AppTy t1 t2) = case eq_rel of -- See Note [AppTy and ReprEq] NomEq -> go t1 || go t2 ReprEq -> go t1 - go (FunTy _ t1 t2) = go t1 || go t2 + go (FunTy _ w t1 t2) = go w || go t1 || go t2 go (ForAllTy (Bndr tv' _) inner_ty) | tv' == tv = False | otherwise = go (varType tv') || go inner_ty @@ -2105,8 +2112,9 @@ isAlmostFunctionFree (TyConApp tc args) | isTypeFamilyTyCon tc = False | otherwise = all isAlmostFunctionFree args isAlmostFunctionFree (ForAllTy bndr _) = isAlmostFunctionFree (binderType bndr) -isAlmostFunctionFree (FunTy _ ty1 ty2) = isAlmostFunctionFree ty1 && - isAlmostFunctionFree ty2 +isAlmostFunctionFree (FunTy _ w ty1 ty2) = isAlmostFunctionFree w && + isAlmostFunctionFree ty1 && + isAlmostFunctionFree ty2 isAlmostFunctionFree (LitTy {}) = True isAlmostFunctionFree (CastTy ty _) = isAlmostFunctionFree ty isAlmostFunctionFree (CoercionTy {}) = True @@ -2447,7 +2455,7 @@ sizeType = go -- size ordering is sound, but why is this better? -- I came across this when investigating #14010. go (LitTy {}) = 1 - go (FunTy _ arg res) = go arg + go res + 1 + go (FunTy _ w arg res) = go w + go arg + go res + 1 go (AppTy fun arg) = go fun + go arg go (ForAllTy (Bndr tv vis) ty) | isVisibleArgFlag vis = go (tyVarKind tv) + go ty + 1 diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index efe8301650..a6711abcc1 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -16,6 +16,7 @@ module GHC.Tc.Utils.Unify ( tcWrapResult, tcWrapResultO, tcWrapResultMono, tcSkolemise, tcSkolemiseScoped, tcSkolemiseET, tcSubType, tcSubTypeSigma, tcSubTypePat, + tcSubMult, checkConstraints, checkTvConstraints, buildImplicationFor, buildTvImplication, emitResidualTvConstraint, @@ -51,6 +52,7 @@ import GHC.Tc.Utils.TcType import GHC.Tc.Utils.Env import GHC.Core.Type import GHC.Core.Coercion +import GHC.Core.Multiplicity import GHC.Tc.Types.Evidence import GHC.Tc.Types.Constraint import GHC.Core.Predicate @@ -145,7 +147,7 @@ matchExpectedFunTys :: forall a. -> UserTypeCtxt -> Arity -> ExpRhoType -- Skolemised - -> ([ExpSigmaType] -> ExpRhoType -> TcM a) + -> ([Scaled ExpSigmaType] -> ExpRhoType -> TcM a) -> TcM (HsWrapper, a) -- If matchExpectedFunTys n ty = (_, wrap) -- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty, @@ -173,11 +175,11 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside go acc_arg_tys n ty | Just ty' <- tcView ty = go acc_arg_tys n ty' - go acc_arg_tys n (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty }) + go acc_arg_tys n (FunTy { ft_mult = mult, ft_af = af, ft_arg = arg_ty, ft_res = res_ty }) = ASSERT( af == VisArg ) - do { (wrap_res, result) <- go (mkCheckExpType arg_ty : acc_arg_tys) + do { (wrap_res, result) <- go ((Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys) (n-1) res_ty - ; let fun_wrap = mkWpFun idHsWrapper wrap_res arg_ty res_ty doc + ; let fun_wrap = mkWpFun idHsWrapper wrap_res (Scaled mult arg_ty) res_ty doc ; return ( fun_wrap, result ) } where doc = text "When inferring the argument type of a function with type" <+> @@ -209,25 +211,25 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside defer acc_arg_tys n (mkCheckExpType ty) ------------ - defer :: [ExpSigmaType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a) + defer :: [Scaled ExpSigmaType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a) defer acc_arg_tys n fun_ty = do { more_arg_tys <- replicateM n newInferExpType ; res_ty <- newInferExpType - ; result <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty + ; result <- thing_inside (reverse acc_arg_tys ++ (map unrestricted more_arg_tys)) res_ty ; more_arg_tys <- mapM readExpType more_arg_tys ; res_ty <- readExpType res_ty - ; let unif_fun_ty = mkVisFunTys more_arg_tys res_ty + ; let unif_fun_ty = mkVisFunTysMany more_arg_tys res_ty ; wrap <- tcSubType AppOrigin ctx unif_fun_ty fun_ty -- Not a good origin at all :-( ; return (wrap, result) } ------------ - mk_ctxt :: [ExpSigmaType] -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) + mk_ctxt :: [Scaled ExpSigmaType] -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) mk_ctxt arg_tys res_ty env = do { (env', ty) <- zonkTidyTcType env (mkVisFunTys arg_tys' res_ty) ; return ( env', mk_fun_tys_msg herald ty arity) } where - arg_tys' = map (checkingExpType "matchExpectedFunTys") (reverse arg_tys) + arg_tys' = map (\(Scaled u v) -> Scaled u (checkingExpType "matchExpectedFunTys" v)) (reverse arg_tys) -- this is safe b/c we're called from "go" -- Like 'matchExpectedFunTys', but used when you have an "actual" type, @@ -237,7 +239,7 @@ matchActualFunTysRho :: SDoc -- See Note [Herald for matchExpectedFunTys] -> Maybe (HsExpr GhcRn) -- the thing with type TcSigmaType -> Arity -> TcSigmaType - -> TcM (HsWrapper, [TcSigmaType], TcRhoType) + -> TcM (HsWrapper, [Scaled TcSigmaType], TcRhoType) -- If matchActualFunTysRho n ty = (wrap, [t1,..,tn], res_ty) -- then wrap : ty ~> (t1 -> ... -> tn -> res_ty) -- and res_ty is a RhoType @@ -266,12 +268,12 @@ matchActualFunTySigma :: SDoc -- See Note [Herald for matchExpectedFunTys] -> CtOrigin -> Maybe (HsExpr GhcRn) -- The thing with type TcSigmaType - -> (Arity, [TcSigmaType]) -- Total number of value args in the call, and + -> (Arity, [Scaled TcSigmaType]) -- Total number of value args in the call, and -- types of values args to which function has -- been applied already (reversed) -- Both are used only for error messages) -> TcSigmaType -- Type to analyse - -> TcM (HsWrapper, TcSigmaType, TcSigmaType) + -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType) -- See Note [matchActualFunTys error handling] for all these arguments -- If (wrap, arg_ty, res_ty) = matchActualFunTySigma ... fun_ty @@ -295,7 +297,7 @@ matchActualFunTySigma herald ct_orig mb_thing err_info fun_ty where go :: TcSigmaType -- The remainder of the type as we're processing - -> TcM (HsWrapper, TcSigmaType, TcSigmaType) + -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType) go ty | Just ty' <- tcView ty = go ty' go ty @@ -306,9 +308,9 @@ matchActualFunTySigma herald ct_orig mb_thing err_info fun_ty where (tvs, theta, _) = tcSplitSigmaTy ty - go (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty }) + go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty }) = ASSERT( af == VisArg ) - return (idHsWrapper, arg_ty, res_ty) + return (idHsWrapper, Scaled w arg_ty, res_ty) go ty@(TyVarTy tv) | isMetaTyVar tv @@ -338,9 +340,9 @@ matchActualFunTySigma herald ct_orig mb_thing err_info fun_ty defer fun_ty = do { arg_ty <- newOpenFlexiTyVarTy ; res_ty <- newOpenFlexiTyVarTy - ; let unif_fun_ty = mkVisFunTy arg_ty res_ty + ; let unif_fun_ty = mkVisFunTyMany arg_ty res_ty ; co <- unifyType mb_thing fun_ty unif_fun_ty - ; return (mkWpCastN co, arg_ty, res_ty) } + ; return (mkWpCastN co, unrestricted arg_ty, res_ty) } ------------ mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) @@ -405,7 +407,7 @@ matchExpectedTyConApp :: TyCon -- T :: forall kv1 ... kvm. k1 -> -- Postcondition: (T k1 k2 k3 a b c) is well-kinded matchExpectedTyConApp tc orig_ty - = ASSERT(tc /= funTyCon) go orig_ty + = ASSERT(not $ isFunTyCon tc) go orig_ty where go ty | Just ty' <- tcView ty @@ -475,7 +477,7 @@ matchExpectedAppTy orig_ty ; return (co, (ty1, ty2)) } orig_kind = tcTypeKind orig_ty - kind1 = mkVisFunTy liftedTypeKind orig_kind + kind1 = mkVisFunTyMany liftedTypeKind orig_kind kind2 = liftedTypeKind -- m :: * -> k -- arg type :: * @@ -723,6 +725,48 @@ to a UserTypeCtxt of GenSigCtxt. Why? -} +-- Note [tcSubMult's wrapper] +-- ~~~~~~~~~~~~~~~~~~~~~~~~~~ +-- There is no notion of multiplicity coercion in Core, therefore the wrapper +-- returned by tcSubMult (and derived function such as tcCheckUsage and +-- checkManyPattern) is quite unlike any other wrapper: it checks whether the +-- coercion produced by the constraint solver is trivial and disappears (it +-- produces a type error is the constraint is not trivial). See [Checking +-- multiplicity coercions] in TcEvidence. +-- +-- This wrapper need to be placed in the term, otherwise checking of the +-- eventual coercion won't be triggered during desuraging. But it can be put +-- anywhere, since it doesn't affect the desugared code. +-- +-- Why do we check this in the desugarer? It's a convenient place, since it's +-- right after all the constraints are solved. We need the constraints to be +-- solved to check whether they are trivial or not. Plus there are precedent for +-- type errors during desuraging (such as the levity polymorphism +-- restriction). An alternative would be to have a kind of constraints which can +-- only produce trivial evidence, then this check would happen in the constraint +-- solver. +tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper +tcSubMult origin (MultMul w1 w2) w_expected = + do { w1 <- tcSubMult origin w1 w_expected + ; w2 <- tcSubMult origin w2 w_expected + ; return (w1 <.> w2) } + -- Currently, we consider p*q and sup p q to be equal. Therefore, p*q <= r is + -- equivalent to p <= r and q <= r. For other cases, we approximate p <= q by p + -- ~ q. This is not complete, but it's sound. See also Note [Overapproximating + -- multiplicities] in Multiplicity. +tcSubMult origin w_actual w_expected = + case submult w_actual w_expected of + Submult -> return WpHole + Unknown -> tcEqMult origin w_actual w_expected + +tcEqMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper +tcEqMult origin w_actual w_expected = do + { + -- Note that here we do not call to `submult`, so we check + -- for strict equality. + ; coercion <- uType TypeLevel origin w_actual w_expected + ; return $ if isReflCo coercion then WpHole else WpMultCoercion coercion } + {- ********************************************************************** %* * ExpType functions: tcInfer, instantiateAndFillInferResult @@ -1308,10 +1352,11 @@ uType t_or_k origin orig_ty1 orig_ty2 | Just ty2' <- tcView ty2 = go ty1 ty2' -- Functions (or predicate functions) just check the two parts - go (FunTy _ fun1 arg1) (FunTy _ fun2 arg2) + go (FunTy _ w1 fun1 arg1) (FunTy _ w2 fun2 arg2) = do { co_l <- uType t_or_k origin fun1 fun2 ; co_r <- uType t_or_k origin arg1 arg2 - ; return $ mkFunCo Nominal co_l co_r } + ; co_w <- uType t_or_k origin w1 w2 + ; return $ mkFunCo Nominal co_w co_l co_r } -- Always defer if a type synonym family (type function) -- is involved. (Data families behave rigidly.) @@ -1975,9 +2020,9 @@ matchExpectedFunKind hs_ty n k = go n k Indirect fun_kind -> go n fun_kind Flexi -> defer n k } - go n (FunTy _ arg res) + go n (FunTy _ w arg res) = do { co <- go (n-1) res - ; return (mkTcFunCo Nominal (mkTcNomReflCo arg) co) } + ; return (mkTcFunCo Nominal (mkTcNomReflCo w) (mkTcNomReflCo arg) co) } go n other = defer n other @@ -1985,7 +2030,7 @@ matchExpectedFunKind hs_ty n k = go n k defer n k = do { arg_kinds <- newMetaKindVars n ; res_kind <- newMetaKindVar - ; let new_fun = mkVisFunTys arg_kinds res_kind + ; let new_fun = mkVisFunTysMany arg_kinds res_kind origin = TypeEqOrigin { uo_actual = k , uo_expected = new_fun , uo_thing = Just (ppr hs_ty) @@ -2156,10 +2201,10 @@ preCheck dflags ty_fam_ok tv ty | bad_tc tc = MTVU_Bad | otherwise = mapM fast_check tys >> ok fast_check (LitTy {}) = ok - fast_check (FunTy{ft_af = af, ft_arg = a, ft_res = r}) + fast_check (FunTy{ft_af = af, ft_mult = w, ft_arg = a, ft_res = r}) | InvisArg <- af , not impredicative_ok = MTVU_Bad - | otherwise = fast_check a >> fast_check r + | otherwise = fast_check w >> fast_check a >> fast_check r fast_check (AppTy fun arg) = fast_check fun >> fast_check arg fast_check (CastTy ty co) = fast_check ty >> fast_check_co co fast_check (CoercionTy co) = fast_check_co co diff --git a/compiler/GHC/Tc/Utils/Unify.hs-boot b/compiler/GHC/Tc/Utils/Unify.hs-boot index 311dbf66aa..a54107fe07 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs-boot +++ b/compiler/GHC/Tc/Utils/Unify.hs-boot @@ -3,9 +3,10 @@ module GHC.Tc.Utils.Unify where import GHC.Prelude import GHC.Tc.Utils.TcType ( TcTauType ) import GHC.Tc.Types ( TcM ) -import GHC.Tc.Types.Evidence ( TcCoercion ) +import GHC.Tc.Types.Evidence ( TcCoercion, HsWrapper ) +import GHC.Tc.Types.Origin ( CtOrigin ) import GHC.Hs.Expr ( HsExpr ) -import GHC.Hs.Type ( HsType ) +import GHC.Hs.Type ( HsType, Mult ) import GHC.Hs.Extension ( GhcRn ) -- This boot file exists only to tie the knot between @@ -13,3 +14,5 @@ import GHC.Hs.Extension ( GhcRn ) unifyType :: Maybe (HsExpr GhcRn) -> TcTauType -> TcTauType -> TcM TcCoercion unifyKind :: Maybe (HsType GhcRn) -> TcTauType -> TcTauType -> TcM TcCoercion + +tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs index 4372a39e9d..05eb4d9ba4 100644 --- a/compiler/GHC/Tc/Utils/Zonk.hs +++ b/compiler/GHC/Tc/Utils/Zonk.hs @@ -36,7 +36,7 @@ module GHC.Tc.Utils.Zonk ( zonkTyVarBinders, zonkTyVarBindersX, zonkTyVarBinderX, zonkTyBndrs, zonkTyBndrsX, zonkTcTypeToType, zonkTcTypeToTypeX, - zonkTcTypesToTypes, zonkTcTypesToTypesX, + zonkTcTypesToTypes, zonkTcTypesToTypesX, zonkScaledTcTypesToTypesX, zonkTyVarOcc, zonkCoToCo, zonkEvBinds, zonkTcEvBinds, @@ -80,6 +80,7 @@ import GHC.Data.Bag import GHC.Utils.Outputable import GHC.Utils.Misc import GHC.Types.Unique.FM +import GHC.Core.Multiplicity import GHC.Core import {-# SOURCE #-} GHC.Tc.Gen.Splice (runTopSplice) @@ -372,11 +373,11 @@ zonkIdOccs env ids = map (zonkIdOcc env) ids -- to its final form. The TyVarEnv give zonkIdBndr :: ZonkEnv -> TcId -> TcM Id zonkIdBndr env v - = do ty' <- zonkTcTypeToTypeX env (idType v) + = do Scaled w' ty' <- zonkScaledTcTypeToTypeX env (idScaledType v) ensureNotLevPoly ty' (text "In the type of binder" <+> quotes (ppr v)) - return (modifyIdInfo (`setLevityInfoWithType` ty') (setIdType v ty')) + return (modifyIdInfo (`setLevityInfoWithType` ty') (setIdMult (setIdType v ty') w')) zonkIdBndrs :: ZonkEnv -> [TcId] -> TcM [Id] zonkIdBndrs env ids = mapM (zonkIdBndr env) ids @@ -401,11 +402,7 @@ zonkEvBndr :: ZonkEnv -> EvVar -> TcM EvVar -- Works for dictionaries and coercions -- Does not extend the ZonkEnv zonkEvBndr env var - = do { let var_ty = varType var - ; ty <- - {-# SCC "zonkEvBndr_zonkTcTypeToType" #-} - zonkTcTypeToTypeX env var_ty - ; return (setVarType var ty) } + = updateVarTypeAndMultM ({-# SCC "zonkEvBndr_zonkTcTypeToType" #-} zonkTcTypeToTypeX env) var {- zonkEvVarOcc :: ZonkEnv -> EvVar -> TcM EvTerm @@ -583,10 +580,10 @@ zonk_bind env (AbsBinds { abs_tvs = tyvars, abs_ev_vars = evs where zonk_val_bind env lbind | has_sig - , (L loc bind@(FunBind { fun_id = L mloc mono_id + , (L loc bind@(FunBind { fun_id = (L mloc mono_id) , fun_matches = ms , fun_ext = co_fn })) <- lbind - = do { new_mono_id <- updateVarTypeM (zonkTcTypeToTypeX env) mono_id + = do { new_mono_id <- updateVarTypeAndMultM (zonkTcTypeToTypeX env) mono_id -- Specifically /not/ zonkIdBndr; we do not -- want to complain about a levity-polymorphic binder ; (env', new_co_fn) <- zonkCoFn env co_fn @@ -674,7 +671,7 @@ zonkMatchGroup env zBody (MG { mg_alts = L l ms , mg_ext = MatchGroupTc arg_tys res_ty , mg_origin = origin }) = do { ms' <- mapM (zonkMatch env zBody) ms - ; arg_tys' <- zonkTcTypesToTypesX env arg_tys + ; arg_tys' <- zonkScaledTcTypesToTypesX env arg_tys ; res_ty' <- zonkTcTypeToTypeX env res_ty ; return (MG { mg_alts = L l ms' , mg_ext = MatchGroupTc arg_tys' res_ty' @@ -1043,7 +1040,7 @@ zonkCoFn env (WpCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1 ; return (env2, WpCompose c1' c2') } zonkCoFn env (WpFun c1 c2 t1 d) = do { (env1, c1') <- zonkCoFn env c1 ; (env2, c2') <- zonkCoFn env1 c2 - ; t1' <- zonkTcTypeToTypeX env2 t1 + ; t1' <- zonkScaledTcTypeToTypeX env2 t1 ; return (env2, WpFun c1' c2' t1' d) } zonkCoFn env (WpCast co) = do { co' <- zonkCoToCo env co ; return (env, WpCast co') } @@ -1058,6 +1055,8 @@ zonkCoFn env (WpTyApp ty) = do { ty' <- zonkTcTypeToTypeX env ty ; return (env, WpTyApp ty') } zonkCoFn env (WpLet bs) = do { (env1, bs') <- zonkTcEvBinds env bs ; return (env1, WpLet bs') } +zonkCoFn env (WpMultCoercion co) = do { co' <- zonkCoToCo env co + ; return (env, WpMultCoercion co') } ------------------------------------------------------------------------- zonkOverLit :: ZonkEnv -> HsOverLit GhcTcId -> TcM (HsOverLit GhcTc) @@ -1199,6 +1198,7 @@ zonkStmt env _ (LetStmt x (L l binds)) zonkStmt env zBody (BindStmt xbs pat body) = do { (env1, new_bind) <- zonkSyntaxExpr env (xbstc_bindOp xbs) + ; new_w <- zonkTcTypeToTypeX env1 (xbstc_boundResultMult xbs) ; new_bind_ty <- zonkTcTypeToTypeX env1 (xbstc_boundResultType xbs) ; new_body <- zBody env1 body ; (env2, new_pat) <- zonkPat env1 pat @@ -1209,6 +1209,7 @@ zonkStmt env zBody (BindStmt xbs pat body) , BindStmt (XBindStmtTc { xbstc_bindOp = new_bind , xbstc_boundResultType = new_bind_ty + , xbstc_boundResultMult = new_w , xbstc_failOp = new_fail }) new_pat new_body) } @@ -1617,10 +1618,11 @@ zonkEvTypeable env (EvTypeableTyApp t1 t2) = do { t1' <- zonkEvTerm env t1 ; t2' <- zonkEvTerm env t2 ; return (EvTypeableTyApp t1' t2') } -zonkEvTypeable env (EvTypeableTrFun t1 t2) - = do { t1' <- zonkEvTerm env t1 +zonkEvTypeable env (EvTypeableTrFun tm t1 t2) + = do { tm' <- zonkEvTerm env tm + ; t1' <- zonkEvTerm env t1 ; t2' <- zonkEvTerm env t2 - ; return (EvTypeableTrFun t1' t2') } + ; return (EvTypeableTrFun tm' t1' t2') } zonkEvTypeable env (EvTypeableTyLit t1) = do { t1' <- zonkEvTerm env t1 ; return (EvTypeableTyLit t1') } @@ -1805,6 +1807,9 @@ commitFlexi flexi tv zonked_kind | isRuntimeRepTy zonked_kind -> do { traceTc "Defaulting flexi tyvar to LiftedRep:" (pprTyVar tv) ; return liftedRepTy } + | isMultiplicityTy zonked_kind + -> do { traceTc "Defaulting flexi tyvar to Many:" (pprTyVar tv) + ; return manyDataConTy } | otherwise -> do { traceTc "Defaulting flexi tyvar to Any:" (pprTyVar tv) ; return (anyTypeOfKind zonked_kind) } @@ -1871,12 +1876,20 @@ zonkTcTypeToType ty = initZonkEnv $ \ ze -> zonkTcTypeToTypeX ze ty zonkTcTypesToTypes :: [TcType] -> TcM [Type] zonkTcTypesToTypes tys = initZonkEnv $ \ ze -> zonkTcTypesToTypesX ze tys +zonkScaledTcTypeToTypeX :: ZonkEnv -> Scaled TcType -> TcM (Scaled TcType) +zonkScaledTcTypeToTypeX env (Scaled m ty) = Scaled <$> zonkTcTypeToTypeX env m + <*> zonkTcTypeToTypeX env ty + zonkTcTypeToTypeX :: ZonkEnv -> TcType -> TcM Type zonkTcTypesToTypesX :: ZonkEnv -> [TcType] -> TcM [Type] zonkCoToCo :: ZonkEnv -> Coercion -> TcM Coercion (zonkTcTypeToTypeX, zonkTcTypesToTypesX, zonkCoToCo, _) = mapTyCoX zonk_tycomapper +zonkScaledTcTypesToTypesX :: ZonkEnv -> [Scaled TcType] -> TcM [Scaled Type] +zonkScaledTcTypesToTypesX env scaled_tys = + mapM (zonkScaledTcTypeToTypeX env) scaled_tys + zonkTcMethInfoToMethInfoX :: ZonkEnv -> TcMethInfo -> TcM MethInfo zonkTcMethInfoToMethInfoX ze (name, ty, gdm_spec) = do { ty' <- zonkTcTypeToTypeX ze ty |