diff options
| author | Krzysztof Gogolewski <krzysztof.gogolewski@tweag.io> | 2020-06-15 19:58:10 +0200 |
|---|---|---|
| committer | Ben Gamari <ben@smart-cactus.org> | 2020-06-17 16:21:58 -0400 |
| commit | 40fa237e1daab7a76b9871bb6c50b953a1addf23 (patch) | |
| tree | 79751e932434be440ba35b4d65c54f25a437e134 /compiler/GHC/Tc | |
| parent | 20616959a7f4821034e14a64c3c9bf288c9bc956 (diff) | |
| download | haskell-40fa237e1daab7a76b9871bb6c50b953a1addf23.tar.gz | |
Linear types (#15981)
This is the first step towards implementation of the linear types proposal
(https://github.com/ghc-proposals/ghc-proposals/pull/111).
It features
* A language extension -XLinearTypes
* Syntax for linear functions in the surface language
* Linearity checking in Core Lint, enabled with -dlinear-core-lint
* Core-to-core passes are mostly compatible with linearity
* Fields in a data type can be linear or unrestricted; linear fields
have multiplicity-polymorphic constructors.
If -XLinearTypes is disabled, the GADT syntax defaults to linear fields
The following items are not yet supported:
* a # m -> b syntax (only prefix FUN is supported for now)
* Full multiplicity inference (multiplicities are really only checked)
* Decent linearity error messages
* Linear let, where, and case expressions in the surface language
(each of these currently introduce the unrestricted variant)
* Multiplicity-parametric fields
* Syntax for annotating lambda-bound or let-bound with a multiplicity
* Syntax for non-linear/multiple-field-multiplicity records
* Linear projections for records with a single linear field
* Linear pattern synonyms
* Multiplicity coercions (test LinearPolyType)
A high-level description can be found at
https://ghc.haskell.org/trac/ghc/wiki/LinearTypes/Implementation
Following the link above you will find a description of the changes made to Core.
This commit has been authored by
* Richard Eisenberg
* Krzysztof Gogolewski
* Matthew Pickering
* Arnaud Spiwack
With contributions from:
* Mark Barbone
* Alexander Vershilov
Updates haddock submodule.
Diffstat (limited to 'compiler/GHC/Tc')
43 files changed, 1045 insertions, 599 deletions
diff --git a/compiler/GHC/Tc/Deriv/Functor.hs b/compiler/GHC/Tc/Deriv/Functor.hs index 6a13cfaccd..a1af9166fe 100644 --- a/compiler/GHC/Tc/Deriv/Functor.hs +++ b/compiler/GHC/Tc/Deriv/Functor.hs @@ -40,6 +40,7 @@ import GHC.Tc.Utils.TcType import GHC.Core.TyCon import GHC.Core.TyCo.Rep import GHC.Core.Type +import GHC.Core.Multiplicity import GHC.Utils.Misc import GHC.Types.Var import GHC.Types.Var.Set @@ -557,7 +558,7 @@ deepSubtypesContaining tv foldDataConArgs :: FFoldType a -> DataCon -> [a] -- Fold over the arguments of the datacon foldDataConArgs ft con - = map foldArg (dataConOrigArgTys con) + = map foldArg (map scaledThing $ dataConOrigArgTys con) where foldArg = case getTyVar_maybe (last (tyConAppArgs (dataConOrigResTy con))) of diff --git a/compiler/GHC/Tc/Deriv/Generate.hs b/compiler/GHC/Tc/Deriv/Generate.hs index a9791043a2..7fa9975790 100644 --- a/compiler/GHC/Tc/Deriv/Generate.hs +++ b/compiler/GHC/Tc/Deriv/Generate.hs @@ -66,6 +66,7 @@ import GHC.Core.Coercion.Axiom ( coAxiomSingleBranch ) import GHC.Builtin.Types.Prim import GHC.Builtin.Types import GHC.Core.Type +import GHC.Core.Multiplicity import GHC.Core.Class import GHC.Types.Var.Set import GHC.Types.Var.Env @@ -210,7 +211,7 @@ gen_Eq_binds loc tycon = do bs_needed = take con_arity bs_RDRs tys_needed = dataConOrigArgTys data_con in - ([con1_pat, con2_pat], nested_eq_expr tys_needed as_needed bs_needed) + ([con1_pat, con2_pat], nested_eq_expr (map scaledThing tys_needed) as_needed bs_needed) where nested_eq_expr [] [] [] = true_Expr nested_eq_expr tys as bs @@ -456,7 +457,7 @@ gen_Ord_binds loc tycon = do -- Returns a case alternative Ki b1 b2 ... bv -> compare (a1,a2,...) with (b1,b2,...) mkInnerEqAlt op data_con = mkHsCaseAlt (nlConVarPat data_con_RDR bs_needed) $ - mkCompareFields op (dataConOrigArgTys data_con) + mkCompareFields op (map scaledThing $ dataConOrigArgTys data_con) where data_con_RDR = getRdrName data_con bs_needed = take (dataConSourceArity data_con) bs_RDRs @@ -1044,7 +1045,7 @@ gen_Read_binds get_fixity loc tycon is_infix = dataConIsInfix data_con is_record = labels `lengthExceeds` 0 as_needed = take con_arity as_RDRs - read_args = zipWithEqual "gen_Read_binds" read_arg as_needed (dataConOrigArgTys data_con) + read_args = zipWithEqual "gen_Read_binds" read_arg as_needed (map scaledThing $ dataConOrigArgTys data_con) (read_a1:read_a2:_) = read_args prefix_prec = appPrecedence @@ -1187,7 +1188,7 @@ gen_Show_binds get_fixity loc tycon where nm = wrapOpParens (unpackFS l) - show_args = zipWithEqual "gen_Show_binds" show_arg bs_needed arg_tys + show_args = zipWithEqual "gen_Show_binds" show_arg bs_needed (map scaledThing arg_tys) (show_arg1:show_arg2:_) = show_args show_prefix_args = intersperse (nlHsVar showSpace_RDR) show_args @@ -1378,7 +1379,7 @@ gen_data dflags data_type_name constr_names loc rep_tc gfoldl_eqn con = ([nlVarPat k_RDR, z_Pat, nlConVarPat con_name as_needed], - foldl' mk_k_app (z_Expr `nlHsApp` nlHsVar con_name) as_needed) + foldl' mk_k_app (z_Expr `nlHsApp` (eta_expand_data_con con)) as_needed) where con_name :: RdrName con_name = getRdrName con @@ -1398,9 +1399,18 @@ gen_data dflags data_type_name constr_names loc rep_tc gunfold_alt dc = mkHsCaseAlt (mk_unfold_pat dc) (mk_unfold_rhs dc) mk_unfold_rhs dc = foldr nlHsApp - (z_Expr `nlHsApp` nlHsVar (getRdrName dc)) + (z_Expr `nlHsApp` (eta_expand_data_con dc)) (replicate (dataConSourceArity dc) (nlHsVar k_RDR)) + eta_expand_data_con dc = + mkHsLam eta_expand_pats + (foldl nlHsApp (nlHsVar (getRdrName dc)) eta_expand_hsvars) + where + eta_expand_pats = map nlVarPat eta_expand_vars + eta_expand_hsvars = map nlHsVar eta_expand_vars + eta_expand_vars = take (dataConSourceArity dc) as_RDRs + + mk_unfold_pat dc -- Last one is a wild-pat, to avoid -- redundant test, and annoying warning | tag-fIRST_TAG == n_cons-1 = nlWildPat -- Last constructor @@ -1448,7 +1458,7 @@ gen_data dflags data_type_name constr_names loc rep_tc kind1, kind2 :: Kind kind1 = typeToTypeKind -kind2 = liftedTypeKind `mkVisFunTy` kind1 +kind2 = liftedTypeKind `mkVisFunTyMany` kind1 gfoldl_RDR, gunfold_RDR, toConstr_RDR, dataTypeOf_RDR, mkConstr_RDR, mkDataType_RDR, conIndex_RDR, prefix_RDR, infix_RDR, @@ -1960,7 +1970,7 @@ genAuxBindSpec dflags loc (DerivCon2Tag tycon) sig_ty = mkLHsSigWcType $ L loc $ XHsType $ NHsCoreTy $ mkSpecSigmaTy (tyConTyVars tycon) (tyConStupidTheta tycon) $ - mkParentType tycon `mkVisFunTy` intPrimTy + mkParentType tycon `mkVisFunTyMany` intPrimTy lots_of_constructors = tyConFamilySize tycon > 8 -- was: mAX_FAMILY_SIZE_FOR_VEC_RETURNS @@ -1984,7 +1994,7 @@ genAuxBindSpec dflags loc (DerivTag2Con tycon) where sig_ty = mkLHsSigWcType $ L loc $ XHsType $ NHsCoreTy $ mkSpecForAllTys (tyConTyVars tycon) $ - intTy `mkVisFunTy` mkParentType tycon + intTy `mkVisFunTyMany` mkParentType tycon rdr_name = tag2con_RDR dflags tycon diff --git a/compiler/GHC/Tc/Deriv/Generics.hs b/compiler/GHC/Tc/Deriv/Generics.hs index ced6f4b690..ea9862d305 100644 --- a/compiler/GHC/Tc/Deriv/Generics.hs +++ b/compiler/GHC/Tc/Deriv/Generics.hs @@ -29,6 +29,7 @@ import GHC.Tc.Deriv.Functor import GHC.Core.DataCon import GHC.Core.TyCon import GHC.Core.FamInstEnv ( FamInst, FamFlavor(..), mkSingleCoAxiom ) +import GHC.Core.Multiplicity import GHC.Tc.Instance.Family import GHC.Unit.Module ( moduleName, moduleNameFS , moduleUnit, unitFS, getModule ) @@ -168,7 +169,7 @@ canDoGenerics tc -- then we can't build the embedding-projection pair, because -- it relies on instantiating *polymorphic* sum and product types -- at the argument types of the constructors - bad_con dc = if (any bad_arg_type (dataConOrigArgTys dc)) + bad_con dc = if (any bad_arg_type (map scaledThing $ dataConOrigArgTys dc)) then (NotValid (ppr dc <+> text "must not have exotic unlifted or polymorphic arguments")) else (if (not (isVanillaDataCon dc)) @@ -575,7 +576,7 @@ tc_mkRepTy gk_ tycon k = mkD a = mkTyConApp d1 [ k, metaDataTy, sumP (tyConDataCons a) ] mkC a = mkTyConApp c1 [ k , metaConsTy a - , prod (dataConInstOrigArgTys a + , prod (map scaledThing . dataConInstOrigArgTys a . mkTyVarTys . tyConTyVars $ tycon) (dataConSrcBangs a) (dataConImplBangs a) @@ -741,7 +742,7 @@ mk1Sum gk_ us i n datacon = (from_alt, to_alt) argTys = dataConOrigArgTys datacon n_args = dataConSourceArity datacon - datacon_varTys = zip (map mkGenericLocal [us .. us+n_args-1]) argTys + datacon_varTys = zip (map mkGenericLocal [us .. us+n_args-1]) (map scaledThing argTys) datacon_vars = map fst datacon_varTys datacon_rdr = getRdrName datacon diff --git a/compiler/GHC/Tc/Deriv/Infer.hs b/compiler/GHC/Tc/Deriv/Infer.hs index 56dafd2097..17eff9a74b 100644 --- a/compiler/GHC/Tc/Deriv/Infer.hs +++ b/compiler/GHC/Tc/Deriv/Infer.hs @@ -41,6 +41,7 @@ import GHC.Tc.Utils.TcType import GHC.Core.TyCon import GHC.Core.TyCo.Ppr (pprTyVars) import GHC.Core.Type +import GHC.Core.Multiplicity import GHC.Tc.Solver import GHC.Tc.Validity (validDerivPred) import GHC.Tc.Utils.Unify (buildImplicationFor, checkConstraints) @@ -186,10 +187,10 @@ inferConstraintsStock (DerivInstTys { dit_cls_tys = cls_tys dataConInstOrigArgTys data_con all_rep_tc_args -- No constraints for unlifted types -- See Note [Deriving and unboxed types] - , not (isUnliftedType arg_ty) + , not (isUnliftedType (irrelevantMult arg_ty)) , let orig = DerivOriginDC data_con arg_n wildcard , preds_and_mbSubst - <- get_arg_constraints orig arg_t_or_k arg_ty + <- get_arg_constraints orig arg_t_or_k (irrelevantMult arg_ty) ] preds = concat predss -- If the constraints require a subtype to be of kind diff --git a/compiler/GHC/Tc/Deriv/Utils.hs b/compiler/GHC/Tc/Deriv/Utils.hs index 66adb4e554..e118c69830 100644 --- a/compiler/GHC/Tc/Deriv/Utils.hs +++ b/compiler/GHC/Tc/Deriv/Utils.hs @@ -48,6 +48,7 @@ import GHC.Tc.Utils.Monad import GHC.Tc.Utils.TcType import GHC.Builtin.Names.TH (liftClassKey) import GHC.Core.TyCon +import GHC.Core.Multiplicity import GHC.Core.TyCo.Ppr (pprSourceTyCon) import GHC.Core.Type import GHC.Utils.Misc @@ -853,7 +854,7 @@ cond_stdOK deriv_ctxt permissive dflags tc rep_tc = bad "has existential type variables in its type" | not (null theta) -- 4. = bad "has constraints in its type" - | not (permissive || all isTauTy (dataConOrigArgTys con)) -- 5. + | not (permissive || all isTauTy (map scaledThing $ dataConOrigArgTys con)) -- 5. = bad "has a higher-rank type" | otherwise = IsValid @@ -887,7 +888,7 @@ cond_args cls _ _ rep_tc 2 (text "for type" <+> quotes (ppr ty))) where bad_args = [ arg_ty | con <- tyConDataCons rep_tc - , arg_ty <- dataConOrigArgTys con + , Scaled _ arg_ty <- dataConOrigArgTys con , isLiftedType_maybe arg_ty /= Just True , not (ok_ty arg_ty) ] diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index d38b7adcbd..631be3465f 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -2079,7 +2079,7 @@ expandSynonymsToMatch ty1 ty2 = (ty1_ret, ty2_ret) (t1_2', t2_2') = go t1_2 t2_2 in (mkAppTy t1_1' t1_2', mkAppTy t2_1' t2_2') - go ty1@(FunTy _ t1_1 t1_2) ty2@(FunTy _ t2_1 t2_2) = + go ty1@(FunTy _ w1 t1_1 t1_2) ty2@(FunTy _ w2 t2_1 t2_2) | w1 `eqType` w2 = let (t1_1', t2_1') = go t1_1 t2_1 (t1_2', t2_2') = go t1_2 t2_2 in ( ty1 { ft_arg = t1_1', ft_res = t1_2' } diff --git a/compiler/GHC/Tc/Errors/Hole.hs b/compiler/GHC/Tc/Errors/Hole.hs index 7c0eaa7912..2edce28eac 100644 --- a/compiler/GHC/Tc/Errors/Hole.hs +++ b/compiler/GHC/Tc/Errors/Hole.hs @@ -620,7 +620,7 @@ findValidHoleFits tidy_env implics simples h@(Hole { hole_sort = ExprHole _ where newTyVars = replicateM refLvl $ setLvl <$> (newOpenTypeKind >>= newFlexiTyVar) setLvl = flip setMetaTyVarTcLevel hole_lvl - wrapWithVars vars = mkVisFunTys (map mkTyVarTy vars) hole_ty + wrapWithVars vars = mkVisFunTysMany (map mkTyVarTy vars) hole_ty sortFits :: SortingAlg -- How we should sort the hole fits -> [HoleFit] -- The subs to sort @@ -758,34 +758,34 @@ tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates = do { traceTc "lookingUp" $ ppr el ; maybeThing <- lookup el ; case maybeThing of - Just id | not_trivial id -> - do { fits <- fitsHole ty (idType id) + Just (id, id_ty) | not_trivial id -> + do { fits <- fitsHole ty id_ty ; case fits of - Just (wrp, matches) -> keep_it id wrp matches + Just (wrp, matches) -> keep_it id id_ty wrp matches _ -> discard_it } _ -> discard_it } where -- We want to filter out undefined and the likes from GHC.Err not_trivial id = nameModule_maybe (idName id) /= Just gHC_ERR - lookup :: HoleFitCandidate -> TcM (Maybe Id) - lookup (IdHFCand id) = return (Just id) + lookup :: HoleFitCandidate -> TcM (Maybe (Id, Type)) + lookup (IdHFCand id) = return (Just (id, idType id)) lookup hfc = do { thing <- tcLookup name ; return $ case thing of - ATcId {tct_id = id} -> Just id - AGlobal (AnId id) -> Just id + ATcId {tct_id = id} -> Just (id, idType id) + AGlobal (AnId id) -> Just (id, idType id) AGlobal (AConLike (RealDataCon con)) -> - Just (dataConWrapId con) + Just (dataConWrapId con, dataConNonlinearType con) _ -> Nothing } where name = case hfc of IdHFCand id -> idName id GreHFCand gre -> gre_name gre NameHFCand name -> name discard_it = go subs seen maxleft ty elts - keep_it eid wrp ms = go (fit:subs) (extendVarSet seen eid) + keep_it eid eid_ty wrp ms = go (fit:subs) (extendVarSet seen eid) ((\n -> n - 1) <$> maxleft) ty elts where - fit = HoleFit { hfId = eid, hfCand = el, hfType = (idType eid) + fit = HoleFit { hfId = eid, hfCand = el, hfType = eid_ty , hfRefLvl = length (snd ty) , hfWrap = wrp, hfMatches = ms , hfDoc = Nothing } diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs index c21a885970..6c5fda73af 100644 --- a/compiler/GHC/Tc/Gen/Arrow.hs +++ b/compiler/GHC/Tc/Gen/Arrow.hs @@ -29,6 +29,7 @@ import GHC.Tc.Utils.Monad import GHC.Tc.Utils.Env import GHC.Tc.Types.Origin import GHC.Tc.Types.Evidence +import GHC.Core.Multiplicity import GHC.Types.Id( mkLocalId ) import GHC.Tc.Utils.Instantiate import GHC.Builtin.Types @@ -92,7 +93,7 @@ tcProc pat cmd exp_ty ; (co, (exp_ty1, res_ty)) <- matchExpectedAppTy exp_ty ; (co1, (arr_ty, arg_ty)) <- matchExpectedAppTy exp_ty1 ; let cmd_env = CmdEnv { cmd_arr = arr_ty } - ; (pat', cmd') <- tcCheckPat ProcExpr pat arg_ty $ + ; (pat', cmd') <- tcCheckPat ProcExpr pat (unrestricted arg_ty) $ tcCmdTop cmd_env cmd (unitTy, res_ty) ; let res_co = mkTcTransCo co (mkTcAppCo co1 (mkTcNomReflCo res_ty)) @@ -179,7 +180,7 @@ tc_cmd env (HsCmdIf x fun@(SyntaxExprRn {}) pred b1 b2) res_ty -- Rebindable syn (text "Predicate type of `ifThenElse' depends on result type") ; (pred', fun') <- tcSyntaxOp IfOrigin fun (map synKnownType [pred_ty, r_ty, r_ty]) - (mkCheckExpType r_ty) $ \ _ -> + (mkCheckExpType r_ty) $ \ _ _ -> tcCheckMonoExpr pred pred_ty ; b1' <- tcCmd env b1 res_ty @@ -254,13 +255,13 @@ tc_cmd env -- Check the patterns, and the GRHSs inside ; (pats', grhss') <- setSrcSpan mtch_loc $ - tcPats LambdaExpr pats (map mkCheckExpType arg_tys) $ + tcPats LambdaExpr pats (map (unrestricted . mkCheckExpType) arg_tys) $ tc_grhss grhss cmd_stk' (mkCheckExpType res_ty) ; let match' = L mtch_loc (Match { m_ext = noExtField , m_ctxt = LambdaExpr, m_pats = pats' , m_grhss = grhss' }) - arg_tys = map hsLPatType pats' + arg_tys = map (unrestricted . hsLPatType) pats' cmd' = HsCmdLam x (MG { mg_alts = L l [match'] , mg_ext = MatchGroupTc arg_tys res_ty , mg_origin = origin }) @@ -309,7 +310,7 @@ tc_cmd env cmd@(HsCmdArrForm x expr f fixity cmd_args) (cmd_stk, res_ty) do { (cmd_args', cmd_tys) <- mapAndUnzipM tc_cmd_arg cmd_args -- We use alphaTyVar for 'w' ; let e_ty = mkInfForAllTy alphaTyVar $ - mkVisFunTys cmd_tys $ + mkVisFunTysMany cmd_tys $ mkCmdArrTy env (mkPairTy alphaTy cmd_stk) res_ty ; expr' <- tcCheckPolyExpr expr e_ty ; return (HsCmdArrForm x expr' f fixity cmd_args') } @@ -340,7 +341,7 @@ tcCmdMatches :: CmdEnv -> CmdType -> TcM (MatchGroup GhcTcId (LHsCmd GhcTcId)) tcCmdMatches env scrut_ty matches (stk, res_ty) - = tcMatchesCase match_ctxt scrut_ty matches (mkCheckExpType res_ty) + = tcMatchesCase match_ctxt (unrestricted scrut_ty) matches (mkCheckExpType res_ty) where match_ctxt = MC { mc_what = CaseAlt, mc_body = mc_body } @@ -382,7 +383,7 @@ tcArrDoStmt env _ (BodyStmt _ rhs _ _) res_ty thing_inside tcArrDoStmt env ctxt (BindStmt _ pat rhs) res_ty thing_inside = do { (rhs', pat_ty) <- tc_arr_rhs env rhs - ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $ + ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat (unrestricted pat_ty) $ thing_inside res_ty ; return (mkTcBindStmt pat' rhs', thing) } @@ -390,7 +391,7 @@ tcArrDoStmt env ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names , recS_rec_ids = rec_names }) res_ty thing_inside = do { let tup_names = rec_names ++ filterOut (`elem` rec_names) later_names ; tup_elt_tys <- newFlexiTyVarTys (length tup_names) liftedTypeKind - ; let tup_ids = zipWith mkLocalId tup_names tup_elt_tys + ; let tup_ids = zipWith (\n p -> mkLocalId n Many p) tup_names tup_elt_tys -- Many because it's a recursive definition ; tcExtendIdEnv tup_ids $ do { (stmts', tup_rets) <- tcStmtsAndThen ctxt (tcArrDoStmt env) stmts res_ty $ \ _res_ty' -> @@ -439,7 +440,7 @@ mkPairTy :: Type -> Type -> Type mkPairTy t1 t2 = mkTyConApp pairTyCon [t1,t2] arrowTyConKind :: Kind -- *->*->* -arrowTyConKind = mkVisFunTys [liftedTypeKind, liftedTypeKind] liftedTypeKind +arrowTyConKind = mkVisFunTysMany [liftedTypeKind, liftedTypeKind] liftedTypeKind {- ************************************************************************ diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs index b88a672795..b87db660e2 100644 --- a/compiler/GHC/Tc/Gen/Bind.hs +++ b/compiler/GHC/Tc/Gen/Bind.hs @@ -41,6 +41,7 @@ import GHC.Tc.Types.Evidence import GHC.Tc.Gen.HsType import GHC.Tc.Gen.Pat import GHC.Tc.Utils.TcMType +import GHC.Core.Multiplicity import GHC.Core.FamInstEnv( normaliseType ) import GHC.Tc.Instance.Family( tcGetFamInstEnvs ) import GHC.Core.TyCon @@ -398,6 +399,9 @@ tcValBinds top_lvl binds sigs thing_inside -- Do not extend the TcBinderStack; instead -- we extend it on a per-rhs basis in tcExtendForRhs -- See Note [Relevant bindings and the binder stack] + -- + -- For the moment, let bindings and top-level bindings introduce + -- only unrestricted variables. ; tcExtendSigIds top_lvl poly_ids $ do { (binds', (extra_binds', thing)) <- tcBindGroups top_lvl sig_fn prag_fn binds $ @@ -497,9 +501,10 @@ tc_group top_lvl sig_fn prag_fn (Recursive, binds) closed thing_inside go :: [SCC (LHsBind GhcRn)] -> TcM (LHsBinds GhcTcId, thing) go (scc:sccs) = do { (binds1, ids1) <- tc_scc scc - ; (binds2, thing) <- tcExtendLetEnv top_lvl sig_fn - closed ids1 $ - go sccs + -- recursive bindings must be unrestricted + -- (the ids added to the environment here are the name of the recursive definitions). + ; (binds2, thing) <- tcExtendLetEnv top_lvl sig_fn closed ids1 + (go sccs) ; return (binds1 `unionBags` binds2, thing) } go [] = do { thing <- thing_inside; return (emptyBag, thing) } @@ -541,6 +546,8 @@ tc_single top_lvl sig_fn prag_fn lbind closed thing_inside NonRecursive NonRecursive closed [lbind] + -- since we are defining a non-recursive binding, it is not necessary here + -- to define an unrestricted binding. But we do so until toplevel linear bindings are supported. ; thing <- tcExtendLetEnv top_lvl sig_fn closed ids thing_inside ; return (binds1, thing) } @@ -633,7 +640,7 @@ recoveryCode binder_names sig_fn , Just poly_id <- completeSigPolyId_maybe sig = poly_id | otherwise - = mkLocalId name forall_a_a + = mkLocalId name Many forall_a_a forall_a_a :: TcType -- At one point I had (forall r (a :: TYPE r). a), but of course @@ -703,7 +710,7 @@ tcPolyCheck prag_fn -- NB: tcSkolemise makes fresh type variables -- See Note [Instantiate sig with fresh variables] - let mono_id = mkLocalId mono_name rho_ty in + let mono_id = mkLocalId mono_name (varMult poly_id) rho_ty in tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $ -- Why mono_id in the BinderStack? -- See Note [Relevant bindings and the binder stack] @@ -719,7 +726,7 @@ tcPolyCheck prag_fn -- We re-use mono-name, but we could equally well use a fresh one ; let prag_sigs = lookupPragEnv prag_fn name - poly_id2 = mkLocalId mono_name (idType poly_id) + poly_id2 = mkLocalId mono_name (idMult poly_id) (idType poly_id) ; spec_prags <- tcSpecPrags poly_id prag_sigs ; poly_id <- addInlinePrags poly_id prag_sigs @@ -933,7 +940,7 @@ mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty -- do this check; otherwise (#14000) we may report an ambiguity -- error for a rather bogus type. - ; return (mkLocalId poly_name inferred_poly_ty) } + ; return (mkLocalId poly_name Many inferred_poly_ty) } chooseInferredQuantifiers :: TcThetaType -- inferred @@ -1288,7 +1295,7 @@ tcMonoBinds is_rec sig_fn no_gen -- type of the thing whose rhs we are type checking tcMatchesFun (L nm_loc name) matches exp_ty - ; mono_id <- newLetBndr no_gen name rhs_ty + ; mono_id <- newLetBndr no_gen name Many rhs_ty ; return (unitBag $ L b_loc $ FunBind { fun_id = L nm_loc mono_id, fun_matches = matches', @@ -1361,7 +1368,10 @@ tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name | otherwise -- No type signature = do { mono_ty <- newOpenFlexiTyVarTy - ; mono_id <- newLetBndr no_gen name mono_ty + ; mono_id <- newLetBndr no_gen name Many mono_ty + -- This ^ generates a binder with Many multiplicity because all + -- let/where-binders are unrestricted. When we introduce linear let + -- binders, we will need to retrieve the multiplicity information. ; let mono_info = MBI { mbi_poly_name = name , mbi_sig = Nothing , mbi_mono_id = mono_id } @@ -1379,7 +1389,10 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss }) ; ((pat', nosig_mbis), pat_ty) <- addErrCtxt (patMonoBindsCtxt pat grhss) $ tcInfer $ \ exp_ty -> - tcLetPat inst_sig_fun no_gen pat exp_ty $ + tcLetPat inst_sig_fun no_gen pat (unrestricted exp_ty) $ + -- The above inferred type get an unrestricted multiplicity. It may be + -- worth it to try and find a finer-grained multiplicity here + -- if examples warrant it. mapM lookup_info nosig_names ; let mbis = sig_mbis ++ nosig_mbis @@ -1426,7 +1439,10 @@ newSigLetBndr (LetGblBndr prags) name (TISI { sig_inst_sig = id_sig }) | CompleteSig { sig_bndr = poly_id } <- id_sig = addInlinePrags poly_id (lookupPragEnv prags name) newSigLetBndr no_gen name (TISI { sig_inst_tau = tau }) - = newLetBndr no_gen name tau + = newLetBndr no_gen name Many tau + -- Binders with a signature are currently always of multiplicity + -- Many. Because they come either from toplevel, let, or where + -- declarations. Which are all unrestricted currently. ------------------- tcRhs :: TcMonoBind -> TcM (HsBind GhcTcId) @@ -1450,6 +1466,12 @@ tcRhs (TcPatBind infos pat' grhss pat_ty) tcExtendIdBinderStackForRhs infos $ do { traceTc "tcRhs: pat bind" (ppr pat' $$ ppr pat_ty) ; grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $ + tcScalingUsage Many $ + -- Like in tcMatchesFun, this scaling happens because all + -- let bindings are unrestricted. A difference, here, is + -- that when this is not the case, any more, we will have to + -- make sure that the pattern is strict, otherwise this will + -- be desugar to incorrect code. tcGRHSsPat grhss pat_ty ; return ( PatBind { pat_lhs = pat', pat_rhs = grhss' , pat_ext = NPatBindTc emptyNameSet pat_ty diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs index 9294d5fe64..477c8eaa1d 100644 --- a/compiler/GHC/Tc/Gen/Expr.hs +++ b/compiler/GHC/Tc/Gen/Expr.hs @@ -35,6 +35,8 @@ import GHC.Tc.Utils.Zonk import GHC.Tc.Utils.Monad import GHC.Tc.Utils.Unify import GHC.Types.Basic +import GHC.Core.Multiplicity +import GHC.Core.UsageEnv import GHC.Tc.Utils.Instantiate import GHC.Tc.Gen.Bind ( chooseInferredQuantifiers, tcLocalBinds ) import GHC.Tc.Gen.Sig ( tcUserTypeSig, tcInstSig ) @@ -69,6 +71,7 @@ import GHC.Core.Type import GHC.Tc.Types.Evidence import GHC.Types.Var.Set import GHC.Builtin.Types +import GHC.Builtin.Types.Prim( multiplicityTyVarList ) import GHC.Builtin.PrimOps( tagToEnumKey ) import GHC.Builtin.Names import GHC.Driver.Session @@ -218,8 +221,8 @@ tcExpr (HsOverLit x lit) res_ty tcExpr (NegApp x expr neg_expr) res_ty = do { (expr', neg_expr') <- tcSyntaxOp NegateOrigin neg_expr [SynAny] res_ty $ - \[arg_ty] -> - tcLExpr expr (mkCheckExpType arg_ty) + \[arg_ty] [arg_mult] -> + tcScalingUsage arg_mult $ tcLExpr expr (mkCheckExpType arg_ty) ; return (NegApp x expr' neg_expr') } tcExpr e@(HsIPVar _ x) res_ty @@ -362,6 +365,13 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty ; (wrap_arg1, [arg2_sigma], op_res_ty) <- matchActualFunTysRho doc orig1 (Just (unLoc arg1)) 1 arg1_ty + ; mult_wrap <- tcSubMult AppOrigin Many (scaledMult arg2_sigma) + -- See Note [tcSubMult's wrapper] in TcUnify. + -- + -- When ($) becomes multiplicity-polymorphic, then the above check will + -- need to go. But in the meantime, it would produce ill-typed + -- desugared code to accept linear functions to the left of a ($). + -- We have (arg1 $ arg2) -- So: arg1_ty = arg2_ty -> op_res_ty -- where arg2_sigma maybe polymorphic; that's the point @@ -372,8 +382,8 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty -- ($) :: forall (r:RuntimeRep) (a:*) (b:TYPE r). (a->b) -> a -> b -- Eg we do not want to allow (D# $ 4.0#) #5570 -- (which gives a seg fault) - ; _ <- unifyKind (Just (XHsType $ NHsCoreTy arg2_sigma)) - (tcTypeKind arg2_sigma) liftedTypeKind + ; _ <- unifyKind (Just (XHsType $ NHsCoreTy (scaledThing arg2_sigma))) + (tcTypeKind (scaledThing arg2_sigma)) liftedTypeKind -- Ignore the evidence. arg2_sigma must have type * or #, -- because we know (arg2_sigma -> op_res_ty) is well-kinded -- (because otherwise matchActualFunTysRho would fail) @@ -385,14 +395,14 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty ; op_id <- tcLookupId op_name ; let op' = L loc (mkHsWrap (mkWpTyApps [ getRuntimeRep op_res_ty - , arg2_sigma + , scaledThing arg2_sigma , op_res_ty]) (HsVar noExtField (L lv op_id))) -- arg1' :: arg1_ty -- wrap_arg1 :: arg1_ty "->" (arg2_sigma -> op_res_ty) -- op' :: (a2_ty -> op_res_ty) -> a2_ty -> op_res_ty - expr' = OpApp fix (mkLHsWrap wrap_arg1 arg1') op' arg2' + expr' = OpApp fix (mkLHsWrap (wrap_arg1 <.> mult_wrap) arg1') op' arg2' ; tcWrapResult expr expr' op_res_ty res_ty } @@ -430,12 +440,12 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty tcExpr expr@(SectionR x op arg2) res_ty = do { (op', op_ty) <- tcInferRhoNC op - ; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty) + ; (wrap_fun, [Scaled arg1_mult arg1_ty, arg2_ty], op_res_ty) <- matchActualFunTysRho (mk_op_msg op) fn_orig (Just (unLoc op)) 2 op_ty ; arg2' <- tcArg (unLoc op) arg2 arg2_ty 2 ; let expr' = SectionR x (mkLHsWrap wrap_fun op') arg2' - act_res_ty = mkVisFunTy arg1_ty op_res_ty + act_res_ty = mkVisFunTy arg1_mult arg1_ty op_res_ty ; tcWrapResultMono expr expr' act_res_ty res_ty } where @@ -491,14 +501,21 @@ tcExpr expr@(ExplicitTuple x tup_args boxity) res_ty ; tup_args1 <- tcTupArgs tup_args arg_tys ; let expr' = ExplicitTuple x tup_args1 boxity - act_res_ty = mkVisFunTys [ty | (ty, (L _ (Missing _))) - <- arg_tys `zip` tup_args] - (mkTupleTy1 boxity arg_tys) + + missing_tys = [ty | (ty, L _ (Missing _)) <- zip arg_tys tup_args] + w_tyvars = multiplicityTyVarList (length missing_tys) + -- See Note [Linear fields generalization] + w_tvb = map (mkTyVarBinder Inferred) w_tyvars + act_res_ty + = mkForAllTys w_tvb $ + mkVisFunTys [ mkScaled (mkTyVarTy w_ty) ty | + (ty, w_ty) <- zip missing_tys w_tyvars] + (mkTupleTy1 boxity arg_tys) -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make ; traceTc "ExplicitTuple" (ppr act_res_ty $$ ppr res_ty) - ; tcWrapResultMono expr expr' act_res_ty res_ty } + ; tcWrapResult expr expr' act_res_ty res_ty } tcExpr (ExplicitSum _ alt arity expr) res_ty = do { let sum_tc = sumTyCon arity @@ -522,9 +539,15 @@ tcExpr (ExplicitList _ witness exprs) res_ty Just fln -> do { ((exprs', elt_ty), fln') <- tcSyntaxOp ListOrigin fln [synKnownType intTy, SynList] res_ty $ - \ [elt_ty] -> + \ [elt_ty] [_int_mul, list_mul] -> + -- We ignore _int_mul because the integer (first + -- argument of fromListN) is statically known: it + -- is desugared to a literal. Therefore there is + -- no variable of which to scale the usage in that + -- first argument, and `_int_mul` is completely + -- free in this expression. do { exprs' <- - mapM (tc_elt elt_ty) exprs + mapM (tcScalingUsage list_mul . tc_elt elt_ty) exprs ; return (exprs', elt_ty) } ; return $ ExplicitList elt_ty (Just fln') exprs' } @@ -553,6 +576,9 @@ tcExpr (HsCase x scrut matches) res_ty -- -- But now, in the GADT world, we need to typecheck the scrutinee -- first, to get type info that may be refined in the case alternatives + let mult = Many + -- There is not yet syntax or inference mechanism for case + -- expressions to be anything else than unrestricted. -- Typecheck the scrutinee. We use tcInferRho but tcInferSigma -- would also be possible (tcMatchesCase accepts sigma-types) @@ -560,10 +586,10 @@ tcExpr (HsCase x scrut matches) res_ty -- case id of {..} -- case (\v -> v) of {..} -- This design choice is discussed in #17790 - (scrut', scrut_ty) <- tcInferRho scrut + ; (scrut', scrut_ty) <- tcScalingUsage mult $ tcInferRho scrut ; traceTc "HsCase" (ppr scrut_ty) - ; matches' <- tcMatchesCase match_ctxt scrut_ty matches res_ty + ; matches' <- tcMatchesCase match_ctxt (Scaled mult scrut_ty) matches res_ty ; return (HsCase x scrut' matches') } where match_ctxt = MC { mc_what = CaseAlt, @@ -575,17 +601,18 @@ tcExpr (HsIf x NoSyntaxExprRn pred b1 b2) res_ty -- Ordinary 'if' -- Just like Note [Case branches must never infer a non-tau type] -- in GHC.Tc.Gen.Match (See #10619) - ; b1' <- tcLExpr b1 res_ty - ; b2' <- tcLExpr b2 res_ty + ; (u1,b1') <- tcCollectingUsage $ tcLExpr b1 res_ty + ; (u2,b2') <- tcCollectingUsage $ tcLExpr b2 res_ty + ; tcEmitBindingUsage (supUE u1 u2) ; return (HsIf x NoSyntaxExprTc pred' b1' b2') } tcExpr (HsIf x fun@(SyntaxExprRn {}) pred b1 b2) res_ty = do { ((pred', b1', b2'), fun') <- tcSyntaxOp IfOrigin fun [SynAny, SynAny, SynAny] res_ty $ - \ [pred_ty, b1_ty, b2_ty] -> - do { pred' <- tcCheckPolyExpr pred pred_ty - ; b1' <- tcCheckPolyExpr b1 b1_ty - ; b2' <- tcCheckPolyExpr b2 b2_ty + \ [pred_ty, b1_ty, b2_ty] [pred_mult, b1_mult, b2_mult] -> + do { pred' <- tcScalingUsage pred_mult $ tcCheckPolyExpr pred pred_ty + ; b1' <- tcScalingUsage b1_mult $ tcCheckPolyExpr b1 b1_ty + ; b2' <- tcScalingUsage b2_mult $ tcCheckPolyExpr b2 b2_ty ; return (pred', b1', b2') } ; return (HsIf x fun' pred' b1' b2') } @@ -679,7 +706,12 @@ tcExpr expr@(RecordCon { rcon_con_name = L loc con_name Nothing -> nonBidirectionalErr (conLikeName con_like) ; Just con_id -> - do { rbinds' <- tcRecordBinds con_like arg_tys rbinds + do { rbinds' <- tcRecordBinds con_like (map scaledThing arg_tys) rbinds + -- It is currently not possible for a record to have + -- multiplicities. When they do, `tcRecordBinds` will take + -- scaled types instead. Meanwhile, it's safe to take + -- `scaledThing` above, as we know all the multiplicities are + -- Many. ; let rcon_tc = RecordConTc { rcon_con_like = con_like , rcon_con_expr = mkHsWrap con_wrap con_expr } @@ -829,7 +861,20 @@ following. tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty = ASSERT( notNull rbnds ) do { -- STEP -2: typecheck the record_expr, the record to be updated - (record_expr', record_rho) <- tcInferRho record_expr + (record_expr', record_rho) <- tcScalingUsage Many $ tcInferRho record_expr + -- Record update drops some of the content of the record (namely the + -- content of the field being updated). As a consequence, unless the + -- field being updated is unrestricted in the record, or we need an + -- unrestricted record. Currently, we simply always require an + -- unrestricted record. + -- + -- Consider the following example: + -- + -- data R a = R { self :: a } + -- bad :: a ⊸ () + -- bad x = let r = R x in case r { self = () } of { R x' -> x' } + -- + -- This should definitely *not* typecheck. -- STEP -1 See Note [Disambiguating record fields] -- After this we know that rbinds is unambiguous @@ -886,8 +931,13 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty -- Take apart a representative constructor ; let con1 = ASSERT( not (null relevant_cons) ) head relevant_cons - (con1_tvs, _, _, _prov_theta, req_theta, con1_arg_tys, _) + (con1_tvs, _, _, _prov_theta, req_theta, scaled_con1_arg_tys, _) = conLikeFullSig con1 + con1_arg_tys = map scaledThing scaled_con1_arg_tys + -- We can safely drop the fields' multiplicities because + -- they are currently always 1: there is no syntax for record + -- fields with other multiplicities yet. This way we don't need + -- to handle it in the rest of the function con1_flds = map flLabel $ conLikeFieldLabels con1 con1_tv_tys = mkTyVarTys con1_tvs con1_res_ty = case mtycon of @@ -1069,36 +1119,36 @@ tcArithSeq :: Maybe (SyntaxExpr GhcRn) -> ArithSeqInfo GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc) tcArithSeq witness seq@(From expr) res_ty - = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty - ; expr' <- tcCheckPolyExpr expr elt_ty + = do { (wrap, elt_mult, elt_ty, wit') <- arithSeqEltType witness res_ty + ; expr' <-tcScalingUsage elt_mult $ tcCheckPolyExpr expr elt_ty ; enum_from <- newMethodFromName (ArithSeqOrigin seq) enumFromName [elt_ty] ; return $ mkHsWrap wrap $ ArithSeq enum_from wit' (From expr') } tcArithSeq witness seq@(FromThen expr1 expr2) res_ty - = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty - ; expr1' <- tcCheckPolyExpr expr1 elt_ty - ; expr2' <- tcCheckPolyExpr expr2 elt_ty + = do { (wrap, elt_mult, elt_ty, wit') <- arithSeqEltType witness res_ty + ; expr1' <- tcScalingUsage elt_mult $ tcCheckPolyExpr expr1 elt_ty + ; expr2' <- tcScalingUsage elt_mult $ tcCheckPolyExpr expr2 elt_ty ; enum_from_then <- newMethodFromName (ArithSeqOrigin seq) enumFromThenName [elt_ty] ; return $ mkHsWrap wrap $ ArithSeq enum_from_then wit' (FromThen expr1' expr2') } tcArithSeq witness seq@(FromTo expr1 expr2) res_ty - = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty - ; expr1' <- tcCheckPolyExpr expr1 elt_ty - ; expr2' <- tcCheckPolyExpr expr2 elt_ty + = do { (wrap, elt_mult, elt_ty, wit') <- arithSeqEltType witness res_ty + ; expr1' <- tcScalingUsage elt_mult $ tcCheckPolyExpr expr1 elt_ty + ; expr2' <- tcScalingUsage elt_mult $ tcCheckPolyExpr expr2 elt_ty ; enum_from_to <- newMethodFromName (ArithSeqOrigin seq) enumFromToName [elt_ty] ; return $ mkHsWrap wrap $ ArithSeq enum_from_to wit' (FromTo expr1' expr2') } tcArithSeq witness seq@(FromThenTo expr1 expr2 expr3) res_ty - = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty - ; expr1' <- tcCheckPolyExpr expr1 elt_ty - ; expr2' <- tcCheckPolyExpr expr2 elt_ty - ; expr3' <- tcCheckPolyExpr expr3 elt_ty + = do { (wrap, elt_mult, elt_ty, wit') <- arithSeqEltType witness res_ty + ; expr1' <- tcScalingUsage elt_mult $ tcCheckPolyExpr expr1 elt_ty + ; expr2' <- tcScalingUsage elt_mult $ tcCheckPolyExpr expr2 elt_ty + ; expr3' <- tcScalingUsage elt_mult $ tcCheckPolyExpr expr3 elt_ty ; eft <- newMethodFromName (ArithSeqOrigin seq) enumFromThenToName [elt_ty] ; return $ mkHsWrap wrap $ @@ -1106,16 +1156,16 @@ tcArithSeq witness seq@(FromThenTo expr1 expr2 expr3) res_ty ----------------- arithSeqEltType :: Maybe (SyntaxExpr GhcRn) -> ExpRhoType - -> TcM (HsWrapper, TcType, Maybe (SyntaxExpr GhcTc)) + -> TcM (HsWrapper, Mult, TcType, Maybe (SyntaxExpr GhcTc)) arithSeqEltType Nothing res_ty = do { res_ty <- expTypeToType res_ty ; (coi, elt_ty) <- matchExpectedListTy res_ty - ; return (mkWpCastN coi, elt_ty, Nothing) } + ; return (mkWpCastN coi, One, elt_ty, Nothing) } arithSeqEltType (Just fl) res_ty - = do { (elt_ty, fl') + = do { ((elt_mult, elt_ty), fl') <- tcSyntaxOp ListOrigin fl [SynList] res_ty $ - \ [elt_ty] -> return elt_ty - ; return (idHsWrapper, elt_ty, Just fl') } + \ [elt_ty] [elt_mult] -> return (elt_mult, elt_ty) + ; return (idHsWrapper, elt_mult, elt_ty, Just fl') } {- ************************************************************************ @@ -1346,7 +1396,7 @@ tcArgs fun orig_fun_ty orig_args _ -> False go :: Int -- Which argment number this is (incl type args) - -> [TcSigmaType] -- Value args to which applied so far + -> [Scaled TcSigmaType] -- Value args to which applied so far -> TcSigmaType -> [LHsExprArgIn] -> TcM ([LHsExprArgOut], TcSigmaType) go _ _ fun_ty [] = traceTc "tcArgs:ret" (ppr fun_ty) >> return ([], fun_ty) @@ -1491,16 +1541,16 @@ and we had the visible type application ---------------- tcArg :: HsExpr GhcRn -- The function (for error messages) -> LHsExpr GhcRn -- Actual arguments - -> TcSigmaType -- expected arg type + -> Scaled TcSigmaType -- expected arg type -> Int -- # of argument -> TcM (LHsExpr GhcTc) -- Resulting argument -tcArg fun arg ty arg_no +tcArg fun arg (Scaled mult ty) arg_no = addErrCtxt (funAppCtxt fun arg arg_no) $ do { traceTc "tcArg" $ vcat [ ppr arg_no <+> text "of" <+> ppr fun , text "arg type:" <+> ppr ty , text "arg:" <+> ppr arg ] - ; tcCheckPolyExprNC arg ty } + ; tcScalingUsage mult $ tcCheckPolyExprNC arg ty } ---------------- tcTupArgs :: [LHsTupArg GhcRn] -> [TcSigmaType] -> TcM [LHsTupArg GhcTc] @@ -1517,7 +1567,10 @@ tcSyntaxOp :: CtOrigin -> SyntaxExprRn -> [SyntaxOpType] -- ^ shape of syntax operator arguments -> ExpRhoType -- ^ overall result type - -> ([TcSigmaType] -> TcM a) -- ^ Type check any arguments + -> ([TcSigmaType] -> [Mult] -> TcM a) -- ^ Type check any arguments, + -- takes a type per hole and a + -- multiplicity per arrow in + -- the shape. -> TcM (a, SyntaxExprTc) -- ^ Typecheck a syntax operator -- The operator is a variable or a lambda at this stage (i.e. renamer @@ -1531,7 +1584,7 @@ tcSyntaxOpGen :: CtOrigin -> SyntaxExprRn -> [SyntaxOpType] -> SyntaxOpType - -> ([TcSigmaType] -> TcM a) + -> ([TcSigmaType] -> [Mult] -> TcM a) -> TcM (a, SyntaxExprTc) tcSyntaxOpGen orig (SyntaxExprRn op) arg_tys res_ty thing_inside = do { (expr, sigma) <- tcInferAppHead op @@ -1560,7 +1613,7 @@ two tcSynArgs. tcSynArgE :: CtOrigin -> TcSigmaType -> SyntaxOpType -- ^ shape it is expected to have - -> ([TcSigmaType] -> TcM a) -- ^ check the arguments + -> ([TcSigmaType] -> [Mult] -> TcM a) -- ^ check the arguments -> TcM (a, HsWrapper) -- ^ returns a wrapper :: (type of right shape) "->" (type passed in) tcSynArgE orig sigma_ty syn_ty thing_inside @@ -1570,26 +1623,26 @@ tcSynArgE orig sigma_ty syn_ty thing_inside ; return (result, skol_wrap <.> ty_wrapper) } where go rho_ty SynAny - = do { result <- thing_inside [rho_ty] + = do { result <- thing_inside [rho_ty] [] ; return (result, idHsWrapper) } go rho_ty SynRho -- same as SynAny, because we skolemise eagerly - = do { result <- thing_inside [rho_ty] + = do { result <- thing_inside [rho_ty] [] ; return (result, idHsWrapper) } go rho_ty SynList = do { (list_co, elt_ty) <- matchExpectedListTy rho_ty - ; result <- thing_inside [elt_ty] + ; result <- thing_inside [elt_ty] [] ; return (result, mkWpCastN list_co) } go rho_ty (SynFun arg_shape res_shape) = do { ( match_wrapper -- :: (arg_ty -> res_ty) "->" rho_ty - , ( ( (result, arg_ty, res_ty) + , ( ( (result, arg_ty, res_ty, op_mult) , res_wrapper ) -- :: res_ty_out "->" res_ty , arg_wrapper1, [], arg_wrapper2 ) ) -- :: arg_ty "->" arg_ty_out <- matchExpectedFunTys herald GenSigCtxt 1 (mkCheckExpType rho_ty) $ \ [arg_ty] res_ty -> - do { arg_tc_ty <- expTypeToType arg_ty + do { arg_tc_ty <- expTypeToType (scaledThing arg_ty) ; res_tc_ty <- expTypeToType res_ty -- another nested arrow is too much for now, @@ -1600,24 +1653,25 @@ tcSynArgE orig sigma_ty syn_ty thing_inside , text "Too many nested arrows in SyntaxOpType" $$ pprCtOrigin orig ) + ; let arg_mult = scaledMult arg_ty ; tcSynArgA orig arg_tc_ty [] arg_shape $ - \ arg_results -> + \ arg_results arg_res_mults -> tcSynArgE orig res_tc_ty res_shape $ - \ res_results -> - do { result <- thing_inside (arg_results ++ res_results) - ; return (result, arg_tc_ty, res_tc_ty) }} + \ res_results res_res_mults -> + do { result <- thing_inside (arg_results ++ res_results) ([arg_mult] ++ arg_res_mults ++ res_res_mults) + ; return (result, arg_tc_ty, res_tc_ty, arg_mult) }} ; return ( result , match_wrapper <.> mkWpFun (arg_wrapper2 <.> arg_wrapper1) res_wrapper - arg_ty res_ty doc ) } + (Scaled op_mult arg_ty) res_ty doc ) } where herald = text "This rebindable syntax expects a function with" doc = text "When checking a rebindable syntax operator arising from" <+> ppr orig go rho_ty (SynType the_ty) = do { wrap <- tcSubTypePat orig GenSigCtxt the_ty rho_ty - ; result <- thing_inside [] + ; result <- thing_inside [] [] ; return (result, wrap) } -- works on "actual" types, instantiating where necessary @@ -1626,7 +1680,7 @@ tcSynArgA :: CtOrigin -> TcSigmaType -> [SyntaxOpType] -- ^ argument shapes -> SyntaxOpType -- ^ result shape - -> ([TcSigmaType] -> TcM a) -- ^ check the arguments + -> ([TcSigmaType] -> [Mult] -> TcM a) -- ^ check the arguments -> TcM (a, HsWrapper, [HsWrapper], HsWrapper) -- ^ returns a wrapper to be applied to the original function, -- wrappers to be applied to arguments @@ -1637,24 +1691,24 @@ tcSynArgA orig sigma_ty arg_shapes res_shape thing_inside (length arg_shapes) sigma_ty -- match_wrapper :: sigma_ty "->" (arg_tys -> res_ty) ; ((result, res_wrapper), arg_wrappers) - <- tc_syn_args_e arg_tys arg_shapes $ \ arg_results -> + <- tc_syn_args_e (map scaledThing arg_tys) arg_shapes $ \ arg_results arg_res_mults -> tc_syn_arg res_ty res_shape $ \ res_results -> - thing_inside (arg_results ++ res_results) + thing_inside (arg_results ++ res_results) (map scaledMult arg_tys ++ arg_res_mults) ; return (result, match_wrapper, arg_wrappers, res_wrapper) } where herald = text "This rebindable syntax expects a function with" tc_syn_args_e :: [TcSigmaType] -> [SyntaxOpType] - -> ([TcSigmaType] -> TcM a) + -> ([TcSigmaType] -> [Mult] -> TcM a) -> TcM (a, [HsWrapper]) -- the wrappers are for arguments tc_syn_args_e (arg_ty : arg_tys) (arg_shape : arg_shapes) thing_inside = do { ((result, arg_wraps), arg_wrap) - <- tcSynArgE orig arg_ty arg_shape $ \ arg1_results -> - tc_syn_args_e arg_tys arg_shapes $ \ args_results -> - thing_inside (arg1_results ++ args_results) + <- tcSynArgE orig arg_ty arg_shape $ \ arg1_results arg1_mults -> + tc_syn_args_e arg_tys arg_shapes $ \ args_results args_mults -> + thing_inside (arg1_results ++ args_results) (arg1_mults ++ args_mults) ; return (result, arg_wrap : arg_wraps) } - tc_syn_args_e _ _ thing_inside = (, []) <$> thing_inside [] + tc_syn_args_e _ _ thing_inside = (, []) <$> thing_inside [] [] tc_syn_arg :: TcSigmaType -> SyntaxOpType -> ([TcSigmaType] -> TcM a) @@ -1817,7 +1871,7 @@ tcCheckRecSelId rn_expr f@(Unambiguous {}) res_ty tcCheckRecSelId rn_expr (Ambiguous _ lbl) res_ty = case tcSplitFunTy_maybe =<< checkingExpType_maybe res_ty of Nothing -> ambiguousSelector lbl - Just (arg, _) -> do { sel_name <- disambiguateSelector lbl arg + Just (arg, _) -> do { sel_name <- disambiguateSelector lbl (scaledThing arg) ; tcCheckRecSelId rn_expr (Unambiguous sel_name lbl) res_ty } @@ -1862,6 +1916,7 @@ tc_infer_id lbl id_name ATcId { tct_id = id } -> do { check_naughty id -- Note [Local record selectors] ; checkThLocalId id + ; tcEmitBindingUsage $ unitUE id_name One ; return_id id } AGlobal (AnId id) @@ -1881,25 +1936,47 @@ tc_infer_id lbl id_name return_id id = return (HsVar noExtField (noLoc id), idType id) return_data_con con - -- For data constructors, must perform the stupid-theta check - | null stupid_theta - = return (HsConLikeOut noExtField (RealDataCon con), con_ty) - - | otherwise - -- See Note [Instantiating stupid theta] - = do { let (tvs, theta, rho) = tcSplitSigmaTy con_ty - ; (subst, tvs') <- newMetaTyVars tvs - ; let tys' = mkTyVarTys tvs' - theta' = substTheta subst theta - rho' = substTy subst rho - ; wrap <- instCall (OccurrenceOf id_name) tys' theta' - ; addDataConStupidTheta con tys' - ; return ( mkHsWrap wrap (HsConLikeOut noExtField (RealDataCon con)) - , rho') } - - where - con_ty = dataConUserType con - stupid_theta = dataConStupidTheta con + = do { let tvs = dataConUserTyVarBinders con + theta = dataConOtherTheta con + args = dataConOrigArgTys con + res = dataConOrigResTy con + + -- See Note [Linear fields generalization] + ; mul_vars <- newFlexiTyVarTys (length args) multiplicityTy + ; let scaleArgs args' = zipWithEqual "return_data_con" combine mul_vars args' + combine var (Scaled One ty) = Scaled var ty + combine _ scaled_ty = scaled_ty + -- The combine function implements the fact that, as + -- described in Note [Linear fields generalization], if a + -- field is not linear (last line) it isn't made polymorphic. + + etaWrapper arg_tys = foldr (\scaled_ty wr -> WpFun WpHole wr scaled_ty empty) WpHole arg_tys + + -- See Note [Instantiating stupid theta] + ; let shouldInstantiate = (not (null (dataConStupidTheta con)) || + isKindLevPoly (tyConResKind (dataConTyCon con))) + ; case shouldInstantiate of + True -> do { (subst, tvs') <- newMetaTyVars (binderVars tvs) + ; let tys' = mkTyVarTys tvs' + theta' = substTheta subst theta + args' = substScaledTys subst args + res' = substTy subst res + ; wrap <- instCall (OccurrenceOf id_name) tys' theta' + ; let scaled_arg_tys = scaleArgs args' + eta_wrap = etaWrapper scaled_arg_tys + ; addDataConStupidTheta con tys' + ; return ( mkHsWrap (eta_wrap <.> wrap) + (HsConLikeOut noExtField (RealDataCon con)) + , mkVisFunTys scaled_arg_tys res') + } + False -> let scaled_arg_tys = scaleArgs args + wrap1 = mkWpTyApps (mkTyVarTys $ binderVars tvs) + eta_wrap = etaWrapper (map unrestricted theta ++ scaled_arg_tys) + wrap2 = mkWpTyLams $ binderVars tvs + in return ( mkHsWrap (wrap2 <.> eta_wrap <.> wrap1) + (HsConLikeOut noExtField (RealDataCon con)) + , mkInvisForAllTys tvs $ mkInvisFunTysMany theta $ mkVisFunTys scaled_arg_tys res) + } check_naughty id | isNaughtyRecordSelector id = failWithTc (naughtyRecordSel lbl) @@ -1918,7 +1995,7 @@ tcUnboundId :: HsExpr GhcRn -> OccName -> ExpRhoType -> TcM (HsExpr GhcTc) tcUnboundId rn_expr occ res_ty = do { ty <- newOpenFlexiTyVarTy -- Allow Int# etc (#12531) ; name <- newSysName occ - ; let ev = mkLocalId name ty + ; let ev = mkLocalId name Many ty ; emitNewExprHole occ ev ty ; tcWrapResultO (UnboundOccurrenceOf occ) rn_expr (HsVar noExtField (noLoc ev)) ty res_ty } @@ -1972,6 +2049,42 @@ in this case. Thus, users cannot use visible type application with a data constructor sporting a stupid theta. I won't feel so bad for the users that complain. +Note [Linear fields generalization] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +As per Note [Polymorphisation of linear fields], linear field of data +constructors get a polymorphic type when the data constructor is used as a term. + + Just :: forall {p} a. a #p-> Maybe a + +This rule is known only to the typechecker: Just keeps its linear type in Core. + +In order to desugar this generalised typing rule, we simply eta-expand: + + \a (x # p :: a) -> Just @a x + +has the appropriate type. We insert these eta-expansion with WpFun wrappers. + +A small hitch: if the constructor is levity-polymorphic (unboxed tuples, sums, +certain newtypes with -XUnliftedNewtypes) then this strategy produces + + \r1 r2 a b (x # p :: a) (y # q :: b) -> (# a, b #) + +Which has type + + forall r1 r2 a b. a #p-> b #q-> (# a, b #) + +Which violates the levity-polymorphism restriction see Note [Levity polymorphism +checking] in DsMonad. + +So we really must instantiate r1 and r2 rather than quantify over them. For +simplicity, we just instantiate the entire type, as described in Note +[Instantiating stupid theta]. It breaks visible type application with unboxed +tuples, sums and levity-polymorphic newtypes, but this doesn't appear to be used +anywhere. + +A better plan: let's force all representation variable to be *inferred*, so that +they are not subject to visible type applications. Then we can instantiate +inferred argument eagerly. -} isTagToEnum :: HsExpr GhcTc -> Bool @@ -2149,7 +2262,7 @@ getFixedTyVars upd_fld_occs univ_tvs cons ++ prov_theta ++ req_theta flds = conLikeFieldLabels con - fixed_tvs = exactTyCoVarsOfTypes fixed_tys + fixed_tvs = exactTyCoVarsOfTypes (map scaledThing fixed_tys) -- fixed_tys: See Note [Type of a record update] `unionVarSet` tyCoVarsOfTypes theta -- Universally-quantified tyvars that @@ -2497,7 +2610,7 @@ tcRecordField con_like flds_w_tys (L loc (FieldOcc sel_name lbl)) rhs do { rhs' <- tcCheckPolyExprNC rhs field_ty ; let field_id = mkUserLocal (nameOccName sel_name) (nameUnique sel_name) - field_ty loc + Many field_ty loc -- Yuk: the field_id has the *unique* of the selector Id -- (so we can find it easily) -- but is a LocalId with the appropriate type of the RHS diff --git a/compiler/GHC/Tc/Gen/Expr.hs-boot b/compiler/GHC/Tc/Gen/Expr.hs-boot index 1f26ef242a..f4b12e28a5 100644 --- a/compiler/GHC/Tc/Gen/Expr.hs-boot +++ b/compiler/GHC/Tc/Gen/Expr.hs-boot @@ -4,6 +4,7 @@ import GHC.Hs ( HsExpr, LHsExpr, SyntaxExprRn, SyntaxExprTc ) import GHC.Tc.Utils.TcType ( TcRhoType, TcSigmaType, SyntaxOpType, ExpType, ExpRhoType ) import GHC.Tc.Types ( TcM ) import GHC.Tc.Types.Origin ( CtOrigin ) +import GHC.Core.Type ( Mult ) import GHC.Hs.Extension ( GhcRn, GhcTcId ) tcCheckPolyExpr :: @@ -31,14 +32,14 @@ tcSyntaxOp :: CtOrigin -> SyntaxExprRn -> [SyntaxOpType] -- ^ shape of syntax operator arguments -> ExpType -- ^ overall result type - -> ([TcSigmaType] -> TcM a) -- ^ Type check any arguments + -> ([TcSigmaType] -> [Mult] -> TcM a) -- ^ Type check any arguments -> TcM (a, SyntaxExprTc) tcSyntaxOpGen :: CtOrigin -> SyntaxExprRn -> [SyntaxOpType] -> SyntaxOpType - -> ([TcSigmaType] -> TcM a) + -> ([TcSigmaType] -> [Mult] -> TcM a) -> TcM (a, SyntaxExprTc) diff --git a/compiler/GHC/Tc/Gen/Foreign.hs b/compiler/GHC/Tc/Gen/Foreign.hs index 06febcef33..97757c0889 100644 --- a/compiler/GHC/Tc/Gen/Foreign.hs +++ b/compiler/GHC/Tc/Gen/Foreign.hs @@ -46,6 +46,7 @@ import GHC.Tc.Instance.Family import GHC.Core.FamInstEnv import GHC.Core.Coercion import GHC.Core.Type +import GHC.Core.Multiplicity import GHC.Types.ForeignCall import GHC.Utils.Error import GHC.Types.Id @@ -93,20 +94,6 @@ parameters. Similarly, we don't need to look in AppTy's, because nothing headed by an AppTy will be marshalable. - -Note [FFI type roles] -~~~~~~~~~~~~~~~~~~~~~ -The 'go' helper function within normaliseFfiType' always produces -representational coercions. But, in the "children_only" case, we need to -use these coercions in a TyConAppCo. Accordingly, the roles on the coercions -must be twiddled to match the expectation of the enclosing TyCon. However, -we cannot easily go from an R coercion to an N one, so we forbid N roles -on FFI type constructors. Currently, only two such type constructors exist: -IO and FunPtr. Thus, this is not an onerous burden. - -If we ever want to lift this restriction, we would need to make 'go' take -the target role as a parameter. This wouldn't be hard, but it's a complication -not yet necessary and so is not yet implemented. -} -- normaliseFfiType takes the type from an FFI declaration, and @@ -120,33 +107,31 @@ normaliseFfiType ty normaliseFfiType' fam_envs ty normaliseFfiType' :: FamInstEnvs -> Type -> TcM (Coercion, Type, Bag GlobalRdrElt) -normaliseFfiType' env ty0 = go initRecTc ty0 +normaliseFfiType' env ty0 = go Representational initRecTc ty0 where - go :: RecTcChecker -> Type -> TcM (Coercion, Type, Bag GlobalRdrElt) - go rec_nts ty + go :: Role -> RecTcChecker -> Type -> TcM (Coercion, Type, Bag GlobalRdrElt) + go role rec_nts ty | Just ty' <- tcView ty -- Expand synonyms - = go rec_nts ty' + = go role rec_nts ty' | Just (tc, tys) <- splitTyConApp_maybe ty - = go_tc_app rec_nts tc tys + = go_tc_app role rec_nts tc tys | (bndrs, inner_ty) <- splitForAllVarBndrs ty , not (null bndrs) - = do (coi, nty1, gres1) <- go rec_nts inner_ty + = do (coi, nty1, gres1) <- go role rec_nts inner_ty return ( mkHomoForAllCos (binderVars bndrs) coi , mkForAllTys bndrs nty1, gres1 ) | otherwise -- see Note [Don't recur in normaliseFfiType'] - = return (mkRepReflCo ty, ty, emptyBag) + = return (mkReflCo role ty, ty, emptyBag) - go_tc_app :: RecTcChecker -> TyCon -> [Type] + go_tc_app :: Role -> RecTcChecker -> TyCon -> [Type] -> TcM (Coercion, Type, Bag GlobalRdrElt) - go_tc_app rec_nts tc tys + go_tc_app role rec_nts tc tys -- We don't want to look through the IO newtype, even if it is -- in scope, so we have a special case for it: | tc_key `elem` [ioTyConKey, funPtrTyConKey, funTyConKey] - -- These *must not* have nominal roles on their parameters! - -- See Note [FFI type roles] = children_only | isNewTyCon tc -- Expand newtypes @@ -160,13 +145,13 @@ normaliseFfiType' env ty0 = go initRecTc ty0 = do { rdr_env <- getGlobalRdrEnv ; case checkNewtypeFFI rdr_env tc of Nothing -> nothing - Just gre -> do { (co', ty', gres) <- go rec_nts' nt_rhs + Just gre -> do { (co', ty', gres) <- go role rec_nts' nt_rhs ; return (mkTransCo nt_co co', ty', gre `consBag` gres) } } | isFamilyTyCon tc -- Expand open tycons - , (co, ty) <- normaliseTcApp env Representational tc tys + , (co, ty) <- normaliseTcApp env role tc tys , not (isReflexiveCo co) - = do (co', ty', gres) <- go rec_nts ty + = do (co', ty', gres) <- go role rec_nts ty return (mkTransCo co co', ty', gres) | otherwise @@ -174,19 +159,15 @@ normaliseFfiType' env ty0 = go initRecTc ty0 where tc_key = getUnique tc children_only - = do xs <- mapM (go rec_nts) tys + = do xs <- zipWithM (\ty r -> go r rec_nts ty) tys (tyConRolesX role tc) let (cos, tys', gres) = unzip3 xs - -- the (repeat Representational) is because 'go' always - -- returns R coercions - cos' = zipWith3 downgradeRole (tyConRoles tc) - (repeat Representational) cos - return ( mkTyConAppCo Representational tc cos' + return ( mkTyConAppCo role tc cos , mkTyConApp tc tys', unionManyBags gres) - nt_co = mkUnbranchedAxInstCo Representational (newTyConCo tc) tys [] + nt_co = mkUnbranchedAxInstCo role (newTyConCo tc) tys [] nt_rhs = newTyConInstRhs tc tys ty = mkTyConApp tc tys - nothing = return (mkRepReflCo ty, ty, emptyBag) + nothing = return (mkReflCo role ty, ty, emptyBag) checkNewtypeFFI :: GlobalRdrEnv -> TyCon -> Maybe GlobalRdrElt checkNewtypeFFI rdr_env tc @@ -251,12 +232,12 @@ tcFImport (L dloc fo@(ForeignImport { fd_name = L nloc nm, fd_sig_ty = hs_ty -- Drop the foralls before inspecting the -- structure of the foreign type. (arg_tys, res_ty) = tcSplitFunTys (dropForAlls norm_sig_ty) - id = mkLocalId nm sig_ty + id = mkLocalId nm Many sig_ty -- Use a LocalId to obey the invariant that locally-defined -- things are LocalIds. However, it does not need zonking, -- (so GHC.Tc.Utils.Zonk.zonkForeignExports ignores it). - ; imp_decl' <- tcCheckFIType arg_tys res_ty imp_decl + ; imp_decl' <- tcCheckFIType (map scaledThing arg_tys) res_ty imp_decl -- Can't use sig_ty here because sig_ty :: Type and -- we need HsType Id hence the undefined ; let fi_decl = ForeignImport { fd_name = L nloc id @@ -275,7 +256,7 @@ tcCheckFIType arg_tys res_ty (CImport (L lc cconv) safety mh l@(CLabel _) src) = do checkCg checkCOrAsmOrLlvmOrInterp -- NB check res_ty not sig_ty! -- In case sig_ty is (forall a. ForeignPtr a) - check (isFFILabelTy (mkVisFunTys arg_tys res_ty)) (illegalForeignTyErr Outputable.empty) + check (isFFILabelTy (mkVisFunTysMany arg_tys res_ty)) (illegalForeignTyErr Outputable.empty) cconv' <- checkCConv cconv return (CImport (L lc cconv') safety mh l src) @@ -287,7 +268,7 @@ tcCheckFIType arg_tys res_ty (CImport (L lc cconv) safety mh CWrapper src) = do checkCg checkCOrAsmOrLlvmOrInterp cconv' <- checkCConv cconv case arg_tys of - [arg1_ty] -> do checkForeignArgs isFFIExternalTy arg1_tys + [arg1_ty] -> do checkForeignArgs isFFIExternalTy (map scaledThing arg1_tys) checkForeignRes nonIOok checkSafe isFFIExportResultTy res1_ty checkForeignRes mustBeIO checkSafe (isFFIDynTy arg1_ty) res_ty where @@ -305,7 +286,7 @@ tcCheckFIType arg_tys res_ty idecl@(CImport (L lc cconv) (L ls safety) mh addErrTc (illegalForeignTyErr Outputable.empty (text "At least one argument expected")) (arg1_ty:arg_tys) -> do dflags <- getDynFlags - let curried_res_ty = mkVisFunTys arg_tys res_ty + let curried_res_ty = mkVisFunTysMany arg_tys res_ty check (isFFIDynTy curried_res_ty arg1_ty) (illegalForeignTyErr argument) checkForeignArgs (isFFIArgumentTy dflags safety) arg_tys @@ -418,7 +399,7 @@ tcCheckFEType sig_ty (CExport (L l (CExportStatic esrc str cconv)) src) = do checkCg checkCOrAsmOrLlvm checkTc (isCLabelString str) (badCName str) cconv' <- checkCConv cconv - checkForeignArgs isFFIExternalTy arg_tys + checkForeignArgs isFFIExternalTy (map scaledThing arg_tys) checkForeignRes nonIOok noCheckSafe isFFIExportResultTy res_ty return (CExport (L l (CExportStatic esrc str cconv')) src) where diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index b99cc6365b..fecd8b9b2e 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -57,6 +57,9 @@ module GHC.Tc.Gen.HsType ( tcLHsKindSig, checkDataKindSig, DataSort(..), checkClassKindSig, + -- Multiplicity + tcMult, + -- Pattern type signatures tcHsPatSigType, @@ -85,6 +88,7 @@ import GHC.Core.TyCo.Ppr import GHC.Tc.Errors ( reportAllUnsolved ) import GHC.Tc.Utils.TcType import GHC.Tc.Utils.Instantiate ( tcInstInvisibleTyBinders, tcInstInvisibleTyBinder ) +import GHC.Core.Multiplicity import GHC.Core.Type import GHC.Builtin.Types.Prim import GHC.Types.Name.Reader( lookupLocalRdrOcc ) @@ -469,7 +473,7 @@ tcHsDeriv hs_ty ; let (tvs, pred) = splitForAllTys ty (kind_args, _) = splitFunTys (tcTypeKind pred) ; case getClassPredTys_maybe pred of - Just (cls, tys) -> return (tvs, cls, tys, kind_args) + Just (cls, tys) -> return (tvs, cls, tys, map scaledThing kind_args) Nothing -> failWithTc (text "Illegal deriving item" <+> quotes (ppr hs_ty)) } -- | Typecheck a deriving strategy. For most deriving strategies, this is a @@ -684,6 +688,9 @@ concern things that the renamer can't handle. -} +tcMult :: HsArrow GhcRn -> TcM Mult +tcMult hc = tc_mult (mkMode TypeLevel) hc + -- | Info about the context in which we're checking a type. Currently, -- differentiates only between types and kinds, but this will likely -- grow, at least to include the distinction between patterns and @@ -888,12 +895,15 @@ tc_hs_type _ ty@(HsSpliceTy {}) _exp_kind = failWithTc (text "Unexpected type splice:" <+> ppr ty) ---------- Functions and applications -tc_hs_type mode (HsFunTy _ ty1 ty2) exp_kind - = tc_fun_type mode ty1 ty2 exp_kind +tc_hs_type mode ty@(HsFunTy _ mult ty1 ty2) exp_kind + | mode_tyki mode == KindLevel && not (isUnrestricted mult) + = failWithTc (text "Linear arrows disallowed in kinds:" <+> ppr ty) + | otherwise + = tc_fun_type mode mult ty1 ty2 exp_kind tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind | op `hasKey` funTyConKey - = tc_fun_type mode ty1 ty2 exp_kind + = tc_fun_type mode HsUnrestrictedArrow ty1 ty2 exp_kind --------- Foralls tc_hs_type mode forall@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind @@ -1084,20 +1094,25 @@ Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in "GHC.Core.TyCo. -} ------------------------------------------ -tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind +tc_mult :: TcTyMode -> HsArrow GhcRn -> TcM Mult +tc_mult mode ty = tc_lhs_type mode (arrowToHsType ty) multiplicityTy +------------------------------------------ +tc_fun_type :: TcTyMode -> HsArrow GhcRn -> LHsType GhcRn -> LHsType GhcRn -> TcKind -> TcM TcType -tc_fun_type mode ty1 ty2 exp_kind = case mode_tyki mode of +tc_fun_type mode mult ty1 ty2 exp_kind = case mode_tyki mode of TypeLevel -> do { arg_k <- newOpenTypeKind ; res_k <- newOpenTypeKind ; ty1' <- tc_lhs_type mode ty1 arg_k ; ty2' <- tc_lhs_type mode ty2 res_k - ; checkExpectedKind (HsFunTy noExtField ty1 ty2) (mkVisFunTy ty1' ty2') + ; mult' <- tc_mult mode mult + ; checkExpectedKind (HsFunTy noExtField mult ty1 ty2) (mkVisFunTy mult' ty1' ty2') liftedTypeKind exp_kind } KindLevel -> -- no representation polymorphism in kinds. yet. do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind - ; checkExpectedKind (HsFunTy noExtField ty1 ty2) (mkVisFunTy ty1' ty2') + ; mult' <- tc_mult mode mult + ; checkExpectedKind (HsFunTy noExtField mult ty1 ty2) (mkVisFunTy mult' ty1' ty2') liftedTypeKind exp_kind } {- Note [Skolem escape and forall-types] @@ -2128,7 +2143,7 @@ kcCheckDeclHeader_cusk name flav ++ mkNamedTyConBinders Specified specified ++ map (mkRequiredTyConBinder mentioned_kv_set) tc_tvs - all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs) + all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs) tycon = mkTcTyCon name final_tc_binders res_kind all_tv_prs True -- it is generalised flav @@ -2363,7 +2378,7 @@ kcCheckDeclHeader_sig kisig name flav -- Example: (a~b) => ZippedBinder (Anon InvisArg bndr_ki) Nothing -> do name <- newSysName (mkTyVarOccFS (fsLit "ev")) - let tv = mkTyVar name bndr_ki + let tv = mkTyVar name (scaledThing bndr_ki) return (mkAnonTyConBinder InvisArg tv, []) -- Non-dependent visible argument with a user-written binder. @@ -2371,7 +2386,7 @@ kcCheckDeclHeader_sig kisig name flav ZippedBinder (Anon VisArg bndr_ki) (Just b) -> return $ let v_name = getName b - tv = mkTyVar v_name bndr_ki + tv = mkTyVar v_name (scaledThing bndr_ki) tcb = mkAnonTyConBinder VisArg tv in (tcb, [(v_name, tv)]) @@ -3181,7 +3196,7 @@ etaExpandAlgTyCon tc_bndrs kind Just (Anon af arg, kind') -> go loc occs' uniqs' subst' (tcb : acc) kind' where - arg' = substTy subst arg + arg' = substTy subst (scaledThing arg) tv = mkTyVar (mkInternalName uniq occ loc) arg' subst' = extendTCvInScope subst tv tcb = Bndr tv (AnonTCB af) diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs index b95899cc1f..0bff299886 100644 --- a/compiler/GHC/Tc/Gen/Match.hs +++ b/compiler/GHC/Tc/Gen/Match.hs @@ -51,6 +51,8 @@ import GHC.Tc.Utils.TcType import GHC.Tc.Gen.Bind import GHC.Tc.Utils.Unify import GHC.Tc.Types.Origin +import GHC.Core.Multiplicity +import GHC.Core.UsageEnv import GHC.Types.Name import GHC.Builtin.Types import GHC.Types.Id @@ -100,6 +102,13 @@ tcMatchesFun fn@(L _ fun_name) matches exp_ty ; matchExpectedFunTys herald ctxt arity exp_ty $ \ pat_tys rhs_ty -> -- NB: exp_type may be polymorphic, but -- matchExpectedFunTys can cope with that + tcScalingUsage Many $ + -- toplevel bindings and let bindings are, at the + -- moment, always unrestricted. The value being bound + -- must, accordingly, be unrestricted. Hence them + -- being scaled by Many. When let binders come with a + -- multiplicity, then @tcMatchesFun@ will have to take + -- a multiplicity argument, and scale accordingly. tcMatches match_ctxt pat_tys rhs_ty matches } where arity = matchGroupArity matches @@ -122,16 +131,16 @@ parser guarantees that each equation has exactly one argument. -} tcMatchesCase :: (Outputable (body GhcRn)) => - TcMatchCtxt body -- Case context - -> TcSigmaType -- Type of scrutinee - -> MatchGroup GhcRn (Located (body GhcRn)) -- The case alternatives - -> ExpRhoType -- Type of whole case expressions - -> TcM (MatchGroup GhcTcId (Located (body GhcTcId))) - -- Translated alternatives - -- wrapper goes from MatchGroup's ty to expected ty + TcMatchCtxt body -- Case context + -> Scaled TcSigmaType -- Type of scrutinee + -> MatchGroup GhcRn (Located (body GhcRn)) -- The case alternatives + -> ExpRhoType -- Type of whole case expressions + -> TcM (MatchGroup GhcTcId (Located (body GhcTcId))) + -- Translated alternatives + -- wrapper goes from MatchGroup's ty to expected ty -tcMatchesCase ctxt scrut_ty matches res_ty - = tcMatches ctxt [mkCheckExpType scrut_ty] res_ty matches +tcMatchesCase ctxt (Scaled scrut_mult scrut_ty) matches res_ty + = tcMatches ctxt [Scaled scrut_mult (mkCheckExpType scrut_ty)] res_ty matches tcMatchLambda :: SDoc -- see Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify -> TcMatchCtxt HsExpr @@ -197,15 +206,16 @@ still gets assigned a polytype. -- expected type into TauTvs. -- See Note [Case branches must never infer a non-tau type] tauifyMultipleMatches :: [LMatch id body] - -> [ExpType] -> TcM [ExpType] + -> [Scaled ExpType] -> TcM [Scaled ExpType] tauifyMultipleMatches group exp_tys | isSingletonMatchGroup group = return exp_tys - | otherwise = mapM tauifyExpType exp_tys + | otherwise = mapM (\(Scaled m t) -> + fmap (Scaled m) (tauifyExpType t)) exp_tys -- NB: In the empty-match case, this ensures we fill in the ExpType -- | Type-check a MatchGroup. tcMatches :: (Outputable (body GhcRn)) => TcMatchCtxt body - -> [ExpSigmaType] -- Expected pattern types + -> [Scaled ExpSigmaType] -- Expected pattern types -> ExpRhoType -- Expected result-type of the Match. -> MatchGroup GhcRn (Located (body GhcRn)) -> TcM (MatchGroup GhcTcId (Located (body GhcTcId))) @@ -216,14 +226,15 @@ data TcMatchCtxt body -- c.f. TcStmtCtxt, also in this module -- an alternative -> ExpRhoType -> TcM (Located (body GhcTcId)) } - tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches , mg_origin = origin }) - = do { rhs_ty:pat_tys <- tauifyMultipleMatches matches (rhs_ty:pat_tys) + = do { (Scaled _ rhs_ty):pat_tys <- tauifyMultipleMatches matches ((Scaled One rhs_ty):pat_tys) -- return type has implicitly multiplicity 1, it doesn't matter all that much in this case since it isn't used and is eliminated immediately. -- See Note [Case branches must never infer a non-tau type] - ; matches' <- mapM (tcMatch ctxt pat_tys rhs_ty) matches - ; pat_tys <- mapM readExpType pat_tys + ; umatches <- mapM (tcCollectingUsage . tcMatch ctxt pat_tys rhs_ty) matches + ; let (usages,matches') = unzip umatches + ; tcEmitBindingUsage $ supUEs usages + ; pat_tys <- mapM (\(Scaled m t) -> fmap (Scaled m) (readExpType t)) pat_tys ; rhs_ty <- readExpType rhs_ty ; return (MG { mg_alts = L l matches' , mg_ext = MatchGroupTc pat_tys rhs_ty @@ -231,7 +242,7 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches ------------- tcMatch :: (Outputable (body GhcRn)) => TcMatchCtxt body - -> [ExpSigmaType] -- Expected pattern types + -> [Scaled ExpSigmaType] -- Expected pattern types -> ExpRhoType -- Expected result-type of the Match. -> LMatch GhcRn (Located (body GhcRn)) -> TcM (LMatch GhcTcId (Located (body GhcTcId))) @@ -266,10 +277,11 @@ tcGRHSs :: TcMatchCtxt body -> GRHSs GhcRn (Located (body GhcRn)) -> ExpRhoType -- but we don't need to do that any more tcGRHSs ctxt (GRHSs _ grhss (L l binds)) res_ty - = do { (binds', grhss') + = do { (binds', ugrhss) <- tcLocalBinds binds $ - mapM (wrapLocM (tcGRHS ctxt res_ty)) grhss - + mapM (tcCollectingUsage . wrapLocM (tcGRHS ctxt res_ty)) grhss + ; let (usages, grhss') = unzip ugrhss + ; tcEmitBindingUsage $ supUEs usages ; return (GRHSs noExtField grhss' (L l binds')) } ------------- @@ -412,7 +424,7 @@ tcGuardStmt ctxt (BindStmt _ pat rhs) res_ty thing_inside = do { (rhs', rhs_ty) <- tcInferRhoNC rhs -- Stmt has a context already ; (pat', thing) <- tcCheckPat_O (StmtCtxt ctxt) (lexprCtOrigin rhs) - pat rhs_ty $ + pat (unrestricted rhs_ty) $ thing_inside res_ty ; return (mkTcBindStmt pat' rhs', thing) } @@ -445,7 +457,7 @@ tcLcStmt _ _ (LastStmt x body noret _) elt_ty thing_inside tcLcStmt m_tc ctxt (BindStmt _ pat rhs) elt_ty thing_inside = do { pat_ty <- newFlexiTyVarTy liftedTypeKind ; rhs' <- tcCheckMonoExpr rhs (mkTyConApp m_tc [pat_ty]) - ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $ + ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat (unrestricted pat_ty) $ thing_inside elt_ty ; return (mkTcBindStmt pat' rhs', thing) } @@ -500,14 +512,14 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts by_arrow :: Type -> Type -- Wraps 'ty' to '(a->t) -> ty' if the By is present by_arrow = case by' of Nothing -> \ty -> ty - Just (_,e_ty) -> \ty -> (alphaTy `mkVisFunTy` e_ty) `mkVisFunTy` ty + Just (_,e_ty) -> \ty -> (alphaTy `mkVisFunTyMany` e_ty) `mkVisFunTyMany` ty tup_ty = mkBigCoreVarTupTy bndr_ids poly_arg_ty = m_app alphaTy poly_res_ty = m_app (n_app alphaTy) using_poly_ty = mkInfForAllTy alphaTyVar $ by_arrow $ - poly_arg_ty `mkVisFunTy` poly_res_ty + poly_arg_ty `mkVisFunTyMany` poly_res_ty ; using' <- tcCheckPolyExpr using using_poly_ty ; let final_using = fmap (mkHsWrap (WpTyApp tup_ty)) using' @@ -516,7 +528,7 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts -- typically something like [(Int,Bool,Int)] -- We don't know what tuple_ty is yet, so we use a variable ; let mk_n_bndr :: Name -> TcId -> TcId - mk_n_bndr n_bndr_name bndr_id = mkLocalId n_bndr_name (n_app (idType bndr_id)) + mk_n_bndr n_bndr_name bndr_id = mkLocalId n_bndr_name Many (n_app (idType bndr_id)) -- Ensure that every old binder of type `b` is linked up with its -- new binder which should have type `n b` @@ -550,8 +562,8 @@ tcMcStmt :: TcExprStmtChecker tcMcStmt _ (LastStmt x body noret return_op) res_ty thing_inside = do { (body', return_op') <- tcSyntaxOp MCompOrigin return_op [SynRho] res_ty $ - \ [a_ty] -> - tcCheckMonoExprNC body a_ty + \ [a_ty] [mult]-> + tcScalingUsage mult $ tcCheckMonoExprNC body a_ty ; thing <- thing_inside (panic "tcMcStmt: thing_inside") ; return (LastStmt x body' noret return_op', thing) } @@ -563,14 +575,14 @@ tcMcStmt _ (LastStmt x body noret return_op) res_ty thing_inside tcMcStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside -- (>>=) :: rhs_ty -> (pat_ty -> new_res_ty) -> res_ty - = do { ((rhs', pat', thing, new_res_ty), bind_op') + = do { ((rhs', pat_mult, pat', thing, new_res_ty), bind_op') <- tcSyntaxOp MCompOrigin (xbsrn_bindOp xbsrn) [SynRho, SynFun SynAny SynRho] res_ty $ - \ [rhs_ty, pat_ty, new_res_ty] -> - do { rhs' <- tcCheckMonoExprNC rhs rhs_ty - ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $ + \ [rhs_ty, pat_ty, new_res_ty] [rhs_mult, fun_mult, pat_mult] -> + do { rhs' <- tcScalingUsage rhs_mult $ tcCheckMonoExprNC rhs rhs_ty + ; (pat', thing) <- tcScalingUsage fun_mult $ tcCheckPat (StmtCtxt ctxt) pat (Scaled pat_mult pat_ty) $ thing_inside (mkCheckExpType new_res_ty) - ; return (rhs', pat', thing, new_res_ty) } + ; return (rhs', pat_mult, pat', thing, new_res_ty) } -- If (but only if) the pattern can fail, typecheck the 'fail' operator ; fail_op' <- fmap join . forM (xbsrn_failOp xbsrn) $ \fail -> @@ -579,6 +591,7 @@ tcMcStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside ; let xbstc = XBindStmtTc { xbstc_bindOp = bind_op' , xbstc_boundResultType = new_res_ty + , xbstc_boundResultMult = pat_mult , xbstc_failOp = fail_op' } ; return (BindStmt xbstc pat' rhs', thing) } @@ -594,13 +607,14 @@ tcMcStmt _ (BodyStmt _ rhs then_op guard_op) res_ty thing_inside -- Where test_ty is, for example, Bool ; ((thing, rhs', rhs_ty, guard_op'), then_op') <- tcSyntaxOp MCompOrigin then_op [SynRho, SynRho] res_ty $ - \ [rhs_ty, new_res_ty] -> + \ [rhs_ty, new_res_ty] [rhs_mult, fun_mult] -> do { (rhs', guard_op') - <- tcSyntaxOp MCompOrigin guard_op [SynAny] + <- tcScalingUsage rhs_mult $ + tcSyntaxOp MCompOrigin guard_op [SynAny] (mkCheckExpType rhs_ty) $ - \ [test_ty] -> - tcCheckMonoExpr rhs test_ty - ; thing <- thing_inside (mkCheckExpType new_res_ty) + \ [test_ty] [test_mult] -> + tcScalingUsage test_mult $ tcCheckMonoExpr rhs test_ty + ; thing <- tcScalingUsage fun_mult $ thing_inside (mkCheckExpType new_res_ty) ; return (thing, rhs', rhs_ty, guard_op') } ; return (BodyStmt rhs_ty rhs' then_op' guard_op', thing) } @@ -640,7 +654,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap -- or res ('by' absent) by_arrow = case by of Nothing -> \res -> res - Just {} -> \res -> (alphaTy `mkVisFunTy` by_e_ty) `mkVisFunTy` res + Just {} -> \res -> (alphaTy `mkVisFunTyMany` by_e_ty) `mkVisFunTyMany` res poly_arg_ty = m1_ty `mkAppTy` alphaTy using_arg_ty = m1_ty `mkAppTy` tup_ty @@ -648,7 +662,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap using_res_ty = m2_ty `mkAppTy` n_app tup_ty using_poly_ty = mkInfForAllTy alphaTyVar $ by_arrow $ - poly_arg_ty `mkVisFunTy` poly_res_ty + poly_arg_ty `mkVisFunTyMany` poly_res_ty -- 'stmts' returns a result of type (m1_ty tuple_ty), -- typically something like [(Int,Bool,Int)] @@ -669,7 +683,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap -- return :: (a,b,c,..) -> m (a,b,c,..) ; (_, return_op') <- tcSyntaxOp MCompOrigin return_op [synKnownType (mkBigCoreVarTupTy bndr_ids)] - res_ty' $ \ _ -> return () + res_ty' $ \ _ _ -> return () ; return (bndr_ids, by', return_op') } @@ -678,8 +692,8 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap ; new_res_ty <- newFlexiTyVarTy liftedTypeKind ; (_, bind_op') <- tcSyntaxOp MCompOrigin bind_op [ synKnownType using_res_ty - , synKnownType (n_app tup_ty `mkVisFunTy` new_res_ty) ] - res_ty $ \ _ -> return () + , synKnownType (n_app tup_ty `mkVisFunTyMany` new_res_ty) ] + res_ty $ \ _ _ -> return () --------------- Typecheck the 'fmap' function ------------- ; fmap_op' <- case form of @@ -687,9 +701,9 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap _ -> fmap unLoc . tcCheckPolyExpr (noLoc fmap_op) $ mkInfForAllTy alphaTyVar $ mkInfForAllTy betaTyVar $ - (alphaTy `mkVisFunTy` betaTy) - `mkVisFunTy` (n_app alphaTy) - `mkVisFunTy` (n_app betaTy) + (alphaTy `mkVisFunTyMany` betaTy) + `mkVisFunTyMany` (n_app alphaTy) + `mkVisFunTyMany` (n_app betaTy) --------------- Typecheck the 'using' function ------------- -- using :: ((a,b,c)->t) -> m1 (a,b,c) -> m2 (n (a,b,c)) @@ -699,7 +713,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap --------------- Building the bindersMap ---------------- ; let mk_n_bndr :: Name -> TcId -> TcId - mk_n_bndr n_bndr_name bndr_id = mkLocalId n_bndr_name (n_app (idType bndr_id)) + mk_n_bndr n_bndr_name bndr_id = mkLocalId n_bndr_name Many (n_app (idType bndr_id)) -- Ensure that every old binder of type `b` is linked up with its -- new binder which should have type `n b` @@ -752,9 +766,9 @@ tcMcStmt ctxt (ParStmt _ bndr_stmts_s mzip_op bind_op) res_ty thing_inside ; let mzip_ty = mkInfForAllTys [alphaTyVar, betaTyVar] $ (m_ty `mkAppTy` alphaTy) - `mkVisFunTy` + `mkVisFunTyMany` (m_ty `mkAppTy` betaTy) - `mkVisFunTy` + `mkVisFunTyMany` (m_ty `mkAppTy` mkBoxedTupleTy [alphaTy, betaTy]) ; mzip_op' <- unLoc `fmap` tcCheckPolyExpr (noLoc mzip_op) mzip_ty @@ -770,7 +784,7 @@ tcMcStmt ctxt (ParStmt _ bndr_stmts_s mzip_op bind_op) res_ty thing_inside <- tcSyntaxOp MCompOrigin bind_op [ synKnownType (m_ty `mkAppTy` tuple_ty) , SynFun (synKnownType tuple_ty) SynRho ] res_ty $ - \ [inner_res_ty] -> + \ [inner_res_ty] _ -> do { stuff <- loop m_ty (mkCheckExpType inner_res_ty) tup_tys bndr_stmts_s ; return (stuff, inner_res_ty) } @@ -800,7 +814,7 @@ tcMcStmt ctxt (ParStmt _ bndr_stmts_s mzip_op bind_op) res_ty thing_inside ; (_, return_op') <- tcSyntaxOp MCompOrigin return_op [synKnownType tup_ty] m_tup_ty' $ - \ _ -> return () + \ _ _ -> return () ; (pairs', thing) <- loop m_ty inner_res_ty tup_tys_in pairs ; return (ids, return_op', pairs', thing) } ; return (ParStmtBlock x stmts' ids return_op' : pairs', thing) } @@ -824,17 +838,17 @@ tcDoStmt _ (LastStmt x body noret _) res_ty thing_inside tcDoStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside = do { -- Deal with rebindable syntax: - -- (>>=) :: rhs_ty -> (pat_ty -> new_res_ty) -> res_ty + -- (>>=) :: rhs_ty ->_rhs_mult (pat_ty ->_pat_mult new_res_ty) ->_fun_mult res_ty -- This level of generality is needed for using do-notation -- in full generality; see #1537 - ((rhs', pat', new_res_ty, thing), bind_op') + ((rhs', pat_mult, pat', new_res_ty, thing), bind_op') <- tcSyntaxOp DoOrigin (xbsrn_bindOp xbsrn) [SynRho, SynFun SynAny SynRho] res_ty $ - \ [rhs_ty, pat_ty, new_res_ty] -> - do { rhs' <- tcCheckMonoExprNC rhs rhs_ty - ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $ + \ [rhs_ty, pat_ty, new_res_ty] [rhs_mult,fun_mult,pat_mult] -> + do { rhs' <-tcScalingUsage rhs_mult $ tcCheckMonoExprNC rhs rhs_ty + ; (pat', thing) <- tcScalingUsage fun_mult $ tcCheckPat (StmtCtxt ctxt) pat (Scaled pat_mult pat_ty) $ thing_inside (mkCheckExpType new_res_ty) - ; return (rhs', pat', new_res_ty, thing) } + ; return (rhs', pat_mult, pat', new_res_ty, thing) } -- If (but only if) the pattern can fail, typecheck the 'fail' operator ; fail_op' <- fmap join . forM (xbsrn_failOp xbsrn) $ \fail -> @@ -842,6 +856,7 @@ tcDoStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside ; let xbstc = XBindStmtTc { xbstc_bindOp = bind_op' , xbstc_boundResultType = new_res_ty + , xbstc_boundResultMult = pat_mult , xbstc_failOp = fail_op' } ; return (BindStmt xbstc pat' rhs', thing) } @@ -854,7 +869,7 @@ tcDoStmt ctxt (ApplicativeStmt _ pairs mb_join) res_ty thing_inside Just join_op -> second Just <$> (tcSyntaxOp DoOrigin join_op [SynRho] res_ty $ - \ [rhs_ty] -> tc_app_stmts (mkCheckExpType rhs_ty)) + \ [rhs_ty] [rhs_mult] -> tcScalingUsage rhs_mult $ tc_app_stmts (mkCheckExpType rhs_ty)) ; return (ApplicativeStmt body_ty pairs' mb_join', thing) } @@ -863,9 +878,9 @@ tcDoStmt _ (BodyStmt _ rhs then_op _) res_ty thing_inside -- (>>) :: rhs_ty -> new_res_ty -> res_ty ; ((rhs', rhs_ty, thing), then_op') <- tcSyntaxOp DoOrigin then_op [SynRho, SynRho] res_ty $ - \ [rhs_ty, new_res_ty] -> - do { rhs' <- tcCheckMonoExprNC rhs rhs_ty - ; thing <- thing_inside (mkCheckExpType new_res_ty) + \ [rhs_ty, new_res_ty] [rhs_mult,fun_mult] -> + do { rhs' <- tcScalingUsage rhs_mult $ tcCheckMonoExprNC rhs rhs_ty + ; thing <- tcScalingUsage fun_mult $ thing_inside (mkCheckExpType new_res_ty) ; return (rhs', rhs_ty, thing) } ; return (BodyStmt rhs_ty rhs' then_op' noSyntaxExpr, thing) } @@ -875,7 +890,8 @@ tcDoStmt ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names res_ty thing_inside = do { let tup_names = rec_names ++ filterOut (`elem` rec_names) later_names ; tup_elt_tys <- newFlexiTyVarTys (length tup_names) liftedTypeKind - ; let tup_ids = zipWith mkLocalId tup_names tup_elt_tys + ; let tup_ids = zipWith (\n t -> mkLocalId n Many t) tup_names tup_elt_tys + -- Many because it's a recursive definition tup_ty = mkBigCoreTupTy tup_elt_tys ; tcExtendIdEnv tup_ids $ do @@ -888,21 +904,21 @@ tcDoStmt ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names -- be polymorphic) with those of "knot-tied" Ids ; (_, ret_op') <- tcSyntaxOp DoOrigin ret_op [synKnownType tup_ty] - inner_res_ty $ \_ -> return () + inner_res_ty $ \_ _ -> return () ; return (ret_op', tup_rets) } ; ((_, mfix_op'), mfix_res_ty) <- tcInfer $ \ exp_ty -> tcSyntaxOp DoOrigin mfix_op - [synKnownType (mkVisFunTy tup_ty stmts_ty)] exp_ty $ - \ _ -> return () + [synKnownType (mkVisFunTyMany tup_ty stmts_ty)] exp_ty $ + \ _ _ -> return () ; ((thing, new_res_ty), bind_op') <- tcSyntaxOp DoOrigin bind_op [ synKnownType mfix_res_ty - , synKnownType tup_ty `SynFun` SynRho ] + , SynFun (synKnownType tup_ty) SynRho ] res_ty $ - \ [new_res_ty] -> + \ [new_res_ty] _ -> do { thing <- thing_inside (mkCheckExpType new_res_ty) ; return (thing, new_res_ty) } @@ -949,7 +965,7 @@ tcMonadFailOp orig pat fail_op res_ty = return Nothing | otherwise = Just . snd <$> (tcSyntaxOp orig fail_op [synKnownType stringTy] - (mkCheckExpType res_ty) $ \_ -> return ()) + (mkCheckExpType res_ty) $ \_ _ -> return ()) {- Note [Treat rebindable syntax first] @@ -993,7 +1009,7 @@ tcApplicativeStmts ctxt pairs rhs_ty thing_inside ; ts <- replicateM (arity-1) $ newInferExpType ; exp_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind ; pat_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind - ; let fun_ty = mkVisFunTys pat_tys body_ty + ; let fun_ty = mkVisFunTysMany pat_tys body_ty -- NB. do the <$>,<*> operators first, we don't want type errors here -- i.e. goOps before goArgs @@ -1018,7 +1034,7 @@ tcApplicativeStmts ctxt pairs rhs_ty thing_inside = do { (_, op') <- tcSyntaxOp DoOrigin op [synKnownType t_left, synKnownType exp_ty] t_i $ - \ _ -> return () + \ _ _ -> return () ; t_i <- readExpType t_i ; ops' <- goOps t_i ops ; return (op' : ops') } @@ -1035,7 +1051,7 @@ tcApplicativeStmts ctxt pairs rhs_ty thing_inside = setSrcSpan (combineSrcSpans (getLoc pat) (getLoc rhs)) $ addErrCtxt (pprStmtInCtxt ctxt (mkRnBindStmt pat rhs)) $ do { rhs' <- tcCheckMonoExprNC rhs exp_ty - ; (pat', _) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $ + ; (pat', _) <- tcCheckPat (StmtCtxt ctxt) pat (unrestricted pat_ty) $ return () ; fail_op' <- fmap join . forM fail_op $ \fail -> tcMonadFailOp (DoPatOrigin pat) pat' fail body_ty @@ -1052,7 +1068,7 @@ tcApplicativeStmts ctxt pairs rhs_ty thing_inside tcStmtsAndThen ctxt tcDoStmt stmts (mkCheckExpType exp_ty) $ \res_ty -> do { ret' <- tcExpr ret res_ty - ; (pat', _) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $ + ; (pat', _) <- tcCheckPat (StmtCtxt ctxt) pat (unrestricted pat_ty) $ return () ; return (ret', pat') } diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs index 830f04a89d..9cbfce243a 100644 --- a/compiler/GHC/Tc/Gen/Pat.hs +++ b/compiler/GHC/Tc/Gen/Pat.hs @@ -41,6 +41,7 @@ import GHC.Types.Id import GHC.Types.Var import GHC.Types.Name import GHC.Types.Name.Reader +import GHC.Core.Multiplicity import GHC.Tc.Utils.Env import GHC.Tc.Utils.TcMType import GHC.Tc.Validity( arityErr ) @@ -77,7 +78,7 @@ import GHC.Data.List.SetOps ( getNth ) tcLetPat :: (Name -> Maybe TcId) -> LetBndrSpec - -> LPat GhcRn -> ExpSigmaType + -> LPat GhcRn -> Scaled ExpSigmaType -> TcM a -> TcM (LPat GhcTcId, a) tcLetPat sig_fn no_gen pat pat_ty thing_inside @@ -94,7 +95,7 @@ tcLetPat sig_fn no_gen pat pat_ty thing_inside ----------------- tcPats :: HsMatchContext GhcRn -> [LPat GhcRn] -- Patterns, - -> [ExpSigmaType] -- and their types + -> [Scaled ExpSigmaType] -- and their types -> TcM a -- and the checker for the body -> TcM ([LPat GhcTcId], a) @@ -119,12 +120,12 @@ tcInferPat :: HsMatchContext GhcRn -> LPat GhcRn -> TcM ((LPat GhcTcId, a), TcSigmaType) tcInferPat ctxt pat thing_inside = tcInfer $ \ exp_ty -> - tc_lpat exp_ty penv pat thing_inside + tc_lpat (unrestricted exp_ty) penv pat thing_inside where penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin } tcCheckPat :: HsMatchContext GhcRn - -> LPat GhcRn -> TcSigmaType + -> LPat GhcRn -> Scaled TcSigmaType -> TcM a -- Checker for body -> TcM (LPat GhcTcId, a) tcCheckPat ctxt = tcCheckPat_O ctxt PatOrigin @@ -132,11 +133,11 @@ tcCheckPat ctxt = tcCheckPat_O ctxt PatOrigin -- | A variant of 'tcPat' that takes a custom origin tcCheckPat_O :: HsMatchContext GhcRn -> CtOrigin -- ^ origin to use if the type needs inst'ing - -> LPat GhcRn -> TcSigmaType + -> LPat GhcRn -> Scaled TcSigmaType -> TcM a -- Checker for body -> TcM (LPat GhcTcId, a) -tcCheckPat_O ctxt orig pat pat_ty thing_inside - = tc_lpat (mkCheckExpType pat_ty) penv pat thing_inside +tcCheckPat_O ctxt orig pat (Scaled pat_mult pat_ty) thing_inside + = tc_lpat (Scaled pat_mult (mkCheckExpType pat_ty)) penv pat thing_inside where penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig } @@ -198,7 +199,7 @@ inPatBind (PE { pe_ctxt = LamPat {} }) = False * * ********************************************************************* -} -tcPatBndr :: PatEnv -> Name -> ExpSigmaType -> TcM (HsWrapper, TcId) +tcPatBndr :: PatEnv -> Name -> Scaled ExpSigmaType -> TcM (HsWrapper, TcId) -- (coi, xp) = tcPatBndr penv x pat_ty -- Then coi : pat_ty ~ typeof(xp) -- @@ -210,34 +211,36 @@ tcPatBndr penv@(PE { pe_ctxt = LetPat { pc_lvl = bind_lvl -- Note [Typechecking pattern bindings] in GHC.Tc.Gen.Bind | Just bndr_id <- sig_fn bndr_name -- There is a signature - = do { wrap <- tc_sub_type penv exp_pat_ty (idType bndr_id) + = do { wrap <- tc_sub_type penv (scaledThing exp_pat_ty) (idType bndr_id) -- See Note [Subsumption check at pattern variables] ; traceTc "tcPatBndr(sig)" (ppr bndr_id $$ ppr (idType bndr_id) $$ ppr exp_pat_ty) ; return (wrap, bndr_id) } | otherwise -- No signature - = do { (co, bndr_ty) <- case exp_pat_ty of + = do { (co, bndr_ty) <- case scaledThing exp_pat_ty of Check pat_ty -> promoteTcType bind_lvl pat_ty Infer infer_res -> ASSERT( bind_lvl == ir_lvl infer_res ) -- If we were under a constructor that bumped -- the level, we'd be in checking mode do { bndr_ty <- inferResultToType infer_res ; return (mkTcNomReflCo bndr_ty, bndr_ty) } - ; bndr_id <- newLetBndr no_gen bndr_name bndr_ty + ; let bndr_mult = scaledMult exp_pat_ty + ; bndr_id <- newLetBndr no_gen bndr_name bndr_mult bndr_ty ; traceTc "tcPatBndr(nosig)" (vcat [ ppr bind_lvl , ppr exp_pat_ty, ppr bndr_ty, ppr co , ppr bndr_id ]) ; return (mkWpCastN co, bndr_id) } tcPatBndr _ bndr_name pat_ty - = do { pat_ty <- expTypeToType pat_ty + = do { let pat_mult = scaledMult pat_ty + ; pat_ty <- expTypeToType (scaledThing pat_ty) ; traceTc "tcPatBndr(not let)" (ppr bndr_name $$ ppr pat_ty) - ; return (idHsWrapper, mkLocalIdOrCoVar bndr_name pat_ty) } + ; return (idHsWrapper, mkLocalIdOrCoVar bndr_name pat_mult pat_ty) } -- We should not have "OrCoVar" here, this is a bug (#17545) -- Whether or not there is a sig is irrelevant, -- as this is local -newLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId +newLetBndr :: LetBndrSpec -> Name -> Mult -> TcType -> TcM TcId -- Make up a suitable Id for the pattern-binder. -- See Note [Typechecking pattern bindings], item (4) in GHC.Tc.Gen.Bind -- @@ -248,11 +251,11 @@ newLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId -- In the monomorphic case when we are not going to generalise -- (plan NoGen, no_gen = LetGblBndr) there is no AbsBinds, -- and we use the original name directly -newLetBndr LetLclBndr name ty +newLetBndr LetLclBndr name w ty = do { mono_name <- cloneLocalName name - ; return (mkLocalId mono_name ty) } -newLetBndr (LetGblBndr prags) name ty - = addInlinePrags (mkLocalId name ty) (lookupPragEnv prags name) + ; return (mkLocalId mono_name w ty) } +newLetBndr (LetGblBndr prags) name w ty + = addInlinePrags (mkLocalId name w ty) (lookupPragEnv prags name) tc_sub_type :: PatEnv -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper -- tcSubTypeET with the UserTypeCtxt specialised to GenSigCtxt @@ -322,7 +325,7 @@ tcMultiple tc_pat penv args thing_inside ; loop penv args } -------------------- -tc_lpat :: ExpSigmaType +tc_lpat :: Scaled ExpSigmaType -> Checker (LPat GhcRn) (LPat GhcTcId) tc_lpat pat_ty penv (L span pat) thing_inside = setSrcSpan span $ @@ -330,7 +333,7 @@ tc_lpat pat_ty penv (L span pat) thing_inside thing_inside ; return (L span pat', res) } -tc_lpats :: [ExpSigmaType] +tc_lpats :: [Scaled ExpSigmaType] -> Checker [LPat GhcRn] [LPat GhcTcId] tc_lpats tys penv pats = ASSERT2( equalLength pats tys, ppr pats $$ ppr tys ) @@ -339,17 +342,24 @@ tc_lpats tys penv pats (zipEqual "tc_lpats" pats tys) -------------------- -tc_pat :: ExpSigmaType +-- See Note [tcSubMult's wrapper] in TcUnify. +checkManyPattern :: Scaled a -> TcM HsWrapper +checkManyPattern pat_ty = tcSubMult NonLinearPatternOrigin Many (scaledMult pat_ty) + +tc_pat :: Scaled ExpSigmaType -- ^ Fully refined result type -> Checker (Pat GhcRn) (Pat GhcTcId) -- ^ Translated pattern + tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of VarPat x (L l name) -> do { (wrap, id) <- tcPatBndr penv name pat_ty - ; res <- tcExtendIdEnv1 name id thing_inside - ; pat_ty <- readExpType pat_ty - ; return (mkHsWrapPat wrap (VarPat x (L l id)) pat_ty, res) } + ; (res, mult_wrap) <- tcCheckUsage name (scaledMult pat_ty) $ + tcExtendIdEnv1 name id thing_inside + -- See Note [tcSubMult's wrapper] in TcUnify. + ; pat_ty <- readExpType (scaledThing pat_ty) + ; return (mkHsWrapPat (wrap <.> mult_wrap) (VarPat x (L l id)) pat_ty, res) } ParPat x pat -> do { (pat', res) <- tc_lpat pat_ty penv pat thing_inside @@ -360,7 +370,9 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of ; return (BangPat x pat', res) } LazyPat x pat -> do - { (pat', (res, pat_ct)) + { mult_wrap <- checkManyPattern pat_ty + -- See Note [tcSubMult's wrapper] in TcUnify. + ; (pat', (res, pat_ct)) <- tc_lpat pat_ty (makeLazy penv) pat $ captureConstraints thing_inside -- Ignore refined penv', revert to penv @@ -370,20 +382,24 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of -- see Note [Hopping the LIE in lazy patterns] -- Check that the expected pattern type is itself lifted - ; pat_ty <- readExpType pat_ty + ; pat_ty <- readExpType (scaledThing pat_ty) ; _ <- unifyType Nothing (tcTypeKind pat_ty) liftedTypeKind - ; return (LazyPat x pat', res) } + ; return (mkHsWrapPat mult_wrap (LazyPat x pat') pat_ty, res) } WildPat _ -> do - { res <- thing_inside - ; pat_ty <- expTypeToType pat_ty - ; return (WildPat pat_ty, res) } + { mult_wrap <- checkManyPattern pat_ty + -- See Note [tcSubMult's wrapper] in TcUnify. + ; res <- thing_inside + ; pat_ty <- expTypeToType (scaledThing pat_ty) + ; return (mkHsWrapPat mult_wrap (WildPat pat_ty) pat_ty, res) } AsPat x (L nm_loc name) pat -> do - { (wrap, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty) + { mult_wrap <- checkManyPattern pat_ty + -- See Note [tcSubMult's wrapper] in TcUnify. + ; (wrap, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty) ; (pat', res) <- tcExtendIdEnv1 name bndr_id $ - tc_lpat (mkCheckExpType $ idType bndr_id) + tc_lpat (pat_ty `scaledSet`(mkCheckExpType $ idType bndr_id)) penv pat thing_inside -- NB: if we do inference on: -- \ (y@(x::forall a. a->a)) = e @@ -392,35 +408,43 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of -- perhaps be fixed, but only with a bit more work. -- -- If you fix it, don't forget the bindInstsOfPatIds! - ; pat_ty <- readExpType pat_ty - ; return (mkHsWrapPat wrap (AsPat x (L nm_loc bndr_id) pat') pat_ty, - res) } + ; pat_ty <- readExpType (scaledThing pat_ty) + ; return (mkHsWrapPat (wrap <.> mult_wrap) (AsPat x (L nm_loc bndr_id) pat') pat_ty, res) } ViewPat _ expr pat -> do - { (expr',expr_ty) <- tcInferRho expr + { mult_wrap <- checkManyPattern pat_ty + -- See Note [tcSubMult's wrapper] in TcUnify. + -- + -- It should be possible to have view patterns at linear (or otherwise + -- non-Many) multiplicity. But it is not clear at the moment what + -- restriction need to be put in place, if any, for linear view + -- patterns to desugar to type-correct Core. + + ; (expr',expr_ty) <- tcInferRho expr -- Note [View patterns and polymorphism] -- Expression must be a function ; let expr_orig = lexprCtOrigin expr herald = text "A view pattern expression expects" - ; (expr_wrap1, inf_arg_ty, inf_res_sigma) + ; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma) <- matchActualFunTySigma herald expr_orig (Just (unLoc expr)) (1,[]) expr_ty -- See Note [View patterns and polymorphism] -- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_sigma) -- Check that overall pattern is more polymorphic than arg type - ; expr_wrap2 <- tc_sub_type penv pat_ty inf_arg_ty + ; expr_wrap2 <- tc_sub_type penv (scaledThing pat_ty) inf_arg_ty -- expr_wrap2 :: pat_ty "->" inf_arg_ty -- Pattern must have inf_res_sigma - ; (pat', res) <- tc_lpat (mkCheckExpType inf_res_sigma) penv pat thing_inside + ; (pat', res) <- tc_lpat (pat_ty `scaledSet` mkCheckExpType inf_res_sigma) penv pat thing_inside - ; pat_ty <- readExpType pat_ty + ; let Scaled w h_pat_ty = pat_ty + ; pat_ty <- readExpType h_pat_ty ; let expr_wrap2' = mkWpFun expr_wrap2 idHsWrapper - pat_ty inf_res_sigma doc + (Scaled w pat_ty) inf_res_sigma doc -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->" -- (pat_ty -> inf_res_sigma) - expr_wrap = expr_wrap2' <.> expr_wrap1 + expr_wrap = expr_wrap2' <.> expr_wrap1 <.> mult_wrap doc = text "When checking the view pattern function:" <+> (ppr expr) ; return (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res)} @@ -446,35 +470,35 @@ Fortunately that's what matchExpectedFunTySigma returns anyway. -- See Note [Pattern coercions] below SigPat _ pat sig_ty -> do { (inner_ty, tv_binds, wcs, wrap) <- tcPatSig (inPatBind penv) - sig_ty pat_ty + sig_ty (scaledThing pat_ty) -- Using tcExtendNameTyVarEnv is appropriate here -- because we're not really bringing fresh tyvars into scope. -- We're *naming* existing tyvars. Note that it is OK for a tyvar -- from an outer scope to mention one of these tyvars in its kind. ; (pat', res) <- tcExtendNameTyVarEnv wcs $ tcExtendNameTyVarEnv tv_binds $ - tc_lpat (mkCheckExpType inner_ty) penv pat thing_inside - ; pat_ty <- readExpType pat_ty + tc_lpat (pat_ty `scaledSet` mkCheckExpType inner_ty) penv pat thing_inside + ; pat_ty <- readExpType (scaledThing pat_ty) ; return (mkHsWrapPat wrap (SigPat inner_ty pat' sig_ty) pat_ty, res) } ------------------------ -- Lists, tuples, arrays ListPat Nothing pats -> do - { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy penv pat_ty - ; (pats', res) <- tcMultiple (tc_lpat $ mkCheckExpType elt_ty) + { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy penv (scaledThing pat_ty) + ; (pats', res) <- tcMultiple (tc_lpat (pat_ty `scaledSet` mkCheckExpType elt_ty)) penv pats thing_inside - ; pat_ty <- readExpType pat_ty + ; pat_ty <- readExpType (scaledThing pat_ty) ; return (mkHsWrapPat coi (ListPat (ListPatTc elt_ty Nothing) pats') pat_ty, res) } ListPat (Just e) pats -> do - { tau_pat_ty <- expTypeToType pat_ty + { tau_pat_ty <- expTypeToType (scaledThing pat_ty) ; ((pats', res, elt_ty), e') <- tcSyntaxOpGen ListOrigin e [SynType (mkCheckExpType tau_pat_ty)] SynList $ - \ [elt_ty] -> - do { (pats', res) <- tcMultiple (tc_lpat $ mkCheckExpType elt_ty) + \ [elt_ty] _ -> + do { (pats', res) <- tcMultiple (tc_lpat (pat_ty `scaledSet` mkCheckExpType elt_ty)) penv pats thing_inside ; return (pats', res, elt_ty) } ; return (ListPat (ListPatTc elt_ty (Just (tau_pat_ty,e'))) pats', res) @@ -486,12 +510,12 @@ Fortunately that's what matchExpectedFunTySigma returns anyway. -- NB: tupleTyCon does not flatten 1-tuples -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc) - penv pat_ty + penv (scaledThing pat_ty) -- Unboxed tuples have RuntimeRep vars, which we discard: -- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon ; let con_arg_tys = case boxity of Unboxed -> drop arity arg_tys Boxed -> arg_tys - ; (pats', res) <- tc_lpats (map mkCheckExpType con_arg_tys) + ; (pats', res) <- tc_lpats (map (scaledSet pat_ty . mkCheckExpType) con_arg_tys) penv pats thing_inside ; dflags <- getDynFlags @@ -508,7 +532,7 @@ Fortunately that's what matchExpectedFunTySigma returns anyway. isBoxed boxity = LazyPat noExtField (noLoc unmangled_result) | otherwise = unmangled_result - ; pat_ty <- readExpType pat_ty + ; pat_ty <- readExpType (scaledThing pat_ty) ; ASSERT( con_arg_tys `equalLength` pats ) -- Syntactically enforced return (mkHsWrapPat coi possibly_mangled_result pat_ty, res) } @@ -516,12 +540,12 @@ Fortunately that's what matchExpectedFunTySigma returns anyway. SumPat _ pat alt arity -> do { let tc = sumTyCon arity ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc) - penv pat_ty + penv (scaledThing pat_ty) ; -- Drop levity vars, we don't care about them here let con_arg_tys = drop arity arg_tys - ; (pat', res) <- tc_lpat (mkCheckExpType (con_arg_tys `getNth` (alt - 1))) + ; (pat', res) <- tc_lpat (pat_ty `scaledSet` mkCheckExpType (con_arg_tys `getNth` (alt - 1))) penv pat thing_inside - ; pat_ty <- readExpType pat_ty + ; pat_ty <- readExpType (scaledThing pat_ty) ; return (mkHsWrapPat coi (SumPat con_arg_tys pat' alt arity) pat_ty , res) } @@ -535,9 +559,9 @@ Fortunately that's what matchExpectedFunTySigma returns anyway. -- Literal patterns LitPat x simple_lit -> do { let lit_ty = hsLitType simple_lit - ; wrap <- tc_sub_type penv pat_ty lit_ty + ; wrap <- tc_sub_type penv (scaledThing pat_ty) lit_ty ; res <- thing_inside - ; pat_ty <- readExpType pat_ty + ; pat_ty <- readExpType (scaledThing pat_ty) ; return ( mkHsWrapPat wrap (LitPat x (convertLit simple_lit)) pat_ty , res) } @@ -560,11 +584,16 @@ Fortunately that's what matchExpectedFunTySigma returns anyway. -- -- When there is no negation, neg_lit_ty and lit_ty are the same NPat _ (L l over_lit) mb_neg eq -> do - { let orig = LiteralOrigin over_lit + { mult_wrap <- checkManyPattern pat_ty + -- See Note [tcSubMult's wrapper] in TcUnify. + -- + -- It may be possible to refine linear pattern so that they work in + -- linear environments. But it is not clear how useful this is. + ; let orig = LiteralOrigin over_lit ; ((lit', mb_neg'), eq') - <- tcSyntaxOp orig eq [SynType pat_ty, SynAny] + <- tcSyntaxOp orig eq [SynType (scaledThing pat_ty), SynAny] (mkCheckExpType boolTy) $ - \ [neg_lit_ty] -> + \ [neg_lit_ty] _ -> let new_over_lit lit_ty = newOverloadedLit over_lit (mkCheckExpType lit_ty) in case mb_neg of @@ -573,11 +602,14 @@ Fortunately that's what matchExpectedFunTySigma returns anyway. -- The 'negate' is re-mappable syntax second Just <$> (tcSyntaxOp orig neg [SynRho] (mkCheckExpType neg_lit_ty) $ - \ [lit_ty] -> new_over_lit lit_ty) + \ [lit_ty] _ -> new_over_lit lit_ty) + -- applied to a closed literal: linearity doesn't matter as + -- literals are typed in an empty environment, hence have + -- all multiplicities. ; res <- thing_inside - ; pat_ty <- readExpType pat_ty - ; return (NPat pat_ty (L l lit') mb_neg' eq', res) } + ; pat_ty <- readExpType (scaledThing pat_ty) + ; return (mkHsWrapPat mult_wrap (NPat pat_ty (L l lit') mb_neg' eq') pat_ty, res) } {- Note [NPlusK patterns] @@ -610,19 +642,21 @@ AST is used for the subtraction operation. -- See Note [NPlusK patterns] NPlusKPat _ (L nm_loc name) (L loc lit) _ ge minus -> do - { pat_ty <- expTypeToType pat_ty + { mult_wrap <- checkManyPattern pat_ty + -- See Note [tcSubMult's wrapper] in TcUnify. + ; pat_ty <- expTypeToType (scaledThing pat_ty) ; let orig = LiteralOrigin lit ; (lit1', ge') <- tcSyntaxOp orig ge [synKnownType pat_ty, SynRho] (mkCheckExpType boolTy) $ - \ [lit1_ty] -> + \ [lit1_ty] _ -> newOverloadedLit lit (mkCheckExpType lit1_ty) ; ((lit2', minus_wrap, bndr_id), minus') <- tcSyntaxOpGen orig minus [synKnownType pat_ty, SynRho] SynAny $ - \ [lit2_ty, var_ty] -> + \ [lit2_ty, var_ty] _ -> do { lit2' <- newOverloadedLit lit (mkCheckExpType lit2_ty) ; (wrap, bndr_id) <- setSrcSpan nm_loc $ - tcPatBndr penv name (mkCheckExpType var_ty) + tcPatBndr penv name (unrestricted $ mkCheckExpType var_ty) -- co :: var_ty ~ idType bndr_id -- minus_wrap is applicable to minus' @@ -650,7 +684,7 @@ AST is used for the subtraction operation. -- we get warnings if we try. #17783 pat' = NPlusKPat pat_ty (L nm_loc bndr_id) (L loc lit1') lit2' ge' minus'' - ; return (pat', res) } + ; return (mkHsWrapPat mult_wrap pat' pat_ty, res) } -- HsSpliced is an annotation produced by 'GHC.Rename.Splice.rnSplicePat'. -- Here we get rid of it and add the finalizers to the global environment. @@ -813,7 +847,7 @@ to express the local scope of GADT refinements. -- with scrutinee of type (T ty) tcConPat :: PatEnv -> Located Name - -> ExpSigmaType -- Type of the pattern + -> Scaled ExpSigmaType -- Type of the pattern -> HsConPatDetails GhcRn -> TcM a -> TcM (Pat GhcTcId, a) tcConPat penv con_lname@(L _ con_name) pat_ty arg_pats thing_inside @@ -826,10 +860,10 @@ tcConPat penv con_lname@(L _ con_name) pat_ty arg_pats thing_inside } tcDataConPat :: PatEnv -> Located Name -> DataCon - -> ExpSigmaType -- Type of the pattern + -> Scaled ExpSigmaType -- Type of the pattern -> HsConPatDetails GhcRn -> TcM a -> TcM (Pat GhcTcId, a) -tcDataConPat penv (L con_span con_name) data_con pat_ty +tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled arg_pats thing_inside = do { let tycon = dataConTyCon data_con -- For data families this is the representation tycon @@ -840,13 +874,13 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty -- Instantiate the constructor type variables [a->ty] -- This may involve doing a family-instance coercion, -- and building a wrapper - ; (wrap, ctxt_res_tys) <- matchExpectedConTy penv tycon pat_ty - ; pat_ty <- readExpType pat_ty + ; (wrap, ctxt_res_tys) <- matchExpectedConTy penv tycon pat_ty_scaled + ; pat_ty <- readExpType (scaledThing pat_ty_scaled) -- Add the stupid theta ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys - ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ arg_tys + ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ (map scaledThing arg_tys) ; checkExistentials ex_tvs all_arg_tys penv ; tenv <- instTyVarsWith PatOrigin univ_tvs ctxt_res_tys @@ -861,7 +895,9 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty -- pat_ty' is type of the actual constructor application -- pat_ty' /= pat_ty iff coi /= IdCo - arg_tys' = substTys tenv arg_tys + arg_tys' = substScaledTys tenv arg_tys + pat_mult = scaledMult pat_ty_scaled + arg_tys_scaled = map (scaleScaled pat_mult) arg_tys' ; traceTc "tcConPat" (vcat [ ppr con_name , pprTyVars univ_tvs @@ -875,7 +911,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty ; if null ex_tvs && null eq_spec && null theta then do { -- The common case; no class bindings etc -- (see Note [Arrows and patterns]) - (arg_pats', res) <- tcConArgs (RealDataCon data_con) arg_tys' + (arg_pats', res) <- tcConArgs (RealDataCon data_con) arg_tys_scaled penv arg_pats thing_inside ; let res_pat = ConPat { pat_con = header , pat_args = arg_pats' @@ -912,7 +948,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty ; given <- newEvVars theta' ; (ev_binds, (arg_pats', res)) <- checkConstraints skol_info ex_tvs' given $ - tcConArgs (RealDataCon data_con) arg_tys' penv arg_pats thing_inside + tcConArgs (RealDataCon data_con) arg_tys_scaled penv arg_pats thing_inside ; let res_pat = ConPat { pat_con = header @@ -929,7 +965,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty } } tcPatSynPat :: PatEnv -> Located Name -> PatSyn - -> ExpSigmaType -- Type of the pattern + -> Scaled ExpSigmaType -- Type of the pattern -> HsConPatDetails GhcRn -> TcM a -> TcM (Pat GhcTcId, a) tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside @@ -937,15 +973,20 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside ; (subst, univ_tvs') <- newMetaTyVars univ_tvs - ; let all_arg_tys = ty : prov_theta ++ arg_tys + ; let all_arg_tys = ty : prov_theta ++ (map scaledThing arg_tys) ; checkExistentials ex_tvs all_arg_tys penv ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs ; let ty' = substTy tenv ty - arg_tys' = substTys tenv arg_tys + arg_tys' = substScaledTys tenv arg_tys + pat_mult = scaledMult pat_ty + arg_tys_scaled = map (scaleScaled pat_mult) arg_tys' prov_theta' = substTheta tenv prov_theta req_theta' = substTheta tenv req_theta - ; wrap <- tc_sub_type penv pat_ty ty' + ; mult_wrap <- checkManyPattern pat_ty + -- See Note [tcSubMult's wrapper] in TcUnify. + + ; wrap <- tc_sub_type penv (scaledThing pat_ty) ty' ; traceTc "tcPatSynPat" (ppr pat_syn $$ ppr pat_ty $$ ppr ty' $$ @@ -966,7 +1007,7 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside ; traceTc "checkConstraints {" Outputable.empty ; (ev_binds, (arg_pats', res)) <- checkConstraints skol_info ex_tvs' prov_dicts' $ - tcConArgs (PatSynCon pat_syn) arg_tys' penv arg_pats thing_inside + tcConArgs (PatSynCon pat_syn) arg_tys_scaled penv arg_pats thing_inside ; traceTc "checkConstraints }" (ppr ev_binds) ; let res_pat = ConPat { pat_con = L con_span $ PatSynCon pat_syn @@ -979,8 +1020,8 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside , cpt_wrap = req_wrap } } - ; pat_ty <- readExpType pat_ty - ; return (mkHsWrapPat wrap res_pat pat_ty, res) } + ; pat_ty <- readExpType (scaledThing pat_ty) + ; return (mkHsWrapPat (wrap <.> mult_wrap) res_pat pat_ty, res) } ---------------------------- -- | Convenient wrapper for calling a matchExpectedXXX function @@ -1001,9 +1042,9 @@ matchExpectedConTy :: PatEnv -- constructor actually returns -- In the case of a data family this is -- the /representation/ TyCon - -> ExpSigmaType -- The type of the pattern; in the case - -- of a data family this would mention - -- the /family/ TyCon + -> Scaled ExpSigmaType -- The type of the pattern; in the + -- case of a data family this would + -- mention the /family/ TyCon -> TcM (HsWrapper, [TcSigmaType]) -- See Note [Matching constructor patterns] -- Returns a wrapper : pat_ty "->" T ty1 ... tyn @@ -1011,7 +1052,7 @@ matchExpectedConTy (PE { pe_orig = orig }) data_tc exp_pat_ty | Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc -- Comments refer to Note [Matching constructor patterns] -- co_tc :: forall a. T [a] ~ T7 a - = do { pat_ty <- expTypeToType exp_pat_ty + = do { pat_ty <- expTypeToType (scaledThing exp_pat_ty) ; (wrap, pat_rho) <- topInstantiate orig pat_ty ; (subst, tvs') <- newMetaTyVars (tyConTyVars data_tc) @@ -1038,7 +1079,7 @@ matchExpectedConTy (PE { pe_orig = orig }) data_tc exp_pat_ty ; return ( mkWpCastR full_co <.> wrap, tys') } | otherwise - = do { pat_ty <- expTypeToType exp_pat_ty + = do { pat_ty <- expTypeToType (scaledThing exp_pat_ty) ; (wrap, pat_rho) <- topInstantiate orig pat_ty ; (coi, tys) <- matchExpectedTyConApp data_tc pat_rho ; return (mkWpCastN (mkTcSymCo coi) <.> wrap, tys) } @@ -1072,7 +1113,7 @@ Suppose (coi, tys) = matchExpectedConType data_tc pat_ty error messages; it's a purely internal thing -} -tcConArgs :: ConLike -> [TcSigmaType] +tcConArgs :: ConLike -> [Scaled TcSigmaType] -> Checker (HsConPatDetails GhcRn) (HsConPatDetails GhcTc) tcConArgs con_like arg_tys penv con_args thing_inside = case con_args of @@ -1114,7 +1155,7 @@ tcConArgs con_like arg_tys penv con_args thing_inside = case con_args of pun), res) } - find_field_ty :: Name -> FieldLabelString -> TcM TcType + find_field_ty :: Name -> FieldLabelString -> TcM (Scaled TcType) find_field_ty sel lbl = case [ty | (fl, ty) <- field_tys, flSelector fl == sel ] of @@ -1131,14 +1172,15 @@ tcConArgs con_like arg_tys penv con_args thing_inside = case con_args of traceTc "find_field" (ppr pat_ty <+> ppr extras) ASSERT( null extras ) (return pat_ty) - field_tys :: [(FieldLabel, TcType)] + field_tys :: [(FieldLabel, Scaled TcType)] field_tys = zip (conLikeFieldLabels con_like) arg_tys -- Don't use zipEqual! If the constructor isn't really a record, then -- dataConFieldLabels will be empty (and each field in the pattern -- will generate an error below). -tcConArg :: Checker (LPat GhcRn, TcSigmaType) (LPat GhcTc) -tcConArg penv (arg_pat, arg_ty) = tc_lpat (mkCheckExpType arg_ty) penv arg_pat +tcConArg :: Checker (LPat GhcRn, Scaled TcSigmaType) (LPat GhcTc) +tcConArg penv (arg_pat, Scaled arg_mult arg_ty) + = tc_lpat (Scaled arg_mult (mkCheckExpType arg_ty)) penv arg_pat addDataConStupidTheta :: DataCon -> [TcType] -> TcM () -- Instantiate the "stupid theta" of the data con, and throw diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs index 7475b2e737..49de48cebd 100644 --- a/compiler/GHC/Tc/Gen/Rule.hs +++ b/compiler/GHC/Tc/Gen/Rule.hs @@ -28,6 +28,7 @@ import GHC.Tc.Utils.Unify( buildImplicationFor ) import GHC.Tc.Types.Evidence( mkTcCoVarCo ) import GHC.Core.Type import GHC.Core.TyCon( isTypeFamilyTyCon ) +import GHC.Core.Multiplicity import GHC.Types.Id import GHC.Types.Var( EvVar ) import GHC.Types.Var.Set @@ -221,7 +222,7 @@ tcRuleTmBndrs [] = return ([],[]) tcRuleTmBndrs (L _ (RuleBndr _ (L _ name)) : rule_bndrs) = do { ty <- newOpenFlexiTyVarTy ; (tyvars, tmvars) <- tcRuleTmBndrs rule_bndrs - ; return (tyvars, mkLocalId name ty : tmvars) } + ; return (tyvars, mkLocalId name Many ty : tmvars) } tcRuleTmBndrs (L _ (RuleBndrSig _ (L _ name) rn_ty) : rule_bndrs) -- e.g x :: a->a -- The tyvar 'a' is brought into scope first, just as if you'd written @@ -230,7 +231,7 @@ tcRuleTmBndrs (L _ (RuleBndrSig _ (L _ name) rn_ty) : rule_bndrs) -- error for each out-of-scope type variable used = do { let ctxt = RuleSigCtxt name ; (_ , tvs, id_ty) <- tcHsPatSigType ctxt rn_ty - ; let id = mkLocalId name id_ty + ; let id = mkLocalId name Many id_ty -- See Note [Typechecking pattern signature binders] in GHC.Tc.Gen.HsType -- The type variables scope over subsequent bindings; yuk diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs index df0c7d37f6..89fcff3079 100644 --- a/compiler/GHC/Tc/Gen/Sig.hs +++ b/compiler/GHC/Tc/Gen/Sig.hs @@ -40,6 +40,7 @@ import GHC.Tc.Utils.Instantiate( topInstantiate ) import GHC.Tc.Utils.Env( tcLookupId ) import GHC.Tc.Types.Evidence( HsWrapper, (<.>) ) import GHC.Core.Type ( mkTyVarBinders ) +import GHC.Core.Multiplicity import GHC.Driver.Session import GHC.Types.Var ( TyVar, Specificity(..), tyVarKind, binderVars ) @@ -224,7 +225,12 @@ tcUserTypeSig loc hs_sig_ty mb_name = do { sigma_ty <- tcHsSigWcType ctxt_F hs_sig_ty ; traceTc "tcuser" (ppr sigma_ty) ; return $ - CompleteSig { sig_bndr = mkLocalId name sigma_ty + CompleteSig { sig_bndr = mkLocalId name Many sigma_ty + -- We use `Many' as the multiplicity here, + -- as if this identifier corresponds to + -- anything, it is a top-level + -- definition. Which are all unrestricted in + -- the current implementation. , sig_ctxt = ctxt_T , sig_loc = loc } } -- Location of the <type> in f :: <type> @@ -266,7 +272,7 @@ no_anon_wc lty = go lty HsWildCardTy _ -> False HsAppTy _ ty1 ty2 -> go ty1 && go ty2 HsAppKindTy _ ty ki -> go ty && go ki - HsFunTy _ ty1 ty2 -> go ty1 && go ty2 + HsFunTy _ w ty1 ty2 -> go ty1 && go ty2 && go (arrowToHsType w) HsListTy _ ty -> go ty HsTupleTy _ _ tys -> gos tys HsSumTy _ tys -> gos tys @@ -436,7 +442,7 @@ tcPatSynSig name sig_ty -- arguments become the types of binders. We thus cannot allow -- levity polymorphism here ; let (arg_tys, _) = tcSplitFunTys body_ty' - ; mapM_ (checkForLevPoly empty) arg_tys + ; mapM_ (checkForLevPoly empty . scaledThing) arg_tys ; traceTc "tcTySig }" $ vcat [ text "implicit_tvs" <+> ppr_tvs implicit_tvs' diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs index 140299997a..5d0db81183 100644 --- a/compiler/GHC/Tc/Gen/Splice.hs +++ b/compiler/GHC/Tc/Gen/Splice.hs @@ -44,6 +44,7 @@ import GHC.Driver.Finder import GHC.Types.Name import GHC.Tc.Utils.Monad import GHC.Tc.Utils.TcType +import GHC.Core.Multiplicity import GHC.Utils.Outputable import GHC.Tc.Gen.Expr @@ -238,7 +239,7 @@ tcUntypedBracket rn_expr brack ps res_ty -- | A type variable with kind * -> * named "m" mkMetaTyVar :: TcM TyVar mkMetaTyVar = - newNamedFlexiTyVar (fsLit "m") (mkVisFunTy liftedTypeKind liftedTypeKind) + newNamedFlexiTyVar (fsLit "m") (mkVisFunTyMany liftedTypeKind liftedTypeKind) -- | For a type 'm', emit the constraint 'Quote m'. @@ -1757,7 +1758,7 @@ reifyDataCon isGadtDataCon tys dc filterOut (`elemVarSet` eq_spec_tvs) g_univ_tvs ; let (tvb_subst, g_user_tvs) = subst_tv_binders univ_subst g_user_tvs' g_theta = substTys tvb_subst g_theta' - g_arg_tys = substTys tvb_subst g_arg_tys' + g_arg_tys = substTys tvb_subst (map scaledThing g_arg_tys') g_res_ty = substTy tvb_subst g_res_ty' ; r_arg_tys <- reifyTypes (if isGadtDataCon then g_arg_tys else arg_tys) @@ -2115,9 +2116,14 @@ reifyType ty@(AppTy {}) = do filter_out_invisible_args ty_head ty_args = filterByList (map isVisibleArgFlag $ appTyArgFlags ty_head ty_args) ty_args -reifyType ty@(FunTy { ft_af = af, ft_arg = t1, ft_res = t2 }) +reifyType ty@(FunTy { ft_af = af, ft_mult = Many, ft_arg = t1, ft_res = t2 }) | InvisArg <- af = reify_for_all Inferred ty -- Types like ((?x::Int) => Char -> Char) - | otherwise = do { [r1,r2] <- reifyTypes [t1,t2] ; return (TH.ArrowT `TH.AppT` r1 `TH.AppT` r2) } + | otherwise = do { [r1,r2] <- reifyTypes [t1,t2] + ; return (TH.ArrowT `TH.AppT` r1 `TH.AppT` r2) } +reifyType ty@(FunTy { ft_af = af, ft_mult = tm, ft_arg = t1, ft_res = t2 }) + | InvisArg <- af = noTH (sLit "linear invisible argument") (ppr ty) + | otherwise = do { [rm,r1,r2] <- reifyTypes [tm,t1,t2] + ; return (TH.MulArrowT `TH.AppT` rm `TH.AppT` r1 `TH.AppT` r2) } reifyType (CastTy t _) = reifyType t -- Casts are ignored in TH reifyType ty@(CoercionTy {})= noTH (sLit "coercions in types") (ppr ty) @@ -2145,7 +2151,7 @@ reifyTypes :: [Type] -> TcM [TH.Type] reifyTypes = mapM reifyType reifyPatSynType - :: ([InvisTVBinder], ThetaType, [InvisTVBinder], ThetaType, [Type], Type) -> TcM TH.Type + :: ([InvisTVBinder], ThetaType, [InvisTVBinder], ThetaType, [Scaled Type], Type) -> TcM TH.Type -- reifies a pattern synonym's type and returns its *complete* type -- signature; see NOTE [Pattern synonym signatures and Template -- Haskell] @@ -2213,7 +2219,7 @@ reify_tc_app tc tys else TH.TupleT arity | tc `hasKey` constraintKindTyConKey = TH.ConstraintT - | tc `hasKey` funTyConKey = TH.ArrowT + | tc `hasKey` unrestrictedFunTyConKey = TH.ArrowT | tc `hasKey` listTyConKey = TH.ListT | tc `hasKey` nilDataConKey = TH.PromotedNilT | tc `hasKey` consDataConKey = TH.PromotedConsT diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs index aec5c85e20..642e303442 100644 --- a/compiler/GHC/Tc/Instance/Class.hs +++ b/compiler/GHC/Tc/Instance/Class.hs @@ -32,6 +32,7 @@ import GHC.Builtin.Names import GHC.Types.Id import GHC.Core.Type +import GHC.Core.Multiplicity import GHC.Core.Make ( mkStringExprFS, mkNaturalExpr ) import GHC.Types.Name ( Name, pprDefinedAt ) @@ -430,15 +431,15 @@ matchTypeable clas [k,t] -- clas = Typeable matchTypeable _ _ = return NoInstance -- | Representation for a type @ty@ of the form @arg -> ret@. -doFunTy :: Class -> Type -> Type -> Type -> TcM ClsInstResult -doFunTy clas ty arg_ty ret_ty +doFunTy :: Class -> Type -> Scaled Type -> Type -> TcM ClsInstResult +doFunTy clas ty (Scaled mult arg_ty) ret_ty = return $ OneInst { cir_new_theta = preds , cir_mk_ev = mk_ev , cir_what = BuiltinInstance } where - preds = map (mk_typeable_pred clas) [arg_ty, ret_ty] - mk_ev [arg_ev, ret_ev] = evTypeable ty $ - EvTypeableTrFun (EvExpr arg_ev) (EvExpr ret_ev) + preds = map (mk_typeable_pred clas) [mult, arg_ty, ret_ty] + mk_ev [mult_ev, arg_ev, ret_ev] = evTypeable ty $ + EvTypeableTrFun (EvExpr mult_ev) (EvExpr arg_ev) (EvExpr ret_ev) mk_ev _ = panic "GHC.Tc.Solver.Interact.doFunTy" @@ -685,7 +686,7 @@ matchHasField dflags short_cut clas tys -- the HasField x r a dictionary. The preds will -- typically be empty, but if the datatype has a -- "stupid theta" then we have to include it here. - ; let theta = mkPrimEqPred sel_ty (mkVisFunTy r_ty a_ty) : preds + ; let theta = mkPrimEqPred sel_ty (mkVisFunTyMany r_ty a_ty) : preds -- Use the equality proof to cast the selector Id to -- type (r -> a), then use the newtype coercion to cast diff --git a/compiler/GHC/Tc/Instance/Typeable.hs b/compiler/GHC/Tc/Instance/Typeable.hs index 3f8b7d8281..a7b3d83e09 100644 --- a/compiler/GHC/Tc/Instance/Typeable.hs +++ b/compiler/GHC/Tc/Instance/Typeable.hs @@ -34,6 +34,7 @@ import GHC.Types.Id import GHC.Core.Type import GHC.Core.TyCon import GHC.Core.DataCon +import GHC.Core.Multiplicity import GHC.Unit.Module import GHC.Hs import GHC.Driver.Session @@ -437,7 +438,9 @@ kindIsTypeable ty | isLiftedTypeKind ty = True kindIsTypeable (TyVarTy _) = True kindIsTypeable (AppTy a b) = kindIsTypeable a && kindIsTypeable b -kindIsTypeable (FunTy _ a b) = kindIsTypeable a && kindIsTypeable b +kindIsTypeable (FunTy _ w a b) = kindIsTypeable w && + kindIsTypeable a && + kindIsTypeable b kindIsTypeable (TyConApp tc args) = tyConIsTypeable tc && all kindIsTypeable args kindIsTypeable (ForAllTy{}) = False @@ -466,8 +469,8 @@ liftTc = KindRepM . lift builtInKindReps :: [(Kind, Name)] builtInKindReps = [ (star, starKindRepName) - , (mkVisFunTy star star, starArrStarKindRepName) - , (mkVisFunTys [star, star] star, starArrStarArrStarKindRepName) + , (mkVisFunTyMany star star, starArrStarKindRepName) + , (mkVisFunTysMany [star, star] star, starArrStarArrStarKindRepName) ] where star = liftedTypeKind @@ -537,7 +540,7 @@ getKindRep stuff@(Stuff {..}) in_scope = go = do -- Place a NOINLINE pragma on KindReps since they tend to be quite -- large and bloat interface files. rep_bndr <- (`setInlinePragma` neverInlinePragma) - <$> newSysLocalId (fsLit "$krep") (mkTyConTy kindRepTyCon) + <$> newSysLocalId (fsLit "$krep") Many (mkTyConTy kindRepTyCon) -- do we need to tie a knot here? flip runStateT env $ unKindRepM $ do @@ -591,7 +594,7 @@ mkKindRepRhs stuff@(Stuff {..}) in_scope = new_kind_rep new_kind_rep (ForAllTy (Bndr var _) ty) = pprPanic "mkTyConKindRepBinds(ForAllTy)" (ppr var $$ ppr ty) - new_kind_rep (FunTy _ t1 t2) + new_kind_rep (FunTy _ _ t1 t2) = do rep1 <- getKindRep stuff in_scope t1 rep2 <- getKindRep stuff in_scope t2 return $ nlHsDataCon kindRepFunDataCon diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs index f6e5b87f53..5ef192befe 100644 --- a/compiler/GHC/Tc/Module.hs +++ b/compiler/GHC/Tc/Module.hs @@ -1274,7 +1274,7 @@ checkBootTyCon is_boot tc1 tc2 check (map flSelector (dataConFieldLabels c1) == map flSelector (dataConFieldLabels c2)) (text "The record label lists for" <+> pname1 <+> text "differ") `andThenCheck` - check (eqType (dataConUserType c1) (dataConUserType c2)) + check (eqType (dataConWrapperType c1) (dataConWrapperType c2)) (text "The types for" <+> pname1 <+> text "differ") where name1 = dataConName c1 @@ -2446,7 +2446,7 @@ getGhciStepIO = do { hst_tele = mkHsForAllInvisTele [noLoc $ UserTyVar noExtField SpecifiedSpec (noLoc a_tv)] , hst_xforall = noExtField - , hst_body = nlHsFunTy ghciM ioM } + , hst_body = nlHsFunTy HsUnrestrictedArrow ghciM ioM } stepTy :: LHsSigWcType GhcRn stepTy = mkEmptyWildCardBndrs (mkEmptyImplicitBndrs step_ty) @@ -2965,7 +2965,8 @@ ppr_datacons debug type_env = ppr_things "DATA CONSTRUCTORS" ppr_dc wanted_dcs -- The filter gets rid of class data constructors where - ppr_dc dc = ppr dc <+> dcolon <+> ppr (dataConUserType dc) + ppr_dc dc = sdocWithDynFlags (\dflags -> + ppr dc <+> dcolon <+> ppr (dataConDisplayType dflags dc)) all_dcs = typeEnvDataCons type_env wanted_dcs | debug = all_dcs | otherwise = filterOut is_cls_dc all_dcs diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index 61477af714..8754ef9fd0 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -50,7 +50,7 @@ import GHC.Core.Predicate import GHC.Tc.Types.Origin import GHC.Tc.Utils.TcType import GHC.Core.Type -import GHC.Builtin.Types ( liftedRepTy ) +import GHC.Builtin.Types ( liftedRepTy, manyDataConTy ) import GHC.Core.Unify ( tcMatchTyKi ) import GHC.Utils.Misc import GHC.Types.Var @@ -2223,6 +2223,13 @@ defaultTyVarTcS the_tv = do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv) ; unifyTyVar the_tv liftedRepTy ; return True } + | isMultiplicityVar the_tv + , not (isTyVarTyVar the_tv) -- TyVarTvs should only be unified with a tyvar + -- never with a type; c.f. TcMType.defaultTyVar + -- See Note [Kind generalisation and SigTvs] + = do { traceTcS "defaultTyVarTcS Multiplicity" (ppr the_tv) + ; unifyTyVar the_tv manyDataConTy + ; return True } | otherwise = return False -- the common case diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 2fc8664450..79b42d29d5 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -25,6 +25,7 @@ import GHC.Tc.Types.Evidence import GHC.Tc.Types.EvTerm import GHC.Core.Class import GHC.Core.TyCon +import GHC.Core.Multiplicity import GHC.Core.TyCo.Rep -- cleverly decomposes types, good for completeness checking import GHC.Core.Coercion import GHC.Core @@ -551,7 +552,7 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc }) (sc_theta, sc_inner_pred) = splitFunTys sc_rho all_tvs = tvs `chkAppend` sc_tvs - all_theta = theta `chkAppend` sc_theta + all_theta = theta `chkAppend` (map scaledThing sc_theta) swizzled_pred = mkInfSigmaTy all_tvs all_theta sc_inner_pred -- evar :: forall tvs. theta => cls tys @@ -1007,16 +1008,16 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _ -- Decompose FunTy: (s -> t) and (c => t) -- NB: don't decompose (Int -> blah) ~ (Show a => blah) can_eq_nc' _flat _rdr_env _envs ev eq_rel - (FunTy { ft_af = af1, ft_arg = ty1a, ft_res = ty1b }) _ - (FunTy { ft_af = af2, ft_arg = ty2a, ft_res = ty2b }) _ + (FunTy { ft_mult = am1, ft_af = af1, ft_arg = ty1a, ft_res = ty1b }) _ + (FunTy { ft_mult = am2, ft_af = af2, ft_arg = ty2a, ft_res = ty2b }) _ | af1 == af2 -- Don't decompose (Int -> blah) ~ (Show a => blah) , Just ty1a_rep <- getRuntimeRep_maybe ty1a -- getRutimeRep_maybe: , Just ty1b_rep <- getRuntimeRep_maybe ty1b -- see Note [Decomposing FunTy] , Just ty2a_rep <- getRuntimeRep_maybe ty2a , Just ty2b_rep <- getRuntimeRep_maybe ty2b = canDecomposableTyConAppOK ev eq_rel funTyCon - [ty1a_rep, ty1b_rep, ty1a, ty1b] - [ty2a_rep, ty2b_rep, ty2a, ty2b] + [am1, ty1a_rep, ty1b_rep, ty1a, ty1b] + [am2, ty2a_rep, ty2b_rep, ty2a, ty2b] -- Decompose type constructor applications -- NB: e have expanded type synonyms already @@ -1177,11 +1178,12 @@ zonk_eq_types = go -- RuntimeReps of the argument and result types. This can be observed in -- testcase tc269. go ty1 ty2 - | Just (arg1, res1) <- split1 - , Just (arg2, res2) <- split2 + | Just (Scaled w1 arg1, res1) <- split1 + , Just (Scaled w2 arg2, res2) <- split2 + , eqType w1 w2 = do { res_a <- go arg1 arg2 ; res_b <- go res1 res2 - ; return $ combine_rev mkVisFunTy res_b res_a + ; return $ combine_rev (mkVisFunTy w1) res_b res_a } | isJust split1 || isJust split2 = bale_out ty1 ty2 @@ -2469,10 +2471,11 @@ unifyWanted loc role orig_ty1 orig_ty2 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2' - go (FunTy _ s1 t1) (FunTy _ s2 t2) + go (FunTy _ w1 s1 t1) (FunTy _ w2 s2 t2) = do { co_s <- unifyWanted loc role s1 s2 ; co_t <- unifyWanted loc role t1 t2 - ; return (mkFunCo role co_s co_t) } + ; co_w <- unifyWanted loc Nominal w1 w2 + ; return (mkFunCo role co_w co_s co_t) } go (TyConApp tc1 tys1) (TyConApp tc2 tys2) | tc1 == tc2, tys1 `equalLength` tys2 , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality @@ -2520,9 +2523,10 @@ unify_derived loc role orig_ty1 orig_ty2 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2' - go (FunTy _ s1 t1) (FunTy _ s2 t2) + go (FunTy _ w1 s1 t1) (FunTy _ w2 s2 t2) = do { unify_derived loc role s1 s2 - ; unify_derived loc role t1 t2 } + ; unify_derived loc role t1 t2 + ; unify_derived loc role w1 w2 } go (TyConApp tc1 tys1) (TyConApp tc2 tys2) | tc1 == tc2, tys1 `equalLength` tys2 , isInjectiveTyCon tc1 role diff --git a/compiler/GHC/Tc/Solver/Flatten.hs b/compiler/GHC/Tc/Solver/Flatten.hs index 6916357691..48249caa5c 100644 --- a/compiler/GHC/Tc/Solver/Flatten.hs +++ b/compiler/GHC/Tc/Solver/Flatten.hs @@ -39,6 +39,8 @@ import Data.Foldable ( foldrM ) import Control.Arrow ( first ) +import GHC.Core.Multiplicity + {- Note [The flattening story] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1175,12 +1177,13 @@ flatten_one (TyConApp tc tys) -- _ -> fmode = flatten_ty_con_app tc tys -flatten_one ty@(FunTy { ft_arg = ty1, ft_res = ty2 }) +flatten_one ty@(FunTy { ft_mult = mult, ft_arg = ty1, ft_res = ty2 }) = do { (xi1,co1) <- flatten_one ty1 ; (xi2,co2) <- flatten_one ty2 + ; (xi3,co3) <- flatten_one mult ; role <- getRole - ; return (ty { ft_arg = xi1, ft_res = xi2 } - , mkFunCo role co1 co2) } + ; return (ty { ft_mult = xi3, ft_arg = xi1, ft_res = xi2 } + , mkFunCo role co3 co1 co2) } flatten_one ty@(ForAllTy {}) -- TODO (RAE): This is inadequate, as it doesn't flatten the kind of @@ -1921,9 +1924,9 @@ split_pi_tys' ty = split ty ty split orig_ty ty | Just ty' <- coreView ty = split orig_ty ty' split _ (ForAllTy b res) = let (bs, ty, _) = split res res in (Named b : bs, ty, True) - split _ (FunTy { ft_af = af, ft_arg = arg, ft_res = res }) + split _ (FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res }) = let (bs, ty, named) = split res res - in (Anon af arg : bs, ty, named) + in (Anon af (mkScaled w arg) : bs, ty, named) split orig_ty _ = ([], orig_ty, False) {-# INLINE split_pi_tys' #-} @@ -1935,6 +1938,6 @@ ty_con_binders_ty_binders' = foldr go ([], False) go (Bndr tv (NamedTCB vis)) (bndrs, _) = (Named (Bndr tv vis) : bndrs, True) go (Bndr tv (AnonTCB af)) (bndrs, n) - = (Anon af (tyVarKind tv) : bndrs, n) + = (Anon af (unrestricted (tyVarKind tv)) : bndrs, n) {-# INLINE go #-} {-# INLINE ty_con_binders_ty_binders' #-} diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs index 6af35c77c2..a4a56c0a14 100644 --- a/compiler/GHC/Tc/TyCl.hs +++ b/compiler/GHC/Tc/TyCl.hs @@ -44,6 +44,7 @@ import GHC.Tc.Instance.Class( AssocInstInfo(..) ) import GHC.Tc.Utils.TcMType import GHC.Builtin.Types ( unitTy, makeRecoveryTyCon ) import GHC.Tc.Utils.TcType +import GHC.Core.Multiplicity import GHC.Rename.Env( lookupConstructorFields ) import GHC.Tc.Instance.Family import GHC.Core.FamInstEnv @@ -823,9 +824,9 @@ swizzleTcTyConBndrs tc_infos swizzle_var :: Var -> Var swizzle_var v | Just nm <- lookupVarEnv swizzle_env v - = updateVarType swizzle_ty (v `setVarName` nm) + = updateVarTypeAndMult swizzle_ty (v `setVarName` nm) | otherwise - = updateVarType swizzle_ty v + = updateVarTypeAndMult swizzle_ty v (map_type, _, _, _) = mapTyCo swizzleMapper swizzle_ty ty = runIdentity (map_type ty) @@ -1561,10 +1562,10 @@ kcTyClDecl (FamDecl _ (FamilyDecl { fdInfo = fd_info })) fam_tc -- This includes doing kind unification if the type is a newtype. -- See Note [Implementation of UnliftedNewtypes] for why we need -- the first two arguments. -kcConArgTys :: NewOrData -> Kind -> [LHsType GhcRn] -> TcM () +kcConArgTys :: NewOrData -> Kind -> [HsScaled GhcRn (LHsType GhcRn)] -> TcM () kcConArgTys new_or_data res_kind arg_tys = do { let exp_kind = getArgExpKind new_or_data res_kind - ; mapM_ (flip tcCheckLHsType exp_kind . getBangType) arg_tys + ; mapM_ (flip tcCheckLHsType exp_kind . getBangType . hsScaledThing) arg_tys -- See Note [Implementation of UnliftedNewtypes], STEP 2 } @@ -3134,7 +3135,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data ; (ze, qkvs) <- zonkTyBndrs kvs ; (ze, user_qtvbndrs) <- zonkTyVarBindersX ze exp_tvbndrs ; let user_qtvs = binderVars user_qtvbndrs - ; arg_tys <- zonkTcTypesToTypesX ze arg_tys + ; arg_tys <- zonkScaledTcTypesToTypesX ze arg_tys ; ctxt <- zonkTcTypesToTypesX ze ctxt ; fam_envs <- tcGetFamInstEnvs @@ -3216,7 +3217,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data -- Zonk to Types ; (ze, tvbndrs) <- zonkTyVarBinders tvbndrs - ; arg_tys <- zonkTcTypesToTypesX ze arg_tys + ; arg_tys <- zonkScaledTcTypesToTypesX ze arg_tys ; ctxt <- zonkTcTypesToTypesX ze ctxt ; res_ty <- zonkTcTypeToTypeX ze res_ty @@ -3225,7 +3226,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data -- See Note [Checking GADT return types] ctxt' = substTys arg_subst ctxt - arg_tys' = substTys arg_subst arg_tys + arg_tys' = substScaledTys arg_subst arg_tys res_ty' = substTy arg_subst res_ty @@ -3262,7 +3263,7 @@ getArgExpKind NewType res_ki = TheKind res_ki getArgExpKind DataType _ = OpenKind tcConIsInfixH98 :: Name - -> HsConDetails (LHsType GhcRn) (Located [LConDeclField GhcRn]) + -> HsConDetails a b -> TcM Bool tcConIsInfixH98 _ details = case details of @@ -3270,7 +3271,7 @@ tcConIsInfixH98 _ details _ -> return False tcConIsInfixGADT :: Name - -> HsConDetails (LHsType GhcRn) (Located [LConDeclField GhcRn]) + -> HsConDetails (HsScaled GhcRn (LHsType GhcRn)) r -> TcM Bool tcConIsInfixGADT con details = case details of @@ -3278,7 +3279,7 @@ tcConIsInfixGADT con details RecCon {} -> return False PrefixCon arg_tys -- See Note [Infix GADT constructors] | isSymOcc (getOccName con) - , [_ty1,_ty2] <- arg_tys + , [_ty1,_ty2] <- map hsScaledThing arg_tys -> do { fix_env <- getFixityEnv ; return (con `elemNameEnv` fix_env) } | otherwise -> return False @@ -3287,7 +3288,7 @@ tcConArgs :: ContextKind -- expected kind of arguments -- always OpenKind for datatypes, but unlifted newtypes -- might have a specific kind -> HsConDeclDetails GhcRn - -> TcM [(TcType, HsSrcBang)] + -> TcM [(Scaled TcType, HsSrcBang)] tcConArgs exp_kind (PrefixCon btys) = mapM (tcConArg exp_kind) btys tcConArgs exp_kind (InfixCon bty1 bty2) @@ -3298,7 +3299,7 @@ tcConArgs exp_kind (RecCon fields) = mapM (tcConArg exp_kind) btys where -- We need a one-to-one mapping from field_names to btys - combined = map (\(L _ f) -> (cd_fld_names f,cd_fld_type f)) + combined = map (\(L _ f) -> (cd_fld_names f,hsLinear (cd_fld_type f))) (unLoc fields) explode (ns,ty) = zip ns (repeat ty) exploded = concatMap explode combined @@ -3307,12 +3308,13 @@ tcConArgs exp_kind (RecCon fields) tcConArg :: ContextKind -- expected kind for args; always OpenKind for datatypes, -- but might be an unlifted type with UnliftedNewtypes - -> LHsType GhcRn -> TcM (TcType, HsSrcBang) -tcConArg exp_kind bty + -> HsScaled GhcRn (LHsType GhcRn) -> TcM (Scaled TcType, HsSrcBang) +tcConArg exp_kind (HsScaled w bty) = do { traceTc "tcConArg 1" (ppr bty) ; arg_ty <- tcCheckLHsType (getBangType bty) exp_kind + ; w' <- tcMult w ; traceTc "tcConArg 2" (ppr bty) - ; return (arg_ty, getBangStrictness bty) } + ; return (Scaled w' arg_ty, getBangStrictness bty) } {- Note [Infix GADT constructors] @@ -3925,10 +3927,10 @@ checkValidDataCon dflags existential_ok tc con ; checkTc (isJust (tcMatchTy res_ty_tmpl orig_res_ty)) (badDataConTyCon con res_ty_tmpl) -- Note that checkTc aborts if it finds an error. This is - -- critical to avoid panicking when we call dataConUserType + -- critical to avoid panicking when we call dataConDisplayType -- on an un-rejiggable datacon! - ; traceTc "checkValidDataCon 2" (ppr (dataConUserType con)) + ; traceTc "checkValidDataCon 2" (ppr data_con_display_type) -- Check that the result type is a *monotype* -- e.g. reject this: MkT :: T (forall a. a->a) @@ -3940,7 +3942,7 @@ checkValidDataCon dflags existential_ok tc con -- later check in checkNewDataCon handles this, producing a -- better error message than checkForLevPoly would. ; unless (isNewTyCon tc) - (mapM_ (checkForLevPoly empty) (dataConOrigArgTys con)) + (mapM_ (checkForLevPoly empty) (map scaledThing $ dataConOrigArgTys con)) -- Extra checks for newtype data constructors. Importantly, these -- checks /must/ come before the call to checkValidType below. This @@ -3950,7 +3952,7 @@ checkValidDataCon dflags existential_ok tc con ; when (isNewTyCon tc) (checkNewDataCon con) -- Check all argument types for validity - ; checkValidType ctxt (dataConUserType con) + ; checkValidType ctxt data_con_display_type -- Check that existentials are allowed if they are used ; checkTc (existential_ok || isVanillaDataCon con) @@ -3980,8 +3982,9 @@ checkValidDataCon dflags existential_ok tc con ; traceTc "Done validity of data con" $ vcat [ ppr con - , text "Datacon user type:" <+> ppr (dataConUserType con) + , text "Datacon wrapper type:" <+> ppr (dataConWrapperType con) , text "Datacon rep type:" <+> ppr (dataConRepType con) + , text "Datacon display type:" <+> ppr data_con_display_type , text "Rep typcon binders:" <+> ppr (tyConBinders (dataConTyCon con)) , case tyConFamInst_maybe (dataConTyCon con) of Nothing -> text "not family" @@ -4023,6 +4026,9 @@ checkValidDataCon dflags existential_ok tc con bad_bang n herald = hang herald 2 (text "on the" <+> speakNth n <+> text "argument of" <+> quotes (ppr con)) + + data_con_display_type = dataConDisplayType dflags con + ------------------------------- checkNewDataCon :: DataCon -> TcM () -- Further checks for the data constructor of a newtype @@ -4032,11 +4038,18 @@ checkNewDataCon con ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes ; let allowedArgType = - unlifted_newtypes || isLiftedType_maybe arg_ty1 == Just True + unlifted_newtypes || isLiftedType_maybe (scaledThing arg_ty1) == Just True ; checkTc allowedArgType $ vcat [ text "A newtype cannot have an unlifted argument type" , text "Perhaps you intended to use UnliftedNewtypes" ] + ; dflags <- getDynFlags + + ; let check_con what msg = + checkTc what (msg $$ ppr con <+> dcolon <+> ppr (dataConDisplayType dflags con)) + + ; checkTc (ok_mult (scaledMult arg_ty1)) $ + text "A newtype constructor must be linear" ; check_con (null eq_spec) $ text "A newtype constructor must have a return type of form T a1 ... an" @@ -4056,8 +4069,6 @@ checkNewDataCon con where (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig con - check_con what msg - = checkTc what (msg $$ ppr con <+> dcolon <+> ppr (dataConUserType con)) (arg_ty1 : _) = arg_tys @@ -4065,6 +4076,9 @@ checkNewDataCon con ok_bang (HsSrcBang _ _ SrcLazy) = False ok_bang _ = True + ok_mult One = True + ok_mult _ = False + ------------------------------- checkValidClass :: Class -> TcM () checkValidClass cls @@ -4511,7 +4525,7 @@ checkValidRoles tc check_dc_roles datacon = do { traceTc "check_dc_roles" (ppr datacon <+> ppr (tyConRoles tc)) ; mapM_ (check_ty_roles role_env Representational) $ - eqSpecPreds eq_spec ++ theta ++ arg_tys } + eqSpecPreds eq_spec ++ theta ++ (map scaledThing arg_tys) } -- See Note [Role-checking data constructor arguments] in GHC.Tc.TyCl.Utils where (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) @@ -4548,8 +4562,9 @@ checkValidRoles tc = check_ty_roles env role ty1 >> check_ty_roles env Nominal ty2 - check_ty_roles env role (FunTy _ ty1 ty2) - = check_ty_roles env role ty1 + check_ty_roles env role (FunTy _ w ty1 ty2) + = check_ty_roles env role w + >> check_ty_roles env role ty1 >> check_ty_roles env role ty2 check_ty_roles env role (ForAllTy (Bndr tv _) ty) @@ -4719,10 +4734,11 @@ badGadtDecl tc_name badExistential :: DataCon -> SDoc badExistential con - = hang (text "Data constructor" <+> quotes (ppr con) <+> - text "has existential type variables, a context, or a specialised result type") - 2 (vcat [ ppr con <+> dcolon <+> ppr (dataConUserType con) - , parens $ text "Enable ExistentialQuantification or GADTs to allow this" ]) + = sdocWithDynFlags (\dflags -> + hang (text "Data constructor" <+> quotes (ppr con) <+> + text "has existential type variables, a context, or a specialised result type") + 2 (vcat [ ppr con <+> dcolon <+> ppr (dataConDisplayType dflags con) + , parens $ text "Enable ExistentialQuantification or GADTs to allow this" ])) badStupidTheta :: Name -> SDoc badStupidTheta tc_name diff --git a/compiler/GHC/Tc/TyCl/Build.hs b/compiler/GHC/Tc/TyCl/Build.hs index af49e9e28c..5361ff0160 100644 --- a/compiler/GHC/Tc/TyCl/Build.hs +++ b/compiler/GHC/Tc/TyCl/Build.hs @@ -36,6 +36,7 @@ import GHC.Core.TyCon import GHC.Core.Type import GHC.Types.Id import GHC.Tc.Utils.TcType +import GHC.Core.Multiplicity import GHC.Types.SrcLoc( SrcSpan, noSrcSpan ) import GHC.Driver.Session @@ -65,7 +66,7 @@ mkNewTyConRhs tycon_name tycon con roles = tyConRoles tycon res_kind = tyConResKind tycon con_arg_ty = case dataConRepArgTys con of - [arg_ty] -> arg_ty + [arg_ty] -> scaledThing arg_ty tys -> pprPanic "mkNewTyConRhs" (ppr con <+> ppr tys) rhs_ty = substTyWith (dataConUnivTyVars con) (mkTyVarTys tvs) con_arg_ty @@ -110,7 +111,7 @@ buildDataCon :: FamInstEnvs -> [EqSpec] -- Equality spec -> KnotTied ThetaType -- Does not include the "stupid theta" -- or the GADT equalities - -> [KnotTied Type] -- Arguments + -> [KnotTied (Scaled Type)] -- Arguments -> KnotTied Type -- Result types -> KnotTied TyCon -- Rep tycon -> NameEnv ConTag -- Maps the Name of each DataCon to its @@ -132,7 +133,7 @@ buildDataCon fam_envs src_name declared_infix prom_info src_bangs impl_bangs ; traceIf (text "buildDataCon 1" <+> ppr src_name) ; us <- newUniqueSupply ; dflags <- getDynFlags - ; let stupid_ctxt = mkDataConStupidTheta rep_tycon arg_tys univ_tvs + ; let stupid_ctxt = mkDataConStupidTheta rep_tycon (map scaledThing arg_tys) univ_tvs tag = lookupNameEnv_NF tag_map src_name -- See Note [Constructor tag allocation], fixes #14657 data_con = mkDataCon src_name declared_infix prom_info @@ -184,10 +185,10 @@ buildPatSyn src_name declared_infix matcher@(matcher_id,_) builder -- compatible with the pattern synonym ASSERT2((and [ univ_tvs `equalLength` univ_tvs1 , ex_tvs `equalLength` ex_tvs1 - , pat_ty `eqType` substTy subst pat_ty1 + , pat_ty `eqType` substTy subst (scaledThing pat_ty1) , prov_theta `eqTypes` substTys subst prov_theta1 , req_theta `eqTypes` substTys subst req_theta1 - , compareArgTys arg_tys (substTys subst arg_tys1) + , compareArgTys arg_tys (substTys subst (map scaledThing arg_tys1)) ]) , (vcat [ ppr univ_tvs <+> twiddle <+> ppr univ_tvs1 , ppr ex_tvs <+> twiddle <+> ppr ex_tvs1 @@ -202,7 +203,7 @@ buildPatSyn src_name declared_infix matcher@(matcher_id,_) builder where ((_:_:univ_tvs1), req_theta1, tau) = tcSplitSigmaTy $ idType matcher_id ([pat_ty1, cont_sigma, _], _) = tcSplitFunTys tau - (ex_tvs1, prov_theta1, cont_tau) = tcSplitSigmaTy cont_sigma + (ex_tvs1, prov_theta1, cont_tau) = tcSplitSigmaTy (scaledThing cont_sigma) (arg_tys1, _) = (tcSplitFunTys cont_tau) twiddle = char '~' subst = zipTvSubst (univ_tvs1 ++ ex_tvs1) @@ -314,7 +315,7 @@ buildClass tycon_name binders roles fds univ_bndrs [{- No GADT equalities -}] [{- No theta -}] - arg_tys + (map unrestricted arg_tys) -- type classes are unrestricted (mkTyConApp rec_tycon (mkTyVarTys univ_tvs)) rec_tycon (mkTyConTagMap rec_tycon) diff --git a/compiler/GHC/Tc/TyCl/Class.hs b/compiler/GHC/Tc/TyCl/Class.hs index cedd42916b..c6f78ae4e2 100644 --- a/compiler/GHC/Tc/TyCl/Class.hs +++ b/compiler/GHC/Tc/TyCl/Class.hs @@ -40,6 +40,7 @@ import GHC.Tc.Gen.HsType import GHC.Tc.Utils.TcMType import GHC.Core.Type ( piResultTys ) import GHC.Core.Predicate +import GHC.Core.Multiplicity import GHC.Tc.Types.Origin import GHC.Tc.Utils.TcType import GHC.Tc.Utils.Monad @@ -284,7 +285,7 @@ tcDefMeth clas tyvars this_dict binds_in hs_sig_fn prag_fn ctxt = FunSigCtxt sel_name warn_redundant - ; let local_dm_id = mkLocalId local_dm_name local_dm_ty + ; let local_dm_id = mkLocalId local_dm_name Many local_dm_ty local_dm_sig = CompleteSig { sig_bndr = local_dm_id , sig_ctxt = ctxt , sig_loc = getLoc (hsSigType hs_ty) } diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs index 4c43d91f3e..68bf24c342 100644 --- a/compiler/GHC/Tc/TyCl/Instance.hs +++ b/compiler/GHC/Tc/TyCl/Instance.hs @@ -41,6 +41,7 @@ import GHC.Tc.Types.Origin import GHC.Tc.TyCl.Build import GHC.Tc.Utils.Instantiate import GHC.Tc.Instance.Class( AssocInstInfo(..), isNotAssociated ) +import GHC.Core.Multiplicity import GHC.Core.InstEnv import GHC.Tc.Instance.Family import GHC.Core.FamInstEnv @@ -1318,7 +1319,7 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds sc_theta ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id sc_ev_tm ; let sc_top_ty = mkInfForAllTys tyvars $ mkPhiTy (map idType dfun_evs) sc_pred - sc_top_id = mkLocalId sc_top_name sc_top_ty + sc_top_id = mkLocalId sc_top_name Many sc_top_ty export = ABE { abe_ext = noExtField , abe_wrap = idHsWrapper , abe_poly = sc_top_id @@ -1798,7 +1799,7 @@ tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind ; let ctxt = FunSigCtxt sel_name True -- True <=> check for redundant constraints in the -- user-specified instance signature - inner_meth_id = mkLocalId inner_meth_name sig_ty + inner_meth_id = mkLocalId inner_meth_name Many sig_ty inner_meth_sig = CompleteSig { sig_bndr = inner_meth_id , sig_ctxt = ctxt , sig_loc = getLoc (hsSigType hs_sig_ty) } @@ -1849,8 +1850,8 @@ mkMethIds clas tyvars dfun_ev_vars inst_tys sel_id ; local_meth_name <- newName sel_occ -- Base the local_meth_name on the selector name, because -- type errors from tcMethodBody come from here - ; let poly_meth_id = mkLocalId poly_meth_name poly_meth_ty - local_meth_id = mkLocalId local_meth_name local_meth_ty + ; let poly_meth_id = mkLocalId poly_meth_name Many poly_meth_ty + local_meth_id = mkLocalId local_meth_name Many local_meth_ty ; return (poly_meth_id, local_meth_id) } where diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs index 57dd16c8f8..5f99763fdd 100644 --- a/compiler/GHC/Tc/TyCl/PatSyn.hs +++ b/compiler/GHC/Tc/TyCl/PatSyn.hs @@ -24,6 +24,7 @@ import GHC.Prelude import GHC.Hs import GHC.Tc.Gen.Pat +import GHC.Core.Multiplicity import GHC.Core.Type ( tidyTyCoVarBinders, tidyTypes, tidyType ) import GHC.Tc.Utils.Monad import GHC.Tc.Gen.Sig( emptyPragEnv, completeSigFromId ) @@ -106,7 +107,7 @@ recoverPSB (PSB { psb_id = L _ name where -- The matcher_id is used only by the desugarer, so actually -- and error-thunk would probably do just as well here. - matcher_id = mkLocalId matcher_name $ + matcher_id = mkLocalId matcher_name Many $ mkSpecForAllTys [alphaTyVar] alphaTy {- Note [Pattern synonym error recovery] @@ -387,7 +388,7 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys ) pushLevelAndCaptureConstraints $ tcExtendTyVarEnv univ_tvs $ - tcCheckPat PatSyn lpat pat_ty $ + tcCheckPat PatSyn lpat (unrestricted pat_ty) $ do { let in_scope = mkInScopeSet (mkVarSet univ_tvs) empty_subst = mkEmptyTCvSubst in_scope ; (subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst ex_tvs @@ -402,7 +403,7 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details -- substitution. -- See also Note [The substitution invariant] in GHC.Core.TyCo.Subst. ; prov_dicts <- mapM (emitWanted (ProvCtxtOrigin psb)) prov_theta' - ; args' <- zipWithM (tc_arg subst) arg_names arg_tys + ; args' <- zipWithM (tc_arg subst) arg_names (map scaledThing arg_tys) ; return (ex_tvs', prov_dicts, args') } ; let skol_info = SigSkol (PatSynCtxt name) pat_ty [] @@ -423,7 +424,7 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details ; tc_patsyn_finish lname dir is_infix lpat' (univ_bndrs, req_theta, ev_binds, req_dicts) (ex_bndrs, mkTyVarTys ex_tvs', prov_theta, prov_dicts) - (args', arg_tys) + (args', (map scaledThing arg_tys)) pat_ty rec_fields } where tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr GhcTcId) @@ -701,16 +702,16 @@ tcPatSynMatcher (L loc name) lpat | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy]) | otherwise = (args, arg_tys) cont_ty = mkInfSigmaTy ex_tvs prov_theta $ - mkVisFunTys cont_arg_tys res_ty + mkVisFunTysMany cont_arg_tys res_ty - fail_ty = mkVisFunTy voidPrimTy res_ty + fail_ty = mkVisFunTyMany voidPrimTy res_ty ; matcher_name <- newImplicitBinder name mkMatcherOcc - ; scrutinee <- newSysLocalId (fsLit "scrut") pat_ty - ; cont <- newSysLocalId (fsLit "cont") cont_ty - ; fail <- newSysLocalId (fsLit "fail") fail_ty + ; scrutinee <- newSysLocalId (fsLit "scrut") Many pat_ty + ; cont <- newSysLocalId (fsLit "cont") Many cont_ty + ; fail <- newSysLocalId (fsLit "fail") Many fail_ty - ; let matcher_tau = mkVisFunTys [pat_ty, cont_ty, fail_ty] res_ty + ; let matcher_tau = mkVisFunTysMany [pat_ty, cont_ty, fail_ty] res_ty matcher_sigma = mkInfSigmaTy (rr_tv:res_tv:univ_tvs) req_theta matcher_tau matcher_id = mkExportedVanillaId matcher_name matcher_sigma -- See Note [Exported LocalIds] in GHC.Types.Id @@ -730,14 +731,14 @@ tcPatSynMatcher (L loc name) lpat L (getLoc lpat) $ HsCase noExtField (nlHsVar scrutinee) $ MG{ mg_alts = L (getLoc lpat) cases - , mg_ext = MatchGroupTc [pat_ty] res_ty + , mg_ext = MatchGroupTc [unrestricted pat_ty] res_ty , mg_origin = Generated } body' = noLoc $ HsLam noExtField $ MG{ mg_alts = noLoc [mkSimpleMatch LambdaExpr args body] - , mg_ext = MatchGroupTc [pat_ty, cont_ty, fail_ty] res_ty + , mg_ext = MatchGroupTc (map unrestricted [pat_ty, cont_ty, fail_ty]) res_ty , mg_origin = Generated } match = mkMatch (mkPrefixFunRhs (L loc name)) [] @@ -799,7 +800,7 @@ mkPatSynBuilderId dir (L _ name) mkInvisForAllTys univ_bndrs $ mkInvisForAllTys ex_bndrs $ mkPhiTy theta $ - mkVisFunTys arg_tys $ + mkVisFunTysMany arg_tys $ pat_ty builder_id = mkExportedVanillaId builder_name builder_sigma -- See Note [Exported LocalIds] in GHC.Types.Id @@ -905,7 +906,7 @@ tcPatSynBuilderOcc ps add_void :: Bool -> Type -> Type add_void need_dummy_arg ty - | need_dummy_arg = mkVisFunTy voidPrimTy ty + | need_dummy_arg = mkVisFunTyMany voidPrimTy ty | otherwise = ty tcPatToExpr :: Name -> [Located Name] -> LPat GhcRn diff --git a/compiler/GHC/Tc/TyCl/Utils.hs b/compiler/GHC/Tc/TyCl/Utils.hs index 00a4c01493..b49e81ddd2 100644 --- a/compiler/GHC/Tc/TyCl/Utils.hs +++ b/compiler/GHC/Tc/TyCl/Utils.hs @@ -36,6 +36,7 @@ import GHC.Tc.Utils.Monad import GHC.Tc.Utils.Env import GHC.Tc.Gen.Bind( tcValBinds ) import GHC.Core.TyCo.Rep( Type(..), Coercion(..), MCoercion(..), UnivCoProvenance(..) ) +import GHC.Core.Multiplicity import GHC.Tc.Utils.TcType import GHC.Core.Predicate import GHC.Builtin.Types( unitTy ) @@ -90,7 +91,7 @@ synonymTyConsOfType ty go (LitTy _) = emptyNameEnv go (TyVarTy _) = emptyNameEnv go (AppTy a b) = go a `plusNameEnv` go b - go (FunTy _ a b) = go a `plusNameEnv` go b + go (FunTy _ w a b) = go w `plusNameEnv` go a `plusNameEnv` go b go (ForAllTy _ ty) = go ty go (CastTy ty co) = go ty `plusNameEnv` go_co co go (CoercionTy co) = go_co co @@ -124,7 +125,7 @@ synonymTyConsOfType ty go_co (TyConAppCo _ tc cs) = go_tc tc `plusNameEnv` go_co_s cs go_co (AppCo co co') = go_co co `plusNameEnv` go_co co' go_co (ForAllCo _ co co') = go_co co `plusNameEnv` go_co co' - go_co (FunCo _ co co') = go_co co `plusNameEnv` go_co co' + go_co (FunCo _ co_mult co co') = go_co co_mult `plusNameEnv` go_co co `plusNameEnv` go_co co' go_co (CoVarCo _) = emptyNameEnv go_co (HoleCo {}) = emptyNameEnv go_co (AxiomInstCo _ _ cs) = go_co_s cs @@ -579,7 +580,7 @@ irDataCon datacon = setRoleInferenceVars univ_tvs $ irExTyVars ex_tvs $ \ ex_var_set -> mapM_ (irType ex_var_set) - (map tyVarKind ex_tvs ++ eqSpecPreds eq_spec ++ theta ++ arg_tys) + (map tyVarKind ex_tvs ++ eqSpecPreds eq_spec ++ theta ++ (map scaledThing arg_tys)) -- See Note [Role-checking data constructor arguments] where (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) @@ -599,7 +600,7 @@ irType = go lcls' = extendVarSet lcls tv ; markNominal lcls (tyVarKind tv) ; go lcls' ty } - go lcls (FunTy _ arg res) = go lcls arg >> go lcls res + go lcls (FunTy _ w arg res) = go lcls w >> go lcls arg >> go lcls res go _ (LitTy {}) = return () -- See Note [Coercions in role inference] go lcls (CastTy ty _) = go lcls ty @@ -635,7 +636,7 @@ markNominal lcls ty = let nvars = fvVarList (FV.delFVs lcls $ get_ty_vars ty) in get_ty_vars :: Type -> FV get_ty_vars (TyVarTy tv) = unitFV tv get_ty_vars (AppTy t1 t2) = get_ty_vars t1 `unionFV` get_ty_vars t2 - get_ty_vars (FunTy _ t1 t2) = get_ty_vars t1 `unionFV` get_ty_vars t2 + get_ty_vars (FunTy _ w t1 t2) = get_ty_vars w `unionFV` get_ty_vars t1 `unionFV` get_ty_vars t2 get_ty_vars (TyConApp _ tys) = mapUnionFV get_ty_vars tys get_ty_vars (ForAllTy tvb ty) = tyCoFVsBndr tvb (get_ty_vars ty) get_ty_vars (LitTy {}) = emptyFV @@ -881,7 +882,10 @@ mkOneRecordSelector all_cons idDetails fl mkPhiTy (conLikeStupidTheta con1) $ -- Urgh! -- req_theta is empty for normal DataCon mkPhiTy req_theta $ - mkVisFunTy data_ty $ + mkVisFunTyMany data_ty $ + -- Record selectors are always typed with Many. We + -- could improve on it in the case where all the + -- fields in all the constructor have multiplicity Many. field_ty -- Make the binding: sel (C2 { fld = x }) = x diff --git a/compiler/GHC/Tc/Types.hs b/compiler/GHC/Tc/Types.hs index 2afb6bc234..1397a3da4b 100644 --- a/compiler/GHC/Tc/Types.hs +++ b/compiler/GHC/Tc/Types.hs @@ -95,6 +95,7 @@ import GHC.Core.TyCon ( TyCon, tyConKind ) import GHC.Core.PatSyn ( PatSyn ) import GHC.Types.Id ( idType, idName ) import GHC.Types.FieldLabel ( FieldLabel ) +import GHC.Core.UsageEnv import GHC.Tc.Utils.TcType import GHC.Tc.Types.Constraint import GHC.Tc.Types.Origin @@ -775,6 +776,9 @@ data TcLclEnv -- Changes as we move inside an expression tcl_env :: TcTypeEnv, -- The local type environment: -- Ids and TyVars defined in this module + tcl_usage :: TcRef UsageEnv, -- Required multiplicity of bindings is accumulated here. + + tcl_bndrs :: TcBinderStack, -- Used for reporting relevant bindings, -- and for tidying types diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs index 8649871670..5b33394136 100644 --- a/compiler/GHC/Tc/Types/Evidence.hs +++ b/compiler/GHC/Tc/Types/Evidence.hs @@ -88,6 +88,7 @@ import GHC.Utils.Outputable import GHC.Types.SrcLoc import Data.IORef( IORef ) import GHC.Types.Unique.Set +import GHC.Core.Multiplicity {- Note [TcCoercions] @@ -117,7 +118,7 @@ mkTcNomReflCo :: TcType -> TcCoercionN mkTcRepReflCo :: TcType -> TcCoercionR mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion mkTcAppCo :: TcCoercion -> TcCoercionN -> TcCoercion -mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion +mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion -> TcCoercion mkTcAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [TcType] -> [TcCoercion] -> TcCoercion mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType] @@ -201,8 +202,8 @@ data HsWrapper -- Hence (\a. []) `WpCompose` (\b. []) = (\a b. []) -- But ([] a) `WpCompose` ([] b) = ([] b a) - | WpFun HsWrapper HsWrapper TcType SDoc - -- (WpFun wrap1 wrap2 t1)[e] = \(x:t1). wrap2[ e wrap1[x] ] + | WpFun HsWrapper HsWrapper (Scaled TcType) SDoc + -- (WpFun wrap1 wrap2 (w, t1))[e] = \(x:_w t1). wrap2[ e wrap1[x] ] -- So note that if wrap1 :: exp_arg <= act_arg -- wrap2 :: act_res <= exp_res -- then WpFun wrap1 wrap2 : (act_arg -> arg_res) <= (exp_arg -> exp_res) @@ -228,6 +229,18 @@ data HsWrapper | WpLet TcEvBinds -- Non-empty (or possibly non-empty) evidence bindings, -- so that the identity coercion is always exactly WpHole + | WpMultCoercion Coercion + -- Note [Checking multiplicity coercions] + -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + -- This wrapper can be returned from tcSubMult. + -- It is used in case a variable is used with multiplicity m1, + -- we need it with multiplicity m2 and we have a coercion c :: m1 ~ m2. + -- Compiling such code would require multiplicity coercions in Core, + -- which we don't have. If the desugarer sees WpMultCoercion + -- with a non-reflexive coercion, it gives an error. + -- This is a temporary measure, as we don't really know yet exactly + -- what multiplicity coercions should be. But it serves as a good + -- approximation for the first iteration for the first iteration of linear types. -- Cannot derive Data instance because SDoc is not Data (it stores a function). -- So we do it manually: @@ -241,6 +254,7 @@ instance Data.Data HsWrapper where gfoldl k z (WpTyLam a1) = z WpTyLam `k` a1 gfoldl k z (WpTyApp a1) = z WpTyApp `k` a1 gfoldl k z (WpLet a1) = z WpLet `k` a1 + gfoldl k z (WpMultCoercion a1) = z WpMultCoercion `k` a1 gunfold k z c = case Data.constrIndex c of 1 -> z WpHole @@ -251,7 +265,8 @@ instance Data.Data HsWrapper where 6 -> k (z WpEvApp) 7 -> k (z WpTyLam) 8 -> k (z WpTyApp) - _ -> k (z WpLet) + 9 -> k (z WpLet) + _ -> k (z WpMultCoercion) toConstr WpHole = wpHole_constr toConstr (WpCompose _ _) = wpCompose_constr @@ -262,6 +277,7 @@ instance Data.Data HsWrapper where toConstr (WpTyLam _) = wpTyLam_constr toConstr (WpTyApp _) = wpTyApp_constr toConstr (WpLet _) = wpLet_constr + toConstr (WpMultCoercion _) = wpMultCoercion_constr dataTypeOf _ = hsWrapper_dataType @@ -270,10 +286,11 @@ hsWrapper_dataType = Data.mkDataType "HsWrapper" [ wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr , wpEvLam_constr, wpEvApp_constr, wpTyLam_constr, wpTyApp_constr - , wpLet_constr] + , wpLet_constr, wpMultCoercion_constr ] wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr, wpEvLam_constr, - wpEvApp_constr, wpTyLam_constr, wpTyApp_constr, wpLet_constr :: Data.Constr + wpEvApp_constr, wpTyLam_constr, wpTyApp_constr, wpLet_constr, + wpMultCoercion_constr :: Data.Constr wpHole_constr = mkHsWrapperConstr "WpHole" wpCompose_constr = mkHsWrapperConstr "WpCompose" wpFun_constr = mkHsWrapperConstr "WpFun" @@ -283,11 +300,12 @@ wpEvApp_constr = mkHsWrapperConstr "WpEvApp" wpTyLam_constr = mkHsWrapperConstr "WpTyLam" wpTyApp_constr = mkHsWrapperConstr "WpTyApp" wpLet_constr = mkHsWrapperConstr "WpLet" +wpMultCoercion_constr = mkHsWrapperConstr "WpMultCoercion" mkHsWrapperConstr :: String -> Data.Constr mkHsWrapperConstr name = Data.mkConstr hsWrapper_dataType name [] Data.Prefix -wpFunEmpty :: HsWrapper -> HsWrapper -> TcType -> HsWrapper +wpFunEmpty :: HsWrapper -> HsWrapper -> Scaled TcType -> HsWrapper wpFunEmpty c1 c2 t1 = WpFun c1 c2 t1 empty (<.>) :: HsWrapper -> HsWrapper -> HsWrapper @@ -296,15 +314,15 @@ c <.> WpHole = c c1 <.> c2 = c1 `WpCompose` c2 mkWpFun :: HsWrapper -> HsWrapper - -> TcType -- the "from" type of the first wrapper + -> (Scaled TcType) -- the "from" type of the first wrapper -> TcType -- either type of the second wrapper (used only when the -- second wrapper is the identity) -> SDoc -- what caused you to want a WpFun? Something like "When converting ..." -> HsWrapper mkWpFun WpHole WpHole _ _ _ = WpHole -mkWpFun WpHole (WpCast co2) t1 _ _ = WpCast (mkTcFunCo Representational (mkTcRepReflCo t1) co2) -mkWpFun (WpCast co1) WpHole _ t2 _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) (mkTcRepReflCo t2)) -mkWpFun (WpCast co1) (WpCast co2) _ _ _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) co2) +mkWpFun WpHole (WpCast co2) (Scaled w t1) _ _ = WpCast (mkTcFunCo Representational (multToCo w) (mkTcRepReflCo t1) co2) +mkWpFun (WpCast co1) WpHole (Scaled w _) t2 _ = WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) (mkTcRepReflCo t2)) +mkWpFun (WpCast co1) (WpCast co2) (Scaled w _) _ _ = WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) co2) mkWpFun co1 co2 t1 _ d = WpFun co1 co2 t1 d mkWpCastR :: TcCoercionR -> HsWrapper @@ -375,6 +393,7 @@ hsWrapDictBinders wrap = go wrap go (WpTyLam {}) = emptyBag go (WpTyApp {}) = emptyBag go (WpLet {}) = emptyBag + go (WpMultCoercion {}) = emptyBag collectHsWrapBinders :: HsWrapper -> ([Var], HsWrapper) -- Collect the outer lambda binders of a HsWrapper, @@ -608,9 +627,9 @@ data EvTypeable -- ^ Dictionary for @Typeable (s t)@, -- given a dictionaries for @s@ and @t@. - | EvTypeableTrFun EvTerm EvTerm - -- ^ Dictionary for @Typeable (s -> t)@, - -- given a dictionaries for @s@ and @t@. + | EvTypeableTrFun EvTerm EvTerm EvTerm + -- ^ Dictionary for @Typeable (s # w -> t)@, + -- given a dictionaries for @w@, @s@, and @t@. | EvTypeableTyLit EvTerm -- ^ Dictionary for a type literal, @@ -893,10 +912,10 @@ evVarsOfTerms = mapUnionVarSet evVarsOfTerm evVarsOfTypeable :: EvTypeable -> VarSet evVarsOfTypeable ev = case ev of - EvTypeableTyCon _ e -> mapUnionVarSet evVarsOfTerm e - EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2] - EvTypeableTrFun e1 e2 -> evVarsOfTerms [e1,e2] - EvTypeableTyLit e -> evVarsOfTerm e + EvTypeableTyCon _ e -> mapUnionVarSet evVarsOfTerm e + EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2] + EvTypeableTrFun em e1 e2 -> evVarsOfTerms [em,e1,e2] + EvTypeableTyLit e -> evVarsOfTerm e {- Note [Free vars of EvFun] @@ -937,7 +956,7 @@ pprHsWrapper wrap pp_thing_inside -- False <=> appears as body of let or lambda help it WpHole = it help it (WpCompose f1 f2) = help (help it f2) f1 - help it (WpFun f1 f2 t1 _) = add_parens $ text "\\(x" <> dcolon <> ppr t1 <> text ")." <+> + help it (WpFun f1 f2 (Scaled w t1) _) = add_parens $ text "\\(x" <> dcolon <> brackets (ppr w) <> ppr t1 <> text ")." <+> help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False help it (WpCast co) = add_parens $ sep [it False, nest 2 (text "|>" <+> pprParendCo co)] @@ -946,6 +965,8 @@ pprHsWrapper wrap pp_thing_inside help it (WpEvLam id) = add_parens $ sep [ text "\\" <> pprLamBndr id <> dot, it False] help it (WpTyLam tv) = add_parens $ sep [text "/\\" <> pprLamBndr tv <> dot, it False] help it (WpLet binds) = add_parens $ sep [text "let" <+> braces (ppr binds), it False] + help it (WpMultCoercion co) = add_parens $ sep [it False, nest 2 (text "<multiplicity coercion>" + <+> pprParendCo co)] pprLamBndr :: Id -> SDoc pprLamBndr v = pprBndr LambdaBind v @@ -992,7 +1013,7 @@ instance Outputable EvCallStack where instance Outputable EvTypeable where ppr (EvTypeableTyCon ts _) = text "TyCon" <+> ppr ts ppr (EvTypeableTyApp t1 t2) = parens (ppr t1 <+> ppr t2) - ppr (EvTypeableTrFun t1 t2) = parens (ppr t1 <+> arrow <+> ppr t2) + ppr (EvTypeableTrFun tm t1 t2) = parens (ppr t1 <+> mulArrow (ppr tm) <+> ppr t2) ppr (EvTypeableTyLit t1) = text "TyLit" <> ppr t1 diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs index b453633c65..7dfa5ffd65 100644 --- a/compiler/GHC/Tc/Types/Origin.hs +++ b/compiler/GHC/Tc/Types/Origin.hs @@ -34,6 +34,7 @@ import GHC.Core.ConLike import GHC.Core.TyCon import GHC.Core.InstEnv import GHC.Core.PatSyn +import GHC.Core.Multiplicity ( scaledThing ) import GHC.Unit.Module import GHC.Types.Name @@ -285,12 +286,13 @@ pprSigSkolInfo ctxt ty pprPatSkolInfo :: ConLike -> SDoc pprPatSkolInfo (RealDataCon dc) - = sep [ text "a pattern with constructor:" - , nest 2 $ ppr dc <+> dcolon - <+> pprType (dataConUserType dc) <> comma ] - -- pprType prints forall's regardless of -fprint-explicit-foralls - -- which is what we want here, since we might be saying - -- type variable 't' is bound by ... + = sdocWithDynFlags (\dflags -> + sep [ text "a pattern with constructor:" + , nest 2 $ ppr dc <+> dcolon + <+> pprType (dataConDisplayType dflags dc) <> comma ]) + -- pprType prints forall's regardless of -fprint-explicit-foralls + -- which is what we want here, since we might be saying + -- type variable 't' is bound by ... pprPatSkolInfo (PatSynCon ps) = sep [ text "a pattern with pattern synonym:" @@ -444,6 +446,9 @@ data CtOrigin | InstProvidedOrigin Module ClsInst -- Skolem variable arose when we were testing if an instance -- is solvable or not. + | NonLinearPatternOrigin + | UsageEnvironmentOf Name + -- An origin is visible if the place where the constraint arises is manifest -- in user code. Currently, all origins are visible except for invisible -- TypeEqOrigins. This is used when choosing which error of @@ -575,7 +580,7 @@ pprCtOrigin (UnboundOccurrenceOf name) pprCtOrigin (DerivOriginDC dc n _) = hang (ctoHerald <+> text "the" <+> speakNth n <+> text "field of" <+> quotes (ppr dc)) - 2 (parens (text "type" <+> quotes (ppr ty))) + 2 (parens (text "type" <+> quotes (ppr (scaledThing ty)))) where ty = dataConOrigArgTys dc !! (n-1) @@ -650,5 +655,7 @@ pprCtO (TypeHoleOrigin occ) = text "a use of wildcard" <+> quotes (ppr occ) pprCtO PatCheckOrigin = text "a pattern-match completeness check" pprCtO ListOrigin = text "an overloaded list" pprCtO StaticOrigin = text "a static form" +pprCtO NonLinearPatternOrigin = text "a non-linear pattern" +pprCtO (UsageEnvironmentOf x) = hsep [text "multiplicity of", quotes (ppr x)] pprCtO BracketOrigin = text "a quotation bracket" pprCtO _ = panic "pprCtOrigin" 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 diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs index 32dfc16ea3..c9eec9838f 100644 --- a/compiler/GHC/Tc/Validity.hs +++ b/compiler/GHC/Tc/Validity.hs @@ -34,7 +34,7 @@ import GHC.Core.TyCo.FVs import GHC.Core.TyCo.Rep import GHC.Core.TyCo.Ppr import GHC.Tc.Utils.TcType hiding ( sizeType, sizeTypes ) -import GHC.Builtin.Types ( heqTyConName, eqTyConName, coercibleTyConName ) +import GHC.Builtin.Types ( heqTyConName, eqTyConName, coercibleTyConName, manyDataConTy ) import GHC.Builtin.Names import GHC.Core.Type import GHC.Core.Unify ( tcMatchTyX_BM, BindFlag(..) ) @@ -711,7 +711,7 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt (theta, tau) = tcSplitPhiTy phi (env', tvbs') = tidyTyCoVarBinders env tvbs -check_type (ve@ValidityEnv{ve_rank = rank}) (FunTy _ arg_ty res_ty) +check_type (ve@ValidityEnv{ve_rank = rank}) (FunTy _ _ arg_ty res_ty) = do { check_type (ve{ve_rank = arg_rank}) arg_ty ; check_type (ve{ve_rank = res_rank}) res_ty } where @@ -1635,17 +1635,24 @@ tcInstHeadTyNotSynonym :: Type -> Bool tcInstHeadTyNotSynonym ty = case ty of -- Do not use splitTyConApp, -- because that expands synonyms! - TyConApp tc _ -> not (isTypeSynonymTyCon tc) + TyConApp tc _ -> not (isTypeSynonymTyCon tc) || tc == unrestrictedFunTyCon + -- Allow (->), e.g. instance Category (->), + -- even though it's a type synonym for FUN 'Many _ -> True tcInstHeadTyAppAllTyVars :: Type -> Bool -- Used in Haskell-98 mode, for the argument types of an instance head -- These must be a constructor applied to type variable arguments -- or a type-level literal. --- But we allow kind instantiations. +-- But we allow +-- 1) kind instantiations +-- 2) the type (->) = FUN 'Many, even though it's not in this form. tcInstHeadTyAppAllTyVars ty | Just (tc, tys) <- tcSplitTyConApp_maybe (dropCasts ty) - = ok (filterOutInvisibleTypes tc tys) -- avoid kinds + = let tys' = filterOutInvisibleTypes tc tys -- avoid kinds + tys'' | tc == funTyCon, tys_h:tys_t <- tys', tys_h `eqType` manyDataConTy = tys_t + | otherwise = tys' + in ok tys'' | LitTy _ <- ty = True -- accept type literals (#13833) | otherwise = False @@ -1663,7 +1670,7 @@ dropCasts :: Type -> Type -- To consider: drop only HoleCo casts dropCasts (CastTy ty _) = dropCasts ty dropCasts (AppTy t1 t2) = mkAppTy (dropCasts t1) (dropCasts t2) -dropCasts ty@(FunTy _ t1 t2) = ty { ft_arg = dropCasts t1, ft_res = dropCasts t2 } +dropCasts ty@(FunTy _ w t1 t2) = ty { ft_mult = dropCasts w, ft_arg = dropCasts t1, ft_res = dropCasts t2 } dropCasts (TyConApp tc tys) = mkTyConApp tc (map dropCasts tys) dropCasts (ForAllTy b ty) = ForAllTy (dropCastsB b) (dropCasts ty) dropCasts ty = ty -- LitTy, TyVarTy, CoercionTy @@ -2831,7 +2838,7 @@ fvType (TyVarTy tv) = [tv] fvType (TyConApp _ tys) = fvTypes tys fvType (LitTy {}) = [] fvType (AppTy fun arg) = fvType fun ++ fvType arg -fvType (FunTy _ arg res) = fvType arg ++ fvType res +fvType (FunTy _ w arg res) = fvType w ++ fvType arg ++ fvType res fvType (ForAllTy (Bndr tv _) ty) = fvType (tyVarKind tv) ++ filter (/= tv) (fvType ty) @@ -2848,7 +2855,7 @@ sizeType (TyVarTy {}) = 1 sizeType (TyConApp tc tys) = 1 + sizeTyConAppArgs tc tys sizeType (LitTy {}) = 1 sizeType (AppTy fun arg) = sizeType fun + sizeType arg -sizeType (FunTy _ arg res) = sizeType arg + sizeType res + 1 +sizeType (FunTy _ w arg res) = sizeType w + sizeType arg + sizeType res + 1 sizeType (ForAllTy _ ty) = sizeType ty sizeType (CastTy ty _) = sizeType ty sizeType (CoercionTy _) = 0 |