[Git][ghc/ghc] Pushed new branch wip/sjakobi/hadrian-readme-tool-args
by Simon Jakobi (＠sjakobi) 08 Oct '26
by Simon Jakobi (＠sjakobi) 08 Oct '26
08 Oct '26
Simon Jakobi pushed new branch wip/sjakobi/hadrian-readme-tool-args at Glasgow Haskell Compiler / GHC
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/sjakobi/hadrian-readme-tool-a…
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/sjakobi/hadrian-readme-tool-args
by Simon Jakobi (＠sjakobi) 08 Oct '26
by Simon Jakobi (＠sjakobi) 08 Oct '26
08 Oct '26
Simon Jakobi pushed new branch wip/sjakobi/hadrian-readme-tool-args at Glasgow Haskell Compiler / GHC
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/sjakobi/hadrian-readme-tool-a…
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] 19 commits: RTS: Update flag parsing/handling:
by Simon Peyton Jones (＠simonpj) 08 Oct '26
by Simon Peyton Jones (＠simonpj) 08 Oct '26
08 Oct '26
Simon Peyton Jones pushed to branch wip/T27844 at Glasgow Haskell Compiler / GHC
Commits:
c406135c by Andreas Klebinger at 2026-10-01T06:57:28-04:00
RTS: Update flag parsing/handling:
Using 0 as argument to any of these flags now resets the flags setting to default:
- ``-n0`` disables nursery chunking.
- ``-K0`` (or a bare ``-K``) removes the stack size limit.
- ``-M0`` removes the heap size limit.
- ``-H0`` resets the suggested heap size, including the nursery scaling set by ``-H``.
- ``-AL0`` makes the large object allocation limit follow ``-A`` again.
GC Generations are now limited to 64.
-n larger than -A now emits a warning and disables chunking.
Fixes #27830 #27829
- - - - -
984ee82b by Andreas Klebinger at 2026-10-01T06:58:10-04:00
Fix MultiLayerModules timeout multiplier.
We accidentally used the compile multiplier for ghci commands which
use the run timeout setting to set the timeout.
Fixes #26263 and #27796.
- - - - -
50a9cf26 by Andreas Klebinger at 2026-10-01T06:58:10-04:00
testsuite: Include runtime in JUnit report.
- - - - -
e358619f by Alan Zimmerman at 2026-10-01T06:59:01-04:00
EPA: Use EpaLocation in EpVirtualBraces
Haddock processing uses EpLayout.EpVirtualBraces to record the current
layout column, for allocating haddock comments correctly.
For exact printing, we need the line as well as the col, so we know
how many lines to skip when the indented code block starts.
This commit updates EpLayout.EpVirtualBraces so that it carries an
EpaLocation instead of just the Int column, to allow it to be used for
both purposes.
It is a simple mechanical change, with no other impact, but it allows
us to use EpLayout instead of AnnListLayout in AnnList, in the next
commit in this series.
- - - - -
1d2a26ee by Andrew Lelechenko at 2026-10-01T20:22:04-04:00
Remove bitSize from MINIMAL pragma of class Bits
Cf. https://github.com/haskell/core-libraries-committee/issues/441
The function is deprecated for 12 years and has a default implementation,
yet it was never removed from the MINIMAL pragma, putting library authors
in a very awkward position. Let's finally remove bitSize from MINIMAL.
- - - - -
3cc21e4c by Hannes Siebenhandl at 2026-10-01T20:22:59-04:00
Add regression test for #27641
- - - - -
c35096f5 by Hannes Siebenhandl at 2026-10-01T20:23:00-04:00
Don't `:add` modules the loader will reject
Only home modules can be actually added to the loader context, thus we
only accept the module if it belongs to a home unit.
- - - - -
a563cb27 by Simon Jakobi at 2026-10-02T17:37:36-04:00
ci: accept modified changelog.d entries in lint-changelog
The changelog guide says to extend an existing entry rather than add a
new one when the feature is already documented. lint_changelog only
counted added files, so such MRs failed before the validator ran.
Fixes #27779.
Assisted-by: Claude Fable 5.1
- - - - -
03082cd4 by Simon Jakobi at 2026-10-02T17:38:17-04:00
changelog.d: Fix warning flag name in the semaphore-v2 entry
The entry refers to -Wsemaphore-version-mismatch, which does not exist.
The warning GHC emits when it cannot use a -jsem semaphore, including
on a protocol version mismatch, is -Wsemaphore-open-failure.
Context: !15729, #25087
Assisted-by: Claude Fable 5.1
- - - - -
a93705ee by Simon Jakobi at 2026-10-02T17:38:17-04:00
changelog.d: Fix the CLC proposal link in the T27455 entry
The entry used the Sphinx :ref: role with a URL as its target. :ref:
resolves only internal labels, so the generated release notes would
show the proposal name without a link. Use the plain hyperlink form
like the other entries.
Context: !16274, #27455
Assisted-by: Claude Fable 5.1
- - - - -
54381079 by Hannes Siebenhandl at 2026-10-02T17:39:01-04:00
Extend the `TrustOverlay` for wired-in units
The TrustOverlay only contained the `UnitId` of all on-disk units.
However, wired-in units are referred to by their wired-in unit id, which
is not the same as the on-disk unit id.
Thus, trust checks for wired-in units failed because the lookup was
using the wired-in unit, which wasn't present in the `TrustOverlay`.
We fix #27834, by copying the trust info for wired-in unit ids.
- - - - -
f8cfb1a5 by Hécate Kleidukos at 2026-10-04T19:36:39+02:00
[CLC 341] Strict variants of mutable types
This commit is the implementation of CLC Proposal 341
https://github.com/haskell/core-libraries-committee/issues/341
- - - - -
575c4bc6 by Rodrigo Mesquita at 2026-10-05T12:32:02-04:00
ttg: HsModuleName in the AST, ModuleName in GHC
This commit makes the AST fully independent from GHC by parsing a
"module name" as an `HsModuleName (= HText)` rather than constructing an
`ModuleName (= FastString)` straight away.
In the GHC side, everything remains as a `ModuleName`. We turn AST
`HsModuleName`s into fast strings with the cheap `mkFastStringShortText`
when we process the AST for manipulation within the compiler.
There are no performance regressions introduced by this approach.
This is the final piece of #21592
Alternative plans were discussed in
gitlab.haskell.org/ghc/ghc/-/merge_requests/16546#note_694647,
but the Simon suggested one won in simplicity and performance when
compared against my attempt at implementing my original plan of having
a family `ModuleNameP`.
- - - - -
b3b89d32 by mangoiv at 2026-10-05T22:03:32-04:00
hadrian: Persist the used flavour name in the build root (#20650)
This executes the idea proposed in #20650, teaching Hadrian to persist
the flavour used to build a build root. This both makes use of multiple
build roots more ergonomic (as the user no longer needs to repeat
themselves) and avoids a tiresome foot-gun (forgetting to specify a
flavour, often wholly invalidating a build root).
Closes #20650.
Co-authored-by: Sylvain Henry <sylvain(a)haskus.fr>
- - - - -
f977837b by mangoiv at 2026-10-05T22:04:21-04:00
configure: fix sed script and subst tooldir script
Fixes #27672
Adds sanity checking for SUBST_TOOLDIR
Metric Decrease:
LinkableUsage01
MultiLayerModulesTH_OneShot
T10547
T12234
T12425
T13035
T13820
T18140
T18730
T18923
T9198
TcPlugin_RewritePerf
mhu-perf
- - - - -
f1cb08be by Hannes Siebenhandl at 2026-10-05T22:05:03-04:00
Prepend in-memory unit database for backpack
The packageDbFlags are stored in reverse order. Thus, prepending will
ensure that the in-memory unit database is the last item on the unit
database stack.
Further, the in-memory unit database needs to be able to shadow units
from earlier unit databases in the unit database stack.
Moreover, a `-clear-package-db` would remove the in-memory database if
it weren't the last item on the stack.
Closes #27835
- - - - -
8d49ed42 by Kazu Yamamoto at 2026-10-06T19:37:25-04:00
Do not leave standard file descriptors free at startup (#24450)
A process may be started with stdout closed -- `prog >&-` from a shell does
exactly that. Nothing then reserves descriptor 1, and open(), pipe() and
socket() hand out the lowest free descriptor, so the next descriptor the
runtime creates for itself takes it: the ticker's pipe, or a capability's IO
manager control pipe.
'GHC.Internal.IO.StdHandles.stdout' is a CAF, built the first time the program
writes to stdout, which is long after that has happened. It builds a 'Handle'
over descriptor 1, which now belongs to the runtime, and nothing reports an
error because the descriptor is perfectly good. The program then writes its
output into the runtime's own plumbing.
What that looks like from the outside is a hang. The descriptor the Handle has
taken over is the read end of a pipe, so poll() for POLLOUT on it never says
yes and epoll_ctl() accepts a registration for it; the thread waiting to write
blocks for ever. Closing the Handle at exit closes the runtime's descriptor,
which is worse: the ticker then fails on every tick.
'hs_init_ghc' now opens /dev/null onto whichever of descriptors 0, 1 and 2 are
closed, before the runtime creates any descriptor of its own. Each is opened
for the access that descriptor would normally have, read-only for 0 and
write-only for 1 and 2, so that writing to 'stdin' or reading from 'stdout'
still fails rather than quietly succeeding against /dev/null. See
Note [Standard file descriptors must be open].
Moving only the descriptors the runtime opens would not do: the first file the
program itself opened would land on the free number instead. The fix has to
leave no free number. A program run this way therefore finds stdout connected
to /dev/null rather than failing with EBADF on the first write, which is what
such a program would get from most other language runtimes.
Co-Authored-By: Claude Opus 5 (1M context) <noreply(a)anthropic.com>
- - - - -
65bcf9e9 by Simon Jakobi at 2026-10-06T19:38:09-04:00
changelog: Repair the sentence describing #27477
The description read "programs using could crash", the object of
"using" having been lost. The synopsis already says which programs are
affected, so drop the dangling word.
Assisted-by: Claude Fable 5.1
- - - - -
6a6de9da by Simon Peyton Jones at 2026-10-08T10:26:26+01:00
Refactor and simplify solver's unification code
Ticket #27844 showed that GHC's constraint solver could miss an
occurs check, and thereby build an infinite type.
This patch significantly simplifes the code in
GHC.Tc.Solver.Equality.canEqCanLHSFinish_try_unification
GHC.Tc.Solver.Equality.canEqCanLHSFinish_no_unification
It is now significantly simpler, and requires much less subtle
reasoning to understand.
Main changes
* If `canEqCanLHSFinish_try_unification` fails to unify, it now /always/ calls
`canEqCanLHSFinish_no_unification` rather than trying to finish the job itself.
* `GHC.Tc.Solver.Monad.checkTypeEq` is moved from Monad into Equality, and renamed
to `GHC.Tc.Solver.Equality.checkTypeEqNoUnification`.
* `canEqCanLHSFinish_no_unification` calls `checkTypeEqNoUnification` to test
the invariants for an inert equality. Before this MR there was a special case for
`do_not_prevent_rewriting`, but that has gone; instead it's just a consequence of
the flags passed to `checkTyEqRhs`, documented in the `PuOK` case of
`canEqCanLHSFinish_no_unification`.
* There is only one bit of "swap back" code, in `finish_no_unify` in
`canEqCanLHSFinish_try_unification. Previously this code was duplicated.
* `kickOutAfterFillingCoercionHole` should account for equalities with a
TyFamLHS. See (KOC5) in Note [Kick out after filling a coercion hole]
* No need to gather coercion holes in the `PuOK` case of `canEqCanLHSFinish_no_unification`.
See documentation with that code.
- - - - -
159 changed files:
- .gitlab/ci.sh
- + changelog.d/24450
- + changelog.d/27641
- changelog.d/T27455
- + changelog.d/T27830-rts-flag-bounds
- + changelog.d/T27844
- + changelog.d/clc-341-strict-mutable-data-types
- changelog.d/fix-parallel-gc-selector-race-27477
- + changelog.d/hadrian-persist-flavour
- changelog.d/semaphore-v2
- changelog.d/unit-index
- compiler/GHC.hs
- compiler/GHC/Builtin/Modules.hs
- compiler/GHC/ByteCode/Asm.hs
- compiler/GHC/ByteCode/Show.hs
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/Opt/CallerCC/Types.hs
- compiler/GHC/Driver/Backpack.hs
- compiler/GHC/Driver/Main/Compile.hs
- compiler/GHC/Driver/Pipeline.hs-boot
- compiler/GHC/Driver/Pipeline/Execute.hs
- compiler/GHC/Driver/Pipeline/Phases.hs
- compiler/GHC/Hs/Doc.hs
- compiler/GHC/Hs/Dump.hs
- compiler/GHC/Hs/Expr.hs
- compiler/GHC/Hs/ImpExp.hs
- compiler/GHC/Hs/Lit.hs
- compiler/GHC/HsToCore/Docs.hs
- compiler/GHC/HsToCore/Quote.hs
- compiler/GHC/Iface/Errors/Types.hs
- compiler/GHC/Iface/Ext/Ast.hs
- compiler/GHC/Iface/Ext/Debug.hs
- compiler/GHC/Iface/Ext/Types.hs
- compiler/GHC/Parser.y
- compiler/GHC/Parser/Annotation.hs
- compiler/GHC/Parser/Errors/Types.hs
- compiler/GHC/Parser/Header.hs
- compiler/GHC/Parser/Lexer.x
- compiler/GHC/Parser/PostProcess.hs
- compiler/GHC/Parser/PostProcess/Haddock.hs
- compiler/GHC/Parser/String.hs
- compiler/GHC/Rename/Env.hs
- compiler/GHC/Rename/Names.hs
- compiler/GHC/Rename/Unbound.hs
- compiler/GHC/Runtime/Heap/Inspect.hs
- compiler/GHC/StgToJS/Linker/Linker.hs
- compiler/GHC/Tc/Deriv/Generics.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/Export.hs
- compiler/GHC/Tc/Module.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Types/ErrCtxt.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/ThToHs.hs
- compiler/GHC/Types/Unique.hs
- compiler/GHC/Types/UnresolvedImport.hs
- compiler/GHC/Unit/External/Wired.hs
- compiler/GHC/Unit/Home.hs
- compiler/GHC/Unit/Module.hs
- compiler/GHC/Unit/Module/Env.hs
- + compiler/GHC/Unit/Module/Name.hs
- compiler/GHC/Unit/Parser.hs
- compiler/GHC/Unit/State.hs
- compiler/GHC/Unit/Types.hs
- compiler/GHC/Unit/Types.hs-boot
- compiler/GHC/Utils/Binary.hs
- compiler/GHC/Utils/Outputable.hs
- compiler/Language/Haskell/Syntax.hs
- compiler/Language/Haskell/Syntax/Expr.hs
- compiler/Language/Haskell/Syntax/ImpExp.hs
- compiler/Language/Haskell/Syntax/Lit.hs
- compiler/Language/Haskell/Syntax/Module/Name.hs
- compiler/Language/Haskell/Syntax/Text.hs
- compiler/ghc.cabal.in
- distrib/configure.ac.in
- docs/users_guide/runtime_control.rst
- ghc/GHCi/UI.hs
- ghc/GHCi/UI/Info.hs
- hadrian/doc/flavours.md
- hadrian/src/Rules.hs
- hadrian/src/Settings.hs
- libraries/base/base.cabal.in
- libraries/base/changelog.md
- libraries/base/src/Control/Concurrent/Chan.hs
- + libraries/base/src/Control/Concurrent/Chan/Strict.hs
- libraries/base/src/Control/Concurrent/MVar.hs
- + libraries/base/src/Control/Concurrent/MVar/Strict.hs
- libraries/base/src/Data/IORef.hs
- + libraries/base/src/Data/IORef/Strict.hs
- libraries/ghc-internal/src/GHC/Internal/Bits.hs
- linters/lint-codes/LintCodes/Static.hs
- m4/subst_tooldir.m4
- rts/RtsFlags.c
- rts/RtsStartup.c
- rts/include/rts/Flags.h
- rts/include/rts/storage/GC.h
- rts/sm/GC.c
- rts/sm/Storage.c
- testsuite/driver/junit.py
- testsuite/driver/testglobals.py
- testsuite/driver/testlib.py
- + testsuite/tests/backpack/should_compile/T27835.bkp
- + testsuite/tests/backpack/should_compile/T27835.stderr
- testsuite/tests/backpack/should_compile/all.T
- testsuite/tests/count-deps/CountDepsAst.stdout
- testsuite/tests/count-deps/CountDepsParser.stdout
- testsuite/tests/ghc-api/downsweep/IncrementalDownsweep.hs
- testsuite/tests/ghc-api/exactprint/T22919.stderr
- testsuite/tests/ghc-api/exactprint/Test20239.stderr
- testsuite/tests/ghc-api/exactprint/ZeroWidthSemi.stderr
- + testsuite/tests/ghci/scripts/T27641.script
- + testsuite/tests/ghci/scripts/T27641.stderr
- + testsuite/tests/ghci/scripts/T27641.stdout
- + testsuite/tests/ghci/scripts/T27834.hs
- + testsuite/tests/ghci/scripts/T27834.script
- + testsuite/tests/ghci/scripts/T27834.stdout
- testsuite/tests/ghci/scripts/all.T
- testsuite/tests/haddock/should_compile_flag_haddock/T17544.stderr
- testsuite/tests/haddock/should_compile_flag_haddock/T17544_kw.stderr
- testsuite/tests/haddock/should_compile_flag_haddock/T24221.stderr
- testsuite/tests/hiefile/should_run/T24544.hs
- testsuite/tests/indexed-types/should_fail/T9662.stderr
- testsuite/tests/interface-stability/base-exports.stdout
- testsuite/tests/interface-stability/base-exports.stdout-javascript-unknown-ghcjs
- testsuite/tests/interface-stability/base-exports.stdout-mingw32
- testsuite/tests/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/T14189.stderr
- testsuite/tests/parser/should_compile/T15323.stderr
- testsuite/tests/parser/should_compile/T20452.stderr
- testsuite/tests/parser/should_compile/T20718.stderr
- testsuite/tests/parser/should_compile/T20718b.stderr
- testsuite/tests/parser/should_compile/T20846.stderr
- testsuite/tests/parser/should_compile/T23315/T23315.stderr
- testsuite/tests/perf/compiler/all.T
- testsuite/tests/printer/AnnotationNoListTuplePuns.stdout
- testsuite/tests/printer/T18791.stderr
- testsuite/tests/printer/Test20297.stdout
- testsuite/tests/printer/Test24533.stdout
- testsuite/tests/profiling/should_run/caller-cc/CallerCcParser.hs
- + testsuite/tests/rts/T24450.hs
- + testsuite/tests/rts/T24450.stderr
- testsuite/tests/rts/all.T
- testsuite/tests/rts/rtsflags001.stderr-ws-32
- testsuite/tests/rts/rtsflags001.stderr-ws-64
- + testsuite/tests/typecheck/should_fail/T27844.hs
- + testsuite/tests/typecheck/should_fail/T27844.stderr
- testsuite/tests/typecheck/should_fail/all.T
- utils/check-exact/ExactPrint.hs
- utils/haddock/haddock-api/src/Haddock/Backends/Hyperlinker/Renderer.hs
The diff was not included because it is too large.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/96911a123bfa84f5e3b079b1ea27ef…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/96911a123bfa84f5e3b079b1ea27ef…
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] 3 commits: Revert back to just using getOccString for DFunIds
by Florian Ragwitz (＠rafl) 07 Oct '26
by Florian Ragwitz (＠rafl) 07 Oct '26
07 Oct '26
Florian Ragwitz pushed to branch wip/rafl/hpc-instances at Glasgow Haskell Compiler / GHC
Commits:
45019587 by Florian Ragwitz at 2026-10-07T18:54:05-07:00
Revert back to just using getOccString for DFunIds
- - - - -
100074ba by Florian Ragwitz at 2026-10-07T18:54:05-07:00
Limit instance and instance method coverage to HPC only
It's not useful for SourceNotes, which is the other tickishType included in
TickForCoverage.
- - - - -
a9c4f52b by Florian Ragwitz at 2026-10-07T18:54:05-07:00
Limit record selector ticking to HPC
- - - - -
3 changed files:
- compiler/GHC/HsToCore/Ticks.hs
- testsuite/tests/hpc/instmeths/instmeths.hs
- testsuite/tests/hpc/instmeths/instmeths.stdout
Changes:
=====================================
compiler/GHC/HsToCore/Ticks.hs
=====================================
@@ -51,7 +51,6 @@ import GHC.Types.CostCentre.State
import GHC.Types.Tickish
import GHC.Types.ProfAuto
import GHC.Tc.Types.ErrCtxt
-import GHC.Tc.Utils.TcType
import Control.Monad
import Data.List (isSuffixOf, intersperse)
@@ -313,7 +312,7 @@ addTickLHsBind (L pos (funBind@(FunBind { fun_id = L _ id, fun_matches = matches
exported = idName id `elemNameSet` exported_names
-- See Note [Instance Method Coverage].
- let generatedInstMeth = density == TickForCoverage
+ let generatedInstMeth = tickishType env == HpcTicks
&& id `elemVarEnv` instMeths env
&& isGenerated (mg_origin (mg_ext matches))
@@ -1236,6 +1235,9 @@ getDensity = TM $ \env st -> (density env, noFVs, st)
ifDensity :: TickDensity -> TM a -> TM a -> TM a
ifDensity d th el = do d0 <- getDensity; if d == d0 then th else el
+ifTickish :: TickishType -> TM a -> TM a -> TM a
+ifTickish want th el = tickishType <$> getEnv >>= \got -> if want == got then th else el
+
getFreeVars :: TM a -> TM (FreeVars, a)
getFreeVars (TM m)
= TM $ \ env st -> case m env st of (a, fv, st') -> ((fv,a), fv, st')
@@ -1295,13 +1297,12 @@ isBlackListed UnhelpfulSpan{} = return False
-- See Note [Instance Method Coverage].
allocInstTicks :: [ClsInst] -> TM (NameEnv CoreTickish)
allocInstTicks insts =
- ifDensity TickForCoverage (mkNameEnv . catMaybes <$> mapM alloc insts) (pure emptyNameEnv)
+ ifTickish HpcTicks (mkNameEnv . catMaybes <$> mapM alloc insts) (pure emptyNameEnv)
where
alloc ClsInst{ is_dfun, is_cls }
| null (classMethods is_cls) = pure Nothing
- | otherwise = fmap (idName is_dfun,) <$> allocATickBox (TopLevelBox [s])
+ | otherwise = fmap (idName is_dfun,) <$> allocATickBox (TopLevelBox [getOccString is_dfun])
False True (getSrcSpan is_dfun) noFVs
- where s = showSDocOneLine defaultSDocContext (pprSigmaType (idType is_dfun))
-- See Note [Instance Method Coverage].
instMethTick :: Id -> TM (Maybe CoreTickish)
@@ -1325,7 +1326,7 @@ allocTickBox boxLabel countEntries topOnly pos m
return (this_loc (XExpr $ HsTick tickish $ this_loc e))
recSelTick :: Id -> TM (Maybe [CoreTickish])
-recSelTick id = ifDensity TickForCoverage maybe_tick (pure Nothing)
+recSelTick id = ifTickish HpcTicks maybe_tick (pure Nothing)
where
maybe_tick = getEnv >>=
maybe (pure Nothing) tick_all . (`lookupVarEnv` id) . recSelBinds
=====================================
testsuite/tests/hpc/instmeths/instmeths.hs
=====================================
@@ -27,7 +27,7 @@ instance Marker (T Bool)
interesting :: (Int, MixEntry) -> Maybe (Int, HpcPos, String)
interesting (n, (pos, TopLevelBox [name])) | isInteresting name = Just (n, pos, name)
where isInteresting = (||) <$> isInst <*> isMeth
- isInst = ("T" `isInfixOf`)
+ isInst = ("$f" `isPrefixOf`)
isMeth = (||) <$> (`elem` ["(==)", "(/=)", "show", "showList", "showsPrec", "fmap", "(<$)"])
<*> ("Meth" `isInfixOf`)
interesting _ = Nothing
=====================================
testsuite/tests/hpc/instmeths/instmeths.stdout
=====================================
@@ -1,10 +1,10 @@
True
"Foo (T' a) instance"
-(1,"Eq a => Eq (T a)","Eq")
-(0,"Foo (T a)","Foo (T a)")
-(1,"Foo (T' a)","Foo (T' a)")
-(1,"Functor T","Functor")
-(0,"Show a => Show (T a)","Show")
+(1,"$fEqT","Eq")
+(0,"$fFooT","Foo (T a)")
+(1,"$fFooT'","Foo (T' a)")
+(1,"$fFunctorT","Functor")
+(0,"$fShowT","Show")
(0,"defMeth","defMeth = const \"class default\"")
(0,"defMeth","defMeth = const \"Foo (T' a) instance\"")
(0,"defMeth'","defMeth' = const \"class default\"")
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/86f16aead8cc4bd2de092eac4aed68…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/86f16aead8cc4bd2de092eac4aed68…
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] 2 commits: Remove tcg_inst_meths in favour of a new IdDetails constructor
by Florian Ragwitz (＠rafl) 07 Oct '26
by Florian Ragwitz (＠rafl) 07 Oct '26
07 Oct '26
Florian Ragwitz pushed to branch wip/rafl/hpc-instances at Glasgow Haskell Compiler / GHC
Commits:
66df1b00 by Florian Ragwitz at 2026-10-07T18:00:32-07:00
Remove tcg_inst_meths in favour of a new IdDetails constructor
Thanks for this great suggestion, Sam! <3
- - - - -
86f16aea by Florian Ragwitz at 2026-10-07T18:00:32-07:00
Revert back to just using getOccString for DFunIds
- - - - -
12 changed files:
- compiler/GHC/Core/Opt/Specialise.hs
- compiler/GHC/CoreToIface.hs
- compiler/GHC/HsToCore.hs
- compiler/GHC/HsToCore/Ticks.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/Types/Id/Info.hs
- testsuite/tests/hpc/instmeths/instmeths.stdout
- testsuite/tests/simplCore/should_compile/T22375.stderr
- testsuite/tests/simplCore/should_compile/T22375DataFamily.stderr
Changes:
=====================================
compiler/GHC/Core/Opt/Specialise.hs
=====================================
@@ -3082,6 +3082,7 @@ wantCallsFor _env f
JoinId {} -> True
WorkerLikeId {} -> True
RepPolyId {} -> True
+ InstMethId {} -> True
interestingDict :: SpecEnv -> CoreExpr -> Bool
-- This is a subtle and important function
=====================================
compiler/GHC/CoreToIface.hs
=====================================
@@ -453,6 +453,7 @@ toIfaceTopBndr id
toIfaceIdDetails :: IdDetails -> IfaceIdDetails
toIfaceIdDetails VanillaId = IfVanillaId
+toIfaceIdDetails (InstMethId {}) = IfVanillaId
toIfaceIdDetails (WorkerLikeId dmds) = IfWorkerLikeId dmds
toIfaceIdDetails (DFunId {}) = IfDFunId
toIfaceIdDetails (RecSelId { sel_naughty = n
=====================================
compiler/GHC/HsToCore.hs
=====================================
@@ -147,7 +147,6 @@ deSugar hsc_env
tcg_tcs = tcs,
tcg_default_exports = defaults,
tcg_insts = insts,
- tcg_inst_meths = inst_meths,
tcg_fam_insts = fam_insts,
tcg_complete_matches = complete_matches,
tcg_self_boot = self_boot
@@ -172,7 +171,7 @@ deSugar hsc_env
(initTicksConfig (hsc_dflags hsc_env))
mod mod_loc
export_set (typeEnvTyCons type_env)
- insts inst_meths binds
+ insts binds
else return (binds, Nothing)
; let modBreaks
| Just (_, _, breakpointSpecs) <- m_tickInfo
=====================================
compiler/GHC/HsToCore/Ticks.hs
=====================================
@@ -1,4 +1,4 @@
-{-# LANGUAGE NondecreasingIndentation, DataKinds #-}
+{-# LANGUAGE NondecreasingIndentation, DataKinds, ViewPatterns #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
@@ -45,12 +45,12 @@ import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Types.Name.Set
import GHC.Types.Name
+import GHC.Types.Name.Env
import GHC.Types.CostCentre
import GHC.Types.CostCentre.State
import GHC.Types.Tickish
import GHC.Types.ProfAuto
import GHC.Tc.Types.ErrCtxt
-import GHC.Tc.Utils.TcType
import Control.Monad
import Data.List (isSuffixOf, intersperse)
@@ -105,14 +105,11 @@ addTicksToBinds
-- hasn't set it), so we have to work from this set.
-> [TyCon] -- ^ Type constructors in this module
-> [ClsInst] -- ^ Class instances in this module
- -> IdEnv DFunId -- ^ Mapping from class method Ids to the DFunIds
- -- of the class instance they belong to. See Note
- -- [Instance Method Coverage].
-> LHsBinds GhcTc
-> IO (LHsBinds GhcTc, Maybe (FilePath, SizedSeq Tick, SizedSeq Tick))
addTicksToBinds logger cfg
- mod mod_loc exports tyCons insts inst_meths binds
+ mod mod_loc exports tyCons insts binds
| let passes = ticks_passes cfg
, not (null passes)
, Just orig_file <- ml_hs_file mod_loc = do
@@ -137,8 +134,8 @@ addTicksToBinds logger cfg
, this_mod = mod
, tickishType = tickish
, recSelBinds = emptyVarEnv
- , instMeths = inst_meths
- , instTicks = emptyVarEnv
+ , instMeths = emptyVarEnv
+ , instTicks = emptyNameEnv
}
addTick = do
instTicks <- allocInstTicks insts
@@ -276,7 +273,9 @@ addTickLHsBind (L pos (XHsBindsLR bind@(AbsBinds { abs_binds = binds
env{ instMeths = instMeths env `extendVarEnvList`
[ (abe_mono, dfun)
| ABE{ abe_poly, abe_mono } <- abs_exports
- , Just dfun <- [lookupVarEnv (instMeths env) abe_poly] ] }
+ , Just dfun <- [instMeth abe_poly] ] }
+ where instMeth (idDetails -> InstMethId dfun) = Just dfun
+ instMeth id = lookupVarEnv (instMeths env) id
addTickLHsBind (L pos (funBind@(FunBind { fun_id = L _ id, fun_matches = matches }))) = do
let name = getOccString id
@@ -375,11 +374,9 @@ addTickLHsBind (L pos (funBind@(FunBind { fun_id = L _ id, fun_matches = matches
-- inherited and hand-written, we need to go out of our way to create top-level
-- tick boxes only for methods which correspond to user-written code.
--
--- To do so, 'addTicksToBinds' receives a mapping from class instance 'Id's to
--- the 'DFunId's of the dictionary backing the associated instance. When
--- creating tick boxes for top-level bindings, we can then decide if a given
--- 'FunBind' corresponds to an inherited/generated instance method of a class
--- and skip creating the tick box for it.
+-- Instance method 'Id's carry the name of the 'DFunId' of the instance they
+-- belong to. When creating tick boxes for top-level bindings, we can use this
+-- information to skip creating boxes for inherited/generated instance methods.
--
-- Additionally, we also want to inform the user whether or not their class
-- instance as a whole has been used at run-time. To do so, we create a single
@@ -1152,8 +1149,8 @@ data TickTransEnv = TTE { fileName :: FastString
, this_mod :: Module
, tickishType :: TickishType
, recSelBinds :: IdEnv DVarSet
- , instMeths :: IdEnv DFunId
- , instTicks :: IdEnv CoreTickish
+ , instMeths :: IdEnv Name
+ , instTicks :: NameEnv CoreTickish
}
-- deriving Show
@@ -1295,19 +1292,18 @@ isBlackListed GeneratedSrcSpan{} = return False
isBlackListed UnhelpfulSpan{} = return False
-- See Note [Instance Method Coverage].
-allocInstTicks :: [ClsInst] -> TM (IdEnv CoreTickish)
+allocInstTicks :: [ClsInst] -> TM (NameEnv CoreTickish)
allocInstTicks insts =
- ifDensity TickForCoverage (mkVarEnv . catMaybes <$> mapM alloc insts) (pure emptyVarEnv)
+ ifDensity TickForCoverage (mkNameEnv . catMaybes <$> mapM alloc insts) (pure emptyNameEnv)
where
alloc ClsInst{ is_dfun, is_cls }
| null (classMethods is_cls) = pure Nothing
- | otherwise = fmap (is_dfun,) <$> allocATickBox (TopLevelBox [s])
- False True (getSrcSpan is_dfun) noFVs
- where s = showSDocOneLine defaultSDocContext (pprSigmaType (idType is_dfun))
+ | otherwise = fmap (idName is_dfun,) <$> allocATickBox (TopLevelBox [getOccString is_dfun])
+ False True (getSrcSpan is_dfun) noFVs
-- See Note [Instance Method Coverage].
instMethTick :: Id -> TM (Maybe CoreTickish)
-instMethTick id = getEnv <&> \e -> lookupVarEnv (instMeths e) id >>= lookupVarEnv (instTicks e)
+instMethTick id = getEnv <&> \e -> lookupVarEnv (instMeths e) id >>= lookupNameEnv (instTicks e)
-- the tick application inherits the source position of its
-- expression argument to support nested box allocations
=====================================
compiler/GHC/Tc/Module.hs
=====================================
@@ -1768,7 +1768,7 @@ tcTopSrcDecls (HsGroup { hs_tyclds = tycl_decls,
-- Second pass over class and instance declarations,
-- now using the kind-checked decls
traceTc "Tc6" empty ;
- (inst_binds, inst_meths) <- tcInstDecls2 (tyClGroupTyClDecls tycl_decls) inst_infos ;
+ inst_binds <- tcInstDecls2 (tyClGroupTyClDecls tycl_decls) inst_infos ;
-- Foreign exports
traceTc "Tc7" empty ;
@@ -1800,9 +1800,8 @@ tcTopSrcDecls (HsGroup { hs_tyclds = tycl_decls,
, tcg_anns = tcg_anns tcg_env ++ annotations
, tcg_ann_env = extendAnnEnvList (tcg_ann_env tcg_env) annotations
, tcg_fords = tcg_fords tcg_env ++ foe_decls ++ fi_decls
- , tcg_dus = tcg_dus tcg_env `plusDU` usesOnly fo_fvs
+ , tcg_dus = tcg_dus tcg_env `plusDU` usesOnly fo_fvs } } ;
-- tcg_dus: see Note [Newtype constructor usage in foreign declarations]
- , tcg_inst_meths = tcg_inst_meths tcg_env `plusVarEnv` inst_meths } } ;
-- See Note [Newtype constructor usage in foreign declarations]
addUsedGREs NoDeprecationWarnings (bagToList fo_gres) ;
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -59,7 +59,7 @@ import GHC.Core.FamInstEnv
import GHC.Core.Type
import GHC.Core.Multiplicity
import GHC.Core.InstEnv
-import GHC.Core.Predicate( classMethodInstTy )
+import GHC.Core.Predicate( classMethodInstTy, isCoVarType )
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom
import GHC.Core.DataCon
@@ -72,6 +72,7 @@ import GHC.Types.Var.Set
import GHC.Types.Basic
import GHC.Types.ForeignCall ( typeCheckCType )
import GHC.Types.Id
+import GHC.Types.Id.Info
import GHC.Types.InlinePragma
import GHC.Types.SourceFile
import GHC.Types.SourceText
@@ -1285,7 +1286,7 @@ takes a slightly different approach.
********************************************************************* -}
tcInstDecls2 :: [LTyClDecl GhcRn] -> [InstInfo GhcRn]
- -> TcM (LHsBinds GhcTc, IdEnv DFunId)
+ -> TcM (LHsBinds GhcTc)
-- (a) From each class declaration,
-- generate any default-method bindings
-- (b) From each instance decl
@@ -1302,11 +1303,11 @@ tcInstDecls2 tycl_decls inst_decls
-- Add the default method Ids (again)
-- (they were already added in GHC.Tc.TyCl.Utils.tcAddImplicits)
-- See Note [Default methods in the type environment]
- ; (inst_binds_s, inst_meths_s) <- unzip <$> (tcExtendGlobalValEnv dm_ids $
- mapM tcInstDecl2 inst_decls)
+ ; inst_binds_s <- tcExtendGlobalValEnv dm_ids $
+ mapM tcInstDecl2 inst_decls
-- Done
- ; return (dm_binds ++ concat inst_binds_s, plusVarEnvList inst_meths_s) }
+ ; return (dm_binds ++ concat inst_binds_s) }
{- Note [Default methods in the type environment]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1322,12 +1323,12 @@ So right here in tcInstDecls2 we must re-extend the type envt with
the default method Ids replete with their INLINE pragmas. Urk.
-}
-tcInstDecl2 :: InstInfo GhcRn -> TcM (LHsBinds GhcTc, IdEnv DFunId)
+tcInstDecl2 :: InstInfo GhcRn -> TcM (LHsBinds GhcTc)
-- Returns a binding for the dfun
tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
- = recoverM (return (emptyLHsBinds, emptyVarEnv)) $
- setSrcSpan loc $
- addErrCtxt (instDeclCtxt2 dfun_ty) $
+ = recoverM (return emptyLHsBinds) $
+ setSrcSpan loc $
+ addErrCtxt (instDeclCtxt2 dfun_ty) $
do { -- Instantiate the instance decl with skolem constants
(skol_info, inst_tyvars, dfun_theta, clas, inst_tys) <- tcSkolDFunType dfun_ty
; dfun_ev_vars <- newEvVars dfun_theta
@@ -1345,7 +1346,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
-- See Note [Typechecking plan for instance declarations]
; dfun_ev_binds_var <- newTcEvBinds
; let dfun_ev_binds = TcEvBinds dfun_ev_binds_var
- ; (tclvl, (sc_meth_ids, sc_meth_binds, sc_meth_implics, meth_ids))
+ ; (tclvl, (sc_meth_ids, sc_meth_binds, sc_meth_implics))
<- pushTcLevelM $
do { (sc_ids, sc_binds, sc_implics)
<- tcSuperClasses skol_info dfun_id clas inst_tyvars
@@ -1359,8 +1360,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
; return ( sc_ids ++ meth_ids
, sc_binds ++ meth_binds
- , sc_implics `unionBags` meth_implics
- , meth_ids ) }
+ , sc_implics `unionBags` meth_implics ) }
; imp <- newImplication
; emitImplication $
@@ -1417,7 +1417,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
, abs_binds = [dict_bind]
, abs_sig = True }
- ; return (L loc' main_bind : sc_meth_binds, mkVarEnv $ (,dfun_id) <$> meth_ids)
+ ; return (L loc' main_bind : sc_meth_binds)
}
where
dfun_id = instanceDFunId ispec
@@ -1860,7 +1860,7 @@ tcMethods _skol_info dfun_id clas tyvars dfun_ev_vars inst_tys
tc_item :: ClassOpItem -> TcM (Id, LHsBind GhcTc, Maybe Implication)
tc_item (sel_id, dm_info)
| Just (user_bind, bndr_loc, prags) <- findMethodBind (idName sel_id) binds prag_fn
- = tcMethodBody False clas tyvars dfun_ev_vars inst_tys
+ = tcMethodBody False dfun_id clas tyvars dfun_ev_vars inst_tys
dfun_ev_binds is_derived hs_sig_fn
spec_inst_prags prags
sel_id user_bind bndr_loc
@@ -1880,7 +1880,7 @@ tcMethods _skol_info dfun_id clas tyvars dfun_ev_vars inst_tys
-- See Note [Implementation of Unsatisfiable constraints],
-- in GHC.Tc.Errors, point (D).
_ | (theta_id,unsat_msg) : _ <- unsat_thetas
- -> do { (meth_id, _) <- mkMethIds clas tyvars dfun_ev_vars
+ -> do { (meth_id, _) <- mkMethIds dfun_id clas tyvars dfun_ev_vars
inst_tys sel_id
; unsat_id <- tcLookupKnownKeyId unsatisfiableIdKey
-- Recall that unsatisfiable :: forall {rep} (msg :: ErrorMessage) (a :: TYPE rep). Unsatisfiable msg => a
@@ -1897,7 +1897,7 @@ tcMethods _skol_info dfun_id clas tyvars dfun_ev_vars inst_tys
Just (dm_name, dm_spec) ->
do { (meth_bind, inline_prags) <- mkDefMethBind inst_loc dfun_id clas sel_id dm_name dm_spec
; tcMethodBody (is_vanilla_dm dm_spec)
- clas tyvars dfun_ev_vars inst_tys
+ dfun_id clas tyvars dfun_ev_vars inst_tys
dfun_ev_binds is_derived hs_sig_fn
spec_inst_prags inline_prags
sel_id meth_bind inst_loc }
@@ -1905,7 +1905,7 @@ tcMethods _skol_info dfun_id clas tyvars dfun_ev_vars inst_tys
-- No default method
Nothing ->
do { traceTc "tc_def: warn" (ppr sel_id)
- ; (meth_id, _) <- mkMethIds clas tyvars dfun_ev_vars
+ ; (meth_id, _) <- mkMethIds dfun_id clas tyvars dfun_ev_vars
inst_tys sel_id
; dflags <- getDynFlags
-- Add a binding whose RHS is an error
@@ -2031,13 +2031,13 @@ Instead, we take the following approach:
tcMethodBody :: Bool -- True <=> This is a vanilla default method
-- See (TRC5) in Note [Tracking needed EvIds]
-- in GHC.Tc.Solver.Solve
- -> Class -> [TcTyVar] -> [EvVar] -> [TcType]
+ -> DFunId -> Class -> [TcTyVar] -> [EvVar] -> [TcType]
-> TcEvBinds -> Bool
-> HsSigFun
-> [LTcSpecPrag] -> [LSig GhcRn]
-> Id -> LHsBind GhcRn -> SrcSpan
-> TcM (TcId, LHsBind GhcTc, Maybe Implication)
-tcMethodBody is_vanilla_dm clas tyvars dfun_ev_vars inst_tys
+tcMethodBody is_vanilla_dm dfun_id clas tyvars dfun_ev_vars inst_tys
dfun_ev_binds is_derived
sig_fn spec_inst_prags prags
sel_id (L bind_loc meth_bind) bndr_loc
@@ -2045,7 +2045,7 @@ tcMethodBody is_vanilla_dm clas tyvars dfun_ev_vars inst_tys
do { traceTc "tcMethodBody" (ppr sel_id <+> ppr (idType sel_id) $$ ppr bndr_loc)
; let skol_info = MethSkol meth_name is_vanilla_dm
; (global_meth_id, local_meth_id) <- setSrcSpan bndr_loc $
- mkMethIds clas tyvars dfun_ev_vars
+ mkMethIds dfun_id clas tyvars dfun_ev_vars
inst_tys sel_id
; let lm_bind = meth_bind { fun_id = L (noAnnSrcSpan bndr_loc)
@@ -2163,16 +2163,19 @@ tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind
-- they are all for meth_id
------------------------
-mkMethIds :: Class -> [TcTyVar] -> [EvVar]
+mkMethIds :: DFunId -> Class -> [TcTyVar] -> [EvVar]
-> [TcType] -> Id -> TcM (TcId, TcId)
-- returns (poly_id, local_id), but ignoring any instance signature
-- See Note [Instance method signatures]
-mkMethIds clas tyvars dfun_ev_vars inst_tys sel_id
+mkMethIds dfun_id clas tyvars dfun_ev_vars inst_tys sel_id
= do { poly_meth_name <- newName (mkClassOpAuxOcc sel_occ)
; local_meth_name <- newName sel_occ
-- Base the local_meth_name on the selector name, because
-- type errors from tcMethodBody come from here
- ; let poly_meth_id = mkLocalId poly_meth_name ManyTy poly_meth_ty
+ ; let poly_meth_id =
+ assert (not (isCoVarType poly_meth_ty)) $
+ Var.mkLocalVar (InstMethId (idName dfun_id))
+ poly_meth_name ManyTy poly_meth_ty vanillaIdInfo
local_meth_id = mkLocalId local_meth_name ManyTy local_meth_ty
; return (poly_meth_id, local_meth_id) }
=====================================
compiler/GHC/Tc/Types.hs
=====================================
@@ -158,7 +158,6 @@ import GHC.Types.Name.Env
import GHC.Types.Name.Set
import GHC.Types.Avail
import GHC.Types.Var
-import GHC.Types.Var.Env
import GHC.Types.TypeEnv
import GHC.Types.SourceFile
import GHC.Types.SrcLoc
@@ -532,9 +531,6 @@ data TcGblEnv
-- NB. BangPattern is to fix a leak, see #15111
tcg_fam_inst_env :: !FamInstEnv, -- ^ Ditto for family instances
-- NB. BangPattern is to fix a leak, see #15111
- tcg_inst_meths :: IdEnv DFunId,
- -- ^ Maps instance method Ids to the DFunId of the instance they belong to.
- -- See Note [Instance Method Coverage] in GHC.HsToCore.Ticks.
tcg_ann_env :: AnnEnv, -- ^ And for annotations
tcg_complete_match_env :: CompleteMatches,
-- ^ The complete matches for all /home-package/ modules;
=====================================
compiler/GHC/Tc/Utils/Monad.hs
=====================================
@@ -409,7 +409,6 @@ initTcGblEnv hsc_env hsc_src keep_rn_syntax mod loc =
, tcg_knot_vars = hsc_type_env_vars hsc_env
, tcg_known_key_maps = known_key_maps_var
, tcg_inst_env = emptyInstEnv
- , tcg_inst_meths = emptyVarEnv
, tcg_fam_inst_env = emptyFamInstEnv
, tcg_ann_env = emptyAnnEnv
, tcg_complete_match_env = []
=====================================
compiler/GHC/Types/Id/Info.hs
=====================================
@@ -222,6 +222,9 @@ data IdDetails
-- - the [CbvMark] is always empty (and ignored) until after Tidy
-- for ids from the current module
-- - If non-empty, at least is isMarkedCbbv; see (CBV2)
+ | InstMethId Name
+ -- ^ An instance method. The 'Name' identifies the dictionary of the
+ -- instance it belongs to.
data RecSelInfo
= RSI { rsi_def :: [ConLike] -- Record selector defined for these
@@ -449,6 +452,7 @@ pprIdDetails other = brackets (pp other)
ppWhen is_naughty (text "(naughty)")
pp CoVarId = text "CoVarId"
pp (JoinId arity marks) = text "JoinId" <> parens (int arity) <> parens (ppr marks)
+ pp (InstMethId name) = text "InstMethId" <> parens (ppr name)
{-
************************************************************************
=====================================
testsuite/tests/hpc/instmeths/instmeths.stdout
=====================================
@@ -1,10 +1,10 @@
True
"Foo (T' a) instance"
-(1,"Eq a => Eq (T a)","Eq")
-(0,"Foo (T a)","Foo (T a)")
-(1,"Foo (T' a)","Foo (T' a)")
-(1,"Functor T","Functor")
-(0,"Show a => Show (T a)","Show")
+(1,"$fEqT","Eq")
+(0,"$fFooT","Foo (T a)")
+(1,"$fFooT'","Foo (T' a)")
+(1,"$fFunctorT","Functor")
+(0,"$fShowT","Show")
(0,"defMeth","defMeth = const \"class default\"")
(0,"defMeth","defMeth = const \"Foo (T' a) instance\"")
(0,"defMeth'","defMeth' = const \"class default\"")
=====================================
testsuite/tests/simplCore/should_compile/T22375.stderr
=====================================
@@ -5,7 +5,7 @@ Result size of Tidy Core
-- RHS size: {terms: 14, types: 9, coercions: 0, joins: 0/0}
T22375.$fEqX_$c== :: X -> X -> Bool
-[GblId,
+[GblId[InstMethId(T22375.$fEqX)],
Arity=2,
Str=<SL><SL>,
Unf=Unf{Src=<vanilla>, TopLvl=True,
@@ -27,7 +27,7 @@ T22375.$fEqX_$c==
-- RHS size: {terms: 18, types: 9, coercions: 0, joins: 0/0}
T22375.$fEqX_$c/= [InlPrag=INLINE (sat-args=2)] :: X -> X -> Bool
-[GblId,
+[GblId[InstMethId(T22375.$fEqX)],
Arity=2,
Str=<SL><SL>,
Unf=Unf{Src=StableUser, TopLvl=True,
=====================================
testsuite/tests/simplCore/should_compile/T22375DataFamily.stderr
=====================================
@@ -5,7 +5,7 @@ Result size of Tidy Core
-- RHS size: {terms: 14, types: 11, coercions: 2, joins: 0/0}
T22375DataFamily.$fEqX_$c== :: X () -> X () -> Bool
-[GblId,
+[GblId[InstMethId(T22375DataFamily.$fEqX)],
Arity=2,
Str=<SL><SL>,
Unf=Unf{Src=<vanilla>, TopLvl=True,
@@ -36,7 +36,7 @@ T22375DataFamily.$fEqX_$c==
-- RHS size: {terms: 18, types: 11, coercions: 2, joins: 0/0}
T22375DataFamily.$fEqX_$c/= [InlPrag=INLINE (sat-args=2)]
:: X () -> X () -> Bool
-[GblId,
+[GblId[InstMethId(T22375DataFamily.$fEqX)],
Arity=2,
Str=<SL><SL>,
Unf=Unf{Src=StableUser, TopLvl=True,
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/1e0330f0f9a405717d5739c3ef5f3e…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/1e0330f0f9a405717d5739c3ef5f3e…
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
07 Oct '26
Simon Peyton Jones pushed to branch wip/T27828 at Glasgow Haskell Compiler / GHC
Commits:
0f09fad1 by Simon Peyton Jones at 2026-10-07T23:42: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 are 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 or 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.Core.TyCo.Subst( elemSubst, extendTvSubstWithClone )
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,27 @@ 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]
+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 = go_fresh subst tv tvs
+
+ -- Using an auxiliary function here to avoid prematurely forcing
+ -- the (banged) recursive call to `go` in the non-fresh case
+ go_fresh subst tv tvs = (subst'', tv':tvs')
+ where
+ !(subst'', tvs') = go subst' tvs
+ tv' = tv `setTyVarKind` substTy subst (tyVarKind tv)
+ subst' = extendTvSubstWithClone subst tv tv'
+ -- extendTvSubstWithClone: see (OF1b) in
+ -- Note [Exploiting open type families]
+
-----------------------------------------
-- Built-in type families
@@ -924,15 +951,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 +977,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))
-
- 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`.
-
-(TIF2) All this applies equally to /closed/ type families; it is /not/
- subsumed by Note [Exploiting closed type families]. Consider:
+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
+
+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:
+
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 +1015,10 @@ iff
(R2) There is no earlier equation that matches S(lhs). See (RW4) below.
+The relevance check is implemented by `getRelevantBranches`, which actually
+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 +1041,130 @@ 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.
-
-Note [Exploiting closed type families]
+ 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 T27828a:
+ 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 = r | r -> a
+ type instance F [a] = a->a
+
+ [W] F alpha ~ Int->Int
+
+Then, since F has been checked as injective, and the RHS `a->a` (pre-)unifies
+with the `Int->Int` in the Wanted with substitution [a :-> Int], we can
+add a derived FunDepEqns
+ FDEqns{ fd_qtvs = [], fd_eqs = [ [Int] ~ alpha ] }
+and thereby emit (via `instantiateFunDepEqns`)
+ [W] [Int] ~ alpha
+
+Things are a bit trickier when not all the quantified variables of the
+instance are bound by the pre-unification step. Suppose we have
+
+ type family F a = r | r -> a
+ type instance F (Maybe a) = [G a] -- G is a type family
+
+ [W] F alpha ~ [ty]
+
+Then, the RHS [G a] pre-unifies with the RHS of the Wanted, but with an
+empty substitution, which does not fix `a`. So we get this FunDepEqns:
+ FDEqns{ fd_qtvs = a, fd_eqs = [ Maybe a ~ alpha ] }
+(note the fd_qtvs=a) and thereby emit (via `instantiateFunDepEqns`)
+ [W] Maybe gamma ~ alpha -- Fresh gamma
+We have learned that `alpha` must be a list, but that is all; we don't
+know what is inside it, hence the fresh `gamma`.
+
+In general we have:
+
+ type family F x1 ... xn = r | r -> x1 x3 (say)
+ type instance forall qs. F t1 ... tn = rhs
+ [W] F a1 ... an ~ b
+
+Suppose `b` pre-unifies with `rhs`, with substitution `S` that binds
+some (but perhaps not all) of the `qs`. Lets say
+ unbound_qs = qs \ dom(S)
+
+Then we generate the FunDepEqs
+ FDEqns{ fd_qtvs = unbound_qs
+ , fd_eqs = [ S(t1) ~ S(a1), S(t3) ~ S(a3) ]
+
+These 'fd_qtvs' are subsequently instantiated to fresh metavariables by
+'instantiateFunDepEqns'.
+
+(OF1) The computation of `unbound_qs` is done by `trim_qtvs`, but we
+ have to be careful. Suppose (OF1a)
+ qs = [ k::*, a::k ]
+ S = [ k :-> UnliftedType ]
+ Then we want
+ unbound_qs = [ a::UnliftedType ] -- Must apply S to q's kind!!
+
+ And (OF1b), although I'm not sure if this can acutally happen:
+ qs = [ k::*, a::(k::*), b::(a::k) ]
+ S = [ k :-> UnliftedType ]
+ We want
+ unbound_qs = [ a::UnliftedType, b::(a::UnliftedType) ]
+ Note that the occurrence of `a` in b's kind should be replaced by the
+ newly-kinded `a` not the original `a::k`.
+
+ 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 `a` that is /not/ matched
+ * Adds the substitution [a::k :-> a::S(k)] to the substitution
+
+Note [Exploiting closed type families] see `mkTopClosedFamEqFDs`
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
type family F a b where
@@ -1042,17 +1175,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 +1194,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 +1303,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 +1335,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 +1343,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 +1388,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 open 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 family 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 +1504,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 T27828b 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/0f09fad1bd63b1e9c2f5d76cecda440…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0f09fad1bd63b1e9c2f5d76cecda440…
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] 2 commits: Remove tcg_inst_meths in favour of a new IdDetails constructor
by Florian Ragwitz (＠rafl) 07 Oct '26
by Florian Ragwitz (＠rafl) 07 Oct '26
07 Oct '26
Florian Ragwitz pushed to branch wip/rafl/hpc-instances at Glasgow Haskell Compiler / GHC
Commits:
5dd9f195 by Florian Ragwitz at 2026-10-07T11:04:51-07:00
Remove tcg_inst_meths in favour of a new IdDetails constructor
Thanks for this great suggestion, Sam! <3
- - - - -
1e0330f0 by Florian Ragwitz at 2026-10-07T11:04:51-07:00
Revert back to just using getOccString for DFunIds
- - - - -
10 changed files:
- compiler/GHC/Core/Opt/Specialise.hs
- compiler/GHC/CoreToIface.hs
- compiler/GHC/HsToCore.hs
- compiler/GHC/HsToCore/Ticks.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/Types/Id/Info.hs
- testsuite/tests/hpc/instmeths/instmeths.stdout
Changes:
=====================================
compiler/GHC/Core/Opt/Specialise.hs
=====================================
@@ -3082,6 +3082,7 @@ wantCallsFor _env f
JoinId {} -> True
WorkerLikeId {} -> True
RepPolyId {} -> True
+ InstMethId {} -> True
interestingDict :: SpecEnv -> CoreExpr -> Bool
-- This is a subtle and important function
=====================================
compiler/GHC/CoreToIface.hs
=====================================
@@ -453,6 +453,7 @@ toIfaceTopBndr id
toIfaceIdDetails :: IdDetails -> IfaceIdDetails
toIfaceIdDetails VanillaId = IfVanillaId
+toIfaceIdDetails (InstMethId {}) = IfVanillaId
toIfaceIdDetails (WorkerLikeId dmds) = IfWorkerLikeId dmds
toIfaceIdDetails (DFunId {}) = IfDFunId
toIfaceIdDetails (RecSelId { sel_naughty = n
=====================================
compiler/GHC/HsToCore.hs
=====================================
@@ -147,7 +147,6 @@ deSugar hsc_env
tcg_tcs = tcs,
tcg_default_exports = defaults,
tcg_insts = insts,
- tcg_inst_meths = inst_meths,
tcg_fam_insts = fam_insts,
tcg_complete_matches = complete_matches,
tcg_self_boot = self_boot
@@ -172,7 +171,7 @@ deSugar hsc_env
(initTicksConfig (hsc_dflags hsc_env))
mod mod_loc
export_set (typeEnvTyCons type_env)
- insts inst_meths binds
+ insts binds
else return (binds, Nothing)
; let modBreaks
| Just (_, _, breakpointSpecs) <- m_tickInfo
=====================================
compiler/GHC/HsToCore/Ticks.hs
=====================================
@@ -1,4 +1,4 @@
-{-# LANGUAGE NondecreasingIndentation, DataKinds #-}
+{-# LANGUAGE NondecreasingIndentation, DataKinds, ViewPatterns #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
@@ -45,12 +45,12 @@ import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Types.Name.Set
import GHC.Types.Name
+import GHC.Types.Name.Env
import GHC.Types.CostCentre
import GHC.Types.CostCentre.State
import GHC.Types.Tickish
import GHC.Types.ProfAuto
import GHC.Tc.Types.ErrCtxt
-import GHC.Tc.Utils.TcType
import Control.Monad
import Data.List (isSuffixOf, intersperse)
@@ -105,14 +105,11 @@ addTicksToBinds
-- hasn't set it), so we have to work from this set.
-> [TyCon] -- ^ Type constructors in this module
-> [ClsInst] -- ^ Class instances in this module
- -> IdEnv DFunId -- ^ Mapping from class method Ids to the DFunIds
- -- of the class instance they belong to. See Note
- -- [Instance Method Coverage].
-> LHsBinds GhcTc
-> IO (LHsBinds GhcTc, Maybe (FilePath, SizedSeq Tick, SizedSeq Tick))
addTicksToBinds logger cfg
- mod mod_loc exports tyCons insts inst_meths binds
+ mod mod_loc exports tyCons insts binds
| let passes = ticks_passes cfg
, not (null passes)
, Just orig_file <- ml_hs_file mod_loc = do
@@ -137,8 +134,8 @@ addTicksToBinds logger cfg
, this_mod = mod
, tickishType = tickish
, recSelBinds = emptyVarEnv
- , instMeths = inst_meths
- , instTicks = emptyVarEnv
+ , instMeths = emptyVarEnv
+ , instTicks = emptyNameEnv
}
addTick = do
instTicks <- allocInstTicks insts
@@ -276,7 +273,9 @@ addTickLHsBind (L pos (XHsBindsLR bind@(AbsBinds { abs_binds = binds
env{ instMeths = instMeths env `extendVarEnvList`
[ (abe_mono, dfun)
| ABE{ abe_poly, abe_mono } <- abs_exports
- , Just dfun <- [lookupVarEnv (instMeths env) abe_poly] ] }
+ , Just dfun <- [instMeth abe_poly] ] }
+ where instMeth (idDetails -> InstMethId dfun) = Just dfun
+ instMeth id = lookupVarEnv (instMeths env) id
addTickLHsBind (L pos (funBind@(FunBind { fun_id = L _ id, fun_matches = matches }))) = do
let name = getOccString id
@@ -375,11 +374,9 @@ addTickLHsBind (L pos (funBind@(FunBind { fun_id = L _ id, fun_matches = matches
-- inherited and hand-written, we need to go out of our way to create top-level
-- tick boxes only for methods which correspond to user-written code.
--
--- To do so, 'addTicksToBinds' receives a mapping from class instance 'Id's to
--- the 'DFunId's of the dictionary backing the associated instance. When
--- creating tick boxes for top-level bindings, we can then decide if a given
--- 'FunBind' corresponds to an inherited/generated instance method of a class
--- and skip creating the tick box for it.
+-- Instance method 'Id's carry the name of the 'DFunId' of the instance they
+-- belong to. When creating tick boxes for top-level bindings, we can use this
+-- information to skip creating boxes for inherited/generated instance methods.
--
-- Additionally, we also want to inform the user whether or not their class
-- instance as a whole has been used at run-time. To do so, we create a single
@@ -1152,8 +1149,8 @@ data TickTransEnv = TTE { fileName :: FastString
, this_mod :: Module
, tickishType :: TickishType
, recSelBinds :: IdEnv DVarSet
- , instMeths :: IdEnv DFunId
- , instTicks :: IdEnv CoreTickish
+ , instMeths :: IdEnv Name
+ , instTicks :: NameEnv CoreTickish
}
-- deriving Show
@@ -1295,19 +1292,18 @@ isBlackListed GeneratedSrcSpan{} = return False
isBlackListed UnhelpfulSpan{} = return False
-- See Note [Instance Method Coverage].
-allocInstTicks :: [ClsInst] -> TM (IdEnv CoreTickish)
+allocInstTicks :: [ClsInst] -> TM (NameEnv CoreTickish)
allocInstTicks insts =
- ifDensity TickForCoverage (mkVarEnv . catMaybes <$> mapM alloc insts) (pure emptyVarEnv)
+ ifDensity TickForCoverage (mkNameEnv . catMaybes <$> mapM alloc insts) (pure emptyNameEnv)
where
alloc ClsInst{ is_dfun, is_cls }
| null (classMethods is_cls) = pure Nothing
- | otherwise = fmap (is_dfun,) <$> allocATickBox (TopLevelBox [s])
- False True (getSrcSpan is_dfun) noFVs
- where s = showSDocOneLine defaultSDocContext (pprSigmaType (idType is_dfun))
+ | otherwise = fmap (idName is_dfun,) <$> allocATickBox (TopLevelBox [getOccString is_dfun])
+ False True (getSrcSpan is_dfun) noFVs
-- See Note [Instance Method Coverage].
instMethTick :: Id -> TM (Maybe CoreTickish)
-instMethTick id = getEnv <&> \e -> lookupVarEnv (instMeths e) id >>= lookupVarEnv (instTicks e)
+instMethTick id = getEnv <&> \e -> lookupVarEnv (instMeths e) id >>= lookupNameEnv (instTicks e)
-- the tick application inherits the source position of its
-- expression argument to support nested box allocations
=====================================
compiler/GHC/Tc/Module.hs
=====================================
@@ -1768,7 +1768,7 @@ tcTopSrcDecls (HsGroup { hs_tyclds = tycl_decls,
-- Second pass over class and instance declarations,
-- now using the kind-checked decls
traceTc "Tc6" empty ;
- (inst_binds, inst_meths) <- tcInstDecls2 (tyClGroupTyClDecls tycl_decls) inst_infos ;
+ inst_binds <- tcInstDecls2 (tyClGroupTyClDecls tycl_decls) inst_infos ;
-- Foreign exports
traceTc "Tc7" empty ;
@@ -1800,9 +1800,8 @@ tcTopSrcDecls (HsGroup { hs_tyclds = tycl_decls,
, tcg_anns = tcg_anns tcg_env ++ annotations
, tcg_ann_env = extendAnnEnvList (tcg_ann_env tcg_env) annotations
, tcg_fords = tcg_fords tcg_env ++ foe_decls ++ fi_decls
- , tcg_dus = tcg_dus tcg_env `plusDU` usesOnly fo_fvs
+ , tcg_dus = tcg_dus tcg_env `plusDU` usesOnly fo_fvs } } ;
-- tcg_dus: see Note [Newtype constructor usage in foreign declarations]
- , tcg_inst_meths = tcg_inst_meths tcg_env `plusVarEnv` inst_meths } } ;
-- See Note [Newtype constructor usage in foreign declarations]
addUsedGREs NoDeprecationWarnings (bagToList fo_gres) ;
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -59,7 +59,7 @@ import GHC.Core.FamInstEnv
import GHC.Core.Type
import GHC.Core.Multiplicity
import GHC.Core.InstEnv
-import GHC.Core.Predicate( classMethodInstTy )
+import GHC.Core.Predicate( classMethodInstTy, isCoVarType )
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom
import GHC.Core.DataCon
@@ -72,6 +72,7 @@ import GHC.Types.Var.Set
import GHC.Types.Basic
import GHC.Types.ForeignCall ( typeCheckCType )
import GHC.Types.Id
+import GHC.Types.Id.Info
import GHC.Types.InlinePragma
import GHC.Types.SourceFile
import GHC.Types.SourceText
@@ -1285,7 +1286,7 @@ takes a slightly different approach.
********************************************************************* -}
tcInstDecls2 :: [LTyClDecl GhcRn] -> [InstInfo GhcRn]
- -> TcM (LHsBinds GhcTc, IdEnv DFunId)
+ -> TcM (LHsBinds GhcTc)
-- (a) From each class declaration,
-- generate any default-method bindings
-- (b) From each instance decl
@@ -1302,11 +1303,11 @@ tcInstDecls2 tycl_decls inst_decls
-- Add the default method Ids (again)
-- (they were already added in GHC.Tc.TyCl.Utils.tcAddImplicits)
-- See Note [Default methods in the type environment]
- ; (inst_binds_s, inst_meths_s) <- unzip <$> (tcExtendGlobalValEnv dm_ids $
- mapM tcInstDecl2 inst_decls)
+ ; inst_binds_s <- tcExtendGlobalValEnv dm_ids $
+ mapM tcInstDecl2 inst_decls
-- Done
- ; return (dm_binds ++ concat inst_binds_s, plusVarEnvList inst_meths_s) }
+ ; return (dm_binds ++ concat inst_binds_s) }
{- Note [Default methods in the type environment]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1322,12 +1323,12 @@ So right here in tcInstDecls2 we must re-extend the type envt with
the default method Ids replete with their INLINE pragmas. Urk.
-}
-tcInstDecl2 :: InstInfo GhcRn -> TcM (LHsBinds GhcTc, IdEnv DFunId)
+tcInstDecl2 :: InstInfo GhcRn -> TcM (LHsBinds GhcTc)
-- Returns a binding for the dfun
tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
- = recoverM (return (emptyLHsBinds, emptyVarEnv)) $
- setSrcSpan loc $
- addErrCtxt (instDeclCtxt2 dfun_ty) $
+ = recoverM (return emptyLHsBinds) $
+ setSrcSpan loc $
+ addErrCtxt (instDeclCtxt2 dfun_ty) $
do { -- Instantiate the instance decl with skolem constants
(skol_info, inst_tyvars, dfun_theta, clas, inst_tys) <- tcSkolDFunType dfun_ty
; dfun_ev_vars <- newEvVars dfun_theta
@@ -1345,7 +1346,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
-- See Note [Typechecking plan for instance declarations]
; dfun_ev_binds_var <- newTcEvBinds
; let dfun_ev_binds = TcEvBinds dfun_ev_binds_var
- ; (tclvl, (sc_meth_ids, sc_meth_binds, sc_meth_implics, meth_ids))
+ ; (tclvl, (sc_meth_ids, sc_meth_binds, sc_meth_implics))
<- pushTcLevelM $
do { (sc_ids, sc_binds, sc_implics)
<- tcSuperClasses skol_info dfun_id clas inst_tyvars
@@ -1359,8 +1360,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
; return ( sc_ids ++ meth_ids
, sc_binds ++ meth_binds
- , sc_implics `unionBags` meth_implics
- , meth_ids ) }
+ , sc_implics `unionBags` meth_implics ) }
; imp <- newImplication
; emitImplication $
@@ -1417,7 +1417,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
, abs_binds = [dict_bind]
, abs_sig = True }
- ; return (L loc' main_bind : sc_meth_binds, mkVarEnv $ (,dfun_id) <$> meth_ids)
+ ; return (L loc' main_bind : sc_meth_binds)
}
where
dfun_id = instanceDFunId ispec
@@ -1860,7 +1860,7 @@ tcMethods _skol_info dfun_id clas tyvars dfun_ev_vars inst_tys
tc_item :: ClassOpItem -> TcM (Id, LHsBind GhcTc, Maybe Implication)
tc_item (sel_id, dm_info)
| Just (user_bind, bndr_loc, prags) <- findMethodBind (idName sel_id) binds prag_fn
- = tcMethodBody False clas tyvars dfun_ev_vars inst_tys
+ = tcMethodBody False dfun_id clas tyvars dfun_ev_vars inst_tys
dfun_ev_binds is_derived hs_sig_fn
spec_inst_prags prags
sel_id user_bind bndr_loc
@@ -1880,7 +1880,7 @@ tcMethods _skol_info dfun_id clas tyvars dfun_ev_vars inst_tys
-- See Note [Implementation of Unsatisfiable constraints],
-- in GHC.Tc.Errors, point (D).
_ | (theta_id,unsat_msg) : _ <- unsat_thetas
- -> do { (meth_id, _) <- mkMethIds clas tyvars dfun_ev_vars
+ -> do { (meth_id, _) <- mkMethIds dfun_id clas tyvars dfun_ev_vars
inst_tys sel_id
; unsat_id <- tcLookupKnownKeyId unsatisfiableIdKey
-- Recall that unsatisfiable :: forall {rep} (msg :: ErrorMessage) (a :: TYPE rep). Unsatisfiable msg => a
@@ -1897,7 +1897,7 @@ tcMethods _skol_info dfun_id clas tyvars dfun_ev_vars inst_tys
Just (dm_name, dm_spec) ->
do { (meth_bind, inline_prags) <- mkDefMethBind inst_loc dfun_id clas sel_id dm_name dm_spec
; tcMethodBody (is_vanilla_dm dm_spec)
- clas tyvars dfun_ev_vars inst_tys
+ dfun_id clas tyvars dfun_ev_vars inst_tys
dfun_ev_binds is_derived hs_sig_fn
spec_inst_prags inline_prags
sel_id meth_bind inst_loc }
@@ -1905,7 +1905,7 @@ tcMethods _skol_info dfun_id clas tyvars dfun_ev_vars inst_tys
-- No default method
Nothing ->
do { traceTc "tc_def: warn" (ppr sel_id)
- ; (meth_id, _) <- mkMethIds clas tyvars dfun_ev_vars
+ ; (meth_id, _) <- mkMethIds dfun_id clas tyvars dfun_ev_vars
inst_tys sel_id
; dflags <- getDynFlags
-- Add a binding whose RHS is an error
@@ -2031,13 +2031,13 @@ Instead, we take the following approach:
tcMethodBody :: Bool -- True <=> This is a vanilla default method
-- See (TRC5) in Note [Tracking needed EvIds]
-- in GHC.Tc.Solver.Solve
- -> Class -> [TcTyVar] -> [EvVar] -> [TcType]
+ -> DFunId -> Class -> [TcTyVar] -> [EvVar] -> [TcType]
-> TcEvBinds -> Bool
-> HsSigFun
-> [LTcSpecPrag] -> [LSig GhcRn]
-> Id -> LHsBind GhcRn -> SrcSpan
-> TcM (TcId, LHsBind GhcTc, Maybe Implication)
-tcMethodBody is_vanilla_dm clas tyvars dfun_ev_vars inst_tys
+tcMethodBody is_vanilla_dm dfun_id clas tyvars dfun_ev_vars inst_tys
dfun_ev_binds is_derived
sig_fn spec_inst_prags prags
sel_id (L bind_loc meth_bind) bndr_loc
@@ -2045,7 +2045,7 @@ tcMethodBody is_vanilla_dm clas tyvars dfun_ev_vars inst_tys
do { traceTc "tcMethodBody" (ppr sel_id <+> ppr (idType sel_id) $$ ppr bndr_loc)
; let skol_info = MethSkol meth_name is_vanilla_dm
; (global_meth_id, local_meth_id) <- setSrcSpan bndr_loc $
- mkMethIds clas tyvars dfun_ev_vars
+ mkMethIds dfun_id clas tyvars dfun_ev_vars
inst_tys sel_id
; let lm_bind = meth_bind { fun_id = L (noAnnSrcSpan bndr_loc)
@@ -2163,16 +2163,19 @@ tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind
-- they are all for meth_id
------------------------
-mkMethIds :: Class -> [TcTyVar] -> [EvVar]
+mkMethIds :: DFunId -> Class -> [TcTyVar] -> [EvVar]
-> [TcType] -> Id -> TcM (TcId, TcId)
-- returns (poly_id, local_id), but ignoring any instance signature
-- See Note [Instance method signatures]
-mkMethIds clas tyvars dfun_ev_vars inst_tys sel_id
+mkMethIds dfun_id clas tyvars dfun_ev_vars inst_tys sel_id
= do { poly_meth_name <- newName (mkClassOpAuxOcc sel_occ)
; local_meth_name <- newName sel_occ
-- Base the local_meth_name on the selector name, because
-- type errors from tcMethodBody come from here
- ; let poly_meth_id = mkLocalId poly_meth_name ManyTy poly_meth_ty
+ ; let poly_meth_id =
+ assert (not (isCoVarType poly_meth_ty)) $
+ Var.mkLocalVar (InstMethId (idName dfun_id))
+ poly_meth_name ManyTy poly_meth_ty vanillaIdInfo
local_meth_id = mkLocalId local_meth_name ManyTy local_meth_ty
; return (poly_meth_id, local_meth_id) }
=====================================
compiler/GHC/Tc/Types.hs
=====================================
@@ -158,7 +158,6 @@ import GHC.Types.Name.Env
import GHC.Types.Name.Set
import GHC.Types.Avail
import GHC.Types.Var
-import GHC.Types.Var.Env
import GHC.Types.TypeEnv
import GHC.Types.SourceFile
import GHC.Types.SrcLoc
@@ -532,9 +531,6 @@ data TcGblEnv
-- NB. BangPattern is to fix a leak, see #15111
tcg_fam_inst_env :: !FamInstEnv, -- ^ Ditto for family instances
-- NB. BangPattern is to fix a leak, see #15111
- tcg_inst_meths :: IdEnv DFunId,
- -- ^ Maps instance method Ids to the DFunId of the instance they belong to.
- -- See Note [Instance Method Coverage] in GHC.HsToCore.Ticks.
tcg_ann_env :: AnnEnv, -- ^ And for annotations
tcg_complete_match_env :: CompleteMatches,
-- ^ The complete matches for all /home-package/ modules;
=====================================
compiler/GHC/Tc/Utils/Monad.hs
=====================================
@@ -409,7 +409,6 @@ initTcGblEnv hsc_env hsc_src keep_rn_syntax mod loc =
, tcg_knot_vars = hsc_type_env_vars hsc_env
, tcg_known_key_maps = known_key_maps_var
, tcg_inst_env = emptyInstEnv
- , tcg_inst_meths = emptyVarEnv
, tcg_fam_inst_env = emptyFamInstEnv
, tcg_ann_env = emptyAnnEnv
, tcg_complete_match_env = []
=====================================
compiler/GHC/Types/Id/Info.hs
=====================================
@@ -222,6 +222,9 @@ data IdDetails
-- - the [CbvMark] is always empty (and ignored) until after Tidy
-- for ids from the current module
-- - If non-empty, at least is isMarkedCbbv; see (CBV2)
+ | InstMethId Name
+ -- ^ An instance method. The 'Name' identifies the dictionary of the
+ -- instance it belongs to.
data RecSelInfo
= RSI { rsi_def :: [ConLike] -- Record selector defined for these
@@ -449,6 +452,7 @@ pprIdDetails other = brackets (pp other)
ppWhen is_naughty (text "(naughty)")
pp CoVarId = text "CoVarId"
pp (JoinId arity marks) = text "JoinId" <> parens (int arity) <> parens (ppr marks)
+ pp (InstMethId name) = text "InstMethId" <> parens (ppr name)
{-
************************************************************************
=====================================
testsuite/tests/hpc/instmeths/instmeths.stdout
=====================================
@@ -1,10 +1,10 @@
True
"Foo (T' a) instance"
-(1,"Eq a => Eq (T a)","Eq")
-(0,"Foo (T a)","Foo (T a)")
-(1,"Foo (T' a)","Foo (T' a)")
-(1,"Functor T","Functor")
-(0,"Show a => Show (T a)","Show")
+(1,"$fEqT","Eq")
+(0,"$fFooT","Foo (T a)")
+(1,"$fFooT'","Foo (T' a)")
+(1,"$fFunctorT","Functor")
+(0,"$fShowT","Show")
(0,"defMeth","defMeth = const \"class default\"")
(0,"defMeth","defMeth = const \"Foo (T' a) instance\"")
(0,"defMeth'","defMeth' = const \"class default\"")
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/dd907dc6ba4b38eba8db6d61d588b9…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/dd907dc6ba4b38eba8db6d61d588b9…
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/apk/tag-strict-bot] Fix a few tag inference bugs.
by Andreas Klebinger (＠AndreasK) 07 Oct '26
by Andreas Klebinger (＠AndreasK) 07 Oct '26
07 Oct '26
Andreas Klebinger pushed to branch wip/apk/tag-strict-bot at Glasgow Haskell Compiler / GHC
Commits:
42b5c293 by Andreas Klebinger at 2026-10-07T17:14:49+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.
- - - - -
24 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/TagSig.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 NOT thunks.
+ , 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
@@ -593,7 +601,7 @@ initSig (bndr, StgRhsClosure _ _ _ bndrs _ _)
{- Note [Bottom functions are TagBottoming]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If we have a function with two branches with one
+If we have a function with two branches with one branch
being bottom, and the other returning a tagged
unboxed tuple what is the result? We give it TagBottoming!
To answer why consider this function:
@@ -603,21 +611,40 @@ foo x = case x of
True -> (# True,True #)
False -> undefined
-The true branch is obviously tagged. The other branch isn't.
-We want to treat the *result* of foo as tagged as well so that
-the combination of the branches also is tagged if all non-bottom
-branches are tagged.
-This is safe because the function is still always called/entered as long
-as it's applied to arguments. Since the function will never return we can give
-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.
+The true branch obviously returns tagged components. The other branch is bottom.
+We want to treat the components in the *result* returned by foo as tagged.
+Because at a call site like:
+
+ case foo e of
+ (# x, y #) ->
+ case x of
+ ...
+
+Either `foo` will have evaluated undefined or blown up. Or we will bind x and y
+to tagged pointers. A fact we take advantage of to optimize `case x of`.
+
+The rule is then simple. A combination of the alternatives of the same case has
+tagged components if all non-bottom branches have tagged components.
+
+To represent the bottoming alternatives we use TagBottoming. Which says all it's
+components are tagged. Now the same is true if we have:
+
+foo :: Bool -> (# Bool, Bool #)
+foo x = case x of
+ True -> (# True,True #)
+ False -> willCrash x
+
+Where we want to check:
-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:
+* Is `willCrash x` bottom?
+* If it is not are the returned components tagged?
- case bottom_id of { ...}
+For the first question we have to be careful about the notion of bottom we use.
+I've got this wrong in the past, because a underapplied bottoming function will
+return a *function* as result. Rather than being bottom.
+If the function *is* bottom then we treat it the same we do undefined above. And
+use TagBottoming as the tagInfo of the expression. Hence the title of the Note.
-}
-----------------------------
=====================================
compiler/GHC/Stg/EnforceEpt/Rewrite.hs
=====================================
@@ -3,6 +3,7 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnboxedTuples #-}
module GHC.Stg.EnforceEpt.Rewrite (rewriteTopBinds, rewriteOpApp)
where
@@ -13,7 +14,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 +23,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
@@ -34,15 +32,48 @@ import GHC.Data.Maybe
import GHC.Utils.Panic
import GHC.Utils.Outputable
-import GHC.Utils.Monad.State.Strict
import GHC.Utils.Misc
import GHC.Stg.EnforceEpt.Types
import Control.Monad
-
-newtype RM a = RM { unRM :: (State (UniqFM Id TagSig, UniqSupply, Module, IdSet) a) }
- deriving (Functor, Monad, Applicative)
+import GHC.Exts (oneShot)
+
+data RmContext = RmContext { rm_mod :: !Module, rm_interpreter :: !Bool }
+
+data RmState = RmState { rm_us :: !UniqSupply, rm_fvs :: IdSet, rm_sig_env :: !(UniqFM Id TagSig)}
+newtype RM a = RM { unRM :: RmContext -> RmState -> (# RmState, a #) }
+
+instance Functor RM where
+ fmap f (RM x) = RM $ oneShot $ \env -> oneShot $ \state ->
+ case x env state of
+ (# !s1, !x' #) ->
+ let !r = f x'
+ in (# s1, r #)
+
+instance Applicative RM where
+ (RM f) <*> (RM x) = RM $ oneShot $ \env -> oneShot $ \state ->
+ case f env state of
+ (# !s1,!f' #) -> case x env s1 of
+ (# !s2, !x' #) ->
+ let !r = f' x'
+ in (# s2, r #)
+ pure !x = RM $ \_ !s -> (# s, x #)
+
+-- See Note [The one-shot state monad trick] in GHC.Utils.Monad
+instance Monad RM where
+ RM x >>= f = RM $ oneShot $ \env -> oneShot $ \state ->
+ case x env state of
+ (# !s1, !x' #) -> case (f x') of RM r -> r env s1
+
+-- | runRM this_mod for_bytecode us
+runRM :: Module -> Bool -> UniqSupply -> RM a -> a
+runRM mod for_bytecode us act =
+ case (unRM act)
+ (RmContext { rm_mod = mod, rm_interpreter = for_bytecode })
+ (RmState { rm_us = us, rm_fvs = emptyVarSet, rm_sig_env = emptyUFM })
+ of
+ (# _, r #) -> r
------------------------------------------------------------
-- Add cases around strict fields where required.
@@ -107,30 +138,29 @@ when building the free variable list.
--------------------------------
instance MonadUnique RM where
- getUniqueSupplyM = RM $ do
- (m, us, mod,lcls) <- get
- let (us1, us2) = splitUniqSupply us
- (put) (m,us2,mod,lcls)
- return us1
+ getUniqueSupplyM = RM $ \_ s ->
+ case splitUniqSupply (rm_us s) of
+ (us1, us2) -> (# s { rm_us = us2 }, us1 #)
getMap :: RM (UniqFM Id TagSig)
-getMap = RM $ ((\(fst,_,_,_) -> fst) <$> get)
+getMap = RM $ \_ s -> (# s, rm_sig_env s #)
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)
+setMap !m = RM $ \_ s -> (# s { rm_sig_env = m }, () #)
getFVs :: RM IdSet
-getFVs = RM $ ((\(_,_,_,lcls) -> lcls) <$> get)
+getFVs = RM $ \_ s -> (# s, rm_fvs s #)
setFVs :: IdSet -> RM ()
-setFVs !fvs = RM $ do
- (tag_map,us,mod,_lcls) <- get
- put (tag_map, us,mod,fvs)
+setFVs !fvs = RM $ \_ s -> (# s { rm_fvs = fvs }, () #)
+
+getMod :: RM Module
+getMod = RM $ \env s -> (# s, rm_mod env #)
+
+-- | When generating bytecode certain bindings might be untagged. So we have to
+-- have a way to check for that.
+getForBytecode :: RM Bool
+getForBytecode = RM $ \env s -> (# s, rm_interpreter env #)
-- 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 +268,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 +304,10 @@ mkLocalArgId id = do
---------------------------
-rewriteTopBinds :: Module -> UniqSupply -> [GenStgTopBinding 'InferTaggedBinders] -> [TgStgTopBinding]
-rewriteTopBinds mod us binds =
- let doBinds = mapM rewriteTop binds
-
- in evalState (unRM doBinds) (mempty, us, mod, mempty)
+rewriteTopBinds :: Bool -- ^ Generating bytecode?
+ -> Module -> UniqSupply -> [GenStgTopBinding 'InferTaggedBinders] -> [TgStgTopBinding]
+rewriteTopBinds for_bytecode mod us binds =
+ runRM mod for_bytecode us (mapM rewriteTop binds)
rewriteTop :: InferStgTopBinding -> RM TgStgTopBinding
rewriteTop (StgTopStringLit v s) = return $! (StgTopStringLit v s)
=====================================
compiler/GHC/Stg/EnforceEpt/TagSig.hs
=====================================
@@ -117,7 +117,7 @@ isTaggedSig (TagVal ti) = isTaggedInfo ti
-- | Is the given value-level tag known to be properly tagged?
-- NB: unboxed tuples are *not* treated as tagged here; they are handled
--- specially by the rewriter (which considers them already evaluated).
+-- specially by the rewriter. See Note [Constructor TagSigs]
isTaggedInfo :: TagInfo -> Bool
isTaggedInfo TagEPT = True
isTaggedInfo TagBottoming = True
=====================================
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,40 @@ 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 -- See Note [EPT enforcement for interpreted code] in GHC.Stg.EnforceEpt
+ else
+ case lf_info of
-- Function, tagged (with arity)
LFReEntrant {}
-> TagEPT
@@ -138,13 +148,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/42b5c293d94f68f6d9c54594b517def…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/42b5c293d94f68f6d9c54594b517def…
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
07 Oct '26
Simon Peyton Jones pushed to branch wip/T27828 at Glasgow Haskell Compiler / GHC
Commits:
2af96935 by Simon Peyton Jones at 2026-10-07T17:46:31+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 are 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 or 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.Core.TyCo.Subst( elemSubst, extendTvSubstWithClone )
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,27 @@ 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]
+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 = go_fresh subst tv tvs
+
+ -- Using an auxiliary function here to avoid prematurely forcing
+ -- the (banged) recursive call to `go` in the non-fresh case
+ go_fresh subst tv tvs = (subst'', tv':tvs')
+ where
+ !(subst'', tvs') = go subst' tvs
+ tv' = tv `setTyVarKind` substTy subst (tyVarKind tv)
+ subst' = extendTvSubstWithClone subst tv tv'
+ -- extendTvSubstWithClone: see (OF1b) in
+ -- Note [Exploiting open type families]
+
-----------------------------------------
-- Built-in type families
@@ -924,15 +951,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 +977,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))
-
- 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`.
-
-(TIF2) All this applies equally to /closed/ type families; it is /not/
- subsumed by Note [Exploiting closed type families]. Consider:
+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
+
+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:
+
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 +1015,10 @@ iff
(R2) There is no earlier equation that matches S(lhs). See (RW4) below.
+The relevance check is implemented by `getRelevantBranches`, which actually
+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 +1041,130 @@ 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.
-
-Note [Exploiting closed type families]
+ 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 T27828a:
+ 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 = r | r -> a
+ type instance F [a] = a->a
+
+ [W] F alpha ~ Int->Int
+
+Then, since F has been checked as injective, and the RHS `a->a` (pre-)unifies
+with the `Int->Int` in the Wanted with substitution [a :-> Int], we can
+add a derived FunDepEqns
+ FDEqns{ fd_qtvs = [], fd_eqs = [ [Int] ~ alpha ] }
+and thereby emit (via `instantiateFunDepEqns`)
+ [W] [Int] ~ alpha
+
+Things are a bit trickier when not all the quantified variables of the
+instance are bound by the pre-unification step. Suppose we have
+
+ type family F a = r | r -> a
+ type instance F (Maybe a) = [G a] -- G is a type family
+
+ [W] F alpha ~ [ty]
+
+Then, the RHS [G a] pre-unifies with the RHS of the Wanted, but with an
+empty substitution, which does not fix `a`. So we get this FunDepEqns:
+ FDEqns{ fd_qtvs = a, fd_eqs = [ Maybe a ~ alpha ] }
+(note the fd_qtvs=a) and thereby emit (via `instantiateFunDepEqns`)
+ [W] Maybe gamma ~ alpha -- Fresh gamma
+We have learned that `alpha` must be a list, but that is all; we don't
+know what is inside it, hence the fresh `gamma`.
+
+In general we have:
+
+ type family F x1 ... xn = r | r -> x1 x3 (say)
+ type instance forall qs. F t1 ... tn = rhs
+ [W] F a1 ... an ~ b
+
+Suppose `b` pre-unifies with `rhs`, with substitution `S` that binds
+some (but perhaps not all) of the `qs`. Lets say
+ unbound_qs = qs \ dom(S)
+
+Then we generate the FunDepEqs
+ FDEqns{ fd_qtvs = unbound_qs
+ , fd_eqs = [ S(t1) ~ S(a1), S(t3) ~ S(a3) ]
+
+These 'fd_qtvs' are subsequently instantiated to fresh metavariables by
+'instantiateFunDepEqns'.
+
+(OF1) The computation of `unbound_qs` is done by `trim_qtvs`, but we
+ have to be careful. Suppose (OF1a)
+ qs = [ k::*, a::k ]
+ S = [ k :-> UnliftedType ]
+ Then we want
+ unbound_qs = [ a::UnliftedType ] -- Must apply S to q's kind!!
+
+ And (OF1b), although I'm not sure if this can acutally happen:
+ qs = [ k::*, a::(k::*), b::(a::k) ]
+ S = [ k :-> UnliftedType ]
+ We want
+ unbound_qs = [ a::UnliftedType, b::(a::UnliftedType) ]
+ Note that the occurrence of `a` in b's kind should be replaced by the
+ newly-kinded `a` not the original `a::k`.
+
+ 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 `a` that is /not/ matched
+ * Adds the substitution [a::k :-> a::S(k)] to the substitution
+
+Note [Exploiting closed type families] see `mkTopClosedFamEqFDs`
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
type family F a b where
@@ -1042,17 +1175,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 +1194,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 +1303,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 +1335,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 +1343,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 +1388,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 open 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 family 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 +1504,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 T27828b 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/2af969356bdfd6bf677d19eddcab9a1…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2af969356bdfd6bf677d19eddcab9a1…
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] 27 commits: Add regression test for #7803
by Florian Ragwitz (＠rafl) 07 Oct '26
by Florian Ragwitz (＠rafl) 07 Oct '26
07 Oct '26
Florian Ragwitz pushed to branch wip/rafl/hpc-instances at Glasgow Haskell Compiler / GHC
Commits:
234bab08 by Vladislav Zavialov at 2026-09-29T17:22:54-04:00
Add regression test for #7803
Commit 2effe18ab5, first shipped with GHC 8.2.1, fixed #7803 "Superclass
methods are left unspecialized".
This change turns the example from the ticket description into a regression
test, checking that foo1 is fully specialised at Double, with no calls to the
overloaded exp5Tail.
Closes #7803
Assisted-by: Claude Opus 5
- - - - -
c406135c by Andreas Klebinger at 2026-10-01T06:57:28-04:00
RTS: Update flag parsing/handling:
Using 0 as argument to any of these flags now resets the flags setting to default:
- ``-n0`` disables nursery chunking.
- ``-K0`` (or a bare ``-K``) removes the stack size limit.
- ``-M0`` removes the heap size limit.
- ``-H0`` resets the suggested heap size, including the nursery scaling set by ``-H``.
- ``-AL0`` makes the large object allocation limit follow ``-A`` again.
GC Generations are now limited to 64.
-n larger than -A now emits a warning and disables chunking.
Fixes #27830 #27829
- - - - -
984ee82b by Andreas Klebinger at 2026-10-01T06:58:10-04:00
Fix MultiLayerModules timeout multiplier.
We accidentally used the compile multiplier for ghci commands which
use the run timeout setting to set the timeout.
Fixes #26263 and #27796.
- - - - -
50a9cf26 by Andreas Klebinger at 2026-10-01T06:58:10-04:00
testsuite: Include runtime in JUnit report.
- - - - -
e358619f by Alan Zimmerman at 2026-10-01T06:59:01-04:00
EPA: Use EpaLocation in EpVirtualBraces
Haddock processing uses EpLayout.EpVirtualBraces to record the current
layout column, for allocating haddock comments correctly.
For exact printing, we need the line as well as the col, so we know
how many lines to skip when the indented code block starts.
This commit updates EpLayout.EpVirtualBraces so that it carries an
EpaLocation instead of just the Int column, to allow it to be used for
both purposes.
It is a simple mechanical change, with no other impact, but it allows
us to use EpLayout instead of AnnListLayout in AnnList, in the next
commit in this series.
- - - - -
1d2a26ee by Andrew Lelechenko at 2026-10-01T20:22:04-04:00
Remove bitSize from MINIMAL pragma of class Bits
Cf. https://github.com/haskell/core-libraries-committee/issues/441
The function is deprecated for 12 years and has a default implementation,
yet it was never removed from the MINIMAL pragma, putting library authors
in a very awkward position. Let's finally remove bitSize from MINIMAL.
- - - - -
3cc21e4c by Hannes Siebenhandl at 2026-10-01T20:22:59-04:00
Add regression test for #27641
- - - - -
c35096f5 by Hannes Siebenhandl at 2026-10-01T20:23:00-04:00
Don't `:add` modules the loader will reject
Only home modules can be actually added to the loader context, thus we
only accept the module if it belongs to a home unit.
- - - - -
a563cb27 by Simon Jakobi at 2026-10-02T17:37:36-04:00
ci: accept modified changelog.d entries in lint-changelog
The changelog guide says to extend an existing entry rather than add a
new one when the feature is already documented. lint_changelog only
counted added files, so such MRs failed before the validator ran.
Fixes #27779.
Assisted-by: Claude Fable 5.1
- - - - -
03082cd4 by Simon Jakobi at 2026-10-02T17:38:17-04:00
changelog.d: Fix warning flag name in the semaphore-v2 entry
The entry refers to -Wsemaphore-version-mismatch, which does not exist.
The warning GHC emits when it cannot use a -jsem semaphore, including
on a protocol version mismatch, is -Wsemaphore-open-failure.
Context: !15729, #25087
Assisted-by: Claude Fable 5.1
- - - - -
a93705ee by Simon Jakobi at 2026-10-02T17:38:17-04:00
changelog.d: Fix the CLC proposal link in the T27455 entry
The entry used the Sphinx :ref: role with a URL as its target. :ref:
resolves only internal labels, so the generated release notes would
show the proposal name without a link. Use the plain hyperlink form
like the other entries.
Context: !16274, #27455
Assisted-by: Claude Fable 5.1
- - - - -
54381079 by Hannes Siebenhandl at 2026-10-02T17:39:01-04:00
Extend the `TrustOverlay` for wired-in units
The TrustOverlay only contained the `UnitId` of all on-disk units.
However, wired-in units are referred to by their wired-in unit id, which
is not the same as the on-disk unit id.
Thus, trust checks for wired-in units failed because the lookup was
using the wired-in unit, which wasn't present in the `TrustOverlay`.
We fix #27834, by copying the trust info for wired-in unit ids.
- - - - -
f8cfb1a5 by Hécate Kleidukos at 2026-10-04T19:36:39+02:00
[CLC 341] Strict variants of mutable types
This commit is the implementation of CLC Proposal 341
https://github.com/haskell/core-libraries-committee/issues/341
- - - - -
575c4bc6 by Rodrigo Mesquita at 2026-10-05T12:32:02-04:00
ttg: HsModuleName in the AST, ModuleName in GHC
This commit makes the AST fully independent from GHC by parsing a
"module name" as an `HsModuleName (= HText)` rather than constructing an
`ModuleName (= FastString)` straight away.
In the GHC side, everything remains as a `ModuleName`. We turn AST
`HsModuleName`s into fast strings with the cheap `mkFastStringShortText`
when we process the AST for manipulation within the compiler.
There are no performance regressions introduced by this approach.
This is the final piece of #21592
Alternative plans were discussed in
gitlab.haskell.org/ghc/ghc/-/merge_requests/16546#note_694647,
but the Simon suggested one won in simplicity and performance when
compared against my attempt at implementing my original plan of having
a family `ModuleNameP`.
- - - - -
b3b89d32 by mangoiv at 2026-10-05T22:03:32-04:00
hadrian: Persist the used flavour name in the build root (#20650)
This executes the idea proposed in #20650, teaching Hadrian to persist
the flavour used to build a build root. This both makes use of multiple
build roots more ergonomic (as the user no longer needs to repeat
themselves) and avoids a tiresome foot-gun (forgetting to specify a
flavour, often wholly invalidating a build root).
Closes #20650.
Co-authored-by: Sylvain Henry <sylvain(a)haskus.fr>
- - - - -
f977837b by mangoiv at 2026-10-05T22:04:21-04:00
configure: fix sed script and subst tooldir script
Fixes #27672
Adds sanity checking for SUBST_TOOLDIR
Metric Decrease:
LinkableUsage01
MultiLayerModulesTH_OneShot
T10547
T12234
T12425
T13035
T13820
T18140
T18730
T18923
T9198
TcPlugin_RewritePerf
mhu-perf
- - - - -
f1cb08be by Hannes Siebenhandl at 2026-10-05T22:05:03-04:00
Prepend in-memory unit database for backpack
The packageDbFlags are stored in reverse order. Thus, prepending will
ensure that the in-memory unit database is the last item on the unit
database stack.
Further, the in-memory unit database needs to be able to shadow units
from earlier unit databases in the unit database stack.
Moreover, a `-clear-package-db` would remove the in-memory database if
it weren't the last item on the stack.
Closes #27835
- - - - -
8d49ed42 by Kazu Yamamoto at 2026-10-06T19:37:25-04:00
Do not leave standard file descriptors free at startup (#24450)
A process may be started with stdout closed -- `prog >&-` from a shell does
exactly that. Nothing then reserves descriptor 1, and open(), pipe() and
socket() hand out the lowest free descriptor, so the next descriptor the
runtime creates for itself takes it: the ticker's pipe, or a capability's IO
manager control pipe.
'GHC.Internal.IO.StdHandles.stdout' is a CAF, built the first time the program
writes to stdout, which is long after that has happened. It builds a 'Handle'
over descriptor 1, which now belongs to the runtime, and nothing reports an
error because the descriptor is perfectly good. The program then writes its
output into the runtime's own plumbing.
What that looks like from the outside is a hang. The descriptor the Handle has
taken over is the read end of a pipe, so poll() for POLLOUT on it never says
yes and epoll_ctl() accepts a registration for it; the thread waiting to write
blocks for ever. Closing the Handle at exit closes the runtime's descriptor,
which is worse: the ticker then fails on every tick.
'hs_init_ghc' now opens /dev/null onto whichever of descriptors 0, 1 and 2 are
closed, before the runtime creates any descriptor of its own. Each is opened
for the access that descriptor would normally have, read-only for 0 and
write-only for 1 and 2, so that writing to 'stdin' or reading from 'stdout'
still fails rather than quietly succeeding against /dev/null. See
Note [Standard file descriptors must be open].
Moving only the descriptors the runtime opens would not do: the first file the
program itself opened would land on the free number instead. The fix has to
leave no free number. A program run this way therefore finds stdout connected
to /dev/null rather than failing with EBADF on the first write, which is what
such a program would get from most other language runtimes.
Co-Authored-By: Claude Opus 5 (1M context) <noreply(a)anthropic.com>
- - - - -
65bcf9e9 by Simon Jakobi at 2026-10-06T19:38:09-04:00
changelog: Repair the sentence describing #27477
The description read "programs using could crash", the object of
"using" having been lost. The synopsis already says which programs are
affected, so drop the dangling word.
Assisted-by: Claude Fable 5.1
- - - - -
cd39cfb0 by Florian Ragwitz at 2026-10-07T06:51:51-07:00
hpc: Test desired HPC behaviour for class instances
- - - - -
4f89a68d by Florian Ragwitz at 2026-10-07T06:51:51-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.
- - - - -
392d18f2 by Florian Ragwitz at 2026-10-07T06:51:52-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.
- - - - -
7698c840 by Florian Ragwitz at 2026-10-07T06:51:52-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.
- - - - -
c08665f2 by Florian Ragwitz at 2026-10-07T06:51:52-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.
- - - - -
a233cc3a by Florian Ragwitz at 2026-10-07T06:51:52-07:00
Add a changelog entry for new HPC features
- - - - -
55f79d0f by Florian Ragwitz at 2026-10-07T09:31:16-07:00
Remove tcg_inst_meths in favour of a new IdDetails constructor
Thanks for this great suggestion, Sam! <3
- - - - -
dd907dc6 by Florian Ragwitz at 2026-10-07T09:31:16-07:00
Revert back to just using getOccString for DFunIds
- - - - -
160 changed files:
- .gitlab/ci.sh
- + changelog.d/24450
- + changelog.d/27641
- changelog.d/T27455
- + changelog.d/T27830-rts-flag-bounds
- + changelog.d/clc-341-strict-mutable-data-types
- changelog.d/fix-parallel-gc-selector-race-27477
- + changelog.d/hadrian-persist-flavour
- + changelog.d/hpc-classinsts
- changelog.d/semaphore-v2
- changelog.d/unit-index
- compiler/GHC.hs
- compiler/GHC/Builtin/Modules.hs
- compiler/GHC/ByteCode/Asm.hs
- compiler/GHC/ByteCode/Show.hs
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/Opt/CallerCC/Types.hs
- compiler/GHC/Core/Opt/Specialise.hs
- compiler/GHC/Driver/Backpack.hs
- compiler/GHC/Driver/Main/Compile.hs
- compiler/GHC/Driver/Pipeline.hs-boot
- compiler/GHC/Driver/Pipeline/Execute.hs
- compiler/GHC/Driver/Pipeline/Phases.hs
- compiler/GHC/Hs/Doc.hs
- compiler/GHC/Hs/Dump.hs
- compiler/GHC/Hs/Expr.hs
- compiler/GHC/Hs/ImpExp.hs
- compiler/GHC/Hs/Lit.hs
- compiler/GHC/HsToCore.hs
- compiler/GHC/HsToCore/Docs.hs
- compiler/GHC/HsToCore/Quote.hs
- compiler/GHC/HsToCore/Ticks.hs
- compiler/GHC/Iface/Errors/Types.hs
- compiler/GHC/Iface/Ext/Ast.hs
- compiler/GHC/Iface/Ext/Debug.hs
- compiler/GHC/Iface/Ext/Types.hs
- compiler/GHC/Parser.y
- compiler/GHC/Parser/Annotation.hs
- compiler/GHC/Parser/Errors/Types.hs
- compiler/GHC/Parser/Header.hs
- compiler/GHC/Parser/Lexer.x
- compiler/GHC/Parser/PostProcess.hs
- compiler/GHC/Parser/PostProcess/Haddock.hs
- compiler/GHC/Parser/String.hs
- compiler/GHC/Rename/Env.hs
- compiler/GHC/Rename/Names.hs
- compiler/GHC/Rename/Unbound.hs
- compiler/GHC/StgToJS/Linker/Linker.hs
- compiler/GHC/Tc/Deriv/Generics.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/Export.hs
- compiler/GHC/Tc/Module.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Types.hs
- compiler/GHC/Tc/Types/ErrCtxt.hs
- compiler/GHC/ThToHs.hs
- compiler/GHC/Types/Id/Info.hs
- compiler/GHC/Types/Unique.hs
- compiler/GHC/Types/UnresolvedImport.hs
- compiler/GHC/Unit/External/Wired.hs
- compiler/GHC/Unit/Home.hs
- compiler/GHC/Unit/Module.hs
- compiler/GHC/Unit/Module/Env.hs
- + compiler/GHC/Unit/Module/Name.hs
- compiler/GHC/Unit/Parser.hs
- compiler/GHC/Unit/State.hs
- compiler/GHC/Unit/Types.hs
- compiler/GHC/Unit/Types.hs-boot
- compiler/GHC/Utils/Binary.hs
- compiler/GHC/Utils/Outputable.hs
- compiler/Language/Haskell/Syntax.hs
- compiler/Language/Haskell/Syntax/Expr.hs
- compiler/Language/Haskell/Syntax/ImpExp.hs
- compiler/Language/Haskell/Syntax/Lit.hs
- compiler/Language/Haskell/Syntax/Module/Name.hs
- compiler/Language/Haskell/Syntax/Text.hs
- compiler/ghc.cabal.in
- distrib/configure.ac.in
- docs/users_guide/runtime_control.rst
- ghc/GHCi/UI.hs
- ghc/GHCi/UI/Info.hs
- hadrian/doc/flavours.md
- hadrian/src/Rules.hs
- hadrian/src/Settings.hs
- libraries/base/base.cabal.in
- libraries/base/changelog.md
- libraries/base/src/Control/Concurrent/Chan.hs
- + libraries/base/src/Control/Concurrent/Chan/Strict.hs
- libraries/base/src/Control/Concurrent/MVar.hs
- + libraries/base/src/Control/Concurrent/MVar/Strict.hs
- libraries/base/src/Data/IORef.hs
- + libraries/base/src/Data/IORef/Strict.hs
- libraries/ghc-internal/src/GHC/Internal/Bits.hs
- linters/lint-codes/LintCodes/Static.hs
- m4/subst_tooldir.m4
- rts/RtsFlags.c
- rts/RtsStartup.c
- rts/include/rts/Flags.h
- rts/include/rts/storage/GC.h
- rts/sm/GC.c
- rts/sm/Storage.c
- testsuite/driver/junit.py
- testsuite/driver/testglobals.py
- testsuite/driver/testlib.py
- + testsuite/tests/backpack/should_compile/T27835.bkp
- + testsuite/tests/backpack/should_compile/T27835.stderr
- testsuite/tests/backpack/should_compile/all.T
- testsuite/tests/count-deps/CountDepsAst.stdout
- testsuite/tests/count-deps/CountDepsParser.stdout
- testsuite/tests/ghc-api/downsweep/IncrementalDownsweep.hs
- testsuite/tests/ghc-api/exactprint/T22919.stderr
- testsuite/tests/ghc-api/exactprint/Test20239.stderr
- testsuite/tests/ghc-api/exactprint/ZeroWidthSemi.stderr
- + testsuite/tests/ghci/scripts/T27641.script
- + testsuite/tests/ghci/scripts/T27641.stderr
- + testsuite/tests/ghci/scripts/T27641.stdout
- + testsuite/tests/ghci/scripts/T27834.hs
- + testsuite/tests/ghci/scripts/T27834.script
- + testsuite/tests/ghci/scripts/T27834.stdout
- testsuite/tests/ghci/scripts/all.T
- testsuite/tests/haddock/should_compile_flag_haddock/T17544.stderr
- testsuite/tests/haddock/should_compile_flag_haddock/T17544_kw.stderr
- testsuite/tests/haddock/should_compile_flag_haddock/T24221.stderr
- testsuite/tests/hiefile/should_run/T24544.hs
- + testsuite/tests/hpc/instmeths/instmeths.hs
- + testsuite/tests/hpc/instmeths/instmeths.stdout
- + testsuite/tests/hpc/instmeths/test.T
- testsuite/tests/interface-stability/base-exports.stdout
- testsuite/tests/interface-stability/base-exports.stdout-javascript-unknown-ghcjs
- testsuite/tests/interface-stability/base-exports.stdout-mingw32
- testsuite/tests/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/T14189.stderr
- testsuite/tests/parser/should_compile/T15323.stderr
- testsuite/tests/parser/should_compile/T20452.stderr
- testsuite/tests/parser/should_compile/T20718.stderr
- testsuite/tests/parser/should_compile/T20718b.stderr
- testsuite/tests/parser/should_compile/T20846.stderr
- testsuite/tests/parser/should_compile/T23315/T23315.stderr
- testsuite/tests/perf/compiler/all.T
- testsuite/tests/printer/AnnotationNoListTuplePuns.stdout
- testsuite/tests/printer/T18791.stderr
- testsuite/tests/printer/Test20297.stdout
- testsuite/tests/printer/Test24533.stdout
- testsuite/tests/profiling/should_run/caller-cc/CallerCcParser.hs
- + testsuite/tests/rts/T24450.hs
- + testsuite/tests/rts/T24450.stderr
- testsuite/tests/rts/all.T
- testsuite/tests/rts/rtsflags001.stderr-ws-32
- testsuite/tests/rts/rtsflags001.stderr-ws-64
- + testsuite/tests/simplCore/should_compile/T7803.hs
- + testsuite/tests/simplCore/should_compile/T7803.stderr
- + testsuite/tests/simplCore/should_compile/T7803a.hs
- testsuite/tests/simplCore/should_compile/all.T
- utils/check-exact/ExactPrint.hs
- utils/haddock/haddock-api/src/Haddock/Backends/Hyperlinker/Renderer.hs
The diff was not included because it is too large.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/638439a1ed142304e625341d9d6936…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/638439a1ed142304e625341d9d6936…
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