- ghc-commits - Haskell.org

[Git][ghc/ghc][master] llvm: fix split sections for llvm backend
by Marge Bot (＠marge-bot) 17 Jan '26

17 Jan '26

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: b18b2c42 by Cheng Shao at 2026-01-17T06:03:44-05:00 llvm: fix split sections for llvm backend This patch fixes split sections for llvm backend: - Pass missing `--data-sections`/`--function-sections` flags to llc/opt. - Use `(a)llvm.compiler.used` instead of `(a)llvm.used` to avoid sections being unnecessarily retained at link-time. Fixes #26770. ------------------------- Metric Decrease: libdir size_hello_artifact size_hello_unicode ------------------------- Co-authored-by: Codex <codex(a)openai.com> - - - - - 3 changed files: - compiler/GHC/CmmToLlvm.hs - compiler/GHC/CmmToLlvm/Base.hs - compiler/GHC/Driver/Pipeline/Execute.hs Changes: ===================================== compiler/GHC/CmmToLlvm.hs ===================================== @@ -271,15 +271,23 @@ cmmUsedLlvmGens = do -- used if we didn't provide these hints. This will generate a -- definition of the form -- - -- @llvm.used = appending global [42 x i8*] [i8* bitcast <var> to i8*, ...] + -- @llvm.compiler.used = appending global [42 x i8*] [i8* bitcast <var> to i8*, ...] -- -- Which is the LLVM way of protecting them against getting removed. + -- + -- We used to emit @llvm.used, but it's too strong and results in + -- SHF_GNU_RETAIN section flag in the object, which prevents linker + -- gc-sections from working properly for LLVM backend (#26770). + -- @llvm.compiler.used serves a similar purpose that protects the + -- variable from being dropped by llc/opt, but it allows linker + -- gc-sections to work. See + -- https://llvm.org/docs/LangRef.html#the-llvm-compiler-used-global-variable ivars <- getUsedVars let cast x = LMBitc (LMStaticPointer (pVarLift x)) i8Ptr ty = LMArray (length ivars) i8Ptr usedArray = LMStaticArray (map cast ivars) ty sectName = Just $ fsLit "llvm.metadata" - lmUsedVar = LMGlobalVar (fsLit "llvm.used") ty Appending sectName Nothing Constant + lmUsedVar = LMGlobalVar (fsLit "llvm.compiler.used") ty Appending sectName Nothing Constant lmUsed = LMGlobal lmUsedVar (Just usedArray) if null ivars then return () ===================================== compiler/GHC/CmmToLlvm/Base.hs ===================================== @@ -286,7 +286,7 @@ data LlvmEnv = LlvmEnv , envUniqMeta :: UniqFM Unique MetaId -- ^ Global metadata nodes , envFunMap :: LlvmEnvMap -- ^ Global functions so far, with type , envAliases :: UniqSet LMString -- ^ Globals that we had to alias, see [Llvm Forward References] - , envUsedVars :: [LlvmVar] -- ^ Pointers to be added to llvm.used (see @cmmUsedLlvmGens@) + , envUsedVars :: [LlvmVar] -- ^ Pointers to be added to llvm.compiler.used (see @cmmUsedLlvmGens@) -- the following get cleared for every function (see @withClearVars@) , envVarMap :: LlvmEnvMap -- ^ Local variables so far, with type ===================================== compiler/GHC/Driver/Pipeline/Execute.hs ===================================== @@ -934,6 +934,14 @@ llvmOptions llvm_config llvm_version dflags = [("-relocation-model=" ++ rmodel ,"-relocation-model=" ++ rmodel) | not (null rmodel)] + -- Both llc/opt need these flags for split sections + ++ [ ("--data-sections", "--data-sections") + | gopt Opt_SplitSections dflags + ] + ++ [ ("--function-sections", "--function-sections") + | gopt Opt_SplitSections dflags + ] + -- Additional llc flags ++ [("", "-mcpu=" ++ mcpu) | not (null mcpu) , not (any (isInfixOf "-mcpu") (getOpts dflags opt_lc)) ] View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b18b2c42c32488ad6d3480a56a1fcd7… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b18b2c42c32488ad6d3480a56a1fcd7… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc][master] add a new issue template for getting verified
by Marge Bot (＠marge-bot) 17 Jan '26

17 Jan '26

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 9e5e0234 by mangoiv at 2026-01-17T06:03:03-05:00 add a new issue template for getting verified To reduce spam created by new users, we will in future not grant any rights but reporting issues to new users. That is why we will have to be able to verify them. The added issue template serves that purpose. - - - - - 1 changed file: - + .gitlab/issue_templates/get-verified.md Changes: ===================================== .gitlab/issue_templates/get-verified.md ===================================== @@ -0,0 +1,21 @@ + + +I cannot create new projects or fork an existing one. I want to contribute to projects here, so please add me to the list of verified users. + + + +- [ ] I want to … + + +Checklist  +--- + +- [ ] I understand that this GitLab instance is intended for projects immediately related to the Glasgow Haskell Compiler + and that personal / unrelated projects can and will be removed + + +/label ~"Account verification" View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9e5e02344add644d6201f6742bdec89… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9e5e02344add644d6201f6742bdec89… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 4 commits: Improve newtype unwrapping
by Marge Bot (＠marge-bot) 16 Jan '26

16 Jan '26

Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC Commits: 29c0aceb by Simon Peyton Jones at 2026-01-16T17:18:11-05:00 Improve newtype unwrapping Ticket #26746 describes several relatively-minor shortcomings of newtype unwrapping. This MR addresses them, while also (arguably) simplifying the code a bit. See new Note [Solving newtype equalities: overview] and Note [Decomposing newtype equalities] and Note [Eager newtype decomposition] and Note [Even more eager newtype decomposition] For some reason, on Windows only, runtime allocations decrease for test T5205 (from 52k to 48k). I have not idea why. No change at all on Linux. I'm just going to accept the change. (I saw this same effect in another MR so I think it's a fault in the baseline.) Metric Decrease: T5205 - - - - - 8b59e62c by Andreas Klebinger at 2026-01-16T17:18:52-05:00 testsuite: Widen acceptance window for T5205. Fixes #26782 - - - - - 41d698ea by mangoiv at 2026-01-16T17:51:50-05:00 add a new issue template for getting verified To reduce spam created by new users, we will in future not grant any rights but reporting issues to new users. That is why we will have to be able to verify them. The added issue template serves that purpose. - - - - - d72448bd by Cheng Shao at 2026-01-16T17:51:50-05:00 llvm: fix split sections for llvm backend This patch fixes split sections for llvm backend: - Pass missing `--data-sections`/`--function-sections` flags to llc/opt. - Use `(a)llvm.compiler.used` instead of `(a)llvm.used` to avoid sections being unnecessarily retained at link-time. Fixes #26770. ------------------------- Metric Decrease: libdir size_hello_artifact size_hello_unicode ------------------------- Co-authored-by: Codex <codex(a)openai.com> - - - - - 20 changed files: - + .gitlab/issue_templates/get-verified.md - compiler/GHC/CmmToLlvm.hs - compiler/GHC/CmmToLlvm/Base.hs - compiler/GHC/Core/FamInstEnv.hs - compiler/GHC/Driver/Pipeline/Execute.hs - compiler/GHC/Tc/Instance/Family.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/Monad.hs - testsuite/tests/deriving/should_fail/T8984.stderr - testsuite/tests/deriving/should_fail/deriving-via-fail.stderr - testsuite/tests/deriving/should_fail/deriving-via-fail4.stderr - testsuite/tests/deriving/should_fail/deriving-via-fail5.stderr - testsuite/tests/perf/should_run/all.T - + testsuite/tests/typecheck/should_compile/T26746.hs - testsuite/tests/typecheck/should_compile/all.T - testsuite/tests/typecheck/should_fail/T15801.stderr - testsuite/tests/typecheck/should_fail/T22924b.stderr - testsuite/tests/typecheck/should_fail/TcCoercibleFail.hs - testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== .gitlab/issue_templates/get-verified.md ===================================== @@ -0,0 +1,21 @@ + + +I cannot create new projects or fork an existing one. I want to contribute to projects here, so please add me to the list of verified users. + + + +- [ ] I want to … + + +Checklist  +--- + +- [ ] I understand that this GitLab instance is intended for projects immediately related to the Glasgow Haskell Compiler + and that personal / unrelated projects can and will be removed + + +/label ~"Account verification" ===================================== compiler/GHC/CmmToLlvm.hs ===================================== @@ -271,15 +271,23 @@ cmmUsedLlvmGens = do -- used if we didn't provide these hints. This will generate a -- definition of the form -- - -- @llvm.used = appending global [42 x i8*] [i8* bitcast <var> to i8*, ...] + -- @llvm.compiler.used = appending global [42 x i8*] [i8* bitcast <var> to i8*, ...] -- -- Which is the LLVM way of protecting them against getting removed. + -- + -- We used to emit @llvm.used, but it's too strong and results in + -- SHF_GNU_RETAIN section flag in the object, which prevents linker + -- gc-sections from working properly for LLVM backend (#26770). + -- @llvm.compiler.used serves a similar purpose that protects the + -- variable from being dropped by llc/opt, but it allows linker + -- gc-sections to work. See + -- https://llvm.org/docs/LangRef.html#the-llvm-compiler-used-global-variable ivars <- getUsedVars let cast x = LMBitc (LMStaticPointer (pVarLift x)) i8Ptr ty = LMArray (length ivars) i8Ptr usedArray = LMStaticArray (map cast ivars) ty sectName = Just $ fsLit "llvm.metadata" - lmUsedVar = LMGlobalVar (fsLit "llvm.used") ty Appending sectName Nothing Constant + lmUsedVar = LMGlobalVar (fsLit "llvm.compiler.used") ty Appending sectName Nothing Constant lmUsed = LMGlobal lmUsedVar (Just usedArray) if null ivars then return () ===================================== compiler/GHC/CmmToLlvm/Base.hs ===================================== @@ -286,7 +286,7 @@ data LlvmEnv = LlvmEnv , envUniqMeta :: UniqFM Unique MetaId -- ^ Global metadata nodes , envFunMap :: LlvmEnvMap -- ^ Global functions so far, with type , envAliases :: UniqSet LMString -- ^ Globals that we had to alias, see [Llvm Forward References] - , envUsedVars :: [LlvmVar] -- ^ Pointers to be added to llvm.used (see @cmmUsedLlvmGens@) + , envUsedVars :: [LlvmVar] -- ^ Pointers to be added to llvm.compiler.used (see @cmmUsedLlvmGens@) -- the following get cleared for every function (see @withClearVars@) , envVarMap :: LlvmEnvMap -- ^ Local variables so far, with type ===================================== compiler/GHC/Core/FamInstEnv.hs ===================================== @@ -1061,10 +1061,10 @@ lookup_fam_inst_env' lookup_mode (FamIE _ ie) fam match_tys , fi_tys = tpl_tys }) = do subst <- tcMatchTys tpl_tys match_tys1 return (FamInstMatch { fim_instance = item - , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2 - , fim_cos = assert (all (isJust . lookupCoVar subst) tpl_cvs) $ - substCoVars subst tpl_cvs - }) + , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2 + , fim_cos = assert (all (isJust . lookupCoVar subst) tpl_cvs) $ + substCoVars subst tpl_cvs + }) where (match_tys1, match_tys2) = split_tys tpl_tys ===================================== compiler/GHC/Driver/Pipeline/Execute.hs ===================================== @@ -934,6 +934,14 @@ llvmOptions llvm_config llvm_version dflags = [("-relocation-model=" ++ rmodel ,"-relocation-model=" ++ rmodel) | not (null rmodel)] + -- Both llc/opt need these flags for split sections + ++ [ ("--data-sections", "--data-sections") + | gopt Opt_SplitSections dflags + ] + ++ [ ("--function-sections", "--function-sections") + | gopt Opt_SplitSections dflags + ] + -- Additional llc flags ++ [("", "-mcpu=" ++ mcpu) | not (null mcpu) , not (any (isInfixOf "-mcpu") (getOpts dflags opt_lc)) ] ===================================== compiler/GHC/Tc/Instance/Family.hs ===================================== @@ -5,7 +5,7 @@ module GHC.Tc.Instance.Family ( FamInstEnvs, tcGetFamInstEnvs, checkFamInstConsistency, tcExtendLocalFamInstEnv, tcLookupDataFamInst, tcLookupDataFamInst_maybe, - tcTopNormaliseNewTypeTF_maybe, + tcUnwrapNewtype_maybe, -- * Injectivity reportInjectivityErrors, reportConflictingInjectivityErrs @@ -46,7 +46,6 @@ import GHC.Utils.Misc import GHC.Utils.Panic import GHC.Utils.FV -import GHC.Data.Bag( Bag, unionBags, unitBag ) import GHC.Data.Maybe import Control.Monad @@ -452,58 +451,57 @@ tcLookupDataFamInst_maybe fam_inst_envs tc tc_args | otherwise = Nothing --- | 'tcTopNormaliseNewTypeTF_maybe' gets rid of top-level newtypes, --- potentially looking through newtype /instances/ and type synonyms. +-- | 'tcUnwrapNewtype_mabye' gets rid of /one layer/ of top-level newtypes -- -- It is only used by the type inference engine (specifically, when -- solving representational equality), and hence it is careful to unwrap -- only if the relevant data constructor is in scope. That's why -- it gets a GlobalRdrEnv argument. -- --- It is careful not to unwrap data/newtype instances nor synonyms --- if it can't continue unwrapping. Such care is necessary for proper --- error messages. +-- It is capable of unwrapping a newtype /instance/. E.g +-- data D a +-- newtype instance D Int = MkD Bool +-- Then `tcUnwrapNewtype_maybe (D Int)` will unwrap to give the `Bool` inside. +-- However, it is careful not to unwrap data/newtype instances if it can't +-- unwrap the newtype inside it; that might in the example if `MkD` was +-- not in scope. Such care is necessary for proper error messages. -- -- It does not look through type families. --- It does not normalise arguments to a tycon. +-- It does not normalise arguments to the tycon. -- --- If the result is Just ((gres, co), rep_ty), then +-- If the result is Just (gre, co, rep_ty), then -- co : ty ~R rep_ty --- gres are the GREs for the data constructors that --- had to be in scope -tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs - -> GlobalRdrEnv - -> Type - -> Maybe ((Bag GlobalRdrElt, TcCoercion), Type) -tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty --- cf. FamInstEnv.topNormaliseType_maybe and Coercion.topNormaliseNewType_maybe - = topNormaliseTypeX stepper plus ty +-- gre is the GRE for the data constructor that had to be in scope +tcUnwrapNewtype_maybe :: FamInstEnvs + -> GlobalRdrEnv + -> Type + -> Maybe (GlobalRdrElt, TcCoercion, Type) +tcUnwrapNewtype_maybe faminsts rdr_env ty + | Just (tc,tys) <- tcSplitTyConApp_maybe ty + = firstJust (try_nt_unwrap tc tys) + (try_fam_unwrap tc tys) + | otherwise + = Nothing where - plus :: (Bag GlobalRdrElt, TcCoercion) -> (Bag GlobalRdrElt, TcCoercion) - -> (Bag GlobalRdrElt, TcCoercion) - plus (gres1, co1) (gres2, co2) = ( gres1 `unionBags` gres2 - , co1 `mkTransCo` co2 ) - - stepper :: NormaliseStepper (Bag GlobalRdrElt, TcCoercion) - stepper = unwrap_newtype `composeSteppers` unwrap_newtype_instance - - -- For newtype instances we take a double step or nothing, so that + -- For newtype /instances/ we take a double step or nothing, so that -- we don't return the representation type of the newtype instance, -- which would lead to terrible error messages - unwrap_newtype_instance rec_nts tc tys - | Just (tc', tys', co) <- tcLookupDataFamInst_maybe faminsts tc tys - = fmap (mkTransCo co) <$> unwrap_newtype rec_nts tc' tys' - | otherwise = NS_Done + try_fam_unwrap tc tys + | Just (tc', tys', fam_co) <- tcLookupDataFamInst_maybe faminsts tc tys + , Just (gre, nt_co, ty') <- try_nt_unwrap tc' tys' + = Just (gre, mkTransCo fam_co nt_co, ty') + | otherwise + = Nothing - unwrap_newtype rec_nts tc tys + try_nt_unwrap tc tys | Just con <- newTyConDataCon_maybe tc , Just gre <- lookupGRE_Name rdr_env (dataConName con) -- This is where we check that the -- data constructor is in scope - = (,) (unitBag gre) <$> unwrapNewTypeStepper rec_nts tc tys - + , Just (ty', co) <- instNewTyCon_maybe tc tys + = Just (gre, co, ty') | otherwise - = NS_Done + = Nothing {- ************************************************************************ ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -23,7 +23,7 @@ import GHC.Tc.Types.CtLoc import GHC.Tc.Types.Origin import GHC.Tc.Utils.Unify import GHC.Tc.Utils.TcType -import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe ) +import GHC.Tc.Instance.Family ( tcUnwrapNewtype_maybe ) import qualified GHC.Tc.Utils.Monad as TcM import GHC.Core.Type @@ -48,7 +48,6 @@ import GHC.Utils.Misc import GHC.Utils.Monad import GHC.Data.Pair -import GHC.Data.Bag import Control.Monad import Data.Maybe ( isJust, isNothing ) import Data.List ( zip4 ) @@ -334,24 +333,52 @@ can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 | Just ty1' <- coreView ty1 = can_eq_nc rewritten rdr_env envs ev eq_rel ty1' ps_ty1 ty2 ps_ty2 | Just ty2' <- coreView ty2 = can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2' ps_ty2 --- need to check for reflexivity in the ReprEq case. --- See Note [Eager reflexivity check] --- Check only when rewritten because the zonk_eq_types check in canEqNC takes --- care of the non-rewritten case. -can_eq_nc True _rdr_env _envs ev ReprEq ty1 _ ty2 _ - | ty1 `tcEqType` ty2 - = canEqReflexive ev ReprEq ty1 - --- When working with ReprEq, unwrap newtypes. --- See Note [Unwrap newtypes first] +-- Look for (N s1 .. sn) ~R# (N t1 .. tn) +-- where either si=ti +-- or N is phantom in i'th position +-- See Note [Solving newtype equalities: overview] +-- and (for details) Note [Eager newtype decomposition] +-- We try this /before/ attempting to unwrap N, because if N is +-- recursive, unwrapping will loop. +-- This /matters/ for newtypes, but is /safe/ for all types +can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _ + | ReprEq <- eq_rel + , TyConApp tc1 tys1 <- ty1 + , TyConApp tc2 tys2 <- ty2 + , tc1 == tc2 + , ok tys1 tys2 (tyConRoles tc1) + = canDecomposableTyConAppOK ev eq_rel tc1 (ty1,tys1) (ty2,tys2) + where + ok :: [TcType] -> [TcType] -> [Role] -> Bool + -- OK to decompose a representational equality + -- if the args are already equal + -- or are phantom role + -- See Note [Eager newtype decomposition] + -- You might think that representational role would also be OK, but + -- see Note [Even more eager newtype decomposition] + ok (ty1:tys1) (ty2:tys2) rs + | Phantom : rs' <- rs = ok tys1 tys2 rs' + | ty1 `tcEqType` ty2 = ok tys1 tys2 (drop 1 rs) + | otherwise = False + ok [] [] _ = True + ok _ _ _ = False -- Mis-matched lengths, just about possible because of + -- kind polymorphism. Anyway False is a safe result! + +-- Unwrap newtypes, when in ReprEq only +-- See Note [Solving newtype equalities: overview] +-- and (for details) Note [Unwrap newtypes first] -- This must be above the TyVarTy case, in order to guarantee (TyEq:N) +-- +-- We unwrap *one layer only*; `can_eq_newtype_nc` then loops back to +-- `can_eq_nc`. If there is a recursive newtype, so that we keep +-- unwrapping, the depth limit in `can_eq_newtype_nc` will blow up. can_eq_nc _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 | ReprEq <- eq_rel - , Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1 + , Just stuff1 <- tcUnwrapNewtype_maybe envs rdr_env ty1 = can_eq_newtype_nc rdr_env envs ev NotSwapped stuff1 ty2 ps_ty2 | ReprEq <- eq_rel - , Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2 + , Just stuff2 <- tcUnwrapNewtype_maybe envs rdr_env ty2 = can_eq_newtype_nc rdr_env envs ev IsSwapped stuff2 ty1 ps_ty1 -- Then, get rid of casts @@ -374,6 +401,11 @@ can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _ = do { setEqIfWanted ev (mkReflCPH eq_rel ty1) ; stopWith ev "Equal LitTy" } +can_eq_nc _rewritten _rdr_env _envs ev eq_rel + s1@ForAllTy{} _ + s2@ForAllTy{} _ + = can_eq_nc_forall ev eq_rel s1 s2 + -- Decompose FunTy: (s -> t) and (c => t) -- NB: don't decompose (Int -> blah) ~ (Show a => blah) can_eq_nc _rewritten _rdr_env _envs ev eq_rel @@ -401,19 +433,20 @@ can_eq_nc rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _ , rewritten || both_generative = canTyConApp ev eq_rel both_generative (ty1,tc1,tys1) (ty2,tc2,tys2) -can_eq_nc _rewritten _rdr_env _envs ev eq_rel - s1@ForAllTy{} _ - s2@ForAllTy{} _ - = can_eq_nc_forall ev eq_rel s1 s2 - --- See Note [Canonicalising type applications] about why we require rewritten types --- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families --- NB: Only decompose AppTy for nominal equality. --- See Note [Decomposing AppTy equalities] -can_eq_nc True _rdr_env _envs ev NomEq ty1 _ ty2 _ - | Just (t1, s1) <- tcSplitAppTy_maybe ty1 +-- Decompose applications +can_eq_nc rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _ + | True <- rewritten -- Why True? See Note [Canonicalising type applications] + -- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families + , Just (t1, s1) <- tcSplitAppTy_maybe ty1 , Just (t2, s2) <- tcSplitAppTy_maybe ty2 - = can_eq_app ev t1 s1 t2 s2 + = case eq_rel of + NomEq -> can_eq_app ev t1 s1 t2 s2 + -- Only decompose AppTy for nominal equality. + -- See (APT1) in Note [Decomposing AppTy equalities] + + ReprEq | ty1 `tcEqType` ty2 -> canEqReflexive ev ReprEq ty1 + -- tcEqType: see (APT2) in Note [Decomposing AppTy equalities] + | otherwise -> finishCanWithIrred ReprEqReason ev ------------------- -- Can't decompose. @@ -665,124 +698,18 @@ There are lots of wrinkles of course: the attempt if we fail. -} -{- Note [Unwrap newtypes first] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -See also Note [Decomposing newtype equalities] - -Consider - newtype N m a = MkN (m a) -N will get a conservative, Nominal role for its second parameter 'a', -because it appears as an argument to the unknown 'm'. Now consider - [W] N Maybe a ~R# N Maybe b - -If we /decompose/, we'll get - [W] a ~N# b - -But if instead we /unwrap/ we'll get - [W] Maybe a ~R# Maybe b -which in turn gives us - [W] a ~R# b -which is easier to satisfy. - -Conclusion: we must unwrap newtypes before decomposing them. This happens -in `can_eq_newtype_nc` - -We did flirt with making the /rewriter/ expand newtypes, rather than -doing it in `can_eq_newtype_nc`. But with recursive newtypes we want -to be super-careful about expanding! - - newtype A = MkA [A] -- Recursive! - - f :: A -> [A] - f = coerce - -We have [W] A ~R# [A]. If we rewrite [A], it'll expand to - [[[[[...]]]]] -and blow the reduction stack. See Note [Newtypes can blow the stack] -in GHC.Tc.Solver.Rewrite. But if we expand only the /top level/ of -both sides, we get - [W] [A] ~R# [A] -which we can, just, solve by reflexivity. - -So we simply unwrap, on-demand, at top level, in `can_eq_newtype_nc`. - -This is all very delicate. There is a real risk of a loop in the type checker -with recursive newtypes -- but I think we're doomed to do *something* -delicate, as we're really trying to solve for equirecursive type -equality. Bottom line for users: recursive newtypes do not play well with type -inference for representational equality. See also Section 5.3.1 and 5.3.4 of -"Safe Zero-cost Coercions for Haskell" (JFP 2016). - -See also Note [Decomposing newtype equalities]. - ---- Historical side note --- - -We flirted with doing /both/ unwrap-at-top-level /and/ rewrite-deeply; -see #22519. But that didn't work: see discussion in #22924. Specifically -we got a loop with a minor variation: - f2 :: a -> [A] - f2 = coerce - -Note [Eager reflexivity check] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have - - newtype X = MkX (Int -> X) - -and - - [W] X ~R X - -Naively, we would start unwrapping X and end up in a loop. Instead, -we do this eager reflexivity check. This is necessary only for representational -equality because the rewriter technology deals with the similar case -(recursive type families) for nominal equality. - -Note that this check does not catch all cases, but it will catch the cases -we're most worried about, types like X above that are actually inhabited. - -Here's another place where this reflexivity check is key: -Consider trying to prove (f a) ~R (f a). The AppTys in there can't -be decomposed, because representational equality isn't congruent with respect -to AppTy. So, when canonicalising the equality above, we get stuck and -would normally produce a CIrredCan. However, we really do want to -be able to solve (f a) ~R (f a). So, in the representational case only, -we do a reflexivity check. - -(This would be sound in the nominal case, but unnecessary, and I [Richard -E.] am worried that it would slow down the common case.) - - Note [Newtypes can blow the stack] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have - - newtype X = MkX (Int -> X) - newtype Y = MkY (Int -> Y) - -and now wish to prove - - [W] X ~R Y - -This Wanted will loop, expanding out the newtypes ever deeper looking -for a solid match or a solid discrepancy. Indeed, there is something -appropriate to this looping, because X and Y *do* have the same representation, -in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized -coercion will ever witness it. This loop won't actually cause GHC to hang, -though, because we check our depth in `can_eq_newtype_nc`. --} - ------------------------ -- | We're able to unwrap a newtype. Update the bits accordingly. can_eq_newtype_nc :: GlobalRdrEnv -> FamInstEnvs -> CtEvidence -- ^ :: ty1 ~ ty2 -> SwapFlag - -> ((Bag GlobalRdrElt, TcCoercion), TcType) -- ^ :: ty1 ~ ty1' + -> (GlobalRdrElt, TcCoercion, TcType) -- ^ :: ty1 ~ ty1' -> TcType -- ^ ty2 -> TcType -- ^ ty2, with type synonyms -> TcS (StopOrContinue (Either IrredCt EqCt)) -can_eq_newtype_nc rdr_env envs ev swapped ((gres, co1), ty1') ty2 ps_ty2 +can_eq_newtype_nc rdr_env envs ev swapped (gre, co1, ty1') ty2 ps_ty2 = do { traceTcS "can_eq_newtype_nc" $ - vcat [ ppr ev, ppr swapped, ppr co1, ppr gres, ppr ty1', ppr ty2 ] + vcat [ ppr ev, ppr swapped, ppr co1, ppr gre, ppr ty1', ppr ty2 ] -- Check for blowing our stack, and increase the depth -- See Note [Newtypes can blow the stack] @@ -791,14 +718,20 @@ can_eq_newtype_nc rdr_env envs ev swapped ((gres, co1), ty1') ty2 ps_ty2 -- Next, we record uses of newtype constructors, since coercing -- through newtypes is tantamount to using their constructors. - ; recordUsedGREs gres + ; recordUsedGRE gre ; let redn1 = mkReduction co1 ty1' redn2 = mkReflRedn Representational ps_ty2 - ; new_ev <- rewriteEqEvidence ev' swapped redn1 redn2 + ; new_ev <- rewriteEqEvidence ev' (flipSwap swapped) redn2 redn1 emptyCoHoleSet - ; can_eq_nc False rdr_env envs new_ev ReprEq ty1' ty1' ty2 ps_ty2 } + -- ty1 is the one being unwrapped. Loop back to can_eq_nc with + -- the arguments flipped so that ty2 is looked at first in the + -- next iteration. That way if we have (Id Rec) ~R# (Id Rec) + -- where newtype Id a = MkId a and newtype Rec = MkRec Rec + -- we'll unwrap both Ids, then spot Rec=Rec. + -- See (END2) in Note [Eager newtype decomposition] + ; can_eq_nc False rdr_env envs new_ev ReprEq ty2 ps_ty2 ty1' ty1' } --------- -- ^ Decompose a type application. @@ -896,7 +829,7 @@ canTyConApp ev eq_rel both_generative (ty1,tc1,tys1) (ty2,tc2,tys2) | tc1 == tc2 , tys1 `equalLength` tys2 = do { inerts <- getInertSet - ; if can_decompose inerts + ; if canDecomposeTcApp ev eq_rel tc1 inerts then canDecomposableTyConAppOK ev eq_rel tc1 (ty1,tys1) (ty2,tys2) else assert (eq_rel == ReprEq) $ canEqSoftFailure ReprEqReason ev ty1 ty2 } @@ -918,19 +851,31 @@ canTyConApp ev eq_rel both_generative (ty1,tc1,tys1) (ty2,tc2,tys2) | otherwise = canEqSoftFailure ReprEqReason ev ty1 ty2 - where + +canDecomposeTcApp :: CtEvidence -> EqRel -> TyCon -> InertSet -> Bool -- See Note [Decomposing TyConApp equalities] -- and Note [Decomposing newtype equalities] - can_decompose inerts - = isInjectiveTyCon tc1 (eqRelRole eq_rel) - || (assert (eq_rel == ReprEq) $ - -- assert: isInjectiveTyCon is always True for Nominal except - -- for type synonyms/families, neither of which happen here - -- Moreover isInjectiveTyCon is True for Representational - -- for algebraic data types. So we are down to newtypes - -- and data families. - ctEvFlavour ev == Wanted && noGivenNewtypeReprEqs tc1 inerts) - -- See Note [Decomposing newtype equalities] (EX2) +canDecomposeTcApp ev eq_rel tc inerts + | isInjectiveTyCon tc eq_role = True + | isGiven ev = False + | otherwise = assert (eq_rel == ReprEq) $ + assert (isNewTyCon tc || + isDataFamilyTyCon tc || + isAbstractTyCon tc ) $ + noGivenNewtypeReprEqs tc inerts + -- The otherwise case deals with + -- * Representational equalities (T s1..sn) ~R# (T t1..tn) + -- * where T is a newtype or data family or abstract + -- Why? isInjectiveTyCon is always True for eq_rel=NomEq except for type + -- synonyms/families, neither of which happen here; and isInjectiveTyCon + -- is True for Representational for algebraic data types. + -- + -- noGivenNewtypeReprEqs: see Note [Decomposing newtype equalities] (EX4) + -- Decomposing here is a last resort + -- NB: despite all these tests, decomposition of data familiies is alas + -- /still/ incomplete. See (EX3) in Note [Decomposing newtype equalities] + where + eq_role = eqRelRole eq_rel {- Note [Canonicalising TyCon/TyCon equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -945,7 +890,7 @@ Suppose we are canonicalising [W] Int ~R# DF (TF a). Then (TC1) We might have an inert Given (a ~# Char), so if we rewrote the wanted (i.e. went around again in `can_eq_nc` with `rewritten`=True, we'd get [W] Int ~R# DF Bool - and then the `tcTopNormaliseNewTypeTF_maybe` call would fire and + and then the `tcUnwrapNewtype_maybe` call would fire and we'd unwrap the newtype. So we must do that "go round again" bit. Hence the complicated guard (rewritten || both_generative) in `can_eq_nc`. @@ -1114,6 +1059,110 @@ This is not a very big deal. It reduces the number of solver steps in the test RaeJobTalk from 1830 to 1815, a 1% reduction. But still, it doesn't cost anything either. +Note [Solving newtype equalities: overview] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +This Note also applies to data families, which we treat like +newtype in case of 'newtype instance'. + +Consider (N s1..sn) ~R# (N t1..tn), where N is a newtype. +We try three strategies, in order: + +(NTE1) Decompose if the si/ti are either (a) identical or (b) phantom. This step + avoids unwrapping, which allows success in some cases where the newtype + would unwrap infinitely. See Note [Eager newtype decomposition] + +(NTE2) Unwrap the newtype, if possible. Always good, but it requires the data + constructor to be in scope. See Note [Unwrap newtypes first]. + + If the newtype is recursive, this unwrapping might go on forever, + so `can_eq_newtype_nc` has a depth bound check. + See Note [Newtypes can blow the stack] + +(NTE3) Decompose the tycon application. This step is a last resort, because it + risks losing completeness. See Note [Decomposing newtype equalities] + +Note [Newtypes can blow the stack] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have + + newtype X = MkX (Int -> X) + newtype Y = MkY (Int -> Y) + +and now wish to prove + + [W] X ~R Y + +This Wanted will loop, expanding out the newtypes ever deeper looking +for a solid match or a solid discrepancy. Indeed, there is something +appropriate to this looping, because X and Y *do* have the same representation, +in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized +coercion will ever witness it. This loop won't actually cause GHC to hang, +though, because we check our depth in `can_eq_newtype_nc`. + +However, GHC can still loop badly: see #26757, which shows how we can create +types whose size is exponential in the depth of newtype expansion. That makes +GHC go out to lunch unless the depth bound is very small indeed; and a small +depth bound makes perfectly legitimate programs fail. We don't have solid +solution for this, but it's rare. + +Note [Unwrap newtypes first] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +See also Note [Decomposing newtype equalities] + +Consider + newtype N m a = MkN (m a) +N will get a conservative, Nominal role for its second parameter 'a', +because it appears as an argument to the unknown 'm'. Now consider + [W] N Maybe a ~R# N Maybe b + +If we /decompose/, we'll get + [W] a ~N# b + +But if instead we /unwrap/ we'll get + [W] Maybe a ~R# Maybe b +which in turn gives us + [W] a ~R# b +which is easier to satisfy. + +Conclusion: we must unwrap newtypes before decomposing them. This happens +in `can_eq_newtype_nc` + +We did flirt with making the /rewriter/ expand newtypes, rather than +doing it in `can_eq_newtype_nc`. But with recursive newtypes we want +to be super-careful about expanding! + + newtype A = MkA [A] -- Recursive! + + f :: A -> [A] + f = coerce + +We have [W] A ~R# [A]. If we rewrite [A], it'll expand to + [[[[[...]]]]] +and blow the reduction stack. See Note [Newtypes can blow the stack] +in GHC.Tc.Solver.Rewrite. But if we expand only the /top level/ of +both sides, we get + [W] [A] ~R# [A] +which we can, just, solve by reflexivity. + +So we simply unwrap, on-demand, at top level, in `can_eq_newtype_nc`. + +This is all very delicate. There is a real risk of a loop in the type checker +with recursive newtypes -- but I think we're doomed to do *something* +delicate, as we're really trying to solve for equirecursive type +equality. Bottom line for users: recursive newtypes do not play well with type +inference for representational equality. See also Section 5.3.1 and 5.3.4 of +"Safe Zero-cost Coercions for Haskell" (JFP 2016). + +See also Note [Decomposing newtype equalities]. + +--- Historical side note --- + +We flirted with doing /both/ unwrap-at-top-level /and/ rewrite-deeply; +see #22519. But that didn't work: see discussion in #22924. Specifically +we got a loop with a minor variation: + f2 :: a -> [A] + f2 = coerce + Note [Decomposing newtype equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ This Note also applies to data families, which we treat like @@ -1133,7 +1182,10 @@ if the newtype is abstract (so can't be unwrapped) we can only solve the equality by (a) using a Given or (b) decomposition. If (a) is impossible (e.g. no Givens) then (b) is safe albeit potentially incomplete. -There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: +Remember: Decomposing Wanteds is always /sound/. + This Note is only about /completeness/. + +There are three ways in which decomposing [W] (N ty1) ~r (N ty2) could be incomplete: * Incompleteness example (EX1): unwrap first newtype Nt a = MkNt (Id a) @@ -1146,7 +1198,7 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: which is unsatisfiable. Unwrapping, though, leads to a solution. CONCLUSION: always unwrap newtypes before attempting to decompose - them. This is done in can_eq_nc. Of course, we can't unwrap if the data + them. This is done in `can_eq_nc`. Of course, we can't unwrap if the data constructor isn't in scope. See Note [Unwrap newtypes first]. * Incompleteness example (EX2): prioritise Nominal equalities. See #24887 @@ -1154,20 +1206,32 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: data instance D Int = MkD1 (D Char) data instance D Bool = MkD2 (D Char) Now suppose we have - [W] g1: D Int ~R# D a - [W] g2: a ~# Bool - If we solve g2 first, giving a:=Bool, then we can solve g1 easily: + [W] g1: D Int ~R# D alpha + [W] g2: alpha ~# Bool + If we solve g2 first, giving alpha:=Bool, then we can solve g1 easily: D Int ~R# D Char ~R# D Bool by newtype unwrapping. BUT: if we instead attempt to solve g1 first, we can unwrap the LHS (only) - leaving [W] D Char ~#R D Bool - If we decompose now, we'll get (Char ~R# Bool), which is insoluble. + leaving [W] D Char ~#R D alpha + If we decompose now, we'll get (Char ~R# alpha), which is insoluble, since + alpha turns out to be Bool. CONCLUSION: prioritise nominal equalites in the work list. See Note [Prioritise equalities] in GHC.Tc.Solver.InertSet. -* Incompleteness example (EX3): check available Givens +* Incompleteness example (EX3) + Sadly, the fix for (EX2) is /still/ incomplete: + * The equality `g2` might be in a sibling implication constraint, + invisible for now. + * The equality `g2` might be hidden in a class constraint: + class C a + instance (a~Bool) => C [a] + [W] g3 :: C [alpha] + When we get around to solving `g3` we'll discover (g2:alpha~Bool) + So that's a real infelicity in the solver. + +* Incompleteness example (EX4): check available Givens newtype Nt a = Mk Bool -- NB: a is not used in the RHS, type role Nt representational -- but the user gives it an R role anyway @@ -1230,18 +1294,48 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: un-expanded equality superclasses; but only in some very obscure recursive-superclass situations. - Yet another approach (!) is described in - Note [Decomposing newtypes a bit more aggressively]. - -Remember: decomposing Wanteds is always /sound/. This Note is -only about /completeness/. - -Note [Decomposing newtypes a bit more aggressively] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -IMPORTANT: the ideas in this Note are *not* implemented. Instead, the -current approach is detailed in Note [Decomposing newtype equalities] -and Note [Unwrap newtypes first]. -For more details about the ideas in this Note see +Note [Eager newtype decomposition] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider [W] (Rec1 Int) ~R# (Rec1 Bool) where + newtype Rec1 a = MkRec1 (Rec1 a) + +If we apply (NTE2), we'll loop because `Rec1` unwraps forever. +But the role of `a` is inferred as Phantom, so it sound and complete +to decompose via `canDecomposableTyConAppOK`, giving nothing at all +(because of the Phantom role). So we win. + +Another useful special case is + newtype Rec = MkRec Rec +where there are no arguments. + +So we do an eager decomposition check in step (NTE1), /before/ trying to unwrap +in (NTE2). This is a HACK: it catches some cases of recursion, but not all. +But it's a hack that has been in GHC for some time. + +Wrinkles + +(END1) The eager-decomposition step is fine for all data types, not just newtypes. + +(END2) Consider newtype Id a = MkId a -- Not recusrive + newtype Rec = MkRec Rec -- Recursive + and [W] Id Rec ~R# Rec + Then (NTE1) will fail; (NTE2) will succeed in unwrapping Id, generating + [W] Rec ~R# Rec; and (NTE1) will succeed when we go round the loop. + + What about [W] Rec ~R# Id Rec? + Here (NTE1) will fail again; (NTE2) will succeed, by unwrapping Rec, to get + Rec again. If we just iterate with [W] Rec ~R# Id Rec, we'll be stuck in + a loop. Instead we want to flip the constraint round so we get + [W] Id Rec ~R# Rec. Now we win. See the flipping in `can_eq_newtype_nc`. + +(END3) See Note [Even more eager newtype decomposition] + +Note [Even more eager newtype decomposition] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Eager newtype decomposition] decomposes [W] (N s ~R# N t) if N's role is +phantom. We could go further and decompose if the arguments are all Phantom +/or/ Representational. This is not implemented. For more details about the +ideas in this Note see * GHC propoosal: https://github.com/ghc-proposals/ghc-proposals/pull/549 * issue #22441 * discussion on !9282. @@ -1249,9 +1343,8 @@ For more details about the ideas in this Note see Consider [G] c, [W] (IO Int) ~R (IO Age) where IO is abstract, and newtype Age = MkAge Int -- Not abstract -With the above rules, if there any Given Irreds, -the Wanted is insoluble because we can't decompose it. But in fact, -if we look at the defn of IO, roughly, +With the above rules, if there any Given Irreds, the Wanted is insoluble because +we can't decompose it. But in fact, if we look at the defn of IO, roughly, newtype IO a = State# -> (State#, a) we can see that decomposing [W] (IO Int) ~R (IO Age) to [W] Int ~R Age @@ -1260,41 +1353,26 @@ IO's argment is representational. Hence: DecomposeNewtypeIdea: decompose [W] (N s1 .. sn) ~R (N t1 .. tn) - if the roles of all N's arguments are representational - -If N's arguments really /are/ representational this will not lose -completeness. Here "really are representational" means "if you expand -all newtypes in N's RHS, we'd infer a representational role for each -of N's type variables in that expansion". See Note [Role inference] -in GHC.Tc.TyCl.Utils. - -But the user might /override/ a phantom role with an explicit role -annotation, and then we could (obscurely) get incompleteness. -Consider - - module A( silly, T ) where - newtype T a = MkT Int - type role T representational -- Override phantom role - - silly :: Coercion (T Int) (T Bool) - silly = Coercion -- Typechecks by unwrapping the newtype + if the roles of all N's arguments are representational (or phantom) - data Coercion a b where -- Actually defined in Data.Type.Coercion - Coercion :: Coercible a b => Coercion a b +If N's arguments really /are/ representational this will not lose completeness. +Here "really are representational" means "if you expand all newtypes in N's RHS, +we'd infer a representational role for each of N's type variables in that +expansion". See Note [Role inference] in GHC.Tc.TyCl.Utils. - module B where - import A - f :: T Int -> T Bool - f = case silly of Coercion -> coerce +But the user might /override/ a phantom role with an explicit role annotation, +and then we could (obscurely) get incompleteness. Consider (#9117): + newtype Phant a = MkPhant Char + type role Phant representational -- Override phantom role + [W] Phant Int ~R# Phant Char -Here the `coerce` gives [W] (T Int) ~R (T Bool) which, if we decompose, -we'll get stuck with (Int ~R Bool). Instead we want to use the -[G] (T Int) ~R (T Bool), which will be in the Irreds. +We do not want to decompose to Int ~R# Char; better to unwrap Summary: we could adopt (DecomposeNewtypeIdea), at the cost of a very obscure incompleteness (above). But no one is reporting a problem from the lack of decompostion, so we'll just leave it for now. This long Note is just to record the thinking for our future selves. +---- End of speculative aside --------- Note [Decomposing AppTy equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1305,12 +1383,12 @@ Note [Decomposing TyConApp equalities]. We have s1 t1 ~N s2 t2 ==> s1 ~N s2, t1 ~N t2 (CO_LEFT, CO_RIGHT) In the first of these, why do we need Nominal equality in (t1 ~N t2)? -See {2} below. +See (APT3) below. For sound and complete solving, we need both directions to decompose. So: * At nominal role, all is well: we have both directions. -* At representational role, decomposition of Givens is unsound (see {1} below), - and decomposition of Wanteds is incomplete. +* At representational role, decomposition of Givens is unsound + (see (APT1) below), and decomposition of Wanteds is incomplete. Here is an example of the incompleteness for Wanteds: @@ -1325,7 +1403,7 @@ Suppose we see w1 before w2. If we decompose, using AppCo to prove w1, we get [W] w4 :: b ~N a Note that w4 is *nominal*. A nominal role here is necessary because AppCo -requires a nominal role on its second argument. (See {2} for an example of +requires a nominal role on its second argument. (See (APT3) for an example of why.) Now we are stuck, because w4 is insoluble. On the other hand, if we see w2 first, setting alpha := Maybe, all is well, as we can decompose Maybe b ~R Maybe a into b ~R a. @@ -1348,12 +1426,21 @@ Bottom line: the lack of an equation in can_eq_nc Extra points -{1} Decomposing a Given AppTy over a representational role is simply +(APT1) Decomposing a Given AppTy at Representational role is simply unsound. For example, if we have co1 :: Phant Int ~R a Bool (for the newtype Phant, above), then we surely don't want any relationship between Int and Bool, lest we also have co2 :: Phant ~ a around. -{2} The role on the AppCo coercion is a conservative choice, because we don't + For Wanteds, decomposing an AppTy at Representational role is incomplete. + +(APT2) What if we have [W] (f a) ~R# (f a) + We can't decompose because of (APT1). But it's silly to reject. So we do + an equality check, in the AppTy/AppTy case of `can_eq_nc`. + + (It would be sound to do this reflexivity check in the Nominal case too, + but not necessary, and there might be a perf cost.) + +(APT3) The role on the AppCo coercion is a conservative choice, because we don't know the role signature of the function. For example, let's assume we could have a representational role on the second argument of AppCo. Then, consider ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -22,7 +22,7 @@ module GHC.Tc.Solver.Monad ( updWorkListTcS, pushLevelNoWorkList, pushTcLevelM_, - runTcPluginTcS, recordUsedGREs, + runTcPluginTcS, recordUsedGRE, matchGlobalInst, TcM.ClsInstResult(..), QCInst(..), @@ -1519,18 +1519,16 @@ tcLookupTyCon n = wrapTcS $ TcM.tcLookupTyCon n -- pure veneer of TcS. But it's just about warnings around unused imports -- and local constructors (GHC will issue fewer warnings than it otherwise -- might), so it's not worth losing sleep over. -recordUsedGREs :: Bag GlobalRdrElt -> TcS () -recordUsedGREs gres - = do { wrapTcS $ TcM.addUsedGREs NoDeprecationWarnings gre_list +recordUsedGRE :: GlobalRdrElt -> TcS () +recordUsedGRE gre + = do { wrapTcS $ TcM.addUsedGRE NoDeprecationWarnings gre -- If a newtype constructor was imported, don't warn about not -- importing it... - ; wrapTcS $ traverse_ (TcM.keepAlive . greName) gre_list } + ; wrapTcS $ TcM.keepAlive (greName gre) } -- ...and similarly, if a newtype constructor was defined in the same -- module, don't warn about it being unused. -- See Note [Tracking unused binding and imports] in GHC.Tc.Utils. - where - gre_list = bagToList gres -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== testsuite/tests/deriving/should_fail/T8984.stderr ===================================== @@ -1,6 +1,6 @@ T8984.hs:7:46: error: [GHC-18872] - • Couldn't match representation of type: cat a (N cat a Int) - with that of: cat a (cat a Int) + • Couldn't match representation of type: cat a (cat a Int) + with that of: cat a (N cat a Int) arising from the coercion of the method ‘app’ from type ‘cat a (cat a Int)’ to type ‘N cat a (N cat a Int)’ Note: We cannot know what roles the parameters to ‘cat a’ have; ===================================== testsuite/tests/deriving/should_fail/deriving-via-fail.stderr ===================================== @@ -1,12 +1,12 @@ deriving-via-fail.hs:10:34: error: [GHC-10283] - • Couldn't match representation of type ‘a’ with that of ‘b’ + • Couldn't match representation of type ‘b’ with that of ‘a’ arising from the coercion of the method ‘showsPrec’ from type ‘Int -> Identity b -> ShowS’ to type ‘Int -> Foo1 a -> ShowS’ - ‘a’ is a rigid type variable bound by + ‘b’ is a rigid type variable bound by the deriving clause for ‘Show (Foo1 a)’ at deriving-via-fail.hs:10:34-37 - ‘b’ is a rigid type variable bound by + ‘a’ is a rigid type variable bound by the deriving clause for ‘Show (Foo1 a)’ at deriving-via-fail.hs:10:34-37 • When deriving the instance for (Show (Foo1 a)) ===================================== testsuite/tests/deriving/should_fail/deriving-via-fail4.stderr ===================================== @@ -1,17 +1,17 @@ deriving-via-fail4.hs:15:12: error: [GHC-18872] - • Couldn't match representation of type ‘Int’ with that of ‘Char’ + • Couldn't match representation of type ‘Char’ with that of ‘Int’ arising from the coercion of the method ‘==’ from type ‘Char -> Char -> Bool’ to type ‘F1 -> F1 -> Bool’ • When deriving the instance for (Eq F1) deriving-via-fail4.hs:18:13: error: [GHC-10283] - • Couldn't match representation of type ‘a1’ with that of ‘a2’ + • Couldn't match representation of type ‘a2’ with that of ‘a1’ arising from the coercion of the method ‘c’ from type ‘a -> a -> Bool’ to type ‘a -> F2 a1 -> Bool’ - ‘a1’ is a rigid type variable bound by + ‘a2’ is a rigid type variable bound by the deriving clause for ‘C a (F2 a1)’ at deriving-via-fail4.hs:18:13-15 - ‘a2’ is a rigid type variable bound by + ‘a1’ is a rigid type variable bound by the deriving clause for ‘C a (F2 a1)’ at deriving-via-fail4.hs:18:13-15 • When deriving the instance for (C a (F2 a1)) ===================================== testsuite/tests/deriving/should_fail/deriving-via-fail5.stderr ===================================== @@ -1,10 +1,10 @@ deriving-via-fail5.hs:8:1: error: [GHC-10283] - • Couldn't match representation of type ‘a’ with that of ‘b’ + • Couldn't match representation of type ‘b’ with that of ‘a’ arising from a use of ‘GHC.Internal.Prim.coerce’ - ‘a’ is a rigid type variable bound by + ‘b’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) - ‘b’ is a rigid type variable bound by + ‘a’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) • In the expression: @@ -25,12 +25,12 @@ deriving-via-fail5.hs:8:1: error: [GHC-10283] (bound at deriving-via-fail5.hs:8:1) deriving-via-fail5.hs:8:1: error: [GHC-10283] - • Couldn't match representation of type ‘a’ with that of ‘b’ + • Couldn't match representation of type ‘b’ with that of ‘a’ arising from a use of ‘GHC.Internal.Prim.coerce’ - ‘a’ is a rigid type variable bound by + ‘b’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) - ‘b’ is a rigid type variable bound by + ‘a’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) • In the expression: @@ -48,12 +48,12 @@ deriving-via-fail5.hs:8:1: error: [GHC-10283] show :: Foo4 a -> String (bound at deriving-via-fail5.hs:8:1) deriving-via-fail5.hs:8:1: error: [GHC-10283] - • Couldn't match representation of type ‘a’ with that of ‘b’ + • Couldn't match representation of type ‘b’ with that of ‘a’ arising from a use of ‘GHC.Internal.Prim.coerce’ - ‘a’ is a rigid type variable bound by + ‘b’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) - ‘b’ is a rigid type variable bound by + ‘a’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) • In the expression: ===================================== testsuite/tests/perf/should_run/all.T ===================================== @@ -128,7 +128,7 @@ test('T4978', ['-O2']) test('T5205', - [collect_stats('bytes allocated',5), + [collect_stats('bytes allocated',15), only_ways(['normal', 'optasm']) ], compile_and_run, ===================================== testsuite/tests/typecheck/should_compile/T26746.hs ===================================== @@ -0,0 +1,33 @@ +module T26746 where + +import Data.Coerce + +newtype Foo a = Foo (Foo a) +newtype Age = MkAge Int + +ex1 :: (Foo Age) -> (Foo Int) +ex1 = coerce + +newtype Womble a = MkWomble (Foo a) + +ex2 :: Womble (Foo Age) -> (Foo Int) +ex2 = coerce + +ex3 :: (Foo Age) -> Womble (Foo Int) +ex3 = coerce + + +-- Surprisingly this one works: +newtype Z1 = MkZ1 Z2 +newtype Z2 = MKZ2 Z1 + +ex4 :: Z1 -> Z2 +ex4 = coerce + +-- But this one does not (commented out) +-- newtype Y1 = MkY1 Y2 +-- newtype Y2 = MKY2 Y3 +-- newtype Y3 = MKY3 Y1 +-- +-- ex5 :: Y1 -> Y3 +-- ex5 = coerce ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -957,3 +957,4 @@ test('T17705', normal, compile, ['']) test('T14745', normal, compile, ['']) test('T26451', normal, compile, ['']) test('T26582', normal, compile, ['']) +test('T26746', normal, compile, ['']) ===================================== testsuite/tests/typecheck/should_fail/T15801.stderr ===================================== @@ -1,7 +1,8 @@ T15801.hs:52:10: error: [GHC-18872] - • Couldn't match representation of type: UnOp op_a -> UnOp b - with that of: op_a --> b - arising (via a quantified constraint) from the superclasses of an instance declaration + • Couldn't match representation of type: op_a --> b + with that of: UnOp op_a -> UnOp b + arising (via a quantified constraint) from + the superclasses of an instance declaration When trying to solve the quantified constraint forall (op_a :: Op (*)) (b :: Op (*)). op_a -#- b arising from the superclasses of an instance declaration ===================================== testsuite/tests/typecheck/should_fail/T22924b.stderr ===================================== @@ -1,6 +1,6 @@ T22924b.hs:10:5: error: [GHC-40404] • Reduction stack overflow; size = 201 - When simplifying the following constraint: Coercible [R] S + When simplifying the following constraint: Coercible S [R] • In the expression: coerce In an equation for ‘f’: f = coerce Suggested fix: ===================================== testsuite/tests/typecheck/should_fail/TcCoercibleFail.hs ===================================== @@ -20,15 +20,6 @@ foo4 = coerce $ one :: Down Int newtype Void = Void Void foo5 = coerce :: Void -> () - ------------------------------------- --- This next one generates an exponentially big type as it --- tries to unwrap. See comment:15 in #11518 --- Adding assertions that force the types can make us --- run out of space. -newtype VoidBad a = VoidBad (VoidBad (a,a)) -foo5' = coerce :: (VoidBad ()) -> () - ------------------------------------ -- This should fail with a context stack overflow newtype Fix f = Fix (f (Fix f)) ===================================== testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr ===================================== @@ -34,23 +34,21 @@ TcCoercibleFail.hs:18:8: error: [GHC-18872] In the expression: coerce $ one :: Down Int In an equation for ‘foo4’: foo4 = coerce $ one :: Down Int -TcCoercibleFail.hs:21:8: error: [GHC-18872] - • Couldn't match representation of type ‘Void’ with that of ‘()’ - arising from a use of ‘coerce’ +TcCoercibleFail.hs:21:8: error: [GHC-40404] + • Reduction stack overflow; size = 201 + When simplifying the following constraint: Coercible () Void • In the expression: coerce :: Void -> () In an equation for ‘foo5’: foo5 = coerce :: Void -> () + Suggested fix: + Use -freduction-depth=0 to disable this check + (any upper bound you could choose might fail unpredictably with + minor updates to GHC, so disabling the check is recommended if + you're sure that type checking should terminate) -TcCoercibleFail.hs:30:9: error: [GHC-18872] - • Couldn't match representation of type ‘VoidBad ()’ - with that of ‘()’ - arising from a use of ‘coerce’ - • In the expression: coerce :: (VoidBad ()) -> () - In an equation for ‘foo5'’: foo5' = coerce :: (VoidBad ()) -> () - -TcCoercibleFail.hs:35:8: error: [GHC-40404] +TcCoercibleFail.hs:26:8: error: [GHC-40404] • Reduction stack overflow; size = 201 When simplifying the following constraint: - Coercible (Either Int (Fix (Either Int))) (Fix (Either Age)) + Coercible (Fix (Either Age)) (Either Int (Fix (Either Int))) • In the expression: coerce :: Fix (Either Int) -> Fix (Either Age) In an equation for ‘foo6’: foo6 = coerce :: Fix (Either Int) -> Fix (Either Age) @@ -60,10 +58,9 @@ TcCoercibleFail.hs:35:8: error: [GHC-40404] minor updates to GHC, so disabling the check is recommended if you're sure that type checking should terminate) -TcCoercibleFail.hs:36:8: error: [GHC-18872] - • Couldn't match representation of type ‘Either - Int (Fix (Either Int))’ - with that of ‘()’ +TcCoercibleFail.hs:27:8: error: [GHC-18872] + • Couldn't match representation of type ‘()’ + with that of ‘Either Int (Fix (Either Int))’ arising from a use of ‘coerce’ • In the expression: coerce :: Fix (Either Int) -> () In an equation for ‘foo7’: foo7 = coerce :: Fix (Either Int) -> () ===================================== testsuite/tests/typecheck/should_fail/all.T ===================================== @@ -326,11 +326,7 @@ test('T7989', normal, compile_fail, ['']) test('T8034', normal, compile_fail, ['']) test('T8142', normal, compile_fail, ['']) test('T8262', normal, compile_fail, ['']) - -# TcCoercibleFail times out with the compiler is compiled with -DDEBUG. -# This is expected (see comment in source file). -test('TcCoercibleFail', [when(compiler_debugged(), skip)], compile_fail, ['']) - +test('TcCoercibleFail', [], compile_fail, ['']) test('TcCoercibleFail2', [], compile_fail, ['']) test('TcCoercibleFail3', [], compile_fail, ['']) test('T8306', normal, compile_fail, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/1c92069b0510ae4f367e441d4d5111… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/1c92069b0510ae4f367e441d4d5111… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc][wip/26737] 3 commits: Improve newtype unwrapping
by Simon Peyton Jones (＠simonpj) 16 Jan '26

16 Jan '26

Simon Peyton Jones pushed to branch wip/26737 at Glasgow Haskell Compiler / GHC Commits: 29c0aceb by Simon Peyton Jones at 2026-01-16T17:18:11-05:00 Improve newtype unwrapping Ticket #26746 describes several relatively-minor shortcomings of newtype unwrapping. This MR addresses them, while also (arguably) simplifying the code a bit. See new Note [Solving newtype equalities: overview] and Note [Decomposing newtype equalities] and Note [Eager newtype decomposition] and Note [Even more eager newtype decomposition] For some reason, on Windows only, runtime allocations decrease for test T5205 (from 52k to 48k). I have not idea why. No change at all on Linux. I'm just going to accept the change. (I saw this same effect in another MR so I think it's a fault in the baseline.) Metric Decrease: T5205 - - - - - 8b59e62c by Andreas Klebinger at 2026-01-16T17:18:52-05:00 testsuite: Widen acceptance window for T5205. Fixes #26782 - - - - - 22fb0ced by Simon Peyton Jones at 2026-01-16T22:44:25+00:00 Make the implicit-parameter class have representational role This MR addresses #26737, by making the built-in class IP have a representational role for its second parameter. See Note [IP: implicit parameter class] in ghc-internal:GHC.Internal.Classes.IP In fact, IP is (unfortunately, currently) exposed by base:GHC.Base, so we ran a quick CLC proposal to agree the change: https://github.com/haskell/core-libraries-committee/issues/385 Some (small) compilations get faster because they only need to load (small) interface file GHC.Internal.Classes.IP.hi, rather than (large) GHC.Internal.Classes.hi. Metric Decrease: T10421 T12150 T12425 T24582 T5837 - - - - - 28 changed files: - compiler/GHC/Builtin/Names.hs - compiler/GHC/Core/FamInstEnv.hs - compiler/GHC/Tc/Instance/Family.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/Monad.hs - docs/users_guide/9.16.1-notes.rst - libraries/ghc-internal/ghc-internal.cabal.in - libraries/ghc-internal/src/GHC/Internal/Classes.hs - + libraries/ghc-internal/src/GHC/Internal/Classes/IP.hs - testsuite/tests/deriving/should_fail/T8984.stderr - testsuite/tests/deriving/should_fail/deriving-via-fail.stderr - testsuite/tests/deriving/should_fail/deriving-via-fail4.stderr - testsuite/tests/deriving/should_fail/deriving-via-fail5.stderr - testsuite/tests/interface-stability/base-exports.stdout - testsuite/tests/interface-stability/base-exports.stdout-mingw32 - testsuite/tests/interface-stability/base-exports.stdout-ws-32 - testsuite/tests/interface-stability/ghc-prim-exports.stdout - testsuite/tests/interface-stability/ghc-prim-exports.stdout-mingw32 - testsuite/tests/perf/should_run/all.T - testsuite/tests/th/TH_implicitParams.stdout - + testsuite/tests/typecheck/should_compile/T26737.hs - + testsuite/tests/typecheck/should_compile/T26746.hs - testsuite/tests/typecheck/should_compile/all.T - testsuite/tests/typecheck/should_fail/T15801.stderr - testsuite/tests/typecheck/should_fail/T22924b.stderr - testsuite/tests/typecheck/should_fail/TcCoercibleFail.hs - testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== compiler/GHC/Builtin/Names.hs ===================================== @@ -526,7 +526,7 @@ genericTyConNames = [ gHC_PRIM, gHC_PRIM_PANIC, gHC_TYPES, gHC_INTERNAL_DATA_DATA, gHC_MAGIC, gHC_MAGIC_DICT, - gHC_CLASSES, gHC_PRIMOPWRAPPERS :: Module + gHC_CLASSES, gHC_CLASSES_IP, gHC_PRIMOPWRAPPERS :: Module gHC_PRIM = mkGhcInternalModule (fsLit "GHC.Internal.Prim") -- Primitive types and values gHC_PRIM_PANIC = mkGhcInternalModule (fsLit "GHC.Internal.Prim.Panic") gHC_TYPES = mkGhcInternalModule (fsLit "GHC.Internal.Types") @@ -534,6 +534,7 @@ gHC_MAGIC = mkGhcInternalModule (fsLit "GHC.Internal.Magic") gHC_MAGIC_DICT = mkGhcInternalModule (fsLit "GHC.Internal.Magic.Dict") gHC_CSTRING = mkGhcInternalModule (fsLit "GHC.Internal.CString") gHC_CLASSES = mkGhcInternalModule (fsLit "GHC.Internal.Classes") +gHC_CLASSES_IP = mkGhcInternalModule (fsLit "GHC.Internal.Classes.IP") gHC_PRIMOPWRAPPERS = mkGhcInternalModule (fsLit "GHC.Internal.PrimopWrappers") gHC_INTERNAL_TUPLE = mkGhcInternalModule (fsLit "GHC.Internal.Tuple") @@ -1521,7 +1522,7 @@ fromLabelClassOpName -- Implicit Parameters ipClassName :: Name ipClassName - = clsQual gHC_CLASSES (fsLit "IP") ipClassKey + = clsQual gHC_CLASSES_IP (fsLit "IP") ipClassKey -- Overloaded record fields hasFieldClassName :: Name ===================================== compiler/GHC/Core/FamInstEnv.hs ===================================== @@ -1061,10 +1061,10 @@ lookup_fam_inst_env' lookup_mode (FamIE _ ie) fam match_tys , fi_tys = tpl_tys }) = do subst <- tcMatchTys tpl_tys match_tys1 return (FamInstMatch { fim_instance = item - , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2 - , fim_cos = assert (all (isJust . lookupCoVar subst) tpl_cvs) $ - substCoVars subst tpl_cvs - }) + , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2 + , fim_cos = assert (all (isJust . lookupCoVar subst) tpl_cvs) $ + substCoVars subst tpl_cvs + }) where (match_tys1, match_tys2) = split_tys tpl_tys ===================================== compiler/GHC/Tc/Instance/Family.hs ===================================== @@ -5,7 +5,7 @@ module GHC.Tc.Instance.Family ( FamInstEnvs, tcGetFamInstEnvs, checkFamInstConsistency, tcExtendLocalFamInstEnv, tcLookupDataFamInst, tcLookupDataFamInst_maybe, - tcTopNormaliseNewTypeTF_maybe, + tcUnwrapNewtype_maybe, -- * Injectivity reportInjectivityErrors, reportConflictingInjectivityErrs @@ -46,7 +46,6 @@ import GHC.Utils.Misc import GHC.Utils.Panic import GHC.Utils.FV -import GHC.Data.Bag( Bag, unionBags, unitBag ) import GHC.Data.Maybe import Control.Monad @@ -452,58 +451,57 @@ tcLookupDataFamInst_maybe fam_inst_envs tc tc_args | otherwise = Nothing --- | 'tcTopNormaliseNewTypeTF_maybe' gets rid of top-level newtypes, --- potentially looking through newtype /instances/ and type synonyms. +-- | 'tcUnwrapNewtype_mabye' gets rid of /one layer/ of top-level newtypes -- -- It is only used by the type inference engine (specifically, when -- solving representational equality), and hence it is careful to unwrap -- only if the relevant data constructor is in scope. That's why -- it gets a GlobalRdrEnv argument. -- --- It is careful not to unwrap data/newtype instances nor synonyms --- if it can't continue unwrapping. Such care is necessary for proper --- error messages. +-- It is capable of unwrapping a newtype /instance/. E.g +-- data D a +-- newtype instance D Int = MkD Bool +-- Then `tcUnwrapNewtype_maybe (D Int)` will unwrap to give the `Bool` inside. +-- However, it is careful not to unwrap data/newtype instances if it can't +-- unwrap the newtype inside it; that might in the example if `MkD` was +-- not in scope. Such care is necessary for proper error messages. -- -- It does not look through type families. --- It does not normalise arguments to a tycon. +-- It does not normalise arguments to the tycon. -- --- If the result is Just ((gres, co), rep_ty), then +-- If the result is Just (gre, co, rep_ty), then -- co : ty ~R rep_ty --- gres are the GREs for the data constructors that --- had to be in scope -tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs - -> GlobalRdrEnv - -> Type - -> Maybe ((Bag GlobalRdrElt, TcCoercion), Type) -tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty --- cf. FamInstEnv.topNormaliseType_maybe and Coercion.topNormaliseNewType_maybe - = topNormaliseTypeX stepper plus ty +-- gre is the GRE for the data constructor that had to be in scope +tcUnwrapNewtype_maybe :: FamInstEnvs + -> GlobalRdrEnv + -> Type + -> Maybe (GlobalRdrElt, TcCoercion, Type) +tcUnwrapNewtype_maybe faminsts rdr_env ty + | Just (tc,tys) <- tcSplitTyConApp_maybe ty + = firstJust (try_nt_unwrap tc tys) + (try_fam_unwrap tc tys) + | otherwise + = Nothing where - plus :: (Bag GlobalRdrElt, TcCoercion) -> (Bag GlobalRdrElt, TcCoercion) - -> (Bag GlobalRdrElt, TcCoercion) - plus (gres1, co1) (gres2, co2) = ( gres1 `unionBags` gres2 - , co1 `mkTransCo` co2 ) - - stepper :: NormaliseStepper (Bag GlobalRdrElt, TcCoercion) - stepper = unwrap_newtype `composeSteppers` unwrap_newtype_instance - - -- For newtype instances we take a double step or nothing, so that + -- For newtype /instances/ we take a double step or nothing, so that -- we don't return the representation type of the newtype instance, -- which would lead to terrible error messages - unwrap_newtype_instance rec_nts tc tys - | Just (tc', tys', co) <- tcLookupDataFamInst_maybe faminsts tc tys - = fmap (mkTransCo co) <$> unwrap_newtype rec_nts tc' tys' - | otherwise = NS_Done + try_fam_unwrap tc tys + | Just (tc', tys', fam_co) <- tcLookupDataFamInst_maybe faminsts tc tys + , Just (gre, nt_co, ty') <- try_nt_unwrap tc' tys' + = Just (gre, mkTransCo fam_co nt_co, ty') + | otherwise + = Nothing - unwrap_newtype rec_nts tc tys + try_nt_unwrap tc tys | Just con <- newTyConDataCon_maybe tc , Just gre <- lookupGRE_Name rdr_env (dataConName con) -- This is where we check that the -- data constructor is in scope - = (,) (unitBag gre) <$> unwrapNewTypeStepper rec_nts tc tys - + , Just (ty', co) <- instNewTyCon_maybe tc tys + = Just (gre, co, ty') | otherwise - = NS_Done + = Nothing {- ************************************************************************ ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -23,7 +23,7 @@ import GHC.Tc.Types.CtLoc import GHC.Tc.Types.Origin import GHC.Tc.Utils.Unify import GHC.Tc.Utils.TcType -import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe ) +import GHC.Tc.Instance.Family ( tcUnwrapNewtype_maybe ) import qualified GHC.Tc.Utils.Monad as TcM import GHC.Core.Type @@ -48,7 +48,6 @@ import GHC.Utils.Misc import GHC.Utils.Monad import GHC.Data.Pair -import GHC.Data.Bag import Control.Monad import Data.Maybe ( isJust, isNothing ) import Data.List ( zip4 ) @@ -334,24 +333,52 @@ can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 | Just ty1' <- coreView ty1 = can_eq_nc rewritten rdr_env envs ev eq_rel ty1' ps_ty1 ty2 ps_ty2 | Just ty2' <- coreView ty2 = can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2' ps_ty2 --- need to check for reflexivity in the ReprEq case. --- See Note [Eager reflexivity check] --- Check only when rewritten because the zonk_eq_types check in canEqNC takes --- care of the non-rewritten case. -can_eq_nc True _rdr_env _envs ev ReprEq ty1 _ ty2 _ - | ty1 `tcEqType` ty2 - = canEqReflexive ev ReprEq ty1 - --- When working with ReprEq, unwrap newtypes. --- See Note [Unwrap newtypes first] +-- Look for (N s1 .. sn) ~R# (N t1 .. tn) +-- where either si=ti +-- or N is phantom in i'th position +-- See Note [Solving newtype equalities: overview] +-- and (for details) Note [Eager newtype decomposition] +-- We try this /before/ attempting to unwrap N, because if N is +-- recursive, unwrapping will loop. +-- This /matters/ for newtypes, but is /safe/ for all types +can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _ + | ReprEq <- eq_rel + , TyConApp tc1 tys1 <- ty1 + , TyConApp tc2 tys2 <- ty2 + , tc1 == tc2 + , ok tys1 tys2 (tyConRoles tc1) + = canDecomposableTyConAppOK ev eq_rel tc1 (ty1,tys1) (ty2,tys2) + where + ok :: [TcType] -> [TcType] -> [Role] -> Bool + -- OK to decompose a representational equality + -- if the args are already equal + -- or are phantom role + -- See Note [Eager newtype decomposition] + -- You might think that representational role would also be OK, but + -- see Note [Even more eager newtype decomposition] + ok (ty1:tys1) (ty2:tys2) rs + | Phantom : rs' <- rs = ok tys1 tys2 rs' + | ty1 `tcEqType` ty2 = ok tys1 tys2 (drop 1 rs) + | otherwise = False + ok [] [] _ = True + ok _ _ _ = False -- Mis-matched lengths, just about possible because of + -- kind polymorphism. Anyway False is a safe result! + +-- Unwrap newtypes, when in ReprEq only +-- See Note [Solving newtype equalities: overview] +-- and (for details) Note [Unwrap newtypes first] -- This must be above the TyVarTy case, in order to guarantee (TyEq:N) +-- +-- We unwrap *one layer only*; `can_eq_newtype_nc` then loops back to +-- `can_eq_nc`. If there is a recursive newtype, so that we keep +-- unwrapping, the depth limit in `can_eq_newtype_nc` will blow up. can_eq_nc _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 | ReprEq <- eq_rel - , Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1 + , Just stuff1 <- tcUnwrapNewtype_maybe envs rdr_env ty1 = can_eq_newtype_nc rdr_env envs ev NotSwapped stuff1 ty2 ps_ty2 | ReprEq <- eq_rel - , Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2 + , Just stuff2 <- tcUnwrapNewtype_maybe envs rdr_env ty2 = can_eq_newtype_nc rdr_env envs ev IsSwapped stuff2 ty1 ps_ty1 -- Then, get rid of casts @@ -374,6 +401,11 @@ can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _ = do { setEqIfWanted ev (mkReflCPH eq_rel ty1) ; stopWith ev "Equal LitTy" } +can_eq_nc _rewritten _rdr_env _envs ev eq_rel + s1@ForAllTy{} _ + s2@ForAllTy{} _ + = can_eq_nc_forall ev eq_rel s1 s2 + -- Decompose FunTy: (s -> t) and (c => t) -- NB: don't decompose (Int -> blah) ~ (Show a => blah) can_eq_nc _rewritten _rdr_env _envs ev eq_rel @@ -401,19 +433,20 @@ can_eq_nc rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _ , rewritten || both_generative = canTyConApp ev eq_rel both_generative (ty1,tc1,tys1) (ty2,tc2,tys2) -can_eq_nc _rewritten _rdr_env _envs ev eq_rel - s1@ForAllTy{} _ - s2@ForAllTy{} _ - = can_eq_nc_forall ev eq_rel s1 s2 - --- See Note [Canonicalising type applications] about why we require rewritten types --- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families --- NB: Only decompose AppTy for nominal equality. --- See Note [Decomposing AppTy equalities] -can_eq_nc True _rdr_env _envs ev NomEq ty1 _ ty2 _ - | Just (t1, s1) <- tcSplitAppTy_maybe ty1 +-- Decompose applications +can_eq_nc rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _ + | True <- rewritten -- Why True? See Note [Canonicalising type applications] + -- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families + , Just (t1, s1) <- tcSplitAppTy_maybe ty1 , Just (t2, s2) <- tcSplitAppTy_maybe ty2 - = can_eq_app ev t1 s1 t2 s2 + = case eq_rel of + NomEq -> can_eq_app ev t1 s1 t2 s2 + -- Only decompose AppTy for nominal equality. + -- See (APT1) in Note [Decomposing AppTy equalities] + + ReprEq | ty1 `tcEqType` ty2 -> canEqReflexive ev ReprEq ty1 + -- tcEqType: see (APT2) in Note [Decomposing AppTy equalities] + | otherwise -> finishCanWithIrred ReprEqReason ev ------------------- -- Can't decompose. @@ -665,124 +698,18 @@ There are lots of wrinkles of course: the attempt if we fail. -} -{- Note [Unwrap newtypes first] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -See also Note [Decomposing newtype equalities] - -Consider - newtype N m a = MkN (m a) -N will get a conservative, Nominal role for its second parameter 'a', -because it appears as an argument to the unknown 'm'. Now consider - [W] N Maybe a ~R# N Maybe b - -If we /decompose/, we'll get - [W] a ~N# b - -But if instead we /unwrap/ we'll get - [W] Maybe a ~R# Maybe b -which in turn gives us - [W] a ~R# b -which is easier to satisfy. - -Conclusion: we must unwrap newtypes before decomposing them. This happens -in `can_eq_newtype_nc` - -We did flirt with making the /rewriter/ expand newtypes, rather than -doing it in `can_eq_newtype_nc`. But with recursive newtypes we want -to be super-careful about expanding! - - newtype A = MkA [A] -- Recursive! - - f :: A -> [A] - f = coerce - -We have [W] A ~R# [A]. If we rewrite [A], it'll expand to - [[[[[...]]]]] -and blow the reduction stack. See Note [Newtypes can blow the stack] -in GHC.Tc.Solver.Rewrite. But if we expand only the /top level/ of -both sides, we get - [W] [A] ~R# [A] -which we can, just, solve by reflexivity. - -So we simply unwrap, on-demand, at top level, in `can_eq_newtype_nc`. - -This is all very delicate. There is a real risk of a loop in the type checker -with recursive newtypes -- but I think we're doomed to do *something* -delicate, as we're really trying to solve for equirecursive type -equality. Bottom line for users: recursive newtypes do not play well with type -inference for representational equality. See also Section 5.3.1 and 5.3.4 of -"Safe Zero-cost Coercions for Haskell" (JFP 2016). - -See also Note [Decomposing newtype equalities]. - ---- Historical side note --- - -We flirted with doing /both/ unwrap-at-top-level /and/ rewrite-deeply; -see #22519. But that didn't work: see discussion in #22924. Specifically -we got a loop with a minor variation: - f2 :: a -> [A] - f2 = coerce - -Note [Eager reflexivity check] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have - - newtype X = MkX (Int -> X) - -and - - [W] X ~R X - -Naively, we would start unwrapping X and end up in a loop. Instead, -we do this eager reflexivity check. This is necessary only for representational -equality because the rewriter technology deals with the similar case -(recursive type families) for nominal equality. - -Note that this check does not catch all cases, but it will catch the cases -we're most worried about, types like X above that are actually inhabited. - -Here's another place where this reflexivity check is key: -Consider trying to prove (f a) ~R (f a). The AppTys in there can't -be decomposed, because representational equality isn't congruent with respect -to AppTy. So, when canonicalising the equality above, we get stuck and -would normally produce a CIrredCan. However, we really do want to -be able to solve (f a) ~R (f a). So, in the representational case only, -we do a reflexivity check. - -(This would be sound in the nominal case, but unnecessary, and I [Richard -E.] am worried that it would slow down the common case.) - - Note [Newtypes can blow the stack] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have - - newtype X = MkX (Int -> X) - newtype Y = MkY (Int -> Y) - -and now wish to prove - - [W] X ~R Y - -This Wanted will loop, expanding out the newtypes ever deeper looking -for a solid match or a solid discrepancy. Indeed, there is something -appropriate to this looping, because X and Y *do* have the same representation, -in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized -coercion will ever witness it. This loop won't actually cause GHC to hang, -though, because we check our depth in `can_eq_newtype_nc`. --} - ------------------------ -- | We're able to unwrap a newtype. Update the bits accordingly. can_eq_newtype_nc :: GlobalRdrEnv -> FamInstEnvs -> CtEvidence -- ^ :: ty1 ~ ty2 -> SwapFlag - -> ((Bag GlobalRdrElt, TcCoercion), TcType) -- ^ :: ty1 ~ ty1' + -> (GlobalRdrElt, TcCoercion, TcType) -- ^ :: ty1 ~ ty1' -> TcType -- ^ ty2 -> TcType -- ^ ty2, with type synonyms -> TcS (StopOrContinue (Either IrredCt EqCt)) -can_eq_newtype_nc rdr_env envs ev swapped ((gres, co1), ty1') ty2 ps_ty2 +can_eq_newtype_nc rdr_env envs ev swapped (gre, co1, ty1') ty2 ps_ty2 = do { traceTcS "can_eq_newtype_nc" $ - vcat [ ppr ev, ppr swapped, ppr co1, ppr gres, ppr ty1', ppr ty2 ] + vcat [ ppr ev, ppr swapped, ppr co1, ppr gre, ppr ty1', ppr ty2 ] -- Check for blowing our stack, and increase the depth -- See Note [Newtypes can blow the stack] @@ -791,14 +718,20 @@ can_eq_newtype_nc rdr_env envs ev swapped ((gres, co1), ty1') ty2 ps_ty2 -- Next, we record uses of newtype constructors, since coercing -- through newtypes is tantamount to using their constructors. - ; recordUsedGREs gres + ; recordUsedGRE gre ; let redn1 = mkReduction co1 ty1' redn2 = mkReflRedn Representational ps_ty2 - ; new_ev <- rewriteEqEvidence ev' swapped redn1 redn2 + ; new_ev <- rewriteEqEvidence ev' (flipSwap swapped) redn2 redn1 emptyCoHoleSet - ; can_eq_nc False rdr_env envs new_ev ReprEq ty1' ty1' ty2 ps_ty2 } + -- ty1 is the one being unwrapped. Loop back to can_eq_nc with + -- the arguments flipped so that ty2 is looked at first in the + -- next iteration. That way if we have (Id Rec) ~R# (Id Rec) + -- where newtype Id a = MkId a and newtype Rec = MkRec Rec + -- we'll unwrap both Ids, then spot Rec=Rec. + -- See (END2) in Note [Eager newtype decomposition] + ; can_eq_nc False rdr_env envs new_ev ReprEq ty2 ps_ty2 ty1' ty1' } --------- -- ^ Decompose a type application. @@ -896,7 +829,7 @@ canTyConApp ev eq_rel both_generative (ty1,tc1,tys1) (ty2,tc2,tys2) | tc1 == tc2 , tys1 `equalLength` tys2 = do { inerts <- getInertSet - ; if can_decompose inerts + ; if canDecomposeTcApp ev eq_rel tc1 inerts then canDecomposableTyConAppOK ev eq_rel tc1 (ty1,tys1) (ty2,tys2) else assert (eq_rel == ReprEq) $ canEqSoftFailure ReprEqReason ev ty1 ty2 } @@ -918,19 +851,31 @@ canTyConApp ev eq_rel both_generative (ty1,tc1,tys1) (ty2,tc2,tys2) | otherwise = canEqSoftFailure ReprEqReason ev ty1 ty2 - where + +canDecomposeTcApp :: CtEvidence -> EqRel -> TyCon -> InertSet -> Bool -- See Note [Decomposing TyConApp equalities] -- and Note [Decomposing newtype equalities] - can_decompose inerts - = isInjectiveTyCon tc1 (eqRelRole eq_rel) - || (assert (eq_rel == ReprEq) $ - -- assert: isInjectiveTyCon is always True for Nominal except - -- for type synonyms/families, neither of which happen here - -- Moreover isInjectiveTyCon is True for Representational - -- for algebraic data types. So we are down to newtypes - -- and data families. - ctEvFlavour ev == Wanted && noGivenNewtypeReprEqs tc1 inerts) - -- See Note [Decomposing newtype equalities] (EX2) +canDecomposeTcApp ev eq_rel tc inerts + | isInjectiveTyCon tc eq_role = True + | isGiven ev = False + | otherwise = assert (eq_rel == ReprEq) $ + assert (isNewTyCon tc || + isDataFamilyTyCon tc || + isAbstractTyCon tc ) $ + noGivenNewtypeReprEqs tc inerts + -- The otherwise case deals with + -- * Representational equalities (T s1..sn) ~R# (T t1..tn) + -- * where T is a newtype or data family or abstract + -- Why? isInjectiveTyCon is always True for eq_rel=NomEq except for type + -- synonyms/families, neither of which happen here; and isInjectiveTyCon + -- is True for Representational for algebraic data types. + -- + -- noGivenNewtypeReprEqs: see Note [Decomposing newtype equalities] (EX4) + -- Decomposing here is a last resort + -- NB: despite all these tests, decomposition of data familiies is alas + -- /still/ incomplete. See (EX3) in Note [Decomposing newtype equalities] + where + eq_role = eqRelRole eq_rel {- Note [Canonicalising TyCon/TyCon equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -945,7 +890,7 @@ Suppose we are canonicalising [W] Int ~R# DF (TF a). Then (TC1) We might have an inert Given (a ~# Char), so if we rewrote the wanted (i.e. went around again in `can_eq_nc` with `rewritten`=True, we'd get [W] Int ~R# DF Bool - and then the `tcTopNormaliseNewTypeTF_maybe` call would fire and + and then the `tcUnwrapNewtype_maybe` call would fire and we'd unwrap the newtype. So we must do that "go round again" bit. Hence the complicated guard (rewritten || both_generative) in `can_eq_nc`. @@ -1114,6 +1059,110 @@ This is not a very big deal. It reduces the number of solver steps in the test RaeJobTalk from 1830 to 1815, a 1% reduction. But still, it doesn't cost anything either. +Note [Solving newtype equalities: overview] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +This Note also applies to data families, which we treat like +newtype in case of 'newtype instance'. + +Consider (N s1..sn) ~R# (N t1..tn), where N is a newtype. +We try three strategies, in order: + +(NTE1) Decompose if the si/ti are either (a) identical or (b) phantom. This step + avoids unwrapping, which allows success in some cases where the newtype + would unwrap infinitely. See Note [Eager newtype decomposition] + +(NTE2) Unwrap the newtype, if possible. Always good, but it requires the data + constructor to be in scope. See Note [Unwrap newtypes first]. + + If the newtype is recursive, this unwrapping might go on forever, + so `can_eq_newtype_nc` has a depth bound check. + See Note [Newtypes can blow the stack] + +(NTE3) Decompose the tycon application. This step is a last resort, because it + risks losing completeness. See Note [Decomposing newtype equalities] + +Note [Newtypes can blow the stack] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have + + newtype X = MkX (Int -> X) + newtype Y = MkY (Int -> Y) + +and now wish to prove + + [W] X ~R Y + +This Wanted will loop, expanding out the newtypes ever deeper looking +for a solid match or a solid discrepancy. Indeed, there is something +appropriate to this looping, because X and Y *do* have the same representation, +in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized +coercion will ever witness it. This loop won't actually cause GHC to hang, +though, because we check our depth in `can_eq_newtype_nc`. + +However, GHC can still loop badly: see #26757, which shows how we can create +types whose size is exponential in the depth of newtype expansion. That makes +GHC go out to lunch unless the depth bound is very small indeed; and a small +depth bound makes perfectly legitimate programs fail. We don't have solid +solution for this, but it's rare. + +Note [Unwrap newtypes first] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +See also Note [Decomposing newtype equalities] + +Consider + newtype N m a = MkN (m a) +N will get a conservative, Nominal role for its second parameter 'a', +because it appears as an argument to the unknown 'm'. Now consider + [W] N Maybe a ~R# N Maybe b + +If we /decompose/, we'll get + [W] a ~N# b + +But if instead we /unwrap/ we'll get + [W] Maybe a ~R# Maybe b +which in turn gives us + [W] a ~R# b +which is easier to satisfy. + +Conclusion: we must unwrap newtypes before decomposing them. This happens +in `can_eq_newtype_nc` + +We did flirt with making the /rewriter/ expand newtypes, rather than +doing it in `can_eq_newtype_nc`. But with recursive newtypes we want +to be super-careful about expanding! + + newtype A = MkA [A] -- Recursive! + + f :: A -> [A] + f = coerce + +We have [W] A ~R# [A]. If we rewrite [A], it'll expand to + [[[[[...]]]]] +and blow the reduction stack. See Note [Newtypes can blow the stack] +in GHC.Tc.Solver.Rewrite. But if we expand only the /top level/ of +both sides, we get + [W] [A] ~R# [A] +which we can, just, solve by reflexivity. + +So we simply unwrap, on-demand, at top level, in `can_eq_newtype_nc`. + +This is all very delicate. There is a real risk of a loop in the type checker +with recursive newtypes -- but I think we're doomed to do *something* +delicate, as we're really trying to solve for equirecursive type +equality. Bottom line for users: recursive newtypes do not play well with type +inference for representational equality. See also Section 5.3.1 and 5.3.4 of +"Safe Zero-cost Coercions for Haskell" (JFP 2016). + +See also Note [Decomposing newtype equalities]. + +--- Historical side note --- + +We flirted with doing /both/ unwrap-at-top-level /and/ rewrite-deeply; +see #22519. But that didn't work: see discussion in #22924. Specifically +we got a loop with a minor variation: + f2 :: a -> [A] + f2 = coerce + Note [Decomposing newtype equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ This Note also applies to data families, which we treat like @@ -1133,7 +1182,10 @@ if the newtype is abstract (so can't be unwrapped) we can only solve the equality by (a) using a Given or (b) decomposition. If (a) is impossible (e.g. no Givens) then (b) is safe albeit potentially incomplete. -There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: +Remember: Decomposing Wanteds is always /sound/. + This Note is only about /completeness/. + +There are three ways in which decomposing [W] (N ty1) ~r (N ty2) could be incomplete: * Incompleteness example (EX1): unwrap first newtype Nt a = MkNt (Id a) @@ -1146,7 +1198,7 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: which is unsatisfiable. Unwrapping, though, leads to a solution. CONCLUSION: always unwrap newtypes before attempting to decompose - them. This is done in can_eq_nc. Of course, we can't unwrap if the data + them. This is done in `can_eq_nc`. Of course, we can't unwrap if the data constructor isn't in scope. See Note [Unwrap newtypes first]. * Incompleteness example (EX2): prioritise Nominal equalities. See #24887 @@ -1154,20 +1206,32 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: data instance D Int = MkD1 (D Char) data instance D Bool = MkD2 (D Char) Now suppose we have - [W] g1: D Int ~R# D a - [W] g2: a ~# Bool - If we solve g2 first, giving a:=Bool, then we can solve g1 easily: + [W] g1: D Int ~R# D alpha + [W] g2: alpha ~# Bool + If we solve g2 first, giving alpha:=Bool, then we can solve g1 easily: D Int ~R# D Char ~R# D Bool by newtype unwrapping. BUT: if we instead attempt to solve g1 first, we can unwrap the LHS (only) - leaving [W] D Char ~#R D Bool - If we decompose now, we'll get (Char ~R# Bool), which is insoluble. + leaving [W] D Char ~#R D alpha + If we decompose now, we'll get (Char ~R# alpha), which is insoluble, since + alpha turns out to be Bool. CONCLUSION: prioritise nominal equalites in the work list. See Note [Prioritise equalities] in GHC.Tc.Solver.InertSet. -* Incompleteness example (EX3): check available Givens +* Incompleteness example (EX3) + Sadly, the fix for (EX2) is /still/ incomplete: + * The equality `g2` might be in a sibling implication constraint, + invisible for now. + * The equality `g2` might be hidden in a class constraint: + class C a + instance (a~Bool) => C [a] + [W] g3 :: C [alpha] + When we get around to solving `g3` we'll discover (g2:alpha~Bool) + So that's a real infelicity in the solver. + +* Incompleteness example (EX4): check available Givens newtype Nt a = Mk Bool -- NB: a is not used in the RHS, type role Nt representational -- but the user gives it an R role anyway @@ -1230,18 +1294,48 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: un-expanded equality superclasses; but only in some very obscure recursive-superclass situations. - Yet another approach (!) is described in - Note [Decomposing newtypes a bit more aggressively]. - -Remember: decomposing Wanteds is always /sound/. This Note is -only about /completeness/. - -Note [Decomposing newtypes a bit more aggressively] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -IMPORTANT: the ideas in this Note are *not* implemented. Instead, the -current approach is detailed in Note [Decomposing newtype equalities] -and Note [Unwrap newtypes first]. -For more details about the ideas in this Note see +Note [Eager newtype decomposition] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider [W] (Rec1 Int) ~R# (Rec1 Bool) where + newtype Rec1 a = MkRec1 (Rec1 a) + +If we apply (NTE2), we'll loop because `Rec1` unwraps forever. +But the role of `a` is inferred as Phantom, so it sound and complete +to decompose via `canDecomposableTyConAppOK`, giving nothing at all +(because of the Phantom role). So we win. + +Another useful special case is + newtype Rec = MkRec Rec +where there are no arguments. + +So we do an eager decomposition check in step (NTE1), /before/ trying to unwrap +in (NTE2). This is a HACK: it catches some cases of recursion, but not all. +But it's a hack that has been in GHC for some time. + +Wrinkles + +(END1) The eager-decomposition step is fine for all data types, not just newtypes. + +(END2) Consider newtype Id a = MkId a -- Not recusrive + newtype Rec = MkRec Rec -- Recursive + and [W] Id Rec ~R# Rec + Then (NTE1) will fail; (NTE2) will succeed in unwrapping Id, generating + [W] Rec ~R# Rec; and (NTE1) will succeed when we go round the loop. + + What about [W] Rec ~R# Id Rec? + Here (NTE1) will fail again; (NTE2) will succeed, by unwrapping Rec, to get + Rec again. If we just iterate with [W] Rec ~R# Id Rec, we'll be stuck in + a loop. Instead we want to flip the constraint round so we get + [W] Id Rec ~R# Rec. Now we win. See the flipping in `can_eq_newtype_nc`. + +(END3) See Note [Even more eager newtype decomposition] + +Note [Even more eager newtype decomposition] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Eager newtype decomposition] decomposes [W] (N s ~R# N t) if N's role is +phantom. We could go further and decompose if the arguments are all Phantom +/or/ Representational. This is not implemented. For more details about the +ideas in this Note see * GHC propoosal: https://github.com/ghc-proposals/ghc-proposals/pull/549 * issue #22441 * discussion on !9282. @@ -1249,9 +1343,8 @@ For more details about the ideas in this Note see Consider [G] c, [W] (IO Int) ~R (IO Age) where IO is abstract, and newtype Age = MkAge Int -- Not abstract -With the above rules, if there any Given Irreds, -the Wanted is insoluble because we can't decompose it. But in fact, -if we look at the defn of IO, roughly, +With the above rules, if there any Given Irreds, the Wanted is insoluble because +we can't decompose it. But in fact, if we look at the defn of IO, roughly, newtype IO a = State# -> (State#, a) we can see that decomposing [W] (IO Int) ~R (IO Age) to [W] Int ~R Age @@ -1260,41 +1353,26 @@ IO's argment is representational. Hence: DecomposeNewtypeIdea: decompose [W] (N s1 .. sn) ~R (N t1 .. tn) - if the roles of all N's arguments are representational - -If N's arguments really /are/ representational this will not lose -completeness. Here "really are representational" means "if you expand -all newtypes in N's RHS, we'd infer a representational role for each -of N's type variables in that expansion". See Note [Role inference] -in GHC.Tc.TyCl.Utils. - -But the user might /override/ a phantom role with an explicit role -annotation, and then we could (obscurely) get incompleteness. -Consider - - module A( silly, T ) where - newtype T a = MkT Int - type role T representational -- Override phantom role - - silly :: Coercion (T Int) (T Bool) - silly = Coercion -- Typechecks by unwrapping the newtype + if the roles of all N's arguments are representational (or phantom) - data Coercion a b where -- Actually defined in Data.Type.Coercion - Coercion :: Coercible a b => Coercion a b +If N's arguments really /are/ representational this will not lose completeness. +Here "really are representational" means "if you expand all newtypes in N's RHS, +we'd infer a representational role for each of N's type variables in that +expansion". See Note [Role inference] in GHC.Tc.TyCl.Utils. - module B where - import A - f :: T Int -> T Bool - f = case silly of Coercion -> coerce +But the user might /override/ a phantom role with an explicit role annotation, +and then we could (obscurely) get incompleteness. Consider (#9117): + newtype Phant a = MkPhant Char + type role Phant representational -- Override phantom role + [W] Phant Int ~R# Phant Char -Here the `coerce` gives [W] (T Int) ~R (T Bool) which, if we decompose, -we'll get stuck with (Int ~R Bool). Instead we want to use the -[G] (T Int) ~R (T Bool), which will be in the Irreds. +We do not want to decompose to Int ~R# Char; better to unwrap Summary: we could adopt (DecomposeNewtypeIdea), at the cost of a very obscure incompleteness (above). But no one is reporting a problem from the lack of decompostion, so we'll just leave it for now. This long Note is just to record the thinking for our future selves. +---- End of speculative aside --------- Note [Decomposing AppTy equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1305,12 +1383,12 @@ Note [Decomposing TyConApp equalities]. We have s1 t1 ~N s2 t2 ==> s1 ~N s2, t1 ~N t2 (CO_LEFT, CO_RIGHT) In the first of these, why do we need Nominal equality in (t1 ~N t2)? -See {2} below. +See (APT3) below. For sound and complete solving, we need both directions to decompose. So: * At nominal role, all is well: we have both directions. -* At representational role, decomposition of Givens is unsound (see {1} below), - and decomposition of Wanteds is incomplete. +* At representational role, decomposition of Givens is unsound + (see (APT1) below), and decomposition of Wanteds is incomplete. Here is an example of the incompleteness for Wanteds: @@ -1325,7 +1403,7 @@ Suppose we see w1 before w2. If we decompose, using AppCo to prove w1, we get [W] w4 :: b ~N a Note that w4 is *nominal*. A nominal role here is necessary because AppCo -requires a nominal role on its second argument. (See {2} for an example of +requires a nominal role on its second argument. (See (APT3) for an example of why.) Now we are stuck, because w4 is insoluble. On the other hand, if we see w2 first, setting alpha := Maybe, all is well, as we can decompose Maybe b ~R Maybe a into b ~R a. @@ -1348,12 +1426,21 @@ Bottom line: the lack of an equation in can_eq_nc Extra points -{1} Decomposing a Given AppTy over a representational role is simply +(APT1) Decomposing a Given AppTy at Representational role is simply unsound. For example, if we have co1 :: Phant Int ~R a Bool (for the newtype Phant, above), then we surely don't want any relationship between Int and Bool, lest we also have co2 :: Phant ~ a around. -{2} The role on the AppCo coercion is a conservative choice, because we don't + For Wanteds, decomposing an AppTy at Representational role is incomplete. + +(APT2) What if we have [W] (f a) ~R# (f a) + We can't decompose because of (APT1). But it's silly to reject. So we do + an equality check, in the AppTy/AppTy case of `can_eq_nc`. + + (It would be sound to do this reflexivity check in the Nominal case too, + but not necessary, and there might be a perf cost.) + +(APT3) The role on the AppCo coercion is a conservative choice, because we don't know the role signature of the function. For example, let's assume we could have a representational role on the second argument of AppCo. Then, consider ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -22,7 +22,7 @@ module GHC.Tc.Solver.Monad ( updWorkListTcS, pushLevelNoWorkList, pushTcLevelM_, - runTcPluginTcS, recordUsedGREs, + runTcPluginTcS, recordUsedGRE, matchGlobalInst, TcM.ClsInstResult(..), QCInst(..), @@ -1519,18 +1519,16 @@ tcLookupTyCon n = wrapTcS $ TcM.tcLookupTyCon n -- pure veneer of TcS. But it's just about warnings around unused imports -- and local constructors (GHC will issue fewer warnings than it otherwise -- might), so it's not worth losing sleep over. -recordUsedGREs :: Bag GlobalRdrElt -> TcS () -recordUsedGREs gres - = do { wrapTcS $ TcM.addUsedGREs NoDeprecationWarnings gre_list +recordUsedGRE :: GlobalRdrElt -> TcS () +recordUsedGRE gre + = do { wrapTcS $ TcM.addUsedGRE NoDeprecationWarnings gre -- If a newtype constructor was imported, don't warn about not -- importing it... - ; wrapTcS $ traverse_ (TcM.keepAlive . greName) gre_list } + ; wrapTcS $ TcM.keepAlive (greName gre) } -- ...and similarly, if a newtype constructor was defined in the same -- module, don't warn about it being unused. -- See Note [Tracking unused binding and imports] in GHC.Tc.Utils. - where - gre_list = bagToList gres -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== docs/users_guide/9.16.1-notes.rst ===================================== @@ -30,6 +30,18 @@ Language - The extension :extension:`ExplicitNamespaces` now allows namespace-specified wildcards ``type ..`` and ``data ..`` in import and export lists. +- Implicit parameters and ``ImpredicativeTypes``. GHC now knows + that if ``?foo::S`` is coecible to ``?foo::T`` only if ``S`` is coercible to ``T``. + Example (from :ghc-ticket:`#26737`):: + + {-# LANGUAGE ImplicitParams, ImpredicativeTypes #-} + newtype N = MkN Int + test :: ((?foo::N) => Bool) -> ((?foo::Int) => Bool) + test = coerce + + This is achieved by arranging that ``?foo :: T`` has a representational + role for ``T``. + Compiler ~~~~~~~~ ===================================== libraries/ghc-internal/ghc-internal.cabal.in ===================================== @@ -343,6 +343,7 @@ Library GHC.Internal.CString GHC.Internal.Classes + GHC.Internal.Classes.IP GHC.Internal.Debug GHC.Internal.Magic GHC.Internal.Magic.Dict ===================================== libraries/ghc-internal/src/GHC/Internal/Classes.hs ===================================== @@ -1,10 +1,9 @@ {-# LANGUAGE Trustworthy #-} {-# LANGUAGE NoImplicitPrelude, MagicHash, StandaloneDeriving, BangPatterns, KindSignatures, DataKinds, ConstraintKinds, - MultiParamTypeClasses, FunctionalDependencies #-} -{-# LANGUAGE UnboxedTuples #-} -{-# LANGUAGE AllowAmbiguousTypes #-} - -- ip :: IP x a => a is strictly speaking ambiguous, but IP is magic + MultiParamTypeClasses, FunctionalDependencies, + UnboxedTuples #-} + {-# LANGUAGE UndecidableSuperClasses #-} -- Because of the type-variable superclasses for tuples @@ -142,6 +141,7 @@ import GHC.Internal.Prim import GHC.Internal.Tuple import GHC.Internal.CString (unpackCString#) import GHC.Internal.Types +import GHC.Internal.Classes.IP infix 4 ==, /=, <, <=, >=, > infixr 3 && @@ -149,12 +149,6 @@ infixr 2 || default () -- Double isn't available yet --- | The syntax @?x :: a@ is desugared into @IP "x" a@ --- IP is declared very early, so that libraries can take --- advantage of the implicit-call-stack feature -class IP (x :: Symbol) a | x -> a where - ip :: a - {- $matching_overloaded_methods_in_rules Matching on class methods (e.g. @(==)@) in rewrite rules tends to be a bit ===================================== libraries/ghc-internal/src/GHC/Internal/Classes/IP.hs ===================================== @@ -0,0 +1,87 @@ +{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE NoImplicitPrelude, MagicHash, StandaloneDeriving, BangPatterns, + KindSignatures, DataKinds, ConstraintKinds, + MultiParamTypeClasses, FunctionalDependencies #-} + +{-# LANGUAGE AllowAmbiguousTypes, RoleAnnotations, IncoherentInstances #-} + -- LANGUAGE pragmas: see Note [IP: implicit parameter class] + +{-# OPTIONS_HADDOCK not-home #-} +----------------------------------------------------------------------------- +-- | +-- Module : GHC.Internal.Classes.IP +-- Copyright : (c) The University of Glasgow, 1992-2002 +-- License : see libraries/base/LICENSE +-- +-- Maintainer : ghc-devs(a)haskell.org +-- Stability : internal +-- Portability : non-portable (GHC extensions) +-- +-- Basic classes. +-- Do not import this module directly. It is an GHC internal only +-- module. Some of its contents are instead available from @Prelude@ +-- and @GHC.Int@. +-- +----------------------------------------------------------------------------- + +module GHC.Internal.Classes.IP( IP(..)) where + +import GHC.Internal.Types + + +default () -- Double isn't available yet + +-- | The syntax @?x :: a@ is desugared into @IP "x" a@ +-- IP is declared very early, so that libraries can take +-- advantage of the implicit-call-stack feature +type role IP nominal representational -- See (IPRoles) +class IP (x :: Symbol) a | x -> a where + ip :: a + +{- Note [IP: implicit parameter class] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +An implicit parameter constraint (?foo::ty) is just short for + + IP "foo" ty + +where ghc-internal:GHC.Internal.Classes.IP is a special class that +GHC knows about, defined in this module. + +* It is a unary type class, with one method `ip`, so it has no cost. + For example, (?foo::Int) is represented just by an Int. + +* Criticially, it has a functional dependency: + class IP (x :: Symbol) a | x -> a where ... + So if we have + [G] IP "foo" Int + [W] IP "foo" alpha + the fundep wil lgive us alpha ~ Int, as desired. + +* The solver has a number of special cases for implicit parameters, + mainly because a binding (let ?foo::Int = rhs in body) + is like a local instance declaration for IP. Search for uses + of `isIPClass`. + +Wrinkles + +(IPAmbiguity) The single method of IP has an ambiguous type + ip :: forall a. IP s a => a + Hence the LANGUAGE pragama AllowAmbiguousTypes. + The method `ip` is never called by the user, so ambiguity doesn't matter. + +(IPRoles) IP has a role annotation. Why? See #26737. We want + [W] IP "foo" t1 ~R# IP "foo" t2 + to decompose to give [W] IP t1 ~R# t2, using /representational/ + equality for (t1 ~R# t2) not nominal. + + This usually gives a complaint about incoherence, because in general + (t1 ~R# t2) does NOT imply (C t1) ~R# (C t2) for any normal class. + But it does for IP, because instance selection is controlled by the Symbol, + not the type of the payload. Hence LANGUAGE pragma IncoherentInstances. + (It is unfortunate that we need a module-wide IncoherentInstances here; + see #17167.) + + Side note: arguably this treatment could be applied to any class + with a functional dependency; but for now we restrict it to IP. +-} + ===================================== testsuite/tests/deriving/should_fail/T8984.stderr ===================================== @@ -1,6 +1,6 @@ T8984.hs:7:46: error: [GHC-18872] - • Couldn't match representation of type: cat a (N cat a Int) - with that of: cat a (cat a Int) + • Couldn't match representation of type: cat a (cat a Int) + with that of: cat a (N cat a Int) arising from the coercion of the method ‘app’ from type ‘cat a (cat a Int)’ to type ‘N cat a (N cat a Int)’ Note: We cannot know what roles the parameters to ‘cat a’ have; ===================================== testsuite/tests/deriving/should_fail/deriving-via-fail.stderr ===================================== @@ -1,12 +1,12 @@ deriving-via-fail.hs:10:34: error: [GHC-10283] - • Couldn't match representation of type ‘a’ with that of ‘b’ + • Couldn't match representation of type ‘b’ with that of ‘a’ arising from the coercion of the method ‘showsPrec’ from type ‘Int -> Identity b -> ShowS’ to type ‘Int -> Foo1 a -> ShowS’ - ‘a’ is a rigid type variable bound by + ‘b’ is a rigid type variable bound by the deriving clause for ‘Show (Foo1 a)’ at deriving-via-fail.hs:10:34-37 - ‘b’ is a rigid type variable bound by + ‘a’ is a rigid type variable bound by the deriving clause for ‘Show (Foo1 a)’ at deriving-via-fail.hs:10:34-37 • When deriving the instance for (Show (Foo1 a)) ===================================== testsuite/tests/deriving/should_fail/deriving-via-fail4.stderr ===================================== @@ -1,17 +1,17 @@ deriving-via-fail4.hs:15:12: error: [GHC-18872] - • Couldn't match representation of type ‘Int’ with that of ‘Char’ + • Couldn't match representation of type ‘Char’ with that of ‘Int’ arising from the coercion of the method ‘==’ from type ‘Char -> Char -> Bool’ to type ‘F1 -> F1 -> Bool’ • When deriving the instance for (Eq F1) deriving-via-fail4.hs:18:13: error: [GHC-10283] - • Couldn't match representation of type ‘a1’ with that of ‘a2’ + • Couldn't match representation of type ‘a2’ with that of ‘a1’ arising from the coercion of the method ‘c’ from type ‘a -> a -> Bool’ to type ‘a -> F2 a1 -> Bool’ - ‘a1’ is a rigid type variable bound by + ‘a2’ is a rigid type variable bound by the deriving clause for ‘C a (F2 a1)’ at deriving-via-fail4.hs:18:13-15 - ‘a2’ is a rigid type variable bound by + ‘a1’ is a rigid type variable bound by the deriving clause for ‘C a (F2 a1)’ at deriving-via-fail4.hs:18:13-15 • When deriving the instance for (C a (F2 a1)) ===================================== testsuite/tests/deriving/should_fail/deriving-via-fail5.stderr ===================================== @@ -1,10 +1,10 @@ deriving-via-fail5.hs:8:1: error: [GHC-10283] - • Couldn't match representation of type ‘a’ with that of ‘b’ + • Couldn't match representation of type ‘b’ with that of ‘a’ arising from a use of ‘GHC.Internal.Prim.coerce’ - ‘a’ is a rigid type variable bound by + ‘b’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) - ‘b’ is a rigid type variable bound by + ‘a’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) • In the expression: @@ -25,12 +25,12 @@ deriving-via-fail5.hs:8:1: error: [GHC-10283] (bound at deriving-via-fail5.hs:8:1) deriving-via-fail5.hs:8:1: error: [GHC-10283] - • Couldn't match representation of type ‘a’ with that of ‘b’ + • Couldn't match representation of type ‘b’ with that of ‘a’ arising from a use of ‘GHC.Internal.Prim.coerce’ - ‘a’ is a rigid type variable bound by + ‘b’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) - ‘b’ is a rigid type variable bound by + ‘a’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) • In the expression: @@ -48,12 +48,12 @@ deriving-via-fail5.hs:8:1: error: [GHC-10283] show :: Foo4 a -> String (bound at deriving-via-fail5.hs:8:1) deriving-via-fail5.hs:8:1: error: [GHC-10283] - • Couldn't match representation of type ‘a’ with that of ‘b’ + • Couldn't match representation of type ‘b’ with that of ‘a’ arising from a use of ‘GHC.Internal.Prim.coerce’ - ‘a’ is a rigid type variable bound by + ‘b’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) - ‘b’ is a rigid type variable bound by + ‘a’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) • In the expression: ===================================== testsuite/tests/interface-stability/base-exports.stdout ===================================== @@ -3293,6 +3293,7 @@ module GHC.Base where {-# MINIMAL fmap #-} type IO :: * -> * newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #)) + type role IP nominal representational type IP :: Symbol -> * -> Constraint class IP x a | x -> a where ip :: a ===================================== testsuite/tests/interface-stability/base-exports.stdout-mingw32 ===================================== @@ -3293,6 +3293,7 @@ module GHC.Base where {-# MINIMAL fmap #-} type IO :: * -> * newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #)) + type role IP nominal representational type IP :: Symbol -> * -> Constraint class IP x a | x -> a where ip :: a ===================================== testsuite/tests/interface-stability/base-exports.stdout-ws-32 ===================================== @@ -3293,6 +3293,7 @@ module GHC.Base where {-# MINIMAL fmap #-} type IO :: * -> * newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #)) + type role IP nominal representational type IP :: Symbol -> * -> Constraint class IP x a | x -> a where ip :: a ===================================== testsuite/tests/interface-stability/ghc-prim-exports.stdout ===================================== @@ -1171,6 +1171,7 @@ module GHC.Classes where (==) :: a -> a -> GHC.Internal.Types.Bool (/=) :: a -> a -> GHC.Internal.Types.Bool {-# MINIMAL (==) | (/=) #-} + type role IP nominal representational type IP :: GHC.Internal.Types.Symbol -> * -> Constraint class IP x a | x -> a where ip :: a ===================================== testsuite/tests/interface-stability/ghc-prim-exports.stdout-mingw32 ===================================== @@ -1171,6 +1171,7 @@ module GHC.Classes where (==) :: a -> a -> GHC.Internal.Types.Bool (/=) :: a -> a -> GHC.Internal.Types.Bool {-# MINIMAL (==) | (/=) #-} + type role IP nominal representational type IP :: GHC.Internal.Types.Symbol -> * -> Constraint class IP x a | x -> a where ip :: a ===================================== testsuite/tests/perf/should_run/all.T ===================================== @@ -128,7 +128,7 @@ test('T4978', ['-O2']) test('T5205', - [collect_stats('bytes allocated',5), + [collect_stats('bytes allocated',15), only_ways(['normal', 'optasm']) ], compile_and_run, ===================================== testsuite/tests/th/TH_implicitParams.stdout ===================================== @@ -1,5 +1,5 @@ -Main.funcToReify :: GHC.Internal.Classes.IP "z" - GHC.Internal.Types.Int => +Main.funcToReify :: GHC.Internal.Classes.IP.IP "z" + GHC.Internal.Types.Int => GHC.Internal.Types.Int 5 1 ===================================== testsuite/tests/typecheck/should_compile/T26737.hs ===================================== @@ -0,0 +1,10 @@ +{-# LANGUAGE ImpredicativeTypes, ImplicitParams #-} + +module T26737 where + +import Data.Coerce + +newtype Foo = MkFoo Int + +b :: ((?foo :: Foo) => Int) -> ((?foo :: Int) => Int) +b = coerce @(((?foo :: Foo) => Int)) @(((?foo :: Int) => Int)) ===================================== testsuite/tests/typecheck/should_compile/T26746.hs ===================================== @@ -0,0 +1,33 @@ +module T26746 where + +import Data.Coerce + +newtype Foo a = Foo (Foo a) +newtype Age = MkAge Int + +ex1 :: (Foo Age) -> (Foo Int) +ex1 = coerce + +newtype Womble a = MkWomble (Foo a) + +ex2 :: Womble (Foo Age) -> (Foo Int) +ex2 = coerce + +ex3 :: (Foo Age) -> Womble (Foo Int) +ex3 = coerce + + +-- Surprisingly this one works: +newtype Z1 = MkZ1 Z2 +newtype Z2 = MKZ2 Z1 + +ex4 :: Z1 -> Z2 +ex4 = coerce + +-- But this one does not (commented out) +-- newtype Y1 = MkY1 Y2 +-- newtype Y2 = MKY2 Y3 +-- newtype Y3 = MKY3 Y1 +-- +-- ex5 :: Y1 -> Y3 +-- ex5 = coerce ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -957,3 +957,5 @@ test('T17705', normal, compile, ['']) test('T14745', normal, compile, ['']) test('T26451', normal, compile, ['']) test('T26582', normal, compile, ['']) +test('T26746', normal, compile, ['']) +test('T26737', normal, compile, ['']) ===================================== testsuite/tests/typecheck/should_fail/T15801.stderr ===================================== @@ -1,7 +1,8 @@ T15801.hs:52:10: error: [GHC-18872] - • Couldn't match representation of type: UnOp op_a -> UnOp b - with that of: op_a --> b - arising (via a quantified constraint) from the superclasses of an instance declaration + • Couldn't match representation of type: op_a --> b + with that of: UnOp op_a -> UnOp b + arising (via a quantified constraint) from + the superclasses of an instance declaration When trying to solve the quantified constraint forall (op_a :: Op (*)) (b :: Op (*)). op_a -#- b arising from the superclasses of an instance declaration ===================================== testsuite/tests/typecheck/should_fail/T22924b.stderr ===================================== @@ -1,6 +1,6 @@ T22924b.hs:10:5: error: [GHC-40404] • Reduction stack overflow; size = 201 - When simplifying the following constraint: Coercible [R] S + When simplifying the following constraint: Coercible S [R] • In the expression: coerce In an equation for ‘f’: f = coerce Suggested fix: ===================================== testsuite/tests/typecheck/should_fail/TcCoercibleFail.hs ===================================== @@ -20,15 +20,6 @@ foo4 = coerce $ one :: Down Int newtype Void = Void Void foo5 = coerce :: Void -> () - ------------------------------------- --- This next one generates an exponentially big type as it --- tries to unwrap. See comment:15 in #11518 --- Adding assertions that force the types can make us --- run out of space. -newtype VoidBad a = VoidBad (VoidBad (a,a)) -foo5' = coerce :: (VoidBad ()) -> () - ------------------------------------ -- This should fail with a context stack overflow newtype Fix f = Fix (f (Fix f)) ===================================== testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr ===================================== @@ -34,23 +34,21 @@ TcCoercibleFail.hs:18:8: error: [GHC-18872] In the expression: coerce $ one :: Down Int In an equation for ‘foo4’: foo4 = coerce $ one :: Down Int -TcCoercibleFail.hs:21:8: error: [GHC-18872] - • Couldn't match representation of type ‘Void’ with that of ‘()’ - arising from a use of ‘coerce’ +TcCoercibleFail.hs:21:8: error: [GHC-40404] + • Reduction stack overflow; size = 201 + When simplifying the following constraint: Coercible () Void • In the expression: coerce :: Void -> () In an equation for ‘foo5’: foo5 = coerce :: Void -> () + Suggested fix: + Use -freduction-depth=0 to disable this check + (any upper bound you could choose might fail unpredictably with + minor updates to GHC, so disabling the check is recommended if + you're sure that type checking should terminate) -TcCoercibleFail.hs:30:9: error: [GHC-18872] - • Couldn't match representation of type ‘VoidBad ()’ - with that of ‘()’ - arising from a use of ‘coerce’ - • In the expression: coerce :: (VoidBad ()) -> () - In an equation for ‘foo5'’: foo5' = coerce :: (VoidBad ()) -> () - -TcCoercibleFail.hs:35:8: error: [GHC-40404] +TcCoercibleFail.hs:26:8: error: [GHC-40404] • Reduction stack overflow; size = 201 When simplifying the following constraint: - Coercible (Either Int (Fix (Either Int))) (Fix (Either Age)) + Coercible (Fix (Either Age)) (Either Int (Fix (Either Int))) • In the expression: coerce :: Fix (Either Int) -> Fix (Either Age) In an equation for ‘foo6’: foo6 = coerce :: Fix (Either Int) -> Fix (Either Age) @@ -60,10 +58,9 @@ TcCoercibleFail.hs:35:8: error: [GHC-40404] minor updates to GHC, so disabling the check is recommended if you're sure that type checking should terminate) -TcCoercibleFail.hs:36:8: error: [GHC-18872] - • Couldn't match representation of type ‘Either - Int (Fix (Either Int))’ - with that of ‘()’ +TcCoercibleFail.hs:27:8: error: [GHC-18872] + • Couldn't match representation of type ‘()’ + with that of ‘Either Int (Fix (Either Int))’ arising from a use of ‘coerce’ • In the expression: coerce :: Fix (Either Int) -> () In an equation for ‘foo7’: foo7 = coerce :: Fix (Either Int) -> () ===================================== testsuite/tests/typecheck/should_fail/all.T ===================================== @@ -326,11 +326,7 @@ test('T7989', normal, compile_fail, ['']) test('T8034', normal, compile_fail, ['']) test('T8142', normal, compile_fail, ['']) test('T8262', normal, compile_fail, ['']) - -# TcCoercibleFail times out with the compiler is compiled with -DDEBUG. -# This is expected (see comment in source file). -test('TcCoercibleFail', [when(compiler_debugged(), skip)], compile_fail, ['']) - +test('TcCoercibleFail', [], compile_fail, ['']) test('TcCoercibleFail2', [], compile_fail, ['']) test('TcCoercibleFail3', [], compile_fail, ['']) test('T8306', normal, compile_fail, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/7e15862f222e172101043123c0d0f2… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/7e15862f222e172101043123c0d0f2… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc][master] testsuite: Widen acceptance window for T5205.
by Marge Bot (＠marge-bot) 16 Jan '26

16 Jan '26

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 8b59e62c by Andreas Klebinger at 2026-01-16T17:18:52-05:00 testsuite: Widen acceptance window for T5205. Fixes #26782 - - - - - 1 changed file: - testsuite/tests/perf/should_run/all.T Changes: ===================================== testsuite/tests/perf/should_run/all.T ===================================== @@ -128,7 +128,7 @@ test('T4978', ['-O2']) test('T5205', - [collect_stats('bytes allocated',5), + [collect_stats('bytes allocated',15), only_ways(['normal', 'optasm']) ], compile_and_run, View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8b59e62c4ecbd23ad8f163e55c02366… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8b59e62c4ecbd23ad8f163e55c02366… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc][master] Improve newtype unwrapping
by Marge Bot (＠marge-bot) 16 Jan '26

16 Jan '26

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 29c0aceb by Simon Peyton Jones at 2026-01-16T17:18:11-05:00 Improve newtype unwrapping Ticket #26746 describes several relatively-minor shortcomings of newtype unwrapping. This MR addresses them, while also (arguably) simplifying the code a bit. See new Note [Solving newtype equalities: overview] and Note [Decomposing newtype equalities] and Note [Eager newtype decomposition] and Note [Even more eager newtype decomposition] For some reason, on Windows only, runtime allocations decrease for test T5205 (from 52k to 48k). I have not idea why. No change at all on Linux. I'm just going to accept the change. (I saw this same effect in another MR so I think it's a fault in the baseline.) Metric Decrease: T5205 - - - - - 15 changed files: - compiler/GHC/Core/FamInstEnv.hs - compiler/GHC/Tc/Instance/Family.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/Monad.hs - testsuite/tests/deriving/should_fail/T8984.stderr - testsuite/tests/deriving/should_fail/deriving-via-fail.stderr - testsuite/tests/deriving/should_fail/deriving-via-fail4.stderr - testsuite/tests/deriving/should_fail/deriving-via-fail5.stderr - + testsuite/tests/typecheck/should_compile/T26746.hs - testsuite/tests/typecheck/should_compile/all.T - testsuite/tests/typecheck/should_fail/T15801.stderr - testsuite/tests/typecheck/should_fail/T22924b.stderr - testsuite/tests/typecheck/should_fail/TcCoercibleFail.hs - testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== compiler/GHC/Core/FamInstEnv.hs ===================================== @@ -1061,10 +1061,10 @@ lookup_fam_inst_env' lookup_mode (FamIE _ ie) fam match_tys , fi_tys = tpl_tys }) = do subst <- tcMatchTys tpl_tys match_tys1 return (FamInstMatch { fim_instance = item - , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2 - , fim_cos = assert (all (isJust . lookupCoVar subst) tpl_cvs) $ - substCoVars subst tpl_cvs - }) + , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2 + , fim_cos = assert (all (isJust . lookupCoVar subst) tpl_cvs) $ + substCoVars subst tpl_cvs + }) where (match_tys1, match_tys2) = split_tys tpl_tys ===================================== compiler/GHC/Tc/Instance/Family.hs ===================================== @@ -5,7 +5,7 @@ module GHC.Tc.Instance.Family ( FamInstEnvs, tcGetFamInstEnvs, checkFamInstConsistency, tcExtendLocalFamInstEnv, tcLookupDataFamInst, tcLookupDataFamInst_maybe, - tcTopNormaliseNewTypeTF_maybe, + tcUnwrapNewtype_maybe, -- * Injectivity reportInjectivityErrors, reportConflictingInjectivityErrs @@ -46,7 +46,6 @@ import GHC.Utils.Misc import GHC.Utils.Panic import GHC.Utils.FV -import GHC.Data.Bag( Bag, unionBags, unitBag ) import GHC.Data.Maybe import Control.Monad @@ -452,58 +451,57 @@ tcLookupDataFamInst_maybe fam_inst_envs tc tc_args | otherwise = Nothing --- | 'tcTopNormaliseNewTypeTF_maybe' gets rid of top-level newtypes, --- potentially looking through newtype /instances/ and type synonyms. +-- | 'tcUnwrapNewtype_mabye' gets rid of /one layer/ of top-level newtypes -- -- It is only used by the type inference engine (specifically, when -- solving representational equality), and hence it is careful to unwrap -- only if the relevant data constructor is in scope. That's why -- it gets a GlobalRdrEnv argument. -- --- It is careful not to unwrap data/newtype instances nor synonyms --- if it can't continue unwrapping. Such care is necessary for proper --- error messages. +-- It is capable of unwrapping a newtype /instance/. E.g +-- data D a +-- newtype instance D Int = MkD Bool +-- Then `tcUnwrapNewtype_maybe (D Int)` will unwrap to give the `Bool` inside. +-- However, it is careful not to unwrap data/newtype instances if it can't +-- unwrap the newtype inside it; that might in the example if `MkD` was +-- not in scope. Such care is necessary for proper error messages. -- -- It does not look through type families. --- It does not normalise arguments to a tycon. +-- It does not normalise arguments to the tycon. -- --- If the result is Just ((gres, co), rep_ty), then +-- If the result is Just (gre, co, rep_ty), then -- co : ty ~R rep_ty --- gres are the GREs for the data constructors that --- had to be in scope -tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs - -> GlobalRdrEnv - -> Type - -> Maybe ((Bag GlobalRdrElt, TcCoercion), Type) -tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty --- cf. FamInstEnv.topNormaliseType_maybe and Coercion.topNormaliseNewType_maybe - = topNormaliseTypeX stepper plus ty +-- gre is the GRE for the data constructor that had to be in scope +tcUnwrapNewtype_maybe :: FamInstEnvs + -> GlobalRdrEnv + -> Type + -> Maybe (GlobalRdrElt, TcCoercion, Type) +tcUnwrapNewtype_maybe faminsts rdr_env ty + | Just (tc,tys) <- tcSplitTyConApp_maybe ty + = firstJust (try_nt_unwrap tc tys) + (try_fam_unwrap tc tys) + | otherwise + = Nothing where - plus :: (Bag GlobalRdrElt, TcCoercion) -> (Bag GlobalRdrElt, TcCoercion) - -> (Bag GlobalRdrElt, TcCoercion) - plus (gres1, co1) (gres2, co2) = ( gres1 `unionBags` gres2 - , co1 `mkTransCo` co2 ) - - stepper :: NormaliseStepper (Bag GlobalRdrElt, TcCoercion) - stepper = unwrap_newtype `composeSteppers` unwrap_newtype_instance - - -- For newtype instances we take a double step or nothing, so that + -- For newtype /instances/ we take a double step or nothing, so that -- we don't return the representation type of the newtype instance, -- which would lead to terrible error messages - unwrap_newtype_instance rec_nts tc tys - | Just (tc', tys', co) <- tcLookupDataFamInst_maybe faminsts tc tys - = fmap (mkTransCo co) <$> unwrap_newtype rec_nts tc' tys' - | otherwise = NS_Done + try_fam_unwrap tc tys + | Just (tc', tys', fam_co) <- tcLookupDataFamInst_maybe faminsts tc tys + , Just (gre, nt_co, ty') <- try_nt_unwrap tc' tys' + = Just (gre, mkTransCo fam_co nt_co, ty') + | otherwise + = Nothing - unwrap_newtype rec_nts tc tys + try_nt_unwrap tc tys | Just con <- newTyConDataCon_maybe tc , Just gre <- lookupGRE_Name rdr_env (dataConName con) -- This is where we check that the -- data constructor is in scope - = (,) (unitBag gre) <$> unwrapNewTypeStepper rec_nts tc tys - + , Just (ty', co) <- instNewTyCon_maybe tc tys + = Just (gre, co, ty') | otherwise - = NS_Done + = Nothing {- ************************************************************************ ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -23,7 +23,7 @@ import GHC.Tc.Types.CtLoc import GHC.Tc.Types.Origin import GHC.Tc.Utils.Unify import GHC.Tc.Utils.TcType -import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe ) +import GHC.Tc.Instance.Family ( tcUnwrapNewtype_maybe ) import qualified GHC.Tc.Utils.Monad as TcM import GHC.Core.Type @@ -48,7 +48,6 @@ import GHC.Utils.Misc import GHC.Utils.Monad import GHC.Data.Pair -import GHC.Data.Bag import Control.Monad import Data.Maybe ( isJust, isNothing ) import Data.List ( zip4 ) @@ -334,24 +333,52 @@ can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 | Just ty1' <- coreView ty1 = can_eq_nc rewritten rdr_env envs ev eq_rel ty1' ps_ty1 ty2 ps_ty2 | Just ty2' <- coreView ty2 = can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2' ps_ty2 --- need to check for reflexivity in the ReprEq case. --- See Note [Eager reflexivity check] --- Check only when rewritten because the zonk_eq_types check in canEqNC takes --- care of the non-rewritten case. -can_eq_nc True _rdr_env _envs ev ReprEq ty1 _ ty2 _ - | ty1 `tcEqType` ty2 - = canEqReflexive ev ReprEq ty1 - --- When working with ReprEq, unwrap newtypes. --- See Note [Unwrap newtypes first] +-- Look for (N s1 .. sn) ~R# (N t1 .. tn) +-- where either si=ti +-- or N is phantom in i'th position +-- See Note [Solving newtype equalities: overview] +-- and (for details) Note [Eager newtype decomposition] +-- We try this /before/ attempting to unwrap N, because if N is +-- recursive, unwrapping will loop. +-- This /matters/ for newtypes, but is /safe/ for all types +can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _ + | ReprEq <- eq_rel + , TyConApp tc1 tys1 <- ty1 + , TyConApp tc2 tys2 <- ty2 + , tc1 == tc2 + , ok tys1 tys2 (tyConRoles tc1) + = canDecomposableTyConAppOK ev eq_rel tc1 (ty1,tys1) (ty2,tys2) + where + ok :: [TcType] -> [TcType] -> [Role] -> Bool + -- OK to decompose a representational equality + -- if the args are already equal + -- or are phantom role + -- See Note [Eager newtype decomposition] + -- You might think that representational role would also be OK, but + -- see Note [Even more eager newtype decomposition] + ok (ty1:tys1) (ty2:tys2) rs + | Phantom : rs' <- rs = ok tys1 tys2 rs' + | ty1 `tcEqType` ty2 = ok tys1 tys2 (drop 1 rs) + | otherwise = False + ok [] [] _ = True + ok _ _ _ = False -- Mis-matched lengths, just about possible because of + -- kind polymorphism. Anyway False is a safe result! + +-- Unwrap newtypes, when in ReprEq only +-- See Note [Solving newtype equalities: overview] +-- and (for details) Note [Unwrap newtypes first] -- This must be above the TyVarTy case, in order to guarantee (TyEq:N) +-- +-- We unwrap *one layer only*; `can_eq_newtype_nc` then loops back to +-- `can_eq_nc`. If there is a recursive newtype, so that we keep +-- unwrapping, the depth limit in `can_eq_newtype_nc` will blow up. can_eq_nc _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 | ReprEq <- eq_rel - , Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1 + , Just stuff1 <- tcUnwrapNewtype_maybe envs rdr_env ty1 = can_eq_newtype_nc rdr_env envs ev NotSwapped stuff1 ty2 ps_ty2 | ReprEq <- eq_rel - , Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2 + , Just stuff2 <- tcUnwrapNewtype_maybe envs rdr_env ty2 = can_eq_newtype_nc rdr_env envs ev IsSwapped stuff2 ty1 ps_ty1 -- Then, get rid of casts @@ -374,6 +401,11 @@ can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _ = do { setEqIfWanted ev (mkReflCPH eq_rel ty1) ; stopWith ev "Equal LitTy" } +can_eq_nc _rewritten _rdr_env _envs ev eq_rel + s1@ForAllTy{} _ + s2@ForAllTy{} _ + = can_eq_nc_forall ev eq_rel s1 s2 + -- Decompose FunTy: (s -> t) and (c => t) -- NB: don't decompose (Int -> blah) ~ (Show a => blah) can_eq_nc _rewritten _rdr_env _envs ev eq_rel @@ -401,19 +433,20 @@ can_eq_nc rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _ , rewritten || both_generative = canTyConApp ev eq_rel both_generative (ty1,tc1,tys1) (ty2,tc2,tys2) -can_eq_nc _rewritten _rdr_env _envs ev eq_rel - s1@ForAllTy{} _ - s2@ForAllTy{} _ - = can_eq_nc_forall ev eq_rel s1 s2 - --- See Note [Canonicalising type applications] about why we require rewritten types --- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families --- NB: Only decompose AppTy for nominal equality. --- See Note [Decomposing AppTy equalities] -can_eq_nc True _rdr_env _envs ev NomEq ty1 _ ty2 _ - | Just (t1, s1) <- tcSplitAppTy_maybe ty1 +-- Decompose applications +can_eq_nc rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _ + | True <- rewritten -- Why True? See Note [Canonicalising type applications] + -- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families + , Just (t1, s1) <- tcSplitAppTy_maybe ty1 , Just (t2, s2) <- tcSplitAppTy_maybe ty2 - = can_eq_app ev t1 s1 t2 s2 + = case eq_rel of + NomEq -> can_eq_app ev t1 s1 t2 s2 + -- Only decompose AppTy for nominal equality. + -- See (APT1) in Note [Decomposing AppTy equalities] + + ReprEq | ty1 `tcEqType` ty2 -> canEqReflexive ev ReprEq ty1 + -- tcEqType: see (APT2) in Note [Decomposing AppTy equalities] + | otherwise -> finishCanWithIrred ReprEqReason ev ------------------- -- Can't decompose. @@ -665,124 +698,18 @@ There are lots of wrinkles of course: the attempt if we fail. -} -{- Note [Unwrap newtypes first] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -See also Note [Decomposing newtype equalities] - -Consider - newtype N m a = MkN (m a) -N will get a conservative, Nominal role for its second parameter 'a', -because it appears as an argument to the unknown 'm'. Now consider - [W] N Maybe a ~R# N Maybe b - -If we /decompose/, we'll get - [W] a ~N# b - -But if instead we /unwrap/ we'll get - [W] Maybe a ~R# Maybe b -which in turn gives us - [W] a ~R# b -which is easier to satisfy. - -Conclusion: we must unwrap newtypes before decomposing them. This happens -in `can_eq_newtype_nc` - -We did flirt with making the /rewriter/ expand newtypes, rather than -doing it in `can_eq_newtype_nc`. But with recursive newtypes we want -to be super-careful about expanding! - - newtype A = MkA [A] -- Recursive! - - f :: A -> [A] - f = coerce - -We have [W] A ~R# [A]. If we rewrite [A], it'll expand to - [[[[[...]]]]] -and blow the reduction stack. See Note [Newtypes can blow the stack] -in GHC.Tc.Solver.Rewrite. But if we expand only the /top level/ of -both sides, we get - [W] [A] ~R# [A] -which we can, just, solve by reflexivity. - -So we simply unwrap, on-demand, at top level, in `can_eq_newtype_nc`. - -This is all very delicate. There is a real risk of a loop in the type checker -with recursive newtypes -- but I think we're doomed to do *something* -delicate, as we're really trying to solve for equirecursive type -equality. Bottom line for users: recursive newtypes do not play well with type -inference for representational equality. See also Section 5.3.1 and 5.3.4 of -"Safe Zero-cost Coercions for Haskell" (JFP 2016). - -See also Note [Decomposing newtype equalities]. - ---- Historical side note --- - -We flirted with doing /both/ unwrap-at-top-level /and/ rewrite-deeply; -see #22519. But that didn't work: see discussion in #22924. Specifically -we got a loop with a minor variation: - f2 :: a -> [A] - f2 = coerce - -Note [Eager reflexivity check] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have - - newtype X = MkX (Int -> X) - -and - - [W] X ~R X - -Naively, we would start unwrapping X and end up in a loop. Instead, -we do this eager reflexivity check. This is necessary only for representational -equality because the rewriter technology deals with the similar case -(recursive type families) for nominal equality. - -Note that this check does not catch all cases, but it will catch the cases -we're most worried about, types like X above that are actually inhabited. - -Here's another place where this reflexivity check is key: -Consider trying to prove (f a) ~R (f a). The AppTys in there can't -be decomposed, because representational equality isn't congruent with respect -to AppTy. So, when canonicalising the equality above, we get stuck and -would normally produce a CIrredCan. However, we really do want to -be able to solve (f a) ~R (f a). So, in the representational case only, -we do a reflexivity check. - -(This would be sound in the nominal case, but unnecessary, and I [Richard -E.] am worried that it would slow down the common case.) - - Note [Newtypes can blow the stack] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have - - newtype X = MkX (Int -> X) - newtype Y = MkY (Int -> Y) - -and now wish to prove - - [W] X ~R Y - -This Wanted will loop, expanding out the newtypes ever deeper looking -for a solid match or a solid discrepancy. Indeed, there is something -appropriate to this looping, because X and Y *do* have the same representation, -in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized -coercion will ever witness it. This loop won't actually cause GHC to hang, -though, because we check our depth in `can_eq_newtype_nc`. --} - ------------------------ -- | We're able to unwrap a newtype. Update the bits accordingly. can_eq_newtype_nc :: GlobalRdrEnv -> FamInstEnvs -> CtEvidence -- ^ :: ty1 ~ ty2 -> SwapFlag - -> ((Bag GlobalRdrElt, TcCoercion), TcType) -- ^ :: ty1 ~ ty1' + -> (GlobalRdrElt, TcCoercion, TcType) -- ^ :: ty1 ~ ty1' -> TcType -- ^ ty2 -> TcType -- ^ ty2, with type synonyms -> TcS (StopOrContinue (Either IrredCt EqCt)) -can_eq_newtype_nc rdr_env envs ev swapped ((gres, co1), ty1') ty2 ps_ty2 +can_eq_newtype_nc rdr_env envs ev swapped (gre, co1, ty1') ty2 ps_ty2 = do { traceTcS "can_eq_newtype_nc" $ - vcat [ ppr ev, ppr swapped, ppr co1, ppr gres, ppr ty1', ppr ty2 ] + vcat [ ppr ev, ppr swapped, ppr co1, ppr gre, ppr ty1', ppr ty2 ] -- Check for blowing our stack, and increase the depth -- See Note [Newtypes can blow the stack] @@ -791,14 +718,20 @@ can_eq_newtype_nc rdr_env envs ev swapped ((gres, co1), ty1') ty2 ps_ty2 -- Next, we record uses of newtype constructors, since coercing -- through newtypes is tantamount to using their constructors. - ; recordUsedGREs gres + ; recordUsedGRE gre ; let redn1 = mkReduction co1 ty1' redn2 = mkReflRedn Representational ps_ty2 - ; new_ev <- rewriteEqEvidence ev' swapped redn1 redn2 + ; new_ev <- rewriteEqEvidence ev' (flipSwap swapped) redn2 redn1 emptyCoHoleSet - ; can_eq_nc False rdr_env envs new_ev ReprEq ty1' ty1' ty2 ps_ty2 } + -- ty1 is the one being unwrapped. Loop back to can_eq_nc with + -- the arguments flipped so that ty2 is looked at first in the + -- next iteration. That way if we have (Id Rec) ~R# (Id Rec) + -- where newtype Id a = MkId a and newtype Rec = MkRec Rec + -- we'll unwrap both Ids, then spot Rec=Rec. + -- See (END2) in Note [Eager newtype decomposition] + ; can_eq_nc False rdr_env envs new_ev ReprEq ty2 ps_ty2 ty1' ty1' } --------- -- ^ Decompose a type application. @@ -896,7 +829,7 @@ canTyConApp ev eq_rel both_generative (ty1,tc1,tys1) (ty2,tc2,tys2) | tc1 == tc2 , tys1 `equalLength` tys2 = do { inerts <- getInertSet - ; if can_decompose inerts + ; if canDecomposeTcApp ev eq_rel tc1 inerts then canDecomposableTyConAppOK ev eq_rel tc1 (ty1,tys1) (ty2,tys2) else assert (eq_rel == ReprEq) $ canEqSoftFailure ReprEqReason ev ty1 ty2 } @@ -918,19 +851,31 @@ canTyConApp ev eq_rel both_generative (ty1,tc1,tys1) (ty2,tc2,tys2) | otherwise = canEqSoftFailure ReprEqReason ev ty1 ty2 - where + +canDecomposeTcApp :: CtEvidence -> EqRel -> TyCon -> InertSet -> Bool -- See Note [Decomposing TyConApp equalities] -- and Note [Decomposing newtype equalities] - can_decompose inerts - = isInjectiveTyCon tc1 (eqRelRole eq_rel) - || (assert (eq_rel == ReprEq) $ - -- assert: isInjectiveTyCon is always True for Nominal except - -- for type synonyms/families, neither of which happen here - -- Moreover isInjectiveTyCon is True for Representational - -- for algebraic data types. So we are down to newtypes - -- and data families. - ctEvFlavour ev == Wanted && noGivenNewtypeReprEqs tc1 inerts) - -- See Note [Decomposing newtype equalities] (EX2) +canDecomposeTcApp ev eq_rel tc inerts + | isInjectiveTyCon tc eq_role = True + | isGiven ev = False + | otherwise = assert (eq_rel == ReprEq) $ + assert (isNewTyCon tc || + isDataFamilyTyCon tc || + isAbstractTyCon tc ) $ + noGivenNewtypeReprEqs tc inerts + -- The otherwise case deals with + -- * Representational equalities (T s1..sn) ~R# (T t1..tn) + -- * where T is a newtype or data family or abstract + -- Why? isInjectiveTyCon is always True for eq_rel=NomEq except for type + -- synonyms/families, neither of which happen here; and isInjectiveTyCon + -- is True for Representational for algebraic data types. + -- + -- noGivenNewtypeReprEqs: see Note [Decomposing newtype equalities] (EX4) + -- Decomposing here is a last resort + -- NB: despite all these tests, decomposition of data familiies is alas + -- /still/ incomplete. See (EX3) in Note [Decomposing newtype equalities] + where + eq_role = eqRelRole eq_rel {- Note [Canonicalising TyCon/TyCon equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -945,7 +890,7 @@ Suppose we are canonicalising [W] Int ~R# DF (TF a). Then (TC1) We might have an inert Given (a ~# Char), so if we rewrote the wanted (i.e. went around again in `can_eq_nc` with `rewritten`=True, we'd get [W] Int ~R# DF Bool - and then the `tcTopNormaliseNewTypeTF_maybe` call would fire and + and then the `tcUnwrapNewtype_maybe` call would fire and we'd unwrap the newtype. So we must do that "go round again" bit. Hence the complicated guard (rewritten || both_generative) in `can_eq_nc`. @@ -1114,6 +1059,110 @@ This is not a very big deal. It reduces the number of solver steps in the test RaeJobTalk from 1830 to 1815, a 1% reduction. But still, it doesn't cost anything either. +Note [Solving newtype equalities: overview] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +This Note also applies to data families, which we treat like +newtype in case of 'newtype instance'. + +Consider (N s1..sn) ~R# (N t1..tn), where N is a newtype. +We try three strategies, in order: + +(NTE1) Decompose if the si/ti are either (a) identical or (b) phantom. This step + avoids unwrapping, which allows success in some cases where the newtype + would unwrap infinitely. See Note [Eager newtype decomposition] + +(NTE2) Unwrap the newtype, if possible. Always good, but it requires the data + constructor to be in scope. See Note [Unwrap newtypes first]. + + If the newtype is recursive, this unwrapping might go on forever, + so `can_eq_newtype_nc` has a depth bound check. + See Note [Newtypes can blow the stack] + +(NTE3) Decompose the tycon application. This step is a last resort, because it + risks losing completeness. See Note [Decomposing newtype equalities] + +Note [Newtypes can blow the stack] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have + + newtype X = MkX (Int -> X) + newtype Y = MkY (Int -> Y) + +and now wish to prove + + [W] X ~R Y + +This Wanted will loop, expanding out the newtypes ever deeper looking +for a solid match or a solid discrepancy. Indeed, there is something +appropriate to this looping, because X and Y *do* have the same representation, +in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized +coercion will ever witness it. This loop won't actually cause GHC to hang, +though, because we check our depth in `can_eq_newtype_nc`. + +However, GHC can still loop badly: see #26757, which shows how we can create +types whose size is exponential in the depth of newtype expansion. That makes +GHC go out to lunch unless the depth bound is very small indeed; and a small +depth bound makes perfectly legitimate programs fail. We don't have solid +solution for this, but it's rare. + +Note [Unwrap newtypes first] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +See also Note [Decomposing newtype equalities] + +Consider + newtype N m a = MkN (m a) +N will get a conservative, Nominal role for its second parameter 'a', +because it appears as an argument to the unknown 'm'. Now consider + [W] N Maybe a ~R# N Maybe b + +If we /decompose/, we'll get + [W] a ~N# b + +But if instead we /unwrap/ we'll get + [W] Maybe a ~R# Maybe b +which in turn gives us + [W] a ~R# b +which is easier to satisfy. + +Conclusion: we must unwrap newtypes before decomposing them. This happens +in `can_eq_newtype_nc` + +We did flirt with making the /rewriter/ expand newtypes, rather than +doing it in `can_eq_newtype_nc`. But with recursive newtypes we want +to be super-careful about expanding! + + newtype A = MkA [A] -- Recursive! + + f :: A -> [A] + f = coerce + +We have [W] A ~R# [A]. If we rewrite [A], it'll expand to + [[[[[...]]]]] +and blow the reduction stack. See Note [Newtypes can blow the stack] +in GHC.Tc.Solver.Rewrite. But if we expand only the /top level/ of +both sides, we get + [W] [A] ~R# [A] +which we can, just, solve by reflexivity. + +So we simply unwrap, on-demand, at top level, in `can_eq_newtype_nc`. + +This is all very delicate. There is a real risk of a loop in the type checker +with recursive newtypes -- but I think we're doomed to do *something* +delicate, as we're really trying to solve for equirecursive type +equality. Bottom line for users: recursive newtypes do not play well with type +inference for representational equality. See also Section 5.3.1 and 5.3.4 of +"Safe Zero-cost Coercions for Haskell" (JFP 2016). + +See also Note [Decomposing newtype equalities]. + +--- Historical side note --- + +We flirted with doing /both/ unwrap-at-top-level /and/ rewrite-deeply; +see #22519. But that didn't work: see discussion in #22924. Specifically +we got a loop with a minor variation: + f2 :: a -> [A] + f2 = coerce + Note [Decomposing newtype equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ This Note also applies to data families, which we treat like @@ -1133,7 +1182,10 @@ if the newtype is abstract (so can't be unwrapped) we can only solve the equality by (a) using a Given or (b) decomposition. If (a) is impossible (e.g. no Givens) then (b) is safe albeit potentially incomplete. -There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: +Remember: Decomposing Wanteds is always /sound/. + This Note is only about /completeness/. + +There are three ways in which decomposing [W] (N ty1) ~r (N ty2) could be incomplete: * Incompleteness example (EX1): unwrap first newtype Nt a = MkNt (Id a) @@ -1146,7 +1198,7 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: which is unsatisfiable. Unwrapping, though, leads to a solution. CONCLUSION: always unwrap newtypes before attempting to decompose - them. This is done in can_eq_nc. Of course, we can't unwrap if the data + them. This is done in `can_eq_nc`. Of course, we can't unwrap if the data constructor isn't in scope. See Note [Unwrap newtypes first]. * Incompleteness example (EX2): prioritise Nominal equalities. See #24887 @@ -1154,20 +1206,32 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: data instance D Int = MkD1 (D Char) data instance D Bool = MkD2 (D Char) Now suppose we have - [W] g1: D Int ~R# D a - [W] g2: a ~# Bool - If we solve g2 first, giving a:=Bool, then we can solve g1 easily: + [W] g1: D Int ~R# D alpha + [W] g2: alpha ~# Bool + If we solve g2 first, giving alpha:=Bool, then we can solve g1 easily: D Int ~R# D Char ~R# D Bool by newtype unwrapping. BUT: if we instead attempt to solve g1 first, we can unwrap the LHS (only) - leaving [W] D Char ~#R D Bool - If we decompose now, we'll get (Char ~R# Bool), which is insoluble. + leaving [W] D Char ~#R D alpha + If we decompose now, we'll get (Char ~R# alpha), which is insoluble, since + alpha turns out to be Bool. CONCLUSION: prioritise nominal equalites in the work list. See Note [Prioritise equalities] in GHC.Tc.Solver.InertSet. -* Incompleteness example (EX3): check available Givens +* Incompleteness example (EX3) + Sadly, the fix for (EX2) is /still/ incomplete: + * The equality `g2` might be in a sibling implication constraint, + invisible for now. + * The equality `g2` might be hidden in a class constraint: + class C a + instance (a~Bool) => C [a] + [W] g3 :: C [alpha] + When we get around to solving `g3` we'll discover (g2:alpha~Bool) + So that's a real infelicity in the solver. + +* Incompleteness example (EX4): check available Givens newtype Nt a = Mk Bool -- NB: a is not used in the RHS, type role Nt representational -- but the user gives it an R role anyway @@ -1230,18 +1294,48 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete: un-expanded equality superclasses; but only in some very obscure recursive-superclass situations. - Yet another approach (!) is described in - Note [Decomposing newtypes a bit more aggressively]. - -Remember: decomposing Wanteds is always /sound/. This Note is -only about /completeness/. - -Note [Decomposing newtypes a bit more aggressively] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -IMPORTANT: the ideas in this Note are *not* implemented. Instead, the -current approach is detailed in Note [Decomposing newtype equalities] -and Note [Unwrap newtypes first]. -For more details about the ideas in this Note see +Note [Eager newtype decomposition] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider [W] (Rec1 Int) ~R# (Rec1 Bool) where + newtype Rec1 a = MkRec1 (Rec1 a) + +If we apply (NTE2), we'll loop because `Rec1` unwraps forever. +But the role of `a` is inferred as Phantom, so it sound and complete +to decompose via `canDecomposableTyConAppOK`, giving nothing at all +(because of the Phantom role). So we win. + +Another useful special case is + newtype Rec = MkRec Rec +where there are no arguments. + +So we do an eager decomposition check in step (NTE1), /before/ trying to unwrap +in (NTE2). This is a HACK: it catches some cases of recursion, but not all. +But it's a hack that has been in GHC for some time. + +Wrinkles + +(END1) The eager-decomposition step is fine for all data types, not just newtypes. + +(END2) Consider newtype Id a = MkId a -- Not recusrive + newtype Rec = MkRec Rec -- Recursive + and [W] Id Rec ~R# Rec + Then (NTE1) will fail; (NTE2) will succeed in unwrapping Id, generating + [W] Rec ~R# Rec; and (NTE1) will succeed when we go round the loop. + + What about [W] Rec ~R# Id Rec? + Here (NTE1) will fail again; (NTE2) will succeed, by unwrapping Rec, to get + Rec again. If we just iterate with [W] Rec ~R# Id Rec, we'll be stuck in + a loop. Instead we want to flip the constraint round so we get + [W] Id Rec ~R# Rec. Now we win. See the flipping in `can_eq_newtype_nc`. + +(END3) See Note [Even more eager newtype decomposition] + +Note [Even more eager newtype decomposition] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Eager newtype decomposition] decomposes [W] (N s ~R# N t) if N's role is +phantom. We could go further and decompose if the arguments are all Phantom +/or/ Representational. This is not implemented. For more details about the +ideas in this Note see * GHC propoosal: https://github.com/ghc-proposals/ghc-proposals/pull/549 * issue #22441 * discussion on !9282. @@ -1249,9 +1343,8 @@ For more details about the ideas in this Note see Consider [G] c, [W] (IO Int) ~R (IO Age) where IO is abstract, and newtype Age = MkAge Int -- Not abstract -With the above rules, if there any Given Irreds, -the Wanted is insoluble because we can't decompose it. But in fact, -if we look at the defn of IO, roughly, +With the above rules, if there any Given Irreds, the Wanted is insoluble because +we can't decompose it. But in fact, if we look at the defn of IO, roughly, newtype IO a = State# -> (State#, a) we can see that decomposing [W] (IO Int) ~R (IO Age) to [W] Int ~R Age @@ -1260,41 +1353,26 @@ IO's argment is representational. Hence: DecomposeNewtypeIdea: decompose [W] (N s1 .. sn) ~R (N t1 .. tn) - if the roles of all N's arguments are representational - -If N's arguments really /are/ representational this will not lose -completeness. Here "really are representational" means "if you expand -all newtypes in N's RHS, we'd infer a representational role for each -of N's type variables in that expansion". See Note [Role inference] -in GHC.Tc.TyCl.Utils. - -But the user might /override/ a phantom role with an explicit role -annotation, and then we could (obscurely) get incompleteness. -Consider - - module A( silly, T ) where - newtype T a = MkT Int - type role T representational -- Override phantom role - - silly :: Coercion (T Int) (T Bool) - silly = Coercion -- Typechecks by unwrapping the newtype + if the roles of all N's arguments are representational (or phantom) - data Coercion a b where -- Actually defined in Data.Type.Coercion - Coercion :: Coercible a b => Coercion a b +If N's arguments really /are/ representational this will not lose completeness. +Here "really are representational" means "if you expand all newtypes in N's RHS, +we'd infer a representational role for each of N's type variables in that +expansion". See Note [Role inference] in GHC.Tc.TyCl.Utils. - module B where - import A - f :: T Int -> T Bool - f = case silly of Coercion -> coerce +But the user might /override/ a phantom role with an explicit role annotation, +and then we could (obscurely) get incompleteness. Consider (#9117): + newtype Phant a = MkPhant Char + type role Phant representational -- Override phantom role + [W] Phant Int ~R# Phant Char -Here the `coerce` gives [W] (T Int) ~R (T Bool) which, if we decompose, -we'll get stuck with (Int ~R Bool). Instead we want to use the -[G] (T Int) ~R (T Bool), which will be in the Irreds. +We do not want to decompose to Int ~R# Char; better to unwrap Summary: we could adopt (DecomposeNewtypeIdea), at the cost of a very obscure incompleteness (above). But no one is reporting a problem from the lack of decompostion, so we'll just leave it for now. This long Note is just to record the thinking for our future selves. +---- End of speculative aside --------- Note [Decomposing AppTy equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1305,12 +1383,12 @@ Note [Decomposing TyConApp equalities]. We have s1 t1 ~N s2 t2 ==> s1 ~N s2, t1 ~N t2 (CO_LEFT, CO_RIGHT) In the first of these, why do we need Nominal equality in (t1 ~N t2)? -See {2} below. +See (APT3) below. For sound and complete solving, we need both directions to decompose. So: * At nominal role, all is well: we have both directions. -* At representational role, decomposition of Givens is unsound (see {1} below), - and decomposition of Wanteds is incomplete. +* At representational role, decomposition of Givens is unsound + (see (APT1) below), and decomposition of Wanteds is incomplete. Here is an example of the incompleteness for Wanteds: @@ -1325,7 +1403,7 @@ Suppose we see w1 before w2. If we decompose, using AppCo to prove w1, we get [W] w4 :: b ~N a Note that w4 is *nominal*. A nominal role here is necessary because AppCo -requires a nominal role on its second argument. (See {2} for an example of +requires a nominal role on its second argument. (See (APT3) for an example of why.) Now we are stuck, because w4 is insoluble. On the other hand, if we see w2 first, setting alpha := Maybe, all is well, as we can decompose Maybe b ~R Maybe a into b ~R a. @@ -1348,12 +1426,21 @@ Bottom line: the lack of an equation in can_eq_nc Extra points -{1} Decomposing a Given AppTy over a representational role is simply +(APT1) Decomposing a Given AppTy at Representational role is simply unsound. For example, if we have co1 :: Phant Int ~R a Bool (for the newtype Phant, above), then we surely don't want any relationship between Int and Bool, lest we also have co2 :: Phant ~ a around. -{2} The role on the AppCo coercion is a conservative choice, because we don't + For Wanteds, decomposing an AppTy at Representational role is incomplete. + +(APT2) What if we have [W] (f a) ~R# (f a) + We can't decompose because of (APT1). But it's silly to reject. So we do + an equality check, in the AppTy/AppTy case of `can_eq_nc`. + + (It would be sound to do this reflexivity check in the Nominal case too, + but not necessary, and there might be a perf cost.) + +(APT3) The role on the AppCo coercion is a conservative choice, because we don't know the role signature of the function. For example, let's assume we could have a representational role on the second argument of AppCo. Then, consider ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -22,7 +22,7 @@ module GHC.Tc.Solver.Monad ( updWorkListTcS, pushLevelNoWorkList, pushTcLevelM_, - runTcPluginTcS, recordUsedGREs, + runTcPluginTcS, recordUsedGRE, matchGlobalInst, TcM.ClsInstResult(..), QCInst(..), @@ -1519,18 +1519,16 @@ tcLookupTyCon n = wrapTcS $ TcM.tcLookupTyCon n -- pure veneer of TcS. But it's just about warnings around unused imports -- and local constructors (GHC will issue fewer warnings than it otherwise -- might), so it's not worth losing sleep over. -recordUsedGREs :: Bag GlobalRdrElt -> TcS () -recordUsedGREs gres - = do { wrapTcS $ TcM.addUsedGREs NoDeprecationWarnings gre_list +recordUsedGRE :: GlobalRdrElt -> TcS () +recordUsedGRE gre + = do { wrapTcS $ TcM.addUsedGRE NoDeprecationWarnings gre -- If a newtype constructor was imported, don't warn about not -- importing it... - ; wrapTcS $ traverse_ (TcM.keepAlive . greName) gre_list } + ; wrapTcS $ TcM.keepAlive (greName gre) } -- ...and similarly, if a newtype constructor was defined in the same -- module, don't warn about it being unused. -- See Note [Tracking unused binding and imports] in GHC.Tc.Utils. - where - gre_list = bagToList gres -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== testsuite/tests/deriving/should_fail/T8984.stderr ===================================== @@ -1,6 +1,6 @@ T8984.hs:7:46: error: [GHC-18872] - • Couldn't match representation of type: cat a (N cat a Int) - with that of: cat a (cat a Int) + • Couldn't match representation of type: cat a (cat a Int) + with that of: cat a (N cat a Int) arising from the coercion of the method ‘app’ from type ‘cat a (cat a Int)’ to type ‘N cat a (N cat a Int)’ Note: We cannot know what roles the parameters to ‘cat a’ have; ===================================== testsuite/tests/deriving/should_fail/deriving-via-fail.stderr ===================================== @@ -1,12 +1,12 @@ deriving-via-fail.hs:10:34: error: [GHC-10283] - • Couldn't match representation of type ‘a’ with that of ‘b’ + • Couldn't match representation of type ‘b’ with that of ‘a’ arising from the coercion of the method ‘showsPrec’ from type ‘Int -> Identity b -> ShowS’ to type ‘Int -> Foo1 a -> ShowS’ - ‘a’ is a rigid type variable bound by + ‘b’ is a rigid type variable bound by the deriving clause for ‘Show (Foo1 a)’ at deriving-via-fail.hs:10:34-37 - ‘b’ is a rigid type variable bound by + ‘a’ is a rigid type variable bound by the deriving clause for ‘Show (Foo1 a)’ at deriving-via-fail.hs:10:34-37 • When deriving the instance for (Show (Foo1 a)) ===================================== testsuite/tests/deriving/should_fail/deriving-via-fail4.stderr ===================================== @@ -1,17 +1,17 @@ deriving-via-fail4.hs:15:12: error: [GHC-18872] - • Couldn't match representation of type ‘Int’ with that of ‘Char’ + • Couldn't match representation of type ‘Char’ with that of ‘Int’ arising from the coercion of the method ‘==’ from type ‘Char -> Char -> Bool’ to type ‘F1 -> F1 -> Bool’ • When deriving the instance for (Eq F1) deriving-via-fail4.hs:18:13: error: [GHC-10283] - • Couldn't match representation of type ‘a1’ with that of ‘a2’ + • Couldn't match representation of type ‘a2’ with that of ‘a1’ arising from the coercion of the method ‘c’ from type ‘a -> a -> Bool’ to type ‘a -> F2 a1 -> Bool’ - ‘a1’ is a rigid type variable bound by + ‘a2’ is a rigid type variable bound by the deriving clause for ‘C a (F2 a1)’ at deriving-via-fail4.hs:18:13-15 - ‘a2’ is a rigid type variable bound by + ‘a1’ is a rigid type variable bound by the deriving clause for ‘C a (F2 a1)’ at deriving-via-fail4.hs:18:13-15 • When deriving the instance for (C a (F2 a1)) ===================================== testsuite/tests/deriving/should_fail/deriving-via-fail5.stderr ===================================== @@ -1,10 +1,10 @@ deriving-via-fail5.hs:8:1: error: [GHC-10283] - • Couldn't match representation of type ‘a’ with that of ‘b’ + • Couldn't match representation of type ‘b’ with that of ‘a’ arising from a use of ‘GHC.Internal.Prim.coerce’ - ‘a’ is a rigid type variable bound by + ‘b’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) - ‘b’ is a rigid type variable bound by + ‘a’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) • In the expression: @@ -25,12 +25,12 @@ deriving-via-fail5.hs:8:1: error: [GHC-10283] (bound at deriving-via-fail5.hs:8:1) deriving-via-fail5.hs:8:1: error: [GHC-10283] - • Couldn't match representation of type ‘a’ with that of ‘b’ + • Couldn't match representation of type ‘b’ with that of ‘a’ arising from a use of ‘GHC.Internal.Prim.coerce’ - ‘a’ is a rigid type variable bound by + ‘b’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) - ‘b’ is a rigid type variable bound by + ‘a’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) • In the expression: @@ -48,12 +48,12 @@ deriving-via-fail5.hs:8:1: error: [GHC-10283] show :: Foo4 a -> String (bound at deriving-via-fail5.hs:8:1) deriving-via-fail5.hs:8:1: error: [GHC-10283] - • Couldn't match representation of type ‘a’ with that of ‘b’ + • Couldn't match representation of type ‘b’ with that of ‘a’ arising from a use of ‘GHC.Internal.Prim.coerce’ - ‘a’ is a rigid type variable bound by + ‘b’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) - ‘b’ is a rigid type variable bound by + ‘a’ is a rigid type variable bound by the instance declaration at deriving-via-fail5.hs:(8,1)-(9,24) • In the expression: ===================================== testsuite/tests/typecheck/should_compile/T26746.hs ===================================== @@ -0,0 +1,33 @@ +module T26746 where + +import Data.Coerce + +newtype Foo a = Foo (Foo a) +newtype Age = MkAge Int + +ex1 :: (Foo Age) -> (Foo Int) +ex1 = coerce + +newtype Womble a = MkWomble (Foo a) + +ex2 :: Womble (Foo Age) -> (Foo Int) +ex2 = coerce + +ex3 :: (Foo Age) -> Womble (Foo Int) +ex3 = coerce + + +-- Surprisingly this one works: +newtype Z1 = MkZ1 Z2 +newtype Z2 = MKZ2 Z1 + +ex4 :: Z1 -> Z2 +ex4 = coerce + +-- But this one does not (commented out) +-- newtype Y1 = MkY1 Y2 +-- newtype Y2 = MKY2 Y3 +-- newtype Y3 = MKY3 Y1 +-- +-- ex5 :: Y1 -> Y3 +-- ex5 = coerce ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -957,3 +957,4 @@ test('T17705', normal, compile, ['']) test('T14745', normal, compile, ['']) test('T26451', normal, compile, ['']) test('T26582', normal, compile, ['']) +test('T26746', normal, compile, ['']) ===================================== testsuite/tests/typecheck/should_fail/T15801.stderr ===================================== @@ -1,7 +1,8 @@ T15801.hs:52:10: error: [GHC-18872] - • Couldn't match representation of type: UnOp op_a -> UnOp b - with that of: op_a --> b - arising (via a quantified constraint) from the superclasses of an instance declaration + • Couldn't match representation of type: op_a --> b + with that of: UnOp op_a -> UnOp b + arising (via a quantified constraint) from + the superclasses of an instance declaration When trying to solve the quantified constraint forall (op_a :: Op (*)) (b :: Op (*)). op_a -#- b arising from the superclasses of an instance declaration ===================================== testsuite/tests/typecheck/should_fail/T22924b.stderr ===================================== @@ -1,6 +1,6 @@ T22924b.hs:10:5: error: [GHC-40404] • Reduction stack overflow; size = 201 - When simplifying the following constraint: Coercible [R] S + When simplifying the following constraint: Coercible S [R] • In the expression: coerce In an equation for ‘f’: f = coerce Suggested fix: ===================================== testsuite/tests/typecheck/should_fail/TcCoercibleFail.hs ===================================== @@ -20,15 +20,6 @@ foo4 = coerce $ one :: Down Int newtype Void = Void Void foo5 = coerce :: Void -> () - ------------------------------------- --- This next one generates an exponentially big type as it --- tries to unwrap. See comment:15 in #11518 --- Adding assertions that force the types can make us --- run out of space. -newtype VoidBad a = VoidBad (VoidBad (a,a)) -foo5' = coerce :: (VoidBad ()) -> () - ------------------------------------ -- This should fail with a context stack overflow newtype Fix f = Fix (f (Fix f)) ===================================== testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr ===================================== @@ -34,23 +34,21 @@ TcCoercibleFail.hs:18:8: error: [GHC-18872] In the expression: coerce $ one :: Down Int In an equation for ‘foo4’: foo4 = coerce $ one :: Down Int -TcCoercibleFail.hs:21:8: error: [GHC-18872] - • Couldn't match representation of type ‘Void’ with that of ‘()’ - arising from a use of ‘coerce’ +TcCoercibleFail.hs:21:8: error: [GHC-40404] + • Reduction stack overflow; size = 201 + When simplifying the following constraint: Coercible () Void • In the expression: coerce :: Void -> () In an equation for ‘foo5’: foo5 = coerce :: Void -> () + Suggested fix: + Use -freduction-depth=0 to disable this check + (any upper bound you could choose might fail unpredictably with + minor updates to GHC, so disabling the check is recommended if + you're sure that type checking should terminate) -TcCoercibleFail.hs:30:9: error: [GHC-18872] - • Couldn't match representation of type ‘VoidBad ()’ - with that of ‘()’ - arising from a use of ‘coerce’ - • In the expression: coerce :: (VoidBad ()) -> () - In an equation for ‘foo5'’: foo5' = coerce :: (VoidBad ()) -> () - -TcCoercibleFail.hs:35:8: error: [GHC-40404] +TcCoercibleFail.hs:26:8: error: [GHC-40404] • Reduction stack overflow; size = 201 When simplifying the following constraint: - Coercible (Either Int (Fix (Either Int))) (Fix (Either Age)) + Coercible (Fix (Either Age)) (Either Int (Fix (Either Int))) • In the expression: coerce :: Fix (Either Int) -> Fix (Either Age) In an equation for ‘foo6’: foo6 = coerce :: Fix (Either Int) -> Fix (Either Age) @@ -60,10 +58,9 @@ TcCoercibleFail.hs:35:8: error: [GHC-40404] minor updates to GHC, so disabling the check is recommended if you're sure that type checking should terminate) -TcCoercibleFail.hs:36:8: error: [GHC-18872] - • Couldn't match representation of type ‘Either - Int (Fix (Either Int))’ - with that of ‘()’ +TcCoercibleFail.hs:27:8: error: [GHC-18872] + • Couldn't match representation of type ‘()’ + with that of ‘Either Int (Fix (Either Int))’ arising from a use of ‘coerce’ • In the expression: coerce :: Fix (Either Int) -> () In an equation for ‘foo7’: foo7 = coerce :: Fix (Either Int) -> () ===================================== testsuite/tests/typecheck/should_fail/all.T ===================================== @@ -326,11 +326,7 @@ test('T7989', normal, compile_fail, ['']) test('T8034', normal, compile_fail, ['']) test('T8142', normal, compile_fail, ['']) test('T8262', normal, compile_fail, ['']) - -# TcCoercibleFail times out with the compiler is compiled with -DDEBUG. -# This is expected (see comment in source file). -test('TcCoercibleFail', [when(compiler_debugged(), skip)], compile_fail, ['']) - +test('TcCoercibleFail', [], compile_fail, ['']) test('TcCoercibleFail2', [], compile_fail, ['']) test('TcCoercibleFail3', [], compile_fail, ['']) test('T8306', normal, compile_fail, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/29c0acebbfbe2cd08d8419b29bae44d… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/29c0acebbfbe2cd08d8419b29bae44d… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc][wip/romes/hadrian-cross-stage2-rebase_SVEN_FINAL] 52 commits: rts: Use INFO_TABLE_CONSTR for stg_dummy_ret_closure
by Sven Tennie (＠supersven) 16 Jan '26

16 Jan '26

Sven Tennie pushed to branch wip/romes/hadrian-cross-stage2-rebase_SVEN_FINAL at Glasgow Haskell Compiler / GHC Commits: 322dd672 by Matthew Pickering at 2026-01-09T02:49:35-05:00 rts: Use INFO_TABLE_CONSTR for stg_dummy_ret_closure Since the closure type is CONSTR_NOCAF, we need to use INFO_TABLE_CONSTR to populate the constructor description field (this crashes ghc-debug when decoding AP_STACK frames sometimes) Fixes #26745 - - - - - 039bac4c by Ben Gamari at 2026-01-09T20:22:16-05:00 ghc-internal: Move STM utilities out of GHC.Internal.Conc.Sync This is necessary to avoid an import cycle on Windows when importing `GHC.Internal.Exception.Context` in `GHC.Internal.Conc.Sync`. On the road to address #25365. - - - - - 8c389e8c by Ben Gamari at 2026-01-09T20:22:16-05:00 base: Capture backtrace from throwSTM Implements core-libraries-committee#297. Fixes #25365. - - - - - e1ce1fc3 by Ben Gamari at 2026-01-09T20:22:16-05:00 base: Annotate rethrown exceptions in catchSTM with WhileHandling Implements core-libraries-committee#298 - - - - - c4ebdbdf by Cheng Shao at 2026-01-09T20:23:06-05:00 compiler: make getPrim eagerly evaluate its result This commit makes `GHC.Utils.Binary.getPrim` eagerly evaluate its result, to avoid accidental laziness when future patches build other binary parsers using `getPrim`. - - - - - 66a0c4f7 by Cheng Shao at 2026-01-09T20:23:06-05:00 compiler: implement fast get/put for Word16/Word32/Word64 Previously, `GHC.Utils.Binary` contains `get`/`put` functions for `Word16`/`Word32`/`Word64` which always loads and stores them as big-endian words at a potentially unaligned address. The previous implementation is based on loads/stores of individual bytes and concatenating bytes with bitwise operations, which currently cannot be fused to a single load/store operation by GHC. This patch implements fast `get`/`put` functions for `Word16`/`Word32`/`Word64` based on a single memory load/store, with an additional `byteSwap` operation on little-endian hosts. It is based on unaligned load/store primops added since GHC 9.10, and we already require booting with at least 9.10, so it's about time to switch to this faster path. - - - - - 641ec3f0 by Simon Peyton Jones at 2026-01-09T20:23:55-05:00 Fix scoping errors in specialisation Using -fspecialise-aggressively in #26682 showed up a couple of subtle errors in the type-class specialiser. * dumpBindUDs failed to call `deleteCallsMentioning`, resulting in a call that mentioned a dictionary that was not in scope. This call has been missing since 2009! commit c43c981705ec33da92a9ce91eb90f2ecf00be9fe Author: Simon Peyton Jones <simonpj(a)microsoft.com> Date: Fri Oct 23 16:15:51 2009 +0000 Fixed by re-combining `dumpBindUDs` and `dumpUDs`. * I think there was another bug involving the quantified type variables in polymorphic specialisation. In any case I refactored `specHeader` and `spec_call` so that the former looks for the extra quantified type variables rather than the latter. This is quite a worthwhile simplification: less code, easier to grok. Test case in simplCore/should_compile/T26682, brilliantly minimised by @sheaf. - - - - - 2433e91d by Cheng Shao at 2026-01-09T20:24:43-05:00 compiler: change sectionProtection to take SectionType argument This commit changes `sectionProtection` to only take `SectionType` argument instead of whole `Section`, since it doesn't need the Cmm section content anyway, and it can then be called in parts of NCG where we only have a `SectionType` in scope. - - - - - e5926fbe by Cheng Shao at 2026-01-09T20:24:43-05:00 compiler: change isInitOrFiniSection to take SectionType argument This commit changes `isInitOrFiniSection` to only take `SectionType` argument instead of whole `Section`, since it doesn't need the Cmm section content anyway, and it can then be called in parts of NCG where we only have a `SectionType` in scope. Also marks it as exported. - - - - - 244d57d7 by Cheng Shao at 2026-01-09T20:24:43-05:00 compiler: fix split sections on windows This patch fixes split sections on windows by emitting the right COMDAT section header in NCG, see added comment for more explanation. Fix #26696 #26494. ------------------------- Metric Decrease: LargeRecord T9675 size_hello_artifact size_hello_artifact_gzip size_hello_unicode size_hello_unicode_gzip Metric Increase: T13035 ------------------------- Co-authored-by: Codex <codex(a)openai.com> - - - - - 182f3d0f by Cheng Shao at 2026-01-09T20:25:28-05:00 iserv: add comment about -fkeep-cafs - - - - - 49675b69 by Matthew Craven at 2026-01-09T20:26:14-05:00 Account for "stupid theta" in demand sig for DataCon wrappers Fixes #26748. - - - - - f3c18890 by Samuel Thibault at 2026-01-10T15:48:22+01:00 hurd: Fix getExecutablePath build 3939a8bf93e27 ("GNU/Hurd: Add getExecutablePath support") added using /proc/self/exe for GNU/Hurd but missed adding the required imports for the corresponding code. - - - - - 7f15bd15 by Samuel Thibault at 2026-01-12T07:16:25-05:00 Fix the OS string encoding for GNU/Hurd Following https://github.com/haskell/cabal/pull/9434/files , and as seen in the various gnu_HOST_OS usages in the source code, it is expected that GNU/Hurd is advertised as "gnu", like the autotools do. - - - - - 1db2f240 by Andrew Lelechenko at 2026-01-12T07:17:06-05:00 Add since annotation for Data.Bifoldable1 Fixes #26432 - - - - - e038a383 by Sven Tennie at 2026-01-12T07:17:49-05:00 Ignore Windows CI tool directories in Git Otherwise, we see thousands of changes in `git status` which is very confusing to work with. - - - - - 023c301c by sheaf at 2026-01-13T04:57:30-05:00 Don't re-use stack slots for growing registers This commit avoids re-using a stack slot for a register that has grown but already had a stack slot. For example, suppose we have stack slot assigments %v1 :: FF64 |-> StackSlot 0 %v2 :: FF64 |-> StackSlot 1 Later, we start using %v1 at a larger format (e.g. F64x2) and we need to spill it again. Then we **must not** use StackSlot 0, as a spill at format F64x2 would clobber the data in StackSlot 1. This can cause some fragmentation of the `StackMap`, but that's probably OK. Fixes #26668 - - - - - d0966e64 by fendor at 2026-01-13T04:58:11-05:00 Remove `traceId` from ghc-pkg executable - - - - - 20d7efec by Simon Peyton Jones at 2026-01-13T12:41:22-05:00 Make SpecContr rules fire a bit later See #26615 and Note [SpecConstr rule activation] - - - - - 8bc4eb8c by Andrew Lelechenko at 2026-01-13T12:42:03-05:00 Upgrade mtl submodule to 2.3.2 Fixes #26656 - - - - - c94aaacd by Cheng Shao at 2026-01-13T12:42:44-05:00 compiler: remove iserv and only use on-demand external interpreter This patch removes `iserv` from the tree completely. Hadrian would no longer build or distribute `iserv`, and the GHC driver would use the on-demand external interpreter by default when invoked with `-fexternal-interpreter`, without needing to specify `-pgmi ""`. This has multiple benefits: - It allows cleanup of a lot of legacy hacks in the hadrian codebase. - It paves the way for running cross ghc's iserv via cross emulator (#25523), fixing TH/ghci support for cross targets other than wasm/js. - - - - - c1fe0097 by Peter Trommler at 2026-01-14T03:54:49-05:00 PPC NCG: Fix shift right MO code The shift amount in shift right [arithmetic] MOs is machine word width. Therefore remove unnecessary zero- or sign-extending of shift amount. It looks harmless to extend the shift amount argument because the shift right instruction uses only the seven lowest bits (i. e. mod 128). But now we have a conversion operation from a smaller type to word width around a memory load at word width. The types are not matching up but there is no check done in CodeGen. The necessary conversion from word width down to the smaller width would be translated into a no-op on PowerPC anyway. So all seems harmless if it was not for a small optimisation in getRegister'. In getRegister' a load instruction with the smaller width of the conversion operation was generated. This loaded the most significant bits of the word in memory on a big-endian platform. These bits were zero and hence shift right was used with shift amount zero and not one as required in test Sized. Fixes #26519 - - - - - 2dafc65a by Cheng Shao at 2026-01-14T03:55:31-05:00 Tree-wide cleanup of cygwin logic GHC has not supported cygwin for quite a few years already, and will not resume support in the forseeable future. The only supported windows toolchain is clang64/clangarm64 of the msys2 project. This patch cleans up the unused cygwin logic in the tree. Co-authored-by: Codex <codex(a)openai.com> - - - - - 66b96e2a by Teo Camarasu at 2026-01-14T03:56:13-05:00 Set default eventlog-flush-interval to 5s Resolves #26707 - - - - - d0254579 by Andrew Lelechenko at 2026-01-14T03:56:53-05:00 Document when -maxN RTS option was added - - - - - f25e2b12 by Cheng Shao at 2026-01-14T11:10:39-05:00 testsuite: remove obsolete --ci option from the testsuite driver This patch removes the obsolete `--ci` option from the testsuite driver: neither the CI scripts nor hadrian ever invokes the testsuite driver with `--ci`, and the perf notes are always fetched to the `refs/notes/perf` local reference anyway. - - - - - 7964763b by Julian Ospald at 2026-01-14T11:11:31-05:00 Fix fetch_cabal * download cabal if the existing one is of an older version * fix FreeBSD download url * fix unpacking on FreeBSD - - - - - 6b0129c1 by Julian Ospald at 2026-01-14T11:11:31-05:00 Bump toolchain in CI - - - - - 0f53ccc6 by Julian Ospald at 2026-01-14T11:11:31-05:00 Use libffi-clib Previously, we would build libffi via hadrian and bundle it manually with the GHC bindist. This now moves all that logic out of hadrian and allows us to have a clean Haskell package to build and link against and ship it without extra logic. This patch still retains the ability to link against a system libffi. The main reason of bundling libffi was that on some platforms (e.g. FreeBSD and Mac), system libffi is not visible to the C toolchain by default, so users would require settings in e.g. cabal to be able to compile anything. This adds the submodule libffi-clib to the repository. - - - - - 5e1cd595 by Peng Fan at 2026-01-14T11:12:26-05:00 NCG/LA64: add support for la664 micro architecture Add '-mla664' flag to LA664, which has some new features: atomic instructions, dbar hints, etc. 'LA464' is the default so that unrecognized instructions are not generated. - - - - - c56567ec by Simon Peyton Jones at 2026-01-15T23:19:04+00:00 Add evals for strict data-con args in worker-functions This fixes #26722, by adding an eval in a worker for arguments of strict data constructors, even if the function body uses them strictly. See (WIS1) in Note [Which Ids should be strictified] I took the opportunity to make substantial improvements in the documentation for call-by-value functions. See especially Note [CBV Function Ids: overview] in GHC.Types.Id.Info Note [Which Ids should be CBV candidates?] ditto Note [EPT enforcement] in GHC.Stg.EnforceEpt among others. - - - - - 9719ce5d by Simon Peyton Jones at 2026-01-15T23:19:04+00:00 Improve `interestingArg` This function analyses a function's argument to see if it is interesting enough to deserve an inlining discount. Improvements for * LitRubbish arguments * exprIsExpandable arguments See Note [Interesting arguments] which is substantially rewritten. - - - - - 7b616b9f by Cheng Shao at 2026-01-16T06:45:00-05:00 compiler: fix regression when compiling foreign stubs in the rts unit This patch fixes a regression when compiling foreign stubs in the rts unit introduced in 05e25647f72bc102061af3f20478aa72bff6ff6e. A simple revert would fix it, but it's better to implement a proper fix with comment for better understanding of the underlying problem, see the added comment for explanation. Co-authored-by: Codex <codex(a)openai.com> - - - - - c343ef64 by Sylvain Henry at 2026-01-16T06:45:51-05:00 base: remove GHC.JS.Prim.Internal.Build (#23432) See accepted CLC proposal https://github.com/haskell/core-libraries-committee/issues/329 - - - - - 7bc29236 by Matthew Pickering at 2026-01-16T22:19:16+01:00 Add missing req_interp modifier to T18441fail3 and T18441fail19 These tests require the interpreter but they were failing in a different way with the javascript backend because the interpreter was disabled and stderr is ignored by the test. - - - - - 997811f1 by Matthew Pickering at 2026-01-16T22:19:16+01:00 Use explicit syntax rather than pure - - - - - c0c2b8b1 by Matthew Pickering at 2026-01-16T22:19:16+01:00 packaging: correctly propagate build/host/target to bindist configure script At the moment the host and target which we will produce a compiler for is fixed at the initial configure time. Therefore we need to persist the choice made at this time into the installation bindist as well so we look for the right tools, with the right prefixes at install time. In the future, we want to provide a bit more control about what kind of bindist we produce so the logic about what the host/target will have to be written by hadrian rather than persisted by the configure script. In particular with cross compilers we want to either build a normal stage 2 cross bindist or a stage 3 bindist, which creates a bindist which has a native compiler for the target platform. Fixes #21970 - - - - - 647f7598 by Matthew Pickering at 2026-01-16T22:19:16+01:00 hadrian: Fill in more of the default.host toolchain file When you are building a cross compiler this file will be used to build stage1 and it's libraries, so we need enough information here to work accurately. There is still more work to be done (see for example, word size is still fixed). - - - - - a3f6d80f by Matthew Pickering at 2026-01-16T22:19:16+01:00 hadrian: Disable docs when cross compiling Before there were a variety of ad-hoc places where doc building was disabled when cross compiling. * Some CI jobs sets --docs=none in gen_ci.hs * Some CI jobs set --docs=none in .gitlab/ci.sh * There was some logic in hadrian to not need the ["docs"] target when making a bindist. Now the situation is simple: * If you are cross compiling then defaultDocsTargets is empty by default. In theory, there is no reason why we can't build documentation for cross compiler bindists, but this is left to future work to generalise the documentation building rules to allow this (#24289) - - - - - dc096eba by Matthew Pickering at 2026-01-16T22:19:16+01:00 hadrian: Build stage 2 cross compilers * Most of hadrian is abstracted over the stage in order to remove the assumption that the target of all stages is the same platform. This allows the RTS to be built for two different targets for example. * Abstracts the bindist creation logic to allow building either normal or cross bindists. Normal bindists use stage 1 libraries and a stage 2 compiler. Cross bindists use stage 2 libararies and a stage 2 compiler. * hadrian: Make binary-dist-dir the default build target. This allows us to have the logic in one place about which libraries/stages to build with cross compilers. Fixes #24192 New hadrian target: * `binary-dist-dir-cross`: Build a cross compiler bindist (compiler = stage 1, libraries = stage 2) This commit also contains various changes to make stage2 compilers feasible. ------------------------- Metric Decrease: ManyAlternatives MultiComponentModulesRecomp MultiLayerModulesRecomp T10421 T12425 T12707 T13035 T13379 T15703 T16577 T18698a T18698b T18923 T1969 T21839c T3294 T4801 T5030 T5321Fun T5642 T783 T9198 T9872d T9961 parsing001 T5321FD T6048 ------------------------- Co-authored-by: Sven Tennie <sven.tennie(a)gmail.com> - - - - - 07a03187 by Sven Tennie at 2026-01-16T22:19:16+01:00 Align CI scripts with master Fixup - - - - - e6ec1ff3 by Matthew Pickering at 2026-01-16T22:19:16+01:00 ci: Test cross bindists We remove the special logic for testing in-tree cross compilers and instead test cross compiler bindists, like we do for all other platforms. - - - - - 365ac1a8 by Matthew Pickering at 2026-01-16T22:19:16+01:00 ci: Introduce CROSS_STAGE variable In preparation for building and testing stage3 bindists we introduce the CROSS_STAGE variable which is used by a CI job to determine what kind of bindist the CI job should produce. At the moment we are only using CROSS_STAGE=2 but in the future we will have some jobs which set CROSS_STAGE=3 to produce native bindists for a target, but produced by a cross compiler, which can be tested on by another CI job on the native platform. CROSS_STAGE=2: Build a normal cross compiler bindist CROSS_STAGE=3: Build a stage 3 bindist, one which is a native compiler and library for the target - - - - - ba73c3bb by Matthew Pickering at 2026-01-16T22:19:16+01:00 hadrian: Refactor system-cxx-std-lib rules0 I noticed a few things wrong with the hadrian rules for `system-cxx-std-lib` rules. * For `text` there is an ad-hoc check to depend on `system-cxx-std-lib` outside of `configurePackage`. * The `system-cxx-std-lib` dependency is not read from cabal files. * Recache is not called on the packge database after the `.conf` file is generated, a more natural place for this rule is `registerRules`. Treating this uniformly like other packages is complicated by it not having any source code or a cabal file. However we can do a bit better by reporting the dependency firstly in `PackageData` and then needing the `.conf` file in the same place as every other package in `configurePackage`. Fixes #25303 - - - - - e61ada48 by Sven Tennie at 2026-01-16T22:19:16+01:00 ci: Increase timeout for emulators Test runs with emulators naturally take longer than on native machines. Generate jobs.yml - - - - - d5a745dd by Sven Tennie at 2026-01-16T22:19:17+01:00 ghc: Distinguish between having an interpreter and having an internal one Otherwise, we fail with warnings when compiling tools. Actually, these are related but different things: - ghc can run an interpreter (either internal or external) - ghc is compiled with an internal interpreter - - - - - 56f91636 by Matthew Pickering at 2026-01-16T22:19:17+01:00 ci: Javascript don't set CROSS_EMULATOR There is no CROSS_EMULATOR needed to run javascript binaries, so we don't set the CROSS_EMULATOR to some dummy value. - - - - - 61f47cb6 by Sven Tennie at 2026-01-16T22:19:17+01:00 Javascript skip T23697 See #22355 about how HSC2HS and the Javascript target don't play well together. - - - - - 89875fff by Sven Tennie at 2026-01-16T22:19:17+01:00 Mark T24602 as fragile It was skipped before (due to CROSS_EMULATOR being set, which changed for JS), so we don't make things worse by marking it as fragile. - - - - - 9a8afd5d by Sven Tennie at 2026-01-16T22:19:17+01:00 WIP: Dirty hack Let Stage0 build with the default.host.target file and decide for other stages if default.target cannot be used. Acutally, I don't like this logic on this level. - - - - - 53dfdb41 by Sven Tennie at 2026-01-16T22:19:17+01:00 Windows needs NM_STAGE0 as well The stage0 always needs nm. - - - - - e96d0e07 by Sven Tennie at 2026-01-16T22:19:17+01:00 T17912 sometimes works for windows-validate This seems to be timing related. However, just simply increasing the timeout (sleep) statement of this test didn't help. Maybe, it has been flaky on CI before. - - - - - 203 changed files: - .gitignore - .gitlab/ci.sh - .gitlab/generate-ci/gen_ci.hs - .gitlab/jobs.yaml - .gitmodules - CODEOWNERS - cabal.project-reinstall - compiler/GHC/Cmm.hs - compiler/GHC/Cmm/InitFini.hs - compiler/GHC/CmmToAsm/AArch64/Ppr.hs - compiler/GHC/CmmToAsm/Config.hs - compiler/GHC/CmmToAsm/PPC/CodeGen.hs - compiler/GHC/CmmToAsm/Ppr.hs - compiler/GHC/CmmToAsm/Reg/Linear.hs - compiler/GHC/CmmToAsm/Reg/Linear/StackMap.hs - compiler/GHC/CmmToAsm/Wasm/FromCmm.hs - compiler/GHC/CmmToAsm/X86/Ppr.hs - compiler/GHC/CmmToC.hs - compiler/GHC/CmmToLlvm/Data.hs - compiler/GHC/Core/Opt/Arity.hs - compiler/GHC/Core/Opt/Simplify/Env.hs - compiler/GHC/Core/Opt/Simplify/Iteration.hs - compiler/GHC/Core/Opt/Simplify/Utils.hs - compiler/GHC/Core/Opt/SpecConstr.hs - compiler/GHC/Core/Opt/Specialise.hs - compiler/GHC/Core/Opt/WorkWrap.hs - compiler/GHC/Core/Opt/WorkWrap/Utils.hs - compiler/GHC/Core/Rules.hs - compiler/GHC/Core/Tidy.hs - compiler/GHC/Core/Unfold.hs - compiler/GHC/Core/Unfold/Make.hs - compiler/GHC/Core/Utils.hs - compiler/GHC/CoreToStg/Prep.hs - compiler/GHC/Driver/CodeOutput.hs - compiler/GHC/Driver/Config/CmmToAsm.hs - compiler/GHC/Driver/DynFlags.hs - compiler/GHC/Driver/MakeFile.hs - compiler/GHC/Driver/Session.hs - compiler/GHC/Linker/Loader.hs - compiler/GHC/Linker/Unit.hs - compiler/GHC/Runtime/Interpreter/Init.hs - compiler/GHC/Settings/IO.hs - compiler/GHC/Stg/EnforceEpt.hs - compiler/GHC/Stg/Lint.hs - compiler/GHC/StgToCmm/Closure.hs - compiler/GHC/StgToCmm/Expr.hs - compiler/GHC/SysTools/Terminal.hs - compiler/GHC/Types/Id.hs - compiler/GHC/Types/Id/Info.hs - compiler/GHC/Types/Id/Make.hs - compiler/GHC/Unit/State.hs - compiler/GHC/Utils/Binary.hs - configure.ac - distrib/configure.ac.in - docs/users_guide/9.16.1-notes.rst - docs/users_guide/ghci.rst - docs/users_guide/packages.rst - docs/users_guide/phases.rst - docs/users_guide/using-concurrent.rst - docs/users_guide/using.rst - docs/users_guide/win32-dlls.rst - driver/ghci/ghci.c - driver/utils/cwrapper.c - driver/utils/isMinTTY.c - ghc/GHC/Driver/Session/Mode.hs - ghc/GHCi/UI.hs - ghc/Main.hs - ghc/ghc-bin.cabal.in - hadrian/README.md - hadrian/bindist/config.mk.in - hadrian/bindist/cwrappers/cwrapper.c - hadrian/cfg/default.host.target.in - + hadrian/cfg/system.config.host.in - hadrian/cfg/system.config.in - + hadrian/cfg/system.config.target.in - hadrian/doc/user-settings.md - hadrian/hadrian.cabal - hadrian/src/Base.hs - + hadrian/src/BindistConfig.hs - hadrian/src/Builder.hs - hadrian/src/Context.hs - hadrian/src/Expression.hs - hadrian/src/Flavour.hs - hadrian/src/Flavour/Type.hs - hadrian/src/Hadrian/Builder.hs - hadrian/src/Hadrian/Haskell/Cabal/Parse.hs - hadrian/src/Hadrian/Haskell/Cabal/Type.hs - hadrian/src/Hadrian/Haskell/Hash.hs - hadrian/src/Hadrian/Oracles/TextFile.hs - hadrian/src/Oracles/Flag.hs - hadrian/src/Oracles/Flavour.hs - hadrian/src/Oracles/Setting.hs - hadrian/src/Oracles/TestSettings.hs - hadrian/src/Packages.hs - hadrian/src/Rules.hs - hadrian/src/Rules/BinaryDist.hs - hadrian/src/Rules/CabalReinstall.hs - hadrian/src/Rules/Compile.hs - hadrian/src/Rules/Documentation.hs - hadrian/src/Rules/Generate.hs - hadrian/src/Rules/Gmp.hs - hadrian/src/Rules/Libffi.hs - hadrian/src/Rules/Library.hs - hadrian/src/Rules/Lint.hs - hadrian/src/Rules/Program.hs - hadrian/src/Rules/Register.hs - hadrian/src/Rules/Rts.hs - hadrian/src/Rules/SourceDist.hs - hadrian/src/Rules/Test.hs - hadrian/src/Settings.hs - hadrian/src/Settings/Builders/Cabal.hs - hadrian/src/Settings/Builders/Common.hs - hadrian/src/Settings/Builders/Configure.hs - hadrian/src/Settings/Builders/DeriveConstants.hs - hadrian/src/Settings/Builders/Ghc.hs - hadrian/src/Settings/Builders/Hsc2Hs.hs - hadrian/src/Settings/Builders/RunTest.hs - hadrian/src/Settings/Builders/SplitSections.hs - hadrian/src/Settings/Default.hs - hadrian/src/Settings/Flavours/Benchmark.hs - hadrian/src/Settings/Flavours/Development.hs - hadrian/src/Settings/Flavours/GhcInGhci.hs - hadrian/src/Settings/Flavours/Performance.hs - hadrian/src/Settings/Flavours/Quick.hs - hadrian/src/Settings/Flavours/QuickCross.hs - hadrian/src/Settings/Flavours/Quickest.hs - hadrian/src/Settings/Flavours/Validate.hs - hadrian/src/Settings/Packages.hs - hadrian/src/Settings/Program.hs - hadrian/src/Settings/Warnings.hs - − libffi-tarballs - libraries/base/base.cabal.in - libraries/base/changelog.md - libraries/base/src/Data/Bifoldable1.hs - libraries/base/src/GHC/Conc.hs - libraries/base/src/GHC/Conc/Sync.hs - − libraries/base/src/GHC/JS/Prim/Internal/Build.hs - libraries/base/tests/IO/T12010/cbits/initWinSock.c - libraries/base/tests/IO/all.T - libraries/base/tests/all.T - libraries/ghc-internal/cbits/consUtils.c - libraries/ghc-internal/configure.ac - libraries/ghc-internal/ghc-internal.cabal.in - libraries/ghc-internal/src/GHC/Internal/Conc/IO.hs - libraries/ghc-internal/src/GHC/Internal/Conc/POSIX.hs - libraries/ghc-internal/src/GHC/Internal/Conc/Sync.hs - libraries/ghc-internal/src/GHC/Internal/Conc/Sync.hs-boot - libraries/ghc-internal/src/GHC/Internal/Conc/Windows.hs - libraries/ghc-internal/src/GHC/Internal/ConsoleHandler.hsc - libraries/ghc-internal/src/GHC/Internal/Event/Thread.hs - libraries/ghc-internal/src/GHC/Internal/Event/Windows/Thread.hs - libraries/ghc-internal/src/GHC/Internal/IO/Handle.hs - + libraries/ghc-internal/src/GHC/Internal/STM.hs - libraries/ghc-internal/src/GHC/Internal/System/Environment/ExecutablePath.hsc - libraries/ghc-platform/src/GHC/Platform/ArchOS.hs - + libraries/libffi-clib - libraries/mtl - m4/fp_find_nm.m4 - m4/fptools_set_platform_vars.m4 - m4/ghc_select_file_extensions.m4 - m4/prep_target_file.m4 - packages - rts/RtsFlags.c - rts/StgMiscClosures.cmm - rts/include/rts/ghc_ffi.h - rts/rts.buildinfo.in - rts/rts.cabal - testsuite/driver/perf_notes.py - testsuite/driver/runtests.py - testsuite/driver/testglobals.py - testsuite/driver/testlib.py - testsuite/ghc-config/ghc-config.hs - testsuite/mk/test.mk - + testsuite/tests/dmdanal/should_run/T26748.hs - + testsuite/tests/dmdanal/should_run/T26748.stdout - testsuite/tests/dmdanal/should_run/all.T - − testsuite/tests/driver/T24731.hs - testsuite/tests/driver/all.T - testsuite/tests/ghc-e/should_fail/all.T - testsuite/tests/interface-stability/base-exports.stdout - testsuite/tests/interface-stability/base-exports.stdout-javascript-unknown-ghcjs - testsuite/tests/interface-stability/base-exports.stdout-mingw32 - testsuite/tests/interface-stability/base-exports.stdout-ws-32 - testsuite/tests/javascript/closure/all.T - testsuite/tests/rts/linker/rdynamic.hs - testsuite/tests/simplCore/should_compile/T14003.stderr - testsuite/tests/simplCore/should_compile/T18013.stderr - testsuite/tests/simplCore/should_compile/T19672.stderr - testsuite/tests/simplCore/should_compile/T21763.stderr - testsuite/tests/simplCore/should_compile/T21763a.stderr - + testsuite/tests/simplCore/should_compile/T26615.hs - + testsuite/tests/simplCore/should_compile/T26615.stderr - + testsuite/tests/simplCore/should_compile/T26615a.hs - + testsuite/tests/simplCore/should_compile/T26682.hs - + testsuite/tests/simplCore/should_compile/T26682a.hs - + testsuite/tests/simplCore/should_compile/T26722.hs - + testsuite/tests/simplCore/should_compile/T26722.stderr - testsuite/tests/simplCore/should_compile/T4908.stderr - testsuite/tests/simplCore/should_compile/all.T - testsuite/tests/simplCore/should_compile/spec-inline.stderr - utils/ghc-pkg/Main.hs - − utils/iserv/iserv.cabal.in - − utils/iserv/src/Main.hs The diff was not included because it is too large. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/676d7b3648db4356da10b206c379da… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/676d7b3648db4356da10b206c379da… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc] Pushed new branch wip/andreask/string_mr
by Andreas Klebinger (＠AndreasK) 16 Jan '26

16 Jan '26

Andreas Klebinger pushed new branch wip/andreask/string_mr at Glasgow Haskell Compiler / GHC -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/andreask/string_mr You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc][wip/andreask/ghc_rts_K] RTS: Document -K behaviour better
by Andreas Klebinger (＠AndreasK) 16 Jan '26

16 Jan '26

Andreas Klebinger pushed to branch wip/andreask/ghc_rts_K at Glasgow Haskell Compiler / GHC Commits: 04271c5d by Andreas Klebinger at 2026-01-16T19:57:15+01:00 RTS: Document -K behaviour better - - - - - 1 changed file: - docs/users_guide/runtime_control.rst Changes: ===================================== docs/users_guide/runtime_control.rst ===================================== @@ -866,6 +866,11 @@ performance. This option is there mainly to stop the program eating up all the available memory in the machine if it gets into an infinite loop. + Note that if the process is termined through a ``StackOverflow`` exception + the reported stack usage is not representative of actual stack use. It + reports stack use during error handling, rather than stack use at the time + the exception was raised initially. + .. rts-flag:: -m ⟨n⟩ :default: 3% View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/04271c5d01e3727516463f3bd1b5ce0… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/04271c5d01e3727516463f3bd1b5ce0… You're receiving this email because of your account on gitlab.haskell.org.

1 0

[Git][ghc/ghc] Pushed new branch wip/andreask/ghc_rts_K
by Andreas Klebinger (＠AndreasK) 16 Jan '26

16 Jan '26

Andreas Klebinger pushed new branch wip/andreask/ghc_rts_K at Glasgow Haskell Compiler / GHC -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/andreask/ghc_rts_K You're receiving this email because of your account on gitlab.haskell.org.

1 0