Simon Peyton Jones pushed to branch wip/T20264 at Glasgow Haskell Compiler / GHC Commits: 687f3662 by Simon Peyton Jones at 2026-03-03T10:11:06+00:00 More wibbles - - - - - 6 changed files: - compiler/GHC/Core.hs - compiler/GHC/Core/Lint.hs - compiler/GHC/Core/Utils.hs - compiler/GHC/CoreToStg/Prep.hs - compiler/GHC/Driver/Config/Core/Lint.hs - compiler/GHC/HsToCore/Utils.hs Changes: ===================================== compiler/GHC/Core.hs ===================================== @@ -465,8 +465,8 @@ TL;DR: we relaxed the let/app invariant to become the let-can-float invariant. Note [Type and coercion lets] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We allow - let @a = TYPE ty in ... +We allow non-recursive type lets: + let a = TYPE ty in ... and similarly for coercions. TODO: fill this out @@ -475,7 +475,7 @@ Wrinkles: (TCL1) In a type let (Let @a = TYPE ty in body), we do /not/ insist that the binder `a` has a TyVarUnfolding. But if it does not, then `body` - must be well-typed without paying atention to the binding. More precisely, + must be well-typed without paying attention to the binding. More precisely, let @a = TYPE ty in body where `a` has no TyVarUnfolding, is well-typed iff (/\a. body) ty @@ -489,15 +489,32 @@ Wrinkles: (which is always substituted) with the tyvar-replete-with-unfolding, rather than merely extending the in-scope set as we do for Ids. +(TCL3) In the output of the desugarer it is very convenient to allow + let a = <type> in ...a.... + where the occurrences of `a` do /not/ have an unfolding, but yet it is essential + to substitute <type> for `a` when Linting. Why? When compiling nested pattern + matching we may combine patterns + K @a1 (co1 :: a1 ~ T) pat1 -> e1 + K @a2 (co2 :: a2 ~ T) pat2 -> e2 + to get a single, shared pattern, something like + K @a1 (co1 :: a1 ~ T) x -> let { a2 = a1; co2 = co1 } in + case x of + pat1 -> e1 + pat2 -> e2 + The bindings { a2=a1; co2=co1 } just make the binders in the two patterns line + up. But for this to be Lint-correct we must actually substitute `a1` for `a2`. + + So, in the ouptut of the desugarer only, if there is no unfolding on the binder, + we just extend the subustitution. + + It's a bit of a hack, but the first roun dof simplification esablishes (TCL1) or + (TCL2). + So: (TCL1) + (TCL2) = EITHER `a` has an unfolding at its binding site, and that unfolding is replicated at every occurrence site OR it doesn't and the occurrences don't either. - -OR we could insist that tyvar bindings always have an unfolding, and use -a beta-redex if not. - Note [Core top-level string literals] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ As an exception to the usual rule that top-level binders must be lifted, ===================================== compiler/GHC/Core/Lint.hs ===================================== @@ -235,8 +235,6 @@ in GHC.Core.Opt.WorkWrap.Utils. (Maybe there are other "clients" of this featur 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! - Note [Bad unsafe coercion] ~~~~~~~~~~~~~~~~~~~~~~~~~~ For discussion see https://gitlab.haskell.org/ghc/ghc/wikis/bad-unsafe-coercions @@ -570,23 +568,31 @@ lintLetExpr :: TyVarSet -- Enclosing let-bound tyvars, all with unfoldings lintLetExpr tvs (Let (NonRec tv (Type rhs_ty)) body) | isTyVar tv = -- See Note [Linting type lets] - do { case tyVarUnfolding_maybe tv of - Nothing -> return () -- See GHC.Core Note [Type and coercion lets] wrinkle (TCL1) - Just unf_ty -> -- These comparisons compare InTypes, which is fine - do { ensureEqTys (tyVarKind tv) (typeKind rhs_ty) $ - tv_err unf_ty "Let-bound tyvar kind incompatible with RHS:" - ; ensureEqTys unf_ty rhs_ty $ - tv_err unf_ty "Let-bound tyvar unfolding not same as RHS:" } - - ; addLoc (RhsOf tv) $ lintType rhs_ty - - ; lintTyCoBndr tv $ \ tv' -> - addLoc (BodyOfLet tv) $ - lintLetExpr (tvs `extendVarSet` tv') body } + do { -- Lint the RHS type + rhs_ty' <- addLoc (RhsOf tv) $ lintTypeAndSubst rhs_ty + + ; lintTyCoBndr tv $ \ tv' -> + do { -- Check that the RHS has the same kind as the tyvar + addLoc (RhsOf tv) $ + lintTyKind tv' rhs_ty' + + -- Check the unfolding + -- See GHC.Core Note [Type and coercion lets] wrinkle (TCL1) + ; case tyVarUnfolding_maybe tv' of + Nothing -> return () + Just unf_ty' -> ensureEqTys unf_ty' rhs_ty' $ + tv_err tv' unf_ty' rhs_ty' + + -- Check the body + ; extendTvLetSubst tv rhs_ty' $ + addLoc (BodyOfLet tv) $ + lintLetExpr (tvs `extendVarSet` tv') body + } } where - tv_err unf_ty msg = hang (text msg <+> pprTyVarWithKind tv) - 2 (vcat [ text "Unfolding:" <+> ppr unf_ty - , text "RHS: " <+> ppr rhs_ty ]) + tv_err tv unf_ty rhs_ty = hang (text "Let-bound tyvar unfolding not same as RHS:" + <+> pprTyVarWithKind tv) + 2 (vcat [ text "Unfolding:" <+> ppr unf_ty + , text "RHS: " <+> ppr rhs_ty ]) lintLetExpr tvs (Let (NonRec bndr rhs) body) | isId bndr @@ -3086,6 +3092,7 @@ data LintFlags , lf_check_linearity :: Bool -- ^ See Note [Linting linearity] , lf_check_fixed_rep :: Bool -- ^ See Note [Checking for representation polymorphism] , lf_check_rubbish_lits :: Bool -- ^ See Note [Checking for rubbish literals] + , lf_inline_type_lets :: Bool -- ^ See Note [Linting type lets] XXX TODO } -- See Note [Checking StaticPtrs] @@ -3505,10 +3512,12 @@ getLintFlags :: LintM LintFlags getLintFlags = LintM $ \ env errs -> fromBoxedLResult (Just (le_flags env), errs) updLintFlags :: (LintFlags -> LintFlags) -> LintM a -> LintM a -updLintFlags upd_flags thing_inside - = LintM $ \env errs -> - let env' = env { le_flags = upd_flags (le_flags env) } - in unLintM thing_inside env' errs +updLintFlags upd_flags + = updLintEnv (\env -> env { le_flags = upd_flags (le_flags env) }) + +updLintEnv :: (LintEnv -> LintEnv) -> LintM a -> LintM a +updLintEnv upd thing_inside + = LintM $ \env errs -> unLintM thing_inside (upd env) errs checkL :: Bool -> SDoc -> LintM () checkL True _ = return () @@ -3634,6 +3643,17 @@ addInScopeTyCoVar tcv tcv_type thing_inside Just unf_ty -> setTyVarUnfolding tcv2 (substTy subst unf_ty) Nothing -> tcv2 +extendTvLetSubst :: TyVar -> Type -> LintM a -> LintM a +extendTvLetSubst tv ty thing_inside + | isJust (tyVarUnfolding_maybe tv) + = thing_inside + | otherwise + = do { flags <- getLintFlags + ; if (lf_inline_type_lets flags) + then updLintEnv (\ env -> env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) + thing_inside + else thing_inside } + getInVarEnv :: LintM (VarEnv (InId, OutVar)) getInVarEnv = LintM (\env errs -> fromBoxedLResult (Just (le_in_vars env), errs)) @@ -3742,7 +3762,7 @@ checkBndrOccCompatibility in_bndr v_occ sameUnfolding :: InVar -- Binder -> InVar -- Occurrence -> LintM Bool --- Check that any unfolding in the /occurence/ is the same as that in the /binder/ +-- Check that any unfolding in the /occurrence/ is the same as that in the /binder/ -- An unfolding in the occurrence is optional for Ids, but compulsory for type-let-boud -- TyVars. Somewhat lazily, we only check the latter. -- We also just compare them as InTypes (as we do the type of the variable); ===================================== compiler/GHC/Core/Utils.hs ===================================== @@ -3323,11 +3323,7 @@ mkPolyAbsLams (getter,setter) bndrs body = go emptyVarSet [] bndrs where wrap_bind :: Expr b -> (b,Expr b) -> Expr b - -- wrap_bind e (bndr, rhs) = (\bndr.e) rhs - -- Very like let bndr=rhs in e - -- but, for type-bindings at least, does not require that the occurrences - -- of bndr have the unfolding from the let-binding - wrap_bind e (bndr, rhs) = App (Lam bndr e) rhs + wrap_bind e (bndr, rhs) = Let (NonRec bndr rhs) e go :: TyVarSet -- Earlier TyVar bndrs that have TyVarUnfoldings -> [(b,Expr b)] -- Accumulated impedence-matching bindings (reversed) ===================================== compiler/GHC/CoreToStg/Prep.hs ===================================== @@ -1527,7 +1527,7 @@ cpeArg :: CorePrepEnv -> Demand -> CoreArg -> UniqSM (Floats, CpeArg) cpeArg env dmd arg = do { (floats1, arg1) <- cpeRhsE env arg -- arg1 can be a lambda - ; let arg_ty = exprType arg1 + ; let arg_ty = exprType arg lev = typeLevity arg_ty dec = wantFloatLocal NonRecursive dmd lev floats1 arg1 ; (floats2, arg2) <- executeFloatDecision env dec floats1 arg1 ===================================== compiler/GHC/Driver/Config/Core/Lint.hs ===================================== @@ -119,7 +119,8 @@ perPassFlags dflags pass , lf_check_inline_loop_breakers = check_lbs , lf_check_static_ptrs = check_static_ptrs , lf_check_linearity = check_linearity - , lf_check_rubbish_lits = check_rubbish } + , lf_check_rubbish_lits = check_rubbish + , lf_inline_type_lets = inline_type_lets } where -- See Note [Checking for global Ids] check_globals = case pass of @@ -156,6 +157,11 @@ perPassFlags dflags pass CorePrep -> True _ -> False + -- See Note [Linting type lets] in GHC.Core.Lint + inline_type_lets = case pass of + CoreDesugar -> True + _ -> False + initLintConfig :: DynFlags -> [Var] -> LintConfig initLintConfig dflags vars =LintConfig { l_diagOpts = initDiagOpts dflags @@ -172,4 +178,5 @@ defaultLintFlags dflags = LF { lf_check_global_ids = False , lf_report_unsat_syns = True , lf_check_fixed_rep = True , lf_check_rubbish_lits = True + , lf_inline_type_lets = False } ===================================== compiler/GHC/HsToCore/Utils.hs ===================================== @@ -245,6 +245,8 @@ wrapBinds [] e = e wrapBinds ((new,old):prs) e = wrapBind new old (wrapBinds prs e) wrapBind :: Var -> Var -> CoreExpr -> CoreExpr +-- Used only to line up varaibles when combining case patterns, +-- in GHC.HsToCore.Match.Constructor and GHC.HsToCore.Match.Literal wrapBind new old body -- NB: this function must deal with term | new==old = body -- variables, type variables or coercion variables | otherwise = Let (NonRec new (varToCoreExpr old)) body View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/687f3662c2f384dec27130862a3352ac... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/687f3662c2f384dec27130862a3352ac... You're receiving this email because of your account on gitlab.haskell.org.