September 2026 - ghc-commits

[Git][ghc/ghc][wip/apk/tag-strict-bot] Fix a few tag inference bugs.
by Andreas Klebinger (＠AndreasK) 26 Sep '26

26 Sep '26

Andreas Klebinger pushed to branch wip/apk/tag-strict-bot at Glasgow Haskell Compiler / GHC Commits: 44222807 by Andreas Klebinger at 2026-09-26T13:12:34+00:00 Fix a few tag inference bugs. * Treat bottoming functions and nullary join points as functions. * When generating bytecode don't rely on imported tag sigs. Fixes #27831, #27841 and #27842. - - - - - 23 changed files: - + changelog.d/T27831-bottoming-strict-field - + changelog.d/T27842-bytecode-imported-tags - compiler/GHC/Stg/EnforceEpt.hs - compiler/GHC/Stg/EnforceEpt/Rewrite.hs - compiler/GHC/Stg/EnforceEpt/Types.hs - + testsuite/tests/bytecode/T27842.hs - + testsuite/tests/bytecode/T27842.stdout - + testsuite/tests/bytecode/T27842A.hs - + testsuite/tests/bytecode/T27842N.hs - testsuite/tests/bytecode/all.T - testsuite/tests/simplStg/should_compile/all.T - + testsuite/tests/simplStg/should_compile/inferTags005.hs - + testsuite/tests/simplStg/should_compile/inferTags005.stderr - + testsuite/tests/simplStg/should_compile/inferTags006.hs - + testsuite/tests/simplStg/should_compile/inferTags006.stderr - + testsuite/tests/simplStg/should_run/InferTags007_A.hs - + testsuite/tests/simplStg/should_run/T27831.hs - + testsuite/tests/simplStg/should_run/T27831.stdout - + testsuite/tests/simplStg/should_run/T27857.hs - + testsuite/tests/simplStg/should_run/T27857.stdout - testsuite/tests/simplStg/should_run/all.T - + testsuite/tests/simplStg/should_run/inferTags007.hs - + testsuite/tests/simplStg/should_run/inferTags007.stdout Changes: ===================================== changelog.d/T27831-bottoming-strict-field ===================================== @@ -0,0 +1,8 @@ +section: compiler +issues: #27831 +mrs: !16719 +synopsis: + Fix a segfault that could occur when a bottoming function was stored in a strict field. +description: + This was happening when a function that always diverges (e.g. ``\_ -> error "..."``) was stored in a strict field, and the constructor was pattern matched on + in "nearby" code where the structure of the constructor application was still visible to GHC. ===================================== changelog.d/T27842-bytecode-imported-tags ===================================== @@ -0,0 +1,6 @@ +section: bytecode +issues: #27842 +mrs: !16719 +synopsis: + Fix a segfault caused by reusing interface files generated with + ``-fbyte-code-and-object-code`` for interpreter sessions using ``-fprefer-byte-code``. ===================================== compiler/GHC/Stg/EnforceEpt.hs ===================================== @@ -334,9 +334,15 @@ a) Tags for let-bindings: b) When referencing ids from other modules the Cmm backend will try to put a proper tag on these references through various means. When doing analysis we usually predict these cases to improve precision of the analysis. - But to my knowledge the bytecode generator makes no such attempts so we must - not infer imported bindings as tagged. - This is handled in GHC.Stg.EnforceEpt.Types.lookupInfo + The bytecode generator gives fewer guarantees about what it tags. + So we simply assume it fails to tag binders, even in the cases where it does. + + This is handled in GHC.Stg.EnforceEpt.Types.argTagInfo + + Eventually we will want to update the Analysis and bco code gen to uphold and + take advantage of tag inference at least to some degree. But for now it's + not a perf benefit for interpreted code, and essentially only run to uphold + the "strict field invariant"/EPT Invariant described in EPT enforcement. -} @@ -359,7 +365,7 @@ enforceEpt ppr_opts !for_bytecode logger this_mod stg_binds = do -- Rewrite STG to uphold the strict field invariant us_t <- mkSplitUniqSupply StgTag - let rewritten_binds = {-# SCC "StgEptRewrite" #-} rewriteTopBinds this_mod us_t stg_binds_w_tags :: [TgStgTopBinding] + let rewritten_binds = {-# SCC "StgEptRewrite" #-} rewriteTopBinds for_bytecode this_mod us_t stg_binds_w_tags :: [TgStgTopBinding] return (rewritten_binds,export_tag_info) @@ -414,12 +420,14 @@ inferTagExpr env (StgApp fun args) | isDeadEndAppSig (idDmdSig fun) (length args) = TagBottoming - | fun_arity == 0 -- Unknown arity => Thunk or unknown call + | not (isJoinId fun) -- zero arity join ids behave like functions. + , fun_arity == 0 -- Unknown arity => Thunk or unknown call = TagDunno -- Imported function with known return tag | Just (TagFun res_info) <- tagSigInfo (idInfo fun) , fun_arity == length args -- Saturated + , not (te_bytecode env) -- #27842 = res_info -- Local function with known return tag @@ -613,8 +621,8 @@ it safely any tag sig we like. So we give it TagBottoming, as it allows the combined tag sig of the case expression to be the combination of all non-bottoming branches. -NB: After the analysis is done we go back to treating bottoming functions as -untagged to ensure they are evaluated as expected in code like: +NB: We now distinguish functions from values. Allowing us to treat bottom functions +as tagged, while still doing the right thing for bottom values in code like: case bottom_id of { ...} ===================================== compiler/GHC/Stg/EnforceEpt/Rewrite.hs ===================================== @@ -13,7 +13,7 @@ import GHC.Builtin.PrimOps ( PrimOp(..) ) import GHC.Types.Basic ( CbvMark (..), isMarkedCbv , TopLevelFlag(..), isTopLevel ) import GHC.Types.Id -import GHC.Types.Name +import GHC.Types.Name ( nameIsLocalOrFrom ) import GHC.Types.Unique.Supply import GHC.Types.Unique.FM import GHC.Types.RepType @@ -22,10 +22,7 @@ import GHC.Unit.Types import GHC.Core.DataCon import GHC.Core ( AltCon(..) ) -import GHC.Core.Type - -import GHC.StgToCmm.Types -import GHC.StgToCmm.Closure (importedIdLFInfo) +import GHC.Core.Type ( definitelyLiftedType ) import GHC.Stg.Utils import GHC.Stg.Syntax as StgSyn @@ -41,7 +38,7 @@ import GHC.Stg.EnforceEpt.Types import Control.Monad -newtype RM a = RM { unRM :: (State (UniqFM Id TagSig, UniqSupply, Module, IdSet) a) } +newtype RM a = RM { unRM :: (State (UniqFM Id TagSig, UniqSupply, Module, IdSet, Bool) a) } deriving (Functor, Monad, Applicative) ------------------------------------------------------------ @@ -108,29 +105,34 @@ when building the free variable list. instance MonadUnique RM where getUniqueSupplyM = RM $ do - (m, us, mod,lcls) <- get + (m, us, mod,lcls,for_bytecode) <- get let (us1, us2) = splitUniqSupply us - (put) (m,us2,mod,lcls) + (put) (m,us2,mod,lcls,for_bytecode) return us1 getMap :: RM (UniqFM Id TagSig) -getMap = RM $ ((\(fst,_,_,_) -> fst) <$> get) +getMap = RM $ ((\(fst,_,_,_,_) -> fst) <$> get) setMap :: (UniqFM Id TagSig) -> RM () setMap !m = RM $ do - (_,us,mod,lcls) <- get - put (m, us,mod,lcls) - -getMod :: RM Module -getMod = RM $ ( (\(_,_,thrd,_) -> thrd) <$> get) + (_,us,mod,lcls,for_bytecode) <- get + put (m, us,mod,lcls,for_bytecode) getFVs :: RM IdSet -getFVs = RM $ ((\(_,_,_,lcls) -> lcls) <$> get) +getFVs = RM $ ((\(_,_,_,lcls,_) -> lcls) <$> get) setFVs :: IdSet -> RM () setFVs !fvs = RM $ do - (tag_map,us,mod,_lcls) <- get - put (tag_map, us,mod,fvs) + (tag_map,us,mod,_lcls,for_bytecode) <- get + put (tag_map, us,mod,fvs,for_bytecode) + +getMod :: RM Module +getMod = RM $ ( (\(_,_,c,_,_) -> c) <$> get) + +-- | When generating bytecode certain bindings might be untagged. So we have to +-- have a way to check for that. +getForBytecode :: RM Bool +getForBytecode = RM $ ((\(_,_,_,_,for_bytecode) -> for_bytecode) <$> get) -- Rewrite the RHS(s) while making the id and it's sig available -- to determine if things are tagged/need to be captured as FV. @@ -238,51 +240,26 @@ indicates a bug in the tag inference implementation. For this reason we assert that we are running in interactive mode if a lookup fails. -} isTagged :: Id -> RM Bool -isTagged v - -- See Note [Bottom functions are TagBottoming] - | isDeadEndId v = pure False - | otherwise = do +isTagged v = do + for_bytecode <- getForBytecode this_mod <- getMod - -- See Note [Tag inference for interactive contexts] - let lookupDefault v = assertPpr (isInteractiveModule this_mod) - (text "unknown Id:" <> ppr this_mod <+> ppr v) - (TagVal TagDunno) - case nameIsLocalOrFrom this_mod (idName v) of - True - | definitelyUnliftedType (idType v) - -- NB: v might be the Id of a representation-polymorphic join point, - -- so we shouldn't use isUnliftedType here. See T22212. - -> return True - | otherwise -> do -- Local binding - !s <- getMap - let !sig = lookupWithDefaultUFM s (lookupDefault v) v - return $ case sig of - TagFun _ -> True -- function closure is tagged - TagVal TagDunno -> False - TagVal TagEPT -> True - TagVal TagBottoming -> True - TagVal (TagTuple _) -> True -- Consider unboxed tuples tagged. - -- Imported - False -> return $! - -- Determine whether it is tagged from the LFInfo of the imported id. - -- See Note [The LFInfo of Imported Ids] - case importedIdLFInfo v of - -- Function, applied not entered. - LFReEntrant {} - -> True - -- Thunks need to be entered. - LFThunk {} - -> False - -- LFCon means we already know the tag, and it's tagged. - LFCon {} - -> True - LFUnknown {} - -> False - LFUnlifted {} -- Unboxed, tagging irrelevant - -> True - LFLetNoEscape {} - -- Shouldn't be possible. I don't think we can export letNoEscapes - -> True + s <- getMap + let get_env_sig = lookupUFM s + massertPpr + -- Assert the env is complete for local lifted binders, which means either + -- - The binder is present in the env + -- - The binder is not a local lifted binder *or* comes from a ghci context + (isJust (get_env_sig v) + -- See Note [Tag inference for interactive contexts] + || isInteractiveModule this_mod + || not (nameIsLocalOrFrom this_mod (idName v)) + || not (definitelyLiftedType (idType v))) + (text "unknown Id:" <> ppr this_mod <+> ppr v) + -- TODO: We could refactor the whole pass such that we also set id_tagSig + -- for every imported id. But this likely comes with a heavy allocation + -- overhead so for now we just ensure to use the same logic across analysis + -- and rewriter. + pure $! isTaggedInfo $ argTagInfo for_bytecode (get_env_sig v) (StgVarArg v) isArgTagged :: StgArg -> RM Bool @@ -299,11 +276,12 @@ mkLocalArgId id = do --------------------------- -rewriteTopBinds :: Module -> UniqSupply -> [GenStgTopBinding 'InferTaggedBinders] -> [TgStgTopBinding] -rewriteTopBinds mod us binds = +rewriteTopBinds :: Bool -- ^ Generating bytecode? + -> Module -> UniqSupply -> [GenStgTopBinding 'InferTaggedBinders] -> [TgStgTopBinding] +rewriteTopBinds for_bytecode mod us binds = let doBinds = mapM rewriteTop binds - in evalState (unRM doBinds) (mempty, us, mod, mempty) + in evalState (unRM doBinds) (mempty, us, mod, mempty, for_bytecode) rewriteTop :: InferStgTopBinding -> RM TgStgTopBinding rewriteTop (StgTopStringLit v s) = return $! (StgTopStringLit v s) ===================================== compiler/GHC/Stg/EnforceEpt/Types.hs ===================================== @@ -12,7 +12,7 @@ where import GHC.Prelude import GHC.Core.DataCon -import GHC.Core.Type (isUnliftedType) +import GHC.Core.Type (isUnliftedType, definitelyUnliftedType) import GHC.Types.Id import GHC.Stg.Syntax import GHC.Stg.EnforceEpt.TagSig as TagSig @@ -22,6 +22,7 @@ import GHC.Utils.Misc( zipWithEqual ) import GHC.Utils.Panic import GHC.StgToCmm.Types +import GHC.StgToCmm.Closure (importedIdLFInfo) {- ********************************************************************* * * @@ -97,31 +98,39 @@ lookupReturnInfo env fun = case lookupVarEnv (te_env env) fun of Just (TagVal _) -> Nothing Nothing -> Nothing --- | Look up a value-level tag for an argument: either from the env (where --- a function-typed argument flattens to TagEPT — its closure is tagged) --- or derived from information on the variable itself. -lookupInfo :: TagEnv p -> StgArg -> TagInfo -lookupInfo env (StgVarArg var) +-- | Look up a value-level tag. +-- +-- If the tag info is completely determined by Id info we use that tag. +-- If the tag info is dependent on the analysis/call site use the passed TagSig. +-- If the passed TagSig is Nothing we fall back to safe tag info based on id properties. +argTagInfo :: Bool -> (Maybe TagSig) -> StgArg -> TagInfo +{-# INLINE argTagInfo #-} -- Specialize for the call site. +argTagInfo _for_bytecode _env_sig (StgLitArg{}) = TagEPT +argTagInfo for_bytecode env_sig (StgVarArg var) -- Nullary data constructors like True, False | Just dc <- isDataConWorkId_maybe var , isNullaryRepDataCon dc , not for_bytecode = TagEPT - | isUnliftedType (idType var) + -- NB: v might be the Id of a representation-polymorphic join point, + -- so we shouldn't use isUnliftedType here. See T22212. + | definitelyUnliftedType (idType var) = TagEPT -- Variables in the environment. A function binding flattens to TagEPT -- since a function closure pointer is properly tagged; its return info -- is not relevant when the function is used as a value. - | Just sig <- lookupVarEnv (te_env env) var + | Just sig <- env_sig = case sig of TagVal info -> info TagFun _ -> TagEPT - | Just lf_info <- idLFInfo_maybe var - , not for_bytecode - = case lf_info of +-- Always save defaults. + | lf_info <- importedIdLFInfo var -- will make up LFInfo if not present. + = if for_bytecode then TagDunno + else + case lf_info of -- Function, tagged (with arity) LFReEntrant {} -> TagEPT @@ -138,13 +147,12 @@ lookupInfo env (StgVarArg var) -- Shouldn't be possible. I don't think we can export letNoEscapes LFLetNoEscape {} -> panic "LFLetNoEscape exported" - | otherwise - = TagDunno - where - for_bytecode = te_bytecode env - -lookupInfo _ (StgLitArg {}) - = TagEPT +-- | Get tag info using the environment. +lookupInfo :: TagEnv p -> StgArg -> TagInfo +lookupInfo env arg@(StgVarArg var) = + let env_sig = (lookupVarEnv (te_env env) var) + in argTagInfo (te_bytecode env) env_sig arg +lookupInfo _env (StgLitArg{}) = TagEPT isDunnoSig :: TagSig -> Bool isDunnoSig (TagVal TagDunno) = True ===================================== testsuite/tests/bytecode/T27842.hs ===================================== @@ -0,0 +1,42 @@ +{-# LANGUAGE UnboxedTuples #-} +{-# OPTIONS_GHC -fno-worker-wrapper -fno-cpr-anal #-} +-- Regression test for #27842. +-- +-- The basic rundown is this: +-- We produce one interface file, however we store information dependent on the +-- code generation method in the interface file. +-- +-- We happen to pick the native code information to store in the interface file. +-- +-- When we compile a module M this way, and then generate byte code for code +-- depending on M based on M.hi we will assume certain exported definitions are EPT +-- tagged, despite the interpreter doing no such thing. +-- +-- This then led to crashes in the interpreter. +-- +-- We test three kinds of imported definitions: +-- * mk uses fun, a function whose TagSig says its result is tagged. +-- * bar uses just_con, a value whose LFInfo says it is a constructor. +-- * baz uses gt_con, the same for a nullary constructor. +module Main where + +import T27842A (fun, just_con, gt_con) +import T27842N (S(..), use_S, M(..), use_M, N(..), use_N) + +mk :: Int -> S +mk x = case fun x of (# xs, _ #) -> S xs +{-# NOINLINE mk #-} + +bar :: M +bar = M just_con +{-# NOINLINE bar #-} + +baz :: N +baz = N gt_con +{-# NOINLINE baz #-} + +main :: IO () +main = do + print (use_S (mk 42)) + print (use_M bar) + print (use_N baz) ===================================== testsuite/tests/bytecode/T27842.stdout ===================================== @@ -0,0 +1,3 @@ +42 +42 +3 ===================================== testsuite/tests/bytecode/T27842A.hs ===================================== @@ -0,0 +1,19 @@ +{-# LANGUAGE UnboxedTuples #-} +{-# OPTIONS_GHC -fno-worker-wrapper -fno-cpr-anal #-} +module T27842A (fun, just_con, gt_con) where + +-- The native EPT run gives fun the TagSig TagFun[TagTuple[TagEPT, TagDunno]]: +fun :: Int -> (# [Int], Int #) +fun x = let xs = x : xs in (# xs, x #) +{-# NOINLINE fun #-} + +-- In native code a static constructor, in bytecode an unevaluated closure. +just_con :: Maybe Int +just_con = Just 42 +{-# NOINLINE just_con #-} + +-- The same for a nullary constructor. Without its pointer tag, the object code +-- in T27842N would take the LT alternative, so GT shows the difference. +gt_con :: Ordering +gt_con = GT +{-# NOINLINE gt_con #-} ===================================== testsuite/tests/bytecode/T27842N.hs ===================================== @@ -0,0 +1,26 @@ +{-# OPTIONS_GHC -fno-byte-code-and-object-code #-} +-- We compile this module as native code, depending on A's interface file. +-- A itself is loaded into GHCi, despite it's interface file being generated based +-- on native code generation. +module T27842N (S(..), use_S, M(..), use_M, N(..), use_N) where + +data S = S ![Int] + +-- We take apart the strict constructor value and branch on the value in its field. +-- If the field content is not EPT this causes undefined behaviour. + +use_S :: S -> Int +use_S (S xs) = case xs of { (y:_) -> y; [] -> -1 } +{-# NOINLINE use_S #-} + +data M = M !(Maybe Int) + +use_M :: M -> Int +use_M (M m) = case m of { Just x -> x; Nothing -> -1 } +{-# NOINLINE use_M #-} + +data N = N !Ordering + +use_N :: N -> Int +use_N (N o) = case o of { LT -> 1; EQ -> 2; GT -> 3 } +{-# NOINLINE use_N #-} ===================================== testsuite/tests/bytecode/all.T ===================================== @@ -17,3 +17,12 @@ test('T26216', extra_files(["T26216_aux.hs"]), ghci_script, ['T26216.script']) test('T27001', [extra_files(['T27001.hs']), req_interp], run_command, ['{compiler} -e main -O -fno-unoptimized-core-for-interpreter T27001.hs']) + +# Bytecode must not trust tag information from imported interfaces, which +# comes from native code (#27842): neither the TagSig of an imported function +# nor the LFInfo of an imported value (with and without constructor fields). +test('T27842', [extra_files(['T27842A.hs', 'T27842N.hs']), req_interp], + run_command, + ['{compiler} -e main -O -fno-unoptimized-core-for-interpreter ' + '-fobject-code -fbyte-code-and-object-code -fwrite-byte-code -fprefer-byte-code ' + 'T27842.hs']) ===================================== testsuite/tests/simplStg/should_compile/all.T ===================================== @@ -25,5 +25,17 @@ test('inferTags003', [ only_ways(['optasm']), ], compile, ['-ddump-cmm -dno-typeable-binds -O']) test('inferTags004', normal, compile, ['-O -ddump-stg-tags -dno-typeable-binds -dsuppress-uniques']) test('T27005b', normal, compile, ['-O -ddump-stg-tags -dno-typeable-binds -dsuppress-uniques']) +# Both f and the join point j should have a signature TagTuple[TagEPT, TagEPT] +test('inferTags005', + grep_errmsg(r'(TagTuple\[TagEPT, TagEPT\])', [1]), + compile, + ['-O -fno-worker-wrapper -fno-cpr-anal -ddump-stg-tags ' + '-dno-typeable-binds -dsuppress-uniques']) +# The function needs to have a signature TagTuple[TagEPT, TagEPT] +test('inferTags006', + grep_errmsg(r'(TagTuple\[TagEPT, TagEPT\])', [1]), + compile, + ['-O -fno-worker-wrapper -fno-cpr-anal -fno-full-laziness -ddump-stg-tags ' + '-dno-typeable-binds -dsuppress-uniques']) test('T24806', grep_errmsg('^\\(T24806\\.\\$wgo'), compile, ['-O -ddump-stg-tags -dno-typeable-binds -dsuppress-uniques']) ===================================== testsuite/tests/simplStg/should_compile/inferTags005.hs ===================================== @@ -0,0 +1,39 @@ +{-# LANGUAGE UnboxedTuples #-} +module EnforceEpt005 where + +-- If we have +-- f x y = +-- join j = +-- <rhs> -- <TagTuple[TagEPT, TagEPT]]> +-- in case x of +-- 1 -> j +-- 2 -> j +-- _ -> +-- <something> -- <TagTuple[TagEPT, TagEPT]]> + +-- Consider the case where rhs and something both represent a tag value of <TagTuple[TagEPT, TagEPT]]> +-- In this case we want `f` to also give rise to TagFun [TagTuple[TagEPT, TagEPT]]] + +-- To achieve this we have to recognize j as a zero-arity function equivalent +-- which is what this test checks. + +-- The payoff is in `g` `r` is then known to be tagged, so `S r` needs no eval. +-- Only an unboxed tuple result exposes this. + +-- We disable worker/wrapper and CPR so `f` matches more closely the tests source. + +data T = A Int Int Int Int Int Int | B + +f :: Int -> Int -> (# T, T #) +f x y = case x of + 0 -> j + 1 -> j + _ -> (# B, B #) + where + j = (# A (y+1) (y*2) (y-3) (y*y) (y+x) (y*x), B #) +{-# NOINLINE f #-} + +data S = S !T + +g :: Int -> Int -> S +g x y = case f x y of (# r, _ #) -> S r ===================================== testsuite/tests/simplStg/should_compile/inferTags005.stderr ===================================== @@ -0,0 +1,2 @@ +TagTuple[TagEPT, TagEPT] +TagTuple[TagEPT, TagEPT] ===================================== testsuite/tests/simplStg/should_compile/inferTags006.hs ===================================== @@ -0,0 +1,31 @@ +{-# LANGUAGE UnboxedTuples #-} +module EnforceEpt006 where + +-- If we have +-- f x y = +-- join j = +-- <rhs> -- TagBottoming +-- in case x of +-- 1 -> j +-- 2 -> j +-- _ -> +-- <something> -- <TagTuple[TagEPT, TagEPT]]> + +-- Similar to inferTage005 we want to give `f` the signature: TagFun <TagTuple[TagEPT, TagEPT]]> +-- This requires us to give `j` a `TagFun[TagBottoming]` signature, which is safe because +-- either its execution will diverge, or the resulting tuple *will* have two +-- tagged values. + +data T = A Int Int Int Int Int Int | B + +f :: Int -> Int -> (# T, T #) +-- This case-of-case is just here to be optimized into a nullary join point. +f x y = case (case x of { 0 -> False; 1 -> False; _ -> True }) of + False -> error ("f: bad input " ++ show x ++ " " ++ show y ++ " " ++ show (x*y)) + True -> (# A (y+1) (y*2) (y-3) (y*y) (y+x) (y*x), B #) +{-# NOINLINE f #-} + +data S = S !T + +g :: Int -> Int -> S +g x y = case f x y of (# r, _ #) -> S r ===================================== testsuite/tests/simplStg/should_compile/inferTags006.stderr ===================================== @@ -0,0 +1 @@ +TagTuple[TagEPT, TagEPT] ===================================== testsuite/tests/simplStg/should_run/InferTags007_A.hs ===================================== @@ -0,0 +1,20 @@ +-- We suppress arity and LfInfo with the option. +{-# OPTIONS_GHC -fomit-interface-pragmas #-} +module InferTags007_A (fun, caf, bot, con) where + +fun :: Int -> Int +fun x = x + 1 +{-# NOINLINE fun #-} + +-- A CAF/thunk +caf :: [Int] +caf = map (* 2) [1 .. 10] +{-# NOINLINE caf #-} + +bot :: Int -> Int +bot _ = error "bot called" +{-# NOINLINE bot #-} + +con :: Maybe Int +con = Just 42 +{-# NOINLINE con #-} ===================================== testsuite/tests/simplStg/should_run/T27831.hs ===================================== @@ -0,0 +1,35 @@ +-- Regression test for #27831: a bottoming function stored in a strict +-- constructor field. +-- +-- Different parts of the tag inference machinery didn't agree on weither or not +-- a bottoming function should be treated as a EPT value, leading to a segfault. +module Main (main) where + +import Control.Exception +import GHC.Exts.Heap (GenClosure(..), getClosureData) +import System.Exit + +data T = MkT Int !(Int -> Int) + +t :: T +t = MkT 1 (\_ -> error "T27831") +{-# NOINLINE t #-} + +f :: () -> T +f _ = t +{-# OPAQUE f #-} + +main :: IO () +main = do + c <- getClosureData t + case c of + ThunkClosure{} -> putStrLn "FAIL: ThunkClosure" >> exitFailure + APClosure{} -> putStrLn "FAIL: APClosure" >> exitFailure + _ -> putStrLn "OK: not a thunk" + + case f () of MkT n _ -> print n + + r <- try (evaluate (case t of MkT _ g -> g 1)) + case r of + Left (ErrorCall msg) -> putStrLn ("OK: " ++ msg) + Right v -> putStrLn ("FAIL: got " ++ show v) >> exitFailure ===================================== testsuite/tests/simplStg/should_run/T27831.stdout ===================================== @@ -0,0 +1,3 @@ +OK: not a thunk +1 +OK: T27831 ===================================== testsuite/tests/simplStg/should_run/T27857.hs ===================================== @@ -0,0 +1,45 @@ +{-# LANGUAGE StrictData #-} +-- Regression test from #27857: We store a function that loops indefinitely +-- in a strict field. +module Main (main) where +import Control.Monad + +data Body + = BNone + | BStream ((Int -> IO ()) -> IO () -> IO ()) + | BIface (Int -> IO ()) + | BBuilder String + | BFile Int + +data Obj = Obj [String] Body Int + +newtype Resp = Resp Obj + +stream :: Int -> [String] -> ((Int -> IO ()) -> IO () -> IO ()) -> Resp +stream st hdr b = Resp $ Obj (show st : hdr) (BStream b) 0 + +noBody :: Int -> [String] -> Resp +noBody st hdr = Resp $ Obj (show st : hdr) BNone 0 + +infinite :: Resp +infinite = stream 200 ["text/plain"] body + where + body :: (Int -> IO ()) -> IO () -> IO () + body write flush = do + let go n = write n *> flush *> go (succ n) + go (0 :: Int) + +other :: Resp +other = noBody 404 [] + +name :: Body -> String +name b = case b of + BNone -> "None" + BStream _ -> "Stream" + BIface _ -> "Iface" + BBuilder _ -> "Builder" + BFile _ -> "File" + +main :: IO () +main = forM_ [("infinite", infinite), ("other", other)] $ \(n, Resp (Obj _ b _)) -> + putStrLn $ n ++ "=" ++ name b ===================================== testsuite/tests/simplStg/should_run/T27857.stdout ===================================== @@ -0,0 +1,2 @@ +infinite=Stream +other=None ===================================== testsuite/tests/simplStg/should_run/all.T ===================================== @@ -3,13 +3,15 @@ # extra run flags # expected process return value, if not zero -# Only compile with optimisation +# Only run optimised code, native and interpreted: +# We now generate bytecode from STG so we should test native and bytecode. def f( name, opts ): - opts.only_ways = ['optasm'] + opts.only_ways = ['optasm', 'ghci-opt'] setTestOpts(f) -test('T9291', normal, compile_and_run, ['']) +# Breakpoint ticks would break CSE which this tests. +test('T9291', [omit_ways(['ghci']), extra_hc_opts('-fno-break-points')], compile_and_run, ['']) test('T13536', normal, compile_and_run, ['']) test('T13536a', @@ -20,6 +22,16 @@ test('T13536a', test('inferTags001', normal, multimod_compile_and_run, ['inferTags001', 'inferTags001_a']) test('T22042', [extra_files(['T22042a.hs']),only_ways('normal'),unless(have_dynamic(), skip)], makefile_test, ['T22042']) -test('T23783', normal, multimod_compile_and_run, ['T23783', '-O -v0']) -test('unpack_enum', normal, compile_and_run, ['']) -test('T27005a', normal, compile_and_run, ['']) + +# Depends on tag inference being similarly effective for bytecode which it is not yet. +test('T23783', omit_ghci, multimod_compile_and_run, ['T23783', '-O -v0']) + +# Requires UNPACK which needs -O +test('unpack_enum', omit_ways(['ghci']), compile_and_run, ['']) + +# Tests that tag inference optimizes well, which is not the case for bytecode or +# when we insert profiling ticks. +test('T27005a', omit_ways(ghci_ways + prof_ways), compile_and_run, ['']) +test('T27831', omit_ways(ghci_ways + prof_ways), compile_and_run, ['']) +test('inferTags007', [extra_files(['InferTags007_A.hs'])], multimod_compile_and_run, ['inferTags007', '-O -v0']) +test('T27857', normal, compile_and_run, ['']) ===================================== testsuite/tests/simplStg/should_run/inferTags007.hs ===================================== @@ -0,0 +1,109 @@ +{-# LANGUAGE MagicHash #-} +-- This test sanity checks the tag info we generate for imported binders which +-- have no real info in the .hi file. +-- +-- This is important to avoid running into cases where we optimistically +-- generated better information based on things like type than the +-- compiled code actually provided. For example GHCi doesn't ensure tagging +-- of constructors. +module Main (main) where + +import Control.Exception +import Control.Monad +import GHC.Exts (Addr#) +import GHC.Exts.Heap (GenClosure(..), getClosureData) +import GHC.Internal.Control.Exception.Base (patError) +import System.Exit + +import qualified InferTags007_A as A + +data S a = S !a + +data P = MkP !(Addr# -> Int) + +-- Put the imported values into a strict field of a top level Con +con_top_fun :: S (Int -> Int) +con_top_fun = S A.fun +{-# NOINLINE con_top_fun #-} + +con_top_caf :: S [Int] +con_top_caf = S A.caf +{-# NOINLINE con_top_caf #-} + +con_top_bot :: S (Int -> Int) +con_top_bot = S A.bot +{-# NOINLINE con_top_bot #-} + +con_top_con :: S (Maybe Int) +con_top_con = S A.con +{-# NOINLINE con_top_con #-} + +con_top_pat :: P +con_top_pat = MkP patError +{-# NOINLINE con_top_pat #-} + +-- Put the imported values into a strict field of a Con inside a rhs +expr_fun :: () -> S (Int -> Int) +expr_fun _ = S A.fun +{-# OPAQUE expr_fun #-} + +expr_caf :: () -> S [Int] +expr_caf _ = S A.caf +{-# OPAQUE expr_caf #-} + +expr_bot :: () -> S (Int -> Int) +expr_bot _ = S A.bot +{-# OPAQUE expr_bot #-} + +expr_con :: () -> S (Maybe Int) +expr_con _ = S A.con +{-# OPAQUE expr_con #-} + +-- Actually use the field. +use_S_head :: S [Int] -> Int +use_S_head (S xs) = case xs of { (y:_) -> y; [] -> -1 } +{-# NOINLINE use_S_head #-} + +use_S_fromJust :: S (Maybe Int) -> Int +use_S_fromJust (S m) = case m of { Just x -> x; Nothing -> -1 } +{-# NOINLINE use_S_fromJust #-} + +use_S_apply :: S (Int -> Int) -> Int +use_S_apply (S f) = f 1 +{-# NOINLINE use_S_apply #-} + +checkNotThunk :: String -> a -> IO () +checkNotThunk name x = do + c <- getClosureData x + case c of + ThunkClosure{} -> putStrLn ("FAIL: " ++ name ++ " is a thunk") >> exitFailure + APClosure{} -> putStrLn ("FAIL: " ++ name ++ " is an AP") >> exitFailure + _ -> pure () + +-- Pattern matching binds the field itself, so no selector thunk is involved. +checkField :: String -> S a -> IO () +checkField name (S x) = checkNotThunk name x +{-# NOINLINE checkField #-} + +main :: IO () +main = do + -- Check if the pointer in the strict field is a thunk. + checkField "con_top_caf" con_top_caf + checkField "con_top_fun" con_top_fun + checkField "con_top_bot" con_top_bot + checkField "con_top_con" con_top_con + case con_top_pat of MkP f -> checkNotThunk "con_top_pat" f + checkField "expr_caf" (expr_caf ()) + checkField "expr_fun" (expr_fun ()) + checkField "expr_bot" (expr_bot ()) + checkField "expr_con" (expr_con ()) + + -- Actually execute a case on the contents of the field. + print (use_S_head con_top_caf, use_S_head (expr_caf ())) + print (use_S_fromJust con_top_con, use_S_fromJust (expr_con ())) + print (use_S_apply con_top_fun, use_S_apply (expr_fun ())) + forM_ [con_top_bot, expr_bot ()] $ \s -> do + r <- try (evaluate (use_S_apply s)) + case r of + Left (ErrorCall msg) -> putStrLn ("OK: " ++ msg) + Right v -> putStrLn ("FAIL: got " ++ show v) >> exitFailure ===================================== testsuite/tests/simplStg/should_run/inferTags007.stdout ===================================== @@ -0,0 +1,5 @@ +(2,2) +(42,42) +(2,2) +OK: bot called +OK: bot called View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4422280758a803eebf97e8ffc62a9d8… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4422280758a803eebf97e8ffc62a9d8… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc][wip/T27828] Refactor fundeps again
by Simon Peyton Jones (＠simonpj) 26 Sep '26

26 Sep '26

Simon Peyton Jones pushed to branch wip/T27828 at Glasgow Haskell Compiler / GHC Commits: cac84324 by Simon Peyton Jones at 2026-09-26T12:27:34+01:00 Refactor fundeps again This MR fixes #27828; there was a bad scoping error in `trim_qtvs`. The main changes are * Refactor `trim_qtvs` completely to eliminate the bug. * Remove a redundant `apartnessCheck` from `mkTopOpenFamEqFDs`. * Lots of improvements to the Notes in FunDeps.hs I also did a couple of pure refactors: * I realised that we were carefully caching `cab_incomps` in each `CoAxBranch`, to make it more efficient to reduce a type family application, but we were not doing the same thing when computing relevance for functional dependencies; see Note [Relevance] in GHC.Tc.Solver.FunDeps. So I added `cab_overlaps`, which is now used in `noEarlierMatch`. * Use a proper data types, `AmIUnifying` and `OuterKindsFlag`, for two previously-Boolean arguments to `tc_unify_tys`. This is a pure refactor. - - - - - 15 changed files: - + changelog.d/T27828 - compiler/GHC/Builtin/WiredIn/Types/Box.hs - compiler/GHC/Core/Coercion/Axiom.hs - compiler/GHC/Core/FamInstEnv.hs - compiler/GHC/Core/Unify.hs - compiler/GHC/Iface/Decl.hs - compiler/GHC/Iface/Syntax.hs - compiler/GHC/IfaceToCore.hs - compiler/GHC/Tc/Instance/FunDeps.hs - compiler/GHC/Tc/Solver/FunDeps.hs - compiler/GHC/Tc/TyCl.hs - + testsuite/tests/indexed-types/should_compile/T27828.hs - + testsuite/tests/indexed-types/should_compile/T27828a.hs - + testsuite/tests/indexed-types/should_compile/T27828b.hs - testsuite/tests/indexed-types/should_compile/all.T Changes: ===================================== changelog.d/T27828 ===================================== @@ -0,0 +1,8 @@ +section: compiler +synopsis: Fix a "No skolem info" compiler crash +issues: #27828 +mrs: !16714 + +description: { + There was a bug in the implementation of functional dependencies for type families. +} ===================================== compiler/GHC/Builtin/WiredIn/Types/Box.hs ===================================== @@ -329,7 +329,8 @@ mkWiredInNewTyCon tc_name dc_name nt_co_uniq bndrs roles nt_fld_ty = , cab_roles = roles , cab_lhs = mkTyVarTys tvs , cab_rhs = nt_fld_ty - , cab_incomps = [] } + , cab_overlaps = [] + , cab_incomps = [] } -- | The wired-in @Box@ newtype: -- ===================================== compiler/GHC/Core/Coercion/Axiom.hs ===================================== @@ -18,7 +18,7 @@ module GHC.Core.Coercion.Axiom ( coAxiomSingleBranch, coAxBranchTyVars, coAxBranchCoVars, coAxBranchRoles, coAxBranchLHS, coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps, - placeHolderIncomps, + placeHolderIncomps, placeHolderOverlaps, Role(..), @@ -195,23 +195,44 @@ mapAccumBranches f (MkBranches arr) Note [Storing compatibility] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -During axiom application, we need to be aware of which branches are compatible -with which others. The full explanation is in Note [Compatibility] in -GHc.Core.FamInstEnv. (The code is placed there to avoid a dependency from -GHC.Core.Coercion.Axiom on the unification algorithm.) Although we could -theoretically compute compatibility on the fly, this is silly, so we store it -in a CoAxiom. +A `CoAxBranch` caches some useful information in `cab_incomps` and `cab_overlaps`: -Specifically, each branch refers to all other branches with which it is -incompatible. This list might well be empty, and it will always be for the -first branch of any axiom. +* `cab_overlaps`: when computing "relevance", in the function + `GHC.Tc.Solver.FunDeps.getRelevantBranches`, we need to know which ealier branches + can match this one -- see `noEarlierMatch`. -CoAxBranches that do not (yet) belong to a CoAxiom should have a panic thunk -stored in cab_incomps. The incompatibilities are properly a property of the -axiom as a whole, and they are computed only when the final axiom is built. + Again we could look at all earlier branches, but instead we cache in `cab_overlaps` + a list of all earlier branches that could overlap with this one. -During serialization, the list is converted into a list of the indices -of the branches. +* `cab_incomps`: during axiom application, we need to be aware of which branches are + /compatible/ with which others. The full explanation is in Note [Compatibility] in + GHC.Core.FamInstEnv. (The code is placed there to avoid a dependency from + GHC.Core.Coercion.Axiom on the unification algorithm.) + + Although we could readily compute compatibility on the fly, this is silly, so we + cache in `cab_incomps` a list of earlier branches that are /incompatible/ with + this one. (See Note [Compatibility] for a definition.) + + Always a sub-list of `cab_overlaps`. + +Both lists can be empty, and always be for the first branch of any axiom. + +Some extra points: + +(SC1) A `CoAxBranch` that does not (yet) belong to a CoAxiom is initialised with panic + thunks, `placeHolderOverlaps` or `placeHolderIncomps`, for the two fields; see `mkCoAxBranch`. + + Then, when a bunch of branches is grouped together in an axiom, we analyse the + branches as a whole and initialise the fields properly, using `computeAxiomIncomps`. + (For open type families, whose axioms have only one branch, we null out both lists + with `noAxiomIncomps`. + +(SC2) We don't need to serialise `cab_overlaps` and `cab_incomps` into an interface + file, because we recompute them in `computeAxiomIncomps`. However, annoyingly, + the pretty printer converts to IfaceSyn before printing, and we do want to show + `cab_incomps` (see Note [Displaying axiom incompatibilities]). So, tiresomely, + `IfaceAxBranch` has a `ifaxbIncomps` field, used only for printing. For historical + reasons this is actually serialised. Yuk. Note [CoAxioms are homogeneous] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -230,7 +251,9 @@ This is checked in FamInstEnv.mkCoAxBranch. -- If you edit this type, you may need to update the GHC formalism -- See Note [GHC Formalism] in GHC.Core.Lint data CoAxiom br - = CoAxiom -- Type equality axiom. + = -- `br` is Unbranched for each of the many axioms of an open type family + -- Branched for the single multi-branch axiom of a closed type family + CoAxiom -- Type equality axiom. { co_ax_unique :: Unique -- Unique identifier , co_ax_name :: Name -- Name for pretty-printing , co_ax_role :: Role -- Role of the axiom's equality @@ -268,8 +291,15 @@ data CoAxBranch , cab_rhs :: Type -- ^ Right-hand side of the equality -- See Note [CoAxioms are homogeneous] + + , cab_overlaps :: [CoAxBranch] + -- ^ The preceding branches whose LHSs are /unify with/ this one + -- Order is unimportant + -- See Note [Storing compatibility] + , cab_incomps :: [CoAxBranch] - -- ^ The previous incompatible branches + -- ^ The preceding branches that are /incompatible/ with this one + -- Order is unimportant -- See Note [Storing compatibility] } deriving Data.Data @@ -342,8 +372,9 @@ coAxBranchIncomps :: CoAxBranch -> [CoAxBranch] coAxBranchIncomps = cab_incomps -- See Note [Compatibility] in GHC.Core.FamInstEnv -placeHolderIncomps :: [CoAxBranch] -placeHolderIncomps = panic "placeHolderIncomps" +placeHolderIncomps, placeHolderOverlaps :: [CoAxBranch] +placeHolderIncomps = panic "placeHolderIncomps" +placeHolderOverlaps = panic "placeHolderOverlaps" {- Note [CoAxBranch type variables] ===================================== compiler/GHC/Core/FamInstEnv.hs ===================================== @@ -19,7 +19,7 @@ module GHC.Core.FamInstEnv ( FamInstMatch(..), lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon, - isDominatedBy, apartnessCheck, compatibleBranches, + isDominatedBy, apartnessCheck, noEarlierMatchCheck, compatibleBranches, -- Injectivity InjectivityCheckResult(..), @@ -487,20 +487,45 @@ in GHC.Core.Unify.) Note [Compatibility] ~~~~~~~~~~~~~~~~~~~~ -Two patterns are /compatible/ if either of the following conditions hold: -1) The patterns are apart. -2) The patterns unify with a substitution S, and their right hand sides -equal under that substitution. +Consider a closed type family with two equations (X1) and (X2) + type family F a where + F lhs1 = rhs1 -- (X1) + ... + F lhs2 = rhs2 -- (X2) + ... +Then equations (X1) and (X2) are /compatible/ if any target (F ty) that +matches both equations yields the very same right hand side. Example: + And True True = True + And a True = a +The target (And True True) matches both equations but they then both +produce the same reduct True. + +More precisely (X1) and (X2) are /compatible/ iff + If LHSs unify with a substitution S, then S(rhs1) = S(rhs2) + +Conversely, (X1) and (X2) are /incompatible/ if + Their LHSs unify with S, and S(rhs1) /= S(rhs2) For open type families, only compatible instances are allowed. For closed -type families, the story is slightly more complicated. Consider the following: +families, we use the Closed Family Matching Rule (see function `findBranch`): -type family F a where - F Int = Bool - F a = Int + When looking up a target (F ty) in a closed type family F, + find an equation (branch) such that: + * the LHS matches the target + * the target is apart from every previous /incompatible/ equation for F -g :: Show a => a -> F a -g x = length (show x) +We don't need to check the earlier equations that are compatible with the +matching equation, because they are either irrelevant (clause 1 of compatible) +or benign (clause 2 of compatible). + +Some examples: + + type family F a where + F Int = Bool + F a = Int + + g :: Show a => a -> F a + g x = length (show x) Should that type-check? No. We need to allow for the possibility that 'a' might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int @@ -516,12 +541,12 @@ potentially-overlapping group is closed. As another example, consider this: -type family G x where - G Int = Bool - G a = Double + type family G x where + G Int = Bool + G a = Double -type family H y --- no instances + type family H y + -- no instances Now, we want to simplify (G (H Char)). We can't, because (H Char) might later simplify to be Int. So, (G (H Char)) is stuck, for now. @@ -529,18 +554,13 @@ simplify to be Int. So, (G (H Char)) is stuck, for now. While everything above is quite sound, it isn't as expressive as we'd like. Consider this: -type family J a where - J Int = Int - J a = a + type family J a where + J Int = Int + J a = a Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if b is instantiated with Int, but the RHSs coincide there, so it's all OK. - -So, the rule is this: when looking up a branch in a closed type family, we -find a branch that matches the target, but then we make sure that the target -is apart from every previous *incompatible* branch. We don't check the -branches that are compatible with the matching branch, because they are either -irrelevant (clause 1 of compatible) or benign (clause 2 of compatible). +Hence the Closed Family Matching Rule. Note [Compatibility of eta-reduced axioms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -572,15 +592,32 @@ fails anyway. -- See Note [Compatibility] compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool -compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) - (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) +compatibleBranches b1 b2 + = case compareBranches b1 b2 of + BC_Apart -> True + BC_Compat -> True + BC_Incompat -> False + +data BranchCompatibility + = BC_Apart -- LHSs are apart + | BC_Compat -- LHSs unify with S, and S(rhs1)=S(rhs2) + | BC_Incompat -- LHSs unify with S, and S(rhs1)/=S(rhs2) + +compareBranches :: CoAxBranch -> CoAxBranch -> BranchCompatibility +compareBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) + (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) = case tcUnifyTysFG alwaysBindFam alwaysBindTv commonlhs1 commonlhs2 of -- Here we need the cab_tvs of the two branches to be disinct. -- See Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom. - SurelyApart -> True - MaybeApart {} -> False - Unifiable subst -> Type.substTyAddInScope subst rhs1 `eqType` + SurelyApart -> BC_Apart + Unifiable subst | Type.substTyAddInScope subst rhs1 `eqType` Type.substTyAddInScope subst rhs2 + -> BC_Compat + | otherwise + -> BC_Incompat + MaybeApart {} -> BC_Incompat + -- An occurs check yields MaybeApart; + -- see Note [Infinitary substitutions] in GHC.Core.Unify where (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2 -- See Note [Compatibility of eta-reduced axioms] @@ -603,8 +640,7 @@ injectiveBranches injectivity ax1@(CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) ax2@(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) -- See Note [Verifying injectivity annotation], case 1. - = case tcUnifyTysForInjectivity True [rhs1] [rhs2] of - -- True = two-way pre-unification + = case tcUnifyTysForInjectivity Unifying [rhs1] [rhs2] of Nothing -> InjectivityAccepted -- RHS are different, so equations are injective. -- This is case 1A from Note [Verifying injectivity annotation] @@ -629,10 +665,11 @@ injectiveBranches injectivity lhs1Subst = Type.substTys subst (getInjArgs lhs1) lhs2Subst = Type.substTys subst (getInjArgs lhs2) --- takes a CoAxiom with unknown branch incompatibilities and computes --- the compatibilities --- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch] +-- Takes a CoAxiom for a closed type family that has place-holder +-- `cab_incomps` and `cab_overlaps` fields, and computes those fields +-- properly from the list of branches. +-- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom computeAxiomIncomps branches = snd (mapAccumL go [] branches) where @@ -640,11 +677,23 @@ computeAxiomIncomps branches go prev_brs cur_br = (new_br : prev_brs, new_br) where - new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br } - - mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch] - mk_incomps prev_brs cur_br - = filter (not . compatibleBranches cur_br) prev_brs + (overlaps,incomps) = get_cab [] [] prev_brs + new_br = cur_br { cab_overlaps = overlaps, cab_incomps = incomps } + + get_cab :: [CoAxBranch] -> [CoAxBranch] -- Accumulators + -> [CoAxBranch] + -> ([CoAxBranch], [CoAxBranch]) + get_cab overlaps incomps [] = (overlaps,incomps) + get_cab overlaps incomps (br:brs) + = case compareBranches cur_br br of + BC_Apart -> get_cab overlaps incomps brs + BC_Compat -> get_cab (br:overlaps) incomps brs + BC_Incompat -> get_cab (br:overlaps) (br:incomps) brs + +noAxiomIncomps :: CoAxBranch -> CoAxBranch +-- Overwrite the placeholders for `cab_incomps` and `cab_overlaps` +-- with [], because unbranched axioms have no "preceding" equations +noAxiomIncomps branch = branch { cab_incomps = [], cab_overlaps = [] } {- ************************************************************************ @@ -715,14 +764,17 @@ mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars -> SrcSpan -> CoAxBranch mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc - = CoAxBranch { cab_tvs = tvs' - , cab_eta_tvs = eta_tvs' - , cab_cvs = cvs' - , cab_lhs = tidyTypes env lhs - , cab_roles = roles - , cab_rhs = tidyType env rhs - , cab_loc = loc - , cab_incomps = placeHolderIncomps } + = CoAxBranch { cab_tvs = tvs' + , cab_eta_tvs = eta_tvs' + , cab_cvs = cvs' + , cab_lhs = tidyTypes env lhs + , cab_roles = roles + , cab_rhs = tidyType env rhs + , cab_loc = loc + + -- See (SC1) in Note [Storing compatibility] + , cab_overlaps = placeHolderOverlaps + , cab_incomps = placeHolderIncomps } where (env1, tvs') = tidyVarBndrs init_tidy_env tvs (env2, eta_tvs') = tidyVarBndrs env1 eta_tvs @@ -736,14 +788,16 @@ mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc -- all of the following code is here to avoid mutual dependencies with -- Coercion -mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched -mkBranchedCoAxiom ax_name fam_tc branches +mkBranchedCoAxiom :: Role -> Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched +mkBranchedCoAxiom role ax_name fam_tc branches = CoAxiom { co_ax_unique = nameUnique ax_name , co_ax_name = ax_name , co_ax_tc = fam_tc - , co_ax_role = Nominal + , co_ax_role = role , co_ax_implicit = False , co_ax_branches = manyBranches (computeAxiomIncomps branches) } + -- computeAxiomIncomps: see (SC1) in + -- Note [Storing compatibility] mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched mkUnbranchedCoAxiom ax_name fam_tc branch @@ -752,7 +806,9 @@ mkUnbranchedCoAxiom ax_name fam_tc branch , co_ax_tc = fam_tc , co_ax_role = Nominal , co_ax_implicit = False - , co_ax_branches = unbranched (branch { cab_incomps = [] }) } + , co_ax_branches = unbranched (noAxiomIncomps branch) } + -- noAxiomIncomps: see (SC1) in + -- Note [Storing compatibility] mkSingleCoAxiom :: Role -> Name -> [TyVar] -> [TyVar] -> [CoVar] @@ -767,7 +823,9 @@ mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty , co_ax_tc = fam_tc , co_ax_role = role , co_ax_implicit = False - , co_ax_branches = unbranched (branch { cab_incomps = [] }) } + , co_ax_branches = unbranched (noAxiomIncomps branch) } + -- noAxiomIncomps: see (SC1) in + -- Note [Storing compatibility] where branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty (map (const Nominal) tvs) @@ -785,7 +843,9 @@ mkNewTypeCoAxiom name tycon tvs roles rhs_ty , co_ax_implicit = True -- See Note [Implicit axioms] in GHC.Core.TyCon , co_ax_role = Representational , co_ax_tc = tycon - , co_ax_branches = unbranched (branch { cab_incomps = [] }) } + , co_ax_branches = unbranched (noAxiomIncomps branch) } + -- noAxiomIncomps: see (SC1) in + -- Note [Storing compatibility] where branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty roles (getSrcSpan name) @@ -1223,7 +1283,9 @@ findBranch :: Array BranchIndex CoAxBranch -> Maybe (BranchIndex, [Type], [Coercion]) -- coercions relate requested types to returned axiom LHS at role N findBranch branches target_tys - = foldr go Nothing (assocs branches) + = -- Implements the Closed Family Matching Rule + -- in Note [Compatibility] + foldr go Nothing (assocs branches) where go :: (BranchIndex, CoAxBranch) -> Maybe (BranchIndex, [Type], [Coercion]) @@ -1258,6 +1320,20 @@ apartnessCheck target (CoAxBranch { cab_incomps = incomps }) isSurelyApart SurelyApart = True isSurelyApart _ = False +-- | Check whether an earlier branch matches these target types +noEarlierMatchCheck + :: [Type] + -> CoAxBranch -- ^ The candidate equation we wish to use + -> Bool -- ^ True <=> equation can fire +noEarlierMatchCheck target (CoAxBranch { cab_overlaps = overlaps }) + -- NB: this is the /only/ use of the `cab_overlaps` field + -- See Note [Storing compatibility] and + -- (RW4) in Note [Relevance] + = not (any matches overlaps) + where + matches earlier_branch + = isJust (tcMatchTys (coAxBranchLHS earlier_branch) target) + {- ************************************************************************ * * ===================================== compiler/GHC/Core/Unify.hs ===================================== @@ -9,6 +9,7 @@ module GHC.Core.Unify ( tcMatchTyX_BM, ruleMatchTyKiX, -- Side-effect free unification + AmIUnifying(..), tcUnifyTy, tcUnifyTys, tcUnifyFunDeps, tcUnifyDebugger, tcUnifyTysFG, tcUnifyTysForInjectivity, BindTvFun, BindFamFun, BindFlag(..), @@ -597,14 +598,14 @@ tcMatchTyX_BM :: HasDebugCallStack => BindTvFun -> Subst -> Type -> Type -> Maybe Subst tcMatchTyX_BM bind_tv subst ty1 ty2 - = tc_match_tys_x bind_tv False subst [ty1] [ty2] + = tc_match_tys_x bind_tv IgnoreOuterKinds subst [ty1] [ty2] -- | Like 'tcMatchTy', but allows the kinds of the types to differ, -- and thus matches them as well. -- See also Note [tcMatchTy vs tcMatchTyKi] tcMatchTyKi :: HasDebugCallStack => Type -> Type -> Maybe Subst tcMatchTyKi ty1 ty2 - = tc_match_tys alwaysBindTv True [ty1] [ty2] + = tc_match_tys alwaysBindTv CheckOuterKinds [ty1] [ty2] -- | This is similar to 'tcMatchTy', but extends a substitution -- See also Note [tcMatchTy vs tcMatchTyKi] @@ -614,7 +615,7 @@ tcMatchTyX :: HasDebugCallStack -> Type -- ^ Target -> Maybe Subst tcMatchTyX subst ty1 ty2 - = tc_match_tys_x alwaysBindTv False subst [ty1] [ty2] + = tc_match_tys_x alwaysBindTv IgnoreOuterKinds subst [ty1] [ty2] -- | Like 'tcMatchTy' but over a list of types. -- See also Note [tcMatchTy vs tcMatchTyKi] @@ -625,7 +626,7 @@ tcMatchTys :: HasDebugCallStack -- variables could be free in the target -- See (CU6) in Note [The Core unifier] tcMatchTys tys1 tys2 - = tc_match_tys alwaysBindTv False tys1 tys2 + = tc_match_tys alwaysBindTv IgnoreOuterKinds tys1 tys2 -- | Like 'tcMatchTyKi' but over a list of types. -- See also Note [tcMatchTy vs tcMatchTyKi] @@ -635,7 +636,7 @@ tcMatchTyKis :: HasDebugCallStack -> Maybe Subst -- ^ One-shot substitution -- See (CU6) in Note [The Core unifier] tcMatchTyKis tys1 tys2 - = tc_match_tys alwaysBindTv True tys1 tys2 + = tc_match_tys alwaysBindTv CheckOuterKinds tys1 tys2 -- | Like 'tcMatchTys', but extending a substitution -- See also Note [tcMatchTy vs tcMatchTyKi] @@ -645,7 +646,7 @@ tcMatchTysX :: HasDebugCallStack -> [Type] -- ^ Target -> Maybe Subst -- ^ One-shot substitution tcMatchTysX subst tys1 tys2 - = tc_match_tys_x alwaysBindTv False subst tys1 tys2 + = tc_match_tys_x alwaysBindTv IgnoreOuterKinds subst tys1 tys2 -- | Like 'tcMatchTyKis', but extending a substitution -- See also Note [tcMatchTy vs tcMatchTyKi] @@ -655,12 +656,12 @@ tcMatchTyKisX :: HasDebugCallStack -> [Type] -- ^ Target -> Maybe Subst -- ^ One-shot substitution tcMatchTyKisX subst tys1 tys2 - = tc_match_tys_x alwaysBindTv True subst tys1 tys2 + = tc_match_tys_x alwaysBindTv CheckOuterKinds subst tys1 tys2 -- | Same as tc_match_tys_x, but starts with an empty substitution tc_match_tys :: HasDebugCallStack => BindTvFun - -> Bool -- ^ match kinds? + -> OuterKindsFlag -- ^ Match kinds? -> [Type] -> [Type] -> Maybe Subst @@ -672,7 +673,7 @@ tc_match_tys bind_me match_kis tys1 tys2 -- | Worker for 'tcMatchTysX' and 'tcMatchTyKisX' tc_match_tys_x :: HasDebugCallStack => BindTvFun - -> Bool -- ^ match kinds? + -> OuterKindsFlag -- ^ Match kinds? -> Subst -> [Type] -> [Type] @@ -680,8 +681,8 @@ tc_match_tys_x :: HasDebugCallStack tc_match_tys_x bind_tv match_kis (Subst in_scope id_env tv_env cv_env) tys1 tys2 = case tc_unify_tys neverBindFam -- (ATF7) in Note [Apartness and type families] bind_tv - False -- Matching, not unifying - False -- Not an injectivity check + Matching -- Matching, not unifying + False -- Not an injectivity check match_kis RespectMultiplicities (mkRnEnv2 in_scope) tv_env cv_env tys1 tys2 of @@ -706,9 +707,9 @@ ruleMatchTyKiX tmpl_tvs rn_env tenv tmpl target -- But even if it did, (ATF8) in Note [Apartness and type families] -- says it doesn't matter becuase here we only care about Unifiable. -- So neverBindFam is efficient, and sufficient. - False -- Matching, not unifying + Matching -- Matching, not unifying False -- No doing an injectivity check - True -- Match the kinds + CheckOuterKinds -- Match the kinds IgnoreMultiplicities -- See Note [Rewrite rules ignore multiplicities in FunTy] rn_env tenv emptyCvSubstEnv [tmpl] [target] of @@ -784,7 +785,7 @@ tcUnifyTy t1 t2 = tcUnifyTys alwaysBindTv [t1] [t2] tcUnifyDebugger :: Type -> Type -> Maybe Subst tcUnifyDebugger t1 t2 = case tc_unify_tys_fg - True -- Unify kinds + CheckOuterKinds -- Unify kinds neverBindFam -- Does not affect Unifiable, so pick max efficient -- See (ATF8) in Note [Apartness and type families] alwaysBindTv @@ -798,7 +799,7 @@ tcUnifyFunDeps :: TyCoVarSet -> Maybe Subst tcUnifyFunDeps qtvs tys1 tys2 = case tc_unify_tys_fg - True -- Unify kinds + CheckOuterKinds -- Unify kinds dontCareBindFam -- Class-instance heads never mention type families (matchBindTv qtvs) tys1 tys2 of @@ -821,7 +822,7 @@ tcUnifyTysForInjectivity unif tys1 tys2 = case tc_unify_tys alwaysBindFam alwaysBindTv unif -- Am I unifying? True -- Do injectivity checks - False -- Don't check outermost kinds + IgnoreOuterKinds -- Don't check outermost kinds RespectMultiplicities rn_env emptyTvSubstEnv emptyCvSubstEnv tys1 tys2 of @@ -838,8 +839,9 @@ tcUnifyTysForInjectivity unif tys1 tys2 -- should never actually be done maybe_fix tv_subst - | unif = niFixSubst in_scope tv_subst - | otherwise = mkTvSubst in_scope tv_subst + = case unif of + Unifying -> niFixSubst in_scope tv_subst + Matching -> mkTvSubst in_scope tv_subst -- When matching, don't confuse domain with range; no fixpoint! ----------------- @@ -866,15 +868,15 @@ tcUnifyTysFG :: BindFamFun -> BindTvFun -> [Type] -> [Type] -> UnifyResult tcUnifyTysFG bind_fam bind_tv tys1 tys2 - = tc_unify_tys_fg False bind_fam bind_tv tys1 tys2 + = tc_unify_tys_fg IgnoreOuterKinds bind_fam bind_tv tys1 tys2 -tc_unify_tys_fg :: Bool +tc_unify_tys_fg :: OuterKindsFlag -> BindFamFun -> BindTvFun -> [Type] -> [Type] -> UnifyResult tc_unify_tys_fg match_kis bind_fam bind_tv tys1 tys2 = do { (tv_env, _) <- tc_unify_tys bind_fam bind_tv - True -- Unifying + Unifying False -- Not doing an injectivity check match_kis -- Match outer kinds RespectMultiplicities rn_env @@ -888,10 +890,10 @@ tc_unify_tys_fg match_kis bind_fam bind_tv tys1 tys2 -- | This function is actually the one to call the unifier -- a little -- too general for outside clients, though. tc_unify_tys :: BindFamFun -> BindTvFun - -> AmIUnifying -- ^ True <=> unify; False <=> match - -> Bool -- ^ True <=> doing an injectivity check - -> Bool -- ^ True <=> treat the kinds as well - -> MultiplicityFlag -- ^ see Note [Rewrite rules ignore multiplicities in FunTy] in GHC.Core.Unify + -> AmIUnifying -- ^ Unifying or matching + -> Bool -- ^ True <=> doing an injectivity check + -> OuterKindsFlag -- ^ Check outer kinds or not + -> MultiplicityFlag -- ^ see Note [Rewrite rules ignore multiplicities in FunTy] in GHC.Core.Unify -> RnEnv2 -> TvSubstEnv -- ^ substitution to extend -> CvSubstEnv @@ -910,8 +912,9 @@ tc_unify_tys :: BindFamFun -> BindTvFun -- See also Note [tcMatchTy vs tcMatchTyKi]. tc_unify_tys bind_fam bind_tv unif inj_check match_kis match_mults rn_env tv_env cv_env tys1 tys2 = initUM tv_env cv_env $ - do { when match_kis $ - unify_tys env kis1 kis2 + do { case match_kis of + CheckOuterKinds -> unify_tys env kis1 kis2 + IgnoreOuterKinds -> return () ; unify_tys env tys1 tys2 } where env = UMEnv { um_bind_tv_fun = bind_tv @@ -926,6 +929,11 @@ tc_unify_tys bind_fam bind_tv unif inj_check match_kis match_mults rn_env tv_env kis2 = map typeKind tys2 +data OuterKindsFlag + = CheckOuterKinds -- Unify or match the /kind/ of the two types + | IgnoreOuterKinds -- Just unify of match the types, ignoring kinds + -- (typically, we already know they are equal) + {- ********************************************************************* * * UnifyResult, MaybeApart etc @@ -1583,8 +1591,7 @@ c.f. Note [Comparing type synonyms] in GHC.Core.TyCo.Compare -------------- unify_ty: the main workhorse ----------- -type AmIUnifying = Bool -- True <=> Unifying - -- False <=> Matching +data AmIUnifying = Matching | Unifying type InType = Type -- Before applying the RnEnv2 type OutCoercion = Coercion -- After applying the RnEnv2 @@ -1618,7 +1625,7 @@ unify_ty env (CastTy ty1 co1) ty2 kco -- See (KCU1) in Note [Kind coercions in Unify] = maybeApart MARCast -- See (KCU2) - | um_unif env + | Unifying <- um_unif env = unify_ty env ty1 ty2 (co1 `mkTransCo` kco) | otherwise -- We are matching, not unifying @@ -1661,7 +1668,7 @@ unify_ty env (CoercionTy co1) (CoercionTy co2) kco = do { c_subst <- getCvSubstEnv ; case co1 of CoVarCo cv - | not (um_unif env) + | Matching <- um_unif env , not (cv `elemVarEnv` c_subst) -- Not forall-bound , let (_mult_co, co_l, co_r) = decomposeFunCo kco -- Because the coercion is used in a type, it should be safe to @@ -1682,7 +1689,7 @@ unify_ty env (TyVarTy tv1) ty2 kco = uVarOrFam env (TyVarLHS tv1) ty2 kco unify_ty env ty1 (TyVarTy tv2) kco - | um_unif env -- If unifying, can swap args; but not when matching + | Unifying <- um_unif env -- If unifying, can swap args; but not when matching = uVarOrFam (umSwapRn env) (TyVarLHS tv2) ty1 (mkSymCo kco) -- Deal with TyConApps @@ -1692,7 +1699,7 @@ unify_ty env ty1 ty2 kco | Just (tc,tys) <- mb_sat_fam_app1 = uVarOrFam env (TyFamLHS tc tys) ty2 kco - | um_unif env + | Unifying <- um_unif env , Just (tc,tys) <- mb_sat_fam_app2 = uVarOrFam (umSwapRn env) (TyFamLHS tc tys) ty1 (mkSymCo kco) @@ -1820,7 +1827,7 @@ uVarOrFam env ty1 ty2 kco go swapped substs lhs@(TyVarLHS tv1) ty2 kco | Just ty1' <- lookupVarEnv (um_tv_env substs) tv1' = -- We already have a substitution for tv1 - if | um_unif env -> unify_ty env ty1' ty2 kco + if | Unifying <- um_unif env -> unify_ty env ty1' ty2 kco | (ty1' `mkCastTy` kco) `tcEqType` ty2 -> return () | otherwise -> surelyApart -- Unifying: recurse into unify_ty @@ -1842,9 +1849,9 @@ uVarOrFam env ty1 ty2 kco | TyVarTy tv2 <- ty2 , let tv2' = umRnOccR env tv2 , tv1' == tv2' - = if | um_unif env -> return () - | tv1_is_bindable -> extendTvEnv tv1' ty2 - | otherwise -> return () + = if | Unifying <- um_unif env -> return () + | tv1_is_bindable -> extendTvEnv tv1' ty2 + | otherwise -> return () | tv1_is_bindable , not (mentionsForAllBoundTyVarsR env ty2_fvs) @@ -1858,9 +1865,9 @@ uVarOrFam env ty1 ty2 kco -- e.g. a ~ F p q with `a` not bindable: we might succeed with go_fam -- e.g. a ~ beta with `a` not bindable: we might be able to bind `beta` -- e.g. beta ~ F beta Int occurs check; but MaybeApart after swapping - | um_unif env + | Unifying <- um_unif env , NotSwapped <- swapped -- If we have swapped already, don't do so again - , Just lhs2 <- canEqLHS_maybe ty2 + , Just lhs2 <- canEqLHS_maybe ty2 = go IsSwapped substs lhs2 (mkTyVarTy tv1) (mkSymCo kco) | occurs_check = maybeApart MARInfinite -- Occurs check @@ -1879,7 +1886,9 @@ uVarOrFam env ty1 ty2 kco | otherwise = False - occurs_check = um_unif env && uOccursCheck substs foralld_tvs lhs rhs + occurs_check = case um_unif env of + Unifying -> uOccursCheck substs foralld_tvs lhs rhs + Matching -> False -- Occurs check, only when unifying -- see Note [Infinitary substitutions] -- Make sure you include `kco` in rhs #14846 @@ -1893,7 +1902,7 @@ uVarOrFam env ty1 ty2 kco -- Hence the RnEnv2 is empty | not under_forall , Just ty1' <- lookupFamEnv (um_fam_env substs) tc1 tys1 - = if | um_unif env -> unify_ty env ty1' ty2 kco + = if | Unifying <- um_unif env -> unify_ty env ty1' ty2 kco -- Below here we are matching -- The return () case deals with: -- Template: (F a)..(F a) @@ -1930,9 +1939,9 @@ uVarOrFam env ty1 ty2 kco -- NB: a type family can appear on the template when matching -- see (ATF6) in Note [Apartness and type families] -- (Only worth doing this if we are not under a forall.) - | um_unif env + | Unifying <- um_unif env , NotSwapped <- swapped - , Just lhs2 <- canEqLHS_maybe ty2 + , Just lhs2 <- canEqLHS_maybe ty2 = go IsSwapped substs lhs2 (mkTyConApp tc1 tys1) (mkSymCo kco) | otherwise -- See (ATF5) in Note [Apartness and type families] @@ -1962,9 +1971,9 @@ uVarOrFam env ty1 ty2 kco (inj_tys2, noninj_tys2) = partitionByList inj tys2 bind_fam_if_poss - | not (um_unif env) -- Not when matching (ATF11-1) + | Matching <- um_unif env -- Not when matching (ATF11-1) = return () - | under_forall -- Not under a forall (ATF3) + | under_forall -- Not under a forall (ATF3) = return () | BindMe <- um_bind_fam_fun env tc tys1 rhs1 = unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys1) rhs1) $ ===================================== compiler/GHC/Iface/Decl.hs ===================================== @@ -112,7 +112,7 @@ coAxBranchToIfaceBranch tc lhs_s , ifaxbRoles = roles , ifaxbRHS = toIfaceType rhs , ifaxbIncomps = iface_incomps } - where + where iface_incomps = map (expectJust . flip findIndex lhs_s . eqTypes ===================================== compiler/GHC/Iface/Syntax.hs ===================================== @@ -338,7 +338,12 @@ data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars :: [IfaceTvBndr] , ifaxbRoles :: [Role] , ifaxbRHS :: IfaceType , ifaxbIncomps :: [BranchIndex] } - -- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom + -- We store the incompatibilities in IfaceAxBranch + -- just for (perhaps unnecessary) display purposes: + -- see Note [Displaying axiom incompatibilities] + -- When we construct a real CoAxBranch we compute cab_incomps directly + -- from the equations, ignoring the ifaxbIncomps. + -- We could consider getting rid of ifaxbIncomps altogether. data IfaceConDecls = IfAbstractTyCon -- c.f TyCon.AbstractTyCon @@ -779,14 +784,13 @@ that is what is seen by importing module with --make Note [Displaying axiom incompatibilities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -With -fprint-axiom-incomps we display which closed type family equations -are incompatible with which. This information is sometimes necessary -because GHC doesn't try equations in order: any equation can be used when -all preceding equations that are incompatible with it do not apply. - -For example, the last "a && a = a" equation in Data.Type.Bool.&& is -actually compatible with all previous equations, and can reduce at any -time. +With -fprint-axiom-incomps we display which closed type family equations are +incompatible with which (see #15546). This information is sometimes necessary +because GHC doesn't try equations in order: any equation can be used when all +preceding equations that are incompatible with it do not apply. + +For example, the last "a && a = a" equation in Data.Type.Bool.&& is actually +compatible with all previous equations, and can reduce at any time. This is displayed as: Prelude> :i Data.Type.Equality.== ===================================== compiler/GHC/IfaceToCore.hs ===================================== @@ -91,7 +91,6 @@ import GHC.Utils.Logger import GHC.Data.Bag import GHC.Data.Maybe import GHC.Data.FastString -import GHC.Data.List.SetOps import GHC.Types.Annotations import GHC.Types.SourceFile @@ -903,12 +902,7 @@ tc_iface_decl _ _ (IfaceAxiom { ifName = tc_name, ifTyCon = tc -- See #13803 ; tc_branches <- forkM (text "Axiom branches" <+> ppr tc_name) $ tc_ax_branches branches - ; let axiom = CoAxiom { co_ax_unique = nameUnique tc_name - , co_ax_name = tc_name - , co_ax_tc = tc_tycon - , co_ax_role = role - , co_ax_branches = manyBranches tc_branches - , co_ax_implicit = False } + ; let axiom = mkBranchedCoAxiom role tc_name tc_tycon tc_branches ; return (ACoAxiom axiom) } tc_iface_decl _ _ (IfacePatSyn{ ifName = name @@ -1116,15 +1110,14 @@ tc_fd (tvs1, tvs2) = do { tvs1' <- mapM tcIfaceTyVar tvs1 ; return (tvs1', tvs2') } tc_ax_branches :: [IfaceAxBranch] -> IfL [CoAxBranch] -tc_ax_branches if_branches = foldlM tc_ax_branch [] if_branches +tc_ax_branches if_branches = mapM tc_ax_branch if_branches -tc_ax_branch :: [CoAxBranch] -> IfaceAxBranch -> IfL [CoAxBranch] -tc_ax_branch prev_branches - (IfaceAxBranch { ifaxbTyVars = tv_bndrs +tc_ax_branch :: IfaceAxBranch -> IfL CoAxBranch +tc_ax_branch (IfaceAxBranch { ifaxbTyVars = tv_bndrs , ifaxbEtaTyVars = eta_tv_bndrs , ifaxbCoVars = cv_bndrs , ifaxbLHS = lhs, ifaxbRHS = rhs - , ifaxbRoles = roles, ifaxbIncomps = incomps }) + , ifaxbRoles = roles }) = bindIfaceTyConBinders_AT (map (\b -> Bndr (IfaceTvBndr b) (NamedTCB Inferred)) tv_bndrs) $ \ tvs -> -- The _AT variant is needed here; see Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom @@ -1135,15 +1128,15 @@ tc_ax_branch prev_branches ; this_mod <- getIfModule ; let loc = mkGeneralSrcSpan (fsLit "module " `appendFS` moduleNameFS (moduleName this_mod)) - br = CoAxBranch { cab_loc = loc - , cab_tvs = binderVars tvs - , cab_eta_tvs = eta_tvs - , cab_cvs = cvs - , cab_lhs = tc_lhs - , cab_roles = roles - , cab_rhs = tc_rhs - , cab_incomps = map (prev_branches `getNth`) incomps } - ; return (prev_branches ++ [br]) } + ; return (CoAxBranch { cab_loc = loc + , cab_tvs = binderVars tvs + , cab_eta_tvs = eta_tvs + , cab_cvs = cvs + , cab_lhs = tc_lhs + , cab_roles = roles + , cab_rhs = tc_rhs + , cab_overlaps = placeHolderOverlaps + , cab_incomps = placeHolderIncomps }) } tcIfaceDataCons :: Name -> TyCon -> IfaceConDecls -> IfL AlgTyConRhs tcIfaceDataCons tycon_name tycon if_cons ===================================== compiler/GHC/Tc/Instance/FunDeps.hs ===================================== @@ -136,10 +136,10 @@ data FunDepEqns -- Plural becuase fd_eqs has multiple equations -- to fresh unification vars, -- See (IMP2) in Note [Improving against instances] - , fd_eqs :: [TypeEqn] -- Make these pairs of types equal - -- Invariant: In each (Pair ty1 ty2), the fd_qtvs may be - -- free in ty1 but not in ty2. See Wrinkle (1) of - -- Note [Improving against instances] + , fd_eqs :: [TypeEqn] -- Make these pairs of types equal + -- Invariant: In each (Pair ty1 ty2), the fd_qtvs may be + -- free in ty1 but not in ty2. See Wrinkle (1) of + -- Note [Improving against instances] } instance Outputable FunDepEqns where ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -26,20 +26,23 @@ import GHC.Core.Coercion import GHC.Core.TyCo.Rep( Type(..) ) import GHC.Core.Predicate( EqRel(..) ) import GHC.Core.TyCon -import GHC.Core.Unify( tcUnifyTysForInjectivity, typeListsAreApart ) +import GHC.Core.Unify( AmIUnifying(..) + , tcUnifyTysForInjectivity, typeListsAreApart ) import GHC.Core.Coercion.Axiom import GHC.Core.TyCo.Subst( elemSubst ) import GHC.Builtin.WiredIn.TypeLits( tryInteractTopFam, tryInteractInertFam ) +import GHC.Types.Var( TyVar, tyVarKind, setTyVarKind ) import GHC.Types.Var.Set +import GHC.Types.Var.Env( mkInScopeSet ) import GHC.Utils.Outputable import GHC.Utils.Panic import Control.Monad( unless ) import GHC.Data.Pair -import Data.Maybe( isNothing, isJust, mapMaybe ) +import Data.Maybe( isJust, mapMaybe ) {- Note [Overview of functional dependencies in type inference] @@ -109,7 +112,6 @@ Wrinkles from fundeps, but that would require new evidence forms, and an extension to FC, so we don't do that right now (Dec 14). - Note [FunDep and implicit parameter reactions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Currently, our story of interacting two dictionaries (or a dictionary @@ -573,6 +575,7 @@ tryEqFunDeps work_item@(EqCt { eq_lhs = work_lhs tryFamEqFunDeps :: TcSMode -> [EqCt] -> TyCon -> [TcType] -> EqCt -> SolverStage () +-- See Note [Type inference for type families with injectivity] tryFamEqFunDeps mode eqs_for_me fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs = work_rhs }) | Just ops <- builtInClosedTyFamTyCon_maybe fam_tc @@ -583,6 +586,7 @@ tryFamEqFunDeps mode eqs_for_me fam_tc work_args ; tryFDEqns False fam_tc work_args work_item eqns ; unless (hasRelevantGiven eqs_for_me work_args work_item) $ + -- hasRelevantGiven: See (CF1) in Note [Exploiting closed type families] do { eqns <- mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs ; tryFDEqns True fam_tc work_args work_item eqns } } @@ -599,8 +603,11 @@ tryFamEqFunDeps mode eqs_for_me fam_tc work_args NotInjective -> nopStage () Injective inj -> do { eqns <- mkLocalFamEqFDs eqs_for_me fam_tc inj work_args work_rhs ; tryFDEqns False fam_tc work_args work_item eqns } + -- NB: tryFDEqns bales out on an insoluble fundep + -- See (CF4) in Note [Exploiting closed type families] ; unless (hasRelevantGiven eqs_for_me work_args work_item) $ + -- hasRelevantGiven: See (CF1) in Note [Exploiting closed type families] do { eqns <- mkTopFamEqFDs fam_tc work_args work_item ; tryFDEqns True fam_tc work_args work_item eqns } } @@ -638,10 +645,11 @@ tryFDEqns is_top fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) f -- User-defined type families ----------------------------------------- mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> EqCt -> SolverStage [FunDepEqns] +-- Implements (INJFAM:Wanted/top-closed) +-- See Note [Exploiting closed type families] -- Look at the top-level axioms; we effectively infer injectivity, --- so we don't need tyConInjectivtyInfo. This works fine for closed +-- so we don't need tyConInjectivityInfo. This works fine for closed -- type families without injectivity info --- See Note [Exploiting closed type families] mkTopClosedFamEqFDs ax work_args (EqCt { eq_ev = ev, eq_rhs = work_rhs }) | isGenerativeType work_rhs -- See (CF5) in Note [Exploiting closed type families] = Stage $ @@ -679,39 +687,46 @@ hasRelevantGiven eqs_for_me work_args (EqCt { eq_rhs = work_rhs }) relevant (EqCt { eq_ev = ev, eq_lhs = lhs, eq_rhs = rhs_ty }) | isGiven ev , TyFamLHS _ lhs_tys <- lhs - = isJust (tcUnifyTysForInjectivity True work_tys (rhs_ty:lhs_tys)) + = isJust (tcUnifyTysForInjectivity Unifying work_tys (rhs_ty:lhs_tys)) | otherwise = False getRelevantBranches :: CoAxiom Branched -> [TcType] -> Xi -> [FunDepEqns] -- Return the FunDepEqns that arise from each relevant branch +-- Implements Note [Relevance] getRelevantBranches ax work_args work_rhs - = go [] (fromBranches (coAxiomBranches ax)) + = go (fromBranches (coAxiomBranches ax)) where work_tys = work_rhs : work_args - go _ [] = [] - go preceding (branch:branches) + go [] = [] + go (branch:branches) = case is_relevant branch of - Just eqn -> eqn : go (branch:preceding) branches - Nothing -> go (branch:preceding) branches + Just eqn -> eqn : go branches + Nothing -> go branches where - is_relevant (CoAxBranch { cab_tvs = qtvs, cab_lhs = lhs_tys, cab_rhs = rhs_ty }) - | Just subst <- tcUnifyTysForInjectivity True (rhs_ty:lhs_tys) work_tys - , let (subst', qtvs') = trim_qtvs subst qtvs - lhs_tys' = substTys subst' lhs_tys - rhs_ty' = substTy subst' rhs_ty - , all (no_match lhs_tys') preceding + is_relevant branch@(CoAxBranch { cab_tvs = qtvs + , cab_lhs = lhs_tys + , cab_rhs = rhs_ty }) + | Just subst <- tcUnifyTysForInjectivity Unifying (rhs_ty:lhs_tys) work_tys + -- See (RW1)-(RW3) in Note [Relevance] + -- This is a pre-/unification/ check (not matching) + -- so `subst` can bind both `qtvs` and fvs(work_tys) + , let (subst',qtvs') = trim_qtvs subst qtvs + lhs_tys' = substTys subst' lhs_tys + rhs_ty' = substTy subst' rhs_ty + branch_tys' = rhs_ty' : lhs_tys' + , noEarlierMatchCheck lhs_tys' branch -- See (RW4) in Note [Relevance] = Just (FDEqns { fd_qtvs = qtvs' - , fd_eqs = zipWith Pair (rhs_ty':lhs_tys') work_tys }) + , fd_eqs = zipWith Pair branch_tys' work_tys }) + -- Do not apply the substition to `work_tys`; + -- See (CF7) in Note [Exploiting closed type families] | otherwise = Nothing - no_match lhs_tys (CoAxBranch { cab_lhs = lhs_tys1 }) - = isNothing (tcUnifyTysForInjectivity False lhs_tys1 lhs_tys) - mkTopOpenFamEqFDs :: TyCon -> [Bool] -> [TcType] -> EqCt -> TcS [FunDepEqns] --- Implements (INJFAM:Wanted/top) +-- Implements (INJFAM:Wanted/top-open) +-- See Note [Exploiting open type families] mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs }) = do { fam_envs <- getFamInstEnvs ; let branches :: [CoAxBranch] @@ -720,15 +735,15 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs }) ; return (mapMaybe do_one branches) } where do_one :: CoAxBranch -> Maybe FunDepEqns - do_one branch@(CoAxBranch { cab_tvs = branch_tvs - , cab_lhs = branch_lhs_tys - , cab_rhs = branch_rhs }) - | Just subst <- tcUnifyTysForInjectivity False [branch_rhs] [work_rhs] - -- False: matching, not unifying - , let (subst', qtvs) = trim_qtvs subst branch_tvs + do_one (CoAxBranch { cab_tvs = branch_qtvs + , cab_lhs = branch_lhs_tys + , cab_rhs = branch_rhs }) + | Just subst <- tcUnifyTysForInjectivity Matching [branch_rhs] [work_rhs] + , let (subst', qtvs') = trim_qtvs subst branch_qtvs branch_lhs_tys' = substTys subst' branch_lhs_tys - , apartnessCheck branch_lhs_tys' branch -- See (TIF3) - = Just (mkInjectivityFDEqn inj_flags qtvs branch_lhs_tys' work_args) + -- No need for an apartness check here; for open type families + -- there are no "preceding" equations + = Just (mkInjectivityFDEqn inj_flags qtvs' branch_lhs_tys' work_args) | otherwise = Nothing @@ -736,7 +751,7 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs }) mkLocalFamEqFDs :: [EqCt] -> TyCon -> [Bool] -> [TcType] -> Xi -> SolverStage [FunDepEqns] -- Wanted constraints only -- Both open and closed type families, but only ones with declared injectivity --- See Note [Type inference for type families with injectivity] esp (TIF2) +-- See Note [Exploiting local type-family injectivity] mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs = do { let -- eqns_from_inerts: see (INJFAM:Wanted/other) eqns_from_inerts = mapMaybe do_one eqs_for_me @@ -755,15 +770,23 @@ mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs mk_eqn iargs = mkInjectivityFDEqn inj_flags [] work_args iargs -trim_qtvs :: Subst -> [TcTyVar] -> (Subst,[TcTyVar]) --- Tricky stuff: see (TIF1) in --- Note [Type inference for type families with injectivity] -trim_qtvs subst [] = (subst, []) -trim_qtvs subst (tv:tvs) - | tv `elemSubst` subst = trim_qtvs subst tvs - | otherwise = let !(subst1, tv') = substTyVarBndr subst tv - !(subst', tvs') = trim_qtvs subst1 tvs - in (subst', tv':tvs') +trim_qtvs :: Subst -> [TyVar] -> (Subst, [TyVar]) +-- Tricky stuff: see (OF1) in Note [Exploiting open type families] +-- The returned substitution is identical to the incoming one, except that +-- its in-scope set is extended with the returned [TyVar] +trim_qtvs unif_subst qtvs + = go unif_subst qtvs + where + go :: Subst -> [TyVar] -> (Subst, [TyVar]) + go subst [] = (subst, []) + go subst (tv:tvs) + | tv `elemSubst` unif_subst = go subst tvs + | otherwise = (subst'', tv':tvs') + where + tv' = tv `setTyVarKind` substTy subst (tyVarKind tv) + subst' = subst `extendSubstInScope` tv' + !(subst'', tvs') = go subst' tvs + ----------------------------------------- -- Built-in type families @@ -924,15 +947,20 @@ we attempt to exploit injectivity, via `mkLocalFamEqFDs`: * (INJFAM:Wanted/other) see `mkLocalFamEqFDs` work item: [W] F s1 s2 ~ rhs -- Wanted inert: [G/W] F t2 t2 ~ rhs -- Same `rhs`, Given or Wanted - We can generate FunDepEqns: (s2 ~ t2) + See Note [Exploiting local type-family injectivity] + +* (INJFAM:Wanted/top-open) for open type families: `mkTopOpenFamEqFDs` + type family F a b = r | r -> b + type instance F Int (Maybe a) = [G Int] -- G is a type family + [W] F alpha beta = [ty] + We can generate (Maybe gamma ~ beta) + See Note [Exploiting open type families] -* (INJFAM:Wanted/top) see `mkTopUserFamEqFDs` - work item: [W] F s1 s2 ~ rhs - type instance forall a b c. F t1 t2 ~ top_rhs - and we can /match/ the LHS, so that - S(top_rhs) = rhs - then we can generate the FunDepEqns: forall a c. s2 ~ S(t2) - But see wrinkle (TIF1), (TIF3) +* (INJFAM:Wanted/top-closed) for closed type families: `mkTopClosedFamEqFDs` + type family F a b where { ...eqns... } + [W] F alpha ~ Int + We may be able to generate some extra equalities to constraint `alpha` + See very clever Note [Exploiting closed type families] For /built-in/ type families, it's pretty similar, except that @@ -945,45 +973,36 @@ For /built-in/ type families, it's pretty similar, except that * mkLocalBuiltinFamEqFDs * mkTopBuiltinFamEqFDs -(TIF1) Generating fundeps from a top-level type instance is covered in - Section 5.2 in the Injective Type Families paper. It's a bit tricky. - Consider - type family F @k (a::k) (b::k) = r | r -> k b - type instance forall k (a::k) (b::k). F @k (Proxy @k a) (Proxy @k b) = Proxy @k a - [W] F @kappa alpha beta ~ Maybe (Proxy @kappa (delta::kappa)) +Note [Exploiting local type-family injectivity] see `mkLocalFamEqFDs` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have a type family with declared injectivity: + type family F a b = r | r -> b +and we have + work item: [W] F s1 s2 ~ F t1 t2 +or + work item: [W] F s1 s2 ~ rhs -- Wanted + inert: [G/W] F t2 t2 ~ rhs -- Same `rhs`, Given or Wanted - we match (Proxy @kappa delta) against the template (Proxy k a), succeeding - with substitution [k:->kappa, a:->delta]. We want to generate this FunDepEqns - FDEqn { fd_qtvs = [b:kappa], fd_eqs = [ beta ~ Proxy @kappa b ] } - Notice that - * we must quantify the FunDepEqns over `b`, which is not matched; for this - we will generate a fresh unification variable in `instantiateFunDepEqn`. - * we must substitute `k:->kappa` in the kind of `b`. - This fancy footwork for `fd_qtvs` is done by `trim_qtvs` in - `mkInjWantedFamEqTopEqns`. +Then we can generate FunDepEqns: (s2 ~ t2) + +This applies equally to /closed/ type families; it is /not/ subsumed +by Note [Exploiting closed type families]. Consider: -(TIF2) All this applies equally to /closed/ type families; it is /not/ - subsumed by Note [Exploiting closed type families]. Consider: type family F a | r -> a where { .... } [W] F t1 ~ a [W] F t2 ~ a - Then since F is declared injective, we can generate t1~t2. +Then since F is declared injective, we can generate t1~t2. - As for open type families, we insist on /user-declared/ injectivity only; we - don't try to /infer/ injectivity even for a closed family. See Section 3.4 - of the "Injective type families" paper. (Arguably, we could /infer/ - injectivity for closed type families, and that would be more in the spirit of - Note [Exploiting closed type families].) +As for open type families, we insist on /user-declared/ injectivity only; we +don't try to /infer/ injectivity even for a closed family. See Section 3.4 +of the "Injective type families" paper. (Arguably, we could /infer/ +injectivity for closed type families, and that would be more in the spirit of +Note [Exploiting closed type families].) -(TIF3) Further to (TIF1), if we are considering a /closed/ type family, we - must ensure (see Section 5.2 of the paper) that after matching that - equation would indeed be the one to fire. So we call `apartnessCheck` - on the branch to ensure this, in `mkTopUserFamEqFDs`. - -Definition [Relevance] -~~~~~~~~~~~~~~~~~~~~~~ +Note [Relevance] +~~~~~~~~~~~~~~~~ We say that a closed-type-family equation `F lhs = rhs` is /relevant/ for a Wanted [W] F wlhs ~ wrhs iff @@ -992,6 +1011,10 @@ iff (R2) There is no earlier equation that matches S(lhs). See (RW4) below. +The relevance check is implemented by `getRelevantBranches`, which acutally +returns the [FunDepEqns] described in the Closed Family Fundep Algorithm in +Note [Exploiting closed type families]. + (RW1) Pre-unification treats type-family applications as binding to anything, rather like type variables. If two types don't even pre-unify, we say that they are /apart/. It is done by `tcUnifyTysForInjectivity`. @@ -1014,24 +1037,99 @@ iff Clearly the RHS is apart from the first equation and we want to fire injectivity on the second equation. -(RW4) Why "no earlier equation matches" in conditoin (R2)? Consider the family +(RW4) Why "no earlier equation matches" in condition (R2)? Consider the family type family Bak a = r where Bak Int = Char -- B1 Bak Char = Int -- B2 Bak a = a -- B3 - and [W] Bak alpha ~ Char. In fact, only (B2) is relevant for this Wanted. + and [W] Bak alpha ~ Char. In fact, only (B1) is relevant for this Wanted. You might think that (B3) could be instantiated to Bak Char ~ Char; but actually that instantiation will never fire because (B2) Bak Char ~ Int would - fire first. So the only way to return a Char is if the argment is Int; so we - can emit [W] alpha ~ Int. Hence (B3) is not relevant; only (B2) is relevant. + fire first. So the only way to return a Char is via (B1); so we + can emit [W] alpha ~ Int. Hence (B3) is not relevant; only (B1) is relevant. That is the reason for condition (R2) in the definition of Relevance above. A watertight proof that this is the Right Thing is not very easy. See more - discussion in #23162. + discussion in #23162, and Section 5.2 of the paper. + + How, precisely, do we implement (R2)? We check that there is no earlier equation + that fires on S(lhs), in this case (on Bak Char). Notice that this is different + from the `apartnessCheck`, which checks that all preceding equations are apart + from S(lhs). Apartness checking uses /unification/; here we want /matching/. + Hence using `noEarlierMatchCheck`, not `apartnessCheck`. + + Here's a good example from T27171_aux. T + type family TMessage m where + {- T1 -} TMessage @f @t (CustomMethod s :: Method f t) = () + {- T2 -} TMessage @f @Req (m :: Method f Req) = TRequestMessage m + {- T3 -} TMessage @f @Not (m :: Method f Not) = TNotificationMessage m + + [W] TMessage @SC @Req alpha ~# TRequestMessage alpha + + There is only one relevant equation, namely (T2). If we apply its + pre-unification substitution [f :-> SC, m :-> alpha] to its LHS we get + TMessage @SC @Req alpha + and equation (T1) does not match that. (It does unify, but we don't care.) + +(RW5) `noEarlierMatchCheck`: in (RW4) We really do need to check that /no/ + earlier equation matches, not just no earlier /incompatible/ equation + matches. Consider T27282a: + type family F a where + F Int = Int -- B1 + F Char = Bool -- B2 + F a = a -- B3 + + [W] F alpha ~ Int + + (B1) is relevant, and (B2) is not. What about (B3)? It pre-unifies with + the Wanted via [alpha :-> Int, a :-> Int]. But under that substitution + (B1) would fire, so (B3) is not relevant. + + And yet, (B1) is /compatible/ with (B3), so it's no good just looking at + the `cab_incomps` of (B3). Instead we look at `cab_overlaps`. + +Note [Exploiting open type families] see `mkTopOpenFamEqFDs` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Generating fundeps from a top-level type instance is covered in Section 5.2 in +the Injective Type Families paper. For open type families, suppose we have + + type family F a b = r | r -> b + type instance F Int (Maybe a) = [G Int] -- G is a type family + + [W] F alpha beta = [ty] + +Then, since F has been checked as injective, and the RHS [G Int] +pre-unifies with [ty], we can add a derived FunDepEqns + FDEqns{ fd_qtvs = a, fd_eqs = [ Maybe a ~ beta ] } +and thereby emit + [W] Maybe gamma ~ beta -- Fresh gamma + +Wrinkles + +(OF1) Consider + type family F @k (a::k) (b::k) = r | r -> k b + type instance forall k (a::k) (b::k). + F @k (Proxy @k a) (Proxy @k b) = Maybe (Proxy @k a) -Note [Exploiting closed type families] + [W] F @kappa alpha beta ~ Maybe (Proxy @kappa (delta::kappa)) + + We match the target (Maybe (Proxy @kappa delta)) + against the template (Maybe (Proxy @k a)) + succeeding with substitution [k:->kappa, a:->delta]. We want to generate this: + FDEqn { fd_qtvs = [b::kappa], fd_eqs = [ Proxy @kappa b ] ~ beta } + Notice that + * we must quantify the FunDepEqns over `b`, which is not matched; for this + we will generate a fresh unification variable in `instantiateFunDepEqn`. + * we must substitute `k:->kappa` in the kind of `b`. + + This fancy footwork for `fd_qtvs` is done by `trim_qtvs`. It + * Drops a quantified tyvar that /is/ matched + * Substitutes in the kind of a quantified tyvar that is /not/ matched + * Adds the not-matched tyvar to the in-scope set of the substitution + +Note [Exploiting closed type families] see `mkTopClosedFamEqFDs` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have type family F a b where @@ -1042,17 +1140,18 @@ Suppose we have [W] F Int alpha ~ Char The /only/ way to solve this Wanted is using (F2), so we can safely unify -alpha:=Char without risking losing any solutions. That is what -`mkTopClosedFamEqFDs` does. Ticket #23162 has lots of background detail +alpha:=Char without risking losing any solutions. We don't even need any +injectivity annotations. Ticket #23162 has lots of background detail. -More precisely, here is the Closed Family Fundep Algorithm (CFFA) +More precisely, here is the very clever Closed Family Fundep Algorithm (CFFA) IF * F a is a closed type family. * We are trying to solve [W] F wlhs ~ wrhs. - * There are no "relevant" Givens [G] F lhs ~ rhs. See (CF1) below. - * F has exactly one equation, F lhs = rhs that is "relevant" for that Wanted + * There are no "relevant Givens" [G] F lhs ~ rhs. See (CF1) below. + * F has exactly one equation, F lhs = rhs that is "relevant" for + that Wanted (see Note [Relevance]) THEN - we can emit and solve the fundep equalities: + we can emit and solve the fundeps :: [FunDepEqns]: [W] wlhs1 ~ lhs1 ... [W] wlhsn ~ lhsn @@ -1060,7 +1159,10 @@ More precisely, here is the Closed Family Fundep Algorithm (CFFA) with fresh unification vars in lhs and rhs for the quantified variables of the equation. -See Definition [Relevance] for what "relevant" means. + Actually we take advantage of the substitution generated by the relevance + check, see (CF7) below. + +See Note [Relevance] for what "relevant" means. We need to take care about non-termination; see (CF3). Key point: equations that are not relevant do not need to be considered for fundeps at all. @@ -1166,6 +1268,8 @@ Key point: equations that are not relevant do not need to be considered for fund I was looking at non-termination for closed type families, but it's a small improvement in general. + This bale-out is implementedn in `tryFDEqns`. + (CF5) Consider (see "Yikes5" in #23162): type family F a where F (Just x) = Int @@ -1196,7 +1300,7 @@ Key point: equations that are not relevant do not need to be considered for fund type family I t = res | res -> t where I TInt = Int |> g -- where g :: Type ~# IK k and [W] I alpha ~ Int |> g2 - Here we definiteily want to take advantage of injectivity. + Here we definitely want to take advantage of injectivity. (CF6) This machinery can also have a significant positive effect on the size of proof terms. For example (simplification of T26426): @@ -1204,7 +1308,8 @@ Key point: equations that are not relevant do not need to be considered for fund type family (++) a b where { '[] ++ ys = ys; (x:xs) ++ ys = x : (xs ++ ys) } type family MapId a where { MapId '[] = '[]; MapId (x:xs) = x : MapId xs } - app :: (MapId xs ++ MapId ys ~ MapId (xs ++ ys)) => Proxy xs -> Proxy ys -> Proxy (xs ++ ys) + app :: (MapId xs ++ MapId ys ~ MapId (xs ++ ys)) + => Proxy xs -> Proxy ys -> Proxy (xs ++ ys) test :: Proxy [ty_1, ..., ty_n] test = Proxy @'[ty_1] @@ -1248,6 +1353,30 @@ Key point: equations that are not relevant do not need to be considered for fund instead of relying on recursively built sub-proof terms, which brings down coercion sizes (in certain situations) from O(n^3) to O(n^2). +(CF7) Relevance. When computing relevance in the Closed Family Fundep Algorithm, + for [W] F wlhs1 wlhs2 ~ wrhs, against an equation F lhs1 lhs2 ~ rhs + we get back a pre-unifying substitution S that makes the two as equal as poss. + Then we use `trim_qtvs` in exactly the same way as in + (OF1) of Note [Exploiting closed type families], to generate qtvs' and S' + Then we generate + FDEqns { fd_qtvs = qtvs', fd_eqs [ S'(lhs1) ~ wlhs1 + , S'(lhs2) ~ wlhs2 + , S'(rhs) ~ wrhs ] } + Notice that we do /not/ apply S' to wlhs/wrhs. These type contain unification + variables that we must actually unify! Example + type familiy F a b where + F [a] (Maybe b) = (a, G b) + [W] F alpha beta ~ (Int, [gamma]) + Pre-unification gives [alpha :-> [a], beta :-> Maybe b, a :-> Int] + This substitution eliminates the quantified variable `a` but not `b`, so we + want this: + FDEqns { fd_qtvs = [b], fd_eqs [ [Int] ~ alpha + , Maybe b ~ beta + , (Int,G b) ~ (Int, [gamma]) ] } + + Notice also that by applying the substitution to the template but not to the + Wanted, we uphold the `fd_eqs` invariant in `FDEqns` (see its data type decl) + Note [Cache-caused loops] ~~~~~~~~~~~~~~~~~~~~~~~~~ It is very dangerous to cache a rewritten wanted family equation as 'solved' in @@ -1340,28 +1469,34 @@ solveFunDeps work_ev fd_eqns ; uPairsTcM uenv eqs } instantiateFunDepEqns :: FunDepEqns -> TcM [TypeEqn] -instantiateFunDepEqns (FDEqns { fd_qtvs = tvs, fd_eqs = eqs }) - | null tvs +-- See GHC.Tc.Instance.Fundeps Note [Improving against instances] +-- Wrinkle (IMP1) +instantiateFunDepEqns (FDEqns { fd_qtvs = qtvs, fd_eqs = eqs }) + | null qtvs = return rev_eqs | otherwise - = do { TcM.traceTc "instantiateFunDepEqns" (ppr tvs $$ ppr eqs) - ; (_, subst) <- instFlexiXTcM emptySubst tvs -- Takes account of kind substitution + = do { TcM.traceTc "instantiateFunDepEqns" (ppr qtvs $$ ppr eqs) + ; (_, subst) <- instFlexiXTcM empty_subst qtvs -- Takes account of kind substitution ; return (map (subst_pair subst) rev_eqs) } where rev_eqs = reverse eqs -- (reverse eqs): See Note [Reverse order of fundep equations] + -- The kinds of `qtvs` can have free variables, because of `trim_qtvs` + -- Example: T27828b + empty_subst = mkEmptySubst $ mkInScopeSet $ + tyCoVarsOfTypes (map tyVarKind qtvs) + subst_pair subst (Pair ty1 ty2) - = Pair (substTyUnchecked subst' ty1) ty2 - -- ty2 does not mention fd_qtvs, so no need to subst it. - -- See GHC.Tc.Instance.Fundeps Note [Improving against instances] - -- Wrinkle (1) + = Pair (substTy subst' ty1) ty2 + -- NB: ty2 does not mention fd_qtvs, so no need to subst it. + -- See invariant on `fv_eqs` in `data FunDepEqns`. where subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1) -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result -- of matching with the [W] constraint. So we add its free -- vars to InScopeSet, to satisfy substTy's invariants, even - -- though ty1 will never (currently) be a poytype, so this + -- though ty1 will never (currently) be a polytype, so this -- InScopeSet will never be looked at. ===================================== compiler/GHC/Tc/TyCl.hs ===================================== @@ -3462,7 +3462,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info ; let mb_co_ax | null eqns = Nothing -- mkBranchedCoAxiom fails on empty list - | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches) + | otherwise = Just (mkBranchedCoAxiom Nominal co_ax_name fam_tc branches) fam_tc = mkFamilyTyCon tc_name kind tc_bndrs 0 res_kind (resultVariableName sig) (ClosedTypeFamilyTyCon $ CTF mb_co_ax) parent inj' ===================================== testsuite/tests/indexed-types/should_compile/T27828.hs ===================================== @@ -0,0 +1,50 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeAbstractions #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +module Bug where + +import Data.Functor.Identity (Identity(..)) +import Data.Kind (Type) +import Data.Proxy (Proxy(..)) +import Data.Type.Equality ((:~:)(..)) + +type TyFun :: Type -> Type -> Type +data TyFun a b + +type (~>) :: Type -> Type -> Type +type a ~> b = TyFun a b -> Type +infixr 0 ~> + +type Apply :: (k1 ~> k2) -> k1 -> k2 +type family Apply f x + +type Rep1 :: (k -> Type) -> k -> Type +type family Rep1 f + +type To1 :: Rep1 f a -> f a +type family To1 z + +type Par1 :: Type -> Type +newtype Par1 p = Par1 p + +type To1Sym0 :: forall k (f :: k -> Type) (a :: k). Rep1 f a ~> f a +data To1Sym0 z + +applyTo1Sym0 :: forall k (f :: k -> Type) (a :: k) (x :: Rep1 f a). Proxy x -> Apply @(Rep1 f a) @(f a) To1Sym0 x :~: To1 x +applyTo1Sym0 _ = undefined + +type IdentitySym0 :: a ~> Identity a +data IdentitySym0 z +type instance Apply IdentitySym0 x = 'Identity x + +type Aux :: Rep1 Identity a -> Rep1 Identity a -> Identity a +type family Aux x y where + Aux x ('Par1 wombat) = Apply IdentitySym0 wombat + +type instance Rep1 Identity = Par1 +type instance To1 @Identity y = Aux y y + +lemma :: forall a (z :: a). Apply @(Rep1 Identity a) @(Identity a) To1Sym0 ('Par1 z) :~: 'Identity z +lemma = applyTo1Sym0 @Type @Identity @a (Proxy @('Par1 z)) +-- lemma = applyTo1Sym0 @Type @Identity @a @('Par1 z) (Proxy @('Par1 z)) ===================================== testsuite/tests/indexed-types/should_compile/T27828a.hs ===================================== @@ -0,0 +1,16 @@ +{-# LANGUAGE TypeFamilies #-} + +module T27828a where + +import Data.Proxy + +type family F a where + F Int = Int -- B1 + F Char = Bool -- B2 + F a = a -- B3 + +h :: (F a ~ Int) => Proxy a -> () +h = error "urk" + +k :: () +k = h Proxy -- [W] F alpha ~ Int ===================================== testsuite/tests/indexed-types/should_compile/T27828b.hs ===================================== @@ -0,0 +1,12 @@ +{-# LANGUAGE TypeFamilies, KindSignatures, AllowAmbiguousTypes #-} + +module T27878b where + +type family IsJust (m :: Maybe k) :: Bool where + IsJust ('Just x) = 'True + IsJust 'Nothing = 'False + +f :: forall k (m :: Maybe k). (IsJust m ~ 'True) => Int -> Int +f = error "urk" + +g _ = f 3 -- Triggered checkValidSubst error in `instantiateFunDepEqns`o ===================================== testsuite/tests/indexed-types/should_compile/all.T ===================================== @@ -316,3 +316,6 @@ test('T25611b', normal, compile, ['']) test('T25611c', normal, compile, ['']) test('T25611d', normal, compile, ['']) test('T25657', normal, compile, ['']) +test('T27828', normal, compile, ['']) +test('T27828a', normal, compile, ['']) +test('T27828b', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/cac84324f535b94e941767f4250fb79… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/cac84324f535b94e941767f4250fb79… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc][wip/rafl/hpc-instances] 12 commits: Improve the `mhu-closure` makefile
by Florian Ragwitz (＠rafl) 26 Sep '26

26 Sep '26

Florian Ragwitz pushed to branch wip/rafl/hpc-instances at Glasgow Haskell Compiler / GHC Commits: 1abef1ef by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Improve the `mhu-closure` makefile - - - - - a79a68ea by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Make `ghci-multi` hide all unneeded packages - - - - - d6e72450 by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Improve the definition of the home unit closure property - - - - - c9a2766d by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Re-implement the home unit closure check Compared to the previous implementation, the new one has the following advantages: * It is correct. - It distinguishes between units that have the same unit ID but different ABI hashes. - When `-hide-all-packages` is not used, it considers as home unit dependencies also units that are made implicitly available because they are in the package database. * It seems to be faster in usual settings. - In particular, it does not have a preparation phase in which it merges the dependency information from all home units, so that its running time does not grow linearly with the size of the package database in normal Cabal scenarios. * It is (hopefully) clearer. * It is better documented. - - - - - fa96acf8 by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Remove erroneous GHC flag in `hadrian-multi` The flag was `-Werror=-Wno-error=incomplete-record-selectors`. Its purpose was to permit incomplete record selectors, but because of the illegal combination of `-Werror=` and `-Wno-error` it was ignored, without any negative consequences. - - - - - 9f48a5b9 by Alan Zimmerman at 2026-09-25T17:02:50-04:00 EPA: Add specific layout field to AnnList Up to now AnnList has effectively served to represent lists of things having layout, regardless of whether they do or not. In Haskell, layout is optional in many places, as there is also an alternative syntax using braces and semi-colons, which is free-form. This commit introduces AnnListLayout, a data structure capturing this distinction. It is deliberately set up similarly to EpLayout, so that these two can be merged in time. The transition is done mechanically, where AnnListBraces is not used yet, the original Nothing case maps to AnnListNoLayout, and the Just case to AnnListLayout. Later commits will fine tune these against the actual parser layout. - - - - - 295cbdc5 by Florian Ragwitz at 2026-09-26T00:33:37-07:00 hpc: Test desired HPC behaviour for class instances - - - - - e3fa5413 by Florian Ragwitz at 2026-09-26T00:33:37-07:00 Extend TcGblEnv with a mapping from instance method Ids to DFunIds We want to use this in HPC to provide better support for instance methods. This is working towards #17155. - - - - - 7997961b by Florian Ragwitz at 2026-09-26T00:33:37-07:00 hpc: Do not create top-level boxes for generated instance methods Users care about which of their written methods are or aren't covered, not whether all of the inherited methods are covered as well. Those should be covered where they are implemented. We achieve that by stopping to generate top-level boxes which will often appear as uncovered with no clear indication as to why, and no way to fix other than excercising code the user has not written. Fixes #17155, #15932. - - - - - db535f0a by Florian Ragwitz at 2026-09-26T00:33:37-07:00 hpc: Provide coverage information for class instances After fixing #17155, we no longer create top-level boxes for the source spans of instance heads (previously that was the source span used for inherited/generated instance methods). With those boxes gone, we can introduce a new top-level box for each class instance with that instance head source span, and provide more meaningful coverage semantics for it. We make the use of any of the instance's methods (user-written or generated) tick this box, providing the programmer with useful information about whether or not the instance was exercised at run-time, and whether the instance might be unnecessary. - - - - - 9ed32dca by Florian Ragwitz at 2026-09-26T00:33:38-07:00 hpc: Don't allocate boxes for methodless classes With the plumbing we currently have, these could never be covered, which is not helpful to hpc users. This could be improved upon further. - - - - - 638439a1 by Florian Ragwitz at 2026-09-26T00:33:38-07:00 Add a changelog entry for new HPC features - - - - - 38 changed files: - .gitlab-ci.yml - + changelog.d/hpc-classinsts - compiler/GHC/Driver/Downsweep.hs - compiler/GHC/Driver/Errors/Ppr.hs - compiler/GHC/Driver/Errors/Types.hs - compiler/GHC/HsToCore.hs - compiler/GHC/HsToCore/Ticks.hs - compiler/GHC/Parser.y - compiler/GHC/Parser/Annotation.hs - compiler/GHC/Parser/PostProcess.hs - compiler/GHC/Tc/Module.hs - compiler/GHC/Tc/TyCl/Instance.hs - compiler/GHC/Tc/Types.hs - compiler/GHC/Tc/Utils/Monad.hs - compiler/GHC/Unit/Env.hs - hadrian/ghci-multi-cabal.in - testsuite/tests/driver/multipleHomeUnits/mhu-closure/Makefile - testsuite/tests/driver/multipleHomeUnits/mhu-closure/mhu-closure.stderr - testsuite/tests/driver/multipleHomeUnits/mhu-closure/mhu-closure.stdout - testsuite/tests/ghc-api/exactprint/T22919.stderr - testsuite/tests/ghc-api/exactprint/ZeroWidthSemi.stderr - + testsuite/tests/hpc/instmeths/instmeths.hs - + testsuite/tests/hpc/instmeths/instmeths.stdout - + testsuite/tests/hpc/instmeths/test.T - testsuite/tests/module/mod185.stderr - testsuite/tests/parser/should_compile/DumpParsedAst.stderr - testsuite/tests/parser/should_compile/DumpParsedAstComments.stderr - testsuite/tests/parser/should_compile/DumpRenamedAst.stderr - testsuite/tests/parser/should_compile/DumpSemis.stderr - testsuite/tests/parser/should_compile/KindSigs.stderr - testsuite/tests/parser/should_compile/T15279.stderr - testsuite/tests/parser/should_compile/T20718.stderr - testsuite/tests/parser/should_compile/T20846.stderr - testsuite/tests/printer/Test20297.stdout - testsuite/tests/printer/Test24533.stdout - utils/check-exact/ExactPrint.hs - utils/check-exact/Main.hs - utils/check-exact/Transform.hs The diff was not included because it is too large. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f6d6ed5b454aa4a8fa4ce58447e296… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f6d6ed5b454aa4a8fa4ce58447e296… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc][wip/T27828] 3 commits: Correct the documentation of `explicitUnits`
by Simon Peyton Jones (＠simonpj) 26 Sep '26

26 Sep '26

Simon Peyton Jones pushed to branch wip/T27828 at Glasgow Haskell Compiler / GHC Commits: 53eead15 by Wolfgang Jeltsch at 2026-09-24T20:12:03-04:00 Correct the documentation of `explicitUnits` Resolves #27787. - - - - - 35bf6f4b by Simon Jakobi at 2026-09-24T20:12:49-04:00 Remove stale specHeader bullet from Note [Don't make fillers for constraint types] The Note said that Specialise.specHeader also calls mkAbsentFiller. abfc224a27c removed that call: the specialiser no longer drops dead arguments at all, see Note [Do not drop dead args from specialisations] in GHC.Core.Opt.Specialise. Assisted-by: Claude Fable 5.1 - - - - - b130101d by Simon Peyton Jones at 2026-09-25T22:59:21+01:00 Refactor fundeps again This MR fixes #27828; there was a bad scoping error in `trim_qtvs`. The main changes are * Refactor `trim_qtvs` completely to eliminate the bug. * Remove a redundant `apartnessCheck` from `mkTopOpenFamEqFDs`. * Lots of improvements to the Notes in FunDeps.hs I also did a couple of pure refactors: * I realised that we were carefully caching `cab_incomps` in each `CoAxBranch`, to make it more efficient to reduce a type family application, but we were not doing the same thing when computing relevance for functional dependencies; see Note [Relevance] in GHC.Tc.Solver.FunDeps. So I added `cab_overlaps`, which is now used in `noEarlierMatch`. * Use a proper data types, `AmIUnifying` and `OuterKindsFlag`, for two previously-Boolean arguments to `tc_unify_tys`. This is a pure refactor. - - - - - 16 changed files: - + changelog.d/T27828 - compiler/GHC/Builtin/WiredIn/Types/Box.hs - compiler/GHC/Core/Coercion/Axiom.hs - compiler/GHC/Core/FamInstEnv.hs - compiler/GHC/Core/Opt/WorkWrap/Utils.hs - compiler/GHC/Core/Unify.hs - compiler/GHC/Iface/Decl.hs - compiler/GHC/Iface/Syntax.hs - compiler/GHC/IfaceToCore.hs - compiler/GHC/Tc/Instance/FunDeps.hs - compiler/GHC/Tc/Solver/FunDeps.hs - compiler/GHC/Tc/TyCl.hs - compiler/GHC/Unit/State.hs - + testsuite/tests/indexed-types/should_compile/T27828.hs - + testsuite/tests/indexed-types/should_compile/T27828a.hs - testsuite/tests/indexed-types/should_compile/all.T Changes: ===================================== changelog.d/T27828 ===================================== @@ -0,0 +1,8 @@ +section: compiler +synopsis: Fix a "No skolem info" compiler crash +issues: #27828 +mrs: !16714 + +description: { + There was a bug in the implementation of functional dependencies for type families. +} ===================================== compiler/GHC/Builtin/WiredIn/Types/Box.hs ===================================== @@ -329,7 +329,8 @@ mkWiredInNewTyCon tc_name dc_name nt_co_uniq bndrs roles nt_fld_ty = , cab_roles = roles , cab_lhs = mkTyVarTys tvs , cab_rhs = nt_fld_ty - , cab_incomps = [] } + , cab_overlaps = [] + , cab_incomps = [] } -- | The wired-in @Box@ newtype: -- ===================================== compiler/GHC/Core/Coercion/Axiom.hs ===================================== @@ -18,7 +18,7 @@ module GHC.Core.Coercion.Axiom ( coAxiomSingleBranch, coAxBranchTyVars, coAxBranchCoVars, coAxBranchRoles, coAxBranchLHS, coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps, - placeHolderIncomps, + placeHolderIncomps, placeHolderOverlaps, Role(..), @@ -195,23 +195,44 @@ mapAccumBranches f (MkBranches arr) Note [Storing compatibility] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -During axiom application, we need to be aware of which branches are compatible -with which others. The full explanation is in Note [Compatibility] in -GHc.Core.FamInstEnv. (The code is placed there to avoid a dependency from -GHC.Core.Coercion.Axiom on the unification algorithm.) Although we could -theoretically compute compatibility on the fly, this is silly, so we store it -in a CoAxiom. +A `CoAxBranch` caches some useful information in `cab_incomps` and `cab_overlaps`: -Specifically, each branch refers to all other branches with which it is -incompatible. This list might well be empty, and it will always be for the -first branch of any axiom. +* `cab_overlaps`: when computing "relevance", in the function + `GHC.Tc.Solver.FunDeps.getRelevantBranches`, we need to know which ealier branches + can match this one -- see `noEarlierMatch`. -CoAxBranches that do not (yet) belong to a CoAxiom should have a panic thunk -stored in cab_incomps. The incompatibilities are properly a property of the -axiom as a whole, and they are computed only when the final axiom is built. + Again we could look at all earlier branches, but instead we cache in `cab_overlaps` + a list of all earlier branches that could overlap with this one. -During serialization, the list is converted into a list of the indices -of the branches. +* `cab_incomps`: during axiom application, we need to be aware of which branches are + /compatible/ with which others. The full explanation is in Note [Compatibility] in + GHC.Core.FamInstEnv. (The code is placed there to avoid a dependency from + GHC.Core.Coercion.Axiom on the unification algorithm.) + + Although we could readily compute compatibility on the fly, this is silly, so we + cache in `cab_incomps` a list of earlier branches that are /incompatible/ with + this one. (See Note [Compatibility] for a definition.) + + Always a sub-list of `cab_overlaps`. + +Both lists can be empty, and always be for the first branch of any axiom. + +Some extra points: + +(SC1) A `CoAxBranch` that does not (yet) belong to a CoAxiom is initialised with panic + thunks, `placeHolderOverlaps` or `placeHolderIncomps`, for the two fields; see `mkCoAxBranch`. + + Then, when a bunch of branches is grouped together in an axiom, we analyse the + branches as a whole and initialise the fields properly, using `computeAxiomIncomps`. + (For open type families, whose axioms have only one branch, we null out both lists + with `noAxiomIncomps`. + +(SC2) We don't need to serialise `cab_overlaps` and `cab_incomps` into an interface + file, because we recompute them in `computeAxiomIncomps`. However, annoyingly, + the pretty printer converts to IfaceSyn before printing, and we do want to show + `cab_incomps` (see Note [Displaying axiom incompatibilities]). So, tiresomely, + `IfaceAxBranch` has a `ifaxbIncomps` field, used only for printing. For historical + reasons this is actually serialised. Yuk. Note [CoAxioms are homogeneous] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -230,7 +251,9 @@ This is checked in FamInstEnv.mkCoAxBranch. -- If you edit this type, you may need to update the GHC formalism -- See Note [GHC Formalism] in GHC.Core.Lint data CoAxiom br - = CoAxiom -- Type equality axiom. + = -- `br` is Unbranched for each of the many axioms of an open type family + -- Branched for the single multi-branch axiom of a closed type family + CoAxiom -- Type equality axiom. { co_ax_unique :: Unique -- Unique identifier , co_ax_name :: Name -- Name for pretty-printing , co_ax_role :: Role -- Role of the axiom's equality @@ -268,8 +291,15 @@ data CoAxBranch , cab_rhs :: Type -- ^ Right-hand side of the equality -- See Note [CoAxioms are homogeneous] + + , cab_overlaps :: [CoAxBranch] + -- ^ The preceding branches whose LHSs are /unify with/ this one + -- Order is unimportant + -- See Note [Storing compatibility] + , cab_incomps :: [CoAxBranch] - -- ^ The previous incompatible branches + -- ^ The preceding branches that are /incompatible/ with this one + -- Order is unimportant -- See Note [Storing compatibility] } deriving Data.Data @@ -342,8 +372,9 @@ coAxBranchIncomps :: CoAxBranch -> [CoAxBranch] coAxBranchIncomps = cab_incomps -- See Note [Compatibility] in GHC.Core.FamInstEnv -placeHolderIncomps :: [CoAxBranch] -placeHolderIncomps = panic "placeHolderIncomps" +placeHolderIncomps, placeHolderOverlaps :: [CoAxBranch] +placeHolderIncomps = panic "placeHolderIncomps" +placeHolderOverlaps = panic "placeHolderOverlaps" {- Note [CoAxBranch type variables] ===================================== compiler/GHC/Core/FamInstEnv.hs ===================================== @@ -19,7 +19,7 @@ module GHC.Core.FamInstEnv ( FamInstMatch(..), lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon, - isDominatedBy, apartnessCheck, compatibleBranches, + isDominatedBy, apartnessCheck, noEarlierMatchCheck, compatibleBranches, -- Injectivity InjectivityCheckResult(..), @@ -487,20 +487,45 @@ in GHC.Core.Unify.) Note [Compatibility] ~~~~~~~~~~~~~~~~~~~~ -Two patterns are /compatible/ if either of the following conditions hold: -1) The patterns are apart. -2) The patterns unify with a substitution S, and their right hand sides -equal under that substitution. +Consider a closed type family with two equations (X1) and (X2) + type family F a where + F lhs1 = rhs1 -- (X1) + ... + F lhs2 = rhs2 -- (X2) + ... +Then equations (X1) and (X2) are /compatible/ if any target (F ty) that +matches both equations yields the very same right hand side. Example: + And True True = True + And a True = a +The target (And True True) matches both equations but they then both +produce the same reduct True. + +More precisely (X1) and (X2) are /compatible/ iff + If LHSs unify with a substitution S, then S(rhs1) = S(rhs2) + +Conversely, (X1) and (X2) are /incompatible/ if + Their LHSs unify with S, and S(rhs1) /= S(rhs2) For open type families, only compatible instances are allowed. For closed -type families, the story is slightly more complicated. Consider the following: +families, we use the Closed Family Matching Rule (see function `findBranch`): -type family F a where - F Int = Bool - F a = Int + When looking up a target (F ty) in a closed type family F, + find an equation (branch) such that: + * the LHS matches the target + * the target is apart from every previous /incompatible/ equation for F -g :: Show a => a -> F a -g x = length (show x) +We don't need to check the earlier equations that are compatible with the +matching equation, because they are either irrelevant (clause 1 of compatible) +or benign (clause 2 of compatible). + +Some examples: + + type family F a where + F Int = Bool + F a = Int + + g :: Show a => a -> F a + g x = length (show x) Should that type-check? No. We need to allow for the possibility that 'a' might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int @@ -516,12 +541,12 @@ potentially-overlapping group is closed. As another example, consider this: -type family G x where - G Int = Bool - G a = Double + type family G x where + G Int = Bool + G a = Double -type family H y --- no instances + type family H y + -- no instances Now, we want to simplify (G (H Char)). We can't, because (H Char) might later simplify to be Int. So, (G (H Char)) is stuck, for now. @@ -529,18 +554,13 @@ simplify to be Int. So, (G (H Char)) is stuck, for now. While everything above is quite sound, it isn't as expressive as we'd like. Consider this: -type family J a where - J Int = Int - J a = a + type family J a where + J Int = Int + J a = a Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if b is instantiated with Int, but the RHSs coincide there, so it's all OK. - -So, the rule is this: when looking up a branch in a closed type family, we -find a branch that matches the target, but then we make sure that the target -is apart from every previous *incompatible* branch. We don't check the -branches that are compatible with the matching branch, because they are either -irrelevant (clause 1 of compatible) or benign (clause 2 of compatible). +Hence the Closed Family Matching Rule. Note [Compatibility of eta-reduced axioms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -572,15 +592,32 @@ fails anyway. -- See Note [Compatibility] compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool -compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) - (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) +compatibleBranches b1 b2 + = case compareBranches b1 b2 of + BC_Apart -> True + BC_Compat -> True + BC_Incompat -> False + +data BranchCompatibility + = BC_Apart -- LHSs are apart + | BC_Compat -- LHSs unify with S, and S(rhs1)=S(rhs2) + | BC_Incompat -- LHSs unify with S, and S(rhs1)/=S(rhs2) + +compareBranches :: CoAxBranch -> CoAxBranch -> BranchCompatibility +compareBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) + (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) = case tcUnifyTysFG alwaysBindFam alwaysBindTv commonlhs1 commonlhs2 of -- Here we need the cab_tvs of the two branches to be disinct. -- See Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom. - SurelyApart -> True - MaybeApart {} -> False - Unifiable subst -> Type.substTyAddInScope subst rhs1 `eqType` + SurelyApart -> BC_Apart + Unifiable subst | Type.substTyAddInScope subst rhs1 `eqType` Type.substTyAddInScope subst rhs2 + -> BC_Compat + | otherwise + -> BC_Incompat + MaybeApart {} -> BC_Incompat + -- An occurs check yields MaybeApart; + -- see Note [Infinitary substitutions] in GHC.Core.Unify where (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2 -- See Note [Compatibility of eta-reduced axioms] @@ -603,8 +640,7 @@ injectiveBranches injectivity ax1@(CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) ax2@(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) -- See Note [Verifying injectivity annotation], case 1. - = case tcUnifyTysForInjectivity True [rhs1] [rhs2] of - -- True = two-way pre-unification + = case tcUnifyTysForInjectivity Unifying [rhs1] [rhs2] of Nothing -> InjectivityAccepted -- RHS are different, so equations are injective. -- This is case 1A from Note [Verifying injectivity annotation] @@ -629,10 +665,11 @@ injectiveBranches injectivity lhs1Subst = Type.substTys subst (getInjArgs lhs1) lhs2Subst = Type.substTys subst (getInjArgs lhs2) --- takes a CoAxiom with unknown branch incompatibilities and computes --- the compatibilities --- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch] +-- Takes a CoAxiom for a closed type family that has place-holder +-- `cab_incomps` and `cab_overlaps` fields, and computes those fields +-- properly from the list of branches. +-- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom computeAxiomIncomps branches = snd (mapAccumL go [] branches) where @@ -640,11 +677,23 @@ computeAxiomIncomps branches go prev_brs cur_br = (new_br : prev_brs, new_br) where - new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br } - - mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch] - mk_incomps prev_brs cur_br - = filter (not . compatibleBranches cur_br) prev_brs + (overlaps,incomps) = get_cab [] [] prev_brs + new_br = cur_br { cab_overlaps = overlaps, cab_incomps = incomps } + + get_cab :: [CoAxBranch] -> [CoAxBranch] -- Accumulators + -> [CoAxBranch] + -> ([CoAxBranch], [CoAxBranch]) + get_cab overlaps incomps [] = (overlaps,incomps) + get_cab overlaps incomps (br:brs) + = case compareBranches cur_br br of + BC_Apart -> get_cab overlaps incomps brs + BC_Compat -> get_cab (br:overlaps) incomps brs + BC_Incompat -> get_cab (br:overlaps) (br:incomps) brs + +noAxiomIncomps :: CoAxBranch -> CoAxBranch +-- Overwrite the placeholders for `cab_incomps` and `cab_overlaps` +-- with [], because unbranched axioms have no "preceding" equations +noAxiomIncomps branch = branch { cab_incomps = [], cab_overlaps = [] } {- ************************************************************************ @@ -715,14 +764,17 @@ mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars -> SrcSpan -> CoAxBranch mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc - = CoAxBranch { cab_tvs = tvs' - , cab_eta_tvs = eta_tvs' - , cab_cvs = cvs' - , cab_lhs = tidyTypes env lhs - , cab_roles = roles - , cab_rhs = tidyType env rhs - , cab_loc = loc - , cab_incomps = placeHolderIncomps } + = CoAxBranch { cab_tvs = tvs' + , cab_eta_tvs = eta_tvs' + , cab_cvs = cvs' + , cab_lhs = tidyTypes env lhs + , cab_roles = roles + , cab_rhs = tidyType env rhs + , cab_loc = loc + + -- See (SC1) in Note [Storing compatibility] + , cab_overlaps = placeHolderOverlaps + , cab_incomps = placeHolderIncomps } where (env1, tvs') = tidyVarBndrs init_tidy_env tvs (env2, eta_tvs') = tidyVarBndrs env1 eta_tvs @@ -736,14 +788,16 @@ mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc -- all of the following code is here to avoid mutual dependencies with -- Coercion -mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched -mkBranchedCoAxiom ax_name fam_tc branches +mkBranchedCoAxiom :: Role -> Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched +mkBranchedCoAxiom role ax_name fam_tc branches = CoAxiom { co_ax_unique = nameUnique ax_name , co_ax_name = ax_name , co_ax_tc = fam_tc - , co_ax_role = Nominal + , co_ax_role = role , co_ax_implicit = False , co_ax_branches = manyBranches (computeAxiomIncomps branches) } + -- computeAxiomIncomps: see (SC1) in + -- Note [Storing compatibility] mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched mkUnbranchedCoAxiom ax_name fam_tc branch @@ -752,7 +806,9 @@ mkUnbranchedCoAxiom ax_name fam_tc branch , co_ax_tc = fam_tc , co_ax_role = Nominal , co_ax_implicit = False - , co_ax_branches = unbranched (branch { cab_incomps = [] }) } + , co_ax_branches = unbranched (noAxiomIncomps branch) } + -- noAxiomIncomps: see (SC1) in + -- Note [Storing compatibility] mkSingleCoAxiom :: Role -> Name -> [TyVar] -> [TyVar] -> [CoVar] @@ -767,7 +823,9 @@ mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty , co_ax_tc = fam_tc , co_ax_role = role , co_ax_implicit = False - , co_ax_branches = unbranched (branch { cab_incomps = [] }) } + , co_ax_branches = unbranched (noAxiomIncomps branch) } + -- noAxiomIncomps: see (SC1) in + -- Note [Storing compatibility] where branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty (map (const Nominal) tvs) @@ -785,7 +843,9 @@ mkNewTypeCoAxiom name tycon tvs roles rhs_ty , co_ax_implicit = True -- See Note [Implicit axioms] in GHC.Core.TyCon , co_ax_role = Representational , co_ax_tc = tycon - , co_ax_branches = unbranched (branch { cab_incomps = [] }) } + , co_ax_branches = unbranched (noAxiomIncomps branch) } + -- noAxiomIncomps: see (SC1) in + -- Note [Storing compatibility] where branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty roles (getSrcSpan name) @@ -1223,7 +1283,9 @@ findBranch :: Array BranchIndex CoAxBranch -> Maybe (BranchIndex, [Type], [Coercion]) -- coercions relate requested types to returned axiom LHS at role N findBranch branches target_tys - = foldr go Nothing (assocs branches) + = -- Implements the Closed Family Matching Rule + -- in Note [Compatibility] + foldr go Nothing (assocs branches) where go :: (BranchIndex, CoAxBranch) -> Maybe (BranchIndex, [Type], [Coercion]) @@ -1258,6 +1320,20 @@ apartnessCheck target (CoAxBranch { cab_incomps = incomps }) isSurelyApart SurelyApart = True isSurelyApart _ = False +-- | Check whether an earlier branch matches these target types +noEarlierMatchCheck + :: [Type] + -> CoAxBranch -- ^ The candidate equation we wish to use + -> Bool -- ^ True <=> equation can fire +noEarlierMatchCheck target (CoAxBranch { cab_overlaps = overlaps }) + -- NB: this is the /only/ use of the `cab_overlaps` field + -- See Note [Storing compatiblity] and + -- (RW4) in Note [Relevance] + = not (any matches overlaps) + where + matches earlier_branch + = isJust (tcMatchTys (coAxBranchLHS earlier_branch) target) + {- ************************************************************************ * * ===================================== compiler/GHC/Core/Opt/WorkWrap/Utils.hs ===================================== @@ -1367,13 +1367,8 @@ It's surprisingly subtle. application; see test `T27627f`. TL;DR: we play safe: we never make an absent filler for any /constraint-kinded/ type, -using `isPredTy` to decide. - - * `mkAbsentFiller` returns `Nothing` for any constraint type, so worker/wrapper - keeps the real argument. - - * `Specialise.specHeader` calls `mkAbsentFiller` too, so it likewise keeps the - dead dictionary argument rather than dropping it for a filler. +using `isPredTy` to decide: `mkAbsentFiller` returns `Nothing` for any constraint +type, so worker/wrapper keeps the real argument. Prior failed approaches ===================================== compiler/GHC/Core/Unify.hs ===================================== @@ -9,6 +9,7 @@ module GHC.Core.Unify ( tcMatchTyX_BM, ruleMatchTyKiX, -- Side-effect free unification + AmIUnifying(..), tcUnifyTy, tcUnifyTys, tcUnifyFunDeps, tcUnifyDebugger, tcUnifyTysFG, tcUnifyTysForInjectivity, BindTvFun, BindFamFun, BindFlag(..), @@ -597,14 +598,14 @@ tcMatchTyX_BM :: HasDebugCallStack => BindTvFun -> Subst -> Type -> Type -> Maybe Subst tcMatchTyX_BM bind_tv subst ty1 ty2 - = tc_match_tys_x bind_tv False subst [ty1] [ty2] + = tc_match_tys_x bind_tv IgnoreOuterKinds subst [ty1] [ty2] -- | Like 'tcMatchTy', but allows the kinds of the types to differ, -- and thus matches them as well. -- See also Note [tcMatchTy vs tcMatchTyKi] tcMatchTyKi :: HasDebugCallStack => Type -> Type -> Maybe Subst tcMatchTyKi ty1 ty2 - = tc_match_tys alwaysBindTv True [ty1] [ty2] + = tc_match_tys alwaysBindTv CheckOuterKinds [ty1] [ty2] -- | This is similar to 'tcMatchTy', but extends a substitution -- See also Note [tcMatchTy vs tcMatchTyKi] @@ -614,7 +615,7 @@ tcMatchTyX :: HasDebugCallStack -> Type -- ^ Target -> Maybe Subst tcMatchTyX subst ty1 ty2 - = tc_match_tys_x alwaysBindTv False subst [ty1] [ty2] + = tc_match_tys_x alwaysBindTv IgnoreOuterKinds subst [ty1] [ty2] -- | Like 'tcMatchTy' but over a list of types. -- See also Note [tcMatchTy vs tcMatchTyKi] @@ -625,7 +626,7 @@ tcMatchTys :: HasDebugCallStack -- variables could be free in the target -- See (CU6) in Note [The Core unifier] tcMatchTys tys1 tys2 - = tc_match_tys alwaysBindTv False tys1 tys2 + = tc_match_tys alwaysBindTv IgnoreOuterKinds tys1 tys2 -- | Like 'tcMatchTyKi' but over a list of types. -- See also Note [tcMatchTy vs tcMatchTyKi] @@ -635,7 +636,7 @@ tcMatchTyKis :: HasDebugCallStack -> Maybe Subst -- ^ One-shot substitution -- See (CU6) in Note [The Core unifier] tcMatchTyKis tys1 tys2 - = tc_match_tys alwaysBindTv True tys1 tys2 + = tc_match_tys alwaysBindTv CheckOuterKinds tys1 tys2 -- | Like 'tcMatchTys', but extending a substitution -- See also Note [tcMatchTy vs tcMatchTyKi] @@ -645,7 +646,7 @@ tcMatchTysX :: HasDebugCallStack -> [Type] -- ^ Target -> Maybe Subst -- ^ One-shot substitution tcMatchTysX subst tys1 tys2 - = tc_match_tys_x alwaysBindTv False subst tys1 tys2 + = tc_match_tys_x alwaysBindTv IgnoreOuterKinds subst tys1 tys2 -- | Like 'tcMatchTyKis', but extending a substitution -- See also Note [tcMatchTy vs tcMatchTyKi] @@ -655,12 +656,12 @@ tcMatchTyKisX :: HasDebugCallStack -> [Type] -- ^ Target -> Maybe Subst -- ^ One-shot substitution tcMatchTyKisX subst tys1 tys2 - = tc_match_tys_x alwaysBindTv True subst tys1 tys2 + = tc_match_tys_x alwaysBindTv CheckOuterKinds subst tys1 tys2 -- | Same as tc_match_tys_x, but starts with an empty substitution tc_match_tys :: HasDebugCallStack => BindTvFun - -> Bool -- ^ match kinds? + -> OuterKindsFlag -- ^ Match kinds? -> [Type] -> [Type] -> Maybe Subst @@ -672,7 +673,7 @@ tc_match_tys bind_me match_kis tys1 tys2 -- | Worker for 'tcMatchTysX' and 'tcMatchTyKisX' tc_match_tys_x :: HasDebugCallStack => BindTvFun - -> Bool -- ^ match kinds? + -> OuterKindsFlag -- ^ Match kinds? -> Subst -> [Type] -> [Type] @@ -680,8 +681,8 @@ tc_match_tys_x :: HasDebugCallStack tc_match_tys_x bind_tv match_kis (Subst in_scope id_env tv_env cv_env) tys1 tys2 = case tc_unify_tys neverBindFam -- (ATF7) in Note [Apartness and type families] bind_tv - False -- Matching, not unifying - False -- Not an injectivity check + Matching -- Matching, not unifying + False -- Not an injectivity check match_kis RespectMultiplicities (mkRnEnv2 in_scope) tv_env cv_env tys1 tys2 of @@ -706,9 +707,9 @@ ruleMatchTyKiX tmpl_tvs rn_env tenv tmpl target -- But even if it did, (ATF8) in Note [Apartness and type families] -- says it doesn't matter becuase here we only care about Unifiable. -- So neverBindFam is efficient, and sufficient. - False -- Matching, not unifying + Matching -- Matching, not unifying False -- No doing an injectivity check - True -- Match the kinds + CheckOuterKinds -- Match the kinds IgnoreMultiplicities -- See Note [Rewrite rules ignore multiplicities in FunTy] rn_env tenv emptyCvSubstEnv [tmpl] [target] of @@ -784,7 +785,7 @@ tcUnifyTy t1 t2 = tcUnifyTys alwaysBindTv [t1] [t2] tcUnifyDebugger :: Type -> Type -> Maybe Subst tcUnifyDebugger t1 t2 = case tc_unify_tys_fg - True -- Unify kinds + CheckOuterKinds -- Unify kinds neverBindFam -- Does not affect Unifiable, so pick max efficient -- See (ATF8) in Note [Apartness and type families] alwaysBindTv @@ -798,7 +799,7 @@ tcUnifyFunDeps :: TyCoVarSet -> Maybe Subst tcUnifyFunDeps qtvs tys1 tys2 = case tc_unify_tys_fg - True -- Unify kinds + CheckOuterKinds -- Unify kinds dontCareBindFam -- Class-instance heads never mention type families (matchBindTv qtvs) tys1 tys2 of @@ -821,7 +822,7 @@ tcUnifyTysForInjectivity unif tys1 tys2 = case tc_unify_tys alwaysBindFam alwaysBindTv unif -- Am I unifying? True -- Do injectivity checks - False -- Don't check outermost kinds + IgnoreOuterKinds -- Don't check outermost kinds RespectMultiplicities rn_env emptyTvSubstEnv emptyCvSubstEnv tys1 tys2 of @@ -838,8 +839,9 @@ tcUnifyTysForInjectivity unif tys1 tys2 -- should never actually be done maybe_fix tv_subst - | unif = niFixSubst in_scope tv_subst - | otherwise = mkTvSubst in_scope tv_subst + = case unif of + Unifying -> niFixSubst in_scope tv_subst + Matching -> mkTvSubst in_scope tv_subst -- When matching, don't confuse domain with range; no fixpoint! ----------------- @@ -866,15 +868,15 @@ tcUnifyTysFG :: BindFamFun -> BindTvFun -> [Type] -> [Type] -> UnifyResult tcUnifyTysFG bind_fam bind_tv tys1 tys2 - = tc_unify_tys_fg False bind_fam bind_tv tys1 tys2 + = tc_unify_tys_fg IgnoreOuterKinds bind_fam bind_tv tys1 tys2 -tc_unify_tys_fg :: Bool +tc_unify_tys_fg :: OuterKindsFlag -> BindFamFun -> BindTvFun -> [Type] -> [Type] -> UnifyResult tc_unify_tys_fg match_kis bind_fam bind_tv tys1 tys2 = do { (tv_env, _) <- tc_unify_tys bind_fam bind_tv - True -- Unifying + Unifying False -- Not doing an injectivity check match_kis -- Match outer kinds RespectMultiplicities rn_env @@ -888,10 +890,10 @@ tc_unify_tys_fg match_kis bind_fam bind_tv tys1 tys2 -- | This function is actually the one to call the unifier -- a little -- too general for outside clients, though. tc_unify_tys :: BindFamFun -> BindTvFun - -> AmIUnifying -- ^ True <=> unify; False <=> match - -> Bool -- ^ True <=> doing an injectivity check - -> Bool -- ^ True <=> treat the kinds as well - -> MultiplicityFlag -- ^ see Note [Rewrite rules ignore multiplicities in FunTy] in GHC.Core.Unify + -> AmIUnifying -- ^ Unifying or matching + -> Bool -- ^ True <=> doing an injectivity check + -> OuterKindsFlag -- ^ Check outer kinds or not + -> MultiplicityFlag -- ^ see Note [Rewrite rules ignore multiplicities in FunTy] in GHC.Core.Unify -> RnEnv2 -> TvSubstEnv -- ^ substitution to extend -> CvSubstEnv @@ -910,8 +912,9 @@ tc_unify_tys :: BindFamFun -> BindTvFun -- See also Note [tcMatchTy vs tcMatchTyKi]. tc_unify_tys bind_fam bind_tv unif inj_check match_kis match_mults rn_env tv_env cv_env tys1 tys2 = initUM tv_env cv_env $ - do { when match_kis $ - unify_tys env kis1 kis2 + do { case match_kis of + CheckOuterKinds -> unify_tys env kis1 kis2 + IgnoreOuterKinds -> return () ; unify_tys env tys1 tys2 } where env = UMEnv { um_bind_tv_fun = bind_tv @@ -926,6 +929,11 @@ tc_unify_tys bind_fam bind_tv unif inj_check match_kis match_mults rn_env tv_env kis2 = map typeKind tys2 +data OuterKindsFlag + = CheckOuterKinds -- Unify or match the /kind/ of the two types + | IgnoreOuterKinds -- Just unify of match the types, ignoring kinds + -- (typically, we already know they are equal) + {- ********************************************************************* * * UnifyResult, MaybeApart etc @@ -1583,8 +1591,7 @@ c.f. Note [Comparing type synonyms] in GHC.Core.TyCo.Compare -------------- unify_ty: the main workhorse ----------- -type AmIUnifying = Bool -- True <=> Unifying - -- False <=> Matching +data AmIUnifying = Matching | Unifying type InType = Type -- Before applying the RnEnv2 type OutCoercion = Coercion -- After applying the RnEnv2 @@ -1618,7 +1625,7 @@ unify_ty env (CastTy ty1 co1) ty2 kco -- See (KCU1) in Note [Kind coercions in Unify] = maybeApart MARCast -- See (KCU2) - | um_unif env + | Unifying <- um_unif env = unify_ty env ty1 ty2 (co1 `mkTransCo` kco) | otherwise -- We are matching, not unifying @@ -1661,7 +1668,7 @@ unify_ty env (CoercionTy co1) (CoercionTy co2) kco = do { c_subst <- getCvSubstEnv ; case co1 of CoVarCo cv - | not (um_unif env) + | Matching <- um_unif env , not (cv `elemVarEnv` c_subst) -- Not forall-bound , let (_mult_co, co_l, co_r) = decomposeFunCo kco -- Because the coercion is used in a type, it should be safe to @@ -1682,7 +1689,7 @@ unify_ty env (TyVarTy tv1) ty2 kco = uVarOrFam env (TyVarLHS tv1) ty2 kco unify_ty env ty1 (TyVarTy tv2) kco - | um_unif env -- If unifying, can swap args; but not when matching + | Unifying <- um_unif env -- If unifying, can swap args; but not when matching = uVarOrFam (umSwapRn env) (TyVarLHS tv2) ty1 (mkSymCo kco) -- Deal with TyConApps @@ -1692,7 +1699,7 @@ unify_ty env ty1 ty2 kco | Just (tc,tys) <- mb_sat_fam_app1 = uVarOrFam env (TyFamLHS tc tys) ty2 kco - | um_unif env + | Unifying <- um_unif env , Just (tc,tys) <- mb_sat_fam_app2 = uVarOrFam (umSwapRn env) (TyFamLHS tc tys) ty1 (mkSymCo kco) @@ -1820,7 +1827,7 @@ uVarOrFam env ty1 ty2 kco go swapped substs lhs@(TyVarLHS tv1) ty2 kco | Just ty1' <- lookupVarEnv (um_tv_env substs) tv1' = -- We already have a substitution for tv1 - if | um_unif env -> unify_ty env ty1' ty2 kco + if | Unifying <- um_unif env -> unify_ty env ty1' ty2 kco | (ty1' `mkCastTy` kco) `tcEqType` ty2 -> return () | otherwise -> surelyApart -- Unifying: recurse into unify_ty @@ -1842,9 +1849,9 @@ uVarOrFam env ty1 ty2 kco | TyVarTy tv2 <- ty2 , let tv2' = umRnOccR env tv2 , tv1' == tv2' - = if | um_unif env -> return () - | tv1_is_bindable -> extendTvEnv tv1' ty2 - | otherwise -> return () + = if | Unifying <- um_unif env -> return () + | tv1_is_bindable -> extendTvEnv tv1' ty2 + | otherwise -> return () | tv1_is_bindable , not (mentionsForAllBoundTyVarsR env ty2_fvs) @@ -1858,9 +1865,9 @@ uVarOrFam env ty1 ty2 kco -- e.g. a ~ F p q with `a` not bindable: we might succeed with go_fam -- e.g. a ~ beta with `a` not bindable: we might be able to bind `beta` -- e.g. beta ~ F beta Int occurs check; but MaybeApart after swapping - | um_unif env + | Unifying <- um_unif env , NotSwapped <- swapped -- If we have swapped already, don't do so again - , Just lhs2 <- canEqLHS_maybe ty2 + , Just lhs2 <- canEqLHS_maybe ty2 = go IsSwapped substs lhs2 (mkTyVarTy tv1) (mkSymCo kco) | occurs_check = maybeApart MARInfinite -- Occurs check @@ -1879,7 +1886,9 @@ uVarOrFam env ty1 ty2 kco | otherwise = False - occurs_check = um_unif env && uOccursCheck substs foralld_tvs lhs rhs + occurs_check = case um_unif env of + Unifying -> uOccursCheck substs foralld_tvs lhs rhs + Matching -> False -- Occurs check, only when unifying -- see Note [Infinitary substitutions] -- Make sure you include `kco` in rhs #14846 @@ -1893,7 +1902,7 @@ uVarOrFam env ty1 ty2 kco -- Hence the RnEnv2 is empty | not under_forall , Just ty1' <- lookupFamEnv (um_fam_env substs) tc1 tys1 - = if | um_unif env -> unify_ty env ty1' ty2 kco + = if | Unifying <- um_unif env -> unify_ty env ty1' ty2 kco -- Below here we are matching -- The return () case deals with: -- Template: (F a)..(F a) @@ -1930,9 +1939,9 @@ uVarOrFam env ty1 ty2 kco -- NB: a type family can appear on the template when matching -- see (ATF6) in Note [Apartness and type families] -- (Only worth doing this if we are not under a forall.) - | um_unif env + | Unifying <- um_unif env , NotSwapped <- swapped - , Just lhs2 <- canEqLHS_maybe ty2 + , Just lhs2 <- canEqLHS_maybe ty2 = go IsSwapped substs lhs2 (mkTyConApp tc1 tys1) (mkSymCo kco) | otherwise -- See (ATF5) in Note [Apartness and type families] @@ -1962,9 +1971,9 @@ uVarOrFam env ty1 ty2 kco (inj_tys2, noninj_tys2) = partitionByList inj tys2 bind_fam_if_poss - | not (um_unif env) -- Not when matching (ATF11-1) + | Matching <- um_unif env -- Not when matching (ATF11-1) = return () - | under_forall -- Not under a forall (ATF3) + | under_forall -- Not under a forall (ATF3) = return () | BindMe <- um_bind_fam_fun env tc tys1 rhs1 = unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys1) rhs1) $ ===================================== compiler/GHC/Iface/Decl.hs ===================================== @@ -112,7 +112,7 @@ coAxBranchToIfaceBranch tc lhs_s , ifaxbRoles = roles , ifaxbRHS = toIfaceType rhs , ifaxbIncomps = iface_incomps } - where + where iface_incomps = map (expectJust . flip findIndex lhs_s . eqTypes ===================================== compiler/GHC/Iface/Syntax.hs ===================================== @@ -338,7 +338,12 @@ data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars :: [IfaceTvBndr] , ifaxbRoles :: [Role] , ifaxbRHS :: IfaceType , ifaxbIncomps :: [BranchIndex] } - -- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom + -- We store the incompatibilities in IfaceAxBranch + -- just for (perhaps unnecessary) display purposes: + -- see Note [Displaying axiom incompatibilities] + -- When we construct a real CoAxBranch we compute cab_incomps directly + -- from the equations, ignoring the ifaxbIncomps. + -- We could consider getting rid of ifaxbIncomps altogether. data IfaceConDecls = IfAbstractTyCon -- c.f TyCon.AbstractTyCon @@ -779,14 +784,13 @@ that is what is seen by importing module with --make Note [Displaying axiom incompatibilities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -With -fprint-axiom-incomps we display which closed type family equations -are incompatible with which. This information is sometimes necessary -because GHC doesn't try equations in order: any equation can be used when -all preceding equations that are incompatible with it do not apply. - -For example, the last "a && a = a" equation in Data.Type.Bool.&& is -actually compatible with all previous equations, and can reduce at any -time. +With -fprint-axiom-incomps we display which closed type family equations are +incompatible with which (see #15546). This information is sometimes necessary +because GHC doesn't try equations in order: any equation can be used when all +preceding equations that are incompatible with it do not apply. + +For example, the last "a && a = a" equation in Data.Type.Bool.&& is actually +compatible with all previous equations, and can reduce at any time. This is displayed as: Prelude> :i Data.Type.Equality.== ===================================== compiler/GHC/IfaceToCore.hs ===================================== @@ -91,7 +91,6 @@ import GHC.Utils.Logger import GHC.Data.Bag import GHC.Data.Maybe import GHC.Data.FastString -import GHC.Data.List.SetOps import GHC.Types.Annotations import GHC.Types.SourceFile @@ -903,12 +902,7 @@ tc_iface_decl _ _ (IfaceAxiom { ifName = tc_name, ifTyCon = tc -- See #13803 ; tc_branches <- forkM (text "Axiom branches" <+> ppr tc_name) $ tc_ax_branches branches - ; let axiom = CoAxiom { co_ax_unique = nameUnique tc_name - , co_ax_name = tc_name - , co_ax_tc = tc_tycon - , co_ax_role = role - , co_ax_branches = manyBranches tc_branches - , co_ax_implicit = False } + ; let axiom = mkBranchedCoAxiom role tc_name tc_tycon tc_branches ; return (ACoAxiom axiom) } tc_iface_decl _ _ (IfacePatSyn{ ifName = name @@ -1116,15 +1110,14 @@ tc_fd (tvs1, tvs2) = do { tvs1' <- mapM tcIfaceTyVar tvs1 ; return (tvs1', tvs2') } tc_ax_branches :: [IfaceAxBranch] -> IfL [CoAxBranch] -tc_ax_branches if_branches = foldlM tc_ax_branch [] if_branches +tc_ax_branches if_branches = mapM tc_ax_branch if_branches -tc_ax_branch :: [CoAxBranch] -> IfaceAxBranch -> IfL [CoAxBranch] -tc_ax_branch prev_branches - (IfaceAxBranch { ifaxbTyVars = tv_bndrs +tc_ax_branch :: IfaceAxBranch -> IfL CoAxBranch +tc_ax_branch (IfaceAxBranch { ifaxbTyVars = tv_bndrs , ifaxbEtaTyVars = eta_tv_bndrs , ifaxbCoVars = cv_bndrs , ifaxbLHS = lhs, ifaxbRHS = rhs - , ifaxbRoles = roles, ifaxbIncomps = incomps }) + , ifaxbRoles = roles }) = bindIfaceTyConBinders_AT (map (\b -> Bndr (IfaceTvBndr b) (NamedTCB Inferred)) tv_bndrs) $ \ tvs -> -- The _AT variant is needed here; see Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom @@ -1135,15 +1128,15 @@ tc_ax_branch prev_branches ; this_mod <- getIfModule ; let loc = mkGeneralSrcSpan (fsLit "module " `appendFS` moduleNameFS (moduleName this_mod)) - br = CoAxBranch { cab_loc = loc - , cab_tvs = binderVars tvs - , cab_eta_tvs = eta_tvs - , cab_cvs = cvs - , cab_lhs = tc_lhs - , cab_roles = roles - , cab_rhs = tc_rhs - , cab_incomps = map (prev_branches `getNth`) incomps } - ; return (prev_branches ++ [br]) } + ; return (CoAxBranch { cab_loc = loc + , cab_tvs = binderVars tvs + , cab_eta_tvs = eta_tvs + , cab_cvs = cvs + , cab_lhs = tc_lhs + , cab_roles = roles + , cab_rhs = tc_rhs + , cab_overlaps = placeHolderOverlaps + , cab_incomps = placeHolderIncomps }) } tcIfaceDataCons :: Name -> TyCon -> IfaceConDecls -> IfL AlgTyConRhs tcIfaceDataCons tycon_name tycon if_cons ===================================== compiler/GHC/Tc/Instance/FunDeps.hs ===================================== @@ -136,10 +136,10 @@ data FunDepEqns -- Plural becuase fd_eqs has multiple equations -- to fresh unification vars, -- See (IMP2) in Note [Improving against instances] - , fd_eqs :: [TypeEqn] -- Make these pairs of types equal - -- Invariant: In each (Pair ty1 ty2), the fd_qtvs may be - -- free in ty1 but not in ty2. See Wrinkle (1) of - -- Note [Improving against instances] + , fd_eqs :: [TypeEqn] -- Make these pairs of types equal + -- Invariant: In each (Pair ty1 ty2), the fd_qtvs may be + -- free in ty1 but not in ty2. See Wrinkle (1) of + -- Note [Improving against instances] } instance Outputable FunDepEqns where ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -26,12 +26,14 @@ import GHC.Core.Coercion import GHC.Core.TyCo.Rep( Type(..) ) import GHC.Core.Predicate( EqRel(..) ) import GHC.Core.TyCon -import GHC.Core.Unify( tcUnifyTysForInjectivity, typeListsAreApart ) +import GHC.Core.Unify( AmIUnifying(..) + , tcUnifyTysForInjectivity, typeListsAreApart ) import GHC.Core.Coercion.Axiom import GHC.Core.TyCo.Subst( elemSubst ) import GHC.Builtin.WiredIn.TypeLits( tryInteractTopFam, tryInteractInertFam ) +import GHC.Types.Var( TyVar, tyVarKind, setTyVarKind ) import GHC.Types.Var.Set import GHC.Utils.Outputable @@ -39,7 +41,7 @@ import GHC.Utils.Panic import Control.Monad( unless ) import GHC.Data.Pair -import Data.Maybe( isNothing, isJust, mapMaybe ) +import Data.Maybe( isJust, mapMaybe ) {- Note [Overview of functional dependencies in type inference] @@ -109,7 +111,6 @@ Wrinkles from fundeps, but that would require new evidence forms, and an extension to FC, so we don't do that right now (Dec 14). - Note [FunDep and implicit parameter reactions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Currently, our story of interacting two dictionaries (or a dictionary @@ -573,6 +574,7 @@ tryEqFunDeps work_item@(EqCt { eq_lhs = work_lhs tryFamEqFunDeps :: TcSMode -> [EqCt] -> TyCon -> [TcType] -> EqCt -> SolverStage () +-- See Note [Type inference for type families with injectivity] tryFamEqFunDeps mode eqs_for_me fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs = work_rhs }) | Just ops <- builtInClosedTyFamTyCon_maybe fam_tc @@ -583,6 +585,7 @@ tryFamEqFunDeps mode eqs_for_me fam_tc work_args ; tryFDEqns False fam_tc work_args work_item eqns ; unless (hasRelevantGiven eqs_for_me work_args work_item) $ + -- hasRelevantGiven: See (CF1) in Note [Exploiting closed type families] do { eqns <- mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs ; tryFDEqns True fam_tc work_args work_item eqns } } @@ -599,8 +602,11 @@ tryFamEqFunDeps mode eqs_for_me fam_tc work_args NotInjective -> nopStage () Injective inj -> do { eqns <- mkLocalFamEqFDs eqs_for_me fam_tc inj work_args work_rhs ; tryFDEqns False fam_tc work_args work_item eqns } + -- NB: tryFDEqns bales out on an insoluble fundep + -- See (CF4) in Note [Exploiting closed type families] ; unless (hasRelevantGiven eqs_for_me work_args work_item) $ + -- hasRelevantGiven: See (CF1) in Note [Exploiting closed type families] do { eqns <- mkTopFamEqFDs fam_tc work_args work_item ; tryFDEqns True fam_tc work_args work_item eqns } } @@ -638,10 +644,11 @@ tryFDEqns is_top fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) f -- User-defined type families ----------------------------------------- mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> EqCt -> SolverStage [FunDepEqns] +-- Implements (INJFAM:Wanted/top-closed) +-- See Note [Exploiting closed type families] -- Look at the top-level axioms; we effectively infer injectivity, --- so we don't need tyConInjectivtyInfo. This works fine for closed +-- so we don't need tyConInjectivityInfo. This works fine for closed -- type families without injectivity info --- See Note [Exploiting closed type families] mkTopClosedFamEqFDs ax work_args (EqCt { eq_ev = ev, eq_rhs = work_rhs }) | isGenerativeType work_rhs -- See (CF5) in Note [Exploiting closed type families] = Stage $ @@ -679,39 +686,46 @@ hasRelevantGiven eqs_for_me work_args (EqCt { eq_rhs = work_rhs }) relevant (EqCt { eq_ev = ev, eq_lhs = lhs, eq_rhs = rhs_ty }) | isGiven ev , TyFamLHS _ lhs_tys <- lhs - = isJust (tcUnifyTysForInjectivity True work_tys (rhs_ty:lhs_tys)) + = isJust (tcUnifyTysForInjectivity Unifying work_tys (rhs_ty:lhs_tys)) | otherwise = False getRelevantBranches :: CoAxiom Branched -> [TcType] -> Xi -> [FunDepEqns] -- Return the FunDepEqns that arise from each relevant branch +-- Implements Note [Relevance] getRelevantBranches ax work_args work_rhs - = go [] (fromBranches (coAxiomBranches ax)) + = go (fromBranches (coAxiomBranches ax)) where work_tys = work_rhs : work_args - go _ [] = [] - go preceding (branch:branches) + go [] = [] + go (branch:branches) = case is_relevant branch of - Just eqn -> eqn : go (branch:preceding) branches - Nothing -> go (branch:preceding) branches + Just eqn -> eqn : go branches + Nothing -> go branches where - is_relevant (CoAxBranch { cab_tvs = qtvs, cab_lhs = lhs_tys, cab_rhs = rhs_ty }) - | Just subst <- tcUnifyTysForInjectivity True (rhs_ty:lhs_tys) work_tys - , let (subst', qtvs') = trim_qtvs subst qtvs - lhs_tys' = substTys subst' lhs_tys - rhs_ty' = substTy subst' rhs_ty - , all (no_match lhs_tys') preceding + is_relevant branch@(CoAxBranch { cab_tvs = qtvs + , cab_lhs = lhs_tys + , cab_rhs = rhs_ty }) + | Just subst <- tcUnifyTysForInjectivity Unifying (rhs_ty:lhs_tys) work_tys + -- See (RW1)-(RW3) in Note [Relevance] + -- This is a pre-/unification/ check (not matching) + -- so `subst` can bind both `qtvs` and fvs(work_tys) + , let (subst',qtvs') = trim_qtvs subst qtvs + lhs_tys' = substTys subst' lhs_tys + rhs_ty' = substTy subst' rhs_ty + branch_tys' = rhs_ty' : lhs_tys' + , noEarlierMatchCheck lhs_tys' branch -- See (RW4) in Note [Relevance] = Just (FDEqns { fd_qtvs = qtvs' - , fd_eqs = zipWith Pair (rhs_ty':lhs_tys') work_tys }) + , fd_eqs = zipWith Pair branch_tys' work_tys }) + -- Do not apply the substition to `work_tys`; + -- See (CF7) in Note [Exploiting closed type families] | otherwise = Nothing - no_match lhs_tys (CoAxBranch { cab_lhs = lhs_tys1 }) - = isNothing (tcUnifyTysForInjectivity False lhs_tys1 lhs_tys) - mkTopOpenFamEqFDs :: TyCon -> [Bool] -> [TcType] -> EqCt -> TcS [FunDepEqns] --- Implements (INJFAM:Wanted/top) +-- Implements (INJFAM:Wanted/top-open) +-- See Note [Exploiting open type families] mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs }) = do { fam_envs <- getFamInstEnvs ; let branches :: [CoAxBranch] @@ -720,15 +734,15 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs }) ; return (mapMaybe do_one branches) } where do_one :: CoAxBranch -> Maybe FunDepEqns - do_one branch@(CoAxBranch { cab_tvs = branch_tvs - , cab_lhs = branch_lhs_tys - , cab_rhs = branch_rhs }) - | Just subst <- tcUnifyTysForInjectivity False [branch_rhs] [work_rhs] - -- False: matching, not unifying - , let (subst', qtvs) = trim_qtvs subst branch_tvs + do_one (CoAxBranch { cab_tvs = branch_qtvs + , cab_lhs = branch_lhs_tys + , cab_rhs = branch_rhs }) + | Just subst <- tcUnifyTysForInjectivity Matching [branch_rhs] [work_rhs] + , let (subst', qtvs') = trim_qtvs subst branch_qtvs branch_lhs_tys' = substTys subst' branch_lhs_tys - , apartnessCheck branch_lhs_tys' branch -- See (TIF3) - = Just (mkInjectivityFDEqn inj_flags qtvs branch_lhs_tys' work_args) + -- No need for an apartness check here; for open type families + -- there are no "preceding" equations + = Just (mkInjectivityFDEqn inj_flags qtvs' branch_lhs_tys' work_args) | otherwise = Nothing @@ -736,7 +750,7 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs }) mkLocalFamEqFDs :: [EqCt] -> TyCon -> [Bool] -> [TcType] -> Xi -> SolverStage [FunDepEqns] -- Wanted constraints only -- Both open and closed type families, but only ones with declared injectivity --- See Note [Type inference for type families with injectivity] esp (TIF2) +-- See Note [Exploiting local type-family injectivity] mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs = do { let -- eqns_from_inerts: see (INJFAM:Wanted/other) eqns_from_inerts = mapMaybe do_one eqs_for_me @@ -755,15 +769,23 @@ mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs mk_eqn iargs = mkInjectivityFDEqn inj_flags [] work_args iargs -trim_qtvs :: Subst -> [TcTyVar] -> (Subst,[TcTyVar]) --- Tricky stuff: see (TIF1) in --- Note [Type inference for type families with injectivity] -trim_qtvs subst [] = (subst, []) -trim_qtvs subst (tv:tvs) - | tv `elemSubst` subst = trim_qtvs subst tvs - | otherwise = let !(subst1, tv') = substTyVarBndr subst tv - !(subst', tvs') = trim_qtvs subst1 tvs - in (subst', tv':tvs') +trim_qtvs :: Subst -> [TyVar] -> (Subst, [TyVar]) +-- Tricky stuff: see (OF1) in Note [Exploiting open type families] +-- The returned substitution is identical to the incoming one, except that +-- its in-scope set is extended with the returned [TyVar] +trim_qtvs unif_subst qtvs + = go unif_subst qtvs + where + go :: Subst -> [TyVar] -> (Subst, [TyVar]) + go subst [] = (subst, []) + go subst (tv:tvs) + | tv `elemSubst` unif_subst = go subst tvs + | otherwise = (subst'', tv':tvs') + where + tv' = tv `setTyVarKind` substTy subst (tyVarKind tv) + subst' = subst `extendSubstInScope` tv' + !(subst'', tvs') = go subst' tvs + ----------------------------------------- -- Built-in type families @@ -924,15 +946,20 @@ we attempt to exploit injectivity, via `mkLocalFamEqFDs`: * (INJFAM:Wanted/other) see `mkLocalFamEqFDs` work item: [W] F s1 s2 ~ rhs -- Wanted inert: [G/W] F t2 t2 ~ rhs -- Same `rhs`, Given or Wanted - We can generate FunDepEqns: (s2 ~ t2) + See Note [Exploiting local type-family injectivity] + +* (INJFAM:Wanted/top-open) for open type families: `mkTopOpenFamEqFDs` + type family F a b = r | r -> b + type instance F Int (Maybe a) = [G Int] -- G is a type family + [W] F alpha beta = [ty] + We can generate (Maybe gamma ~ beta) + See Note [Exploiting open type families] -* (INJFAM:Wanted/top) see `mkTopUserFamEqFDs` - work item: [W] F s1 s2 ~ rhs - type instance forall a b c. F t1 t2 ~ top_rhs - and we can /match/ the LHS, so that - S(top_rhs) = rhs - then we can generate the FunDepEqns: forall a c. s2 ~ S(t2) - But see wrinkle (TIF1), (TIF3) +* (INJFAM:Wanted/top-closed) for closed type families: `mkTopClosedFamEqFDs` + type family F a b where { ...eqns... } + [W] F alpha ~ Int + We may be able to generate some extra equalities to constraint `alpha` + See very clever Note [Exploiting closed type families] For /built-in/ type families, it's pretty similar, except that @@ -945,45 +972,36 @@ For /built-in/ type families, it's pretty similar, except that * mkLocalBuiltinFamEqFDs * mkTopBuiltinFamEqFDs -(TIF1) Generating fundeps from a top-level type instance is covered in - Section 5.2 in the Injective Type Families paper. It's a bit tricky. - Consider - type family F @k (a::k) (b::k) = r | r -> k b - type instance forall k (a::k) (b::k). F @k (Proxy @k a) (Proxy @k b) = Proxy @k a - [W] F @kappa alpha beta ~ Maybe (Proxy @kappa (delta::kappa)) +Note [Exploiting local type-family injectivity] see `mkLocalFamEqFDs` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have a type family with declared injectivity: + type family F a b = r | r -> b +and we have + work item: [W] F s1 s2 ~ F t1 t2 +or + work item: [W] F s1 s2 ~ rhs -- Wanted + inert: [G/W] F t2 t2 ~ rhs -- Same `rhs`, Given or Wanted - we match (Proxy @kappa delta) against the template (Proxy k a), succeeding - with substitution [k:->kappa, a:->delta]. We want to generate this FunDepEqns - FDEqn { fd_qtvs = [b:kappa], fd_eqs = [ beta ~ Proxy @kappa b ] } - Notice that - * we must quantify the FunDepEqns over `b`, which is not matched; for this - we will generate a fresh unification variable in `instantiateFunDepEqn`. - * we must substitute `k:->kappa` in the kind of `b`. - This fancy footwork for `fd_qtvs` is done by `trim_qtvs` in - `mkInjWantedFamEqTopEqns`. +Then we can generate FunDepEqns: (s2 ~ t2) + +This applies equally to /closed/ type families; it is /not/ subsumed +by Note [Exploiting closed type families]. Consider: -(TIF2) All this applies equally to /closed/ type families; it is /not/ - subsumed by Note [Exploiting closed type families]. Consider: type family F a | r -> a where { .... } [W] F t1 ~ a [W] F t2 ~ a - Then since F is declared injective, we can generate t1~t2. +Then since F is declared injective, we can generate t1~t2. - As for open type families, we insist on /user-declared/ injectivity only; we - don't try to /infer/ injectivity even for a closed family. See Section 3.4 - of the "Injective type families" paper. (Arguably, we could /infer/ - injectivity for closed type families, and that would be more in the spirit of - Note [Exploiting closed type families].) +As for open type families, we insist on /user-declared/ injectivity only; we +don't try to /infer/ injectivity even for a closed family. See Section 3.4 +of the "Injective type families" paper. (Arguably, we could /infer/ +injectivity for closed type families, and that would be more in the spirit of +Note [Exploiting closed type families].) -(TIF3) Further to (TIF1), if we are considering a /closed/ type family, we - must ensure (see Section 5.2 of the paper) that after matching that - equation would indeed be the one to fire. So we call `apartnessCheck` - on the branch to ensure this, in `mkTopUserFamEqFDs`. - -Definition [Relevance] -~~~~~~~~~~~~~~~~~~~~~~ +Note [Relevance] +~~~~~~~~~~~~~~~~ We say that a closed-type-family equation `F lhs = rhs` is /relevant/ for a Wanted [W] F wlhs ~ wrhs iff @@ -992,6 +1010,10 @@ iff (R2) There is no earlier equation that matches S(lhs). See (RW4) below. +The relevance check is implemented by `getRelevantBranches`, which acutally +returns the [FunDepEqns] described in the Closed Family Fundep Algorithm in +Note [Exploiting closed type families]. + (RW1) Pre-unification treats type-family applications as binding to anything, rather like type variables. If two types don't even pre-unify, we say that they are /apart/. It is done by `tcUnifyTysForInjectivity`. @@ -1014,24 +1036,99 @@ iff Clearly the RHS is apart from the first equation and we want to fire injectivity on the second equation. -(RW4) Why "no earlier equation matches" in conditoin (R2)? Consider the family +(RW4) Why "no earlier equation matches" in condition (R2)? Consider the family type family Bak a = r where Bak Int = Char -- B1 Bak Char = Int -- B2 Bak a = a -- B3 - and [W] Bak alpha ~ Char. In fact, only (B2) is relevant for this Wanted. + and [W] Bak alpha ~ Char. In fact, only (B1) is relevant for this Wanted. You might think that (B3) could be instantiated to Bak Char ~ Char; but actually that instantiation will never fire because (B2) Bak Char ~ Int would - fire first. So the only way to return a Char is if the argment is Int; so we - can emit [W] alpha ~ Int. Hence (B3) is not relevant; only (B2) is relevant. + fire first. So the only way to return a Char is via (B1); so we + can emit [W] alpha ~ Int. Hence (B3) is not relevant; only (B1) is relevant. That is the reason for condition (R2) in the definition of Relevance above. A watertight proof that this is the Right Thing is not very easy. See more - discussion in #23162. + discussion in #23162, and Section 5.2 of the paper. + + How, precisely, do we implement (R2)? We check that there is no earlier equation + that fires on S(lhs), in this case (on Bak Char). Notice that this is different + from the `apartnessCheck`, which checks that all preceding equations are apart + from S(lhs). Apartness checking uses /unification/; here we want /matching/. + Hence using `noEarlierMatchCheck`, not `apartnessCheck`. + + Here's a good example from T27171_aux. T + type family TMessage m where + {- T1 -} TMessage @f @t (CustomMethod s :: Method f t) = () + {- T2 -} TMessage @f @Req (m :: Method f Req) = TRequestMessage m + {- T3 -} TMessage @f @Not (m :: Method f Not) = TNotificationMessage m + + [W] TMessage @SC @Req alpha ~# TRequestMessage alpha + + There is only one relevant equation, namely (T2). If we apply its + pre-unification substitution [f :-> SC, m :-> alpha] to its LHS we get + TMessage @SC @Req alpha + and equation (T1) does not match that. (It does unify, but we don't care.) + +(RW5) `noEarlierMatchCheck`: in (RW4) We really do need to check that /no/ + earlier equation matches, not just no earlier /incompatible/ equation + matches. Consider T27282a: + type family F a where + F Int = Int -- B1 + F Char = Bool -- B2 + F a = a -- B3 + + [W] F alpha ~ Int + + (B1) is relevant, and (B2) is not. What about (B3)? It pre-unifies with + the Wanted via [alpha :-> Int, a :-> Int]. But under that substitution + (B1) would fire, so (B3) is not relevant. + + And yet, (B1) is /compatible/ with (B3), so it's no good just looking at + the `cab_incomps` of (B3). Instead we look at `cab_overlaps`. + +Note [Exploiting open type families] see `mkTopOpenFamEqFDs` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Generating fundeps from a top-level type instance is covered in Section 5.2 in +the Injective Type Families paper. For open type families, suppose we have + + type family F a b = r | r -> b + type instance F Int (Maybe a) = [G Int] -- G is a type family + + [W] F alpha beta = [ty] + +Then, since F has been checked as injective, and the RHS [G Int] +pre-unifies with [ty], we can add a derived FunDepEqns + FDEqns{ fd_qtvs = a, fd_eqs = [ Maybe a ~ beta ] } +and thereby emit + [W] Maybe gamma ~ beta -- Fresh gamma + +Wrinkles + +(OF1) Consider + type family F @k (a::k) (b::k) = r | r -> k b + type instance forall k (a::k) (b::k). + F @k (Proxy @k a) (Proxy @k b) = Maybe (Proxy @k a) -Note [Exploiting closed type families] + [W] F @kappa alpha beta ~ Maybe (Proxy @kappa (delta::kappa)) + + We match the target (Maybe (Proxy @kappa delta)) + against the template (Maybe (Proxy @k a)) + succeeding with substitution [k:->kappa, a:->delta]. We want to generate this: + FDEqn { fd_qtvs = [b::kappa], fd_eqs = [ Proxy @kappa b ] ~ beta } + Notice that + * we must quantify the FunDepEqns over `b`, which is not matched; for this + we will generate a fresh unification variable in `instantiateFunDepEqn`. + * we must substitute `k:->kappa` in the kind of `b`. + + This fancy footwork for `fd_qtvs` is done by `trim_qtvs`. It + * Drops a quantified tyvar that /is/ matched + * Substitutes in the kind of a quantified tyvar that is /not/ matched + * Adds the not-matched tyvar to the in-scope set of the substitution + +Note [Exploiting closed type families] see `mkTopClosedFamEqFDs` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have type family F a b where @@ -1042,17 +1139,18 @@ Suppose we have [W] F Int alpha ~ Char The /only/ way to solve this Wanted is using (F2), so we can safely unify -alpha:=Char without risking losing any solutions. That is what -`mkTopClosedFamEqFDs` does. Ticket #23162 has lots of background detail +alpha:=Char without risking losing any solutions. We don't even need any +injectivity annotations. Ticket #23162 has lots of background detail. -More precisely, here is the Closed Family Fundep Algorithm (CFFA) +More precisely, here is the very clever Closed Family Fundep Algorithm (CFFA) IF * F a is a closed type family. * We are trying to solve [W] F wlhs ~ wrhs. - * There are no "relevant" Givens [G] F lhs ~ rhs. See (CF1) below. - * F has exactly one equation, F lhs = rhs that is "relevant" for that Wanted + * There are no "relevant Givens" [G] F lhs ~ rhs. See (CF1) below. + * F has exactly one equation, F lhs = rhs that is "relevant" for + that Wanted (see Note [Relevance]) THEN - we can emit and solve the fundep equalities: + we can emit and solve the fundeps :: [FunDepEqns]: [W] wlhs1 ~ lhs1 ... [W] wlhsn ~ lhsn @@ -1060,7 +1158,10 @@ More precisely, here is the Closed Family Fundep Algorithm (CFFA) with fresh unification vars in lhs and rhs for the quantified variables of the equation. -See Definition [Relevance] for what "relevant" means. + Actually we take advantage of the substitution generated by the relevance + check, see (CF7) below. + +See Note [Relevance] for what "relevant" means. We need to take care about non-termination; see (CF3). Key point: equations that are not relevant do not need to be considered for fundeps at all. @@ -1166,6 +1267,8 @@ Key point: equations that are not relevant do not need to be considered for fund I was looking at non-termination for closed type families, but it's a small improvement in general. + This bale-out is implementedn in `tryFDEqns`. + (CF5) Consider (see "Yikes5" in #23162): type family F a where F (Just x) = Int @@ -1196,7 +1299,7 @@ Key point: equations that are not relevant do not need to be considered for fund type family I t = res | res -> t where I TInt = Int |> g -- where g :: Type ~# IK k and [W] I alpha ~ Int |> g2 - Here we definiteily want to take advantage of injectivity. + Here we definitely want to take advantage of injectivity. (CF6) This machinery can also have a significant positive effect on the size of proof terms. For example (simplification of T26426): @@ -1204,7 +1307,8 @@ Key point: equations that are not relevant do not need to be considered for fund type family (++) a b where { '[] ++ ys = ys; (x:xs) ++ ys = x : (xs ++ ys) } type family MapId a where { MapId '[] = '[]; MapId (x:xs) = x : MapId xs } - app :: (MapId xs ++ MapId ys ~ MapId (xs ++ ys)) => Proxy xs -> Proxy ys -> Proxy (xs ++ ys) + app :: (MapId xs ++ MapId ys ~ MapId (xs ++ ys)) + => Proxy xs -> Proxy ys -> Proxy (xs ++ ys) test :: Proxy [ty_1, ..., ty_n] test = Proxy @'[ty_1] @@ -1248,6 +1352,30 @@ Key point: equations that are not relevant do not need to be considered for fund instead of relying on recursively built sub-proof terms, which brings down coercion sizes (in certain situations) from O(n^3) to O(n^2). +(CF7) Relevance. When computing relevance in the Closed Family Fundep Algorithm, + for [W] F wlhs1 wlhs2 ~ wrhs, against an equation F lhs1 lhs2 ~ rhs + we get back a pre-unifying substitution S that makes the two as equal as poss. + Then we use `trim_qtvs` in exactly the same way as in + (OF1) of Note [Exploiting closed type families], to generate qtvs' and S' + Then we generate + FDEqns { fd_qtvs = qtvs', fd_eqs [ S'(lhs1) ~ wlhs1 + , S'(lhs2) ~ wlhs2 + , S'(rhs) ~ wrhs ] } + Notice that we do /not/ apply S' to wlhs/wrhs. These type contain unification + variables that we must actually unify! Example + type familiy F a b where + F [a] (Maybe b) = (a, G b) + [W] F alpha beta ~ (Int, [gamma]) + Pre-unification gives [alpha :-> [a], beta :-> Maybe b, a :-> Int] + This substitution eliminates the quantified variable `a` but not `b`, so we + want this: + FDEqns { fd_qtvs = [b], fd_eqs [ [Int] ~ alpha + , Maybe b ~ beta + , (Int,G b) ~ (Int, [gamma]) ] } + + Notice also that by applying the substitution to the template but not to the + Wanted, we uphold the `fd_eqs` invariant in `FDEqns` (see its data type decl) + Note [Cache-caused loops] ~~~~~~~~~~~~~~~~~~~~~~~~~ It is very dangerous to cache a rewritten wanted family equation as 'solved' in @@ -1340,28 +1468,29 @@ solveFunDeps work_ev fd_eqns ; uPairsTcM uenv eqs } instantiateFunDepEqns :: FunDepEqns -> TcM [TypeEqn] -instantiateFunDepEqns (FDEqns { fd_qtvs = tvs, fd_eqs = eqs }) - | null tvs +-- See GHC.Tc.Instance.Fundeps Note [Improving against instances] +-- Wrinkle (IMP1) +instantiateFunDepEqns (FDEqns { fd_qtvs = qtvs, fd_eqs = eqs }) + | null qtvs = return rev_eqs | otherwise - = do { TcM.traceTc "instantiateFunDepEqns" (ppr tvs $$ ppr eqs) - ; (_, subst) <- instFlexiXTcM emptySubst tvs -- Takes account of kind substitution + = do { TcM.traceTc "instantiateFunDepEqns" (ppr qtvs $$ ppr eqs) + ; (_, subst) <- instFlexiXTcM emptySubst qtvs -- Takes account of kind substitution ; return (map (subst_pair subst) rev_eqs) } where rev_eqs = reverse eqs -- (reverse eqs): See Note [Reverse order of fundep equations] subst_pair subst (Pair ty1 ty2) - = Pair (substTyUnchecked subst' ty1) ty2 + = Pair (substTy subst' ty1) ty2 -- ty2 does not mention fd_qtvs, so no need to subst it. - -- See GHC.Tc.Instance.Fundeps Note [Improving against instances] - -- Wrinkle (1) + -- See invariant on `fv_eqs` in `data FunDepEqns`. where - subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1) + subst' = extendSubstInScopeSet subst (tyCoVarsOfTypes [ty1,ty2]) -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result -- of matching with the [W] constraint. So we add its free -- vars to InScopeSet, to satisfy substTy's invariants, even - -- though ty1 will never (currently) be a poytype, so this + -- though ty1 will never (currently) be a polytype, so this -- InScopeSet will never be looked at. ===================================== compiler/GHC/Tc/TyCl.hs ===================================== @@ -3462,7 +3462,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info ; let mb_co_ax | null eqns = Nothing -- mkBranchedCoAxiom fails on empty list - | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches) + | otherwise = Just (mkBranchedCoAxiom Nominal co_ax_name fam_tc branches) fam_tc = mkFamilyTyCon tc_name kind tc_bndrs 0 res_kind (resultVariableName sig) (ClosedTypeFamilyTyCon $ CTF mb_co_ax) parent inj' ===================================== compiler/GHC/Unit/State.hs ===================================== @@ -369,10 +369,15 @@ data UnitState = UnitState { -- is always mentioned before the units it depends on. preloadUnits :: [UnitId], - -- | Units which we explicitly depend on (from a command line flag). - -- We'll use this to generate version macros and the unused packages warning. The - -- original flag which was used to bring the unit into scope is recorded for the - -- -Wunused-packages warning. + -- | The units that can be used by the respective home unit. Despite the + -- identifier, this does not just cover units that are enabled explicitly + -- using flags but also units from the package database that are enabled + -- implicitly in case @-hide-all-packages@ is absent. The former are paired + -- with 'Just' applied to the respective flags, the latter are paired with + -- 'Nothing'. + -- + -- This field is used for generating version macros and “unused packages” + -- warnings. explicitUnits :: [(Unit, Maybe PackageArg)], homeUnitDepends :: Set UnitId, @@ -907,7 +912,7 @@ mkUnitState logger unit_index cfg = do let pkgname_map = listToUFM [ (unitPackageName p, unitInstanceOf p) | p <- pkgs2 ] - -- The explicitUnits accurately reflects the set of units we have turned + -- The explicitUnits accurately reflects the set of units that are turned -- on; as such, it also is the only way one can come up with requirements. -- The requirement context is directly based off of this: we simply -- look for nested unit IDs that are directly fed holes: the requirements ===================================== testsuite/tests/indexed-types/should_compile/T27828.hs ===================================== @@ -0,0 +1,50 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeAbstractions #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +module Bug where + +import Data.Functor.Identity (Identity(..)) +import Data.Kind (Type) +import Data.Proxy (Proxy(..)) +import Data.Type.Equality ((:~:)(..)) + +type TyFun :: Type -> Type -> Type +data TyFun a b + +type (~>) :: Type -> Type -> Type +type a ~> b = TyFun a b -> Type +infixr 0 ~> + +type Apply :: (k1 ~> k2) -> k1 -> k2 +type family Apply f x + +type Rep1 :: (k -> Type) -> k -> Type +type family Rep1 f + +type To1 :: Rep1 f a -> f a +type family To1 z + +type Par1 :: Type -> Type +newtype Par1 p = Par1 p + +type To1Sym0 :: forall k (f :: k -> Type) (a :: k). Rep1 f a ~> f a +data To1Sym0 z + +applyTo1Sym0 :: forall k (f :: k -> Type) (a :: k) (x :: Rep1 f a). Proxy x -> Apply @(Rep1 f a) @(f a) To1Sym0 x :~: To1 x +applyTo1Sym0 _ = undefined + +type IdentitySym0 :: a ~> Identity a +data IdentitySym0 z +type instance Apply IdentitySym0 x = 'Identity x + +type Aux :: Rep1 Identity a -> Rep1 Identity a -> Identity a +type family Aux x y where + Aux x ('Par1 wombat) = Apply IdentitySym0 wombat + +type instance Rep1 Identity = Par1 +type instance To1 @Identity y = Aux y y + +lemma :: forall a (z :: a). Apply @(Rep1 Identity a) @(Identity a) To1Sym0 ('Par1 z) :~: 'Identity z +lemma = applyTo1Sym0 @Type @Identity @a (Proxy @('Par1 z)) +-- lemma = applyTo1Sym0 @Type @Identity @a @('Par1 z) (Proxy @('Par1 z)) ===================================== testsuite/tests/indexed-types/should_compile/T27828a.hs ===================================== @@ -0,0 +1,16 @@ +{-# LANGUAGE TypeFamilies #-} + +module T27828a where + +import Data.Proxy + +type family F a where + F Int = Int -- B1 + F Char = Bool -- B2 + F a = a -- B3 + +h :: (F a ~ Int) => Proxy a -> () +h = error "urk" + +k :: () +k = h Proxy -- [W] F alpha ~ Int ===================================== testsuite/tests/indexed-types/should_compile/all.T ===================================== @@ -316,3 +316,5 @@ test('T25611b', normal, compile, ['']) test('T25611c', normal, compile, ['']) test('T25611d', normal, compile, ['']) test('T25657', normal, compile, ['']) +test('T27828', normal, compile, ['']) +test('T27828a', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/c5cd2f1adaccf6da85beae64f13fa5… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/c5cd2f1adaccf6da85beae64f13fa5… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc] Deleted branch wip/jeltsch/improve-closure-property-check
by Wolfgang Jeltsch (＠jeltsch) 25 Sep '26

25 Sep '26

Wolfgang Jeltsch deleted branch wip/jeltsch/improve-closure-property-check at Glasgow Haskell Compiler / GHC -- You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc][master] EPA: Add specific layout field to AnnList
by Marge Bot (＠marge-bot) 25 Sep '26

25 Sep '26

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 9f48a5b9 by Alan Zimmerman at 2026-09-25T17:02:50-04:00 EPA: Add specific layout field to AnnList Up to now AnnList has effectively served to represent lists of things having layout, regardless of whether they do or not. In Haskell, layout is optional in many places, as there is also an alternative syntax using braces and semi-colons, which is free-form. This commit introduces AnnListLayout, a data structure capturing this distinction. It is deliberately set up similarly to EpLayout, so that these two can be merged in time. The transition is done mechanically, where AnnListBraces is not used yet, the original Nothing case maps to AnnListNoLayout, and the Just case to AnnListLayout. Later commits will fine tune these against the actual parser layout. - - - - - 19 changed files: - compiler/GHC/Parser.y - compiler/GHC/Parser/Annotation.hs - compiler/GHC/Parser/PostProcess.hs - testsuite/tests/ghc-api/exactprint/T22919.stderr - testsuite/tests/ghc-api/exactprint/ZeroWidthSemi.stderr - testsuite/tests/module/mod185.stderr - testsuite/tests/parser/should_compile/DumpParsedAst.stderr - testsuite/tests/parser/should_compile/DumpParsedAstComments.stderr - testsuite/tests/parser/should_compile/DumpRenamedAst.stderr - testsuite/tests/parser/should_compile/DumpSemis.stderr - testsuite/tests/parser/should_compile/KindSigs.stderr - testsuite/tests/parser/should_compile/T15279.stderr - testsuite/tests/parser/should_compile/T20718.stderr - testsuite/tests/parser/should_compile/T20846.stderr - testsuite/tests/printer/Test20297.stdout - testsuite/tests/printer/Test24533.stdout - utils/check-exact/ExactPrint.hs - utils/check-exact/Main.hs - utils/check-exact/Transform.hs Changes: ===================================== compiler/GHC/Parser.y ===================================== @@ -1796,10 +1796,10 @@ cvars1 :: { [RecordPatSynField GhcPs] } where_decls :: { LocatedA (OrdList (LHsDecl GhcPs), EpToken "where", AnnList) } : 'where' '{' decls '}' {% amsA' (sLL $1 $> (thdOf3 $ unLoc $3, epTok $1, - AnnList (Just (fstOf3 $ unLoc $3)) (ListBraces (epTok $2) (epTok $4)) (sndOf3 $ unLoc $3))) } + AnnList (AnnListLayout (fstOf3 $ unLoc $3)) (ListBraces (epTok $2) (epTok $4)) (sndOf3 $ unLoc $3))) } | 'where' vocurly decls close {% amsA' (sLL $1 $3 (thdOf3 $ unLoc $3, epTok $1, - AnnList (Just (fstOf3 $ unLoc $3)) ListNone (sndOf3 $ unLoc $3))) } + AnnList (AnnListLayout (fstOf3 $ unLoc $3)) ListNone (sndOf3 $ unLoc $3))) } pattern_synonym_sig :: { LSig GhcPs } : 'pattern' con_list '::' sigtype @@ -1935,9 +1935,9 @@ decls :: { Located (EpaLocation, [EpToken ";"], OrdList (LHsDecl GhcPs)) } | {- empty -} { noLoc (noAnn, [],nilOL) } decllist :: { Located (AnnList,Located (OrdList (LHsDecl GhcPs))) } - : '{' decls '}' { sLL $1 $> (AnnList (Just (fstOf3 $ unLoc $2)) (ListBraces (epTok $1) (epTok $3)) (sndOf3 $ unLoc $2) + : '{' decls '}' { sLL $1 $> (AnnList (AnnListLayout (fstOf3 $ unLoc $2)) (ListBraces (epTok $1) (epTok $3)) (sndOf3 $ unLoc $2) ,sL1 $2 $ thdOf3 $ unLoc $2) } - | vocurly decls close { sL1 $2 (AnnList (Just (fstOf3 $ unLoc $2)) ListNone (sndOf3 $ unLoc $2) + | vocurly decls close { sL1 $2 (AnnList (AnnListLayout (fstOf3 $ unLoc $2)) ListNone (sndOf3 $ unLoc $2) ,sL1 $2 $ thdOf3 $ unLoc $2) } -- Binding groups other than those of class and instance declarations @@ -1945,16 +1945,16 @@ decllist :: { Located (AnnList,Located (OrdList (LHsDecl GhcPs))) } binds :: { Located (HsLocalBinds GhcPs) } -- May have implicit parameters -- No type declarations - : decllist {% do { let { (AnnList anc p s, decls) = unLoc $1 } + : decllist {% do { let { (AnnList la p s, decls) = unLoc $1 } ; val_binds <- cvBindGroup (unLoc $ decls) ; !cs <- getCommentsFor (gl $1) - ; return (sL1 $1 $ HsValBinds (EpAnn (glR $1) (AnnList anc p s) cs, noEpTok) val_binds)} } + ; return (sL1 $1 $ HsValBinds (EpAnn (glR $1) (AnnList la p s) cs, noEpTok) val_binds)} } | '{' dbinds '}' {% acs (comb3 $1 $2 $3) (\loc cs -> (L loc - $ HsIPBinds (EpAnn (spanAsAnchor (comb3 $1 $2 $3)) (AnnList (Just$ glR $2) (ListBraces (epTok $1) (epTok $3)) []) cs, noEpTok) (IPBinds noExtField (reverse $ unLoc $2)))) } + $ HsIPBinds (EpAnn (spanAsAnchor (comb3 $1 $2 $3)) (AnnList (AnnListLayout$ glR $2) (ListBraces (epTok $1) (epTok $3)) []) cs, noEpTok) (IPBinds noExtField (reverse $ unLoc $2)))) } | vocurly dbinds close {% acs (gl $2) (\loc cs -> (L loc - $ HsIPBinds (EpAnn (glR $1) (AnnList (Just $ glR $2) ListNone []) cs, noEpTok) (IPBinds noExtField (reverse $ unLoc $2)))) } + $ HsIPBinds (EpAnn (glR $1) (AnnList (AnnListLayout $ glR $2) ListNone []) cs, noEpTok) (IPBinds noExtField (reverse $ unLoc $2)))) } wherebinds :: { Maybe (Located (HsLocalBinds GhcPs, Maybe EpAnnComments )) } @@ -3542,11 +3542,11 @@ guardquals1 :: { Located [LStmt GhcPs (LHsExpr GhcPs)] } altslist(PATS) :: { forall b. DisambECP b => PV (LocatedA ([LMatch GhcPs (LocatedA b)], AnnList)) } : '{' alts(PATS) '}' { $2 >>= \ $2 -> amsA' (sLL $1 $> (reverse (snd $ unLoc $2), - (AnnList (Just $ glR $2) (ListBraces (epTok $1) (epTok $3)) (fst $ unLoc $2)))) } + (AnnList (AnnListLayout $ glR $2) (ListBraces (epTok $1) (epTok $3)) (fst $ unLoc $2)))) } | vocurly alts(PATS) close { $2 >>= \ $2 -> amsA' (L (getLoc $2) (reverse (snd $ unLoc $2), - (AnnList (Just $ glR $2) ListNone (fst $ unLoc $2)))) } - | '{' '}' { amsA' (sLL $1 $> ([], (AnnList Nothing (ListBraces (epTok $1) (epTok $2)) []))) } + (AnnList (AnnListLayout $ glR $2) ListNone (fst $ unLoc $2)))) } + | '{' '}' { amsA' (sLL $1 $> ([], (AnnList AnnListNoLayout (ListBraces (epTok $1) (epTok $2)) []))) } | vocurly close { return $ noLocA ([], noAnn) } alts(PATS) :: { forall b. DisambECP b => PV (Located ([EpToken ";"],[LMatch GhcPs (LocatedA b)])) } @@ -3656,10 +3656,10 @@ apat : aexp {% (checkPattern <=< runPV) (unECP $1) } stmtlist :: { forall b. DisambECP b => PV (LocatedA (AnnList, Located [LocatedA (Stmt GhcPs (LocatedA b))])) } : '{' stmts '}' { $2 >>= \ $2 -> - amsA' (sLL $1 $> (AnnList (Just (spanAsAnchor $ stmtsLoc $2)) (ListBraces (epTok $1) (epTok $3)) (fromOL $ fst $ unLoc $2) + amsA' (sLL $1 $> (AnnList (AnnListLayout (spanAsAnchor $ stmtsLoc $2)) (ListBraces (epTok $1) (epTok $3)) (fromOL $ fst $ unLoc $2) , sL1 $2 $ reverse $ snd $ unLoc $2))} | vocurly stmts close { $2 >>= \ $2 -> - amsA' (L (stmtsLoc $2) (AnnList (Just (spanAsAnchor $ stmtsLoc $2)) ListNone (fromOL $ fst $ unLoc $2) + amsA' (L (stmtsLoc $2) (AnnList (AnnListLayout (spanAsAnchor $ stmtsLoc $2)) ListNone (fromOL $ fst $ unLoc $2) , sL1 $2 $ reverse $ snd $ unLoc $2))} -- do { ;; s ; s ; ; s ;; } @@ -4630,9 +4630,6 @@ glEEz !x !y = if isZeroWidthSpan (getHasLoc y) then spanAsAnchor (getHasLoc x) else spanAsAnchor $ comb2 x y -glRM :: Located a -> Maybe EpaLocation -glRM (L !l _) = Just $ spanAsAnchor l - n2l :: LocatedN a -> LocatedA a n2l (L !la !a) = L (l2l la) a ===================================== compiler/GHC/Parser/Annotation.hs ===================================== @@ -31,10 +31,6 @@ module GHC.Parser.Annotation ( SrcSpanAnnA, SrcSpanAnnN, -- ** Annotation data types used in 'GenLocated' - - AnnList(..), AnnListBrackets(..), - AnnParen(..), - AnnCType(..),AnnWarningTxt(..),AnnOverlap(..),AnnAnnDecl(..),AnnPragSCC(..), NameAnn(..), NameAdornment(..), NoEpAnns(..), @@ -43,6 +39,12 @@ module GHC.Parser.Annotation ( addTrailingAnnToA, addTrailingCommaToN, noTrailingN, + -- ** Annotation data types used in TTG extension points + + AnnList(..), AnnListBrackets(..), AnnListLayout(..), + AnnParen(..), + AnnCType(..),AnnWarningTxt(..),AnnOverlap(..),AnnAnnDecl(..),AnnPragSCC(..), + -- ** Utilities for converting between different 'GenLocated' when -- ** we do not care about the annotations. l2l, la2la, @@ -513,7 +515,7 @@ instance Outputable TrailingAnn where -- AZ: goal: only used when there is layout, so vertical alignment matters data AnnList = AnnList { - al_anchor :: !(Maybe EpaLocation), -- ^ start point of a list having layout + al_layout :: !AnnListLayout, al_brackets :: !AnnListBrackets, al_semis :: [EpToken ";"] -- decls } deriving (Data,Eq) @@ -523,6 +525,18 @@ data AnnListBrackets | ListNone deriving (Data,Eq) +-- | How the extent of a list was delimited in the source. +data AnnListLayout + = AnnListBraces -- ^ Explicit @{ ; }@ written by the user. The tokens + -- live in 'al_brackets' and 'al_semis'. + | AnnListLayout !EpaLocation + -- ^ The lexer opened an implicit layout context. + -- The 'EpaLocation' is the @vocurly@ token (or, for + -- MultiWayIf, the leading @|@), whose start column is + -- the layout column chosen by 'new_layout_context'. + | AnnListNoLayout -- ^ Neither: an Empty or compiler-generated list. + deriving (Data, Eq) + -- --------------------------------------------------------------------- -- Annotations for parenthesised elements, such as tuples, lists -- --------------------------------------------------------------------- @@ -993,7 +1007,10 @@ instance NoAnn NoEpAnns where noAnn = NoEpAnns instance NoAnn AnnList where - noAnn = AnnList Nothing ListNone noAnn + noAnn = AnnList noAnn ListNone noAnn + +instance NoAnn AnnListLayout where + noAnn = AnnListNoLayout instance NoAnn NameAnn where noAnn = NameAnnTrailing [] @@ -1094,6 +1111,11 @@ instance Outputable AnnListBrackets where ppr (ListBraces o c) = text "ListBraces" <+> ppr o <+> ppr c ppr ListNone = text "ListNone" +instance Outputable AnnListLayout where + ppr AnnListBraces = text "AnnListBraces" + ppr (AnnListLayout l) = text "AnnListLayout" <+> ppr l + ppr AnnListNoLayout = text "AnnListNoLayout" + instance Outputable AnnCType where ppr (AnnCType o c l ca) = text "AnnCType" <+> ppr o <+> ppr c <+> ppr l ===================================== compiler/GHC/Parser/PostProcess.hs ===================================== @@ -466,7 +466,7 @@ add_where w@(EpTok (EpaSpan (RealSrcSpan rs _))) (EpAnn a al cs) cs2 = (EpAnn (widenAnchorT a w) al (cs Semi.<> cs2), w) | otherwise = (EpAnn (patch_anchor rs a) - (al { al_anchor = (fmap (patch_anchor rs) (al_anchor al))}) + (al { al_layout = patch_layout (al_layout al)}) (cs Semi.<> cs2), w) add_where _ _ _ = panic "add_where" -- EpaDelta should only be used for transformations @@ -484,6 +484,12 @@ patch_anchor r1 (EpaSpan (RealSrcSpan r0 mb)) = EpaSpan (RealSrcSpan r mb) r = if srcSpanStartLine r0 < 0 then r1 else r0 patch_anchor _ (EpaSpan ss) = EpaSpan ss +-- If the decl list for where binds is empty, the anchor ends up +-- invalid. Explicitly mark it as not having layout +patch_layout :: AnnListLayout -> AnnListLayout +patch_layout (AnnListLayout _) = AnnListNoLayout +patch_layout lo = lo + -- | The anchor for a stmtlist is based on either the location or -- the first semicolon annotion. stmtsAnchor :: Located (OrdList (EpToken tok),a) -> Maybe EpaLocation ===================================== testsuite/tests/ghc-api/exactprint/T22919.stderr ===================================== @@ -70,7 +70,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/ghc-api/exactprint/ZeroWidthSemi.stderr ===================================== @@ -82,7 +82,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/module/mod185.stderr ===================================== @@ -97,7 +97,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/parser/should_compile/DumpParsedAst.stderr ===================================== @@ -2223,7 +2223,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/parser/should_compile/DumpParsedAstComments.stderr ===================================== @@ -90,7 +90,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -213,7 +213,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -291,7 +291,7 @@ ((,) (Right (AnnList - (Just + (AnnListLayout (EpaSpan { DumpParsedAstComments.hs:16:3 })) (ListNone) [])) @@ -361,7 +361,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/parser/should_compile/DumpRenamedAst.stderr ===================================== @@ -30,7 +30,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/parser/should_compile/DumpSemis.stderr ===================================== @@ -261,7 +261,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -333,7 +333,7 @@ ((,) (Right (AnnList - (Just + (AnnListLayout (EpaSpan { DumpSemis.hs:(11,3)-(12,3) })) (ListNone) [])) @@ -364,7 +364,7 @@ ((,) (Right (AnnList - (Just + (AnnListLayout (EpaSpan { DumpSemis.hs:11:8-13 })) (ListBraces (EpTok (EpaSpan { DumpSemis.hs:11:6 })) @@ -555,7 +555,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -627,7 +627,7 @@ ((,) (Right (AnnList - (Just + (AnnListLayout (EpaSpan { DumpSemis.hs:(16,5)-(18,5) })) (ListBraces (EpTok (EpaSpan { DumpSemis.hs:16:3 })) @@ -808,7 +808,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -880,7 +880,7 @@ ((,) (Right (AnnList - (Just + (AnnListLayout (EpaSpan { DumpSemis.hs:22:12-28 })) (ListBraces (EpTok (EpaSpan { DumpSemis.hs:22:10 })) @@ -1017,7 +1017,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -1122,7 +1122,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -1229,7 +1229,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -1731,7 +1731,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -1857,7 +1857,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -1936,7 +1936,7 @@ (EpAnn (EpaSpan { DumpSemis.hs:34:13-31 }) (AnnList - (Just + (AnnListLayout (EpaSpan { DumpSemis.hs:34:18-30 })) (ListBraces (EpTok (EpaSpan { DumpSemis.hs:34:13 })) @@ -1984,7 +1984,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -2097,7 +2097,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -2222,7 +2222,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -2333,7 +2333,7 @@ ((,) (FromSource) (AnnList - (Just + (AnnListLayout (EpaSpan { DumpSemis.hs:(38,6)-(43,13) })) (ListBraces (EpTok (EpaSpan { DumpSemis.hs:38:4 })) ===================================== testsuite/tests/parser/should_compile/KindSigs.stderr ===================================== @@ -1000,7 +1000,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -1719,7 +1719,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/parser/should_compile/T15279.stderr ===================================== @@ -8,14 +8,15 @@ (EpAnn (EpaSpan { T15279.hs:1:1 }) (AnnsModule - (NoEpTok) + (EpTok + (EpaSpan { <no location info> })) (EpTok (EpaSpan { T15279.hs:3:1-6 })) (EpTok (EpaSpan { T15279.hs:3:15-19 })) ((,,) - (NoEpTok) - (NoEpTok) + (EpTok (EpaSpan { <no location info> })) + (EpTok (EpaSpan { <no location info> })) []) [] [] @@ -100,7 +101,8 @@ (EpaComments [])) (HsTyVar - (NoEpTok) + (EpTok + (EpaSpan { <no location info> })) (NotPromoted) (L (EpAnn @@ -118,7 +120,8 @@ (EpaComments [])) (HsTyVar - (NoEpTok) + (EpTok + (EpaSpan { <no location info> })) (NotPromoted) (L (EpAnn @@ -152,7 +155,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -182,7 +185,8 @@ (Prefix) (NoSrcStrict) (AnnFunRhs - (NoEpTok) + (EpTok + (EpaSpan { <no location info> })) [] [])) (L @@ -258,7 +262,8 @@ (Prefix) (NoSrcStrict) (AnnFunRhs - (NoEpTok) + (EpTok + (EpaSpan { <no location info> })) [] [])) (L @@ -334,7 +339,8 @@ (Prefix) (NoSrcStrict) (AnnFunRhs - (NoEpTok) + (EpTok + (EpaSpan { <no location info> })) [] [])) (L ===================================== testsuite/tests/parser/should_compile/T20718.stderr ===================================== @@ -104,7 +104,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/parser/should_compile/T20846.stderr ===================================== @@ -94,7 +94,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/printer/Test20297.stdout ===================================== @@ -70,7 +70,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -161,8 +161,7 @@ (EpAnn (EpaSpan { <no location info> }) (AnnList - (Just - (EpaSpan { Test20297.hs:7:3-7 })) + (AnnListNoLayout) (ListNone) []) (EpaComments @@ -201,7 +200,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -286,7 +285,7 @@ (EpAnn (EpaSpan { Test20297.hs:(10,3)-(11,26) }) (AnnList - (Just + (AnnListLayout (EpaSpan { Test20297.hs:11:9-26 })) (ListNone) []) @@ -324,7 +323,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -396,7 +395,7 @@ ((,) (Right (AnnList - (Just + (AnnListLayout (EpaSpan { Test20297.hs:11:22-26 })) (ListNone) [])) @@ -513,7 +512,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -598,8 +597,7 @@ (EpAnn (EpaSpan { <no location info> }) (AnnList - (Just - (EpaSpan { Test20297.ppr.hs:5:3-7 })) + (AnnListNoLayout) (ListNone) []) (EpaComments @@ -632,7 +630,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -717,7 +715,7 @@ (EpAnn (EpaSpan { Test20297.ppr.hs:(8,3)-(9,24) }) (AnnList - (Just + (AnnListLayout (EpaSpan { Test20297.ppr.hs:9:7-24 })) (ListNone) []) @@ -749,7 +747,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -821,7 +819,7 @@ ((,) (Right (AnnList - (Just + (AnnListLayout (EpaSpan { Test20297.ppr.hs:9:20-24 })) (ListNone) [])) ===================================== testsuite/tests/printer/Test24533.stdout ===================================== @@ -534,7 +534,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -1121,7 +1121,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== utils/check-exact/ExactPrint.hs ===================================== @@ -231,7 +231,7 @@ setAnchorAn (L (EpAnn _ an _) a) anc ts cs = (L (EpAnn anc (setTrailing an ts) c -- `debug` ("setAnchorAn: anc=" ++ showAst anc) setAnchorEpaL :: EpAnn AnnList -> EpaLocation -> [TrailingAnn] -> EpAnnComments -> EpAnn AnnList -setAnchorEpaL (EpAnn _ an _) anc ts cs = EpAnn anc (setTrailing (an {al_anchor = Nothing}) ts) cs +setAnchorEpaL (EpAnn _ an _) anc ts cs = EpAnn anc (setTrailing (an {al_layout = AnnListNoLayout}) ts) cs -- --------------------------------------------------------------------- @@ -2672,8 +2672,8 @@ instance ExactPrint (HsLocalBinds GhcPs) where exact (HsValBinds (an0, w) valbinds) = do w' <- markEpToken w -- 'where' - case al_anchor $ anns an0 of - Just anc -> do + case al_layout $ anns an0 of + AnnListLayout anc -> do when (not $ isEmptyValBinds valbinds) $ setExtraDP (Just anc) _ -> return () @@ -2684,7 +2684,7 @@ instance ExactPrint (HsLocalBinds GhcPs) where Nothing -> return an1 Just (ss,dp) -> do setExtraDPReturn Nothing - return $ an1 { anns = (anns an1) { al_anchor = Just (EpaDelta ss dp []) }} + return $ an1 { anns = (anns an1) { al_layout = AnnListLayout (EpaDelta ss dp []) }} return (HsValBinds (an2, w') valbinds') exact (HsIPBinds (an,w) bs) = do ===================================== utils/check-exact/Main.hs ===================================== @@ -521,8 +521,8 @@ changeLocalDecls libdir (L l p) = do let oldDecls' = captureLineSpacing oldDecls let (VbSig o:oldBinds) = map wrapValBind oldDecls' o' = setEntryDP o (DifferentLine 2 0) - let (EpAnn anc (AnnList (Just _) a b) cs) = van - let van' = (EpAnn anc (AnnList (Just (EpaDelta noSrcSpan (DifferentLine 1 4) [])) a b) cs) + let (EpAnn anc (AnnList (AnnListLayout _) a b) cs) = van + let van' = (EpAnn anc (AnnList (AnnListLayout (EpaDelta noSrcSpan (DifferentLine 1 4) [])) a b) cs) let binds' = (HsValBinds (van',w) (ValBinds noExtField (VbSig sig':VbBind decl':VbSig o':oldBinds))) return (L lm (Match an mln pats (GRHSs emptyComments rhs binds'))) @@ -548,7 +548,7 @@ changeLocalDecls2 libdir (L l p) = do let anc = (EpaDelta noSrcSpan (DifferentLine 1 2) []) let anc2 = (EpaDelta noSrcSpan (DifferentLine 1 4) []) let an = (EpAnn anc - (AnnList (Just anc2) ListNone + (AnnList (AnnListLayout anc2) ListNone []) emptyComments, EpTok (EpaDelta noSrcSpan (SameLine 0) [])) let decls = [VbSig sig', VbBind decl'] ===================================== utils/check-exact/Transform.hs ===================================== @@ -1046,7 +1046,7 @@ newWhereAnnotation ww = (an, w) WithWhere -> EpTok (EpaDelta noSrcSpan (SameLine 0) []) WithoutWhere -> noEpTok an = EpAnn anc - (AnnList (Just anc2) ListNone []) + (AnnList (AnnListLayout anc2) ListNone []) emptyComments -- --------------------------------------------------------------------- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9f48a5b908f572847bc8ba4657c9f5a… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9f48a5b908f572847bc8ba4657c9f5a… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc][master] 5 commits: Improve the `mhu-closure` makefile
by Marge Bot (＠marge-bot) 25 Sep '26

25 Sep '26

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 1abef1ef by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Improve the `mhu-closure` makefile - - - - - a79a68ea by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Make `ghci-multi` hide all unneeded packages - - - - - d6e72450 by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Improve the definition of the home unit closure property - - - - - c9a2766d by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Re-implement the home unit closure check Compared to the previous implementation, the new one has the following advantages: * It is correct. - It distinguishes between units that have the same unit ID but different ABI hashes. - When `-hide-all-packages` is not used, it considers as home unit dependencies also units that are made implicitly available because they are in the package database. * It seems to be faster in usual settings. - In particular, it does not have a preparation phase in which it merges the dependency information from all home units, so that its running time does not grow linearly with the size of the package database in normal Cabal scenarios. * It is (hopefully) clearer. * It is better documented. - - - - - fa96acf8 by Wolfgang Jeltsch at 2026-09-25T17:02:07-04:00 Remove erroneous GHC flag in `hadrian-multi` The flag was `-Werror=-Wno-error=incomplete-record-selectors`. Its purpose was to permit incomplete record selectors, but because of the illegal combination of `-Werror=` and `-Wno-error` it was ignored, without any negative consequences. - - - - - 9 changed files: - .gitlab-ci.yml - compiler/GHC/Driver/Downsweep.hs - compiler/GHC/Driver/Errors/Ppr.hs - compiler/GHC/Driver/Errors/Types.hs - compiler/GHC/Unit/Env.hs - hadrian/ghci-multi-cabal.in - testsuite/tests/driver/multipleHomeUnits/mhu-closure/Makefile - testsuite/tests/driver/multipleHomeUnits/mhu-closure/mhu-closure.stderr - testsuite/tests/driver/multipleHomeUnits/mhu-closure/mhu-closure.stdout Changes: ===================================== .gitlab-ci.yml ===================================== @@ -497,12 +497,7 @@ hadrian-multi: # workaround for docker permissions - sudo chown ghc:ghc -R . variables: - GHC_FLAGS: "-Werror=-Wno-error=incomplete-record-selectors -Wwarn=deprecations -Wwarn=unused-imports" - # -Wno-error=incomplete-record-selectors is present because -Wall now - # includes -Wincomplete-record-selectors, and hadrian-multi has many, many - # warnings about incomplete record selectors. A better fix would be to - # remove the use of incomplete record selectors, since each of them represents - # a potential crash. + GHC_FLAGS: "-Wwarn=deprecations -Wwarn=unused-imports" CONFIGURE_ARGS: --enable-bootstrap-with-devel-snapshot tags: - x86_64-linux ===================================== compiler/GHC/Driver/Downsweep.hs ===================================== @@ -6,6 +6,8 @@ {-# LANGUAGE BlockArguments #-} {-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wno-invalid-haddock #-} + -- | See Note [The ModuleGraph] module GHC.Driver.Downsweep ( downsweep @@ -54,8 +56,6 @@ import GHC.Runtime.Context import Language.Haskell.Syntax.ImpExp import GHC.Types.UnresolvedImport -import GHC.Data.Graph.Directed -import GHC.Data.FastString import GHC.Data.Maybe ( expectJust ) import qualified GHC.Data.Maybe as M import GHC.Data.OsPath ( OsPath, unsafeEncodeUtf ) @@ -71,12 +71,15 @@ import GHC.Utils.Logger import GHC.Utils.Fingerprint import GHC.Utils.TmpFs import GHC.Utils.Constants +import GHC.Utils.Monad (concatMapM) +import GHC.Utils.Monad.State.Strict import GHC.Types.Error import GHC.Types.Target import GHC.Types.SourceFile import GHC.Types.SourceError import GHC.Types.SrcLoc +import GHC.Types.Unique.Set import GHC.Types.Unique.Map import GHC.Types.PkgQual import GHC.Types.Basic @@ -91,9 +94,12 @@ import GHC.Unit.Module.Graph import GHC.Unit.Module.Deps import qualified GHC.Unit.Home.Graph as HUG import GHC.Unit.Module.Stage +import GHC.Unit.External.Index (UnitAbiHash) import Data.Either ( partitionEithers, lefts ) +import Data.Map (Map) import qualified Data.Map as Map +import Data.Set (Set) import qualified Data.Set as Set import Control.Concurrent.MVar @@ -101,7 +107,7 @@ import Control.Monad import Control.Monad.Trans.Except ( ExceptT(..), runExceptT, throwE ) import qualified Control.Monad.Catch as MC import Data.Maybe -import Data.List (partition) +import Data.List (sort, partition) import Data.Time import Data.List (unfoldr) import Data.Bifunctor (first, bimap) @@ -864,7 +870,7 @@ getRootSummary excl_mods summ_cache imports_cache hsc_env target mkPlainErrorMsgEnvelope noSrcSpan (DriverFileNotFound offset_file) | TargetModule modl <- targetId = do - let root_imp = (generatedImport FromTarget (L rootLoc modl)) + let root_imp = (generatedImport FromTarget (L noSrcSpan modl)) { ui_pkg_qual = ThisPkg (homeUnitId home_unit) } maybe_summary <- summariseModule hsc_env home_unit summ_cache imports_cache root_imp maybe_buf excl_mods @@ -875,7 +881,6 @@ getRootSummary excl_mods summ_cache imports_cache hsc_env target where Target {targetId, targetContents = maybe_buf, targetUnitId = uid} = target home_unit = ue_unitHomeUnit uid (hsc_unit_env hsc_env) - rootLoc = mkGeneralSrcSpan (fsLit "<command line>") dflags = homeUnitEnv_dflags (ue_findHomeUnitEnv uid (hsc_unit_env hsc_env)) -- | Execute 'getRootSummary' for the 'Target's using the parallelism pipeline @@ -933,52 +938,171 @@ rootSummariesParallel n_jobs hsc_env diag_wrapper msg get_summary = do -- * Check/validate properties and error out -------------------------------------------------------------------------------- --- | This function checks then important property that if both p and q are home units --- then any dependency of p, which transitively depends on q is also a home unit. +-- | Checks whether the given 'UnitEnv' has the closure property. -- --- See Note [Multiple Home Units], section 'Closure Property'. -checkHomeUnitsClosed :: UnitEnv -> [DriverMessages] -checkHomeUnitsClosed ue - | Set.null bad_unit_ids = [] - | otherwise = [singleMessage $ mkPlainErrorMsgEnvelope rootLoc $ DriverHomePackagesNotClosed (Set.toList bad_unit_ids)] +-- See the section “Closure Property” in @Note [Multiple Home Units]@ for the +-- definition of the closure property and +-- @Note [Home unit closure property check]@ below for a discussion of the +-- algorithm used for this check, its justification, and a potential +-- alternative. +checkHomeUnitsClosed :: UnitEnv -> [DriverMessages] +checkHomeUnitsClosed unit_env + | null offenders = [] + | otherwise = [ + singleMessage $ + mkPlainErrorMsgEnvelope noSrcSpan $ + DriverHomePackagesNotClosed (sort offenders) + ] where - home_id_set = HUG.allUnits $ ue_home_unit_graph ue - bad_unit_ids = upwards_closure Set.\\ home_id_set {- Remove all home units reached, keep only bad nodes -} - rootLoc = mkGeneralSrcSpan (fsLit "<command line>") - downwards_closure :: Graph (Node UnitId UnitId) - downwards_closure = graphFromEdgedVerticesUniq graphNodes + -- | The 'UnitId' and 'HomeUnitEnv' of each home unit. + home_unit_data :: [(UnitId, HomeUnitEnv)] + home_unit_data = HUG.unitEnv_assocs (ue_home_unit_graph unit_env) + + -- | The 'UnitId's of all home units. + home_units :: UniqSet UnitId + home_units = mkUniqSet (map fst home_unit_data) + + -- | All offending dependencies. A dependency of a unit /u/ on a unit /v/ is + -- offending exactly if /u/ is an external unit reachable from a home unit + -- and /v/ is a home unit. Each such dependency is represented in this list + -- by the pair of the 'UnitId' of /u/ and the 'UnitId' of /v/. + offenders :: [(UnitId, UnitId)] + offenders + = evalState (collect (map (homeUnitEnv_units . snd) home_unit_data)) + emptyUniqMap + where - inverse_closure = graphReachability $ transposeG downwards_closure + -- | Collects offending dependencies. + collect :: [UnitState] + -- ^ The 'UnitState's of the home units from which to traverse + -- the dependency graph. + -> State (UniqMap UnitId (Set UnitAbiHash)) [(UnitId, UnitId)] + -- ^ A stateful computation that collects offending dependencies + -- that have not yet been found. It uses its state, which is an + -- efficent representation of a set of 'GlobalUnitKey's, to + -- keep track of which units have already been considered as + -- sources of offending dependencies. + collect = concatMapM $ \ unit_state -> + collect_for_home_unit + (unitInfoMap unit_state) + (map (toUnitId . fst) $ explicitUnits $ unit_state) + where - upwards_closure = Set.fromList $ map node_key $ allReachableMany inverse_closure [DigraphNode uid uid [] | uid <- Set.toList home_id_set] + -- | Collects offending dependencies that are reachable from a particular + -- home unit. + collect_for_home_unit + :: UnitInfoMap + -- ^ The 'UnitInfoMap' of the home unit. + -> [UnitId] + -- ^ The 'UnitId's of the units from which to traverse the dependency + -- graph. + -> State (UniqMap UnitId (Set UnitAbiHash)) [(UnitId, UnitId)] + -- ^ A stateful computation that collects offending dependencies that + -- have not yet been found. It uses its state, which is an efficent + -- representation of a set of 'GlobalUnitKey's, to keep track of + -- which units have already been considered as sources of offending + -- dependencies. + collect_for_home_unit _ [] + = return [] + collect_for_home_unit unit_info_map (current_unit : remaining_units) = do + let + + -- | The 'UnitInfo' of the current unit. + unit_info :: UnitInfo + unit_info + = fromMaybe (pprPanic unit_not_found_msg (ppr current_unit)) $ + lookupUniqMap unit_info_map current_unit + where + + -- | The message that says that a unit was not found. + unit_not_found_msg :: String + unit_not_found_msg = "Unit not found during closure property check" + + -- | The ABI hash of the current unit. + unit_abi_hash :: UnitAbiHash + unit_abi_hash = unitAbiHash unit_info + + has_been_processed <- gets $ maybe False (Set.member unit_abi_hash) . + (`lookupUniqMap` current_unit) + if has_been_processed + then collect_for_home_unit unit_info_map remaining_units + else do + modify $ \ processed -> addToUniqMap_C Set.union + processed + current_unit + (Set.singleton unit_abi_hash) + let + + -- | The 'UnitId's of the units that the current unit depends on. + needed_units :: [UnitId] + needed_units = unitDepends unit_info + + -- | The offending dependencies of the current unit. + current_offenders :: [(UnitId, UnitId)] + current_offenders + | current_unit `elementOfUniqSet` home_units + = [] + | otherwise + = map ((,) current_unit) $ + nonDetEltsUniqSet $ + mkUniqSet needed_units `intersectUniqSets` home_units + + remaining_offenders <- collect_for_home_unit unit_info_map $ + needed_units ++ remaining_units + return $ current_offenders ++ remaining_offenders - all_unit_direct_deps :: UniqMap UnitId (Set.Set UnitId) - all_unit_direct_deps - = HUG.unitEnv_foldWithKey go emptyUniqMap $ ue_home_unit_graph ue - where - go rest this this_uis = - plusUniqMap_C Set.union - (addToUniqMap_C Set.union external_depends this (Set.fromList $ this_deps)) - rest - where - external_depends = mapUniqMap (Set.fromList . unitDepends) (unitInfoMap this_units) - this_units = homeUnitEnv_units this_uis - this_deps = [ toUnitId unit | (unit,Just _) <- explicitUnits this_units] - - graphNodes :: [Node UnitId UnitId] - graphNodes = go Set.empty home_id_set - where - go done todo - = case Set.minView todo of - Nothing -> [] - Just (uid, todo') - | Set.member uid done -> go done todo' - | otherwise -> case lookupUniqMap all_unit_direct_deps uid of - Nothing -> pprPanic "uid not found" (ppr (uid, all_unit_direct_deps)) - Just depends -> - let todo'' = (depends Set.\\ done) `Set.union` todo' - in DigraphNode uid uid (Set.toList depends) : go (Set.insert uid done) todo'' +{- + +Note [Home unit closure property check] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Per the definition in Note [Multiple Home Units], a unit environment has the +closure property exactly if there are no paths /h/₁ →* /e/ →* /h/₂ in the +dependency graph, where /h/₁ and /h/₂ are home units and /e/ is an external +unit. However, the algorithm used by 'checkHomeUnitsClosed' searches for +so-called offending dependencies, which are dependencies /e/ → /h/₂ that are +part of a path /h/₁ →* /e/ → /h/₂ in the dependency graph. To see that this is a +viable approach, consider the following: + + * A path /h/₁ →* /e/ → /h/₂ is also a path /h/₁ →* /e/ →* /h/₂. + + * For each path /h/₁ →* /e/ →* /h/₂, there exists a path /h/₁ →* /e/′ → /h/₂′, + where /e/′ is an external unit and /h/₂′ is a home unit. Such a path can be + constructed by taking as /h/₂′ the first home unit on the path /e/ →* /h/₂ + and as /e/′ the, necessarily external, unit preceding it. + +Concretely, the algorithm picks one home unit after the other, determines what +units it directly depends on, and, starting from them, follows unit dependencies +to search for offending dependencies. It does not follow dependencies that have +been followed before, possibly when processing another home unit. To achieve +this, the algorithm tracks, across home units, from which units it has already +followed dependencies. For this tracking, it identifies each unit by a 'UnitId' +and an ABI hash. Using only a 'UnitId' would not work, because 'UnitId's are not +always globally unique. Also using only an ABI hash is not an option, because an +ABI hash is not necessarily an ABI hash: it can also be the string @"inline"@. + +The correctness of this algorithm rests on the, likely correct, assumption that, +among the units mentioned in the 'UnitState' of a particular home unit, any unit +can be uniquely identified by its 'UnitId' and thus 'UnitId' clashes can only +occur across the 'UnitState's of different home units. + +An alternative approach to finding offending dependencies would be to follow +dependencies starting from all units that /any/ home unit directly depends on +instead of considering the different home units separately. A corresponding +algorithm could in principle find the dependencies of a particular unit +independently of any home unit by fetching the 'UnitInfo' of that unit from the +'GlobalUnitInfoMap'. However, for such a lookup the algorithm would need not +only the 'UnitId' but also the ABI hash of the unit in question. Therefore, +whenever following a dependency of a unit /u/ on a unit /v/, it would have to +determine the ABI hash of /v/, so that it could later look up /v/’s +dependencies. The ABI hashes of all units that /u/ depends on should be +available in the 'unitAbiDepends' field of /u/’s 'UnitInfo'. However, at the +time of writing, 'unitAbiDepends' never contained anything other than the empty +list during GHC test runs, which indicated that this alternative solution was +impossible to realize. + +-} -------------------------------------------------------------------------------- -- * Enable Code Gen for Template Haskell @@ -1763,7 +1887,7 @@ data NodeRes v -- -- See also Note [Downsweep Control Flow and Caching] dfsBuild :: (Ord k, Monad m) - => Maybe (Map.Map k (NodeRes v)) + => Maybe (Map k (NodeRes v)) -- ^ Base map, existing results. We won't re-expand any of the nodes -- already present in this map. -> [n] @@ -1773,7 +1897,7 @@ dfsBuild :: (Ord k, Monad m) -> (n -> m (NodeRes (v,[n]))) -- ^ Expand this node into its payload result and into the list of -- children nodes to visit next. - -> m (Map.Map k (NodeRes v)) + -> m (Map k (NodeRes v)) -- ^ The result accumulates the payload of expanding the root nodes -- and all nodes transitively reachable from those roots. dfsBuild base_map roots key expand = go roots (fromMaybe Map.empty base_map) ===================================== compiler/GHC/Driver/Errors/Ppr.hs ===================================== @@ -235,10 +235,17 @@ instance Diagnostic DriverMessage where "but no output will be generated.") $$ (text "There is no module named" <+> quotes (ppr mod_name) <> text ".")) - DriverHomePackagesNotClosed needed_unit_ids - -> mkSimpleDecorated $ vcat ([text "Home units are not closed." - , text "It is necessary to also load the following units:" ] - ++ map (\uid -> text "-" <+> ppr uid) needed_unit_ids) + DriverHomePackagesNotClosed offending_dependencies + -> mkSimpleDecorated $ + hang (text "Some units are not loaded but depend on loaded units.") + 4 + (vcat (map pprDependency offending_dependencies)) + where + + pprDependency :: (UnitId, UnitId) -> SDoc + pprDependency (external_unit, home_unit) + = ppr external_unit <+> arrow <+> ppr home_unit + DriverInterfaceError reason -> diagnosticMessage (ifaceDiagnosticOpts opts) reason DriverInconsistentDynFlags msg ===================================== compiler/GHC/Driver/Errors/Types.hs ===================================== @@ -369,7 +369,7 @@ data DriverMessage where DriverRedirectedNoMain :: !ModuleName -> DriverMessage - DriverHomePackagesNotClosed :: ![UnitId] -> DriverMessage + DriverHomePackagesNotClosed :: ![(UnitId, UnitId)] -> DriverMessage DriverInterfaceError :: !IfaceMessage -> DriverMessage ===================================== compiler/GHC/Unit/Env.hs ===================================== @@ -443,13 +443,14 @@ The flow: Closure Property ---------------- -You must perform a clean cut of the dependency graph. +A unit environment must have the closure property: -> Any dependency which is not a home unit must not (transitively) depend on a home unit. + No used external unit depends on a home unit. -For example, if you have three packages p, q and r, then if p depends on q which -depends on r then it is illegal to load both p and r as home units but not q, -because q is a dependency of the home unit p which depends on another home unit r. +More concretely, a unit environment has the closure property exactly if no home +unit directly or indirectly depends on an external unit that directly or +indirectly depends on a home unit. 'GHC.Driver.Downsweep.checkHomeUnitsClosed' +checks whether a given unit environment indeed has this property. Offsetting Paths ---------------- ===================================== hadrian/ghci-multi-cabal.in ===================================== @@ -10,4 +10,4 @@ export TOOL_OUTPUT=.hadrian_ghci_multi/ghci_args # Replace newlines with spaces, as these otherwise break the ghci invocation on windows. CABFLAGS=-v0 "hadrian/build-cabal" multi --build-root=.hadrian_ghci_multi --flavour=ghc-in-ghci $HADRIAN_ARGS GHC_FLAGS="$GHC_FLAGS $(cat $TOOL_OUTPUT | tr '\n\r' ' ')" -$RUN_GHC --interactive $GHC_FLAGS $@ -fno-code -fwrite-interface -O0 +RTS -A128m +$RUN_GHC --interactive $GHC_FLAGS $@ -hide-all-packages -fno-code -fwrite-interface -O0 +RTS -A128m ===================================== testsuite/tests/driver/multipleHomeUnits/mhu-closure/Makefile ===================================== @@ -3,39 +3,47 @@ include $(TOP)/mk/boilerplate.mk include $(TOP)/mk/test.mk SETUP=../Setup -v0 +CONFIGURE=configure \ + $(CABAL_MINIMAL_BUILD) \ + --with-ghc='$(TEST_HC)' \ + --with-hc-pkg='$(GHC_PKG)' \ + --ghc-options='$(TEST_HC_OPTS)' \ + --package-db=../tmp.d +TEST_BUILD='$(TEST_HC)' $(TEST_HC_OPTS) -fhide-source-paths -fforce-recomp +ONLY_BASE=-hide-all-packages -package base -mhu-closure: clean - $(MAKE) -s --no-print-directory clean +mhu-closure: clean pkg-database + ! $(TEST_BUILD) -unit @unitP + ! $(TEST_BUILD) -unit @unitP -unit @unitQ + ! $(TEST_BUILD) -unit @unitP -unit @unitR + ! $(TEST_BUILD) -unit @unitP -unit @unitR1 + $(TEST_BUILD) -unit @unitP -unit @unitQ -unit @unitR + ! $(TEST_BUILD) -unit @unitP -unit @unitQ -unit @unitR1 + $(TEST_BUILD) $(ONLY_BASE) -unit @unitP + $(TEST_BUILD) $(ONLY_BASE) -unit @unitP -unit @unitQ + ! $(TEST_BUILD) $(ONLY_BASE) -unit @unitP -unit @unitR + ! $(TEST_BUILD) $(ONLY_BASE) -unit @unitP -unit @unitR1 + $(TEST_BUILD) $(ONLY_BASE) -unit @unitP -unit @unitQ -unit @unitR + $(TEST_BUILD) $(ONLY_BASE) -unit @unitP -unit @unitQ -unit @unitR1 + +.PHONY: pkg-database +pkg-database: '$(GHC_PKG)' init tmp.d '$(TEST_HC)' $(TEST_HC_OPTS) -v0 --make Setup - cd p && $(SETUP) clean - cd p && $(SETUP) configure $(CABAL_MINIMAL_BUILD) --ipid=p-0.1.0.0 --with-ghc='$(TEST_HC)' --with-hc-pkg='$(GHC_PKG)' --ghc-options='$(TEST_HC_OPTS)' --package-db=../tmp.d + cd p && $(SETUP) $(CONFIGURE) --ipid=p-0.1.0.0 cd p && $(SETUP) build cd p && $(SETUP) register --inplace - cd q && $(SETUP) configure $(CABAL_MINIMAL_BUILD) --ipid=q-0.1.0.0 --with-ghc='$(TEST_HC)' --with-hc-pkg='$(GHC_PKG)' --ghc-options='$(TEST_HC_OPTS)' --package-db=../tmp.d + cd q && $(SETUP) $(CONFIGURE) --ipid=q-0.1.0.0 cd q && $(SETUP) build cd q && $(SETUP) register --inplace - cd r && $(SETUP) configure $(CABAL_MINIMAL_BUILD) --ipid=r-0.1.0.0 --with-ghc='$(TEST_HC)' --with-hc-pkg='$(GHC_PKG)' --ghc-options='$(TEST_HC_OPTS)' --package-db=../tmp.d + cd r && $(SETUP) $(CONFIGURE) --ipid=r-0.1.0.0 cd r && $(SETUP) build cd r && $(SETUP) register --inplace - # This should work - '$(TEST_HC)' $(TEST_HC_OPTS) -fhide-source-paths -fforce-recomp -unit @unitP - # So should this - '$(TEST_HC)' $(TEST_HC_OPTS) -fhide-source-paths -fforce-recomp -unit @unitP -unit @unitQ - # So should this - '$(TEST_HC)' $(TEST_HC_OPTS) -fhide-source-paths -fforce-recomp -unit @unitP -unit @unitQ -unit @unitR - # This should error with a closure message - ! '$(TEST_HC)' $(TEST_HC_OPTS) -fhide-source-paths -fforce-recomp -unit @unitP -unit @unitR - # This should work, even though r1 is not in the package db - '$(TEST_HC)' $(TEST_HC_OPTS) -fhide-source-paths -fforce-recomp -unit @unitP -unit @unitQ -unit @unitR1 - # This should fail, even though r1 is not in the package db - ! '$(TEST_HC)' $(TEST_HC_OPTS) -fhide-source-paths -fforce-recomp -unit @unitP -unit @unitR1 +.PHONY: clean +clean: + $(RM) -r tmp.d Setup$(exeext) */dist* *.hi *.o */*.hi */*.o ifeq "$(CLEANUP)" "1" $(MAKE) -s --no-print-directory clean endif - -clean : - $(RM) -r tmp*.d inst-* *.o *.hi */*.o */*.hi */Setup$(exeext) */dist Setup$(exeext) - ===================================== testsuite/tests/driver/multipleHomeUnits/mhu-closure/mhu-closure.stderr ===================================== @@ -1,10 +1,28 @@ -<command line>: error: [GHC-03271] - Home units are not closed. - It is necessary to also load the following units: - - q-0.1.0.0 - -<command line>: error: [GHC-03271] - Home units are not closed. - It is necessary to also load the following units: - - q-0.1.0.0 +<no location info>: error: [GHC-03271] + Some units are not loaded but depend on loaded units. + q-0.1.0.0 -> p-0.1.0.0 + +<no location info>: error: [GHC-03271] + Some units are not loaded but depend on loaded units. + r-0.1.0.0 -> q-0.1.0.0 + +<no location info>: error: [GHC-03271] + Some units are not loaded but depend on loaded units. + q-0.1.0.0 -> p-0.1.0.0 + +<no location info>: error: [GHC-03271] + Some units are not loaded but depend on loaded units. + q-0.1.0.0 -> p-0.1.0.0 + +<no location info>: error: [GHC-03271] + Some units are not loaded but depend on loaded units. + r-0.1.0.0 -> q-0.1.0.0 + +<no location info>: error: [GHC-03271] + Some units are not loaded but depend on loaded units. + q-0.1.0.0 -> p-0.1.0.0 + +<no location info>: error: [GHC-03271] + Some units are not loaded but depend on loaded units. + q-0.1.0.0 -> p-0.1.0.0 ===================================== testsuite/tests/driver/multipleHomeUnits/mhu-closure/mhu-closure.stdout ===================================== @@ -1,3 +1,6 @@ +[1 of 3] Compiling P[p-0.1.0.0] +[2 of 3] Compiling Q[q-0.1.0.0] +[3 of 3] Compiling R[r-0.1.0.0] [1 of 1] Compiling P [1 of 2] Compiling P[p-0.1.0.0] [2 of 2] Compiling Q[q-0.1.0.0] View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/35bf6f4bcf06675565992725df62e8… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/35bf6f4bcf06675565992725df62e8… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 8 commits: Correct the documentation of `explicitUnits`
by Marge Bot (＠marge-bot) 25 Sep '26

25 Sep '26

Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC Commits: 53eead15 by Wolfgang Jeltsch at 2026-09-24T20:12:03-04:00 Correct the documentation of `explicitUnits` Resolves #27787. - - - - - 35bf6f4b by Simon Jakobi at 2026-09-24T20:12:49-04:00 Remove stale specHeader bullet from Note [Don't make fillers for constraint types] The Note said that Specialise.specHeader also calls mkAbsentFiller. abfc224a27c removed that call: the specialiser no longer drops dead arguments at all, see Note [Do not drop dead args from specialisations] in GHC.Core.Opt.Specialise. Assisted-by: Claude Fable 5.1 - - - - - 514d28cc by Wolfgang Jeltsch at 2026-09-25T13:11:36-04:00 Improve the `mhu-closure` makefile - - - - - 49e5112e by Wolfgang Jeltsch at 2026-09-25T13:11:36-04:00 Make `ghci-multi` hide all unneeded packages - - - - - 69e4d73f by Wolfgang Jeltsch at 2026-09-25T13:11:36-04:00 Improve the definition of the home unit closure property - - - - - ec357a2d by Wolfgang Jeltsch at 2026-09-25T13:11:36-04:00 Re-implement the home unit closure check Compared to the previous implementation, the new one has the following advantages: * It is correct. - It distinguishes between units that have the same unit ID but different ABI hashes. - When `-hide-all-packages` is not used, it considers as home unit dependencies also units that are made implicitly available because they are in the package database. * It seems to be faster in usual settings. - In particular, it does not have a preparation phase in which it merges the dependency information from all home units, so that its running time does not grow linearly with the size of the package database in normal Cabal scenarios. * It is (hopefully) clearer. * It is better documented. - - - - - f57edc3e by Wolfgang Jeltsch at 2026-09-25T13:11:36-04:00 Remove erroneous GHC flag in `hadrian-multi` The flag was `-Werror=-Wno-error=incomplete-record-selectors`. Its purpose was to permit incomplete record selectors, but because of the illegal combination of `-Werror=` and `-Wno-error` it was ignored, without any negative consequences. - - - - - ce087204 by Alan Zimmerman at 2026-09-25T13:11:37-04:00 EPA: Add specific layout field to AnnList Up to now AnnList has effectively served to represent lists of things having layout, regardless of whether they do or not. In Haskell, layout is optional in many places, as there is also an alternative syntax using braces and semi-colons, which is free-form. This commit introduces AnnListLayout, a data structure capturing this distinction. It is deliberately set up similarly to EpLayout, so that these two can be merged in time. The transition is done mechanically, where AnnListBraces is not used yet, the original Nothing case maps to AnnListNoLayout, and the Just case to AnnListLayout. Later commits will fine tune these against the actual parser layout. - - - - - 30 changed files: - .gitlab-ci.yml - compiler/GHC/Core/Opt/WorkWrap/Utils.hs - compiler/GHC/Driver/Downsweep.hs - compiler/GHC/Driver/Errors/Ppr.hs - compiler/GHC/Driver/Errors/Types.hs - compiler/GHC/Parser.y - compiler/GHC/Parser/Annotation.hs - compiler/GHC/Parser/PostProcess.hs - compiler/GHC/Unit/Env.hs - compiler/GHC/Unit/State.hs - hadrian/ghci-multi-cabal.in - testsuite/tests/driver/multipleHomeUnits/mhu-closure/Makefile - testsuite/tests/driver/multipleHomeUnits/mhu-closure/mhu-closure.stderr - testsuite/tests/driver/multipleHomeUnits/mhu-closure/mhu-closure.stdout - testsuite/tests/ghc-api/exactprint/T22919.stderr - testsuite/tests/ghc-api/exactprint/ZeroWidthSemi.stderr - testsuite/tests/module/mod185.stderr - testsuite/tests/parser/should_compile/DumpParsedAst.stderr - testsuite/tests/parser/should_compile/DumpParsedAstComments.stderr - testsuite/tests/parser/should_compile/DumpRenamedAst.stderr - testsuite/tests/parser/should_compile/DumpSemis.stderr - testsuite/tests/parser/should_compile/KindSigs.stderr - testsuite/tests/parser/should_compile/T15279.stderr - testsuite/tests/parser/should_compile/T20718.stderr - testsuite/tests/parser/should_compile/T20846.stderr - testsuite/tests/printer/Test20297.stdout - testsuite/tests/printer/Test24533.stdout - utils/check-exact/ExactPrint.hs - utils/check-exact/Main.hs - utils/check-exact/Transform.hs Changes: ===================================== .gitlab-ci.yml ===================================== @@ -497,12 +497,7 @@ hadrian-multi: # workaround for docker permissions - sudo chown ghc:ghc -R . variables: - GHC_FLAGS: "-Werror=-Wno-error=incomplete-record-selectors -Wwarn=deprecations -Wwarn=unused-imports" - # -Wno-error=incomplete-record-selectors is present because -Wall now - # includes -Wincomplete-record-selectors, and hadrian-multi has many, many - # warnings about incomplete record selectors. A better fix would be to - # remove the use of incomplete record selectors, since each of them represents - # a potential crash. + GHC_FLAGS: "-Wwarn=deprecations -Wwarn=unused-imports" CONFIGURE_ARGS: --enable-bootstrap-with-devel-snapshot tags: - x86_64-linux ===================================== compiler/GHC/Core/Opt/WorkWrap/Utils.hs ===================================== @@ -1367,13 +1367,8 @@ It's surprisingly subtle. application; see test `T27627f`. TL;DR: we play safe: we never make an absent filler for any /constraint-kinded/ type, -using `isPredTy` to decide. - - * `mkAbsentFiller` returns `Nothing` for any constraint type, so worker/wrapper - keeps the real argument. - - * `Specialise.specHeader` calls `mkAbsentFiller` too, so it likewise keeps the - dead dictionary argument rather than dropping it for a filler. +using `isPredTy` to decide: `mkAbsentFiller` returns `Nothing` for any constraint +type, so worker/wrapper keeps the real argument. Prior failed approaches ===================================== compiler/GHC/Driver/Downsweep.hs ===================================== @@ -6,6 +6,8 @@ {-# LANGUAGE BlockArguments #-} {-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wno-invalid-haddock #-} + -- | See Note [The ModuleGraph] module GHC.Driver.Downsweep ( downsweep @@ -54,8 +56,6 @@ import GHC.Runtime.Context import Language.Haskell.Syntax.ImpExp import GHC.Types.UnresolvedImport -import GHC.Data.Graph.Directed -import GHC.Data.FastString import GHC.Data.Maybe ( expectJust ) import qualified GHC.Data.Maybe as M import GHC.Data.OsPath ( OsPath, unsafeEncodeUtf ) @@ -71,12 +71,15 @@ import GHC.Utils.Logger import GHC.Utils.Fingerprint import GHC.Utils.TmpFs import GHC.Utils.Constants +import GHC.Utils.Monad (concatMapM) +import GHC.Utils.Monad.State.Strict import GHC.Types.Error import GHC.Types.Target import GHC.Types.SourceFile import GHC.Types.SourceError import GHC.Types.SrcLoc +import GHC.Types.Unique.Set import GHC.Types.Unique.Map import GHC.Types.PkgQual import GHC.Types.Basic @@ -91,9 +94,12 @@ import GHC.Unit.Module.Graph import GHC.Unit.Module.Deps import qualified GHC.Unit.Home.Graph as HUG import GHC.Unit.Module.Stage +import GHC.Unit.External.Index (UnitAbiHash) import Data.Either ( partitionEithers, lefts ) +import Data.Map (Map) import qualified Data.Map as Map +import Data.Set (Set) import qualified Data.Set as Set import Control.Concurrent.MVar @@ -101,7 +107,7 @@ import Control.Monad import Control.Monad.Trans.Except ( ExceptT(..), runExceptT, throwE ) import qualified Control.Monad.Catch as MC import Data.Maybe -import Data.List (partition) +import Data.List (sort, partition) import Data.Time import Data.List (unfoldr) import Data.Bifunctor (first, bimap) @@ -864,7 +870,7 @@ getRootSummary excl_mods summ_cache imports_cache hsc_env target mkPlainErrorMsgEnvelope noSrcSpan (DriverFileNotFound offset_file) | TargetModule modl <- targetId = do - let root_imp = (generatedImport FromTarget (L rootLoc modl)) + let root_imp = (generatedImport FromTarget (L noSrcSpan modl)) { ui_pkg_qual = ThisPkg (homeUnitId home_unit) } maybe_summary <- summariseModule hsc_env home_unit summ_cache imports_cache root_imp maybe_buf excl_mods @@ -875,7 +881,6 @@ getRootSummary excl_mods summ_cache imports_cache hsc_env target where Target {targetId, targetContents = maybe_buf, targetUnitId = uid} = target home_unit = ue_unitHomeUnit uid (hsc_unit_env hsc_env) - rootLoc = mkGeneralSrcSpan (fsLit "<command line>") dflags = homeUnitEnv_dflags (ue_findHomeUnitEnv uid (hsc_unit_env hsc_env)) -- | Execute 'getRootSummary' for the 'Target's using the parallelism pipeline @@ -933,52 +938,171 @@ rootSummariesParallel n_jobs hsc_env diag_wrapper msg get_summary = do -- * Check/validate properties and error out -------------------------------------------------------------------------------- --- | This function checks then important property that if both p and q are home units --- then any dependency of p, which transitively depends on q is also a home unit. +-- | Checks whether the given 'UnitEnv' has the closure property. -- --- See Note [Multiple Home Units], section 'Closure Property'. -checkHomeUnitsClosed :: UnitEnv -> [DriverMessages] -checkHomeUnitsClosed ue - | Set.null bad_unit_ids = [] - | otherwise = [singleMessage $ mkPlainErrorMsgEnvelope rootLoc $ DriverHomePackagesNotClosed (Set.toList bad_unit_ids)] +-- See the section “Closure Property” in @Note [Multiple Home Units]@ for the +-- definition of the closure property and +-- @Note [Home unit closure property check]@ below for a discussion of the +-- algorithm used for this check, its justification, and a potential +-- alternative. +checkHomeUnitsClosed :: UnitEnv -> [DriverMessages] +checkHomeUnitsClosed unit_env + | null offenders = [] + | otherwise = [ + singleMessage $ + mkPlainErrorMsgEnvelope noSrcSpan $ + DriverHomePackagesNotClosed (sort offenders) + ] where - home_id_set = HUG.allUnits $ ue_home_unit_graph ue - bad_unit_ids = upwards_closure Set.\\ home_id_set {- Remove all home units reached, keep only bad nodes -} - rootLoc = mkGeneralSrcSpan (fsLit "<command line>") - downwards_closure :: Graph (Node UnitId UnitId) - downwards_closure = graphFromEdgedVerticesUniq graphNodes + -- | The 'UnitId' and 'HomeUnitEnv' of each home unit. + home_unit_data :: [(UnitId, HomeUnitEnv)] + home_unit_data = HUG.unitEnv_assocs (ue_home_unit_graph unit_env) + + -- | The 'UnitId's of all home units. + home_units :: UniqSet UnitId + home_units = mkUniqSet (map fst home_unit_data) + + -- | All offending dependencies. A dependency of a unit /u/ on a unit /v/ is + -- offending exactly if /u/ is an external unit reachable from a home unit + -- and /v/ is a home unit. Each such dependency is represented in this list + -- by the pair of the 'UnitId' of /u/ and the 'UnitId' of /v/. + offenders :: [(UnitId, UnitId)] + offenders + = evalState (collect (map (homeUnitEnv_units . snd) home_unit_data)) + emptyUniqMap + where - inverse_closure = graphReachability $ transposeG downwards_closure + -- | Collects offending dependencies. + collect :: [UnitState] + -- ^ The 'UnitState's of the home units from which to traverse + -- the dependency graph. + -> State (UniqMap UnitId (Set UnitAbiHash)) [(UnitId, UnitId)] + -- ^ A stateful computation that collects offending dependencies + -- that have not yet been found. It uses its state, which is an + -- efficent representation of a set of 'GlobalUnitKey's, to + -- keep track of which units have already been considered as + -- sources of offending dependencies. + collect = concatMapM $ \ unit_state -> + collect_for_home_unit + (unitInfoMap unit_state) + (map (toUnitId . fst) $ explicitUnits $ unit_state) + where - upwards_closure = Set.fromList $ map node_key $ allReachableMany inverse_closure [DigraphNode uid uid [] | uid <- Set.toList home_id_set] + -- | Collects offending dependencies that are reachable from a particular + -- home unit. + collect_for_home_unit + :: UnitInfoMap + -- ^ The 'UnitInfoMap' of the home unit. + -> [UnitId] + -- ^ The 'UnitId's of the units from which to traverse the dependency + -- graph. + -> State (UniqMap UnitId (Set UnitAbiHash)) [(UnitId, UnitId)] + -- ^ A stateful computation that collects offending dependencies that + -- have not yet been found. It uses its state, which is an efficent + -- representation of a set of 'GlobalUnitKey's, to keep track of + -- which units have already been considered as sources of offending + -- dependencies. + collect_for_home_unit _ [] + = return [] + collect_for_home_unit unit_info_map (current_unit : remaining_units) = do + let + + -- | The 'UnitInfo' of the current unit. + unit_info :: UnitInfo + unit_info + = fromMaybe (pprPanic unit_not_found_msg (ppr current_unit)) $ + lookupUniqMap unit_info_map current_unit + where + + -- | The message that says that a unit was not found. + unit_not_found_msg :: String + unit_not_found_msg = "Unit not found during closure property check" + + -- | The ABI hash of the current unit. + unit_abi_hash :: UnitAbiHash + unit_abi_hash = unitAbiHash unit_info + + has_been_processed <- gets $ maybe False (Set.member unit_abi_hash) . + (`lookupUniqMap` current_unit) + if has_been_processed + then collect_for_home_unit unit_info_map remaining_units + else do + modify $ \ processed -> addToUniqMap_C Set.union + processed + current_unit + (Set.singleton unit_abi_hash) + let + + -- | The 'UnitId's of the units that the current unit depends on. + needed_units :: [UnitId] + needed_units = unitDepends unit_info + + -- | The offending dependencies of the current unit. + current_offenders :: [(UnitId, UnitId)] + current_offenders + | current_unit `elementOfUniqSet` home_units + = [] + | otherwise + = map ((,) current_unit) $ + nonDetEltsUniqSet $ + mkUniqSet needed_units `intersectUniqSets` home_units + + remaining_offenders <- collect_for_home_unit unit_info_map $ + needed_units ++ remaining_units + return $ current_offenders ++ remaining_offenders - all_unit_direct_deps :: UniqMap UnitId (Set.Set UnitId) - all_unit_direct_deps - = HUG.unitEnv_foldWithKey go emptyUniqMap $ ue_home_unit_graph ue - where - go rest this this_uis = - plusUniqMap_C Set.union - (addToUniqMap_C Set.union external_depends this (Set.fromList $ this_deps)) - rest - where - external_depends = mapUniqMap (Set.fromList . unitDepends) (unitInfoMap this_units) - this_units = homeUnitEnv_units this_uis - this_deps = [ toUnitId unit | (unit,Just _) <- explicitUnits this_units] - - graphNodes :: [Node UnitId UnitId] - graphNodes = go Set.empty home_id_set - where - go done todo - = case Set.minView todo of - Nothing -> [] - Just (uid, todo') - | Set.member uid done -> go done todo' - | otherwise -> case lookupUniqMap all_unit_direct_deps uid of - Nothing -> pprPanic "uid not found" (ppr (uid, all_unit_direct_deps)) - Just depends -> - let todo'' = (depends Set.\\ done) `Set.union` todo' - in DigraphNode uid uid (Set.toList depends) : go (Set.insert uid done) todo'' +{- + +Note [Home unit closure property check] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Per the definition in Note [Multiple Home Units], a unit environment has the +closure property exactly if there are no paths /h/₁ →* /e/ →* /h/₂ in the +dependency graph, where /h/₁ and /h/₂ are home units and /e/ is an external +unit. However, the algorithm used by 'checkHomeUnitsClosed' searches for +so-called offending dependencies, which are dependencies /e/ → /h/₂ that are +part of a path /h/₁ →* /e/ → /h/₂ in the dependency graph. To see that this is a +viable approach, consider the following: + + * A path /h/₁ →* /e/ → /h/₂ is also a path /h/₁ →* /e/ →* /h/₂. + + * For each path /h/₁ →* /e/ →* /h/₂, there exists a path /h/₁ →* /e/′ → /h/₂′, + where /e/′ is an external unit and /h/₂′ is a home unit. Such a path can be + constructed by taking as /h/₂′ the first home unit on the path /e/ →* /h/₂ + and as /e/′ the, necessarily external, unit preceding it. + +Concretely, the algorithm picks one home unit after the other, determines what +units it directly depends on, and, starting from them, follows unit dependencies +to search for offending dependencies. It does not follow dependencies that have +been followed before, possibly when processing another home unit. To achieve +this, the algorithm tracks, across home units, from which units it has already +followed dependencies. For this tracking, it identifies each unit by a 'UnitId' +and an ABI hash. Using only a 'UnitId' would not work, because 'UnitId's are not +always globally unique. Also using only an ABI hash is not an option, because an +ABI hash is not necessarily an ABI hash: it can also be the string @"inline"@. + +The correctness of this algorithm rests on the, likely correct, assumption that, +among the units mentioned in the 'UnitState' of a particular home unit, any unit +can be uniquely identified by its 'UnitId' and thus 'UnitId' clashes can only +occur across the 'UnitState's of different home units. + +An alternative approach to finding offending dependencies would be to follow +dependencies starting from all units that /any/ home unit directly depends on +instead of considering the different home units separately. A corresponding +algorithm could in principle find the dependencies of a particular unit +independently of any home unit by fetching the 'UnitInfo' of that unit from the +'GlobalUnitInfoMap'. However, for such a lookup the algorithm would need not +only the 'UnitId' but also the ABI hash of the unit in question. Therefore, +whenever following a dependency of a unit /u/ on a unit /v/, it would have to +determine the ABI hash of /v/, so that it could later look up /v/’s +dependencies. The ABI hashes of all units that /u/ depends on should be +available in the 'unitAbiDepends' field of /u/’s 'UnitInfo'. However, at the +time of writing, 'unitAbiDepends' never contained anything other than the empty +list during GHC test runs, which indicated that this alternative solution was +impossible to realize. + +-} -------------------------------------------------------------------------------- -- * Enable Code Gen for Template Haskell @@ -1763,7 +1887,7 @@ data NodeRes v -- -- See also Note [Downsweep Control Flow and Caching] dfsBuild :: (Ord k, Monad m) - => Maybe (Map.Map k (NodeRes v)) + => Maybe (Map k (NodeRes v)) -- ^ Base map, existing results. We won't re-expand any of the nodes -- already present in this map. -> [n] @@ -1773,7 +1897,7 @@ dfsBuild :: (Ord k, Monad m) -> (n -> m (NodeRes (v,[n]))) -- ^ Expand this node into its payload result and into the list of -- children nodes to visit next. - -> m (Map.Map k (NodeRes v)) + -> m (Map k (NodeRes v)) -- ^ The result accumulates the payload of expanding the root nodes -- and all nodes transitively reachable from those roots. dfsBuild base_map roots key expand = go roots (fromMaybe Map.empty base_map) ===================================== compiler/GHC/Driver/Errors/Ppr.hs ===================================== @@ -235,10 +235,17 @@ instance Diagnostic DriverMessage where "but no output will be generated.") $$ (text "There is no module named" <+> quotes (ppr mod_name) <> text ".")) - DriverHomePackagesNotClosed needed_unit_ids - -> mkSimpleDecorated $ vcat ([text "Home units are not closed." - , text "It is necessary to also load the following units:" ] - ++ map (\uid -> text "-" <+> ppr uid) needed_unit_ids) + DriverHomePackagesNotClosed offending_dependencies + -> mkSimpleDecorated $ + hang (text "Some units are not loaded but depend on loaded units.") + 4 + (vcat (map pprDependency offending_dependencies)) + where + + pprDependency :: (UnitId, UnitId) -> SDoc + pprDependency (external_unit, home_unit) + = ppr external_unit <+> arrow <+> ppr home_unit + DriverInterfaceError reason -> diagnosticMessage (ifaceDiagnosticOpts opts) reason DriverInconsistentDynFlags msg ===================================== compiler/GHC/Driver/Errors/Types.hs ===================================== @@ -369,7 +369,7 @@ data DriverMessage where DriverRedirectedNoMain :: !ModuleName -> DriverMessage - DriverHomePackagesNotClosed :: ![UnitId] -> DriverMessage + DriverHomePackagesNotClosed :: ![(UnitId, UnitId)] -> DriverMessage DriverInterfaceError :: !IfaceMessage -> DriverMessage ===================================== compiler/GHC/Parser.y ===================================== @@ -1796,10 +1796,10 @@ cvars1 :: { [RecordPatSynField GhcPs] } where_decls :: { LocatedA (OrdList (LHsDecl GhcPs), EpToken "where", AnnList) } : 'where' '{' decls '}' {% amsA' (sLL $1 $> (thdOf3 $ unLoc $3, epTok $1, - AnnList (Just (fstOf3 $ unLoc $3)) (ListBraces (epTok $2) (epTok $4)) (sndOf3 $ unLoc $3))) } + AnnList (AnnListLayout (fstOf3 $ unLoc $3)) (ListBraces (epTok $2) (epTok $4)) (sndOf3 $ unLoc $3))) } | 'where' vocurly decls close {% amsA' (sLL $1 $3 (thdOf3 $ unLoc $3, epTok $1, - AnnList (Just (fstOf3 $ unLoc $3)) ListNone (sndOf3 $ unLoc $3))) } + AnnList (AnnListLayout (fstOf3 $ unLoc $3)) ListNone (sndOf3 $ unLoc $3))) } pattern_synonym_sig :: { LSig GhcPs } : 'pattern' con_list '::' sigtype @@ -1935,9 +1935,9 @@ decls :: { Located (EpaLocation, [EpToken ";"], OrdList (LHsDecl GhcPs)) } | {- empty -} { noLoc (noAnn, [],nilOL) } decllist :: { Located (AnnList,Located (OrdList (LHsDecl GhcPs))) } - : '{' decls '}' { sLL $1 $> (AnnList (Just (fstOf3 $ unLoc $2)) (ListBraces (epTok $1) (epTok $3)) (sndOf3 $ unLoc $2) + : '{' decls '}' { sLL $1 $> (AnnList (AnnListLayout (fstOf3 $ unLoc $2)) (ListBraces (epTok $1) (epTok $3)) (sndOf3 $ unLoc $2) ,sL1 $2 $ thdOf3 $ unLoc $2) } - | vocurly decls close { sL1 $2 (AnnList (Just (fstOf3 $ unLoc $2)) ListNone (sndOf3 $ unLoc $2) + | vocurly decls close { sL1 $2 (AnnList (AnnListLayout (fstOf3 $ unLoc $2)) ListNone (sndOf3 $ unLoc $2) ,sL1 $2 $ thdOf3 $ unLoc $2) } -- Binding groups other than those of class and instance declarations @@ -1945,16 +1945,16 @@ decllist :: { Located (AnnList,Located (OrdList (LHsDecl GhcPs))) } binds :: { Located (HsLocalBinds GhcPs) } -- May have implicit parameters -- No type declarations - : decllist {% do { let { (AnnList anc p s, decls) = unLoc $1 } + : decllist {% do { let { (AnnList la p s, decls) = unLoc $1 } ; val_binds <- cvBindGroup (unLoc $ decls) ; !cs <- getCommentsFor (gl $1) - ; return (sL1 $1 $ HsValBinds (EpAnn (glR $1) (AnnList anc p s) cs, noEpTok) val_binds)} } + ; return (sL1 $1 $ HsValBinds (EpAnn (glR $1) (AnnList la p s) cs, noEpTok) val_binds)} } | '{' dbinds '}' {% acs (comb3 $1 $2 $3) (\loc cs -> (L loc - $ HsIPBinds (EpAnn (spanAsAnchor (comb3 $1 $2 $3)) (AnnList (Just$ glR $2) (ListBraces (epTok $1) (epTok $3)) []) cs, noEpTok) (IPBinds noExtField (reverse $ unLoc $2)))) } + $ HsIPBinds (EpAnn (spanAsAnchor (comb3 $1 $2 $3)) (AnnList (AnnListLayout$ glR $2) (ListBraces (epTok $1) (epTok $3)) []) cs, noEpTok) (IPBinds noExtField (reverse $ unLoc $2)))) } | vocurly dbinds close {% acs (gl $2) (\loc cs -> (L loc - $ HsIPBinds (EpAnn (glR $1) (AnnList (Just $ glR $2) ListNone []) cs, noEpTok) (IPBinds noExtField (reverse $ unLoc $2)))) } + $ HsIPBinds (EpAnn (glR $1) (AnnList (AnnListLayout $ glR $2) ListNone []) cs, noEpTok) (IPBinds noExtField (reverse $ unLoc $2)))) } wherebinds :: { Maybe (Located (HsLocalBinds GhcPs, Maybe EpAnnComments )) } @@ -3542,11 +3542,11 @@ guardquals1 :: { Located [LStmt GhcPs (LHsExpr GhcPs)] } altslist(PATS) :: { forall b. DisambECP b => PV (LocatedA ([LMatch GhcPs (LocatedA b)], AnnList)) } : '{' alts(PATS) '}' { $2 >>= \ $2 -> amsA' (sLL $1 $> (reverse (snd $ unLoc $2), - (AnnList (Just $ glR $2) (ListBraces (epTok $1) (epTok $3)) (fst $ unLoc $2)))) } + (AnnList (AnnListLayout $ glR $2) (ListBraces (epTok $1) (epTok $3)) (fst $ unLoc $2)))) } | vocurly alts(PATS) close { $2 >>= \ $2 -> amsA' (L (getLoc $2) (reverse (snd $ unLoc $2), - (AnnList (Just $ glR $2) ListNone (fst $ unLoc $2)))) } - | '{' '}' { amsA' (sLL $1 $> ([], (AnnList Nothing (ListBraces (epTok $1) (epTok $2)) []))) } + (AnnList (AnnListLayout $ glR $2) ListNone (fst $ unLoc $2)))) } + | '{' '}' { amsA' (sLL $1 $> ([], (AnnList AnnListNoLayout (ListBraces (epTok $1) (epTok $2)) []))) } | vocurly close { return $ noLocA ([], noAnn) } alts(PATS) :: { forall b. DisambECP b => PV (Located ([EpToken ";"],[LMatch GhcPs (LocatedA b)])) } @@ -3656,10 +3656,10 @@ apat : aexp {% (checkPattern <=< runPV) (unECP $1) } stmtlist :: { forall b. DisambECP b => PV (LocatedA (AnnList, Located [LocatedA (Stmt GhcPs (LocatedA b))])) } : '{' stmts '}' { $2 >>= \ $2 -> - amsA' (sLL $1 $> (AnnList (Just (spanAsAnchor $ stmtsLoc $2)) (ListBraces (epTok $1) (epTok $3)) (fromOL $ fst $ unLoc $2) + amsA' (sLL $1 $> (AnnList (AnnListLayout (spanAsAnchor $ stmtsLoc $2)) (ListBraces (epTok $1) (epTok $3)) (fromOL $ fst $ unLoc $2) , sL1 $2 $ reverse $ snd $ unLoc $2))} | vocurly stmts close { $2 >>= \ $2 -> - amsA' (L (stmtsLoc $2) (AnnList (Just (spanAsAnchor $ stmtsLoc $2)) ListNone (fromOL $ fst $ unLoc $2) + amsA' (L (stmtsLoc $2) (AnnList (AnnListLayout (spanAsAnchor $ stmtsLoc $2)) ListNone (fromOL $ fst $ unLoc $2) , sL1 $2 $ reverse $ snd $ unLoc $2))} -- do { ;; s ; s ; ; s ;; } @@ -4630,9 +4630,6 @@ glEEz !x !y = if isZeroWidthSpan (getHasLoc y) then spanAsAnchor (getHasLoc x) else spanAsAnchor $ comb2 x y -glRM :: Located a -> Maybe EpaLocation -glRM (L !l _) = Just $ spanAsAnchor l - n2l :: LocatedN a -> LocatedA a n2l (L !la !a) = L (l2l la) a ===================================== compiler/GHC/Parser/Annotation.hs ===================================== @@ -31,10 +31,6 @@ module GHC.Parser.Annotation ( SrcSpanAnnA, SrcSpanAnnN, -- ** Annotation data types used in 'GenLocated' - - AnnList(..), AnnListBrackets(..), - AnnParen(..), - AnnCType(..),AnnWarningTxt(..),AnnOverlap(..),AnnAnnDecl(..),AnnPragSCC(..), NameAnn(..), NameAdornment(..), NoEpAnns(..), @@ -43,6 +39,12 @@ module GHC.Parser.Annotation ( addTrailingAnnToA, addTrailingCommaToN, noTrailingN, + -- ** Annotation data types used in TTG extension points + + AnnList(..), AnnListBrackets(..), AnnListLayout(..), + AnnParen(..), + AnnCType(..),AnnWarningTxt(..),AnnOverlap(..),AnnAnnDecl(..),AnnPragSCC(..), + -- ** Utilities for converting between different 'GenLocated' when -- ** we do not care about the annotations. l2l, la2la, @@ -513,7 +515,7 @@ instance Outputable TrailingAnn where -- AZ: goal: only used when there is layout, so vertical alignment matters data AnnList = AnnList { - al_anchor :: !(Maybe EpaLocation), -- ^ start point of a list having layout + al_layout :: !AnnListLayout, al_brackets :: !AnnListBrackets, al_semis :: [EpToken ";"] -- decls } deriving (Data,Eq) @@ -523,6 +525,18 @@ data AnnListBrackets | ListNone deriving (Data,Eq) +-- | How the extent of a list was delimited in the source. +data AnnListLayout + = AnnListBraces -- ^ Explicit @{ ; }@ written by the user. The tokens + -- live in 'al_brackets' and 'al_semis'. + | AnnListLayout !EpaLocation + -- ^ The lexer opened an implicit layout context. + -- The 'EpaLocation' is the @vocurly@ token (or, for + -- MultiWayIf, the leading @|@), whose start column is + -- the layout column chosen by 'new_layout_context'. + | AnnListNoLayout -- ^ Neither: an Empty or compiler-generated list. + deriving (Data, Eq) + -- --------------------------------------------------------------------- -- Annotations for parenthesised elements, such as tuples, lists -- --------------------------------------------------------------------- @@ -993,7 +1007,10 @@ instance NoAnn NoEpAnns where noAnn = NoEpAnns instance NoAnn AnnList where - noAnn = AnnList Nothing ListNone noAnn + noAnn = AnnList noAnn ListNone noAnn + +instance NoAnn AnnListLayout where + noAnn = AnnListNoLayout instance NoAnn NameAnn where noAnn = NameAnnTrailing [] @@ -1094,6 +1111,11 @@ instance Outputable AnnListBrackets where ppr (ListBraces o c) = text "ListBraces" <+> ppr o <+> ppr c ppr ListNone = text "ListNone" +instance Outputable AnnListLayout where + ppr AnnListBraces = text "AnnListBraces" + ppr (AnnListLayout l) = text "AnnListLayout" <+> ppr l + ppr AnnListNoLayout = text "AnnListNoLayout" + instance Outputable AnnCType where ppr (AnnCType o c l ca) = text "AnnCType" <+> ppr o <+> ppr c <+> ppr l ===================================== compiler/GHC/Parser/PostProcess.hs ===================================== @@ -466,7 +466,7 @@ add_where w@(EpTok (EpaSpan (RealSrcSpan rs _))) (EpAnn a al cs) cs2 = (EpAnn (widenAnchorT a w) al (cs Semi.<> cs2), w) | otherwise = (EpAnn (patch_anchor rs a) - (al { al_anchor = (fmap (patch_anchor rs) (al_anchor al))}) + (al { al_layout = patch_layout (al_layout al)}) (cs Semi.<> cs2), w) add_where _ _ _ = panic "add_where" -- EpaDelta should only be used for transformations @@ -484,6 +484,12 @@ patch_anchor r1 (EpaSpan (RealSrcSpan r0 mb)) = EpaSpan (RealSrcSpan r mb) r = if srcSpanStartLine r0 < 0 then r1 else r0 patch_anchor _ (EpaSpan ss) = EpaSpan ss +-- If the decl list for where binds is empty, the anchor ends up +-- invalid. Explicitly mark it as not having layout +patch_layout :: AnnListLayout -> AnnListLayout +patch_layout (AnnListLayout _) = AnnListNoLayout +patch_layout lo = lo + -- | The anchor for a stmtlist is based on either the location or -- the first semicolon annotion. stmtsAnchor :: Located (OrdList (EpToken tok),a) -> Maybe EpaLocation ===================================== compiler/GHC/Unit/Env.hs ===================================== @@ -443,13 +443,14 @@ The flow: Closure Property ---------------- -You must perform a clean cut of the dependency graph. +A unit environment must have the closure property: -> Any dependency which is not a home unit must not (transitively) depend on a home unit. + No used external unit depends on a home unit. -For example, if you have three packages p, q and r, then if p depends on q which -depends on r then it is illegal to load both p and r as home units but not q, -because q is a dependency of the home unit p which depends on another home unit r. +More concretely, a unit environment has the closure property exactly if no home +unit directly or indirectly depends on an external unit that directly or +indirectly depends on a home unit. 'GHC.Driver.Downsweep.checkHomeUnitsClosed' +checks whether a given unit environment indeed has this property. Offsetting Paths ---------------- ===================================== compiler/GHC/Unit/State.hs ===================================== @@ -369,10 +369,15 @@ data UnitState = UnitState { -- is always mentioned before the units it depends on. preloadUnits :: [UnitId], - -- | Units which we explicitly depend on (from a command line flag). - -- We'll use this to generate version macros and the unused packages warning. The - -- original flag which was used to bring the unit into scope is recorded for the - -- -Wunused-packages warning. + -- | The units that can be used by the respective home unit. Despite the + -- identifier, this does not just cover units that are enabled explicitly + -- using flags but also units from the package database that are enabled + -- implicitly in case @-hide-all-packages@ is absent. The former are paired + -- with 'Just' applied to the respective flags, the latter are paired with + -- 'Nothing'. + -- + -- This field is used for generating version macros and “unused packages” + -- warnings. explicitUnits :: [(Unit, Maybe PackageArg)], homeUnitDepends :: Set UnitId, @@ -907,7 +912,7 @@ mkUnitState logger unit_index cfg = do let pkgname_map = listToUFM [ (unitPackageName p, unitInstanceOf p) | p <- pkgs2 ] - -- The explicitUnits accurately reflects the set of units we have turned + -- The explicitUnits accurately reflects the set of units that are turned -- on; as such, it also is the only way one can come up with requirements. -- The requirement context is directly based off of this: we simply -- look for nested unit IDs that are directly fed holes: the requirements ===================================== hadrian/ghci-multi-cabal.in ===================================== @@ -10,4 +10,4 @@ export TOOL_OUTPUT=.hadrian_ghci_multi/ghci_args # Replace newlines with spaces, as these otherwise break the ghci invocation on windows. CABFLAGS=-v0 "hadrian/build-cabal" multi --build-root=.hadrian_ghci_multi --flavour=ghc-in-ghci $HADRIAN_ARGS GHC_FLAGS="$GHC_FLAGS $(cat $TOOL_OUTPUT | tr '\n\r' ' ')" -$RUN_GHC --interactive $GHC_FLAGS $@ -fno-code -fwrite-interface -O0 +RTS -A128m +$RUN_GHC --interactive $GHC_FLAGS $@ -hide-all-packages -fno-code -fwrite-interface -O0 +RTS -A128m ===================================== testsuite/tests/driver/multipleHomeUnits/mhu-closure/Makefile ===================================== @@ -3,39 +3,47 @@ include $(TOP)/mk/boilerplate.mk include $(TOP)/mk/test.mk SETUP=../Setup -v0 +CONFIGURE=configure \ + $(CABAL_MINIMAL_BUILD) \ + --with-ghc='$(TEST_HC)' \ + --with-hc-pkg='$(GHC_PKG)' \ + --ghc-options='$(TEST_HC_OPTS)' \ + --package-db=../tmp.d +TEST_BUILD='$(TEST_HC)' $(TEST_HC_OPTS) -fhide-source-paths -fforce-recomp +ONLY_BASE=-hide-all-packages -package base -mhu-closure: clean - $(MAKE) -s --no-print-directory clean +mhu-closure: clean pkg-database + ! $(TEST_BUILD) -unit @unitP + ! $(TEST_BUILD) -unit @unitP -unit @unitQ + ! $(TEST_BUILD) -unit @unitP -unit @unitR + ! $(TEST_BUILD) -unit @unitP -unit @unitR1 + $(TEST_BUILD) -unit @unitP -unit @unitQ -unit @unitR + ! $(TEST_BUILD) -unit @unitP -unit @unitQ -unit @unitR1 + $(TEST_BUILD) $(ONLY_BASE) -unit @unitP + $(TEST_BUILD) $(ONLY_BASE) -unit @unitP -unit @unitQ + ! $(TEST_BUILD) $(ONLY_BASE) -unit @unitP -unit @unitR + ! $(TEST_BUILD) $(ONLY_BASE) -unit @unitP -unit @unitR1 + $(TEST_BUILD) $(ONLY_BASE) -unit @unitP -unit @unitQ -unit @unitR + $(TEST_BUILD) $(ONLY_BASE) -unit @unitP -unit @unitQ -unit @unitR1 + +.PHONY: pkg-database +pkg-database: '$(GHC_PKG)' init tmp.d '$(TEST_HC)' $(TEST_HC_OPTS) -v0 --make Setup - cd p && $(SETUP) clean - cd p && $(SETUP) configure $(CABAL_MINIMAL_BUILD) --ipid=p-0.1.0.0 --with-ghc='$(TEST_HC)' --with-hc-pkg='$(GHC_PKG)' --ghc-options='$(TEST_HC_OPTS)' --package-db=../tmp.d + cd p && $(SETUP) $(CONFIGURE) --ipid=p-0.1.0.0 cd p && $(SETUP) build cd p && $(SETUP) register --inplace - cd q && $(SETUP) configure $(CABAL_MINIMAL_BUILD) --ipid=q-0.1.0.0 --with-ghc='$(TEST_HC)' --with-hc-pkg='$(GHC_PKG)' --ghc-options='$(TEST_HC_OPTS)' --package-db=../tmp.d + cd q && $(SETUP) $(CONFIGURE) --ipid=q-0.1.0.0 cd q && $(SETUP) build cd q && $(SETUP) register --inplace - cd r && $(SETUP) configure $(CABAL_MINIMAL_BUILD) --ipid=r-0.1.0.0 --with-ghc='$(TEST_HC)' --with-hc-pkg='$(GHC_PKG)' --ghc-options='$(TEST_HC_OPTS)' --package-db=../tmp.d + cd r && $(SETUP) $(CONFIGURE) --ipid=r-0.1.0.0 cd r && $(SETUP) build cd r && $(SETUP) register --inplace - # This should work - '$(TEST_HC)' $(TEST_HC_OPTS) -fhide-source-paths -fforce-recomp -unit @unitP - # So should this - '$(TEST_HC)' $(TEST_HC_OPTS) -fhide-source-paths -fforce-recomp -unit @unitP -unit @unitQ - # So should this - '$(TEST_HC)' $(TEST_HC_OPTS) -fhide-source-paths -fforce-recomp -unit @unitP -unit @unitQ -unit @unitR - # This should error with a closure message - ! '$(TEST_HC)' $(TEST_HC_OPTS) -fhide-source-paths -fforce-recomp -unit @unitP -unit @unitR - # This should work, even though r1 is not in the package db - '$(TEST_HC)' $(TEST_HC_OPTS) -fhide-source-paths -fforce-recomp -unit @unitP -unit @unitQ -unit @unitR1 - # This should fail, even though r1 is not in the package db - ! '$(TEST_HC)' $(TEST_HC_OPTS) -fhide-source-paths -fforce-recomp -unit @unitP -unit @unitR1 +.PHONY: clean +clean: + $(RM) -r tmp.d Setup$(exeext) */dist* *.hi *.o */*.hi */*.o ifeq "$(CLEANUP)" "1" $(MAKE) -s --no-print-directory clean endif - -clean : - $(RM) -r tmp*.d inst-* *.o *.hi */*.o */*.hi */Setup$(exeext) */dist Setup$(exeext) - ===================================== testsuite/tests/driver/multipleHomeUnits/mhu-closure/mhu-closure.stderr ===================================== @@ -1,10 +1,28 @@ -<command line>: error: [GHC-03271] - Home units are not closed. - It is necessary to also load the following units: - - q-0.1.0.0 - -<command line>: error: [GHC-03271] - Home units are not closed. - It is necessary to also load the following units: - - q-0.1.0.0 +<no location info>: error: [GHC-03271] + Some units are not loaded but depend on loaded units. + q-0.1.0.0 -> p-0.1.0.0 + +<no location info>: error: [GHC-03271] + Some units are not loaded but depend on loaded units. + r-0.1.0.0 -> q-0.1.0.0 + +<no location info>: error: [GHC-03271] + Some units are not loaded but depend on loaded units. + q-0.1.0.0 -> p-0.1.0.0 + +<no location info>: error: [GHC-03271] + Some units are not loaded but depend on loaded units. + q-0.1.0.0 -> p-0.1.0.0 + +<no location info>: error: [GHC-03271] + Some units are not loaded but depend on loaded units. + r-0.1.0.0 -> q-0.1.0.0 + +<no location info>: error: [GHC-03271] + Some units are not loaded but depend on loaded units. + q-0.1.0.0 -> p-0.1.0.0 + +<no location info>: error: [GHC-03271] + Some units are not loaded but depend on loaded units. + q-0.1.0.0 -> p-0.1.0.0 ===================================== testsuite/tests/driver/multipleHomeUnits/mhu-closure/mhu-closure.stdout ===================================== @@ -1,3 +1,6 @@ +[1 of 3] Compiling P[p-0.1.0.0] +[2 of 3] Compiling Q[q-0.1.0.0] +[3 of 3] Compiling R[r-0.1.0.0] [1 of 1] Compiling P [1 of 2] Compiling P[p-0.1.0.0] [2 of 2] Compiling Q[q-0.1.0.0] ===================================== testsuite/tests/ghc-api/exactprint/T22919.stderr ===================================== @@ -70,7 +70,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/ghc-api/exactprint/ZeroWidthSemi.stderr ===================================== @@ -82,7 +82,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/module/mod185.stderr ===================================== @@ -97,7 +97,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/parser/should_compile/DumpParsedAst.stderr ===================================== @@ -2223,7 +2223,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/parser/should_compile/DumpParsedAstComments.stderr ===================================== @@ -90,7 +90,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -213,7 +213,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -291,7 +291,7 @@ ((,) (Right (AnnList - (Just + (AnnListLayout (EpaSpan { DumpParsedAstComments.hs:16:3 })) (ListNone) [])) @@ -361,7 +361,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/parser/should_compile/DumpRenamedAst.stderr ===================================== @@ -30,7 +30,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/parser/should_compile/DumpSemis.stderr ===================================== @@ -261,7 +261,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -333,7 +333,7 @@ ((,) (Right (AnnList - (Just + (AnnListLayout (EpaSpan { DumpSemis.hs:(11,3)-(12,3) })) (ListNone) [])) @@ -364,7 +364,7 @@ ((,) (Right (AnnList - (Just + (AnnListLayout (EpaSpan { DumpSemis.hs:11:8-13 })) (ListBraces (EpTok (EpaSpan { DumpSemis.hs:11:6 })) @@ -555,7 +555,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -627,7 +627,7 @@ ((,) (Right (AnnList - (Just + (AnnListLayout (EpaSpan { DumpSemis.hs:(16,5)-(18,5) })) (ListBraces (EpTok (EpaSpan { DumpSemis.hs:16:3 })) @@ -808,7 +808,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -880,7 +880,7 @@ ((,) (Right (AnnList - (Just + (AnnListLayout (EpaSpan { DumpSemis.hs:22:12-28 })) (ListBraces (EpTok (EpaSpan { DumpSemis.hs:22:10 })) @@ -1017,7 +1017,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -1122,7 +1122,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -1229,7 +1229,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -1731,7 +1731,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -1857,7 +1857,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -1936,7 +1936,7 @@ (EpAnn (EpaSpan { DumpSemis.hs:34:13-31 }) (AnnList - (Just + (AnnListLayout (EpaSpan { DumpSemis.hs:34:18-30 })) (ListBraces (EpTok (EpaSpan { DumpSemis.hs:34:13 })) @@ -1984,7 +1984,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -2097,7 +2097,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -2222,7 +2222,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -2333,7 +2333,7 @@ ((,) (FromSource) (AnnList - (Just + (AnnListLayout (EpaSpan { DumpSemis.hs:(38,6)-(43,13) })) (ListBraces (EpTok (EpaSpan { DumpSemis.hs:38:4 })) ===================================== testsuite/tests/parser/should_compile/KindSigs.stderr ===================================== @@ -1000,7 +1000,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -1719,7 +1719,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/parser/should_compile/T15279.stderr ===================================== @@ -8,14 +8,15 @@ (EpAnn (EpaSpan { T15279.hs:1:1 }) (AnnsModule - (NoEpTok) + (EpTok + (EpaSpan { <no location info> })) (EpTok (EpaSpan { T15279.hs:3:1-6 })) (EpTok (EpaSpan { T15279.hs:3:15-19 })) ((,,) - (NoEpTok) - (NoEpTok) + (EpTok (EpaSpan { <no location info> })) + (EpTok (EpaSpan { <no location info> })) []) [] [] @@ -100,7 +101,8 @@ (EpaComments [])) (HsTyVar - (NoEpTok) + (EpTok + (EpaSpan { <no location info> })) (NotPromoted) (L (EpAnn @@ -118,7 +120,8 @@ (EpaComments [])) (HsTyVar - (NoEpTok) + (EpTok + (EpaSpan { <no location info> })) (NotPromoted) (L (EpAnn @@ -152,7 +155,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -182,7 +185,8 @@ (Prefix) (NoSrcStrict) (AnnFunRhs - (NoEpTok) + (EpTok + (EpaSpan { <no location info> })) [] [])) (L @@ -258,7 +262,8 @@ (Prefix) (NoSrcStrict) (AnnFunRhs - (NoEpTok) + (EpTok + (EpaSpan { <no location info> })) [] [])) (L @@ -334,7 +339,8 @@ (Prefix) (NoSrcStrict) (AnnFunRhs - (NoEpTok) + (EpTok + (EpaSpan { <no location info> })) [] [])) (L ===================================== testsuite/tests/parser/should_compile/T20718.stderr ===================================== @@ -104,7 +104,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/parser/should_compile/T20846.stderr ===================================== @@ -94,7 +94,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== testsuite/tests/printer/Test20297.stdout ===================================== @@ -70,7 +70,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -161,8 +161,7 @@ (EpAnn (EpaSpan { <no location info> }) (AnnList - (Just - (EpaSpan { Test20297.hs:7:3-7 })) + (AnnListNoLayout) (ListNone) []) (EpaComments @@ -201,7 +200,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -286,7 +285,7 @@ (EpAnn (EpaSpan { Test20297.hs:(10,3)-(11,26) }) (AnnList - (Just + (AnnListLayout (EpaSpan { Test20297.hs:11:9-26 })) (ListNone) []) @@ -324,7 +323,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -396,7 +395,7 @@ ((,) (Right (AnnList - (Just + (AnnListLayout (EpaSpan { Test20297.hs:11:22-26 })) (ListNone) [])) @@ -513,7 +512,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -598,8 +597,7 @@ (EpAnn (EpaSpan { <no location info> }) (AnnList - (Just - (EpaSpan { Test20297.ppr.hs:5:3-7 })) + (AnnListNoLayout) (ListNone) []) (EpaComments @@ -632,7 +630,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -717,7 +715,7 @@ (EpAnn (EpaSpan { Test20297.ppr.hs:(8,3)-(9,24) }) (AnnList - (Just + (AnnListLayout (EpaSpan { Test20297.ppr.hs:9:7-24 })) (ListNone) []) @@ -749,7 +747,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -821,7 +819,7 @@ ((,) (Right (AnnList - (Just + (AnnListLayout (EpaSpan { Test20297.ppr.hs:9:20-24 })) (ListNone) [])) ===================================== testsuite/tests/printer/Test24533.stdout ===================================== @@ -534,7 +534,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L @@ -1121,7 +1121,7 @@ ((,) (FromSource) (AnnList - (Nothing) + (AnnListNoLayout) (ListNone) [])) (L ===================================== utils/check-exact/ExactPrint.hs ===================================== @@ -231,7 +231,7 @@ setAnchorAn (L (EpAnn _ an _) a) anc ts cs = (L (EpAnn anc (setTrailing an ts) c -- `debug` ("setAnchorAn: anc=" ++ showAst anc) setAnchorEpaL :: EpAnn AnnList -> EpaLocation -> [TrailingAnn] -> EpAnnComments -> EpAnn AnnList -setAnchorEpaL (EpAnn _ an _) anc ts cs = EpAnn anc (setTrailing (an {al_anchor = Nothing}) ts) cs +setAnchorEpaL (EpAnn _ an _) anc ts cs = EpAnn anc (setTrailing (an {al_layout = AnnListNoLayout}) ts) cs -- --------------------------------------------------------------------- @@ -2672,8 +2672,8 @@ instance ExactPrint (HsLocalBinds GhcPs) where exact (HsValBinds (an0, w) valbinds) = do w' <- markEpToken w -- 'where' - case al_anchor $ anns an0 of - Just anc -> do + case al_layout $ anns an0 of + AnnListLayout anc -> do when (not $ isEmptyValBinds valbinds) $ setExtraDP (Just anc) _ -> return () @@ -2684,7 +2684,7 @@ instance ExactPrint (HsLocalBinds GhcPs) where Nothing -> return an1 Just (ss,dp) -> do setExtraDPReturn Nothing - return $ an1 { anns = (anns an1) { al_anchor = Just (EpaDelta ss dp []) }} + return $ an1 { anns = (anns an1) { al_layout = AnnListLayout (EpaDelta ss dp []) }} return (HsValBinds (an2, w') valbinds') exact (HsIPBinds (an,w) bs) = do ===================================== utils/check-exact/Main.hs ===================================== @@ -521,8 +521,8 @@ changeLocalDecls libdir (L l p) = do let oldDecls' = captureLineSpacing oldDecls let (VbSig o:oldBinds) = map wrapValBind oldDecls' o' = setEntryDP o (DifferentLine 2 0) - let (EpAnn anc (AnnList (Just _) a b) cs) = van - let van' = (EpAnn anc (AnnList (Just (EpaDelta noSrcSpan (DifferentLine 1 4) [])) a b) cs) + let (EpAnn anc (AnnList (AnnListLayout _) a b) cs) = van + let van' = (EpAnn anc (AnnList (AnnListLayout (EpaDelta noSrcSpan (DifferentLine 1 4) [])) a b) cs) let binds' = (HsValBinds (van',w) (ValBinds noExtField (VbSig sig':VbBind decl':VbSig o':oldBinds))) return (L lm (Match an mln pats (GRHSs emptyComments rhs binds'))) @@ -548,7 +548,7 @@ changeLocalDecls2 libdir (L l p) = do let anc = (EpaDelta noSrcSpan (DifferentLine 1 2) []) let anc2 = (EpaDelta noSrcSpan (DifferentLine 1 4) []) let an = (EpAnn anc - (AnnList (Just anc2) ListNone + (AnnList (AnnListLayout anc2) ListNone []) emptyComments, EpTok (EpaDelta noSrcSpan (SameLine 0) [])) let decls = [VbSig sig', VbBind decl'] ===================================== utils/check-exact/Transform.hs ===================================== @@ -1046,7 +1046,7 @@ newWhereAnnotation ww = (an, w) WithWhere -> EpTok (EpaDelta noSrcSpan (SameLine 0) []) WithoutWhere -> noEpTok an = EpAnn anc - (AnnList (Just anc2) ListNone []) + (AnnList (AnnListLayout anc2) ListNone []) emptyComments -- --------------------------------------------------------------------- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a6b642b69933d2f038764114a9021f… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a6b642b69933d2f038764114a9021f… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc][wip/T27844] Do more on swapAndFinish
by Simon Peyton Jones (＠simonpj) 25 Sep '26

25 Sep '26

Simon Peyton Jones pushed to branch wip/T27844 at Glasgow Haskell Compiler / GHC Commits: f3b36989 by Simon Peyton Jones at 2026-09-25T17:45:47+01:00 Do more on swapAndFinish - - - - - 1 changed file: - compiler/GHC/Tc/Solver/Equality.hs Changes: ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -2294,23 +2294,18 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs -- If we had F a ~ G (F a), which gives an occurs check, -- then swap it to G (F a) ~ F a, which does not -- See Note [Orienting TyVarLHS/TyFamLHS] - -- ToDo: fix me + -- ToDo: fix me ... also needed for a ~ G (F a) -- However `swap_for_size` above will orient it with (G (F a)) on -- the left anwyway. `swap_for_rewriting` "wins", but that doesn't -- matter: in the occurs check case swap_for_rewriting will be moot. -- TL;DR: the next four lines of code are redundant -- I'm leaving them here in case they become relevant again - | TyFamLHS {} <- lhs - , Just can_rhs <- canTyFamEqLHS_maybe rhs + | Just can_rhs <- canTyFamEqLHS_maybe rhs , reason `cterHasOnlyProblem` cteSolubleOccurs - -> swapAndFinish ev eq_rel swapped lhs_ty can_rhs + -> finishWith ev eq_rel (flipSwap swapped) can_rhs lhs_ty | reason `cterHasOnlyProblems` do_not_prevent_rewriting - -> do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs - ; continueWith $ Right $ - EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel - , eq_lhs = lhs , eq_rhs = rhs } - } + -> finishWith ev eq_rel swapped lhs rhs | otherwise -> tryIrredInstead reason ev eq_rel swapped lhs rhs @@ -2343,6 +2338,16 @@ do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<> cteProblem cteConcrete ---------------------- +finishWith :: CtEvidence -> EqRel -> SwapFlag + -> CanEqLHS -> TcType + -> TcS (StopOrContinue (Either unused EqCt)) +finishWith ev eq_rel swapped can_lhs rhs_ty + = do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped can_lhs rhs_ty + ; continueWith $ Right $ + EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel + , eq_lhs = can_lhs , eq_rhs = rhs_ty } } + +{- swapAndFinish :: CtEvidence -> EqRel -> SwapFlag -> TcType -> CanEqLHS -- ty ~ F tys -> TcS (StopOrContinue (Either unused EqCt)) @@ -2354,6 +2359,7 @@ swapAndFinish ev eq_rel swapped lhs_ty can_rhs ; continueWith $ Right $ EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel , eq_lhs = can_rhs, eq_rhs = lhs_ty } } +-} ---------------------- tryIrredInstead :: CheckTyEqResult -> CtEvidence View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f3b36989d97f7839876ec4f47142cf0… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f3b36989d97f7839876ec4f47142cf0… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc] Pushed new branch wip/fendor/27836
by Hannes Siebenhandl (＠fendor) 25 Sep '26

25 Sep '26

Hannes Siebenhandl pushed new branch wip/fendor/27836 at Glasgow Haskell Compiler / GHC -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/fendor/27836 You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0