Simon Peyton Jones pushed to branch wip/T27078 at Glasgow Haskell Compiler / GHC Commits: 28e0ef3c by Simon Peyton Jones at 2026-04-02T00:09:09+01:00 Delete the substition stuff in Lint - - - - - 1 changed file: - compiler/GHC/Core/Lint.hs Changes: ===================================== compiler/GHC/Core/Lint.hs ===================================== @@ -179,65 +179,7 @@ Note [Linting function types] All saturated applications of funTyCon are represented with the FunTy constructor. See Note [Function type constructors and FunTy] in GHC.Builtin.Types.Prim - We check this invariant in lintType. - -Note [Linting type lets] -~~~~~~~~~~~~~~~~~~~~~~~~ -In the desugarer, it's very very convenient to be able to say (in effect) - let a = Type Bool in - let x::a = True in <body> -That is, use a type let. See Note [Core type and coercion invariant] in "GHC.Core". -One place it is used is in mkWwBodies; see Note [Join points and beta-redexes] -in GHC.Core.Opt.WorkWrap.Utils. (Maybe there are other "clients" of this feature; I'm not sure). - -* Hence when linting <body> we need to remember that a=Int, else we - might reject a correct program. So we carry a type substitution (in - this example [a -> Bool]) and apply this substitution before - comparing types. In effect, in Lint, type equality is always - equality-modulo-le-subst. This is in the le_subst field of - LintEnv. But nota bene: - - (SI1) The le_subst substitution is applied to types and coercions only - - (SI2) The result of that substitution is used only to check for type - equality, to check well-typed-ness, /but is then discarded/. - The result of substitution does not outlive the CoreLint pass. - - (SI3) The InScopeSet of le_subst includes only TyVar and CoVar binders. - -* The function - lintInTy :: Type -> LintM (Type, Kind) - returns a substituted type. - -* When we encounter a binder (like x::a) we must apply the substitution - to the type of the binding variable. lintBinders does this. - -* Clearly we need to clone tyvar binders as we go. - -* But take care (#17590)! We must also clone CoVar binders: - let a = TYPE (ty |> cv) - in \cv -> blah - blindly substituting for `a` might capture `cv`. - -* Alas, when cloning a coercion variable we might choose a unique - that happens to clash with an inner Id, thus - \cv_66 -> let wild_X7 = blah in blah - We decide to clone `cv_66` because it's already in scope. Fine, - choose a new unique. Aha, X7 looks good. So we check the lambda - body with le_subst of [cv_66 :-> cv_X7] - - This is all fine, even though we use the same unique as wild_X7. - As (SI2) says, we do /not/ return a new lambda - (\cv_X7 -> let wild_X7 = blah in ...) - We simply use the le_subst substitution in types/coercions only, when - checking for equality. - -* We still need to check that Id occurrences are bound by some - enclosing binding. We do /not/ use the InScopeSet for the le_subst - for this purpose -- it contains only TyCoVars. Instead we have a separate - le_ids for the in-scope Id binders. - -Sigh. We might want to explore getting rid of type-let! +We check this invariant in lintType. Note [Bad unsafe coercion] ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -564,11 +506,11 @@ Check a core binding, returning the list of variables bound. -- Let lintRecBindings :: TopLevelFlag -> [(Id, CoreExpr)] - -> ([OutId] -> LintM a) -> LintM (a, [UsageEnv]) + -> LintM a -> LintM (a, [UsageEnv]) lintRecBindings top_lvl pairs thing_inside - = lintIdBndrs top_lvl bndrs $ \ bndrs' -> - do { ues <- zipWithM lint_pair bndrs' rhss - ; a <- thing_inside bndrs' + = lintIdBndrs top_lvl bndrs $ + do { ues <- zipWithM lint_pair bndrs rhss + ; a <- thing_inside ; return (a, ues) } where (bndrs, rhss) = unzip pairs @@ -578,14 +520,14 @@ lintRecBindings top_lvl pairs thing_inside ; lintLetBind top_lvl Recursive bndr' rhs rhs_ty ; return ue } -lintLetBody :: LintLocInfo -> [OutId] -> CoreExpr -> LintM (OutType, UsageEnv) +lintLetBody :: LintLocInfo -> [Id] -> CoreExpr -> LintM (Type, UsageEnv) lintLetBody loc bndrs body = do { (body_ty, body_ue) <- addLoc loc (lintCoreExpr body) ; mapM_ (lintJoinBndrType body_ty) bndrs ; return (body_ty, body_ue) } -lintLetBind :: TopLevelFlag -> RecFlag -> OutId - -> CoreExpr -> OutType -> LintM () +lintLetBind :: TopLevelFlag -> RecFlag -> Id + -> CoreExpr -> Type -> LintM () -- Binder's type, and the RHS, have already been linted -- This function checks other invariants lintLetBind top_lvl rec_flag binder rhs rhs_ty @@ -676,7 +618,7 @@ lintLetBind top_lvl rec_flag binder rhs rhs_ty -- join point. -- -- See Note [Checking StaticPtrs]. -lintRhs :: Id -> CoreExpr -> LintM (OutType, UsageEnv) +lintRhs :: Id -> CoreExpr -> LintM (Type, UsageEnv) -- NB: the Id can be Linted or not -- it's only used for -- its OccInfo and join-pointer-hood lintRhs bndr rhs @@ -691,7 +633,7 @@ lintRhs _bndr rhs = fmap lf_check_static_ptrs getLintFlags >>= go where -- Allow occurrences of 'makeStatic' at the top-level but produce errors -- otherwise. - go :: StaticPtrCheck -> LintM (OutType, UsageEnv) + go :: StaticPtrCheck -> LintM (Type, UsageEnv) go AllowAtTopLevel | (binders0, rhs') <- collectTyBinders rhs , Just (fun, t, info, e) <- collectMakeStaticArgs rhs' @@ -708,7 +650,7 @@ lintRhs _bndr rhs = fmap lf_check_static_ptrs getLintFlags >>= go -- | Lint the RHS of a join point with expected join arity of @n@ (see Note -- [Join points] in "GHC.Core"). -lintJoinLams :: JoinArity -> Maybe Id -> CoreExpr -> LintM (OutType, UsageEnv) +lintJoinLams :: JoinArity -> Maybe Id -> CoreExpr -> LintM (Type, UsageEnv) lintJoinLams join_arity enforce rhs = go join_arity rhs where @@ -896,13 +838,8 @@ suspicious and worth investigating if you have a seg-fault or bizarre behaviour. ************************************************************************ -} -lintCoreExpr :: InExpr -> LintM (OutType, UsageEnv) --- The returned type has the substitution from the monad --- already applied to it: --- lintCoreExpr e subst = exprType (subst e) --- --- The returned "type" can be a kind, if the expression is (Type ty) - +lintCoreExpr :: CoreExpr -> LintM (Type, UsageEnv) +-- The returned type is the type of the expression -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] @@ -929,7 +866,7 @@ lintCoreExpr (Cast expr co) ; lintCoercion co ; lintRole co Representational (coercionRole co) - ; Pair from_ty to_ty <- substCoKindM co + ; let Pair from_ty to_ty = coercionKind co ; checkValueType (typeKind to_ty) $ text "target of cast" <+> quotes (ppr co) ; ensureEqTys from_ty expr_ty (mkCastErr expr co from_ty expr_ty) @@ -944,13 +881,12 @@ lintCoreExpr (Tick tickish expr) lintCoreExpr (Let (NonRec tv (Type ty)) body) | isTyVar tv = -- See Note [Linting type lets] - do { ty' <- lintTypeAndSubst ty - ; lintTyCoBndr tv $ \ tv' -> - do { addLoc (RhsOf tv) $ lintTyKind tv' ty' + do { lintType ty + ; lintTyCoBndr tv $ + do { addLoc (RhsOf tv) $ lintTyKind tv ty -- Now extend the substitution so we -- take advantage of it in the body - ; -- extendTvSubstL tv ty' $ - addLoc (BodyOfLet tv) $ + ; addLoc (BodyOfLet tv) $ lintCoreExpr body } } lintCoreExpr (Let (NonRec bndr rhs) body) @@ -960,10 +896,10 @@ lintCoreExpr (Let (NonRec bndr rhs) body) -- See Note [Multiplicity of let binders] in Var -- Now lint the binder - ; lintBinder LetBind bndr $ \bndr' -> - do { lintLetBind NotTopLevel NonRecursive bndr' rhs rhs_ty - ; addAliasUE bndr' let_ue $ - lintLetBody (BodyOfLet bndr') [bndr'] body } } + ; lintBinder LetBind bndr $ + do { lintLetBind NotTopLevel NonRecursive bndr rhs rhs_ty + ; addAliasUE bndr let_ue $ + lintLetBody (BodyOfLet bndr) [bndr] body } } | otherwise = failWithL (mkLetErr bndr rhs) -- Not quite accurate @@ -982,8 +918,8 @@ lintCoreExpr e@(Let (Rec pairs) body) -- See Note [Multiplicity of let binders] in Var ; ((body_type, body_ue), ues) <- - lintRecBindings NotTopLevel pairs $ \ bndrs' -> - lintLetBody (BodyOfLetRec bndrs') bndrs' body + lintRecBindings NotTopLevel pairs $ + lintLetBody (BodyOfLetRec bndrs) bndrs body ; return (body_type, body_ue `addUE` scaleUE ManyTy (foldr1WithDefault zeroUE addUE ues)) } where bndrs = map fst pairs @@ -995,7 +931,7 @@ lintCoreExpr e@(App _ _) -- N.B. we may have an over-saturated application of the form: -- runRW (\s -> \x -> ...) y , ty_arg1 : ty_arg2 : cont_arg : rest <- args - = do { let lint_rw_cont :: CoreArg -> Mult -> UsageEnv -> LintM (OutType, UsageEnv) + = do { let lint_rw_cont :: CoreArg -> Mult -> UsageEnv -> LintM (Type, UsageEnv) lint_rw_cont expr@(Lam _ _) mult fun_ue = do { (arg_ty, arg_ue) <- lintJoinLams 1 (Just fun) expr ; let app_ue = addUE fun_ue (scaleUE mult arg_ue) @@ -1045,53 +981,42 @@ lintCoreExpr (Type ty) lintCoreExpr (Coercion co) -- See Note [Coercions in terms] = do { addLoc (InCo co) $ lintCoercion co - ; ty <- substTyM (coercionType co) + ; let ty = coercionType co ; return (ty, zeroUE) } ---------------------- -lintIdOcc :: InId -> Int -- Number of arguments (type or value) being passed - -> LintM (OutType, UsageEnv) -- returns type of the *variable* -lintIdOcc in_id nargs - = addLoc (OccOf in_id) $ - do { checkL (isNonCoVarId in_id) - (text "Non term variable" <+> ppr in_id) +lintIdOcc :: Id -> Int -- Number of arguments (type or value) being passed + -> LintM (Type, UsageEnv) -- returns type of the *variable* +lintIdOcc id nargs + = addLoc (OccOf id) $ + do { checkL (isNonCoVarId id) + (text "Non term variable" <+> ppr id) -- See GHC.Core Note [Variable occurrences in Core] - -- Check that the type of the occurrence is the same - -- as the type of the binding site. The inScopeIds are - -- /un-substituted/, so this checks that the occurrence type - -- is identical to the binder type. - -- This makes things much easier for things like: - -- /\a. \(x::Maybe a). /\a. ...(x::Maybe a)... - -- The "::Maybe a" on the occurrence is referring to the /outer/ a. - -- If we compared /substituted/ types we'd risk comparing - -- (Maybe a) from the binding site with bogus (Maybe a1) from - -- the occurrence site. Comparing un-substituted types finesses - -- this altogether - ; out_ty <- lintVarOcc in_id + ; lintVarOcc id -- Check for a nested occurrence of the StaticPtr constructor. -- See Note [Checking StaticPtrs]. ; when (nargs /= 0) $ - checkL (idName in_id /= makeStaticName) $ + checkL (idName id /= makeStaticName) $ text "Found makeStatic nested in an expression" - ; checkDeadIdOcc in_id + ; checkDeadIdOcc id - ; case isDataConId_maybe in_id of + ; case isDataConId_maybe id of Nothing -> return () Just dc -> checkTypeDataConOcc "expression" dc - ; checkJoinOcc in_id nargs - ; usage <- varCallSiteUsage in_id + ; checkJoinOcc id nargs + ; usage <- varCallSiteUsage id - ; return (out_ty, usage) } + ; return (idType id, usage) } lintCoreFun :: CoreExpr -> Int -- Number of arguments (type or val) being passed - -> LintM (OutType, UsageEnv) -- Returns type of the *function* + -> LintM (Type, UsageEnv) -- Returns type of the *function* lintCoreFun (Var var) nargs = lintIdOcc var nargs @@ -1109,10 +1034,10 @@ lintCoreFun expr nargs lintLambda :: Var -> LintM (Type, UsageEnv) -> LintM (Type, UsageEnv) lintLambda var lintBody = addLoc (LambdaBodyOf var) $ - lintBinder LambdaBind var $ \ var' -> + lintBinder LambdaBind var $ do { (body_ty, ue) <- lintBody - ; ue' <- checkLinearity ue var' - ; return (mkLamType var' body_ty, ue') } + ; ue' <- checkLinearity ue var + ; return (mkLamType var body_ty, ue') } ------------------ checkDeadIdOcc :: Id -> LintM () -- Occurrences of an Id should never be dead.... @@ -1126,8 +1051,8 @@ checkDeadIdOcc id = return () ------------------ -lintJoinBndrType :: OutType -- Type of the body - -> OutId -- Possibly a join Id +lintJoinBndrType :: Type -- Type of the body + -> Id -- Possibly a join Id -> LintM () -- Checks that the return type of a join Id matches the body -- E.g. join j x = rhs in body @@ -1458,23 +1383,24 @@ subtype of the required type, as one would expect. -- Takes the functions type and arguments as argument. -- Returns the *result* of applying the function to arguments. -- e.g. f :: Int -> Bool -> Int would return `Int` as result type. -lintCoreArgs :: (OutType, UsageEnv) -> [InExpr] -> LintM (OutType, UsageEnv) +lintCoreArgs :: (Type, UsageEnv) -> [CoreExpr] -> LintM (Type, UsageEnv) lintCoreArgs (fun_ty, fun_ue) args = lintApp (text "expression") lintTyArg lintValArg fun_ty args fun_ue -lintTyArg :: InExpr -> LintM OutType +lintTyArg :: CoreExpr -> LintM Type -- Type argument lintTyArg (Type arg_ty) = do { checkL (not (isCoercionTy arg_ty)) (text "Unnecessary coercion-to-type injection:" <+> ppr arg_ty) - ; lintTypeAndSubst arg_ty } + ; lintType arg_ty + ; return arg_ty } lintTyArg arg = failWithL (hang (text "Expected type argument but found") 2 (ppr arg)) -lintValArg :: InExpr -> Mult -> UsageEnv -> LintM (OutType, UsageEnv) +lintValArg :: CoreExpr -> Mult -> UsageEnv -> LintM (Type, UsageEnv) lintValArg arg mult fun_ue = do { (arg_ty, arg_ue) <- markAllJoinsBad $ lintCoreExpr arg -- See Note [Representation polymorphism invariants] in GHC.Core @@ -1494,8 +1420,8 @@ lintValArg arg mult fun_ue ----------------- lintAltBinders :: UsageEnv -> Var -- Case binder - -> OutType -- Scrutinee type - -> OutType -- Constructor type + -> Type -- Scrutinee type + -> Type -- Constructor type -> [(Mult, OutVar)] -- Binders -> LintM UsageEnv -- If you edit this function, you may need to update the GHC formalism @@ -1545,7 +1471,7 @@ checkCaseLinearity ue case_bndr var_w bndr = do ----------------- -lintTyApp :: OutType -> OutType -> LintM OutType +lintTyApp :: Type -> Type -> LintM Type lintTyApp fun_ty arg_ty | Just (tv,body_ty) <- splitForAllTyVar_maybe fun_ty = do { lintTyKind tv arg_ty @@ -1563,8 +1489,8 @@ lintTyApp fun_ty arg_ty -- | @lintValApp arg fun_ty arg_ty@ lints an application of @fun arg@ -- where @fun :: fun_ty@ and @arg :: arg_ty@, returning the type of the -- application. -lintValApp :: CoreExpr -> OutType -> OutType -> UsageEnv -> UsageEnv - -> LintM (OutType, UsageEnv) +lintValApp :: CoreExpr -> Type -> Type -> UsageEnv -> UsageEnv + -> LintM (Type, UsageEnv) lintValApp arg fun_ty arg_ty fun_ue arg_ue | Just (_, w, arg_ty', res_ty') <- splitFunTy_maybe fun_ty = do { ensureEqTys arg_ty' arg_ty (mkAppMsg arg_ty' arg_ty arg) @@ -1575,7 +1501,7 @@ lintValApp arg fun_ty arg_ty fun_ue arg_ue where err2 = mkNonFunAppMsg fun_ty arg_ty arg -lintTyKind :: OutTyVar -> OutType -> LintM () +lintTyKind :: OutTyVar -> Type -> LintM () -- Both args have had substitution applied -- If you edit this function, you may need to update the GHC formalism @@ -1595,36 +1521,36 @@ lintTyKind tyvar arg_ty ************************************************************************ -} -lintCaseExpr :: CoreExpr -> InId -> InType -> [CoreAlt] -> LintM (OutType, UsageEnv) +lintCaseExpr :: CoreExpr -> Id -> Type -> [CoreAlt] -> LintM (Type, UsageEnv) lintCaseExpr scrut case_bndr alt_ty alts = do { let e = Case scrut case_bndr alt_ty alts -- Just for error messages -- Check the scrutinee - ; (scrut_ty', scrut_ue) <- markAllJoinsBad $ lintCoreExpr scrut + ; (scrut_ty, scrut_ue) <- markAllJoinsBad $ lintCoreExpr scrut -- See Note [Join points are less general than the paper] -- in GHC.Core - ; alt_ty' <- addLoc (CaseTy scrut) $ lintValueType alt_ty + ; addLoc (CaseTy scrut) $ lintValueType alt_ty - ; checkCaseAlts e scrut scrut_ty' alts + ; checkCaseAlts e scrut scrut_ty alts -- Lint the case-binder. Must do this after linting the scrutinee -- because the case-binder isn't in scope in the scrutineex - ; lintBinder CaseBind case_bndr $ \case_bndr' -> + ; lintBinder CaseBind case_bndr $ -- Don't use lintIdBndr on case_bndr, because unboxed tuple is legitimate - do { let case_bndr_ty' = idType case_bndr' - scrut_mult = idMult case_bndr' + do { let case_bndr_ty = idType case_bndr + scrut_mult = idMult case_bndr - ; ensureEqTys case_bndr_ty' scrut_ty' (mkScrutMsg case_bndr case_bndr_ty' scrut_ty') + ; ensureEqTys case_bndr_ty scrut_ty (mkScrutMsg case_bndr case_bndr_ty scrut_ty) -- See GHC.Core Note [Case expression invariants] item (7) ; -- Check the alternatives - ; alt_ues <- mapM (lintCoreAlt case_bndr' scrut_ty' scrut_mult alt_ty') alts + ; alt_ues <- mapM (lintCoreAlt case_bndr scrut_ty scrut_mult alt_ty) alts ; let case_ue = (scaleUE scrut_mult scrut_ue) `addUE` supUEs alt_ues - ; return (alt_ty', case_ue) } } + ; return (alt_ty, case_ue) } } -checkCaseAlts :: InExpr -> InExpr -> OutType -> [CoreAlt] -> LintM () +checkCaseAlts :: CoreExpr -> CoreExpr -> Type -> [CoreAlt] -> LintM () -- a) Check that the alts are non-empty -- b1) Check that the DEFAULT comes first, if it exists -- b2) Check that the others are in increasing order @@ -1699,17 +1625,17 @@ checkCaseAlts e scrut scrut_ty alts is_lit_alt (Alt (LitAlt _) _ _) = True is_lit_alt _ = False -lintAltExpr :: CoreExpr -> OutType -> LintM UsageEnv +lintAltExpr :: CoreExpr -> Type -> LintM UsageEnv lintAltExpr expr ann_ty = do { (actual_ty, ue) <- lintCoreExpr expr ; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) ; return ue } -- See GHC.Core Note [Case expression invariants] item (6) -lintCoreAlt :: OutId -- Case binder - -> OutType -- Type of scrutinee +lintCoreAlt :: Id -- Case binder + -> Type -- Type of scrutinee -> Mult -- Multiplicity of scrutinee - -> OutType -- Type of the alternative + -> Type -- Type of the alternative -> CoreAlt -> LintM UsageEnv -- If you edit this function, you may need to update the GHC formalism @@ -1754,11 +1680,11 @@ lintCoreAlt case_bndr scrut_ty _scrut_mult alt_ty alt@(Alt (DataAlt con) args rh ; multiplicities = map binderMult $ fst $ splitPiTys con_payload_ty } -- And now bring the new binders into scope - ; lintBinders CasePatBind args $ \ args' -> do + ; lintBinders CasePatBind args $ do { rhs_ue <- lintAltExpr rhs alt_ty ; rhs_ue' <- addLoc (CasePat alt) $ lintAltBinders rhs_ue case_bndr scrut_ty con_payload_ty - (zipEqual multiplicities args') + (zipEqual multiplicities args) ; return $ deleteUE rhs_ue' case_bndr } } @@ -1803,49 +1729,50 @@ lintLinearBinder doc actual_usage described_usage -- 1. Lint var types or kinds (possibly substituting) -- 2. Add the binder to the in scope set, and if its a coercion var, -- we may extend the substitution to reflect its (possibly) new kind -lintBinders :: HasDebugCallStack => BindingSite -> [InVar] -> ([OutVar] -> LintM a) -> LintM a -lintBinders _ [] linterF = linterF [] -lintBinders site (var:vars) linterF = lintBinder site var $ \var' -> - lintBinders site vars $ \ vars' -> - linterF (var':vars') +lintBinders :: HasDebugCallStack => BindingSite -> [Var] -> LintM a -> LintM a +lintBinders _ [] linterF = linterF +lintBinders site (var:vars) linterF = lintBinder site var $ + lintBinders site vars $ + linterF -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] -lintBinder :: HasDebugCallStack => BindingSite -> InVar -> (OutVar -> LintM a) -> LintM a +lintBinder :: HasDebugCallStack => BindingSite -> Var -> LintM a -> LintM a lintBinder site var linterF | isTyCoVar var = lintTyCoBndr var linterF | otherwise = lintIdBndr NotTopLevel site var linterF -lintTyCoBndr :: HasDebugCallStack => TyCoVar -> (OutTyCoVar -> LintM a) -> LintM a +lintTyCoBndr :: HasDebugCallStack => TyCoVar -> LintM a -> LintM a lintTyCoBndr tcv thing_inside - = do { tcv_type' <- lintTypeAndSubst (varType tcv) - ; let tcv_kind' = typeKind tcv_type' + = do { let tcv_type = varType tcv + tcv_kind = typeKind tcv_type + ; lintType (varType tcv) -- See (FORALL1) and (FORALL2) in GHC.Core.Type ; if (isTyVar tcv) then -- Check that in (forall (a:ki). blah) we have ki:Type - lintL (isLiftedTypeKind tcv_kind') $ + lintL (isLiftedTypeKind tcv_kind) $ hang (text "TyVar whose kind does not have kind Type:") - 2 (ppr tcv <+> dcolon <+> ppr tcv_type' <+> dcolon <+> ppr tcv_kind') + 2 (ppr tcv <+> dcolon <+> ppr tcv_type <+> dcolon <+> ppr tcv_kind) else -- Check that in (forall (cv::ty). blah), -- then ty looks like (t1 ~# t2) - lintL (isCoVarType tcv_type') $ + lintL (isCoVarType tcv_type) $ text "CoVar with non-coercion type:" <+> pprTyVar tcv - ; addInScopeTyCoVar tcv tcv_type' thing_inside } + ; addInScopeTyCoVar tcv thing_inside } -lintIdBndrs :: forall a. TopLevelFlag -> [InId] -> ([OutId] -> LintM a) -> LintM a +lintIdBndrs :: forall a. TopLevelFlag -> [Id] -> LintM a -> LintM a lintIdBndrs top_lvl ids thing_inside = go ids thing_inside where - go :: [Id] -> ([Id] -> LintM a) -> LintM a - go [] thing_inside = thing_inside [] - go (id:ids) thing_inside = lintIdBndr top_lvl LetBind id $ \id' -> - go ids $ \ids' -> - thing_inside (id' : ids') + go :: [Id] -> LintM a -> LintM a + go [] thing_inside = thing_inside + go (id:ids) thing_inside = lintIdBndr top_lvl LetBind id $ + go ids $ + thing_inside lintIdBndr :: TopLevelFlag -> BindingSite - -> InVar -> (OutVar -> LintM a) -> LintM a + -> Var -> LintM a -> LintM a -- Do substitution on the type of a binder and add the var with this -- new type to the in-scope set of the second argument -- ToDo: lint its rules @@ -1885,9 +1812,9 @@ lintIdBndr top_lvl bind_site id thing_inside ; lintL (not (bind_site == LambdaBind && isEvaldUnfolding (idUnfolding id))) (text "Lambda binder with value or OtherCon unfolding.") - ; out_ty <- addLoc (IdTy id) (lintValueType id_ty) + ; addLoc (IdTy id) (lintValueType id_ty) - ; addInScopeId id out_ty thing_inside } + ; addInScopeId id thing_inside } where id_ty = idType id @@ -1907,8 +1834,8 @@ lintIdBndr top_lvl bind_site id thing_inside {- Note [Linting types and coercions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Notice that - lintType :: InType -> LintM () - lintCoercion :: InCoercion -> LintM () + lintType :: Type -> LintM () + lintCoercion :: Coercion -> LintM () Neither returns anything. If you need the kind of the type, then do `typeKind` and then apply @@ -1921,48 +1848,41 @@ and then take the kind, becaues the kind is usually smaller. Note: you might wonder if we should apply the same logic to expressions. Why do we have - lintExpr :: InExpr -> LintM OutType + lintExpr :: CoreExpr -> LintM Type Partly inertia; but also taking the type of an expresison involve looking down a deep chain of let's, whereas that is not true of taking the kind of a type. It'd be worth an experiment though. Historical note: in the olden days we had - lintType :: InType -> LintM OutType -but that burned a huge amount of allocation building an OutType that was + lintType :: Type -> LintM Type +but that burned a huge amount of allocation building an Type that was often discarded, or used only to get its kind. I also experimented with - lintType :: InType -> LintM OutKind + lintType :: Type -> LintM Kind but that too was slower. It is also much simpler to return ()! If we return the kind we have to duplicate the logic in `typeKind`; and it is much worse for coercions. -} -lintValueType :: Type -> LintM OutType +lintValueType :: Type -> LintM () -- Types only, not kinds -- Check the type, and apply the substitution to it -- See Note [Linting type lets] lintValueType ty = addLoc (InType ty) $ - do { ty' <- lintTypeAndSubst ty - ; let sk = typeKind ty' + do { lintType ty + ; let sk = typeKind ty ; lintL (isTYPEorCONSTRAINT sk) $ hang (text "Ill-kinded type:" <+> ppr ty) - 2 (text "has kind:" <+> ppr sk) - ; return ty' } + 2 (text "has kind:" <+> ppr sk)} checkTyCon :: TyCon -> LintM () checkTyCon tc = checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc) ------------------- -lintTypeAndSubst :: InType -> LintM OutType -lintTypeAndSubst ty = do { lintType ty; substTyM ty } - -- In GHCi we may lint an expression with a free - -- type variable. Then it won't be in the - -- substitution, but it should be in scope - -lintType :: InType -> LintM () +lintType :: Type -> LintM () -- See Note [Linting types and coercions] -- -- If you edit this function, you may need to update the GHC formalism @@ -1972,8 +1892,7 @@ lintType (TyVarTy tv) = failWithL (mkBadTyVarMsg tv) | otherwise - = do { _ <- lintVarOcc tv - ; return () } + = lintVarOcc tv lintType ty@(AppTy t1 t2) | TyConApp {} <- t1 @@ -1981,7 +1900,7 @@ lintType ty@(AppTy t1 t2) | otherwise = do { let (fun_ty, arg_tys) = collect t1 [t2] ; lintType fun_ty - ; fun_kind <- substTyM (typeKind fun_ty) + ; let fun_kind = typeKind fun_ty ; lint_ty_app ty fun_kind arg_tys } where collect (AppTy f a) as = collect f (a:as) @@ -2013,21 +1932,21 @@ lintType ty@(FunTy af tw t1 t2) lintType ty@(ForAllTy {}) = go [] ty where - go :: [OutTyCoVar] -> InType -> LintM () + go :: [OutTyCoVar] -> Type -> LintM () -- Loop, collecting the forall-binders go tcvs ty@(ForAllTy (Bndr tcv _) body_ty) | not (isTyCoVar tcv) = failWithL (text "Non-TyVar or Non-CoVar bound in type:" <+> ppr ty) | otherwise - = lintTyCoBndr tcv $ \tcv' -> + = lintTyCoBndr tcv $ do { -- See GHC.Core.TyCo.Rep Note [Unused coercion variable in ForAllTy] -- Suspicious because it works on InTyCoVar; c.f. ForAllCo when (isCoVar tcv) $ lintL (anyFreeVarsOfType (== tcv) body_ty) $ text "Covar does not occur in the body:" <+> (ppr tcv $$ ppr body_ty) - ; go (tcv' : tcvs) body_ty } + ; go (tcv : tcvs) body_ty } go tcvs body_ty = do { lintType body_ty @@ -2035,7 +1954,7 @@ lintType ty@(ForAllTy {}) lintType (CastTy ty co) = do { lintType ty - ; ty_kind <- substTyM (typeKind ty) + ; let ty_kind = typeKind ty ; co_lk <- lintStarCoercion co ; ensureEqTys ty_kind co_lk (mkCastTyErr ty co ty_kind co_lk) } @@ -2043,14 +1962,14 @@ lintType (LitTy l) = lintTyLit l lintType (CoercionTy co) = lintCoercion co ----------------- -lintForAllBody :: [OutTyCoVar] -> InType -> LintM () +lintForAllBody :: [OutTyCoVar] -> Type -> LintM () -- Do the checks for the body of a forall-type lintForAllBody tcvs body_ty = do { -- For type variables, check for skolem escape -- See Note [Phantom type variables in kinds] in GHC.Core.Type -- The kind of (forall cv. th) is liftedTypeKind, so no -- need to check for skolem-escape in the CoVar case - body_kind <- substTyM (typeKind body_ty) + let body_kind = typeKind body_ty ; case occCheckExpand tcvs body_kind of Just {} -> return () Nothing -> failWithL $ @@ -2061,7 +1980,7 @@ lintForAllBody tcvs body_ty ; checkValueType body_kind (text "the body of forall:" <+> ppr body_ty) } ----------------- -lintTySynFamApp :: Bool -> InType -> TyCon -> [InType] -> LintM () +lintTySynFamApp :: Bool -> Type -> TyCon -> [Type] -> LintM () -- The TyCon is a type synonym or a type family (not a data family) -- See Note [Linting type synonym applications] -- c.f. GHC.Tc.Validity.check_syn_tc_app @@ -2087,21 +2006,21 @@ lintTySynFamApp report_unsat ty tc tys ----------------- -- Confirms that a kind is really TYPE r or Constraint -checkValueType :: OutKind -> SDoc -> LintM () +checkValueType :: Kind -> SDoc -> LintM () checkValueType kind doc = lintL (isTYPEorCONSTRAINT kind) (text "Non-Type-like kind when Type-like expected:" <+> ppr kind $$ text "when checking" <+> doc) ----------------- -lintArrow :: SDoc -> FunTyFlag -> InType -> InType -> InType -> LintM () +lintArrow :: SDoc -> FunTyFlag -> Type -> Type -> Type -> LintM () -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] lintArrow what af t1 t2 tw -- Eg lintArrow "type or kind `blah'" k1 k2 kw -- or lintArrow "coercion `blah'" k1 k2 kw - = do { k1 <- substTyM (typeKind t1) - ; k2 <- substTyM (typeKind t2) - ; kw <- substTyM (typeKind tw) + = do { let k1 = typeKind t1 + k2 = typeKind t2 + kw = typeKind tw ; unless (isTYPEorCONSTRAINT k1) (report (text "argument") t1 k1) ; unless (isTYPEorCONSTRAINT k2) (report (text "result") t2 k2) ; unless (isMultiplicityTy kw) (report (text "multiplicity") tw kw) @@ -2127,29 +2046,29 @@ lintTyLit (StrTyLit _) = return () lintTyLit (CharTyLit _) = return () ----------------- -lint_ty_app :: InType -> OutKind -> [InType] -> LintM () +lint_ty_app :: Type -> Kind -> [Type] -> LintM () lint_ty_app ty = lint_tyco_app (text "type" <+> quotes (ppr ty)) -lint_co_app :: HasDebugCallStack => Coercion -> OutKind -> [InType] -> LintM () +lint_co_app :: HasDebugCallStack => Coercion -> Kind -> [Type] -> LintM () lint_co_app co = lint_tyco_app (text "coercion" <+> quotes (ppr co)) -lint_tyco_app :: SDoc -> OutKind -> [InType] -> LintM () +lint_tyco_app :: SDoc -> Kind -> [Type] -> LintM () lint_tyco_app msg fun_kind arg_tys -- See Note [Avoiding compiler perf traps when constructing error messages.] - = do { _ <- lintApp msg (\ty -> do { lintType ty; substTyM ty }) - (\ty _ _ -> do { lintType ty; ki <- substTyM (typeKind ty); return (ki,()) }) - fun_kind arg_tys () + = do { _ <- lintApp msg (\ty -> do { lintType ty; return ty }) + (\ty _ _ -> do { lintType ty; return (typeKind ty,()) }) + fun_kind arg_tys () ; return () } ---------------- lintApp :: forall in_a acc. Outputable in_a => SDoc - -> (in_a -> LintM OutType) -- Lint the thing and return its value - -> (in_a -> Mult -> acc -> LintM (OutKind, acc)) -- Lint the thing and return its type - -> OutType + -> (in_a -> LintM Type) -- Lint the thing and return its value + -> (in_a -> Mult -> acc -> LintM (Kind, acc)) -- Lint the thing and return its type + -> Type -> [in_a] -- The arguments, always "In" things -> acc -- Used (only) for UsageEnv in /term/ applications - -> LintM (OutType,acc) + -> LintM (Type,acc) -- lintApp is a performance-critical function, which deals with multiple -- applications such as (/\a./\b./\c. expr) @ta @tb @tc -- When returning the type of this expression we want to avoid substituting a:=ta, @@ -2174,7 +2093,7 @@ lintApp msg lint_forall_arg lint_arrow_arg !orig_fun_ty all_args acc ; let init_subst = mkEmptySubst in_scope - go :: Subst -> OutType -> acc -> [in_a] -> LintM (OutType, acc) + go :: Subst -> Type -> acc -> [in_a] -> LintM (Type, acc) -- The Subst applies (only) to the fun_ty -- c.f. GHC.Core.Type.piResultTys, which has a similar loop @@ -2218,7 +2137,7 @@ lintApp msg lint_forall_arg lint_arrow_arg !orig_fun_ty all_args acc -- explicitly and don't capture them as free variables. Otherwise this binder might -- become a thunk that get's allocated in the hot code path. -- See Note [Avoiding compiler perf traps when constructing error messages.] -lint_app_fail_msg :: (Outputable a2) => SDoc -> OutType -> a2 -> SDoc -> SDoc +lint_app_fail_msg :: (Outputable a2) => SDoc -> Type -> a2 -> SDoc -> SDoc lint_app_fail_msg msg kfn arg_tys extra = vcat [ hang (text "Application error in") 2 msg , nest 2 (text "Function type =" <+> ppr kfn) @@ -2231,7 +2150,7 @@ lint_app_fail_msg msg kfn arg_tys extra * * ********************************************************************* -} -lintCoreRule :: OutVar -> OutType -> CoreRule -> LintM () +lintCoreRule :: OutVar -> Type -> CoreRule -> LintM () lintCoreRule _ _ (BuiltinRule {}) = return () -- Don't bother @@ -2239,7 +2158,7 @@ lintCoreRule fun fun_ty rule@(Rule { ru_name = name, ru_bndrs = bndrs , ru_args = args, ru_rhs = rhs }) = noMultiplicityChecks $ -- Skip linearity checking for rules -- See Note [Linting linearity] - lintBinders LambdaBind bndrs $ \ _ -> + lintBinders LambdaBind bndrs $ do { (lhs_ty, _) <- lintCoreArgs (fun_ty, zeroUE) args ; (rhs_ty, _) <- case idJoinPointHood fun of JoinPoint join_arity @@ -2349,23 +2268,16 @@ which is what used to happen. But that proved tricky and error prone -- lintStarCoercion lints a coercion, confirming that its lh kind and -- its rh kind are both *; also ensures that the role is Nominal -- Returns the lh kind -lintStarCoercion :: InCoercion -> LintM OutType +lintStarCoercion :: Coercion -> LintM Type lintStarCoercion g = do { lintCoercion g - ; Pair t1 t2 <- substCoKindM g + ; let Pair t1 t2 = coercionKind g ; checkValueType (typeKind t1) (text "the kind of the left type in" <+> ppr g) ; checkValueType (typeKind t2) (text "the kind of the right type in" <+> ppr g) ; lintRole g Nominal (coercionRole g) ; return t1 } -substCoKindM :: InCoercion -> LintM (Pair OutType) -substCoKindM co - = do { let !(Pair lk rk) = coercionKind co - ; lk' <- substTyM lk - ; rk' <- substTyM rk - ; return (Pair lk' rk') } - -lintCoercion :: HasDebugCallStack => InCoercion -> LintM () +lintCoercion :: HasDebugCallStack => Coercion -> LintM () -- See Note [Linting types and coercions] -- -- If you edit this function, you may need to update the GHC formalism @@ -2377,7 +2289,7 @@ lintCoercion (CoVarCo cv) 2 (text "With offending type:" <+> ppr (varType cv))) | otherwise -- C.f. lintType (TyVarTy tv), which has better docs - = do { _ <- lintVarOcc cv; return () } + = lintVarOcc cv lintCoercion (Refl ty) = lintType ty lintCoercion (GRefl _r ty MRefl) = lintType ty @@ -2385,8 +2297,8 @@ lintCoercion (GRefl _r ty MRefl) = lintType ty lintCoercion (GRefl _r ty (MCo co)) = do { lintType ty ; lintCoercion co - ; tk <- substTyM (typeKind ty) - ; tl <- substTyM (coercionLKind co) + ; let tk = typeKind ty + tl = coercionLKind co ; ensureEqTys tk tl $ hang (text "GRefl coercion kind mis-match:" <+> ppr co) 2 (vcat [ppr ty, ppr tk, ppr tl]) @@ -2419,8 +2331,8 @@ lintCoercion co@(AppCo co1 co2) = do { lintCoercion co1 ; lintCoercion co2 ; let !(Pair lt1 rt1) = coercionKind co1 - ; lk1 <- substTyM (typeKind lt1) - ; rk1 <- substTyM (typeKind rt1) + lk1 = typeKind lt1 + rk1 = typeKind rt1 ; lint_co_app co lk1 [coercionLKind co2] ; lint_co_app co rk1 [coercionRKind co2] @@ -2437,7 +2349,7 @@ lintCoercion co@(ForAllCo {}) = do { _ <- go [] co; return () } where go :: [OutTyCoVar] -- Binders in reverse order - -> InCoercion -> LintM Role + -> Coercion -> LintM Role go tcvs co@(ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR , fco_kind = kind_mco, fco_body = body_co }) | not (isTyCoVar tcv) @@ -2447,15 +2359,15 @@ lintCoercion co@(ForAllCo {}) = do { mb_lk <- case kind_mco of MRefl -> return Nothing MCo kind_co -> Just <$> lintStarCoercion kind_co - ; lintTyCoBndr tcv $ \tcv' -> + ; lintTyCoBndr tcv $ do { case mb_lk of Nothing -> return () - Just lk -> ensureEqTys (varType tcv') lk $ + Just lk -> ensureEqTys (varType tcv) lk $ text "Kind mis-match in ForallCo" <+> ppr co -- I'm not very sure about this part, because it traverses body_co -- but at least it's on a cold path (a ForallCo for a CoVar) - -- Also it works on InTyCoVar and InCoercion, which is suspect + -- Also it works on InTyCoVar and Coercion, which is suspect ; when (isCoVar tcv) $ do { lintL (visL == coreTyLamForAllTyFlag && visR == coreTyLamForAllTyFlag) $ text "Invalid visibility flags in CoVar ForAllCo" <+> ppr co @@ -2464,7 +2376,7 @@ lintCoercion co@(ForAllCo {}) text "Covar can only appear in Refl and GRefl: " <+> ppr co } -- See (FC6) in Note [ForAllCo] in GHC.Core.TyCo.Rep - ; role <- go (tcv':tcvs) body_co + ; role <- go (tcv:tcvs) body_co ; when (role == Nominal) $ lintL (visL `eqForAllVis` visR) $ @@ -2521,8 +2433,8 @@ lintCoercion co@(UnivCo { uco_role = r, uco_prov = prov -- Check the to and from types ; lintType ty1 ; lintType ty2 - ; tk1 <- substTyM (typeKind ty1) - ; tk2 <- substTyM (typeKind ty2) + ; let tk1 = typeKind ty1 + tk2 = typeKind ty2 ; when (r /= Phantom && isTYPEorCONSTRAINT tk1 && isTYPEorCONSTRAINT tk2) (checkTypes ty1 ty2) @@ -2576,8 +2488,8 @@ lintCoercion (SymCo co) = lintCoercion co lintCoercion co@(TransCo co1 co2) = do { lintCoercion co1 ; lintCoercion co2 - ; rk1 <- substTyM (coercionRKind co1) - ; lk2 <- substTyM (coercionLKind co2) + ; let rk1 = coercionRKind co1 + lk2 = coercionLKind co2 ; ensureEqTys rk1 lk2 (hang (text "Trans coercion mis-match:" <+> ppr co) 2 (vcat [ppr (coercionKind co1), ppr (coercionKind co2)])) @@ -2585,7 +2497,7 @@ lintCoercion co@(TransCo co1 co2) lintCoercion the_co@(SelCo cs co) = do { lintCoercion co - ; Pair s t <- substCoKindM co + ; let Pair s t = coercionKind co ; if -- forall (both TyVar and CoVar) | Just _ <- splitForAllTyCoVar_maybe s @@ -2620,7 +2532,7 @@ lintCoercion the_co@(SelCo cs co) lintCoercion the_co@(LRCo _lr co) = do { lintCoercion co - ; Pair s t <- substCoKindM co + ; let Pair s t = coercionKind co ; lintRole co Nominal (coercionRole co) ; case (splitAppTy_maybe s, splitAppTy_maybe t) of (Just {}, Just {}) -> return () @@ -2634,14 +2546,12 @@ lintCoercion orig_co@(InstCo co arg) go (InstCo co arg) args = do { lintCoercion arg; go co (arg:args) } go co args = do { lintCoercion co ; let Pair lty rty = coercionKind co - ; lty' <- substTyM lty - ; rty' <- substTyM rty ; in_scope <- getInScope ; let subst = mkEmptySubst in_scope - ; go_args (subst, lty') (subst,rty') args } + ; go_args (subst, lty) (subst,rty) args } ------------- - go_args :: (Subst, OutType) -> (Subst,OutType) -> [InCoercion] + go_args :: (Subst, Type) -> (Subst,Type) -> [Coercion] -> LintM () go_args _ _ [] = return () @@ -2650,11 +2560,11 @@ lintCoercion orig_co@(InstCo co arg) ; go_args lty1 rty1 args } ------------- - go_arg :: (Subst, OutType) -> (Subst,OutType) -> InCoercion - -> LintM ((Subst,OutType), (Subst,OutType)) + go_arg :: (Subst, Type) -> (Subst,Type) -> Coercion + -> LintM ((Subst,Type), (Subst,Type)) go_arg (lsubst,lty) (rsubst,rty) arg = do { lintRole arg Nominal (coercionRole arg) - ; Pair arg_lty arg_rty <- substCoKindM arg + ; let Pair arg_lty arg_rty = coercionKind arg ; case (splitForAllTyCoVar_maybe lty, splitForAllTyCoVar_maybe rty) of -- forall over tvar @@ -2678,11 +2588,11 @@ lintCoercion orig_co@(InstCo co arg) lintCoercion this_co@(AxiomCo ax cos) = do { mapM_ lintCoercion cos ; lint_roles 0 (coAxiomRuleArgRoles ax) cos - ; prs <- mapM substCoKindM cos + ; let prs = map coercionKind cos ; lint_ax ax prs } where - lint_ax :: CoAxiomRule -> [Pair OutType] -> LintM () + lint_ax :: CoAxiomRule -> [Pair Type] -> LintM () lint_ax (BuiltInFamRew bif) prs = checkL (isJust (bifrw_proves bif prs)) bad_bif lint_ax (BuiltInFamInj bif) prs @@ -2770,8 +2680,8 @@ lintBranch this_co fam_tc branch arg_kinds = do { checkL (arg_kinds `equalLength` (ktvs ++ cvs)) $ (bad_ax this_co (text "lengths")) - ; subst <- getSubst - ; let empty_subst = zapSubst subst + ; in_scope <- getInScope + ; let empty_subst = mkEmptySubst in_scope ; _ <- foldlM check_ki (empty_subst, empty_subst) (zip (ktvs ++ cvs) arg_kinds) @@ -2896,12 +2806,12 @@ lint_axiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches lint_branch :: TyCon -> CoAxBranch -> LintM () lint_branch ax_tc (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs , cab_lhs = lhs_args, cab_rhs = rhs }) - = lintBinders LambdaBind (tvs ++ cvs) $ \_ -> + = lintBinders LambdaBind (tvs ++ cvs) $ do { let lhs = mkTyConApp ax_tc lhs_args ; lintType lhs ; lintType rhs - ; lhs_kind <- substTyM (typeKind lhs) - ; rhs_kind <- substTyM (typeKind rhs) + ; let lhs_kind = typeKind lhs + rhs_kind = typeKind rhs ; lintL (not (lhs_kind `typesAreApart` rhs_kind)) $ hang (text "Inhomogeneous axiom") 2 (text "lhs:" <+> ppr lhs <+> dcolon <+> ppr lhs_kind $$ @@ -2985,35 +2895,26 @@ type LintLevel = Int -- If you edit this type, you may need to update the GHC formalism -- See Note [GHC Formalism] data LintEnv - = LE { le_flags :: LintFlags -- Linting the result of this pass - , le_loc :: [LintLocInfo] -- Locations - - , le_subst :: Subst - -- Current substitution, for TyCoVars only. - -- Non-CoVar Ids don't appear in here, not even in the InScopeSet - -- Used for (a) cloning to avoid shadowing of TyCoVars, - -- so that eqType works ok - -- (b) substituting for let-bound tyvars, when we have - -- (let @a = Int -> Int in ...) - - , le_level :: LintLevel - , le_in_vars :: VarEnv (InVar, OutType, LintLevel) - -- Maps an InVar (i.e. its unique) to its binding InVar - -- and to its OutType - -- /All/ in-scope variables are here (term variables, - -- type variables, and coercion variables) - -- Used at an occurrence of the InVar + = LE { le_flags :: LintFlags -- Linting the result of this pass + , le_loc :: [LintLocInfo] -- Locations + , le_level :: LintLevel + , le_in_scope :: InScopeSet + + , le_in_vars :: VarEnv (Var, LintLevel) + -- Maps an Var (i.e. its unique) to its binding Var and level + -- /All/ in-scope variables are here (term variables, + -- type variables, and coercion variables) + -- Used at an occurrence of the Var , le_joins :: UniqMap Id JoinOcc -- ^ Join points in scope that are valid - -- A subset of the InScopeSet in le_subst -- See Note [Join points] , le_ue_aliases :: NameEnv UsageEnv -- See Note [Linting linearity] -- Assigns usage environments to the alias-like binders, -- as found in non-recursive lets. - -- Domain is OutIds + -- Domain is Ids , le_platform :: Platform -- ^ Target platform , le_diagOpts :: DiagOpts -- ^ Target platform @@ -3369,12 +3270,12 @@ initL cfg m where vars = l_vars cfg init_level = 0 - env = LE { le_flags = l_flags cfg - , le_subst = mkEmptySubst (mkInScopeSetList vars) - , le_level = init_level - , le_in_vars = mkVarEnv [ (v,(v, varType v, init_level)) | v <- vars ] - , le_joins = emptyUniqMap - , le_loc = [] + env = LE { le_flags = l_flags cfg + , le_level = init_level + , le_in_vars = mkVarEnv [ (v,(v, init_level)) | v <- vars ] + , le_in_scope = mkInScopeSetList vars + , le_joins = emptyUniqMap + , le_loc = [] , le_ue_aliases = emptyNameEnv , le_platform = l_platform cfg , le_diagOpts = l_diagOpts cfg @@ -3437,8 +3338,7 @@ addMsg show_context env msgs msg loc_msgs :: [(SrcLoc, SDoc)] -- Innermost first loc_msgs = map dumpLoc (le_loc env) - cxt_doc = vcat [ vcat $ reverse $ map snd loc_msgs - , text "Substitution:" <+> ppr (le_subst env) ] + cxt_doc = vcat $ reverse $ map snd loc_msgs context | show_context = cxt_doc | otherwise = whenPprDebug cxt_doc @@ -3465,78 +3365,45 @@ inCasePat = LintM $ \ env errs -> fromBoxedLResult (Just (is_case_pat env), errs is_case_pat (LE { le_loc = CasePat {} : _ }) = True is_case_pat _other = False -addInScopeId :: InId -> OutType -> (OutId -> LintM a) -> LintM a +addInScopeId :: Id -> LintM a -> LintM a -- Unlike addInScopeTyCoVar, this function does no cloning; Ids never get cloned -addInScopeId in_id out_ty thing_inside +addInScopeId id thing_inside = LintM $ \ env errs -> - let !(out_id, env') = add env - in unLintM (thing_inside out_id) env' errs - + unLintM thing_inside (add env) errs where add env@(LE { le_level = level, le_in_vars = id_vars, le_joins = valid_joins - , le_ue_aliases = aliases, le_subst = subst }) - = (out_id, env1) + , le_ue_aliases = aliases, le_in_scope = in_scope }) + = env { le_level = level1, le_in_vars = in_vars' + , le_in_scope = in_scope `extendInScopeSet` id + , le_joins = valid_joins', le_ue_aliases = aliases' } where level1 = level + 1 - env1 = env { le_level = level1, le_in_vars = in_vars' - , le_joins = valid_joins', le_ue_aliases = aliases' } - in_vars' = extendVarEnv id_vars in_id (in_id, out_ty, level1) - aliases' = delFromNameEnv aliases (idName in_id) + in_vars' = extendVarEnv id_vars id (id, level1) + aliases' = delFromNameEnv aliases (idName id) -- aliases': when shadowing an alias, we need to make sure the -- Id is no longer classified as such. E.g. -- let x = <e1> in case x of x { _DEFAULT -> <e2> } -- Occurrences of 'x' in e2 shouldn't count as occurrences of e1. - -- A very tiny optimisation, not sure if it's really worth it - -- Short-cut when the substitution is a no-op - out_id | isEmptyTCvSubst subst = in_id - | otherwise = setIdType in_id out_ty - valid_joins' - | isJoinId out_id = addToUniqMap valid_joins in_id NormalJoinOcc -- Overwrite with new arity - | otherwise = delFromUniqMap valid_joins in_id -- Remove any existing binding + | isJoinId id = addToUniqMap valid_joins id NormalJoinOcc -- Overwrite with new arity + | otherwise = delFromUniqMap valid_joins id -- Remove any existing binding -addInScopeTyCoVar :: InTyCoVar -> OutType -> (OutTyCoVar -> LintM a) -> LintM a +addInScopeTyCoVar :: TyCoVar -> LintM a -> LintM a -- This function clones to avoid shadowing of TyCoVars -addInScopeTyCoVar tcv tcv_type thing_inside - = LintM $ \ env@(LE { le_level = level, le_in_vars = in_vars, le_subst = subst }) errs -> - let (tcv', subst') = subst_bndr subst - level' = level + 1 +addInScopeTyCoVar tcv thing_inside + = LintM $ \ env@(LE { le_level = level, le_in_vars = in_vars + , le_in_scope = in_scope }) errs -> + let level' = level + 1 env' = env { le_level = level' - , le_in_vars = extendVarEnv in_vars tcv (tcv, tcv_type, level') - , le_subst = subst' } - in unLintM (thing_inside tcv') env' errs - where - subst_bndr subst - = (tcv, subst `extendSubstInScope` tcv) -{- - | isEmptyTCvSubst subst -- No change in kind - , not (tcv `elemInScopeSet` in_scope) -- Not already in scope - = -- Do not extend the substitution, just the in-scope set - (if (varType tcv `eqType` tcv_type) then (\x->x) else - pprTrace "addInScopeTyCoVar" ( - vcat [ text "tcv" <+> ppr tcv <+> dcolon <+> ppr (varType tcv) - , text "tcv_type" <+> ppr tcv_type ])) $ - (tcv, subst `extendSubstInScope` tcv) - - -- Clone, and extend the substitution - | let tcv' = uniqAway in_scope (setVarType tcv tcv_type) - = (tcv', extendTCvSubstWithClone subst tcv tcv') - where - in_scope = substInScopeSet subst --} + , le_in_scope = in_scope `extendInScopeSet` tcv + , le_in_vars = extendVarEnv in_vars tcv (tcv, level') } + in unLintM thing_inside env' errs -getInVarEnv :: LintM (VarEnv (InId, OutType, LintLevel)) +getInVarEnv :: LintM (VarEnv (Id, LintLevel)) getInVarEnv = LintM (\env errs -> fromBoxedLResult (Just (le_in_vars env), errs)) -{- -extendTvSubstL :: TyVar -> Type -> LintM a -> LintM a -extendTvSubstL tv ty m - = LintM $ \ env errs -> - unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs --} - markAllJoinsBad :: LintM a -> LintM a markAllJoinsBad m = LintM $ \ env errs -> unLintM m (env { le_joins = emptyUniqMap }) errs @@ -3570,54 +3437,42 @@ markAllJoinsBadIf False m = m getValidJoins :: LintM (UniqMap Id JoinOcc) getValidJoins = LintM (\ env errs -> fromBoxedLResult (Just (le_joins env), errs)) -getSubst :: LintM Subst -getSubst = LintM (\ env errs -> fromBoxedLResult (Just (le_subst env), errs)) - -substTyM :: InType -> LintM OutType --- Apply the substitution to the type --- The substitution is often empty, in which case it is a no-op -substTyM ty - = do { subst <- getSubst - ; return (substTy subst ty) } - getUEAliases :: LintM (NameEnv UsageEnv) getUEAliases = LintM (\ env errs -> fromBoxedLResult (Just (le_ue_aliases env), errs)) getInScope :: LintM InScopeSet -getInScope = LintM (\ env errs -> fromBoxedLResult (Just (substInScopeSet $ le_subst env), errs)) +getInScope = LintM (\ env errs -> fromBoxedLResult (Just (le_in_scope env), errs)) -lintVarOcc :: InVar -> LintM OutType +lintVarOcc :: Var -> LintM () -- Used at an occurrence of a variable: term variables, type variables, and coercion variables -- Checks -- - that it is in scope -- - that it is not a GlobalId bound by a LocalId --- - that the InType at the ocurrence matches the InType at the binding site +-- - that the Type at the ocurrence matches the Type at the binding site -- - that the variables free in its type are not shadowed at the occurrence site lintVarOcc v_occ | isGlobalId v_occ - = return (idType v_occ) + = return () | otherwise = do { in_var_env <- getInVarEnv ; case lookupVarEnv in_var_env v_occ of Nothing -> failWithL (text pp_what <+> quotes (ppr v_occ) <+> text "is out of scope") - Just (v_bndr, out_ty, bind_level) + Just (v_bndr, bind_level) -> do { let bndr_ty = idType v_bndr ; check_bad_global v_bndr ; check_occ_type_match bndr_ty - ; check_occ_type_scope in_var_env bndr_ty bind_level - ; return out_ty } - + ; check_occ_type_scope in_var_env bndr_ty bind_level } } where - occ_ty :: InType + occ_ty :: Type occ_ty = idType v_occ pp_what | isTyVar v_occ = "The type variable" | isCoVar v_occ = "The coercion variable" | otherwise = "The value variable" - check_bad_global :: InVar -> LintM () + check_bad_global :: Var -> LintM () -- 'check_bad_global' checks for the case where an /occurrence/ is -- a GlobalId, but there is an enclosing binding for a LocalId. -- NB: the in-scope variables are mostly LocalIds, checked by lintIdBndr, @@ -3637,26 +3492,26 @@ lintVarOcc v_occ | otherwise = return () - check_occ_type_match :: InType -> LintM () + check_occ_type_match :: Type -> LintM () -- Check that the type in /binder/ and the type in the /occurrence/ are the same check_occ_type_match bndr_ty - = ensureEqTys bndr_ty occ_ty $ -- Compares InTypes + = ensureEqTys bndr_ty occ_ty $ -- Compares Types mkBndrOccTypeMismatchMsg v_occ bndr_ty occ_ty - check_occ_type_scope :: VarEnv (InVar,OutType,LintLevel) -> InType -> LintLevel -> LintM () + check_occ_type_scope :: VarEnv (Var,LintLevel) -> Type -> LintLevel -> LintM () -- Check that the free vars of the binder's type -- are not shadowed at the occurrence site check_occ_type_scope in_var_env bndr_ty bind_level = checkL (null bad_fvs) $ mkBndrOccFreeVarMsg v_occ occ_ty bad_fvs where - bad_fvs :: [InVar] + bad_fvs :: [Var] bad_fvs = filter is_bad (tyCoVarsOfTypeList bndr_ty) - is_bad :: InVar -> Bool + is_bad :: Var -> Bool -- True of a variable bound inside bind_level is_bad v = case lookupVarEnv in_var_env v of - Just (_, _, v_level) -> v_level > bind_level + Just (_, v_level) -> v_level > bind_level Nothing -> True lookupJoinId :: Id -> LintM (Maybe (JoinArity, JoinOcc)) @@ -3668,21 +3523,21 @@ lookupJoinId id Just join_occ -> return $ Just (idJoinArity id, join_occ) Nothing -> return Nothing } -addAliasUE :: OutId -> UsageEnv -> LintM a -> LintM a +addAliasUE :: Id -> UsageEnv -> LintM a -> LintM a addAliasUE id ue thing_inside = LintM $ \ env errs -> let new_ue_aliases = extendNameEnv (le_ue_aliases env) (getName id) ue in unLintM thing_inside (env { le_ue_aliases = new_ue_aliases }) errs -varCallSiteUsage :: OutId -> LintM UsageEnv +varCallSiteUsage :: Id -> LintM UsageEnv varCallSiteUsage id = do m <- getUEAliases return $ case lookupNameEnv m (getName id) of Nothing -> singleUsageUE id Just id_ue -> id_ue -ensureEqTys :: OutType -> OutType -> SDoc -> LintM () +ensureEqTys :: Type -> Type -> SDoc -> LintM () -- check ty2 is subtype of ty1 (ie, has same structure but usage -- annotations need only be consistent, not equal) -- Assumes ty1,ty2 are have already had the substitution applied @@ -3906,7 +3761,7 @@ mkLetErr bndr rhs hang (text "Rhs:") 4 (ppr rhs)] -mkTyAppMsg :: OutType -> Type -> SDoc +mkTyAppMsg :: Type -> Type -> SDoc mkTyAppMsg ty arg_ty = vcat [text "Illegal type application:", hang (text "Function type:") @@ -4027,13 +3882,13 @@ mkJoinBndrOccMismatchMsg bndr join_arity_bndr join_arity_occ , text "Arity at binding site:" <+> ppr join_arity_bndr , text "Arity at occurrence: " <+> ppr join_arity_occ ] -mkBndrOccTypeMismatchMsg :: InVar -> InType -> InType -> SDoc +mkBndrOccTypeMismatchMsg :: Var -> Type -> Type -> SDoc mkBndrOccTypeMismatchMsg var bndr_ty occ_ty = vcat [ text "Mismatch in type between binder and occurrence" , text "Binder: " <+> ppr var <+> dcolon <+> ppr bndr_ty , text "Occurrence:" <+> ppr var <+> dcolon <+> ppr occ_ty ] -mkBndrOccFreeVarMsg :: InVar -> InType -> [TyCoVar] -> SDoc +mkBndrOccFreeVarMsg :: Var -> Type -> [TyCoVar] -> SDoc mkBndrOccFreeVarMsg var occ_ty bad_tvs = vcat [ text "Free vars of type are shadowed:" <+> ppr bad_tvs , text "Occurrence:" <+> ppr var <+> dcolon <+> ppr occ_ty ] View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/28e0ef3c647b0be6876bd52fd5953637... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/28e0ef3c647b0be6876bd52fd5953637... You're receiving this email because of your account on gitlab.haskell.org.
participants (1)
-
Simon Peyton Jones (＠simonpj)