[Git][ghc/ghc][wip/T26543b] 13 commits: Remove the Eq and Ord instances for ForAllTyFlag
by Simon Peyton Jones (＠simonpj) 13 Oct '26
by Simon Peyton Jones (＠simonpj) 13 Oct '26
13 Oct '26
Simon Peyton Jones pushed to branch wip/T26543b at Glasgow Haskell Compiler / GHC
Commits:
d07a5176 by Simon Peyton Jones at 2026-10-13T18:10:39-04:00
Remove the Eq and Ord instances for ForAllTyFlag
In Note [Comparing visibility] in GHC.Core.TyCo.Compare we read that
"we always compare ForAllTyFlags with `eqForAllVis` or `cmpForAllVis`"
But alas there was an Eq and Ord instance for ForAllTyFlag, which made it
impossible to check this claim. So I made these changes:
* Move the definition of ForAllTyFlag and its related functions from
L.H.S.Specificity (where it did not belong, since L.H.S didn't use it)
into GHC.Types.Var.
* Remove the Eq and Ord instances for ForAllTyFlag
* Deal with the fallout, by using `eqForAllVis` or related functions.
* In interface files we use IfaceType as a key for a de-deduplication map
See Note [Deduplication during iface binary serialisation]
in GHC.Iface.Binary. For this we need /exact/ comparison, so we use a
newtype wrapper for IfaceForAllTyFlag, and give use `cmpForAllTyFlagExactly`
to implement its Ord instance. Tiresome but easy.
* Rename `toIfaceForAllBndrs` to `toIfaceForAllTyBndrs`
- - - - -
ea5c054d by Simon Peyton Jones at 2026-10-13T18:10:39-04:00
Refactor type and coercion substitution
This MR refactors type and coercion substitution so that they use
TyCoMapper, rather than hand-rolled code. Fundamentally it's a simple
idea, but I had to do quite a bit of refactoring to make it fly.
I got Claude to help me this this refactoring, but I paid careful
attention to every line of code.
Main changes:
* New module GHC.Core.TyCo.Make which defines TyCoMapper, and a bunch of other
simple "smart constructors" for types and coercions. See
GHC.Core.TyCo.Rep Note [The Type-related module hierarchy], esp (TRM1)
* The new TyCoMapper has new fields `tcm_tcapp_ty` and `tcm_tcapp_co` to handle
type-constructor applications. These replace `tcm_tycon`.
* Rewrite GHC.Core.TyCo.Subst to use TyCoMapper
* Rewrite GHC.Core.Type.expandTypeSynonyms to use TyCoMapper.
* Implement `seqType` and `seqCo` with TyCoFolder. To to this I had to add
a `tcf_lit` field to TyCoFolder.
* A new module GHC.Utils.StrictIdentity to define a strict identity monad,
which itself is used for
substTyCoMapper :: TyCoMapper Subst StrictIdentity
* I removed an apparently-unused instance for Binary Levity
Refactoring `seq` functions
* In GHC.Core.Seq, redefine `seqOneShot`, `seqRuleInfo`, and friends to return
`SeqResult`, a new type defined in GHC.Types.Baseic, rather than `()`. We
can define a Monoid instance for `SeqResult` that does the right thing.
* This has knock-on effects across the compiler.
- - - - -
34165e23 by Simon Peyton Jones at 2026-10-13T18:10:39-04:00
Refactor TyCoMapper to take a single monad; add StrictReaderT
TyCoMapper used to be parameterised over both an environment and a
monad, with fields like
tcm_tyvar :: env -> TyVar -> m Type
Now it is parameterised over just the monad:
tcm_tyvar :: TyVar -> m Type
If the mapping needs an environment, `m` is a reader monad over that
environment. Many uses (e.g. zonkTcTypeMapper, swizzleMapper) need no
environment at all, and used to pass a dummy (). The binder field
becomes
tcm_tycobinder :: forall r. TyCoVar -> ForAllTyFlag
-> (TyCoVar -> m r) -> m r
and runs the continuation in the extended environment. mapTyCoX is gone;
only mapTyCo remains.
To make this efficient, the reader monad must use the one-shot trick and
be strict in the environment. So:
* New module GHC.Utils.Monad.StrictReader defines
newtype StrictReaderT r m a
with hand-written instances. The builder of the pattern synonym
`StrictReaderT` is a smart constructor that adds both `oneShot` and a
bang on the environment, so every StrictReaderT computation is strict
in the environment. See Note [Instances for StrictReaderT].
* ZonkT becomes type ZonkT = StrictReaderT ZonkEnv
ZonkM becomes type ZonkM = StrictReaderT ZonkGblEnv IO
replacing their own hand-written instances.
* Substitution uses
type SubstM = StrictReaderT Subst StrictIdentity
substTyCoMapper :: TyCoMapper SubstM
and similarly expandTypeSynonymMapper.
* zonk_tycomapper :: TyCoMapper (ZonkT TcM) is now much simpler.
* swizzleMapper uses StrictIdentity rather than Identity.
* Module renaming, so that the strict monads are all peers in GHC.Utils.Monad:
GHC.Utils.StrictIdentity ==> GHC.Utils.Monad.StrictIdentity
GHC.Utils.Monad.State.Strict ==> GHC.Utils.Monad.StrictState
alongside the new GHC.Utils.Monad.StrictReader.
Co-Authored-By: Claude Opus 5.5 <noreply(a)anthropic.com>
- - - - -
c0299e15 by Simon Jakobi at 2026-10-13T18:11:23-04:00
testsuite: Line-buffer the driver's stdout
Python block-buffers stdout when it is a pipe. This is the case for
example in CI. As a result there is often no indication of progress at
all until the run ends.
To fix this, we configure it explicitly to use line buffering instead.
stderr is reconfigured too, for consistency: Python line-buffers it by
default since 3.9.
The type-ignores are for mypy, which types these handles as TextIO — an
interface without reconfigure.
Fixes #12934.
Assisted-by: Claude Fable 5
- - - - -
9b5beaa2 by Florian Ragwitz at 2026-10-13T18:12:05-04:00
hpc: Improve coverage semantics for instance methods and instances
Users care about which of their explicitly 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 therefore skip generating top-level boxes for inherited methods which will
appear as uncovered with no clear indication as to why, and no way to fix other
than exercising code the user has not written.
Previously, top-level boxes for those inherited methods would use the instance
head as their source span. Now that those boxes are gone, we can use that
source span for another purpose:
We introduce a new top-level box for each class instance with its instance head
as the source span, and use that to indicate whether or not an instance has
been covered at all.
We do this by making any method of the instance, inherited/generated or
otherwise, tick the box for the instance head. Excluded from this are
methodless classes, which could never be covered using the current mechanism.
This could be improved upon further.
These changes apply to ticking for program coverage only, and don't affect
source notes. Additionally, we update the scope of record selector ticking to
be limited to program coverage as well, as the oversight to also extend it to
source notes has previously caused bugs and because record selector ticking is
coverage-specific.
Fixes #17155, #15932.
- - - - -
836ec50a by Simon Peyton Jones at 2026-10-13T18:12:54-04: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.
- - - - -
889ef371 by Simon Peyton Jones at 2026-10-13T18:13:36-04: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.
- - - - -
f9193e53 by Simon Peyton Jones at 2026-10-13T18:13:37-04:00
One line fix to fallout from
...#27731, !16564, simplifying Tc.Errors machinery
There was an over-eager assert!
- - - - -
cdd56b7a by Florian Ragwitz at 2026-10-13T18:14:19-04:00
Fix several sphinx errors and warnings from rendering the release notes
The extension references which are removed here are for extension which were
already previously undocumented, so just removing them seems fine for now.
- - - - -
4f00da25 by Florian Ragwitz at 2026-10-13T18:14:19-04:00
Link to QualifiedStrings documentation
- - - - -
97adaf89 by Simon Peyton Jones at 2026-10-14T00:07:27+01:00
Line up simpleUnifyCheck and check_ty_eq_rhs
Even after #26543 was allegedly fixed, the original repo case in the
Description continued to fail. The reason was that the QuickLook
unifier, `qlUnify`, used `simpleUnifyCheck` for checking unification
invariants; and `simpleUnifyCheck` conservatively rejected any RHS
with a coercion hole in it. The upshot was that QuickLook was not
as clever as it should be, wrongly failing to do an impredicative
instantiation.
Interestingly `check_ty_eq_rhs`, which does the same job during
constraint solving, was more liberal: it just looked at the free vars
of the coercion, and allowed coercion holes.
This MR lines them up, adding some careful notes. See
Note [simpleUnifyCheck]
Note [Occurs check and coercions]
Note [Unification preconditions] esp (COERCIONS)
Things are better than before, but I am still uncomfortable about the
possibilty that a hole might be filled with a coercion that mentions
the LHS type variable; for now I have left this discomfort documented
in Note [Occurs check and coercions].
Main changes
* `qlUnify` now only unifies /instantiation variables/ not regular unification
variables. This makes QuickLook more predictable. See (UQL6) in
Note [QuickLook unification].
* `qlUnify` no longer needs to call `simpleUnifyCheck`, so we can get rid of
`UC_QuickLook` and its code in `simpleUnifyCheck`.
* I found I could get rid of `mkOccFolders` in favour of `anyFreeVarsOfType`.
Hooray.
* Improve documentation of CycleBreakerTv, and rename it to GivenCycleBreakerTv
because they are only uesd for Givens!
* I accepted a 9% worsening in compile time allocation on T5030
because the newly-consistent story triggered #27934.
Other changes
* I refactored `atvFolder` so that it pairs the "interesting-var" function
with the in-scope set, to avoid building a closure with a free variable.
Now we get nice tight loops for `anyFreeVarsOfType` and friends.
See Note [Any-free-var folder].
Metric Increase:
T5030
- - - - -
5f7b3047 by Simon Peyton Jones at 2026-10-14T00:07:27+01:00
Fix order-dependence in QuickLook
Ticket #27917 pointed out that QuickLook was order-dependent
-- very bad!
The solution is in `qlUnify`: spot when we are unifying a type with a
definite monotype, and then monomorphise any free instantiation
variables of that type.
See (UQL8) and (UQL9) in Note [QuickLook unification].
- - - - -
c391c70c by Simon Peyton Jones at 2026-10-14T00:07:28+01:00
Add some comments about RuntimeUnk
This commit just adds comments explaining why we don't need to worry about
RuntimeUnkTv in the constraint solver.
It also tightens up docmentation of earlier (overlapping) commits in
this MR.
- - - - -
142 changed files:
- changelog.d/26616
- + changelog.d/T26543
- changelog.d/T27329
- + changelog.d/T27828
- + changelog.d/T27844
- changelog.d/boxing-family
- + changelog.d/hpc-classinsts
- changelog.d/tcplugin_init.md
- changelog.d/unit-index
- compiler/GHC/Builtin/WiredIn/Prim.hs
- compiler/GHC/Builtin/WiredIn/Types/Box.hs
- compiler/GHC/Cmm/GenericOpt.hs
- compiler/GHC/Cmm/UniqueRenamer.hs
- compiler/GHC/CmmToAsm/Dwarf/Types.hs
- compiler/GHC/CmmToAsm/Monad.hs
- compiler/GHC/CmmToAsm/Reg/Graph/Spill.hs
- compiler/GHC/CmmToAsm/Reg/Graph/SpillClean.hs
- compiler/GHC/CmmToAsm/Reg/Graph/SpillCost.hs
- compiler/GHC/CmmToAsm/Reg/Graph/Stats.hs
- compiler/GHC/CmmToAsm/Reg/Linear/State.hs
- compiler/GHC/CmmToAsm/Reg/Linear/Stats.hs
- compiler/GHC/CmmToAsm/Reg/Liveness.hs
- compiler/GHC/CmmToAsm/Wasm/Asm.hs
- compiler/GHC/CmmToAsm/Wasm/Types.hs
- compiler/GHC/CmmToC.hs
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion.hs-boot
- compiler/GHC/Core/Coercion/Axiom.hs
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/FVs.hs
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Map/Type.hs
- compiler/GHC/Core/Opt/Arity.hs
- compiler/GHC/Core/Opt/CallerCC.hs
- compiler/GHC/Core/Opt/Exitify.hs
- compiler/GHC/Core/Opt/Specialise.hs
- compiler/GHC/Core/Reduction.hs
- compiler/GHC/Core/Seq.hs
- compiler/GHC/Core/TyCo/Compare.hs
- compiler/GHC/Core/TyCo/FVs.hs
- + compiler/GHC/Core/TyCo/Make.hs
- + compiler/GHC/Core/TyCo/Make.hs-boot
- compiler/GHC/Core/TyCo/Ppr.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCo/Rep.hs-boot
- compiler/GHC/Core/TyCo/Subst.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Type.hs-boot
- compiler/GHC/Core/Unify.hs
- compiler/GHC/CoreToIface.hs
- compiler/GHC/CoreToIface.hs-boot
- compiler/GHC/Driver/Downsweep.hs
- compiler/GHC/Driver/Main/Compile.hs
- compiler/GHC/HsToCore.hs
- compiler/GHC/HsToCore/Ticks.hs
- compiler/GHC/Iface/Decl.hs
- compiler/GHC/Iface/Ext/Types.hs
- compiler/GHC/Iface/Ext/Utils.hs
- compiler/GHC/Iface/Syntax.hs
- compiler/GHC/Iface/Type.hs
- compiler/GHC/Iface/Type.hs-boot
- compiler/GHC/IfaceToCore.hs
- compiler/GHC/Runtime/Heap/Inspect.hs
- compiler/GHC/Stg/BcPrep.hs
- compiler/GHC/Stg/Debug.hs
- compiler/GHC/Stg/EnforceEpt/Rewrite.hs
- compiler/GHC/Stg/EnforceEpt/TagSig.hs
- compiler/GHC/Stg/Subst.hs
- compiler/GHC/Tc/Deriv/Functor.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Instance/FunDeps.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/FunDeps.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Tc/Zonk/Env.hs
- compiler/GHC/Tc/Zonk/Monad.hs
- compiler/GHC/Tc/Zonk/TcType.hs
- compiler/GHC/Tc/Zonk/Type.hs
- compiler/GHC/Types/Arity.hs
- compiler/GHC/Types/Basic.hs
- compiler/GHC/Types/Cpr.hs
- compiler/GHC/Types/Demand.hs
- compiler/GHC/Types/Id/Info.hs
- compiler/GHC/Types/Name/Env.hs
- compiler/GHC/Types/Name/Occurrence.hs
- compiler/GHC/Types/Unique/DSM.hs
- compiler/GHC/Types/Unique/FM.hs
- compiler/GHC/Types/Unique/Map.hs
- compiler/GHC/Types/Unique/Set.hs
- compiler/GHC/Types/Unique/Supply.hs
- compiler/GHC/Types/Var.hs
- compiler/GHC/Types/Var.hs-boot
- compiler/GHC/Types/Var/FV.hs
- compiler/GHC/Types/Var/Set.hs
- compiler/GHC/Utils/Binary.hs
- + compiler/GHC/Utils/Monad/StrictIdentity.hs
- + compiler/GHC/Utils/Monad/StrictReader.hs
- compiler/GHC/Utils/Monad/State/Strict.hs → compiler/GHC/Utils/Monad/StrictState.hs
- compiler/GHC/Utils/Outputable.hs
- compiler/Language/Haskell/Syntax/Specificity.hs
- compiler/ghc.cabal.in
- docs/users_guide/exts/literals.rst
- testsuite/driver/runtests.py
- testsuite/tests/count-deps/CountDepsParser.stdout
- testsuite/tests/default/default-fail05.stderr
- testsuite/tests/ghci.debugger/scripts/T14628.stderr
- + testsuite/tests/hpc/instmeths/instmeths.hs
- + testsuite/tests/hpc/instmeths/instmeths.stdout
- + testsuite/tests/hpc/instmeths/test.T
- + testsuite/tests/impredicative/T27917.hs
- testsuite/tests/impredicative/all.T
- + 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
- testsuite/tests/indexed-types/should_fail/T1897b.stderr
- testsuite/tests/indexed-types/should_fail/T9662.stderr
- testsuite/tests/simplCore/should_compile/T22375.stderr
- testsuite/tests/simplCore/should_compile/T22375DataFamily.stderr
- testsuite/tests/typecheck/should_compile/LocalGivenEqs.hs
- + testsuite/tests/typecheck/should_compile/T26543_orig.hs
- testsuite/tests/typecheck/should_compile/all.T
- testsuite/tests/typecheck/should_fail/T12785b.stderr
- testsuite/tests/typecheck/should_fail/T22707.stderr
- + testsuite/tests/typecheck/should_fail/T26543a.hs
- + testsuite/tests/typecheck/should_fail/T26543a.stderr
- + testsuite/tests/typecheck/should_fail/T27844.hs
- + testsuite/tests/typecheck/should_fail/T27844.stderr
- testsuite/tests/typecheck/should_fail/all.T
- utils/check-exact/Utils.hs
- utils/haddock/haddock-api/src/Haddock/Backends/Hyperlinker/Utils.hs
The diff was not included because it is too large.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/3ffab1d97c53032a52a0a6e48728ec…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/3ffab1d97c53032a52a0a6e48728ec…
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
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
836ec50a by Simon Peyton Jones at 2026-10-13T18:12:54-04: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
=====================================
@@ -3469,7 +3469,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/836ec50a2bda086d73657ea291fdd51…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/836ec50a2bda086d73657ea291fdd51…
You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help
1
0
[Git][ghc/ghc][master] 2 commits: Fix several sphinx errors and warnings from rendering the release notes
by Marge Bot (＠marge-bot) 13 Oct '26
by Marge Bot (＠marge-bot) 13 Oct '26
13 Oct '26
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
cdd56b7a by Florian Ragwitz at 2026-10-13T18:14:19-04:00
Fix several sphinx errors and warnings from rendering the release notes
The extension references which are removed here are for extension which were
already previously undocumented, so just removing them seems fine for now.
- - - - -
4f00da25 by Florian Ragwitz at 2026-10-13T18:14:19-04:00
Link to QualifiedStrings documentation
- - - - -
6 changed files:
- changelog.d/26616
- changelog.d/T27329
- changelog.d/boxing-family
- changelog.d/tcplugin_init.md
- changelog.d/unit-index
- docs/users_guide/exts/literals.rst
Changes:
=====================================
changelog.d/26616
=====================================
@@ -3,6 +3,7 @@ synopsis: Fix the interaction of ExplicitLevelImports with qualified imports
description:
GHC now properly considers module qualification when tracking the levels that an identifier
is imported at:
+
- A qualified occurrence must be bound in a corresponding qualified import of the right level.
- The level error message now correctly reports the user-written qualification.
mrs: !16195
=====================================
changelog.d/T27329
=====================================
@@ -7,9 +7,9 @@ description: {
The following language extensions have been marked as deprecated,
meaning they will now issue a warning with :ghc-flag:`-Wdeprecated-flags`:
- - :extension:`AlternativeLayoutRule`
- - :extension:`AlternativeLayoutRuleTransitional`
- - :extension:`ParallelArrays`
+ - ``AlternativeLayoutRule``
+ - ``AlternativeLayoutRuleTransitional``
+ - ``ParallelArrays``
- :extension:`PolymorphicComponents`
- :extension:`Rank2Types`
}
=====================================
changelog.d/boxing-family
=====================================
@@ -14,6 +14,6 @@ description:
comprehensions). The main two issues fixed are:
- GHC can now box types of any representation, including unboxed tuples,
- unboxed sums, ``AddrRep`` and all ``VecRep``s. This fixes #20864.
+ unboxed sums, ``AddrRep`` and all ``VecRep``\s. This fixes #20864.
- GHC can now box in the middle of typechecking, before the representation
of the value to box has even been determined. This fixes #25065.
=====================================
changelog.d/tcplugin_init.md
=====================================
@@ -12,13 +12,13 @@ description:
The fields ``tcPluginStop :: s -> TcPluginM ()`` and ``dePluginStop :: s -> TcPluginM ()``
are replaced by the two fields::
- tcPluginPostTc :: s -> TcPluginM ()
- tcPluginShutdown :: s -> IO ()
+ tcPluginPostTc :: s -> TcPluginM ()
+ tcPluginShutdown :: s -> IO ()
respectively::
- dePluginPostTc :: s -> TcPluginM ()
- dePluginShutdown :: s -> IO ()
+ dePluginPostTc :: s -> TcPluginM ()
+ dePluginShutdown :: s -> IO ()
The "post-tc" actions are run at the end of typechecking, and can be used to
inspect the final ``TcGblEnv``/``TcLclEnv`` of the module being typechecker.
=====================================
changelog.d/unit-index
=====================================
@@ -1,14 +1,14 @@
section: compiler
-synopsis: Use global ``UnitIndex`` to deduplicate ``UnitInfo``s over multiple home units
+synopsis: Use global ``UnitIndex`` to deduplicate ``UnitInfo``\s over multiple home units
issues: #27500 #26423 #27748 #27834 #27835
mrs: !16115 !16598 !16743 !16748
description: {
- The ``UnitState`` used to be duplicated for all ``HomeUnitEnv``, not sharing any of the ``UnitInfo``s.
+ The ``UnitState`` used to be duplicated for all ``HomeUnitEnv``, not sharing any of the ``UnitInfo``\s.
This can lead to excessive memory usage with multiple home units and large package databases.
- Our solution to this problem is deduplicating ``UnitInfo``s globally across the whole ``UnitEnv``.
- We store this information in the ``UnitIndex`` which contains data global to all ``UnitState``s.
- All processed ``UnitInfo``s and the ``WiredMap`` are stored in there, and in the future, we might
+ Our solution to this problem is deduplicating ``UnitInfo``\s xxx globally across the whole ``UnitEnv``.
+ We store this information in the ``UnitIndex`` which contains data global to all ``UnitState``\s.
+ All processed ``UnitInfo``\s and the ``WiredMap`` are stored in there, and in the future, we might
move more fields from ``UnitState`` to ``UnitIndex``.
}
=====================================
docs/users_guide/exts/literals.rst
=====================================
@@ -15,3 +15,4 @@ Literals
overloaded_strings
overloaded_labels
multiline_strings
+ qualified_strings
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f9193e53d726e02244029cf97c3648…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f9193e53d726e02244029cf97c3648…
You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help
1
0
[Git][ghc/ghc][master] 2 commits: Refactor and simplify solver's unification code
by Marge Bot (＠marge-bot) 13 Oct '26
by Marge Bot (＠marge-bot) 13 Oct '26
13 Oct '26
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
889ef371 by Simon Peyton Jones at 2026-10-13T18:13:36-04: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.
- - - - -
f9193e53 by Simon Peyton Jones at 2026-10-13T18:13:37-04:00
One line fix to fallout from
...#27731, !16564, simplifying Tc.Errors machinery
There was an over-eager assert!
- - - - -
13 changed files:
- + changelog.d/T27844
- compiler/GHC/Runtime/Heap/Inspect.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/indexed-types/should_fail/T9662.stderr
- testsuite/tests/typecheck/should_fail/T12785b.stderr
- + testsuite/tests/typecheck/should_fail/T27844.hs
- + testsuite/tests/typecheck/should_fail/T27844.stderr
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
changelog.d/T27844
=====================================
@@ -0,0 +1,9 @@
+section: compiler
+issues: #27844
+mrs: !16723
+synopsis:
+ Reinstate a missing occurs check in the constraint solver
+description:
+ Simplifies code in GHC's type-constraint solver, thereby fixing an outright
+ compiler loop (via a missing occurs check).
+
=====================================
compiler/GHC/Runtime/Heap/Inspect.hs
=====================================
@@ -630,7 +630,7 @@ be sigmas and not taus.
~~~~~~~~~~~~~~~~~~~~~~
In the GHCi debugger we use unification variables whose MetaInfo is
RuntimeUnkTv. The special property of a RuntimeUnkTv is that it can
-unify with a polytype (see GHC.Tc.Utils.Unify.checkTypeEq).
+unify with a polytype (see GHC.Tc.Solver.Equality.checkTypeEqNoUnification).
If we don't do this `:print <term>` will fail if the type of <term>
has nested `forall`s or `=>`s.
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -581,7 +581,6 @@ mkErrorItem ct
CtGiven {} -> Nothing
CtWanted (WantedCt { ctev_dest = dest }) -> Just dest
-
m_reason = case ct of
CIrredCan (IrredCt { ir_reason = reason }) -> Just reason
_ -> Nothing
@@ -2107,10 +2106,11 @@ mkTyVarEqErr' ctxt item tv1 ty2
-- See Note [Error messages for untouchables]
| (implic:_) <- cec_encl ctxt -- Get the innermost context
, Implic { ic_tclvl = lvl } <- implic
- = assertPpr (not (isTouchableMetaTyVar lvl tv1) || hasCoercionHole ty2)
+ = assertPpr (not (isTouchableMetaTyVar lvl tv1) || ei_suppress item)
(ppr tv1 $$ ppr lvl) $ do -- See Note [Error messages for untouchables]
-- We can still get touchable meta-tyvars on the LHS if there is an
-- unsolved coercion hole, e.g. (alpha::Type) ~ Int# |> co_hole
+ -- Hence (ei_suppress item)
tv_extra <- extraTyVarEqInfo (tv1, Just implic) ty2
let tv_extra' = tv_extra { thisTyVarIsUntouchable = Just implic }
msg = Mismatch
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -21,6 +21,7 @@ import GHC.Tc.Types.Evidence
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.CtLoc
import GHC.Tc.Types.Origin
+import GHC.Tc.Types( TcM )
import GHC.Tc.Utils.Unify
import GHC.Tc.Utils.TcType
import GHC.Tc.Instance.Family ( tcUnwrapNewtype_maybe )
@@ -36,8 +37,8 @@ import GHC.Core.Coercion
import GHC.Core.Reduction
import GHC.Core.FamInstEnv ( FamInstEnvs )
import GHC.Core
-import GHC.Types.Var
+import GHC.Types.Var
import GHC.Types.Basic
import GHC.Types.Name.Reader
import GHC.Types.Var.Env
@@ -49,6 +50,8 @@ import GHC.Utils.Misc
import GHC.Utils.Monad
import GHC.Data.Pair
+import GHC.Data.Bag
+
import Control.Monad
import Data.Maybe ( isJust, isNothing )
import Data.List ( zip4 )
@@ -406,11 +409,13 @@ canonicaliseEquality
-- hold.
canonicaliseEquality ev eq_rel ty1 ty2
- = Stage $ do { traceTcS "canonicaliseEquality" $
+ = Stage $ do { traceTcS "canonicaliseEquality {" $
vcat [ ppr ev, ppr eq_rel, ppr ty1, ppr ty2 ]
; rdr_env <- getGlobalRdrEnvTcS
; fam_insts <- getFamInstEnvs
- ; can_eq_nc initCanEqState rdr_env fam_insts ev eq_rel ty1 ty1 ty2 ty2 }
+ ; res <- can_eq_nc initCanEqState rdr_env fam_insts ev eq_rel ty1 ty1 ty2 ty2
+ ; traceTcS "canonicaliseEquality }" (ppr res)
+ ; return res }
-- | Main worker function for 'canonicaliseEquality'.
--
@@ -1822,7 +1827,7 @@ Ticket #10009, a very nasty example:
g :: forall a. (UnF (F a) ~ a) => a -> ()
g _ = f (undefined :: F a)
-For g we get [G] g1 : UnF (F a) ~ a
+For g we get [G] g1 : UnF (F a) ~ a
[W] w1 : UnF (F beta) ~ beta
[W] w2 : F a ~ F beta
@@ -1982,7 +1987,7 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
finish rewriters kind_co
= do { traceTcS "Hetero equality gives rise to kind equality"
(ppr swapped $$
- ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ])
+ ppr kind_co <+> dcolon <+> sep [ ppr ki2, text "~#", ppr ki1 ])
; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn rewriters
-- rewriteEqEvidence adds any as-yet-unsolved equalities
-- from the kind equality (namely `rewriters`) to the
@@ -2040,15 +2045,15 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
then finish_with_swapping
else finish_without_swapping }
- | TyVarLHS {} <- lhs1
+ | TyVarLHS tv <- lhs1
, TyFamLHS {} <- lhs2
- = if put_tyvar_on_lhs
+ = if mightPossiblyUnify ev eq_rel tv
then finish_without_swapping
else finish_with_swapping
| TyFamLHS {} <- lhs1
- , TyVarLHS {} <- lhs2
- = if put_tyvar_on_lhs
+ , TyVarLHS tv <- lhs2
+ = if mightPossiblyUnify ev eq_rel tv
then finish_with_swapping
else finish_without_swapping
@@ -2096,10 +2101,6 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
; new_ev <-rewriteEqEvidence ev swapped lhs1_redn lhs2_redn emptyCoHoleSet
; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) }
- put_tyvar_on_lhs = isWanted ev && eq_rel == NomEq
- -- See Note [Orienting TyVarLHS/TyFamLHS]
- -- Same conditions as for canEqCanLHSFinish_try_unification
- -- which we are setting ourselves up for here
{- Note [Orienting TyVarLHS/TyFamLHS]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2108,16 +2109,16 @@ Which to put on the left? Answer:
* If there is no chance of unifying, put the type family on the left,
(F tys ~ a), because it's generally better to rewrite away function
- calls. See `put_tyvar_on_lhs` in canEqCanLHS2; and
- Note [Orienting TyVarLHS/TyFamLHS]
+ calls. For the "no chance of unifying" test, see calls to
+ `mightPossiblyUnify` in `canEqCanLHS2; and Note [Orienting TyVarLHS/TyFamLHS]
* But if there /is/ a chance of unifying, put the tyvar on the left,
(a ~ F tys), as this may be our only shot to unify. Again see
- `put_tyvar_on_lhs`.
+ `mightPossiblyUnify`.
* But if we /fail/ to unify then flip back to (F tys ~ a) because it's
- generally better to rewrite away function calls. See the call to
- `swapAndFinish` in `canEqCanLHSFinish_try_unification`
+ generally better to rewrite away function calls. See the swapping-back
+ code in `finish_on_unify` in `canEqCanLHSFinish_try_unification`
It's important to flip back. Consider
[W] F alpha ~ alpha
@@ -2197,71 +2198,64 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
= return True
-----------------------
-canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
- -- Try unification; for Wanted, Nominal equalities with a meta-tyvar on the LHS
- | CtWanted wev <- ev -- See Note [Do not unify Givens]
+mightPossiblyUnify :: CtEvidence -> EqRel -> TcTyVar -> Bool
+-- Is this equality (tv ~ ty) one we could perhaps solve by unification?
+-- True <=> perhaps yes
+-- False <=> definitely not
+mightPossiblyUnify ev eq_rel tv
+ | isMetaTyVar tv
+ , CtWanted wev <- ev -- See Note [Do not unify Givens]
, NomEq <- eq_rel -- See Note [Do not unify representational equalities]
, wantedCtHasNoRewriters wev -- See Note [Unify only if the rewriter set is empty]
- , TyVarLHS lhs_tv <- lhs
+ = True
+ | otherwise
+ = False
+
+canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
+ -- Try unification; for Wanted, Nominal equalities with a meta-tyvar on the LHS
+ | TyVarLHS lhs_tv <- lhs
+ , mightPossiblyUnify ev eq_rel lhs_tv
= do { given_eq_lvl <- getInnermostGivenEqLevel
; case simpleUnifyCheck UC_Solver given_eq_lvl lhs_tv rhs of
- SUC_CanUnify ->
- unify lhs_tv (mkReflRedn Nominal rhs)
- SUC_CannotUnify
- | Just can_rhs <- canTyFamEqLHS_maybe rhs
- -> swap_and_finish lhs_tv can_rhs -- See Note [Orienting TyVarLHS/TyFamLHS]
- | otherwise
- -> finish_no_unify
- SUC_NotSure ->
- -- We have a touchable unification variable on the left,
+ SUC_CannotUnify -> finish_no_unify
+ SUC_CanUnify -> do_unification lhs_tv (mkReflRedn Nominal rhs)
+ SUC_NotSure ->
+ -- We have a touchable, unfilled unification variable on the left,
-- and the top-shape check succeeded. These are both guaranteed
-- by the fact that simpleUnifyCheck did not return SUC_CannotUnify.
+ --
+ -- Next, do a full `checkTyEqRhs` check to see if we can unify
+ -- See Note [checkTyEqRhs] in GHC.Tc.Utils.Unify
do { let flags = unifyingLHSMetaTyVar_TEFTask ev lhs_tv
; check_result <- wrapTcS (checkTyEqRhs flags rhs)
+ ; traceTcS "canEqCanLHSFinish_try_unification" $
+ vcat [ text "lhs" <+> ppr lhs
+ , text "rhs" <+> ppr rhs
+ , text "check_result" <+> ppr check_result ]
; case check_result of
- PuOK cts rhs_redn ->
- do { emitWork cts
- ; unify lhs_tv rhs_redn }
- PuFail reason
- | Just can_rhs <- canTyFamEqLHS_maybe rhs
- -> swap_and_finish lhs_tv can_rhs -- See Note [Orienting TyVarLHS/TyFamLHS]
- | reason `cterHasOnlyProblems` do_not_prevent_rewriting
- ->
- -- ContinueWith, to allow using this constraint for
- -- rewriting (e.g. alpha[2] ~ beta[3]).
- do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs
- ; continueWith $ Right $
- EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
- , eq_lhs = lhs , eq_rhs = rhs }
- }
- | otherwise
- -> try_irred reason
- }
+ PuFail {} -> finish_no_unify
+ PuOK cts rhs_redn -> do { emitWork cts
+ ; do_unification lhs_tv rhs_redn } }
}
-- Otherwise unification is off the table
| otherwise
= finish_no_unify
where
- -- We can't unify, but this equality can go in the inert set
- -- and be used to rewrite other constraints.
- finish_no_unify =
- canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
-
- -- We can't unify, and this equality should not be used to rewrite
- -- other constraints (e.g. because it has an occurs check).
- -- So add it to the inert Irreds.
- try_irred reason =
- tryIrredInstead reason ev eq_rel swapped lhs rhs
-
- -- We can't unify as-is, and want to flip the equality around.
- -- Example: alpha ~ F tys, flip it around to become the canonical
- -- equality f tys ~ alpha.
- swap_and_finish tv can_rhs =
- swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs
-
- -- Phew! Finally! We can unify; go ahead and do so.
- unify tv rhs_redn =
+ -- finish_no_unify: abandon the attempt to unify, and instead hand off to
+ -- canEqCanLHSFinish_no_unification
+ -- First, though, if we have (tv ~ F tys)
+ -- swap it over so we get (F tys ~ tv), with `F tys` on the LHS
+ -- See Note [Orienting TyVarLHS/TyFamLHS]
+ finish_no_unify
+ | TyVarLHS lhs_tv <- lhs
+ , Just can_rhs <- canTyFamEqLHS_maybe rhs
+ = canEqCanLHSFinish_no_unification ev eq_rel (flipSwap swapped) can_rhs (mkTyVarTy lhs_tv)
+ | otherwise
+ = canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
+
+ -- do_unification: Phew! Finally! We can unify; go ahead and do so.
+ do_unification tv rhs_redn =
do { -- In the common case where rhs_redn is Refl, we don't need to rewrite
-- the evidence, even if swapped=IsSwapped. Suppose the original was
-- [W] co : Int ~ alpha
@@ -2273,7 +2267,8 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
else rewriteEqEvidence ev swapped
(mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn
emptyCoHoleSet
- -- emptyCoHoleSet: rhs_redn has no CoercionHoles
+ -- emptyCoHoleSet: we are about to /solve/ this
+ -- constraint, so its CoHoleSet doesn't matter
; let tv_ty = mkTyVarTy tv
final_rhs = reductionReducedType rhs_redn
@@ -2297,45 +2292,48 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
; return (Stop new_ev (text "Solved by unification")) }
---------------------------
--- Unification is off the table
canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
- = do { -- Do checkTypeEq to guarantee (TyEq:OC), (TyEq:F)
+ -- We can't unify, but we can see if this equality can go in the inert set
+ -- and be used to rewrite other constraints.
+ -- See Note [Equalities where unification fails]
+ = do { -- Do checkTypeEqNoUnification to guarantee (TyEq:OC), (TyEq:F)
-- Must do the occurs check even on tyvar/tyvar equalities,
-- in case have x ~ (y :: ..x...); this is #12593.
- ; check_result <- checkTypeEq ev eq_rel lhs rhs
-
- ; let lhs_ty = canEqLHSType lhs
+ ; check_result <- checkTypeEqNoUnification ev eq_rel lhs rhs
; case check_result of
PuFail reason
-
- -- If we had F a ~ G (F a), which gives an occurs check,
- -- then swap it to G (F a) ~ F a, which does not
- -- However `swap_for_size` above will orient it with (G (F a)) on
- -- the left anwyway. `swap_for_rewriting` "wins", but that doesn't
- -- matter: in the occurs check case swap_for_rewriting will be moot.
- -- TL;DR: the next four lines of code are redundant
- -- I'm leaving them here in case they become relevant again
--- | TyFamLHS {} <- lhs
--- , Just can_rhs <- canTyFamEqLHS_maybe rhs
--- , reason `cterHasOnlyProblem` cteSolubleOccurs
--- -> swapAndFinish ev eq_rel swapped lhs_ty can_rhs
--- | otherwise
-
- | reason `cterHasOnlyProblems` do_not_prevent_rewriting
- -> do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs
- ; continueWith $ Right $
- EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
- , eq_lhs = lhs , eq_rhs = rhs }
- }
-
- | otherwise
- -> tryIrredInstead reason ev eq_rel swapped lhs rhs
+ -> -- We can't unify, and this equality should not be used to rewrite
+ -- other constraints (e.g. because it has an occurs check).
+ -- So add it to the inert Irreds.
+ -- NB: The `reason` will never include `cteConcrete` or `cteSkolemEscape`
+ -- because checkTypeEqNoUnification doesn't check for those things;
+ -- they do not prevent the equality being canonical. So you can't
+ -- rely on `reason` reporting those points, nor do we need to.
+ do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs
+ ; finishCanWithIrred (NonCanonicalReason reason) new_ev }
PuOK new_eqs rhs_redn
- -> do { emitWork new_eqs
- ; let new_holes = rewriterSetFromCts new_eqs
+ -> -- Put this constraint into the inert set, so that it will be used
+ -- to solve or rewrite other constraints.
+ --
+ -- NB: checkTypeEqNoUnification does not check for
+ -- (a) skolem-escape (tefTyVar_levelCheck = LC_None)
+ -- (b) concreteness (tefTyVar_concreteCheck = CC_None)
+ -- So an equality whose only problem is e.g. skolem-escape will
+ -- return PuOK, will be put in the inert set, will be used for
+ -- rewriting. That is fine.
+ --
+ -- assertPpr (isEmptyCts new_eqs):
+ -- checkTypeEqNoUnification does neither promotion nor type-family
+ -- flattening for Wanteds, and hence creates no equalities to solve
+ assertPpr (isEmptyCts new_eqs)
+ (vcat [ text "new_eqs" <+> ppr new_eqs
+ , text "rhs_redn" <+> ppr rhs_redn
+ , text "lhs" <+> ppr lhs
+ , text "rhs" <+> ppr rhs ]) $
+ do { let lhs_ty = canEqLHSType lhs
lhs_redn = mkReflRedn (eqRelRole eq_rel) lhs_ty
- ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn new_holes
+ ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn emptyCoHoleSet
-- Important: even if the coercion is Refl,
-- * new_ev has reductionReducedType on the RHS
@@ -2346,45 +2344,56 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
, eq_lhs = lhs
, eq_rhs = reductionReducedType rhs_redn } } }
--- | Some problems prevent /unification/ but not /rewriting/:
---
--- Skolem-escape: if we have [W] alpha[2] ~ Maybe b[3]
--- we can't unify (skolem-escape); but it /is/ canonical,
--- and hence we /can/ use it for rewriting
---
--- Concrete-ness: alpha[conc] ~ b[sk]
--- We can use it to rewrite; we still have to solve the original
-do_not_prevent_rewriting :: CheckTyEqResult
-do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<>
- cteProblem cteConcrete
+checkTypeEqNoUnification :: CtEvidence -> EqRel -> CanEqLHS -> TcType
+ -> TcS (PuResult Ct Reduction)
+-- Used for general CanEqLHSs, when we have decided that we cannot unify
+checkTypeEqNoUnification ev eq_rel lhs rhs =
+ case ev of
+ CtGiven {} ->
+ do { traceTcS "checkTypeEqNoUnification (given) {" (vcat [ text "lhs:" <+> ppr lhs
+ , text "rhs:" <+> ppr rhs ])
+ ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs)
+ ; traceTcS "checkTypeEqNoUnification }" (ppr check_result)
+ ; case check_result of
+ PuFail reason -> return (PuFail reason)
+ PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs
+ ; emitWork new_givens
+ ; updInertSet (addCycleBreakerBindings prs)
+ ; return (pure redn) } }
+ CtWanted {} -> do { traceTcS "checkTypeEqNoUnification (wanted) {" $
+ vcat [ text "lhs:" <+> ppr lhs
+ , text "rhs:" <+> ppr rhs ]
+ ; check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs)
+ ; traceTcS "checkTypeEqNoUnification }" (ppr check_result)
+ ; return check_result }
+ where
+ wanted_flags :: TyEqFlags TcM Ct
+ wanted_flags = notUnifying_TEFTask occ_prob lhs
+ -- See Note [Don't cycle-break Wanteds when not unifying]
+
+ given_flags :: TyEqFlags TcM (TcTyVar, TcType)
+ given_flags = wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven }
+ -- TEFA_Break used for: [G] a ~ Maybe (F a)
+ -- or [G] F a ~ Maybe (F a)
+
+ -- occ_prob: see Note [Occurs check and representational equality]
+ occ_prob = case eq_rel of
+ NomEq -> cteInsolubleOccurs
+ ReprEq -> cteSolubleOccurs
+
+ ---------------------------
+ mk_new_given :: (TcTyVar, TcType) -> TcS Ct
+ mk_new_given (new_tv, fam_app)
+ = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term)
+ where
+ new_ty = mkTyVarTy new_tv
+ given_pred = mkNomEqPred fam_app new_ty
+ given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note
-----------------------
-swapAndFinish :: CtEvidence -> EqRel -> SwapFlag
- -> TcType -> CanEqLHS -- ty ~ F tys
- -> TcS (StopOrContinue (Either unused EqCt))
--- We have an equality alpha ~ F tys, that we can't unify e.g because 'tys'
--- mentions alpha, it would not be a canonical constraint as-is.
--- We want to flip it to (F tys ~ a), whereupon it is canonical
-swapAndFinish ev eq_rel swapped lhs_ty can_rhs
- = do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel (flipSwap swapped) can_rhs lhs_ty
- ; continueWith $ Right $
- EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
- , eq_lhs = can_rhs, eq_rhs = lhs_ty } }
+ -- See Detail (7) of the Note
+ cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
----------------------
-tryIrredInstead :: CheckTyEqResult -> CtEvidence
- -> EqRel -> SwapFlag -> CanEqLHS -> TcType
- -> TcS (StopOrContinue (Either IrredCt unused))
--- We have a non-canonical equality
--- We still swap it if 'swapped' says so, so that it is oriented
--- in the direction that the error-reporting machinery
--- expects it; e.g. (m ~ t m) rather than (t m ~ m)
--- This is not very important, and only affects error reporting.
-tryIrredInstead reason ev eq_rel swapped lhs rhs
- = do { traceTcS "cantMakeCanonical" (ppr reason $$ ppr lhs $$ ppr rhs)
- ; new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs
- ; finishCanWithIrred (NonCanonicalReason reason) new_ev }
-
finishCanWithIrred :: CtIrredReason -> CtEvidence
-> TcS (StopOrContinue (Either IrredCt a))
finishCanWithIrred reason ev
@@ -2404,8 +2413,63 @@ canEqReflexive ev eq_rel ty
= do { setEqIfWanted ev (mkReflCPH eq_rel ty)
; stopWith ev "Solved by reflexivity" }
-{- Note [Equalities with heterogeneous kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Equalities where unification fails]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we can't unify, but the equality is canonical, we still want to add it to the
+inert set so that it can be used to rewrite other Wanteds. (There are many
+reasons that unification might not happen: the LHS is not a touchable unification
+variable, it has rewriters, it's a Given etc.)
+
+* In this case we call `checkTypeEqNoUnification` to see whether it is canonical
+ (which in turn calls `checkTypeEqRhs` with suitable flags).
+
+* NB: we do /not/ try to take advantage of the case where
+ `canEqCanLHSFinish_try_unification` has already called `checkTyEqRhs`; doing so
+ caused #27844. (The first call did fam-app breaking, which concealed a genuine
+ occurs check.) It's just too clever; better to do the simple thing.
+
+Note [Don't cycle-break Wanteds when not unifying]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ [W] a[2] ~ Maybe (F a[2])
+
+Should we cycle-break this Wanted, thus?
+
+ [W] a[2] ~ Maybe delta[2]
+ [W] delta[2] ~ F a[2]
+
+For a start, this is dodgy because we might just unify delta, thus undoing
+what we have done, and getting an infinite loop in the solver. Even if we
+somehow prevented ourselves from doing so, is there any merit in the split?
+Maybe: perhaps we can use that equality on `a` to unlock other constraints?
+Consider
+ type instance F (Maybe _) = Bool
+
+ [G] g1: a ~ Maybe Bool
+ [W] w1: a ~ Maybe (F a)
+
+If we loop-break w1 to get
+ [W] w1': a ~ Maybe gamma
+ [W] w3: gamma ~ F a
+Now rewrite w3 with w1'
+ [W] w3': gamma ~ F (Maybe gamma)
+Now use the type instance to get
+ gamma := Bool
+Now we are left with
+ [W] w1': a ~ Maybe Bool
+which we can solve from the Given.
+
+BUT in this situation we could have rewritten the
+/original/ Wanted from the Given, like this:
+ [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool))
+and that is readily soluble.
+
+In short: loop-breaking Wanteds, when we aren't unifying,
+seems of no merit. Hence TEFA_Recurse, rather than TEFA_Break,
+in `wanted_flags` in `checkTypeEqNoUnification`.
+
+Note [Equalities with heterogeneous kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
What do we do when we have an equality
(tv :: k1) ~ (rhs :: k2)
@@ -2587,8 +2651,8 @@ The details depend on whether we're working with a Given or a Wanted.
Given
-----
We emit a new Given, [G] F a ~ cbv, equating the type family application
-to our new cbv. This is actually done by `break_given` in
-`GHC.Tc.Solver.Monad.checkTypeEq`.
+to our new cbv. This is actually done by `BreakGiven` in the `given_flags`
+in `checkTypeEqNoUnification`.
Note its orientation: The type family ends up on the left; see
Note [Orienting TyFamLHS/TyFamLHS]. No special treatment for
@@ -2629,7 +2693,7 @@ Note that
Wanted
------
First, we do not cycle-break unless the LHS is a unifiable type variable
-See Note [Don't cycle-break Wanteds when not unifying] in GHC.Tc.Solver.Monad.
+See Note [Don't cycle-break Wanteds when not unifying].
OK, so suppose the LHS is a unifiable type variable. The fresh cycle-breaker
variables here must actually be normal, touchable metavariables. That is, they
@@ -3073,11 +3137,10 @@ inertsEqsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w
|| (empty_rw_w && not (isEmptyCoHoleSet (ctEvRewriters ev_i)))
-- Prefer the one that has no rewriters
-- See (CE4) in Note [Combining equalities]
+ -- and (WRW10) in Note [Wanteds rewrite Wanteds: rewriter-sets]
inertsEqsCanDischarge _ _ = Nothing
-
-
{- Note [Do not unify Givens]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this GADT match
@@ -3143,34 +3206,6 @@ Wrinkles:
we should kick out `co` so that we can now unify it, which might
unlock other stuff. See `kickOutAfterFillingCoercionHole` in
GHC.Tc.Solver.Monad.
-
-Note [Solve by unification]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If we solve
- alpha[n] ~ ty
-by unification, there are two cases to consider
-
-* TouchableSameLevel: if the ambient level is 'n', then
- we can simply update alpha := ty, and do nothing else
-
-* TouchableOuterLevel free_metas n: if the ambient level is greater than
- 'n' (the level of alpha), in addition to setting alpha := ty we must
- do two other things:
-
- 1. Promote all the free meta-vars of 'ty' to level n. After all,
- alpha[n] is at level n, and so if we set, say,
- alpha[n] := Maybe beta[m],
- we must ensure that when unifying beta we do skolem-escape checks
- etc relevant to level n. Simple way to do that: promote beta to
- level n.
-
- 2. Set the Unification Level Flag to record that a level-n unification has
- taken place. See Note [WhatUnifications] in GHC.Tc.Utils.Unify
-
-NB: TouchableSameLevel is just an optimisation for TouchableOuterLevel. Promotion
-would be a no-op, and setting the unification flag unnecessarily would just
-make the solver iterate more often. (We don't need to iterate when unifying
-at the ambient level because of the kick-out mechanism.)
-}
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -22,7 +22,7 @@ module GHC.Tc.Solver.InertSet (
InertEqs,
foldTyEqs, delEq, findEq,
partitionInertEqs, partitionFunEqs, transformAndPartitionTyVarEqs,
- filterInertEqs, filterFunEqs,
+ filterInertEqs, filterFunEqs, transformAndPartitionFunEqs,
foldFunEqs, addEqToCans,
-- * Inert Dicts
@@ -128,7 +128,7 @@ Further refinements:
* Among the equalities we prioritise ones with an empty rewriter set;
see Note [Wanteds rewrite Wanteds: rewriter-sets] in GHC.Tc.Types.Constraint,
- wrinkle (WRW8).
+ wrinkle (WRW7).
* Among equalities with an empty rewriter set, we prioritise nominal equalities.
* They have more rewriting power, so doing them first is better.
@@ -983,7 +983,7 @@ How do we establish these conditions?
with S(fw,_).
* (T3) is guaranteed by an occurs-check on the work item.
- This is done during canonicalisation, in checkTypeEq; invariant
+ This is done during canonicalisation, in checkTyEqRhs; invariant
(TyEq:OC) of CEqCan. See also Note [EqCt occurs check] in GHC.Tc.Types.Constraint.
* (T4) is established by GHC.Tc.Solver.Monad.kickOutRewritable. If the inert
@@ -1422,6 +1422,19 @@ addCanFunEq old_eqs fun_tc fun_args ct
foldFunEqs :: (EqCt -> b -> b) -> FunEqMap EqualCtList -> b -> b
foldFunEqs k fun_eqs z = foldTcAppMap (\eqs z -> foldr k z eqs) fun_eqs z
+transformAndPartitionFunEqs
+ :: (EqCt -> Either EqCt EqCt) -- Left => chuck out, Right => keep
+ -> InertFunEqs
+ -> ([EqCt], InertFunEqs) -- (chuck-out, keep)
+transformAndPartitionFunEqs pred orig_inerts
+ = foldFunEqs folder orig_inerts ([], emptyFunEqs)
+ where
+ folder :: EqCt -> ([EqCt], InertFunEqs) -> ([EqCt], InertFunEqs)
+ folder eq_ct (acc_true, acc_false)
+ = case pred eq_ct of
+ Left eq_ct' -> (eq_ct' : acc_true, acc_false)
+ Right eq_ct' -> (acc_true, addFunEqs eq_ct' acc_false)
+
partitionFunEqs :: (EqCt -> Bool) -- EqCt will have a TyFamLHS
-> InertFunEqs
-> ([EqCt], InertFunEqs)
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -117,10 +117,7 @@ module GHC.Tc.Solver.Monad (
getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
matchFam, matchFamTcM,
checkWellLevelledDFun,
- pprEq,
-
- -- Enforcing invariants for type equalities
- checkTypeEq
+ pprEq
) where
import GHC.Prelude
@@ -436,32 +433,48 @@ we should kick out `co` so that we can now unify it, which might unlock other st
See Note [Unify only if the rewriter set is empty] in GHC.Tc.Solver.Equality for
why solving `kco` might unlock `co`, especially (URW2).
-Hence `kickOutAfterFillingCoercionHole`. It looks at inert constraints that are
+Hence `kickOutAfterFillingCoercionHole`. It looks at inert constraints
+ [W] co :: ty1 ~ tys
+that are
* Wanted
- * Of the form alpha ~ rhs, where alpha is a unification variable
-and kicks out any that will have an empty rewriter set after filling the hole.
+ * Of the form (alpha ~ rhs)
+ or (F tys ~ alpha)
+ or (F tys ~ alpha |> co)
+ where alpha is a unification variable
+ and kicks out any that have an empty rewriter set after filling the hole.
Wrinkles:
+
(KOC1) If co's rewriter-set is {kco, xco}, there is no point in kicking it out,
because it still can't be unified. So we only kick out if the co's
rewriter-set becomes empty.
-(KOC2) `kco` might itself have a rewriter set. This is fairly common. E.g.
+(KOC2) `kco` might itself have been rewritten by other as-yet-unsolved new_holes.
+ This is fairly common. E.g.
kco : a[sk] ~ beta[tau]
Assuming we can't unify it for some reason, we may swap that over to give
kco2 : beta[tau] ~ a[sk] kco := sym kco2
So `kco` is "solved" but the coercion that solves it has free coercion holes!
So rather than kick out `co`, we should just change its rewriter-set to depend
- on `kco2` instead of `kco`. Hence the `new_holes` passed to
- `kickOutAfterFillingCoercionHole`
+ on `kco2` instead of `kco`.
-(KOC3) It's possible that this could just go ahead and unify, but could there
- be occurs-check problems? Seems simpler just to kick out.
+ Hence the `new_holes` passed to `kickOutAfterFillingCoercionHole`
+
+(KOC3) It's possible that this could just go ahead and unify on the spot, but could
+ there be occurs-check problems? Seems simpler just to kick out.
(KOC4) Kick-out is undesirable, so it'd be better to solve `kco` before `co`. So
the solver prioritises equalities with an empty rewriter set, to try to
avoid unnecessary kick-out. See GHC.Tc.Types.Constraint
Note [Prioritise Wanteds with empty CoHoleSet] esp (PER1)
+
+(KOC5) We kick out from both `inert_eqs` and `inert_funeqs`. The latter is needed
+ in case we have (F tys ~ alpha), which might (if it now has an empty rewriter
+ set) allow unifying alpha.
+
+(KOC6) Annoyingly, we /also/ need to look for (F tys ~ (alpha |> co)), with a cast,
+ because that may be unifiable by moving the cast to the other side. Hence
+ `getCastedTyVar_maybe`.
-}
kickOutRewritable :: KickOutSpec -> CtFlavourRole -> TcS ()
@@ -526,27 +539,36 @@ kickOutAfterFillingCoercionHole hole (CPH { cph_holes = new_holes })
; setInertCans ics' }
where
kick_out :: InertCans -> ([EqCt], InertCans)
- kick_out ics@(IC { inert_eqs = eqs })
- = (eqs_to_kick, ics { inert_eqs = eqs_to_keep })
+ kick_out ics@(IC { inert_eqs = eqs, inert_funeqs = funeqs })
+ = ( kick_funeqs ++ kick_eqs
+ , ics { inert_eqs = keep_eqs, inert_funeqs = keep_funeqs })
where
- (eqs_to_kick, eqs_to_keep) = transformAndPartitionTyVarEqs kick_out_eq eqs
+ (kick_eqs, keep_eqs) = transformAndPartitionTyVarEqs kick_out_eq eqs
+ (kick_funeqs, keep_funeqs) = transformAndPartitionFunEqs kick_out_eq funeqs
+ -- Kick out from funeqs as well as eqs.
+ -- See (KOC5) in Note [Kick out after filling a coercion hole]
kick_out_eq :: EqCt -> Either EqCt EqCt
- kick_out_eq eq_ct@(EqCt { eq_ev = ev, eq_lhs = lhs })
+ kick_out_eq eq_ct@(EqCt { eq_ev = ev })
| CtWanted (wev@(WantedCt { ctev_rewriters = rewriters })) <- ev
- , TyVarLHS tv <- lhs
- , isMetaTyVar tv
, hole `elemCoHoleSet` rewriters
- , let holes' = (rewriters `delCoHoleSet` hole) `mappend` new_holes
- -- Adding new_holes and deleting hole: see (KOC2)
- eq_ct' = eq_ct { eq_ev = CtWanted (wev { ctev_rewriters = holes' }) }
- = if isEmptyCoHoleSet holes'
+ , is_meta_tv_equality eq_ct
+ , let rewriters' = (rewriters `delCoHoleSet` hole) `mappend` new_holes
+ -- Adding new_holes and deleting hole: see (KOC2)
+ eq_ct' = eq_ct { eq_ev = CtWanted (wev { ctev_rewriters = rewriters' }) }
+ = if isEmptyCoHoleSet rewriters'
then Left eq_ct' -- Kick out, if new rewriter set is empty (KOC1)
else Right eq_ct' -- Keep, but with trimmed holes see (KOC2)
+
| otherwise
= Right eq_ct
---------------
+ is_meta_tv_equality (EqCt { eq_lhs = lhs, eq_rhs = rhs })
+ | TyVarLHS tv <- lhs = isMetaTyVar tv
+ | Just (tv,_) <- getCastedTyVar_maybe rhs = isMetaTyVar tv
+ | otherwise = False
+ -- getCastedTyVar: see (KOC5) in Note [Kick out after filling a coercion hole]
+
insertSafeOverlapFailureTcS :: InstanceWhat -> DictCt -> TcS ()
-- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver
insertSafeOverlapFailureTcS what item
@@ -2302,52 +2324,6 @@ wrapUnifier rws loc role do_unifications
************************************************************************
-}
-checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType
- -> TcS (PuResult Ct Reduction)
--- Used for general CanEqLHSs, ones that do
--- not have a touchable type variable on the LHS (i.e. not unifying)
-checkTypeEq ev eq_rel lhs rhs =
- case ev of
- CtGiven {} ->
- do { traceTcS "checkTypeEq {" (vcat [ text "lhs:" <+> ppr lhs
- , text "rhs:" <+> ppr rhs ])
- ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs)
- ; traceTcS "checkTypeEq }" (ppr check_result)
- ; case check_result of
- PuFail reason -> return (PuFail reason)
- PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs
- ; emitWork new_givens
- ; updInertSet (addCycleBreakerBindings prs)
- ; return (pure redn) } }
- CtWanted {} -> wrapTcS (checkTyEqRhs wanted_flags rhs)
- where
- wanted_flags :: TyEqFlags TcM Ct
- wanted_flags = notUnifying_TEFTask occ_prob lhs
- -- checkTypeEq deals only with the non-unifying case
-
- given_flags :: TyEqFlags TcM (TcTyVar, TcType)
- given_flags = wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven }
- -- TEFA_Break used for: [G] a ~ Maybe (F a)
- -- or [W] F a ~ Maybe (F a)
-
- -- occ_prob: see Note [Occurs check and representational equality]
- occ_prob = case eq_rel of
- NomEq -> cteInsolubleOccurs
- ReprEq -> cteSolubleOccurs
-
- ---------------------------
- mk_new_given :: (TcTyVar, TcType) -> TcS Ct
- mk_new_given (new_tv, fam_app)
- = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term)
- where
- new_ty = mkTyVarTy new_tv
- given_pred = mkNomEqPred fam_app new_ty
- given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note
-
- -- See Detail (7) of the Note
- cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
-
--------------------------
-- | Fill in CycleBreakerTvs with the variables they stand for.
-- See Note [Type equality cycles] in GHC.Tc.Solver.Equality
restoreTyVarCycles :: InertSet -> TcM ()
@@ -2363,43 +2339,4 @@ restoreTyVarCycles is
(a ~R# b a) is soluble if b later turns out to be Identity
So we treat this as a "soluble occurs check".
-Note [Don't cycle-break Wanteds when not unifying]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consdier
- [W] a[2] ~ Maybe (F a[2])
-
-Should we cycle-break this Wanted, thus?
-
- [W] a[2] ~ Maybe delta[2]
- [W] delta[2] ~ F a[2]
-
-For a start, this is dodgy because we might just unify delta, thus undoing
-what we have done, and getting an infinite loop in the solver. Even if we
-somehow prevented ourselves from doing so, is there any merit in the split?
-Maybe: perhaps we can use that equality on `a` to unlock other constraints?
-Consider
- type instance F (Maybe _) = Bool
-
- [G] g1: a ~ Maybe Bool
- [W] w1: a ~ Maybe (F a)
-
-If we loop-break w1 to get
- [W] w1': a ~ Maybe gamma
- [W] w3: gamma ~ F a
-Now rewrite w3 with w1'
- [W] w3': gamma ~ F (Maybe gamma)
-Now use the type instance to get
- gamma := Bool
-Now we are left with
- [W] w1': a ~ Maybe Bool
-which we can solve from the Given.
-
-BUT in this situation we could have rewritten the
-/original/ Wanted from the Given, like this:
- [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool))
-and that is readily soluble.
-
-In short: loop-breaking Wanteds, when we aren't unifying,
-seems of no merit. Hence TEFA_Recurse, rather than TEFA_Break,
-in `wanted_flags` in `checkTypeEq`.
-}
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -524,7 +524,7 @@ isInsolubleReason (InsolubleFunDepReason {}) = True
------------------------------------------------------------------------------
-- | A /set/ of problems in checking the validity of a type equality.
--- See 'checkTypeEq'.
+-- See 'GHC.Tc.Utils.Unify.checkTyEqRhs'.
newtype CheckTyEqResult = CTER Word8
-- | No problems in checking the validity of a type equality.
@@ -2603,19 +2603,24 @@ The rewriter-set plan
thereby dropping the reference to `co`. I'm not certain whether this actually
happens or not.
-(WRW7) In error reporting, we simply suppress any errors that have been rewritten
- by /unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem,
+(WRW7) When we fill a coercion hole `h` we kick out any inert Wanted that has `h`
+ in its rewriter set. See `kickOutAfterFilling CoercionHole`.
+ See Note [Kick out after filling a coercion hole] in GHC.Tc.Solver.Monad.
+
+ Furthermore, when we select a work item, in `selectNextWorkItem` we zonk the
+ rewriter set so that it accurately reflects the unsolved coercion holes. That
+ sets it up ready for the no-rewriter check in (WR5), when we process the equality.
+
+ In `selectNextWorkItem`, we also prioritise equalities with no rewiters.
+ See Note [Prioritise Wanteds with empty CoHoleSet] in GHC.Tc.Types.Constraint
+ wrinkle (PER1).
+
+(WRW8) In error reporting, we suppress any errors that have been rewritten
+ by /unsolved/ wanteds. This suppression happens in `GHC.Tc.Errors.mkErrorItem`,
which uses `GHC.Tc.Zonk.Type.zonkCoHoleSet` to look through any filled
coercion holes. The idea is that we wish to report the "root cause" -- the
error that rewrote all the others.
-(WRW8) In `selectNextWorkItem`, priorities equalities with no rewiters. See
- Note [Prioritise Wanteds with empty CoHoleSet] in GHC.Tc.Types.Constraint
- wrinkle (PER1).
-
-(WRW9) In error reporting, we prioritise Wanteds that have an empty CoHoleSet:
- see Note [Prioritise Wanteds with empty CoHoleSet].
-
Let's continue our first example above:
inert: [W] w1 :: a ~ Char
@@ -2641,8 +2646,10 @@ Wrinkles:
(WRW11) When zonking a constraint (with `zonkCt` and `zonkCtEvidence`) we take
the opportunity to zonk its `CoHoleSet`, which eliminates solved ones.
- This doesn't guarantee that rewriter sets are always up to date -- c.f.
- (WRW10) -- but it helps, and it de-clutters debug output.
+ This doesn't guarantee that rewriter sets are always up to date (c.f. (WRW10))
+ but it helps, and it de-clutters debug output.
+
+ See also (WRW7) which does the crucial just-in-time zonking of the rewriters.
Note [Prioritise Wanteds with empty CoHoleSet]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2685,9 +2692,8 @@ in our simplify_loop iteration, we happened to start with co_aym. All would have
been well if we'd started with the (not-rewritten) co_ayb and gotten it into the
inert set.
-With that in mind, we /prioritise/ the work-list to put
-constraints with no rewriters first. This prioritisation
-is done in `GHC.Tc.Solver.Monad.selectNextWorkItem`.
+With that in mind, we /prioritise/ the work-list to put constraints with no rewriters
+first. This prioritisation is done in `GHC.Tc.Solver.Monad.selectNextWorkItem`.
Wrinkles
@@ -2700,8 +2706,8 @@ Wrinkles
order to report /some/ error in this case, we simply report all the
Wanteds. The user will get a perhaps-confusing error message, but they've
written a confusing program! (T22707 and T22793 were close, but they do
- not exhibit this behaviour.) So belt and braces: see the `suppress`
- stuff in GHC.Tc.Errors.mkErrorItem.
+ not exhibit this behaviour.) So belt and braces:
+ see `GHC.Tc.Errors.reportWanteds`.
Note [Avoiding rewriting cycles]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -3617,15 +3617,20 @@ instance Outputable SimpleUnifyResult where
simpleUnifyCheck :: UnifyCheckCaller -> TcLevel -> TcTyVar -> TcType -> SimpleUnifyResult
-- ^ A fast check for unification. May return "not sure", in which case
-- unification might still be OK, but it'll take more work to do
--- (use the full 'checkTypeEq').
+-- (use the full 'checkTyEqRhs').
--
--- * Rejects if lhs_tv occurs in rhs_ty (occurs check)
--- * Rejects foralls unless
--- lhs_tv is RuntimeUnk (used by GHCi debugger)
--- or is a QL instantiation variable
--- * Rejects a non-concrete type if lhs_tv is concrete
--- * Rejects type families unless fam_ok=True
--- * Does a level-check for type variables, to avoid skolem escape
+-- It returns SUC_CannotUnify for
+-- * Touchability failure
+-- * Top level-shape failure
+--
+-- It returns SUC_NotSure for
+-- * Occurs check: lhs_tv occurs in rhs_ty
+-- * Type families unless fam_ok=True
+-- * Foralls unless
+-- lhs_tv is RuntimeUnk (used by GHCi debugger)
+-- or is a QL instantiation variable
+-- * Concreteness: lhs_tv is concrete and rhs is a non-concrete type
+-- * Skolem-escape: a level-check for type variables, to avoid skolem escape
--
-- This function is pretty heavily used, so it's optimised not to allocate
simpleUnifyCheck caller given_eq_lvl lhs_tv rhs
@@ -3753,8 +3758,8 @@ Consider
[W] alpha[2] ~ Maybe (S beta[4] gamma[2])
We don't want to promote beta to level 2; rather, we should
-expand the synonym. (Currently, in checkTypeEqRhs promotion
-is irrevocable, by side effect.)
+expand the synonym. (Currently, in `checkTyEqRhs` promotion
+is irrevocable, by side effect in `promote` in `checkTyVar`.)
To avoid this risk we eagerly expand forgetful synonyms.
This also means we won't get an occurs check in
@@ -4198,7 +4203,7 @@ famAppArgFlags flags = case flags of
The key function `checkTyEqRhs ty_eq_flags rhs` is called on the
RHS of a type equality
lhs ~ rhs
-and checks to see if `rhs` satisfies, or can be made to satisfy,
+and checks to see if `rhs` satisfies, /or can be made to satisfy/,
invariants described by `ty_eq_flags`. It can succeded or fail; in
the latter case it returns a `CheckTyEqResult` that describes why it
failed.
@@ -4219,6 +4224,15 @@ Notably, it can check for things like:
* Concreteness error
e.g. alpha[conc] ~ r[sk]
+Note "or can be made to satisfy the preconditions"! `checkTyEqRhs` may transform
+the RHS by
+
+ * Turning a type-family application into a type variable, perhaps to avoid
+ an occurs check. See Note Note [Family applications in canonical constraints]
+
+ * Promoting any nested unification variables, in order to satisfy the
+ level invariant. See Note [Promotion and level-checking]
+
Its specific behaviour is governed by the `TyEqFlags` that are passed
to it; see Note [TyEqFlags].
@@ -4275,7 +4289,7 @@ NB: We never see a TyVarLHS here, such as
[G] a ~ F tys here
because we'd have swapped it to
[G] F tys ~ a
-in canEqCanLHS2, before getting to checkTypeEq.
+in canEqCanLHS2, before getting to checkTyEqRhs.
-}
check_ty_eq_rhs :: forall m a
@@ -4799,7 +4813,6 @@ promote_meta_tyvar info dest_lvl occ_tv
touchabilityTest :: TcLevel -> TcTyVar -> Bool
-- ^ This is the key test for untouchability:
-- See Note [Unification preconditions] in GHC.Tc.Utils.Unify
--- and Note [Solve by unification] in GHC.Tc.Solver.Equality
--
-- @True@ <=> the variable is touchable
touchabilityTest given_eq_lvl tv
=====================================
testsuite/tests/indexed-types/should_fail/T9662.stderr
=====================================
@@ -1,12 +1,12 @@
T9662.hs:49:8: error: [GHC-25897]
- • Couldn't match type ‘n’ with ‘Int’
+ • Couldn't match type ‘m’ with ‘Int’
Expected: Exp (((sh :. k) :. m) :. n)
-> Exp (((sh :. m) :. n) :. k)
Actual: Exp
(Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
-> Exp
(Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))
- ‘n’ is a rigid type variable bound by
+ ‘m’ is a rigid type variable bound by
the type signature for:
test :: forall sh k m n.
Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
=====================================
testsuite/tests/typecheck/should_fail/T12785b.stderr
=====================================
@@ -1,6 +1,5 @@
-
T12785b.hs:30:65: error: [GHC-25897]
- • Could not deduce ‘s ~ Payload (S n) (Payload n s1)’
+ • Could not deduce ‘Payload (S n) (Payload n s1) ~ s’
arising from a use of ‘SBranchX’
from the context: m ~ S n
bound by a pattern with constructor:
@@ -25,3 +24,4 @@ T12785b.hs:30:65: error: [GHC-25897]
a :: STree (S m) f s (bound at T12785b.hs:30:12)
nest :: HTree m (Hidden (S m) f) -> Hidden m (STree (S m) f)
(bound at T12785b.hs:28:1)
+
=====================================
testsuite/tests/typecheck/should_fail/T27844.hs
=====================================
@@ -0,0 +1,14 @@
+-- Repro.hs
+-- The call to f forces c ~ (b, F c) inside the scope of the skolem b.
+-- Correct behaviour: a type error at the first argument of const
+-- (as GHC 9.12.4 reports).
+
+{-# LANGUAGE RankNTypes, TypeFamilies #-}
+module T27844 where
+
+type family F a
+
+f :: (forall b. b -> (b, F c)) -> c -> ()
+f _ _ = ()
+
+g x = f (\_ -> const x (show x)) x
=====================================
testsuite/tests/typecheck/should_fail/T27844.stderr
=====================================
@@ -0,0 +1,12 @@
+T27844.hs:14:22: error: [GHC-25897]
+ • Couldn't match expected type ‘(b, F c)’ with actual type ‘c’
+ ‘c’ is a rigid type variable bound by
+ the inferred type of g :: Show c => c -> ()
+ at T27844.hs:14:1-34
+ • In the first argument of ‘const’, namely ‘x’
+ In the expression: const x (show x)
+ In the first argument of ‘f’, namely ‘(\ _ -> const x (show x))’
+ • Relevant bindings include
+ x :: c (bound at T27844.hs:14:3)
+ g :: c -> () (bound at T27844.hs:14:1)
+
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -766,3 +766,5 @@ test('T26862', normal, compile_fail, [''])
test('T27210', normal, compile_fail, [''])
test('T26532', normal, compile_fail, [''])
test('T27731', normal, compile_fail, [''])
+test('T27844', normal, compile_fail, [''])
+
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/836ec50a2bda086d73657ea291fdd5…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/836ec50a2bda086d73657ea291fdd5…
You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help
1
0
[Git][ghc/ghc][master] hpc: Improve coverage semantics for instance methods and instances
by Marge Bot (＠marge-bot) 13 Oct '26
by Marge Bot (＠marge-bot) 13 Oct '26
13 Oct '26
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
9b5beaa2 by Florian Ragwitz at 2026-10-13T18:12:05-04:00
hpc: Improve coverage semantics for instance methods and instances
Users care about which of their explicitly 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 therefore skip generating top-level boxes for inherited methods which will
appear as uncovered with no clear indication as to why, and no way to fix other
than exercising code the user has not written.
Previously, top-level boxes for those inherited methods would use the instance
head as their source span. Now that those boxes are gone, we can use that
source span for another purpose:
We introduce a new top-level box for each class instance with its instance head
as the source span, and use that to indicate whether or not an instance has
been covered at all.
We do this by making any method of the instance, inherited/generated or
otherwise, tick the box for the instance head. Excluded from this are
methodless classes, which could never be covered using the current mechanism.
This could be improved upon further.
These changes apply to ticking for program coverage only, and don't affect
source notes. Additionally, we update the scope of record selector ticking to
be limited to program coverage as well, as the oversight to also extend it to
source notes has previously caused bugs and because record selector ticking is
coverage-specific.
Fixes #17155, #15932.
- - - - -
12 changed files:
- + changelog.d/hpc-classinsts
- compiler/GHC/Core/Opt/Specialise.hs
- compiler/GHC/CoreToIface.hs
- compiler/GHC/HsToCore.hs
- compiler/GHC/HsToCore/Ticks.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Types/Id/Info.hs
- + testsuite/tests/hpc/instmeths/instmeths.hs
- + testsuite/tests/hpc/instmeths/instmeths.stdout
- + testsuite/tests/hpc/instmeths/test.T
- testsuite/tests/simplCore/should_compile/T22375.stderr
- testsuite/tests/simplCore/should_compile/T22375DataFamily.stderr
Changes:
=====================================
changelog.d/hpc-classinsts
=====================================
@@ -0,0 +1,23 @@
+section: compiler
+synopsis: Improve coverage reporting for class instances and their methods
+description:
+
+ Coverage reporting (:ghc-flag:`-fhpc`) now treats class instances more
+ naturally.
+
+ Compiler-generated instance methods, such as inherited default methods, no
+ longer receive separate top-level coverage boxes. Explicitly implemented
+ instance methods retain their own declaration coverage.
+
+ This means that it is no longer necessary to exercise all of a class' methods
+ in order for it to appear "covered".
+
+ Additionally, top-level coverage boxes are now created for all instances of
+ classes with methods, and ticked by the use of *any* of the class' methods.
+ This indicates that an instance was in fact used at run-time.
+
+ Note that classes without any instance methods are currently excluded from
+ this, and won't have any coverage boxes created.
+
+mrs: !16632
+issues: #17155 #15932
=====================================
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
=====================================
@@ -466,6 +466,7 @@ toIfaceTopBndr id
toIfaceIdDetails :: Name -- ^ for trace/panic messages only
-> 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
=====================================
@@ -170,7 +170,8 @@ deSugar hsc_env
(hsc_logger hsc_env)
(initTicksConfig (hsc_dflags hsc_env))
mod mod_loc
- export_set (typeEnvTyCons type_env) binds
+ export_set (typeEnvTyCons type_env)
+ insts binds
else return (binds, Nothing)
; let modBreaks
| Just (_, _, breakpointSpecs) <- m_tickInfo
=====================================
compiler/GHC/HsToCore/Ticks.hs
=====================================
@@ -1,11 +1,11 @@
-{-# LANGUAGE NondecreasingIndentation, DataKinds #-}
+{-# LANGUAGE NondecreasingIndentation, DataKinds, ViewPatterns #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
{-
(c) Galois, 2006
(c) University of Glasgow, 2007
-(c) Florian Ragwitz, 2025
+(c) Florian Ragwitz, 2025-2026
-}
module GHC.HsToCore.Ticks
@@ -24,6 +24,8 @@ import GHC.Unit
import GHC.Core.Type
import GHC.Core.TyCon
+import GHC.Core.InstEnv
+import GHC.Core.Class
import GHC.Data.Maybe
import GHC.Data.FastString
@@ -43,6 +45,7 @@ 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
@@ -56,6 +59,7 @@ import Data.Foldable (toList)
import Trace.Hpc.Mix
import Data.Bifunctor (second)
+import Data.Functor
import Data.List.NonEmpty (NonEmpty (..))
import Data.Set (Set)
import qualified Data.Set as Set
@@ -100,11 +104,12 @@ addTicksToBinds
-- isExportedId doesn't work yet (the desugarer
-- hasn't set it), so we have to work from this set.
-> [TyCon] -- ^ Type constructors in this module
+ -> [ClsInst] -- ^ Class instances in this module
-> LHsBinds GhcTc
-> IO (LHsBinds GhcTc, Maybe (FilePath, SizedSeq Tick, SizedSeq Tick))
addTicksToBinds logger cfg
- mod mod_loc exports tyCons 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
@@ -129,8 +134,13 @@ addTicksToBinds logger cfg
, this_mod = mod
, tickishType = tickish
, recSelBinds = emptyVarEnv
+ , instMeths = emptyVarEnv
+ , instTicks = emptyNameEnv
}
- (binds',_,st') = unTM (addTickLHsBinds binds) env st
+ addTick = do
+ instTicks <- allocInstTicks insts
+ withEnv (\e -> e{ instTicks }) $ addTickLHsBinds binds
+ (binds',_,st') = unTM addTick env st
in (binds', st')
(binds1,st) = foldr tickPass (binds, initTTState) passes
@@ -231,7 +241,7 @@ addTickLHsBind :: LHsBind GhcTc -> TM (LHsBind GhcTc)
addTickLHsBind (L pos (XHsBindsLR bind@(AbsBinds { abs_binds = binds
, abs_exports = abs_exports
}))) =
- withEnv (add_rec_sels . add_inlines . add_exports) $ do
+ withEnv (add_inst_meths . add_rec_sels . add_inlines . add_exports) $ do
binds' <- addTickLHsBinds binds
return $ L pos $ XHsBindsLR $ bind { abs_binds = binds' }
where
@@ -259,19 +269,26 @@ addTickLHsBind (L pos (XHsBindsLR bind@(AbsBinds { abs_binds = binds
| ABE{ abe_poly, abe_mono } <- abs_exports
, RecSelId{} <- [idDetails abe_poly] ] }
+ add_inst_meths env =
+ env{ instMeths = instMeths env `extendVarEnvList`
+ [ (abe_mono, dfun)
+ | ABE{ abe_poly, abe_mono } <- abs_exports
+ , 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
decl_path <- getPathEntry
density <- getDensity
+ env <- getEnv
- inline_ids <- liftM inlines getEnv
-- See Note [inline sccs]
let inline = isInlinePragma (idInlinePragma id)
- || id `elemVarSet` inline_ids
+ || id `elemVarSet` inlines env
-- See Note [inline sccs]
- tickish <- tickishType `liftM` getEnv
- case tickish of { ProfNotes | inline -> return (L pos funBind); _ -> do
+ case tickishType env of { ProfNotes | inline -> return (L pos funBind); _ -> do
-- See Note [Record-selector ticks]
selTicks <- recSelTick id
@@ -294,16 +311,28 @@ addTickLHsBind (L pos (funBind@(FunBind { fun_id = L _ id, fun_matches = matches
toplev = null decl_path
exported = idName id `elemNameSet` exported_names
- tick <- if not blackListed &&
- shouldTickBind density toplev exported simple inline
+ -- See Note [Instance Method Coverage].
+ -- We only exclude generated instance methods for now, not generated code in
+ -- general, whose coverage semantics may need to be considered separately.
+ let generatedInstMeth = tickishType env == HpcTicks
+ && id `elemVarEnv` instMeths env
+ && isGenerated (mg_origin (mg_ext matches))
+
+ tick <- if not generatedInstMeth
+ && not blackListed
+ && shouldTickBind density toplev exported simple inline
then
bindTick density name (locA pos) fvs
else
return Nothing
+ -- See Note [Instance Method Coverage].
+ instTick <- instMethTick id
+
let mbCons = maybe Prelude.id (:)
return $ L pos $ funBind { fun_matches = mg
- , fun_ext = second (tick `mbCons`) (fun_ext funBind) }
+ , fun_ext = second ((instTick `mbCons`) . (tick `mbCons`))
+ (fun_ext funBind) }
} }
where
-- See Note [Record-selector ticks]
@@ -338,6 +367,30 @@ addTickLHsBind (L pos (funBind@(FunBind { fun_id = L _ id, fun_matches = matches
-- This scheme could be extended further in the future, making coverage for
-- positional constructor fields mean that the field was accessed at run-time.
+-- Note [Instance Method Coverage]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- Users expect source-level semantics for coverage reports (see #17155,
+-- #15932). That is, code they've written themselves should be marked as covered
+-- iff it is evaluated at run-time. Given that the implementation of class
+-- instances creates top-level bindings for all methods of an instance,
+-- 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.
+--
+-- 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
+-- tick box at the instance head and tick that box when any method of that
+-- instance is evaluated.
+--
+-- As marker/tag-like class instances without any methods would always appear
+-- as uncovered using the above mechanism, we exclude them when creating
+-- instance tick boxes. This could potentially be improved in the future by
+-- tracking if any functions requiring an instance of an empty class have been
+-- evaluated.
+
-- TODO: Revisit this
addTickLHsBind (L pos (pat@(PatBind { pat_lhs = lhs
, pat_rhs = rhs
@@ -1098,6 +1151,8 @@ data TickTransEnv = TTE { fileName :: FastString
, this_mod :: Module
, tickishType :: TickishType
, recSelBinds :: IdEnv DVarSet
+ , instMeths :: IdEnv Name
+ , instTicks :: NameEnv CoreTickish
}
-- deriving Show
@@ -1182,6 +1237,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')
@@ -1238,6 +1296,20 @@ isBlackListed (RealSrcSpan pos _) = TM $ \ env st -> (Set.member pos (blackList
isBlackListed GeneratedSrcSpan{} = return False
isBlackListed UnhelpfulSpan{} = return False
+-- See Note [Instance Method Coverage].
+allocInstTicks :: [ClsInst] -> TM (NameEnv CoreTickish)
+allocInstTicks insts =
+ 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 [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 >>= lookupNameEnv (instTicks e)
+
-- the tick application inherits the source position of its
-- expression argument to support nested box allocations
allocTickBox :: BoxLabel -> Bool -> Bool -> SrcSpan -> TM (HsExpr GhcTc)
@@ -1256,7 +1328,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
=====================================
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
@@ -1859,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
@@ -1879,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
@@ -1896,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 }
@@ -1904,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
@@ -2030,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
@@ -2044,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)
@@ -2162,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/Types/Id/Info.hs
=====================================
@@ -222,6 +222,10 @@ 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
+ -- ^ An instance method.
+ Name
+ -- ^ 'Name' of the dictionary function the instance method belongs to.
data RecSelInfo
= RSI { rsi_def :: [ConLike] -- Record selector defined for these
@@ -449,6 +453,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.hs
=====================================
@@ -0,0 +1,57 @@
+import Data.List
+import Data.Maybe
+import Trace.Hpc.Mix
+import Trace.Hpc.Reflect
+import Trace.Hpc.Tix
+import Trace.Hpc.Util
+
+class Foo a where
+ defMeth, defMeth', reqMeth :: a -> String
+ defMeth = const "class default"
+ defMeth' = const "class default"
+
+newtype T a = T a deriving (Show, Eq, Functor)
+instance Foo (T a) where
+ reqMeth = const "Foo (T a) instance"
+
+newtype T' a = T' a
+
+instance Foo (T' a) where
+ reqMeth = const "Foo (T' a) instance"
+ defMeth = const "Foo (T' a) instance"
+
+-- no method use could "cover" this instance, so we (for now) omit the top-level box for it
+class Marker a
+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 = ("$f" `isPrefixOf`)
+ isMeth = (||) <$> (`elem` ["(==)", "(/=)", "show", "showList", "showsPrec", "fmap", "(<$)"])
+ <*> ("Meth" `isInfixOf`)
+interesting _ = Nothing
+
+-- candidate for HPC.Utils, maybe?
+sourceAt :: String -> HpcPos -> String
+sourceAt src pos
+ | l1 == l2 = take (c2 - c1 + 1) . drop (c1 - 1) $ ls !! (l1 - 1)
+ | otherwise = intercalate "\n" $ first : (middle ++ [last])
+ where
+ (l1, c1, l2, c2) = fromHpcPos pos
+ ls = lines src
+ first = drop (c1 - 1) $ ls !! (l1 - 1)
+ middle = take (l2 - l1 - 1) $ drop l1 ls
+ last = take c2 $ ls !! (l2 - 1)
+
+main :: IO ()
+main = do
+ print (T 23 == (succ <$> T 22)) -- tick Eq and Functor by using any of their methods
+ print (reqMeth (T' 1)) -- tick `Foo (T' a)` and that instance's `reqMeth`
+
+ Mix source _ _ _ mixEntries <- readMix [".hpc"] (Left "Main")
+ src <- readFileUtf8 source
+ let boxes = mapMaybe interesting $ zip [0 ..] mixEntries
+ Tix [TixModule "Main" _ _ counts] <- examineTix
+ mapM_ print [ (counts !! n, path, sourceAt src pos)
+ | (n, pos, path) <- sortOn (\(_, l, p) -> (p, l)) boxes ]
=====================================
testsuite/tests/hpc/instmeths/instmeths.stdout
=====================================
@@ -0,0 +1,12 @@
+True
+"Foo (T' a) instance"
+(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\"")
+(0,"reqMeth","reqMeth = const \"Foo (T a) instance\"")
+(1,"reqMeth","reqMeth = const \"Foo (T' a) instance\"")
=====================================
testsuite/tests/hpc/instmeths/test.T
=====================================
@@ -0,0 +1,3 @@
+setTestOpts([omit_ghci, when(fast(), skip), js_skip])
+
+test('instmeths', normal, compile_and_run, ['-fhpc'])
=====================================
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/-/commit/9b5beaa243ae72a389e2876e818a505…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9b5beaa243ae72a389e2876e818a505…
You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help
1
0
[Git][ghc/ghc][master] testsuite: Line-buffer the driver's stdout
by Marge Bot (＠marge-bot) 13 Oct '26
by Marge Bot (＠marge-bot) 13 Oct '26
13 Oct '26
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
c0299e15 by Simon Jakobi at 2026-10-13T18:11:23-04:00
testsuite: Line-buffer the driver's stdout
Python block-buffers stdout when it is a pipe. This is the case for
example in CI. As a result there is often no indication of progress at
all until the run ends.
To fix this, we configure it explicitly to use line buffering instead.
stderr is reconfigured too, for consistency: Python line-buffers it by
default since 3.9.
The type-ignores are for mypy, which types these handles as TextIO — an
interface without reconfigure.
Fixes #12934.
Assisted-by: Claude Fable 5
- - - - -
1 changed file:
- testsuite/driver/runtests.py
Changes:
=====================================
testsuite/driver/runtests.py
=====================================
@@ -38,6 +38,12 @@ import term_color
from term_color import Color, colored
import cpu_features
+# Line-buffer stdout: when it is a pipe (as in CI), the block-buffered
+# default delays test and progress output (#12934). stderr is included
+# for consistency, although Python line-buffers it by default since 3.9.
+sys.stdout.reconfigure(line_buffering=True) # type: ignore[union-attr]
+sys.stderr.reconfigure(line_buffering=True) # type: ignore[union-attr]
+
# Readline sometimes spews out ANSI escapes for some values of TERM,
# which result in test failures. Thus set TERM to a nice, simple, safe
# value.
@@ -352,8 +358,6 @@ try:
except Exception as e:
print('Failed to detect CPU features: ', e)
-sys.stdout.flush()
-
if config.local:
tempdir = ''
else:
@@ -518,9 +522,6 @@ else:
except KeyboardInterrupt:
pass
- # flush everything before we continue
- sys.stdout.flush()
-
# Dump metrics data.
print("\nPerformance Metrics (test environment: {}):\n".format(config.test_env))
if config.baseline_commit:
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c0299e158109bee16924e257ef28a99…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c0299e158109bee16924e257ef28a99…
You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help
1
0
[Git][ghc/ghc][master] 3 commits: Remove the Eq and Ord instances for ForAllTyFlag
by Marge Bot (＠marge-bot) 13 Oct '26
by Marge Bot (＠marge-bot) 13 Oct '26
13 Oct '26
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
d07a5176 by Simon Peyton Jones at 2026-10-13T18:10:39-04:00
Remove the Eq and Ord instances for ForAllTyFlag
In Note [Comparing visibility] in GHC.Core.TyCo.Compare we read that
"we always compare ForAllTyFlags with `eqForAllVis` or `cmpForAllVis`"
But alas there was an Eq and Ord instance for ForAllTyFlag, which made it
impossible to check this claim. So I made these changes:
* Move the definition of ForAllTyFlag and its related functions from
L.H.S.Specificity (where it did not belong, since L.H.S didn't use it)
into GHC.Types.Var.
* Remove the Eq and Ord instances for ForAllTyFlag
* Deal with the fallout, by using `eqForAllVis` or related functions.
* In interface files we use IfaceType as a key for a de-deduplication map
See Note [Deduplication during iface binary serialisation]
in GHC.Iface.Binary. For this we need /exact/ comparison, so we use a
newtype wrapper for IfaceForAllTyFlag, and give use `cmpForAllTyFlagExactly`
to implement its Ord instance. Tiresome but easy.
* Rename `toIfaceForAllBndrs` to `toIfaceForAllTyBndrs`
- - - - -
ea5c054d by Simon Peyton Jones at 2026-10-13T18:10:39-04:00
Refactor type and coercion substitution
This MR refactors type and coercion substitution so that they use
TyCoMapper, rather than hand-rolled code. Fundamentally it's a simple
idea, but I had to do quite a bit of refactoring to make it fly.
I got Claude to help me this this refactoring, but I paid careful
attention to every line of code.
Main changes:
* New module GHC.Core.TyCo.Make which defines TyCoMapper, and a bunch of other
simple "smart constructors" for types and coercions. See
GHC.Core.TyCo.Rep Note [The Type-related module hierarchy], esp (TRM1)
* The new TyCoMapper has new fields `tcm_tcapp_ty` and `tcm_tcapp_co` to handle
type-constructor applications. These replace `tcm_tycon`.
* Rewrite GHC.Core.TyCo.Subst to use TyCoMapper
* Rewrite GHC.Core.Type.expandTypeSynonyms to use TyCoMapper.
* Implement `seqType` and `seqCo` with TyCoFolder. To to this I had to add
a `tcf_lit` field to TyCoFolder.
* A new module GHC.Utils.StrictIdentity to define a strict identity monad,
which itself is used for
substTyCoMapper :: TyCoMapper Subst StrictIdentity
* I removed an apparently-unused instance for Binary Levity
Refactoring `seq` functions
* In GHC.Core.Seq, redefine `seqOneShot`, `seqRuleInfo`, and friends to return
`SeqResult`, a new type defined in GHC.Types.Baseic, rather than `()`. We
can define a Monoid instance for `SeqResult` that does the right thing.
* This has knock-on effects across the compiler.
- - - - -
34165e23 by Simon Peyton Jones at 2026-10-13T18:10:39-04:00
Refactor TyCoMapper to take a single monad; add StrictReaderT
TyCoMapper used to be parameterised over both an environment and a
monad, with fields like
tcm_tyvar :: env -> TyVar -> m Type
Now it is parameterised over just the monad:
tcm_tyvar :: TyVar -> m Type
If the mapping needs an environment, `m` is a reader monad over that
environment. Many uses (e.g. zonkTcTypeMapper, swizzleMapper) need no
environment at all, and used to pass a dummy (). The binder field
becomes
tcm_tycobinder :: forall r. TyCoVar -> ForAllTyFlag
-> (TyCoVar -> m r) -> m r
and runs the continuation in the extended environment. mapTyCoX is gone;
only mapTyCo remains.
To make this efficient, the reader monad must use the one-shot trick and
be strict in the environment. So:
* New module GHC.Utils.Monad.StrictReader defines
newtype StrictReaderT r m a
with hand-written instances. The builder of the pattern synonym
`StrictReaderT` is a smart constructor that adds both `oneShot` and a
bang on the environment, so every StrictReaderT computation is strict
in the environment. See Note [Instances for StrictReaderT].
* ZonkT becomes type ZonkT = StrictReaderT ZonkEnv
ZonkM becomes type ZonkM = StrictReaderT ZonkGblEnv IO
replacing their own hand-written instances.
* Substitution uses
type SubstM = StrictReaderT Subst StrictIdentity
substTyCoMapper :: TyCoMapper SubstM
and similarly expandTypeSynonymMapper.
* zonk_tycomapper :: TyCoMapper (ZonkT TcM) is now much simpler.
* swizzleMapper uses StrictIdentity rather than Identity.
* Module renaming, so that the strict monads are all peers in GHC.Utils.Monad:
GHC.Utils.StrictIdentity ==> GHC.Utils.Monad.StrictIdentity
GHC.Utils.Monad.State.Strict ==> GHC.Utils.Monad.StrictState
alongside the new GHC.Utils.Monad.StrictReader.
Co-Authored-By: Claude Opus 5.5 <noreply(a)anthropic.com>
- - - - -
87 changed files:
- compiler/GHC/Builtin/WiredIn/Prim.hs
- compiler/GHC/Cmm/GenericOpt.hs
- compiler/GHC/Cmm/UniqueRenamer.hs
- compiler/GHC/CmmToAsm/Dwarf/Types.hs
- compiler/GHC/CmmToAsm/Monad.hs
- compiler/GHC/CmmToAsm/Reg/Graph/Spill.hs
- compiler/GHC/CmmToAsm/Reg/Graph/SpillClean.hs
- compiler/GHC/CmmToAsm/Reg/Graph/SpillCost.hs
- compiler/GHC/CmmToAsm/Reg/Graph/Stats.hs
- compiler/GHC/CmmToAsm/Reg/Linear/State.hs
- compiler/GHC/CmmToAsm/Reg/Linear/Stats.hs
- compiler/GHC/CmmToAsm/Reg/Liveness.hs
- compiler/GHC/CmmToAsm/Wasm/Asm.hs
- compiler/GHC/CmmToAsm/Wasm/Types.hs
- compiler/GHC/CmmToC.hs
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion.hs-boot
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Map/Type.hs
- compiler/GHC/Core/Opt/Arity.hs
- compiler/GHC/Core/Opt/CallerCC.hs
- compiler/GHC/Core/Opt/Exitify.hs
- compiler/GHC/Core/Reduction.hs
- compiler/GHC/Core/Seq.hs
- compiler/GHC/Core/TyCo/Compare.hs
- compiler/GHC/Core/TyCo/FVs.hs
- + compiler/GHC/Core/TyCo/Make.hs
- + compiler/GHC/Core/TyCo/Make.hs-boot
- compiler/GHC/Core/TyCo/Ppr.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCo/Rep.hs-boot
- compiler/GHC/Core/TyCo/Subst.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Type.hs-boot
- compiler/GHC/Core/Unify.hs
- compiler/GHC/CoreToIface.hs
- compiler/GHC/CoreToIface.hs-boot
- compiler/GHC/Driver/Downsweep.hs
- compiler/GHC/Driver/Main/Compile.hs
- compiler/GHC/Iface/Decl.hs
- compiler/GHC/Iface/Ext/Types.hs
- compiler/GHC/Iface/Ext/Utils.hs
- compiler/GHC/Iface/Syntax.hs
- compiler/GHC/Iface/Type.hs
- compiler/GHC/Iface/Type.hs-boot
- compiler/GHC/IfaceToCore.hs
- compiler/GHC/Stg/BcPrep.hs
- compiler/GHC/Stg/Debug.hs
- compiler/GHC/Stg/EnforceEpt/Rewrite.hs
- compiler/GHC/Stg/EnforceEpt/TagSig.hs
- compiler/GHC/Stg/Subst.hs
- compiler/GHC/Tc/Deriv/Functor.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Tc/Zonk/Env.hs
- compiler/GHC/Tc/Zonk/Monad.hs
- compiler/GHC/Tc/Zonk/TcType.hs
- compiler/GHC/Tc/Zonk/Type.hs
- compiler/GHC/Types/Arity.hs
- compiler/GHC/Types/Basic.hs
- compiler/GHC/Types/Cpr.hs
- compiler/GHC/Types/Demand.hs
- compiler/GHC/Types/Name/Env.hs
- compiler/GHC/Types/Name/Occurrence.hs
- compiler/GHC/Types/Unique/DSM.hs
- compiler/GHC/Types/Unique/FM.hs
- compiler/GHC/Types/Unique/Map.hs
- compiler/GHC/Types/Unique/Set.hs
- compiler/GHC/Types/Unique/Supply.hs
- compiler/GHC/Types/Var.hs
- compiler/GHC/Types/Var.hs-boot
- compiler/GHC/Types/Var/Set.hs
- compiler/GHC/Utils/Binary.hs
- + compiler/GHC/Utils/Monad/StrictIdentity.hs
- + compiler/GHC/Utils/Monad/StrictReader.hs
- compiler/GHC/Utils/Monad/State/Strict.hs → compiler/GHC/Utils/Monad/StrictState.hs
- compiler/GHC/Utils/Outputable.hs
- compiler/Language/Haskell/Syntax/Specificity.hs
- compiler/ghc.cabal.in
- testsuite/tests/count-deps/CountDepsParser.stdout
- utils/check-exact/Utils.hs
- utils/haddock/haddock-api/src/Haddock/Backends/Hyperlinker/Utils.hs
The diff was not included because it is too large.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f217fc315b7fc67a7a96bafc08f303…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f217fc315b7fc67a7a96bafc08f303…
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/sjakobi/deprecated-flags-2016] 2 commits: Make T2464 actually test #ifdef'd pragmas
by Simon Jakobi (＠sjakobi) 13 Oct '26
by Simon Jakobi (＠sjakobi) 13 Oct '26
13 Oct '26
Simon Jakobi pushed to branch wip/sjakobi/deprecated-flags-2016 at Glasgow Haskell Compiler / GHC
Commits:
62b509fe by Simon Jakobi at 2026-10-13T21:43:20+02:00
Make T2464 actually test #ifdef'd pragmas
The test guarded a LANGUAGE EmptyDataDecls pragma behind #if, but
EmptyDataDecls is on by default since Haskell2010, so the module
compiled even when the guarded pragma was ignored. Guard MagicHash
instead, which is unlikely to be included in a future default language.
The test also checks that warnings from file-header pragmas are emitted
only once, even though the pragmas are parsed both before and after
CPP, using the -fffi deprecation warning as the canary. Use an
unrecognised warning flag instead, so the test no longer depends on a
deprecated flag that is about to be removed.
Context: #27939
Assisted-by: Claude Fable 5.1
- - - - -
15f211c9 by Simon Jakobi at 2026-10-13T22:00:15+02:00
Remove command-line flags deprecated in GHC 8.2 or earlier
Also remove the INCLUDE file-header pragma, which only expanded to
the now-removed -#include.
Closes #27939.
Assisted-by: Claude Fable 5.1
- - - - -
29 changed files:
- + changelog.d/remove-long-deprecated-flags.md
- compiler/GHC/CmmToC.hs
- compiler/GHC/CoreToStg.hs
- compiler/GHC/Driver/Flags.hs
- compiler/GHC/Driver/Session.hs
- compiler/GHC/Parser/Errors/Ppr.hs
- compiler/GHC/Parser/Errors/Types.hs
- compiler/GHC/Parser/Header.hs
- compiler/GHC/Parser/Lexer.x
- compiler/GHC/Stg/Make.hs
- compiler/GHC/Types/Tickish.hs
- docs/users_guide/codegens.rst
- docs/users_guide/expected-undocumented-flags.txt
- docs/users_guide/exts/control.rst
- docs/users_guide/exts/ffi.rst
- docs/users_guide/exts/pragmas.rst
- docs/users_guide/ghc.rst
- docs/users_guide/profiling.rst
- − docs/users_guide/what_glasgow_exts_does.rst
- testsuite/tests/driver/Makefile
- testsuite/tests/driver/T2464.hs
- testsuite/tests/driver/T2464.stderr
- testsuite/tests/ffi/should_run/T2594.hs
- testsuite/tests/ffi/should_run/ffi015.hs
- testsuite/tests/ffi/should_run/fptr01.hs
- testsuite/tests/ffi/should_run/fptrfail01.hs
- testsuite/tests/indexed-types/should_compile/all.T
- testsuite/tests/indexed-types/should_fail/SkolemOccursLoop.hs
- utils/haddock/haddock-api/src/Haddock/Backends/Hyperlinker/Parser.hs
Changes:
=====================================
changelog.d/remove-long-deprecated-flags.md
=====================================
@@ -0,0 +1,15 @@
+section: compiler
+synopsis: Remove command-line flags deprecated in GHC 8.2 or earlier
+issues: #27939
+mrs: !16801
+description: {
+ The following flags, deprecated in GHC 8.2 or earlier, are no longer
+ accepted: ``-n``, ``-Onot``, ``-recomp``, ``-syslib``, ``-package-conf``,
+ ``-no-user-package-conf``, ``-auto``, ``-auto-all``, ``-caf-all``,
+ ``-fglasgow-exts``, ``-frewrite-rules``, ``-fvia-C``, ``-fcontext-stack``,
+ ``-ftype-function-depth``, ``-#include``, the pre-``-X`` extension
+ spellings such as ``-fth`` and ``-fffi``, and their negations.
+
+ The ``INCLUDE`` file-header pragma, which only expanded to ``-#include``,
+ is no longer recognised either.
+}
=====================================
compiler/GHC/CmmToC.hs
=====================================
@@ -8,8 +8,6 @@
--
-- (c) The University of Glasgow 2004-2006
--
--- Print Cmm as real C, for -fvia-C
---
-- See wiki:commentary/compiler/backends/ppr-c
--
-- This is simpler than the old PprAbsC, because Cmm is "macro-expanded"
=====================================
compiler/GHC/CoreToStg.hs
=====================================
@@ -190,12 +190,12 @@ We now initialize these correctly. The initialization works like this:
- For top-level bindings, check if the binding is a CAF
- - CAF: If -fcaf-all is enabled, create a new CAF just for this CAF
+ - CAF: If -fprof-cafs is enabled, create a new CAF just for this CAF
and use it. Note that these new cost centres need to be
collected to be able to generate cost centre initialization
code, so `coreToTopStgRhs` now returns `CollectedCCs`.
- If -fcaf-all is not enabled, use "all CAFs" cost centre.
+ If -fprof-cafs is not enabled, use "all CAFs" cost centre.
- Non-CAF: Top-level (static) data is not counted in heap profiles; nor
do we set CCCS from it; so we just slam in
=====================================
compiler/GHC/Driver/Flags.hs
=====================================
@@ -35,7 +35,6 @@ module GHC.Driver.Flags
, validHoleFitsImpliedGFlags
, impliedGFlags
, impliedOffGFlags
- , glasgowExtsFlags
, ExtensionDeprecation(..)
, Deprecation(..)
@@ -403,41 +402,6 @@ impliedGFlags = [(Opt_DeferTypeErrors, turnOn, Opt_DeferTypedHoles)
impliedOffGFlags :: [(GeneralFlag, TurnOnFlag, GeneralFlag)]
impliedOffGFlags = [(Opt_Strictness, turnOff, Opt_WorkerWrapper)]
--- Please keep @docs/users_guide/what_glasgow_exts_does.rst@ up to date with this list.
-glasgowExtsFlags :: [LangExt.Extension]
-glasgowExtsFlags = [
- LangExt.ConstrainedClassMethods
- , LangExt.DeriveDataTypeable
- , LangExt.DeriveFoldable
- , LangExt.DeriveFunctor
- , LangExt.DeriveGeneric
- , LangExt.DeriveTraversable
- , LangExt.EmptyDataDecls
- , LangExt.ExistentialQuantification
- , LangExt.ExplicitNamespaces
- , LangExt.FlexibleContexts
- , LangExt.FlexibleInstances
- , LangExt.ForeignFunctionInterface
- , LangExt.FunctionalDependencies
- , LangExt.GeneralizedNewtypeDeriving
- , LangExt.ImplicitParams
- , LangExt.KindSignatures
- , LangExt.LiberalTypeSynonyms
- , LangExt.MagicHash
- , LangExt.MultiParamTypeClasses
- , LangExt.ParallelListComp
- , LangExt.PatternGuards
- , LangExt.PostfixOperators
- , LangExt.RankNTypes
- , LangExt.RecursiveDo
- , LangExt.ScopedTypeVariables
- , LangExt.StandaloneDeriving
- , LangExt.TypeOperators
- , LangExt.TypeSynonymInstances
- , LangExt.UnboxedTuples
- , LangExt.UnicodeSyntax
- , LangExt.UnliftedFFITypes ]
-
-- | Debugging flags
data DumpFlag
-- See Note [Updating flag description in the User's Guide] in GHC.Driver.Session
=====================================
compiler/GHC/Driver/Session.hs
=====================================
@@ -21,7 +21,6 @@ module GHC.Driver.Session (
Language(..),
FatalMessager, FlushOut(..),
ProfAuto(..),
- glasgowExtsFlags,
hasPprDebug, hasNoDebugOutput, hasNoStateHack, hasNoOptCoercion,
dopt, dopt_set, dopt_unset,
gopt, gopt_set, gopt_unset, setGeneralFlag', unSetGeneralFlag',
@@ -55,7 +54,7 @@ module GHC.Driver.Session (
PackageDBFlag(..), PkgDbRef(..),
Option(..), showOpt,
DynLibLoader(..),
- fFlags, fLangFlags, xFlags,
+ fFlags, xFlags,
wWarningFlags,
makeDynFlagsConsistent,
positionIndependent,
@@ -1084,14 +1083,8 @@ add_dep_message (AnySuffix f) message =
-- See Note [Supporting CLI completion]
dynamic_flags_deps :: [(Deprecation, Flag (CmdLineP DynFlags))]
dynamic_flags_deps = [
- make_dep_flag defFlag "n" (NoArg $ return ())
- "The -n flag is deprecated and no longer has any effect"
- , make_ord_flag defFlag "cpp" (NoArg (setExtensionFlag LangExt.Cpp))
+ make_ord_flag defFlag "cpp" (NoArg (setExtensionFlag LangExt.Cpp))
, make_ord_flag defFlag "F" (NoArg (setGeneralFlag Opt_Pp))
- , (Deprecated, defFlag "#include"
- (HasArg (\_s ->
- deprecate ("-#include and INCLUDE pragmas are " ++
- "deprecated: They no longer have any effect"))))
, make_ord_flag defFlag "v" (OptIntSuffix setVerbosity)
, make_ord_flag defGhcFlag "j" (OptIntSuffix
@@ -1408,13 +1401,6 @@ dynamic_flags_deps = [
(NoArg (setGeneralFlag Opt_Ticky_Dyn_Thunk))
, make_ord_flag defGhcFlag "ticky-tag-checks"
(NoArg (setGeneralFlag Opt_Ticky_Tag))
-
- ------- recompilation checker --------------------------------------
- , make_dep_flag defGhcFlag "recomp"
- (NoArg $ unSetGeneralFlag Opt_ForceRecomp)
- "Use -fno-force-recomp instead"
- , make_dep_flag defGhcFlag "no-recomp"
- (NoArg $ setGeneralFlag Opt_ForceRecomp) "Use -fforce-recomp instead"
, make_ord_flag defFlag "fmax-errors"
(intSuffix (\n d -> d { maxErrors = Just (max 1 n) }))
, make_ord_flag defFlag "fno-max-errors"
@@ -1772,8 +1758,6 @@ dynamic_flags_deps = [
, make_ord_flag defGhcFlag "fplugin-library" (hasArg addExternalPlugin)
------ Optimisation flags ------------------------------------------
- , make_dep_flag defGhcFlag "Onot" (noArgM $ setOptLevel 0 )
- "Use -O0 instead"
, make_ord_flag defGhcFlag "O" (optIntSuffixM (\mb_n ->
setOptLevel (mb_n `orElse` 1)))
-- If the number is missing, use 1
@@ -1850,14 +1834,6 @@ dynamic_flags_deps = [
(intSuffix (\n d -> d { wantedsFuel = n }))
, make_ord_flag defFlag "fqcs-expansion-fuel"
(intSuffix (\n d -> d { qcsFuel = n }))
- , (Deprecated, defFlag "fcontext-stack"
- (intSuffixM (\n d ->
- do { deprecate $ "use -freduction-depth=" ++ show n ++ " instead"
- ; return $ d { reductionDepth = treatZeroAsInf n } })))
- , (Deprecated, defFlag "ftype-function-depth"
- (intSuffixM (\n d ->
- do { deprecate $ "use -freduction-depth=" ++ show n ++ " instead"
- ; return $ d { reductionDepth = treatZeroAsInf n } })))
, make_ord_flag defFlag "fstrictness-before"
(intSuffix (\n d -> d { strictnessBefore = n : strictnessBefore d }))
, make_ord_flag defFlag "ffloat-lam-args"
@@ -1936,28 +1912,6 @@ dynamic_flags_deps = [
(intSuffix (\n d -> d { uniqueIncrement = n }))
------ Profiling ----------------------------------------------------
-
- -- OLD profiling flags
- , make_dep_flag defGhcFlag "auto-all"
- (noArg (\d -> d { profAuto = ProfAutoAll } ))
- "Use -fprof-auto instead"
- , make_dep_flag defGhcFlag "no-auto-all"
- (noArg (\d -> d { profAuto = NoProfAuto } ))
- "Use -fno-prof-auto instead"
- , make_dep_flag defGhcFlag "auto"
- (noArg (\d -> d { profAuto = ProfAutoExports } ))
- "Use -fprof-auto-exported instead"
- , make_dep_flag defGhcFlag "no-auto"
- (noArg (\d -> d { profAuto = NoProfAuto } ))
- "Use -fno-prof-auto instead"
- , make_dep_flag defGhcFlag "caf-all"
- (NoArg (setGeneralFlag Opt_AutoSccsOnIndividualCafs))
- "Use -fprof-cafs instead"
- , make_dep_flag defGhcFlag "no-caf-all"
- (NoArg (unSetGeneralFlag Opt_AutoSccsOnIndividualCafs))
- "Use -fno-prof-cafs instead"
-
- -- NEW profiling flags
, make_ord_flag defGhcFlag "fprof-auto"
(noArg (\d -> d { profAuto = ProfAutoAll } ))
, make_ord_flag defGhcFlag "fprof-auto-top"
@@ -1982,12 +1936,6 @@ dynamic_flags_deps = [
------ Compiler flags -----------------------------------------------
, make_ord_flag defGhcFlag "fasm" (NoArg (setObjBackend ncgBackend))
- , make_ord_flag defGhcFlag "fvia-c" (NoArg
- (deprecate $ "The -fvia-c flag does nothing; " ++
- "it will be removed in a future GHC release"))
- , make_ord_flag defGhcFlag "fvia-C" (NoArg
- (deprecate $ "The -fvia-C flag does nothing; " ++
- "it will be removed in a future GHC release"))
, make_ord_flag defGhcFlag "fllvm" (NoArg (setObjBackend llvmBackend))
, make_ord_flag defFlag "fno-code" (NoArg ((upd $ \d ->
@@ -2001,11 +1949,6 @@ dynamic_flags_deps = [
dflags' <- liftEwM getCmdLineState
pure $ gopt_unset dflags' Opt_ByteCodeAndObjectCode
- , make_dep_flag defFlag "fglasgow-exts"
- (NoArg enableGlasgowExts) "Use individual extensions instead"
- , make_dep_flag defFlag "fno-glasgow-exts"
- (NoArg disableGlasgowExts) "Use individual extensions instead"
-
------ Safe Haskell flags -------------------------------------------
, make_ord_flag defFlag "fpackage-trust" (NoArg setPackageTrust)
, make_ord_flag defFlag "fno-safe-infer" (noArg (\d ->
@@ -2067,8 +2010,6 @@ dynamic_flags_deps = [
]
------ Language flags -------------------------------------------------
- ++ map (mkFlag turnOn "f" setExtensionFlag ) fLangFlagsDeps
- ++ map (mkFlag turnOff "fno-" unSetExtensionFlag) fLangFlagsDeps
++ map (mkFlag turnOn "X" setExtensionFlag ) xFlagsDeps
++ map (mkFlag turnOff "XNo" unSetExtensionFlag) xFlagsDeps
++ map (mkFlag turnOn "X" setLanguage ) languageFlagsDeps
@@ -2142,11 +2083,6 @@ package_flags_deps = [
(NoArg (addPkgDbRef GlobalPkgDb))
, make_ord_flag defFlag "user-package-db"
(NoArg (addPkgDbRef UserPkgDb))
- -- backwards compat with GHC<=7.4 :
- , make_dep_flag defFlag "package-conf"
- (HasArg $ addPkgDbRef . PkgDbPath . OsPath.unsafeEncodeUtf) "Use -package-db instead"
- , make_dep_flag defFlag "no-user-package-conf"
- (NoArg removeUserPkgDb) "Use -no-user-package-db instead"
, make_ord_flag defGhcFlag "package-name" (HasArg $ \name ->
upd (setUnitId name))
, make_ord_flag defGhcFlag "this-unit-id" (hasArg setUnitId)
@@ -2167,7 +2103,6 @@ package_flags_deps = [
(NoArg (setGeneralFlag Opt_HideAllPluginPackages))
, make_ord_flag defFlag "package-env" (HasArg setPackageEnv)
, make_ord_flag defFlag "ignore-package" (HasArg ignorePackage)
- , make_dep_flag defFlag "syslib" (HasArg exposePackage) "Use -package instead"
, make_ord_flag defFlag "distrust-all-packages"
(NoArg (setGeneralFlag Opt_DistrustAllPackages))
, make_ord_flag defFlag "trust" (HasArg trustPackage)
@@ -2643,8 +2578,6 @@ fFlagsDeps = [
flagSpec "prof-late-inline" Opt_ProfLateInlineCcs,
flagSpec "regs-graph" Opt_RegsGraph,
flagSpec "regs-iterative" Opt_RegsIterative,
- depFlagSpec' "rewrite-rules" Opt_EnableRewriteRules
- (useInstead "-f" "enable-rewrite-rules"),
flagSpec "shared-implib" Opt_SharedImplib,
flagSpec "spec-constr" Opt_SpecConstr,
flagSpec "spec-constr-keen" Opt_SpecConstrKeen,
@@ -2739,43 +2672,6 @@ fHoleFlags = [
flagSpec "unclutter-valid-hole-fits" Opt_UnclutterValidHoleFits
]
--- | These @-f\<blah\>@ flags can all be reversed with @-fno-\<blah\>@
-fLangFlags :: [FlagSpec LangExt.Extension]
-fLangFlags = map snd fLangFlagsDeps
-
-fLangFlagsDeps :: [(Deprecation, FlagSpec LangExt.Extension)]
-fLangFlagsDeps = [
--- See Note [Updating flag description in the User's Guide]
--- See Note [Supporting CLI completion]
- depFlagSpecOp' "th" LangExt.TemplateHaskell
- checkTemplateHaskellOk
- (deprecatedForExtension "TemplateHaskell"),
- depFlagSpec' "fi" LangExt.ForeignFunctionInterface
- (deprecatedForExtension "ForeignFunctionInterface"),
- depFlagSpec' "ffi" LangExt.ForeignFunctionInterface
- (deprecatedForExtension "ForeignFunctionInterface"),
- depFlagSpec' "arrows" LangExt.Arrows
- (deprecatedForExtension "Arrows"),
- depFlagSpec' "implicit-prelude" LangExt.ImplicitPrelude
- (deprecatedForExtension "ImplicitPrelude"),
- depFlagSpec' "bang-patterns" LangExt.BangPatterns
- (deprecatedForExtension "BangPatterns"),
- depFlagSpec' "monomorphism-restriction" LangExt.MonomorphismRestriction
- (deprecatedForExtension "MonomorphismRestriction"),
- depFlagSpec' "extended-default-rules" LangExt.ExtendedDefaultRules
- (deprecatedForExtension "ExtendedDefaultRules"),
- depFlagSpec' "implicit-params" LangExt.ImplicitParams
- (deprecatedForExtension "ImplicitParams"),
- depFlagSpec' "scoped-type-variables" LangExt.ScopedTypeVariables
- (deprecatedForExtension "ScopedTypeVariables"),
- depFlagSpec' "allow-overlapping-instances" LangExt.OverlappingInstances
- (deprecatedForExtension "OverlappingInstances"),
- depFlagSpec' "allow-undecidable-instances" LangExt.UndecidableInstances
- (deprecatedForExtension "UndecidableInstances"),
- depFlagSpec' "allow-incoherent-instances" LangExt.IncoherentInstances
- (deprecatedForExtension "IncoherentInstances")
- ]
-
supportedLanguages :: [String]
supportedLanguages = map (flagSpecName . snd) languageFlagsDeps
@@ -2876,15 +2772,6 @@ enableDLint = do
, Opt_LlvmFillUndefWithGarbage
]
-enableGlasgowExts :: DynP ()
-enableGlasgowExts = do setGeneralFlag Opt_PrintExplicitForalls
- mapM_ setExtensionFlag glasgowExtsFlags
-
-disableGlasgowExts :: DynP ()
-disableGlasgowExts = do unSetGeneralFlag Opt_PrintExplicitForalls
- mapM_ unSetExtensionFlag glasgowExtsFlags
-
-
setWarnSafe :: Bool -> DynP ()
setWarnSafe True = getCurLoc >>= \l -> upd (\d -> d { warnSafeOnLoc = l })
setWarnSafe False = return ()
@@ -3094,7 +2981,6 @@ setExtensionFlag' f dflags = foldr ($) (xopt_set dflags f) deps
unSetExtensionFlag' f dflags = xopt_unset dflags f
-- When you un-set f, however, we don't un-set the things it implies
- -- (except for -fno-glasgow-exts, which is treated specially)
--------------------------
=====================================
compiler/GHC/Parser/Errors/Ppr.hs
=====================================
@@ -971,6 +971,5 @@ forallSym False = text "forall"
pprFileHeaderPragmaType :: FileHeaderPragmaType -> SDoc
pprFileHeaderPragmaType OptionsPrag = text "OPTIONS"
-pprFileHeaderPragmaType IncludePrag = text "INCLUDE"
pprFileHeaderPragmaType LanguagePrag = text "LANGUAGE"
pprFileHeaderPragmaType DocOptionsPrag = text "OPTIONS_HADDOCK"
=====================================
compiler/GHC/Parser/Errors/Types.hs
=====================================
@@ -650,7 +650,6 @@ data TransLayoutReason
data FileHeaderPragmaType
= OptionsPrag
- | IncludePrag
| LanguagePrag
| DocOptionsPrag
=====================================
compiler/GHC/Parser/Header.hs
=====================================
@@ -319,11 +319,6 @@ getOptions' opts sec supported toks
src_span = getLoc open
real_src_span = expectJust (srcSpanToRealSrcSpan src_span)
starting_loc = realSrcSpanStart real_src_span
- parseToks (open:close:xs)
- | ITinclude_prag str <- unLoc open
- , ITclose_prag <- unLoc close
- = fmap (map (L (getLoc open)) ["-#include",removeSpaces str] ++)
- (parseToks xs)
parseToks (open:close:xs)
| ITdocOptions str _ <- unLoc open
, ITclose_prag <- unLoc close
@@ -355,8 +350,6 @@ getOptions' opts sec supported toks
mkMessage (L loc token)
| IToptions_prag _ <- token
= Just (singleMessage $ mkPlainMsgEnvelope diag_opts loc (PsWarnMisplacedPragma OptionsPrag))
- | ITinclude_prag _ <- token
- = Just (singleMessage $ mkPlainMsgEnvelope diag_opts loc (PsWarnMisplacedPragma IncludePrag))
| ITdocOptions _ _ <- token
= Just (singleMessage $ mkPlainMsgEnvelope diag_opts loc (PsWarnMisplacedPragma DocOptionsPrag))
| ITlanguage_prag <- token
=====================================
compiler/GHC/Parser/Lexer.x
=====================================
@@ -857,7 +857,6 @@ data Token
| ITcomplete_prag SourceText
| ITclose_prag
| IToptions_prag String
- | ITinclude_prag String
| ITlanguage_prag
| ITminimal_prag SourceText
| IToverlappable_prag SourceText -- instance overlap mode
@@ -3507,8 +3506,7 @@ linePrags = Map.singleton "line" linePrag
fileHeaderPrags = Map.fromList([("options", lex_string_prag IToptions_prag),
("options_ghc", lex_string_prag IToptions_prag),
("options_haddock", lex_string_prag_comment ITdocOptions),
- ("language", token ITlanguage_prag),
- ("include", lex_string_prag ITinclude_prag)])
+ ("language", token ITlanguage_prag)])
ignoredPrags = Map.fromList (map ignored pragmas)
where ignored opt = (opt, nested_comment)
=====================================
compiler/GHC/Stg/Make.hs
=====================================
@@ -67,7 +67,7 @@ mkTopStgRhs allow_toplevel_con_app opt_AutoSccsOnIndividualCafs this_mod ccs bnd
upd_flag | isAtMostOnceDmd (idDemandInfo bndr) = SingleEntry
| otherwise = Updatable
- -- CAF cost centres generated for -fcaf-all
+ -- CAF cost centres generated for -fprof-cafs
caf_cc = mkAutoCC bndr modl
caf_ccs = mkSingletonCCS caf_cc
-- careful: the binder might be :Main.main,
=====================================
compiler/GHC/Types/Tickish.hs
=====================================
@@ -106,7 +106,7 @@ type CmmTickish = GenTickish 'TickishPassCmm
-- See Note [GHC Formalism] in GHC.Core.Lint
data GenTickish pass =
-- | An @{-# SCC #-}@ profiling annotation, either automatically
- -- added by the desugarer as a result of -auto-all, or added by
+ -- added by the desugarer as a result of -fprof-auto, or added by
-- the user.
ProfNote {
profNoteCC :: CostCentre, -- ^ the cost centre
=====================================
docs/users_guide/codegens.rst
=====================================
@@ -69,23 +69,14 @@ To install LLVM and Clang:
.. _c-code-gen:
-C Code Generator (``-fvia-C``)
-------------------------------
+C Code Generator
+----------------
.. index::
single: C code generator
- single: -fvia-C
-
-.. ghc-flag:: -fvia-C
- :shortdesc: use the C code generator
- :type: dynamic
- :category: warnings
-
- Use the C code generator. Only supposed in unregisterised GHC builds.
This is the oldest code generator in GHC and is generally not included
-any more having been deprecated around GHC 7.0. Select it with the
-:ghc-flag:`-fvia-C` flag.
+any more.
The C code generator is only supported when GHC is built in
unregisterised mode, a mode where GHC produces "portable" C code as
=====================================
docs/users_guide/expected-undocumented-flags.txt
=====================================
@@ -1,8 +1,6 @@
--#include
--abi-hash
--backpack
--show-packages
--Onot
-Walternative-layout-rule-transitional
-XAlternativeLayoutRule
-XAlternativeLayoutRuleTransitional
@@ -19,17 +17,11 @@
-dsource-stats
-dstg-stats
-dsuppress-stg-exts
--fallow-incoherent-instances
--fallow-overlapping-instances
--fallow-undecidable-instances
--farrows
--fbang-patterns
-fbuilding-cabal-package
-fconstraint-solver-iterations
-fgivens-expansion-fuel
-fwanteds-expansion-fuel
-fqcs-expansion-fuel
--fcontext-stack
-fcross-module-specialize
-fdiagnostics-color=always
-fdiagnostics-color=auto
@@ -38,10 +30,7 @@
-fprint-error-index-links=auto
-fprint-error-index-links=never
-fembed-manifest
--fextended-default-rules
-ffast-pap-calls
--fffi
--ffi
-ffloat-all-lams
-ffloat-lam-args
-ffrontend-opt
@@ -49,48 +38,34 @@
-fghci-history
-fghci-sandbox
-fhistory-size
--fimplicit-params
--fimplicit-prelude
-firrefutable-tuples
-fmax-errors
-fmax-pmcheck-iterations
--fmonomorphism-restriction
-fpre-inlining
-fprint-bind-contents
-freduction-depth
--frewrite-rules
--fscoped-type-variables
-fshared-implib
-fshow-valid-hole-fits
-fshow-valid-substitutions
-fspec-constr-recursive
-fspecialize
-fspecialize-aggressively
--fth
--ftype-function-depth
-fversion-macros
--fvia-c
-haddock-opts
-instantiated-with
-keep-hi-file
-keep-o-file
--n
-no-keep-hi-file
-no-keep-o-file
-no-link
--no-recomp
-no-rtsopts
--no-user-package-conf
--package-conf
-package-name
-pgmar
-pgmranlib
--recomp
-relative-dynlib-paths
-rtsopts=all
-rtsopts=ignore
-rtsopts=ignoreAll
-rtsopts=none
-rtsopts=some
--syslib
-this-component-id
=====================================
docs/users_guide/exts/control.rst
=====================================
@@ -244,25 +244,3 @@ Similarly, language extensions can be controlled (either enabled or disabled):
* :extension:`StarIsType`
* :extension:`TraditionalRecordSyntax`
* :extension:`ImplicitStagePersistence`
-
-
-
-Although not recommended, the deprecated :ghc-flag:`-fglasgow-exts` flag enables
-a large swath of the extensions supported by GHC at once.
-
-.. ghc-flag:: -fglasgow-exts
- :shortdesc: Deprecated. Enable most language extensions;
- see :ref:`options-language` for exactly which ones.
- :type: dynamic
- :reverse: -fno-glasgow-exts
- :category: misc
-
- The flag ``-fglasgow-exts`` is equivalent to enabling the following extensions:
-
- .. include:: ../what_glasgow_exts_does.rst
-
- Enabling these options is the *only* effect of ``-fglasgow-exts``. We are trying
- to move away from this portmanteau flag, and towards enabling features
- individually.
-
-
=====================================
docs/users_guide/exts/ffi.rst
=====================================
@@ -766,9 +766,6 @@ calls across module and package boundaries: there's no need for the header file
to be available when compiling an inlined version of a foreign call, so the
compiler is free to inline foreign calls in any context.
-The ``-#include`` option is now deprecated, and the ``includes``
-field in a Cabal package specification is ignored.
-
Memory Allocation
~~~~~~~~~~~~~~~~~
=====================================
docs/users_guide/exts/pragmas.rst
=====================================
@@ -26,8 +26,8 @@ Certain pragmas are *file-header pragmas*:
- File-header pragmas are read once only, before pre-processing the
file (e.g. with cpp).
-- The file-header pragmas are: ``{-# LANGUAGE #-}``,
- ``{-# OPTIONS_GHC #-}``, and ``{-# INCLUDE #-}``.
+- The file-header pragmas are: ``{-# LANGUAGE #-}`` and
+ ``{-# OPTIONS_GHC #-}``.
.. _language-pragma:
@@ -80,16 +80,6 @@ Previous versions of GHC accepted ``OPTIONS`` rather than
``OPTIONS_GHC`` is a file-header pragma (see :ref:`pragmas`).
-.. _include-pragma:
-
-``INCLUDE`` pragma
-------------------
-
-The ``INCLUDE`` used to be necessary for specifying header files to be
-included when using the FFI and compiling via C. It is no longer
-required for GHC, but is accepted (and ignored) for compatibility with
-other compilers.
-
.. _warning-deprecated-pragma:
``WARNING`` and ``DEPRECATED`` pragmas
=====================================
docs/users_guide/ghc.rst
=====================================
@@ -28,8 +28,7 @@ As a rule of thumb, all the language options are dynamic, as are the
warning options and the debugging options.
The rest are static, with the notable exceptions of
-``-v``, ``-cpp``, ``-fasm``, ``-fvia-C``, ``-fllvm``, and
-``-#include``.
+``-v``, ``-cpp``, ``-fasm``, and ``-fllvm``.
The OPTIONS sections lists the status of each flag.
Common suffixes of file names for Haskell are:
=====================================
docs/users_guide/profiling.rst
=====================================
@@ -594,42 +594,6 @@ of your profiled program will be different to that of the unprofiled one.
Process (or ignore) manual ``SCC`` annotations. Can be helpful to ignore annotations from libraries which
are not desired.
-.. ghc-flag:: -auto-all
- :shortdesc: *(deprecated)* Alias for :ghc-flag:`-fprof-auto`
- :type: dynamic
-
- Deprecated alias for :ghc-flag:`-fprof-auto`
-
-.. ghc-flag:: -auto
- :shortdesc: *(deprecated)* Alias for :ghc-flag:`-fprof-auto-exported`
- :type: dynamic
-
- Deprecated alias for :ghc-flag:`-fprof-auto-exported`
-
-.. ghc-flag:: -caf-all
- :shortdesc: *(deprecated)* Alias for :ghc-flag:`-fprof-cafs`
- :type: dynamic
-
- Deprecated alias for :ghc-flag:`-fprof-cafs`
-
-.. ghc-flag:: -no-auto-all
- :shortdesc: *(deprecated)* Alias for :ghc-flag:`-fno-prof-auto`
- :type: dynamic
-
- Deprecated alias for :ghc-flag:`-fno-prof-auto`
-
-.. ghc-flag:: -no-auto
- :shortdesc: *(deprecated)* Alias for :ghc-flag:`-fno-prof-auto`
- :type: dynamic
-
- Deprecated alias for :ghc-flag:`-fno-prof-auto`
-
-.. ghc-flag:: -no-caf-all
- :shortdesc: *(deprecated)* Alias for :ghc-flag:`-fno-prof-cafs`
- :type: dynamic
-
- Deprecated alias for :ghc-flag:`-fno-prof-cafs`
-
.. _prof-time-options:
Time and allocation profiling
=====================================
docs/users_guide/what_glasgow_exts_does.rst deleted
=====================================
@@ -1,34 +0,0 @@
-.. hlist::
-
- * :extension:`ConstrainedClassMethods`
- * :extension:`DeriveDataTypeable`
- * :extension:`DeriveFoldable`
- * :extension:`DeriveFunctor`
- * :extension:`DeriveGeneric`
- * :extension:`DeriveTraversable`
- * :extension:`EmptyDataDecls`
- * :extension:`ExistentialQuantification`
- * :extension:`ExplicitNamespaces`
- * :extension:`FlexibleContexts`
- * :extension:`FlexibleInstances`
- * :extension:`ForeignFunctionInterface`
- * :extension:`FunctionalDependencies`
- * :extension:`GeneralizedNewtypeDeriving`
- * :extension:`ImplicitParams`
- * :extension:`InterruptibleFFI`
- * :extension:`KindSignatures`
- * :extension:`LiberalTypeSynonyms`
- * :extension:`MagicHash`
- * :extension:`MultiParamTypeClasses`
- * :extension:`ParallelListComp`
- * :extension:`PatternGuards`
- * :extension:`PostfixOperators`
- * :extension:`RankNTypes`
- * :extension:`RecursiveDo`
- * :extension:`ScopedTypeVariables`
- * :extension:`StandaloneDeriving`
- * :extension:`TypeOperators`
- * :extension:`TypeSynonymInstances`
- * :extension:`UnboxedTuples`
- * :extension:`UnicodeSyntax`
- * :extension:`UnliftedFFITypes`
=====================================
testsuite/tests/driver/Makefile
=====================================
@@ -149,18 +149,16 @@ test026:
test -f d026/P/Q$(OBJSUFFIX)
# test stub generation
-# -fvia-C, because we want to check that the .hc file can #include the stub.h
test027:
$(RM) B027/F.hi B027/F$(OBJSUFFIX) B027/F_stub.h
- "$(TEST_HC)" $(TEST_HC_OPTS) -c B027/F.hs -fno-warn-deprecated-flags -fvia-C
+ "$(TEST_HC)" $(TEST_HC_OPTS) -c B027/F.hs
test -f B027/F_stub.h
# test -stubdir
-# -fvia-C, because we want to check that the .hc file can #include the stub.h
test028:
$(RM) B028/F.hi B028/F$(OBJSUFFIX)
$(RM) stub028/B028/F_stub.h
- "$(TEST_HC)" $(TEST_HC_OPTS) -c B028/F.hs -stubdir stub028 -fno-warn-deprecated-flags -fvia-C
+ "$(TEST_HC)" $(TEST_HC_OPTS) -c B028/F.hs -stubdir stub028
test -f stub028/B028/F_stub.h
# -----------------------------------------------------------------------------
@@ -289,16 +287,16 @@ test053:
# -----------------------------------------------------------------------------
# Other tests
-# Test that -keep-s-files works with --make and -fvia-C
+# Test that -keep-s-files works with --make
test061a:
$(RM) A061a.hi A061a$(OBJSUFFIX) A061a.s
- "$(TEST_HC)" $(TEST_HC_OPTS) -v0 --make -keep-s-files -fno-warn-deprecated-flags -fvia-C A061a.hs
+ "$(TEST_HC)" $(TEST_HC_OPTS) -v0 --make -keep-s-files A061a.hs
test -f A061a.s
# Test that -keep-s-files works without --make
test061b:
$(RM) A061b.hi A061b$(OBJSUFFIX) A061b.s
- "$(TEST_HC)" $(TEST_HC_OPTS) -c -keep-s-files -fno-warn-deprecated-flags -fvia-C A061b.hs
+ "$(TEST_HC)" $(TEST_HC_OPTS) -c -keep-s-files A061b.hs
test -f A061b.s
# Test that -main-is works with --make
=====================================
testsuite/tests/driver/T2464.hs
=====================================
@@ -1,9 +1,13 @@
{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -DTEST #-}
-{-# OPTIONS_GHC -fffi #-} -- deprecation warning
+{-# OPTIONS_GHC -Wno-such-warning #-} -- warned about exactly once
#if defined(TEST)
-{-# LANGUAGE EmptyDataDecls #-}
+{-# LANGUAGE MagicHash #-}
#endif
module Test2464 where
-data T
+
+import GHC.Exts
+
+f :: Int# -> Int#
+f x = x +# 1#
=====================================
testsuite/tests/driver/T2464.stderr
=====================================
@@ -1,3 +1,3 @@
-T2464.hs:3:17: warning: [GHC-53692] [-Wdeprecated-flags (in -Wdefault)]
- -fffi is deprecated: use -XForeignFunctionInterface or pragma {-# LANGUAGE ForeignFunctionInterface #-} instead
+T2464.hs:3:17: warning: [GHC-93741] [-Wunrecognised-warning-flags (in -Wdefault)]
+ unrecognised warning flag: -Wno-such-warning
=====================================
testsuite/tests/ffi/should_run/T2594.hs
=====================================
@@ -1,4 +1,4 @@
-{-# options -fffi #-}
+{-# LANGUAGE ForeignFunctionInterface #-}
import Foreign
import Foreign.C.Types
=====================================
testsuite/tests/ffi/should_run/ffi015.hs
=====================================
@@ -1,4 +1,3 @@
-{-# OPTIONS_GHC -#include "ffi015_cbits.h" #-}
{-# LANGUAGE ForeignFunctionInterface #-}
import Foreign
=====================================
testsuite/tests/ffi/should_run/fptr01.hs
=====================================
@@ -4,8 +4,6 @@ module Main where
import Foreign
-{-# INCLUDE "fptr01.h" #-}
-
foreign import ccall "&f" fptr :: FunPtr (Ptr Int -> IO ())
foreign import ccall "&g" gptr :: FunPtr (Ptr Int -> IO ())
foreign import ccall "&h" hptr :: FunPtr (Ptr Int -> IO ())
=====================================
testsuite/tests/ffi/should_run/fptrfail01.hs
=====================================
@@ -5,8 +5,6 @@ module Main where
import Foreign
import GHC.ForeignPtr
-{-# INCLUDE "fptrfail01.h" #-}
-
foreign import ccall "&f" fptr :: FunPtr (Ptr Int -> IO ())
main :: IO ()
=====================================
testsuite/tests/indexed-types/should_compile/all.T
=====================================
@@ -17,7 +17,7 @@ test('Simple16', normal, compile, [''])
test('Simple17', normal, compile, [''])
test('Simple18', normal, compile, [''])
test('Simple19', normal, compile, [''])
-test('Simple20', expect_broken(4296), compile, ['-fcontext-stack=10'])
+test('Simple20', expect_broken(4296), compile, ['-freduction-depth=10'])
test('Simple21', normal, compile, [''])
test('Simple22', normal, compile, [''])
test('Simple23', normal, compile, [''])
=====================================
testsuite/tests/indexed-types/should_fail/SkolemOccursLoop.hs
=====================================
@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -ftype-function-depth=3 #-}
+{-# OPTIONS_GHC -freduction-depth=3 #-}
{-# LANGUAGE TypeFamilies, FlexibleContexts, EmptyDataDecls #-}
module SkolemOccursLoop where
=====================================
utils/haddock/haddock-api/src/Haddock/Backends/Hyperlinker/Parser.hs
=====================================
@@ -257,7 +257,6 @@ classify tok =
ITcomplete_prag{} -> TkPragma
ITclose_prag -> TkPragma
IToptions_prag{} -> TkPragma
- ITinclude_prag{} -> TkPragma
ITlanguage_prag -> TkPragma
ITminimal_prag{} -> TkPragma
IToverlappable_prag{} -> TkPragma
@@ -397,7 +396,6 @@ inPragma False tok =
ITann_prag{} -> True
ITcomplete_prag{} -> True
IToptions_prag{} -> True
- ITinclude_prag{} -> True
ITlanguage_prag -> True
ITminimal_prag{} -> True
IToverlappable_prag{} -> True
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/b3ba3621bb41972b140eb7857e50f2…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/b3ba3621bb41972b140eb7857e50f2…
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/fendor/dep-json] 4 commits: Add `-dep-json` flag to `ghc -M`
by Hannes Siebenhandl (＠fendor) 13 Oct '26
by Hannes Siebenhandl (＠fendor) 13 Oct '26
13 Oct '26
Hannes Siebenhandl pushed to branch wip/fendor/dep-json at Glasgow Haskell Compiler / GHC
Commits:
821889fb by fendor at 2026-10-13T21:55:52+02:00
Add `-dep-json` flag to `ghc -M`
Add an optional flag to `ghc -M` that allows to write the dependency
information in JSON Lines format.
The JSON Lines format enables us to stream the output of the dependency
generation to a consumer.
The output of `-dep-json` is streamed to a temporary file and then
copied to the final destination to avoid partial writes.
Each line contains one of two possible json objects:
1. A Home Unit Dependency
* Contains the name of the home module, its unit, where it is
located, whether a preprocessor is used, and all of its imports.
Importantly, the imports include `-XExplicitLevelImports`
information.
* If requested via `-include-pkg-deps`, includes imports of external
units, e.g. modules from `base`.
* If requested via `-include-cpp-deps`, files included via CPP.
2. External Unit Dependency
* Only if `-include-pkg-deps` is given
* Contains unit-id, its package name and package id.
- - - - -
7efdd5c5 by fendor at 2026-10-13T21:55:52+02:00
Add multiple home unit support to `ghc -M`
Allows to process the module graph of multiple home units at once using
the same syntax as `--make` and `--interactive`:
ghc -M -unit @unitA -unit @unitB
The semantics are identical to `--make` and `--interactive`.
Each home unit can declare individually to use `-include-cpp-deps` and
`-include-pkg-deps`.
However, there can only be one output file, and `-dep-json` and
`-dep-makefile` can only be provided at the top of the cli invocation.
We introduce a new GHC API `doMkDepend` that allows to use multiple home
units conveniently.
The output of `-dep-json` and `-dep-makefile` does not change, since we
were careful to choose a format that supports multiple home units from
the start.
Single home units are still accepted like before with no changes.
- - - - -
57781c86 by fendor at 2026-10-13T21:55:52+02:00
Deprecate `doMkDependHS` in favour of `doMkDepend`
- - - - -
cd063639 by fendor at 2026-10-13T21:55:52+02:00
Improve `ghc -M` test-suite
Adds a more extensive test-suite for `ghc -M` mode.
Introduce a dedicated test mode for running `ghc -M` tests more
conveniently.
Adds lots of normalizers that help to write `ghc -M` tests in a platform
independent manner.
Adds utility scripts that help format the output of `ghc -M`.
Add new perf regression tests for json and makefile generation.
Add perf regression test for multiple home unit support.
- - - - -
62 changed files:
- + changelog.d/make-depends-json
- compiler/GHC/Driver/DynFlags.hs
- compiler/GHC/Driver/MakeFile.hs
- compiler/GHC/Driver/Session.hs
- compiler/GHC/Driver/Session/Units.hs
- compiler/GHC/Utils/Json.hs
- + docs/users_guide/make-depends-json-schema-1_0.json
- docs/users_guide/separate_compilation.rst
- ghc/Main.hs
- testsuite/driver/testglobals.py
- testsuite/driver/testlib.py
- testsuite/tests/driver/mkdepend/Makefile
- + testsuite/tests/driver/mkdepend/README.md
- testsuite/tests/driver/mkdepend/A.hs → testsuite/tests/driver/mkdepend/T24384/A.hs
- testsuite/tests/driver/mkdepend/C.hs → testsuite/tests/driver/mkdepend/T24384/C.hs
- testsuite/tests/driver/mkdepend/C.hs-boot → testsuite/tests/driver/mkdepend/T24384/C.hs-boot
- testsuite/tests/driver/mkdepend/D.hs → testsuite/tests/driver/mkdepend/T24384/D.hs
- testsuite/tests/driver/mkdepend/E.hs → testsuite/tests/driver/mkdepend/T24384/E.hs
- testsuite/tests/driver/mkdepend/dep-internal/DepInternal.hs → testsuite/tests/driver/mkdepend/T24384/dep-internal/DepInternal.hs
- testsuite/tests/driver/mkdepend/dep-internal/dep-internal.pkg → testsuite/tests/driver/mkdepend/T24384/dep-internal/dep-internal.pkg
- testsuite/tests/driver/mkdepend/dep-public/DepPublic.hs → testsuite/tests/driver/mkdepend/T24384/dep-public/DepPublic.hs
- testsuite/tests/driver/mkdepend/dep-public/dep-public.pkg → testsuite/tests/driver/mkdepend/T24384/dep-public/dep-public.pkg
- testsuite/tests/driver/mkdepend/dep/Dep.hs → testsuite/tests/driver/mkdepend/T24384/dep/Dep.hs
- testsuite/tests/driver/mkdepend/dep/dep.pkg → testsuite/tests/driver/mkdepend/T24384/dep/dep.pkg
- testsuite/tests/driver/mkdepend/foo.h → testsuite/tests/driver/mkdepend/T24384/foo.h
- testsuite/tests/driver/mkdepend/lib/B.hs → testsuite/tests/driver/mkdepend/T24384/lib/B.hs
- + testsuite/tests/driver/mkdepend/T24384/lib/B.hs-boot
- testsuite/tests/driver/mkdepend/preproc.sh → testsuite/tests/driver/mkdepend/T24384/preproc.sh
- testsuite/tests/driver/mkdepend/T24384a.stdout
- + testsuite/tests/driver/mkdepend/T24384b.stdout
- + testsuite/tests/driver/mkdepend/T24384c.stdout
- testsuite/tests/driver/mkdepend/all.T
- + testsuite/tests/driver/mkdepend/format_json.sh
- + testsuite/tests/driver/mkdepend/format_makefile.sh
- + testsuite/tests/driver/mkdepend/mhu01/a/A/Base.hs
- + testsuite/tests/driver/mkdepend/mhu01/a/A/Base.hs-boot
- + testsuite/tests/driver/mkdepend/mhu01/a/A/TH.hs
- + testsuite/tests/driver/mkdepend/mhu01/a/Util.hs
- + testsuite/tests/driver/mkdepend/mhu01/b/B/Normal.hs
- + testsuite/tests/driver/mkdepend/mhu01/b/B/Splice.hs
- + testsuite/tests/driver/mkdepend/mhu01/b/Util.hs
- + testsuite/tests/driver/mkdepend/mhu01/c/C.hs
- + testsuite/tests/driver/mkdepend/mhu01/unitA
- + testsuite/tests/driver/mkdepend/mhu01/unitB
- + testsuite/tests/driver/mkdepend/mhu01/unitC
- + testsuite/tests/driver/mkdepend/mhu02/A.hs
- + testsuite/tests/driver/mkdepend/mhu02/B.hs
- + testsuite/tests/driver/mkdepend/mhu02/pp.sh
- + testsuite/tests/driver/mkdepend/mhu02/unitA
- + testsuite/tests/driver/mkdepend/mhu02/unitB
- + testsuite/tests/driver/mkdepend/mhu03/pkg/A.hs
- + testsuite/tests/driver/mkdepend/mhu03/pkg/pp.sh
- + testsuite/tests/driver/mkdepend/mhu03/unitA
- + testsuite/tests/driver/mkdepend/mkdepend01.dep-json
- + testsuite/tests/driver/mkdepend/mkdepend01.dep-makefile
- + testsuite/tests/driver/mkdepend/mkdepend01/A.hs
- + testsuite/tests/driver/mkdepend/mkdepend_mhu01.dep-json
- + testsuite/tests/driver/mkdepend/mkdepend_mhu01.dep-makefile
- + testsuite/tests/driver/mkdepend/mkdepend_mhu02.dep-json
- + testsuite/tests/driver/mkdepend/mkdepend_mhu03.dep-json
- testsuite/tests/perf/compiler/large-project/all.T
- + testsuite/tests/perf/compiler/large-project/large-project-mhu.sh
The diff was not included because it is too large.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f10cb35cf25d9a55c591a9c05e9add…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f10cb35cf25d9a55c591a9c05e9add…
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/fendor/27836] 13 commits: Do not leave standard file descriptors free at startup (#24450)
by Hannes Siebenhandl (＠fendor) 13 Oct '26
by Hannes Siebenhandl (＠fendor) 13 Oct '26
13 Oct '26
Hannes Siebenhandl pushed to branch wip/fendor/27836 at Glasgow Haskell Compiler / GHC
Commits:
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
- - - - -
15ece296 by mangoiv at 2026-10-08T15:14:56-04:00
ci: move hadrian/ghci into the lint category so it can be picked up by more runners
Fixes #27817
- - - - -
c0823135 by mangoiv at 2026-10-08T15:14:56-04:00
ci: make lint-adjacent jobs into platform independent
- move lint jobs into lint-anyarch tag
- unify lint jobs under the same platform independent container
- - - - -
f76464cf by Zubin Duggal at 2026-10-08T15:15:39-04:00
DmdAnal: Make AbsDmd neutral in maxDmd
fixes #27845
- - - - -
ffa56ae4 by sheaf at 2026-10-09T17:15:59+02:00
Preserve sign of zero when parsing -0.0#
This commit leverages the recently added GHC.Types.Literal.Floating
module in order to preserve the sign of negative zero from
source-written floating-point literals.
Fixes #27545
- - - - -
d538cac9 by Facundo Domínguez at 2026-10-09T20:26:38-04:00
Propagate annotations to simple interfaces
This allows annotations to be visible to plugins when run by
haddock. The LiquidHaskell plugin needs the annotations, in particular.
Fixes #26761
- - - - -
32c4f4ab by meooow25 at 2026-10-09T20:27:28-04:00
Bump containers submodule to 0.8.1
And fix affected tests.
* T4086a: containers depends on template-haskell-lift now instead of
template-haskell.
* T22611: Updated to be less dependent on containers internals.
- - - - -
c786065e by sheaf at 2026-10-09T20:28:20-04:00
Use an explicit pattern match in toIfaceIdDetails
The old wildcard pattern let this code bit rot: it did not properly account
for recently added 'IdDetails' such as 'RepPolyId', which resulted in
spurious 'pprTrace' messages that could even pollute HLS sessions.
Fixes #23785
- - - - -
e7cacf59 by sheaf at 2026-10-09T20:29:09-04:00
Take into account ifKind in freeNamesIfDecl
Commit 3c2f4bb4 added the 'ifKind' field to various constructors
of 'IfaceDecl', which preserves the original kind (before type synonym
expansion) for better error messages.
However, that commit forgot to update 'freeNamesIfDecl' correspondingly.
This could result in a "urk! lookup local fingerpring" crash when e.g.
a type's kind uses a type synonym defined later, as we failed to add a
dependency on the type synonym during dependency analysis.
Fixes #27916
- - - - -
41e80f41 by Simon Peyton Jones at 2026-10-11T14:38:51-04:00
Simplify the error-suppression mechanism in GHC.Tc.Errors
In `GHC.Tc.Errors.reportWanteds` we suppress some errors in favour of
others. But the mechanism had grown crufty, and #27331 exposed a bug.
This MR makes it simpler and more uniform, by doing everything via
the `ei_suppress` field of the ErrorItem.
Claude then found another closely-related bug (see the review linked
on !16564). That bug is immortalised in new test T18851d.
I'm still not happy with `ignoreConstraint` but we can worry about
that another day; I have not touched it.
Main changes
* Instead of /predicting/ when an error will be reported, we set
`cec_error_reported` when an error is /actually/ reported. (I renamed
it from `cec_suppress` to reflect this change.)
Now errors are suppressed only when a preceding error has actually been
reported. Simpler and more robust.
See `Note [cec_error_reported: suppressing less-serious errors]`
The big changes are in `reportWanteds` which looks very different.
* New `Note [ei_suppress: suppressing confusing errors]` describes the
(quite separate) `ei_suppress` mechanism for suppressing confusing
errors, mainly arising from non-empty rewriter sets
* In `tryTypeClassDefaulting`, instead of switching off type-class defaulting
if there is an insoluble /anywhere/, we just switch it off locally when
we find an insoluble sub-tree. See Note [When to do type-class defaulting]
and (W5) in Note [ApproximateWC]
* Greatly simplify `insolubleWantedCt`.
* I made type-class-defaulting be a bit more eager, only switched off when
a peer or ancestor (but not child) constraint is insoluble. See
Note [When to do type-class defaulting].
Small refactorings
* Rename `askNoErrs` to `askErrsFound` and flip its polarity
* The code for "check if ei_suppress is true of all items" code is
moved to `mkErrorItems` rather than in the large `reportWanteds`.
* Code for `has_gadt_match` moves to `mkGivenErrorReporter`, rather than
polluting the large `reportWanteds`.
* Many tests with `-fdefer-type-errors` get more warnings, especially
about ambiguous (Num a) constraints. This is by-design: see
Note [Always warn with -fdefer-type-errors]. Previously GHC was not
honouring this Note but now it is, hence the extra errors.
- - - - -
f217fc31 by Cheng Shao at 2026-10-11T14:39:33-04:00
compiler: ensure cross ghc --info output target unit ids
Previously, for cross ghcs, the base/ghc/ghc-internal unit ids in
--info output do not match the target unit ids reported by ghc-pkg,
breaking cross ghc release builds with hash-unit-ids when being used
with cabal 3.18. This patch fixes it by making --info output target
unit ids. Fixes #27919.
Co-authored-by: Codex <codex(a)openai.com>
- - - - -
602eda76 by Hannes Siebenhandl at 2026-10-13T18:21:46+02:00
Fix #27836, normalise unit database path in ExternalUnitDatabases
Add a regression test, proofing that all variations:
- local-unit-db/my-test.conf
- ./local-unit-db/my-test.conf
- ./local-unit-db/my-test.conf/
are parsed only once.
- - - - -
120 changed files:
- .gitlab-ci.yml
- .gitlab/hello.hs
- + changelog.d/24450
- + changelog.d/26761
- + changelog.d/27845
- + changelog.d/T23785
- + changelog.d/T27545
- + changelog.d/T27731
- + changelog.d/T27916
- + changelog.d/fix-cross-ghc-info-unit-id
- changelog.d/fix-parallel-gc-selector-race-27477
- changelog.d/unit-index
- compiler/GHC/Builtin/WiredIn/Ids.hs
- compiler/GHC/Core/Make.hs
- compiler/GHC/CoreToIface.hs
- compiler/GHC/Data/OsPath.hs
- compiler/GHC/Driver/Session.hs
- compiler/GHC/Hs/Lit.hs
- compiler/GHC/HsToCore/Match/Literal.hs
- compiler/GHC/Iface/Decl.hs
- compiler/GHC/Iface/Syntax.hs
- compiler/GHC/Iface/Tidy.hs
- compiler/GHC/Rename/Module.hs
- compiler/GHC/Settings.hs
- compiler/GHC/Settings/IO.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Instance/Family.hs
- compiler/GHC/Tc/Solver/Default.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/Monad.hs
- compiler/GHC/Types/Demand.hs
- compiler/GHC/Unit/External/Database.hs
- compiler/Language/Haskell/Syntax/Lit.hs
- distrib/configure.ac.in
- hadrian/bindist/Makefile
- hadrian/bindist/config.mk.in
- hadrian/src/Rules/BinaryDist.hs
- hadrian/src/Rules/Generate.hs
- libraries/containers
- rts/RtsStartup.c
- + testsuite/tests/dmdanal/should_run/T27845.hs
- + testsuite/tests/dmdanal/should_run/T27845.stdout
- + testsuite/tests/dmdanal/should_run/T27845_Lib.hs
- + testsuite/tests/dmdanal/should_run/T27845b.hs
- + testsuite/tests/dmdanal/should_run/T27845b.stdout
- + testsuite/tests/dmdanal/should_run/T27845b_Lib.hs
- testsuite/tests/dmdanal/should_run/all.T
- + testsuite/tests/driver/T27836/A.hs
- + testsuite/tests/driver/T27836/B.hs
- + testsuite/tests/driver/T27836/C.hs
- + testsuite/tests/driver/T27836/Makefile
- + testsuite/tests/driver/T27836/T27836.stdout
- + testsuite/tests/driver/T27836/all.T
- + testsuite/tests/driver/T27836/unitA
- + testsuite/tests/driver/T27836/unitB
- + testsuite/tests/driver/T27836/unitC
- testsuite/tests/ghci/prog020/ghci.prog020a.stderr
- testsuite/tests/ghci/prog020/ghci.prog020b.stderr
- testsuite/tests/ghci/prog021/prog021a.stderr
- testsuite/tests/ghci/prog021/prog021b.stderr
- testsuite/tests/ghci/prog022/ghci.prog022a.stderr
- testsuite/tests/ghci/prog022/ghci.prog022b.stderr
- testsuite/tests/ghci/prog022/ghci.prog022c.stderr
- testsuite/tests/ghci/prog022/ghci.prog022d.stderr
- testsuite/tests/ghci/prog022/ghci.prog022e.stderr
- testsuite/tests/ghci/prog022/ghci.prog022f.stderr
- testsuite/tests/ghci/scripts/Defer02.stderr
- testsuite/tests/module/mod130.stderr
- + testsuite/tests/numeric/should_run/T27545.hs
- + testsuite/tests/numeric/should_run/T27545.stdout
- testsuite/tests/numeric/should_run/all.T
- testsuite/tests/overloadedstrings/should_fail/T25926.stderr
- testsuite/tests/overloadedstrings/should_fail/T27124.stderr
- testsuite/tests/package/T4806a.stderr
- testsuite/tests/package/all.T
- testsuite/tests/patsyn/should_fail/records-nofieldselectors.stderr
- + testsuite/tests/plugins/T26761.hs
- + testsuite/tests/plugins/T26761.stderr
- + testsuite/tests/plugins/T26761Plugin.hs
- + testsuite/tests/plugins/T26761a.hs
- testsuite/tests/plugins/all.T
- testsuite/tests/printer/T17697.stderr
- testsuite/tests/rename/should_fail/T15607.stderr
- testsuite/tests/rename/should_fail/T19843b.stderr
- + testsuite/tests/rts/T24450.hs
- + testsuite/tests/rts/T24450.stderr
- testsuite/tests/rts/all.T
- testsuite/tests/safeHaskell/ghci/p4.stderr
- testsuite/tests/safeHaskell/ghci/p6.stderr
- testsuite/tests/simplCore/should_compile/T22611.hs
- testsuite/tests/simplCore/should_compile/T22611.stderr
- + testsuite/tests/simplCore/should_compile/T22611a.hs
- testsuite/tests/simplCore/should_compile/all.T
- testsuite/tests/typecheck/should_compile/T11254.stderr
- testsuite/tests/typecheck/should_compile/T15370.stderr
- + testsuite/tests/typecheck/should_compile/T27916.hs
- testsuite/tests/typecheck/should_compile/all.T
- testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr
- testsuite/tests/typecheck/should_fail/ClassOperator.stderr
- testsuite/tests/typecheck/should_fail/DoExpansion2.stderr
- testsuite/tests/typecheck/should_fail/DoExpansion3.stderr
- testsuite/tests/typecheck/should_fail/FunDepOrigin1b.hs
- testsuite/tests/typecheck/should_fail/T18851.stderr
- + testsuite/tests/typecheck/should_fail/T18851e.hs
- + testsuite/tests/typecheck/should_fail/T18851e.stderr
- + testsuite/tests/typecheck/should_fail/T18851f.hs
- + testsuite/tests/typecheck/should_fail/T18851f.stderr
- testsuite/tests/typecheck/should_fail/T22940.stderr
- testsuite/tests/typecheck/should_fail/T26823.stderr
- + testsuite/tests/typecheck/should_fail/T27731.hs
- + testsuite/tests/typecheck/should_fail/T27731.stderr
- testsuite/tests/typecheck/should_fail/T5691.stderr
- testsuite/tests/typecheck/should_fail/T7437.stderr
- testsuite/tests/typecheck/should_fail/all.T
- testsuite/tests/typecheck/should_fail/mc24.stderr
- testsuite/tests/typecheck/should_fail/tcfail019.stderr
- testsuite/tests/typecheck/should_fail/tcfail189.stderr
The diff was not included because it is too large.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9033b04b101cd3edae073c352f8fd1…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9033b04b101cd3edae073c352f8fd1…
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