[Git][ghc/ghc][wip/T26514a] 12 commits: Refactor fundep solving
by Simon Peyton Jones (@simonpj) 05 Nov '25
by Simon Peyton Jones (@simonpj) 05 Nov '25
05 Nov '25
Simon Peyton Jones pushed to branch wip/T26514a at Glasgow Haskell Compiler / GHC
Commits:
fcf6331e by Richard Eisenberg at 2025-11-03T08:33:05+00:00
Refactor fundep solving
This commit is a large-scale refactor of the increasingly-messy code that
handles functional dependencies. It has virtually no effect on what compiles
but improves error messages a bit. And it does the groundwork for #23162.
The big picture is described in
Note [Overview of functional dependencies in type inference]
in GHC.Tc.Solver.FunDeps
* New module GHC.Tc.Solver.FunDeps contains all the fundep-handling
code for the constraint solver.
* Fundep-equalities are solved in a nested scope; they may generate
unifications but otherwise have no other effect.
See GHC.Tc.Solver.FunDeps.solveFunDeps
The nested needs to start from the Givens in the inert set, but
not the Wanteds; hence a new function `resetInertCans`, used in
`nestFunDepsTcS`.
* That in turn means that fundep equalities never show up in error
messages, so the complicated FunDepOrigin tracking can all disappear.
* We need to be careful about tracking unifications, so we kick out
constraints from the inert set after doing unifications. Unification
tracking has been majorly reformed: see Note [WhatUnifications] in
GHC.Tc.Utils.Unify.
A good consequence is that the hard-to-grok `resetUnificationFlag`
has been replaced with a simpler use of
`reportCoarseGrainUnifications`
Smaller things:
* Rename `FunDepEqn` to `FunDepEqns` since it contains multiple
type equalities.
Some compile time improvement
Metrics: compile_time/bytes allocated
Baseline
Test value New value Change
---------------------- --------------------------------------
T5030(normal) 173,839,232 148,115,248 -14.8% GOOD
hard_hole_fits(normal) 286,768,048 284,015,416 -1.0%
geo. mean -0.2%
minimum -14.8%
maximum +0.3%
Metric Decrease:
T5030
- - - - -
231adc30 by Simon Peyton Jones at 2025-11-03T08:33:05+00:00
QuickLook's tcInstFun should make instantiation variables directly
tcInstFun must make "instantiation variables", not regular
unification variables, when instantiating function types. That was
previously implemented by a hack: set the /ambient/ level to QLInstTyVar.
But the hack finally bit me, when I was refactoring WhatUnifications.
And it was always wrong: see the now-expunged (TCAPP2) note.
This commit does it right, by making tcInstFun call its own
instantiation functions. That entails a small bit of duplication,
but the result is much, much cleaner.
- - - - -
39d4a24b by Simon Peyton Jones at 2025-11-03T08:33:05+00:00
Build implication for constraints from (static e)
This commit addresses #26466, by buiding an implication for the
constraints arising from a (static e) form. The implication has
a special ic_info field of StaticFormSkol, which tells the constraint
solver to use an empty set of Givens.
See (SF3) in Note [Grand plan for static forms]
in GHC.Iface.Tidy.StaticPtrTable
This commit also reinstates an `assert` in GHC.Tc.Solver.Equality.
The test `StaticPtrTypeFamily` was failing with an assertion failure,
but it now works.
- - - - -
2e2aec1e by Simon Peyton Jones at 2025-11-03T08:33:05+00:00
Comments about defaulting representation equalities
- - - - -
52a4d1da by Simon Peyton Jones at 2025-11-03T08:33:05+00:00
Improve tracking of rewriter-sets
This refactor substantially improves the treatment of so-called
"rewriter-sets" in the constraint solver.
The story is described in the rewritten
Note [Wanteds rewrite Wanteds: rewriter-sets]
in GHC.Tc.Types.Constraint
Some highlights
* Trace the free coercion holes of a filled CoercionHole,
in CoercionPlusHoles. See Note [Coercion holes] (COH5)
This avoids taking having to take the free coercion variables
of a coercion when zonking a rewrriter-set
* Many knock on changes
* Make fillCoercionHole take CoercionPlusHoles as its argument
rather than to separate arguments.
* Similarly setEqIfWanted, setWantedE, wrapUnifierAndEmit.
* Be more careful about passing the correct CoHoleSet to
`rewriteEqEvidence` and friends
* Make kickOurAfterFillingCoercionHole more clever. See
new Note [Kick out after filling a coercion hole]
Smaller matters
* Rename RewriterSet to CoHoleSet
* Add special-case helper `rewriteEqEvidenceSwapOnly`
- - - - -
3e78e1ba by Simon Peyton Jones at 2025-11-03T08:33:05+00:00
Tidy up constraint solving for foralls
* In `can_eq_nc_forall` make sure to track Givens that are used
in the nested solve step.
* Tiny missing-swap bug-fix in `lookup_eq_in_qcis`
* Fix some leftover mess from
commit 14123ee646f2b9738a917b7cec30f9d3941c13de
Author: Simon Peyton Jones <simon.peytonjones(a)gmail.com>
Date: Wed Aug 20 00:35:48 2025 +0100
Solve forall-constraints via an implication, again
Specifically, trySolveImplication is now dead.
- - - - -
973f2c25 by Simon Peyton Jones at 2025-11-03T08:33:05+00:00
Do not treat CoercionHoles as free variables in coercions
This fixes a long-standing wart in the free-variable finder;
now CoercionHoles are no longer treated as a "free variable"
of a coercion.
I got big and unexpected performance regressions when making
this change. Turned out that CallArity didn't discover that
the free variable finder could be eta-expanded, which gave very
poor code.
So I re-used Note [The one-shot state monad trick] for Endo,
resulting in GHC.Utils.EndoOS. Very simple, big win.
- - - - -
c2b8a0f9 by Simon Peyton Jones at 2025-11-03T08:33:05+00:00
Update debug-tracing in CallArity
No effect on behaviour, and commented out anyway
- - - - -
9aa5ee99 by Simon Peyton Jones at 2025-11-03T08:33:28+00:00
Comments only -- remove dangling Note references
- - - - -
6683f183 by Simon Peyton Jones at 2025-11-03T08:33:28+00:00
Accept error message wibbles
- - - - -
3ba3d9f9 by Luite Stegeman at 2025-11-04T00:59:41-05:00
rts: fix eager black holes: record mutated closure and fix assertion
This fixes two problems with handling eager black holes, introduced
by a1de535f762bc23d4cf23a5b1853591dda12cdc9.
- the closure mutation must be recorded even for eager black holes,
since the mutator has mutated it before calling threadPaused
- The assertion that an unmarked eager black hole must be owned by
the TSO calling threadPaused is incorrect, since multiple threads
can race to claim the black hole.
fixes #26495
- - - - -
593e996d by Simon Peyton Jones at 2025-11-04T14:16:30+00:00
Eliminate duplicates lazily in PmAltConSet
Addresses #26514.
See Note [PmLits in PmAltConSet]
- - - - -
96 changed files:
- compiler/GHC/Core/Opt/CallArity.hs
- compiler/GHC/Core/Opt/Simplify/Iteration.hs
- compiler/GHC/Core/Opt/Simplify/Utils.hs
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/HsToCore/Pmc/Solver/Types.hs
- compiler/GHC/Iface/Tidy/StaticPtrTable.hs
- compiler/GHC/Runtime/Eval.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Instance/FunDeps.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Default.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- + compiler/GHC/Tc/Solver/FunDeps.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Irred.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Rewrite.hs
- compiler/GHC/Tc/Solver/Solve.hs
- compiler/GHC/Tc/Solver/Solve.hs-boot
- compiler/GHC/Tc/Types.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Types/Origin.hs
- compiler/GHC/Tc/Utils/Concrete.hs
- compiler/GHC/Tc/Utils/Instantiate.hs
- compiler/GHC/Tc/Utils/Monad.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Tc/Zonk/TcType.hs
- compiler/GHC/Tc/Zonk/Type.hs
- compiler/GHC/Types/Basic.hs
- compiler/GHC/Types/Unique/DSM.hs
- + compiler/GHC/Utils/EndoOS.hs
- compiler/ghc.cabal.in
- rts/ThreadPaused.c
- testsuite/tests/count-deps/CountDepsAst.stdout
- testsuite/tests/count-deps/CountDepsParser.stdout
- testsuite/tests/default/default-fail05.stderr
- testsuite/tests/dependent/should_fail/T13135_simple.stderr
- testsuite/tests/deriving/should_fail/T3621.stderr
- testsuite/tests/indexed-types/should_fail/T14369.stderr
- testsuite/tests/indexed-types/should_fail/T1897b.stderr
- testsuite/tests/linters/notes.stdout
- testsuite/tests/parser/should_fail/RecordDotSyntaxFail10.stderr
- testsuite/tests/parser/should_fail/RecordDotSyntaxFail13.stderr
- testsuite/tests/parser/should_fail/T20654a.stderr
- testsuite/tests/partial-sigs/should_fail/T14584a.stderr
- testsuite/tests/polykinds/T6068.stdout
- testsuite/tests/quantified-constraints/T15359.hs
- testsuite/tests/rep-poly/RepPolyNPlusK.stderr
- testsuite/tests/rep-poly/RepPolyRightSection.stderr
- testsuite/tests/rep-poly/T13233.stderr
- testsuite/tests/rep-poly/T19709b.stderr
- testsuite/tests/rep-poly/T23903.stderr
- testsuite/tests/typecheck/no_skolem_info/T13499.stderr
- testsuite/tests/typecheck/should_compile/T13651.hs
- − testsuite/tests/typecheck/should_compile/T13651.stderr
- + testsuite/tests/typecheck/should_compile/T14745.hs
- testsuite/tests/typecheck/should_compile/all.T
- testsuite/tests/typecheck/should_compile/hole_constraints_nested.stderr
- testsuite/tests/typecheck/should_compile/tc126.hs
- testsuite/tests/typecheck/should_fail/AmbigFDs.hs
- − testsuite/tests/typecheck/should_fail/AmbigFDs.stderr
- testsuite/tests/typecheck/should_fail/FD3.stderr
- testsuite/tests/typecheck/should_fail/FDsFromGivens2.stderr
- testsuite/tests/typecheck/should_fail/T13506.stderr
- testsuite/tests/typecheck/should_fail/T16512a.stderr
- testsuite/tests/typecheck/should_fail/T18851b.hs
- − testsuite/tests/typecheck/should_fail/T18851b.stderr
- testsuite/tests/typecheck/should_fail/T18851c.hs
- − testsuite/tests/typecheck/should_fail/T18851c.stderr
- testsuite/tests/typecheck/should_fail/T19415.stderr
- testsuite/tests/typecheck/should_fail/T19415b.stderr
- testsuite/tests/typecheck/should_fail/T22684.stderr
- + testsuite/tests/typecheck/should_fail/T23162a.hs
- + testsuite/tests/typecheck/should_fail/T23162a.stderr
- testsuite/tests/typecheck/should_fail/T25325.stderr
- testsuite/tests/typecheck/should_fail/T5246.stderr
- testsuite/tests/typecheck/should_fail/T5978.stderr
- testsuite/tests/typecheck/should_fail/T7368a.stderr
- testsuite/tests/typecheck/should_fail/T7696.stderr
- testsuite/tests/typecheck/should_fail/T8603.stderr
- testsuite/tests/typecheck/should_fail/T9612.stderr
- testsuite/tests/typecheck/should_fail/TcStaticPointersFail03.stderr
- testsuite/tests/typecheck/should_fail/all.T
- testsuite/tests/typecheck/should_fail/tcfail122.stderr
- testsuite/tests/typecheck/should_fail/tcfail143.stderr
The diff was not included because it is too large.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/6d2496466b77e72cfd6c3e8d44cea9…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/6d2496466b77e72cfd6c3e8d44cea9…
You're receiving this email because of your account on gitlab.haskell.org.
1
0
[Git][ghc/ghc][wip/T26425] 2 commits: Fix a performance hole in the occurrence analyser
by Simon Peyton Jones (@simonpj) 05 Nov '25
by Simon Peyton Jones (@simonpj) 05 Nov '25
05 Nov '25
Simon Peyton Jones pushed to branch wip/T26425 at Glasgow Haskell Compiler / GHC
Commits:
eba3bda4 by Simon Peyton Jones at 2025-11-05T08:32:37+00:00
Fix a performance hole in the occurrence analyser
As #26425 showed, the clever stuff in
Note [Occurrence analysis for join points]
does a lot of duplication of usage details. This patch
improved matters with a little fancy footwork. It is
described in the new (W5) of the same Note.
- - - - -
fd2bb45c by Simon Peyton Jones at 2025-11-05T08:34:52+00:00
Add a fast-path for args=[] to occAnalApp
In the common case of having not arguments, occAnalApp
was doing redundant work.
- - - - -
5 changed files:
- compiler/GHC/Core/Opt/OccurAnal.hs
- compiler/GHC/Core/Opt/Simplify/Iteration.hs
- compiler/GHC/Types/Unique/FM.hs
- compiler/GHC/Types/Unique/Set.hs
- compiler/GHC/Types/Var/Env.hs
Changes:
=====================================
compiler/GHC/Core/Opt/OccurAnal.hs
=====================================
@@ -664,14 +664,14 @@ through A, so it should have ManyOcc. Bear this case in mind!
* maps a OneOcc to OneOcc{ occ_n_br = 0 }
In our example, occ_join_points will be extended with
[j :-> [v :-> OneOcc{occ_n_br=0}]]
- See addJoinPoint.
+ See `addJoinPoint` and (W5) below.
* At an occurrence of a join point, we do everything as normal, but add in the
UsageDetails from the occ_join_points. See mkOneOcc.
* Crucially, at the NonRec binding of the join point, in `occAnalBind`, we use
- `orUDs`, not `andUDs` to combine the usage from the RHS with the usage from
- the body.
+ `combineJoinPointUDs`, not `andUDs` to combine the usage from the RHS with
+ the usage from the body.
Here are the consequences
@@ -688,7 +688,7 @@ Here are the consequences
These are `andUDs` together in `addOccInfo`, and hence
`v` gets ManyOccs, just as it should. Clever!
-There are a couple of tricky wrinkles
+There are, of course, some tricky wrinkles
(W1) Consider this example which shadows `j`:
join j = rhs in
@@ -718,6 +718,8 @@ There are a couple of tricky wrinkles
* In `postprcess_uds`, we add the chucked-out join points to the
returned UsageDetails, with `andUDs`.
+Wrinkles (W1) and (W2) are very similar to Note [Binder swap] (BS3).
+
(W3) Consider this example, which shadows `j`, but this time in an argument
join j = rhs
in f (case x of { K j -> ...; ... })
@@ -734,10 +736,38 @@ There are a couple of tricky wrinkles
(W4) What if the join point binding has a stable unfolding, or RULES?
They are just alternative right-hand sides, and at each call site we
- will use only one of them. So again, we can use `orUDs` to combine
- usage info from all these alternatives RHSs.
-
-Wrinkles (W1) and (W2) are very similar to Note [Binder swap] (BS3).
+ will use only one of them. So again, we can use `combineJoinPointUDs`
+ to combine usage info from all these alternatives RHSs.
+
+(W5) Other things being equal, we want keep the OccInfoEnv in the range of
+ `occ_join_points` as small as possible, because it is /duplicated/ at
+ /every occurrence/ of the join point. We really only want to include
+ OccInfo for
+ * Local, non-recursive let-bound Ids
+ * that occur just once in the RHS of the join point
+ particularly including
+ * thunks (that's the original point) and
+ * join points (so that the trick works recursively).
+ We call these the "tracked Ids of j".
+
+ Including lambda binders is pointless, and slows down the occurrence analyser.
+
+ e.g. \x. let y = x+1 in
+ join j v = ..x..y..(f z z)..
+ in ...
+ In the `occ_join_points` binding for `j`, we want to track `y`, but
+ not `x` (lambda bound) nor `z` (occurs many times).
+
+ To exploit this:
+ * `occ_local_lets` tracks which Ids are local, non-recursive lets
+ * `addJoinPoint` only populates j's entry with occ-info for the "tracked Ids"
+ of `j`; that is, that are (a) in occ_local_lets and (b) have OneOcc.
+ * `combineJoinPointUDs` uses
+ orLocalOcc for local-let Ids
+ andLocalOcc for non-local-let Ids
+
+ This fancy footwork can matter in extreme cases: it gave a 25% reduction in
+ total compiler allocation in #26425..
Note [Finding join points]
~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -759,62 +789,62 @@ rest of 'OccInfo' until it goes on the binder.
Note [Join arity prediction based on joinRhsArity]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In general, the join arity from tail occurrences of a join point (O) may be
-higher or lower than the manifest join arity of the join body (M). E.g.,
+In general, the join arity from tail occurrences of a join point (OAr) may be
+higher or lower than the manifest join arity of the join body (MAr). E.g.,
- -- M > O:
- let f x y = x + y -- M = 2
- in if b then f 1 else f 2 -- O = 1
+ -- MAr > Oar:
+ let f x y = x + y -- MAr = 2
+ in if b then f 1 else f 2 -- OAr = 1
==> { Contify for join arity 1 }
join f x = \y -> x + y
in if b then jump f 1 else jump f 2
- -- M < O
- let f = id -- M = 0
- in if ... then f 12 else f 13 -- O = 1
+ -- MAr < Oar
+ let f = id -- MAr = 0
+ in if ... then f 12 else f 13 -- OAr = 1
==> { Contify for join arity 1, eta-expand f }
join f x = id x
in if b then jump f 12 else jump f 13
-But for *recursive* let, it is crucial that both arities match up, consider
+But for *recursive* let, it is crucial MAr=OAr. Consider:
letrec f x y = if ... then f x else True
in f 42
-Here, M=2 but O=1. If we settled for a joinrec arity of 1, the recursive jump
+Here, MAr=2 but OAr=1. If we settled for a joinrec arity of 1, the recursive jump
would not happen in a tail context! Contification is invalid here.
-So indeed it is crucial to demand that M=O.
+So indeed it is crucial to demand that MAr=OAr.
-(Side note: Actually, we could be more specific: Let O1 be the join arity of
-occurrences from the letrec RHS and O2 the join arity from the let body. Then
-we need M=O1 and M<=O2 and could simply eta-expand the RHS to match O2 later.
-M=O is the specific case where we don't want to eta-expand. Neither the join
+(Side note: Actually, we could be more specific: Let OAr1 be the join arity of
+occurrences from the letrec RHS and OAr2 the join arity from the let body. Then
+we need MAr=OAr1 and MAr<=OAr2 and could simply eta-expand the RHS to match OAr2 later.
+MAr=OAr is the specific case where we don't want to eta-expand. Neither the join
points paper nor GHC does this at the moment.)
We can capitalise on this observation and conclude that *if* f could become a
-joinrec (without eta-expansion), it will have join arity M.
-Now, M is just the result of 'joinRhsArity', a rather simple, local analysis.
+joinrec (without eta-expansion), it will have join arity MAr.
+Now, MAr is just the result of 'joinRhsArity', a rather simple, local analysis.
It is also the join arity inside the 'TailUsageDetails' returned by
'occAnalLamTail', so we can predict join arity without doing any fixed-point
iteration or really doing any deep traversal of let body or RHS at all.
-We check for M in the 'adjustTailUsage' call inside 'tagRecBinders'.
+We check for MAr in the 'adjustTailUsage' call inside 'tagRecBinders'.
All this is quite apparent if you look at the contification transformation in
Fig. 5 of "Compiling without Continuations" (which does not account for
eta-expansion at all, mind you). The letrec case looks like this
-
+n
letrec f = /\as.\xs. L[us] in L'[es]
... and a bunch of conditions establishing that f only occurs
in app heads of join arity (len as + len xs) inside us and es ...
-The syntactic form `/\as.\xs. L[us]` forces M=O iff `f` occurs in `us`. However,
+The syntactic form `/\as.\xs. L[us]` forces MAr=OAr iff `f` occurs in `us`. However,
for non-recursive functions, this is the definition of contification from the
paper:
let f = /\as.\xs.u in L[es] ... conditions ...
-Note that u could be a lambda itself, as we have seen. No relationship between M
-and O to exploit here.
+Note that u could be a lambda itself, as we have seen. No relationship between MAr
+and OAr to exploit here.
Note [Join points and unfoldings/rules]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -992,23 +1022,29 @@ occAnalBind !env lvl ire (NonRec bndr rhs) thing_inside combine
= -- Analyse the RHS and /then/ the body
let -- Analyse the rhs first, generating rhs_uds
!(rhs_uds_s, bndr', rhs') = occAnalNonRecRhs env lvl ire mb_join bndr rhs
- rhs_uds = foldl1' orUDs rhs_uds_s -- NB: orUDs. See (W4) of
- -- Note [Occurrence analysis for join points]
+ rhs_uds = foldl1' (combineJoinPointUDs env)
+ rhs_uds_s -- NB: combineJoinPointUDs. See (W4) of
+ -- Note [Occurrence analysis for join points]
-- Now analyse the body, adding the join point
-- into the environment with addJoinPoint
- !(WUD body_uds (occ, body)) = occAnalNonRecBody env bndr' $ \env ->
+ env_body = addLocalLet env lvl bndr
+ !(WUD body_uds (occ, body)) = occAnalNonRecBody env_body bndr' $ \env ->
thing_inside (addJoinPoint env bndr' rhs_uds)
in
if isDeadOcc occ -- Drop dead code; see Note [Dead code]
then WUD body_uds body
- else WUD (rhs_uds `orUDs` body_uds) -- Note `orUDs`
+ else -- pprTrace "occAnal-nonrec" (vcat [ ppr bndr <+> ppr occ
+ -- , text "rhs_uds" <+> ppr rhs_uds
+ -- , text "body_uds" <+> ppr body_uds ]) $
+ WUD (combineJoinPointUDs env rhs_uds body_uds) -- Note `orUDs`
(combine [NonRec (fst (tagNonRecBinder lvl occ bndr')) rhs']
body)
-- The normal case, including newly-discovered join points
-- Analyse the body and /then/ the RHS
- | WUD body_uds (occ,body) <- occAnalNonRecBody env bndr thing_inside
+ | let env_body = addLocalLet env lvl bndr
+ , WUD body_uds (occ,body) <- occAnalNonRecBody env_body bndr thing_inside
= if isDeadOcc occ -- Drop dead code; see Note [Dead code]
then WUD body_uds body
else let
@@ -1054,7 +1090,7 @@ occAnalNonRecRhs !env lvl imp_rule_edges mb_join bndr rhs
rhs_ctxt = mkNonRecRhsCtxt lvl bndr unf
-- See Note [Join arity prediction based on joinRhsArity]
- -- Match join arity O from mb_join_arity with manifest join arity M as
+ -- Match join arity OAr from mb_join_arity with manifest join arity MAr as
-- returned by of occAnalLamTail. It's totally OK for them to mismatch;
-- hence adjust the UDs from the RHS
@@ -1764,7 +1800,7 @@ makeNode !env imp_rule_edges bndr_set (bndr, rhs)
-- here because that is what we are setting!
WTUD unf_tuds unf' = occAnalUnfolding rhs_env unf
adj_unf_uds = adjustTailArity (JoinPoint rhs_ja) unf_tuds
- -- `rhs_ja` is `joinRhsArity rhs` and is the prediction for source M
+ -- `rhs_ja` is `joinRhsArity rhs` and is the prediction for source MAr
-- of Note [Join arity prediction based on joinRhsArity]
--------- IMP-RULES --------
@@ -1775,7 +1811,7 @@ makeNode !env imp_rule_edges bndr_set (bndr, rhs)
--------- All rules --------
-- See Note [Join points and unfoldings/rules]
- -- `rhs_ja` is `joinRhsArity rhs'` and is the prediction for source M
+ -- `rhs_ja` is `joinRhsArity rhs'` and is the prediction for source MAr
-- of Note [Join arity prediction based on joinRhsArity]
rules_w_uds :: [(CoreRule, UsageDetails, UsageDetails)]
rules_w_uds = [ (r,l,adjustTailArity (JoinPoint rhs_ja) rhs_wuds)
@@ -2177,7 +2213,9 @@ occAnalLamTail :: OccEnv -> CoreExpr -> WithTailUsageDetails CoreExpr
-- See Note [Adjusting right-hand sides]
occAnalLamTail env expr
= let !(WUD usage expr') = occ_anal_lam_tail env expr
- in WTUD (TUD (joinRhsArity expr) usage) expr'
+ in WTUD (TUD (joinRhsArity expr') usage) expr'
+ -- If expr looks like (\x. let dead = e in \y. blah), where `dead` is dead
+ -- then joinRhsArity expr' might exceed joinRhsArity expr
occ_anal_lam_tail :: OccEnv -> CoreExpr -> WithUsageDetails CoreExpr
-- Does not markInsideLam etc for the outmost batch of lambdas
@@ -2598,7 +2636,7 @@ occAnalArgs :: OccEnv -> CoreExpr -> [CoreExpr]
-> WithUsageDetails CoreExpr
-- The `fun` argument is just an accumulating parameter,
-- the base for building the application we return
-occAnalArgs !env fun args !one_shots
+occAnalArgs env fun args one_shots
= go emptyDetails fun args one_shots
where
env_args = setNonTailCtxt encl env
@@ -2657,8 +2695,19 @@ Constructors are rather like lambdas in this way.
occAnalApp :: OccEnv
-> (Expr CoreBndr, [Arg CoreBndr], [CoreTickish])
-> WithUsageDetails (Expr CoreBndr)
--- Naked variables (not applied) end up here too
-occAnalApp !env (Var fun, args, ticks)
+occAnalApp !env (Var fun_id, [], ticks)
+ = -- Naked variables (not applied) end up here too, and it's worth giving
+ -- this common case special treatment, because there is so much less to do.
+ -- This is just a specialised copy of the (Var fun_id) case below
+ WUD fun_uds (mkTicks ticks fun')
+ where
+ !(fun', fun_id') = lookupBndrSwap env fun_id
+ !fun_uds = mkOneOcc env fun_id' int_cxt 0
+ !int_cxt = case occ_encl env of
+ OccScrut -> IsInteresting
+ _other -> NotInteresting
+
+occAnalApp env (Var fun, args, ticks)
-- Account for join arity of runRW# continuation
-- See Note [Simplification of runRW#]
--
@@ -2863,7 +2912,11 @@ data OccEnv
-- Invariant: no Id maps to an empty OccInfoEnv
-- See Note [Occurrence analysis for join points]
, occ_join_points :: !JoinPointInfo
- }
+
+ , occ_local_lets :: IdSet -- Non-top-level non-rec-bound lets
+ -- I tried making this field strict, but
+ -- doing so slightly increased allocation
+ }
type JoinPointInfo = IdEnv OccInfoEnv
@@ -2914,7 +2967,8 @@ initOccEnv
, occ_join_points = emptyVarEnv
, occ_bs_env = emptyVarEnv
- , occ_bs_rng = emptyVarSet }
+ , occ_bs_rng = emptyVarSet
+ , occ_local_lets = emptyVarSet }
noBinderSwaps :: OccEnv -> Bool
noBinderSwaps (OccEnv { occ_bs_env = bs_env }) = isEmptyVarEnv bs_env
@@ -3154,23 +3208,26 @@ postprocess_uds bndrs bad_joins uds
| uniq `elemVarEnvByKey` env = plusVarEnv_C andLocalOcc env join_env
| otherwise = env
+addLocalLet :: OccEnv -> TopLevelFlag -> Id -> OccEnv
+addLocalLet env@(OccEnv { occ_local_lets = ids }) top_lvl id
+ | isTopLevel top_lvl = env
+ | otherwise = env { occ_local_lets = ids `extendVarSet` id }
+
addJoinPoint :: OccEnv -> Id -> UsageDetails -> OccEnv
-addJoinPoint env bndr rhs_uds
+addJoinPoint env@(OccEnv { occ_join_points = join_points, occ_local_lets = local_lets })
+ join_bndr (UD { ud_env = rhs_occs })
| isEmptyVarEnv zeroed_form
= env
| otherwise
- = env { occ_join_points = extendVarEnv (occ_join_points env) bndr zeroed_form }
+ = env { occ_join_points = extendVarEnv join_points join_bndr zeroed_form }
where
- zeroed_form = mkZeroedForm rhs_uds
+ zeroed_form = mapMaybeUniqSetToUFM do_one local_lets
+ -- See Note [Occurrence analysis for join points] for "zeroed form"
-mkZeroedForm :: UsageDetails -> OccInfoEnv
--- See Note [Occurrence analysis for join points] for "zeroed form"
-mkZeroedForm (UD { ud_env = rhs_occs })
- = mapMaybeUFM do_one rhs_occs
- where
- do_one :: LocalOcc -> Maybe LocalOcc
- do_one (ManyOccL {}) = Nothing
- do_one occ@(OneOccL {}) = Just (occ { lo_n_br = 0 })
+ do_one :: Var -> Maybe LocalOcc
+ do_one bndr = case lookupVarEnv rhs_occs bndr of
+ Just occ@(OneOccL {}) -> Just (occ { lo_n_br = 0 })
+ _ -> Nothing
--------------------
transClosureFV :: VarEnv VarSet -> VarEnv VarSet
@@ -3628,7 +3685,12 @@ data LocalOcc -- See Note [LocalOcc]
-- Combining (AlwaysTailCalled 2) and (AlwaysTailCalled 3)
-- gives NoTailCallInfo
, lo_int_cxt :: !InterestingCxt }
+
| ManyOccL !TailCallInfo
+ -- Why do we need TailCallInfo on ManyOccL?
+ -- Answer: recursive bindings are entered many times:
+ -- rec { j x = ...j x'... } in j y
+ -- See the uses of `andUDs` in `tagRecBinders`
instance Outputable LocalOcc where
ppr (OneOccL { lo_n_br = n, lo_tail = tci })
@@ -3663,7 +3725,7 @@ instance Outputable UsageDetails where
-- | TailUsageDetails captures the result of applying 'occAnalLamTail'
-- to a function `\xyz.body`. The TailUsageDetails pairs together
-- * the number of lambdas (including type lambdas: a JoinArity)
--- * UsageDetails for the `body` of the lambda, unadjusted by `adjustTailUsage`.
+-- * UsageDetails for the `body` of the lambda, /unadjusted/ by `adjustTailUsage`.
-- If the binding turns out to be a join point with the indicated join
-- arity, this unadjusted usage details is just what we need; otherwise we
-- need to discard tail calls. That's what `adjustTailUsage` does.
@@ -3681,8 +3743,17 @@ data WithTailUsageDetails a = WTUD !TailUsageDetails !a
andUDs:: UsageDetails -> UsageDetails -> UsageDetails
orUDs :: UsageDetails -> UsageDetails -> UsageDetails
-andUDs = combineUsageDetailsWith andLocalOcc
-orUDs = combineUsageDetailsWith orLocalOcc
+andUDs = combineUsageDetailsWith (\_uniq -> andLocalOcc)
+orUDs = combineUsageDetailsWith (\_uniq -> orLocalOcc)
+
+combineJoinPointUDs :: OccEnv -> UsageDetails -> UsageDetails -> UsageDetails
+-- See (W5) in Note [Occurrence analysis for join points]
+combineJoinPointUDs (OccEnv { occ_local_lets = local_lets }) uds1 uds2
+ = combineUsageDetailsWith combine uds1 uds2
+ where
+ combine uniq occ1 occ2
+ | uniq `elemVarSetByKey` local_lets = orLocalOcc occ1 occ2
+ | otherwise = andLocalOcc occ1 occ2
mkOneOcc :: OccEnv -> Id -> InterestingCxt -> JoinArity -> UsageDetails
mkOneOcc !env id int_cxt arity
@@ -3699,7 +3770,8 @@ mkOneOcc !env id int_cxt arity
= mkSimpleDetails (unitVarEnv id occ)
where
- occ = OneOccL { lo_n_br = 1, lo_int_cxt = int_cxt
+ occ = OneOccL { lo_n_br = 1
+ , lo_int_cxt = int_cxt
, lo_tail = AlwaysTailCalled arity }
-- Add several occurrences, assumed not to be tail calls
@@ -3786,7 +3858,7 @@ restrictFreeVars bndrs fvs = restrictUniqSetToUFM bndrs fvs
-------------------
-- Auxiliary functions for UsageDetails implementation
-combineUsageDetailsWith :: (LocalOcc -> LocalOcc -> LocalOcc)
+combineUsageDetailsWith :: (Unique -> LocalOcc -> LocalOcc -> LocalOcc)
-> UsageDetails -> UsageDetails -> UsageDetails
{-# INLINE combineUsageDetailsWith #-}
combineUsageDetailsWith plus_occ_info
@@ -3796,9 +3868,9 @@ combineUsageDetailsWith plus_occ_info
| isEmptyVarEnv env2 = uds1
| otherwise
-- See Note [Strictness in the occurrence analyser]
- -- Using strictPlusVarEnv here speeds up the test T26425 by about 10% by avoiding
- -- intermediate thunks.
- = UD { ud_env = strictPlusVarEnv_C plus_occ_info env1 env2
+ -- Using strictPlusVarEnv here speeds up the test T26425
+ -- by about 10% by avoiding intermediate thunks.
+ = UD { ud_env = strictPlusVarEnv_C_Directly plus_occ_info env1 env2
, ud_z_many = strictPlusVarEnv z_many1 z_many2
, ud_z_in_lam = plusVarEnv z_in_lam1 z_in_lam2
, ud_z_tail = strictPlusVarEnv z_tail1 z_tail2 }
@@ -3842,8 +3914,6 @@ lookupOccInfoByUnique (UD { ud_env = env
| uniq `elemVarEnvByKey` z_tail = NoTailCallInfo
| otherwise = ti
-
-
-------------------
-- See Note [Adjusting right-hand sides]
@@ -3853,21 +3923,22 @@ adjustNonRecRhs :: JoinPointHood
-- ^ This function concentrates shared logic between occAnalNonRecBind and the
-- AcyclicSCC case of occAnalRec.
-- It returns the adjusted rhs UsageDetails combined with the body usage
-adjustNonRecRhs mb_join_arity rhs_wuds@(WTUD _ rhs)
- = WUD (adjustTailUsage mb_join_arity rhs_wuds) rhs
-
+adjustNonRecRhs mb_join_arity (WTUD (TUD rhs_ja uds) rhs)
+ = WUD (adjustTailUsage exact_join rhs uds) rhs
+ where
+ exact_join = mb_join_arity == JoinPoint rhs_ja
-adjustTailUsage :: JoinPointHood
- -> WithTailUsageDetails CoreExpr -- Rhs usage, AFTER occAnalLamTail
+adjustTailUsage :: Bool -- True <=> Exactly-matching join point; don't do markNonTail
+ -> CoreExpr -- Rhs usage, AFTER occAnalLamTail
-> UsageDetails
-adjustTailUsage mb_join_arity (WTUD (TUD rhs_ja uds) rhs)
+ -> UsageDetails
+adjustTailUsage exact_join rhs uds
= -- c.f. occAnal (Lam {})
markAllInsideLamIf (not one_shot) $
markAllNonTailIf (not exact_join) $
uds
where
one_shot = isOneShotFun rhs
- exact_join = mb_join_arity == JoinPoint rhs_ja
adjustTailArity :: JoinPointHood -> TailUsageDetails -> UsageDetails
adjustTailArity mb_rhs_ja (TUD ja usage)
@@ -3914,8 +3985,9 @@ tagNonRecBinder lvl occ bndr
tagRecBinders :: TopLevelFlag -- At top level?
-> UsageDetails -- Of body of let ONLY
-> [NodeDetails]
- -> WithUsageDetails -- Adjusted details for whole scope,
- -- with binders removed
+ -> WithUsageDetails -- Adjusted details for whole scope
+ -- still including the binders;
+ -- (they are removed by `addInScope`)
[IdWithOccInfo] -- Tagged binders
-- Substantially more complicated than non-recursive case. Need to adjust RHS
-- details *before* tagging binders (because the tags depend on the RHSes).
@@ -3925,32 +3997,21 @@ tagRecBinders lvl body_uds details_s
-- 1. See Note [Join arity prediction based on joinRhsArity]
-- Determine possible join-point-hood of whole group, by testing for
- -- manifest join arity M.
- -- This (re-)asserts that makeNode had made tuds for that same arity M!
+ -- manifest join arity MAr.
+ -- This (re-)asserts that makeNode had made tuds for that same arity MAr!
unadj_uds = foldr (andUDs . test_manifest_arity) body_uds details_s
- test_manifest_arity ND{nd_rhs = WTUD tuds rhs}
- = adjustTailArity (JoinPoint (joinRhsArity rhs)) tuds
+ test_manifest_arity ND{nd_rhs = WTUD (TUD rhs_ja uds) rhs}
+ = assertPpr (rhs_ja == joinRhsArity rhs) (ppr rhs_ja $$ ppr uds $$ ppr rhs) $
+ uds
+ will_be_joins :: Bool
will_be_joins = decideRecJoinPointHood lvl unadj_uds bndrs
- mb_join_arity :: Id -> JoinPointHood
- -- mb_join_arity: See Note [Join arity prediction based on joinRhsArity]
- -- This is the source O
- mb_join_arity bndr
- -- Can't use willBeJoinId_maybe here because we haven't tagged
- -- the binder yet (the tag depends on these adjustments!)
- | will_be_joins
- , AlwaysTailCalled arity <- lookupTailCallInfo unadj_uds bndr
- = JoinPoint arity
- | otherwise
- = assert (not will_be_joins) -- Should be AlwaysTailCalled if
- NotJoinPoint -- we are making join points!
-
-- 2. Adjust usage details of each RHS, taking into account the
-- join-point-hood decision
- rhs_udss' = [ adjustTailUsage (mb_join_arity bndr) rhs_wuds
+ rhs_udss' = [ adjustTailUsage will_be_joins rhs rhs_uds
-- Matching occAnalLamTail in makeNode
- | ND { nd_bndr = bndr, nd_rhs = rhs_wuds } <- details_s ]
+ | ND { nd_rhs = WTUD (TUD _ rhs_uds) rhs } <- details_s ]
-- 3. Compute final usage details from adjusted RHS details
adj_uds = foldr andUDs body_uds rhs_udss'
@@ -3969,9 +4030,9 @@ setBinderOcc occ_info bndr
| otherwise = setIdOccInfo bndr occ_info
-- | Decide whether some bindings should be made into join points or not, based
--- on its occurrences. This is
+-- on its occurrences.
-- Returns `False` if they can't be join points. Note that it's an
--- all-or-nothing decision, as if multiple binders are given, they're
+-- all-or-nothing decision: if multiple binders are given, they are
-- assumed to be mutually recursive.
--
-- It must, however, be a final decision. If we say `True` for 'f',
=====================================
compiler/GHC/Core/Opt/Simplify/Iteration.hs
=====================================
@@ -4595,13 +4595,21 @@ mkLetUnfolding :: SimplEnv -> TopLevelFlag -> UnfoldingSource
-> InId -> Bool -- True <=> this is a join point
-> OutExpr -> SimplM Unfolding
mkLetUnfolding env top_lvl src id is_join new_rhs
- = return (mkUnfolding uf_opts src is_top_lvl is_bottoming is_join new_rhs Nothing)
- -- We make an unfolding *even for loop-breakers*.
- -- Reason: (a) It might be useful to know that they are WHNF
- -- (b) In GHC.Iface.Tidy we currently assume that, if we want to
- -- expose the unfolding then indeed we *have* an unfolding
- -- to expose. (We could instead use the RHS, but currently
- -- we don't.) The simple thing is always to have one.
+-- | is_join
+-- , UnfNever <- guidance
+-- = -- For large join points, don't keep an unfolding at all if it is large
+-- -- This is just an attempt to keep residency under control in
+-- -- deeply-nested join-point such as those arising in #26425
+-- return NoUnfolding
+
+ | otherwise
+ = return (mkCoreUnfolding src is_top_lvl new_rhs Nothing guidance)
+ -- We make an unfolding *even for loop-breakers*.
+ -- Reason: (a) It might be useful to know that they are WHNF
+ -- (b) In GHC.Iface.Tidy we currently assume that, if we want to
+ -- expose the unfolding then indeed we *have* an unfolding
+ -- to expose. (We could instead use the RHS, but currently
+ -- we don't.) The simple thing is always to have one.
where
-- !opts: otherwise, we end up retaining all the SimpleEnv
!uf_opts = seUnfoldingOpts env
@@ -4612,6 +4620,9 @@ mkLetUnfolding env top_lvl src id is_join new_rhs
-- See Note [Force bottoming field]
!is_bottoming = isDeadEndId id
+ is_top_bottoming = is_top_lvl && is_bottoming
+ guidance = calcUnfoldingGuidance uf_opts is_top_bottoming is_join new_rhs
+
-------------------
simplStableUnfolding :: SimplEnv -> BindContext
-> InId
=====================================
compiler/GHC/Types/Unique/FM.hs
=====================================
@@ -53,7 +53,7 @@ module GHC.Types.Unique.FM (
plusUFM,
strictPlusUFM,
plusUFM_C,
- strictPlusUFM_C,
+ strictPlusUFM_C, strictPlusUFM_C_Directly,
plusUFM_CD,
plusUFM_CD2,
mergeUFM,
@@ -281,6 +281,9 @@ plusUFM_C f (UFM x) (UFM y) = UFM (M.unionWith f x y)
strictPlusUFM_C :: (elt -> elt -> elt) -> UniqFM key elt -> UniqFM key elt -> UniqFM key elt
strictPlusUFM_C f (UFM x) (UFM y) = UFM (MS.unionWith f x y)
+strictPlusUFM_C_Directly :: (Unique -> elt -> elt -> elt) -> UniqFM key elt -> UniqFM key elt -> UniqFM key elt
+strictPlusUFM_C_Directly f (UFM x) (UFM y) = UFM (MS.unionWithKey (f . mkUniqueGrimily) x y)
+
-- | `plusUFM_CD f m1 d1 m2 d2` merges the maps using `f` as the
-- combinding function and `d1` resp. `d2` as the default value if
-- there is no entry in `m1` reps. `m2`. The domain is the union of
=====================================
compiler/GHC/Types/Unique/Set.hs
=====================================
@@ -40,6 +40,7 @@ module GHC.Types.Unique.Set (
lookupUniqSet_Directly,
partitionUniqSet,
mapUniqSet,
+ mapUniqSetToUFM, mapMaybeUniqSetToUFM,
unsafeUFMToUniqSet,
nonDetEltsUniqSet,
nonDetKeysUniqSet,
@@ -211,6 +212,14 @@ mapUniqSet f = mkUniqSet . map f . nonDetEltsUniqSet
mapMaybeUniqSet_sameUnique :: (a -> Maybe b) -> UniqSet a -> UniqSet b
mapMaybeUniqSet_sameUnique f (UniqSet a) = UniqSet $ mapMaybeUFM_sameUnique f a
+mapUniqSetToUFM :: (a -> b) -> UniqSet a -> UniqFM a b
+-- Same keys, new values
+mapUniqSetToUFM f (UniqSet ufm) = mapUFM f ufm
+
+mapMaybeUniqSetToUFM :: (a -> Maybe b) -> UniqSet a -> UniqFM a b
+-- Same keys, new values
+mapMaybeUniqSetToUFM f (UniqSet ufm) = mapMaybeUFM f ufm
+
-- Two 'UniqSet's are considered equal if they contain the same
-- uniques.
instance Eq (UniqSet a) where
=====================================
compiler/GHC/Types/Var/Env.hs
=====================================
@@ -12,7 +12,8 @@ module GHC.Types.Var.Env (
elemVarEnv, disjointVarEnv, anyVarEnv,
extendVarEnv, extendVarEnv_C, extendVarEnv_Acc,
extendVarEnvList,
- strictPlusVarEnv, plusVarEnv, plusVarEnv_C, strictPlusVarEnv_C,
+ strictPlusVarEnv, plusVarEnv, plusVarEnv_C,
+ strictPlusVarEnv_C, strictPlusVarEnv_C_Directly,
plusVarEnv_CD, plusMaybeVarEnv_C,
plusVarEnvList, alterVarEnv,
delVarEnvList, delVarEnv,
@@ -525,6 +526,7 @@ delVarEnv :: VarEnv a -> Var -> VarEnv a
minusVarEnv :: VarEnv a -> VarEnv b -> VarEnv a
plusVarEnv_C :: (a -> a -> a) -> VarEnv a -> VarEnv a -> VarEnv a
strictPlusVarEnv_C :: (a -> a -> a) -> VarEnv a -> VarEnv a -> VarEnv a
+strictPlusVarEnv_C_Directly :: (Unique -> a -> a -> a) -> VarEnv a -> VarEnv a -> VarEnv a
plusVarEnv_CD :: (a -> a -> a) -> VarEnv a -> a -> VarEnv a -> a -> VarEnv a
plusMaybeVarEnv_C :: (a -> a -> Maybe a) -> VarEnv a -> VarEnv a -> VarEnv a
mapVarEnv :: (a -> b) -> VarEnv a -> VarEnv b
@@ -552,6 +554,7 @@ extendVarEnv_Acc = addToUFM_Acc
extendVarEnvList = addListToUFM
plusVarEnv_C = plusUFM_C
strictPlusVarEnv_C = strictPlusUFM_C
+strictPlusVarEnv_C_Directly = strictPlusUFM_C_Directly
plusVarEnv_CD = plusUFM_CD
plusMaybeVarEnv_C = plusMaybeUFM_C
delVarEnvList = delListFromUFM
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ec080d05d53af029018ee11db9aeab…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ec080d05d53af029018ee11db9aeab…
You're receiving this email because of your account on gitlab.haskell.org.
1
0
Simon Peyton Jones pushed new branch wip/T26548 at Glasgow Haskell Compiler / GHC
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/T26548
You're receiving this email because of your account on gitlab.haskell.org.
1
0
Zubin pushed to branch wip/inline-fs at Glasgow Haskell Compiler / GHC
Commits:
5fb45025 by Zubin Duggal at 2025-11-05T12:58:44+05:30
wip
- - - - -
1 changed file:
- compiler/GHC/Data/FastString.hs
Changes:
=====================================
compiler/GHC/Data/FastString.hs
=====================================
@@ -214,6 +214,11 @@ data FastStringPayload = FastString {
data FastString = FastStringId {-# UNPACK #-} !Word64
+-- first 5 bits set: inlined faststring
+-- next 3 bits: length
+-- next 7 bytes: unpacked BS
+--
+
fs_sbs :: FastString -> ShortByteString
fs_sbs (FastStringId w)
| w .&. 0xf8000000_00000000 == 0xf8000000_00000000
@@ -230,7 +235,8 @@ fs_sbs (FastStringId w)
5 -> SBS.pack [ w8_64 (w `uncheckedShiftRL64#` 32#), w8_64 (w `uncheckedShiftRL64#` 24#), w8_64 (w `uncheckedShiftRL64#` 16#), w8_64 (w `uncheckedShiftRL64#` 8#), w8_64 w)]
6 -> SBS.pack [ w8_64 (w `uncheckedShiftRL64#` 40#), w8_64 (w `uncheckedShiftRL64#` 32#), w8_64 (w `uncheckedShiftRL64#` 24#), w8_64 (w `uncheckedShiftRL64#` 16#), w8_64 (w `uncheckedShiftRL64#` 8#), w8_64 w)]
7 -> SBS.pack [ w8_64 (w `uncheckedShiftRL64#` 48#), w8_64 (w `uncheckedShiftRL64#` 40#), w8_64 (w `uncheckedShiftRL64#` 32#), w8_64 (w `uncheckedShiftRL64#` 24#), w8_64 (w `uncheckedShiftRL64#` 16#), w8_64 (w `uncheckedShiftRL64#` 8#), w8_64 w)]
- | otherwise
+ | otherwise =
+
n_chars :: FastString -> Int
uniq :: FastString -> Int
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5fb45025d1233d90db0b6102e4434fb…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5fb45025d1233d90db0b6102e4434fb…
You're receiving this email because of your account on gitlab.haskell.org.
1
0
Zubin pushed new branch wip/inline-fs at Glasgow Haskell Compiler / GHC
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/inline-fs
You're receiving this email because of your account on gitlab.haskell.org.
1
0
[Git][ghc/ghc][ghc-9.14] level imports: Fix infinite loop with cyclic module imports
by Zubin (@wz1000) 05 Nov '25
by Zubin (@wz1000) 05 Nov '25
05 Nov '25
Zubin pushed to branch ghc-9.14 at Glasgow Haskell Compiler / GHC
Commits:
0e08b9ae by Matthew Pickering at 2025-11-04T20:56:40+05:30
level imports: Fix infinite loop with cyclic module imports
I didn't anticipate that downsweep would run before we checked for
cyclic imports. Therefore we need to use the reachability function which
handles cyclic graphs.
Fixes #26087
(cherry picked from commit 8b731e3c900291655a767123bcda55eddd63920c)
- - - - -
5 changed files:
- compiler/GHC/Unit/Module/Graph.hs
- + testsuite/tests/splice-imports/T26087.stderr
- + testsuite/tests/splice-imports/T26087A.hs
- + testsuite/tests/splice-imports/T26087B.hs
- testsuite/tests/splice-imports/all.T
Changes:
=====================================
compiler/GHC/Unit/Module/Graph.hs
=====================================
@@ -866,7 +866,7 @@ mkTransZeroDeps = first graphReachability {- module graph is acyclic -} . module
-- | Transitive dependencies, but with the stage that each module is required at.
mkStageDeps :: [ModuleGraphNode] -> (ReachabilityIndex StageSummaryNode, (NodeKey, ModuleStage) -> Maybe StageSummaryNode)
-mkStageDeps = first graphReachability . moduleGraphNodesStages
+mkStageDeps = first cyclicGraphReachability . moduleGraphNodesStages
type ZeroSummaryNode = Node Int ZeroScopeKey
=====================================
testsuite/tests/splice-imports/T26087.stderr
=====================================
@@ -0,0 +1,6 @@
+./T26087B.hs: error: [GHC-92213]
+ Module graph contains a cycle:
+ module ‘main:T26087B’ (./T26087B.hs)
+ imports module ‘main:T26087A’ (T26087A.hs)
+ which imports module ‘main:T26087B’ (./T26087B.hs)
+
=====================================
testsuite/tests/splice-imports/T26087A.hs
=====================================
@@ -0,0 +1,4 @@
+{-# LANGUAGE ExplicitLevelImports #-}
+module T26087A where
+
+import quote T26087B
=====================================
testsuite/tests/splice-imports/T26087B.hs
=====================================
@@ -0,0 +1,4 @@
+{-# LANGUAGE ExplicitLevelImports, TemplateHaskell #-}
+module T26087B where
+
+import T26087A
=====================================
testsuite/tests/splice-imports/all.T
=====================================
@@ -46,7 +46,4 @@ test('SI35',
compile_and_run,
['-package ghc'])
test('SI36', [extra_files(["SI36_A.hs", "SI36_B1.hs", "SI36_B2.hs", "SI36_B3.hs", "SI36_C1.hs", "SI36_C2.hs", "SI36_C3.hs"])], multimod_compile_fail, ['SI36', '-v0'])
-test('T26090', [], multimod_compile_fail, ['T26090', '-v0'])
-test('ModuleExport', [], multimod_compile_fail, ['ModuleExport', '-v0'])
-test('LevelImportExports', [], makefile_test, [])
-test('DodgyLevelExport', [], multimod_compile, ['DodgyLevelExport', '-v0 -Wdodgy-exports'])
+test('T26087', [], multimod_compile_fail, ['T26087A', ''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0e08b9aee6ce58fe7099f14ac1d7dea…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0e08b9aee6ce58fe7099f14ac1d7dea…
You're receiving this email because of your account on gitlab.haskell.org.
1
0
[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 7 commits: rts: fix eager black holes: record mutated closure and fix assertion
by Marge Bot (@marge-bot) 04 Nov '25
by Marge Bot (@marge-bot) 04 Nov '25
04 Nov '25
Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC
Commits:
3ba3d9f9 by Luite Stegeman at 2025-11-04T00:59:41-05:00
rts: fix eager black holes: record mutated closure and fix assertion
This fixes two problems with handling eager black holes, introduced
by a1de535f762bc23d4cf23a5b1853591dda12cdc9.
- the closure mutation must be recorded even for eager black holes,
since the mutator has mutated it before calling threadPaused
- The assertion that an unmarked eager black hole must be owned by
the TSO calling threadPaused is incorrect, since multiple threads
can race to claim the black hole.
fixes #26495
- - - - -
b5508f2c by Rodrigo Mesquita at 2025-11-04T14:10:56+00:00
build: Relax ghc/ghc-boot Cabal bound to 3.16
Fixes #26202
- - - - -
c5b3541f by Rodrigo Mesquita at 2025-11-04T14:10:56+00:00
cabal-reinstall: Use haddock-api +in-tree-ghc
Fixes #26202
- - - - -
c6d4b945 by Rodrigo Mesquita at 2025-11-04T14:10:56+00:00
cabal-reinstall: Pass --strict to Happy
This is necessary to make the generated Parser build successfully
This mimics Hadrian, which always passes --strict to happy.
Fixes #26202
- - - - -
79df1e0e by Rodrigo Mesquita at 2025-11-04T14:10:56+00:00
genprimopcode: Require higher happy version
I've bumped the happy version to forbid deprecated Happy versions which
don't successfully compile.
- - - - -
9cbfc2ce by Simon Peyton Jones at 2025-11-04T23:24:30-05:00
Add a HsWrapper optimiser
This MR addresses #26349, by introduceing optSubTypeHsWrapper.
There is a long
Note [Deep subsumption and WpSubType]
in GHC.Tc.Types.Evidence that explains what is going on.
- - - - -
4098947b by Simon Peyton Jones at 2025-11-04T23:24:30-05:00
Improve mkWpFun_FRR
This commit ensures that `mkWpFun_FRR` directly produces a `FunCo` in
the cases where it can.
(Previously called `mkWpFun` which in turn optimised to a `FunCo`, but
that made the smarts in `mkWpFun` /essential/ rather than (as they
should be) optional.
- - - - -
24 changed files:
- cabal.project-reinstall
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Hs/Syn/Type.hs
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/HsToCore/Match.hs
- compiler/GHC/Iface/Ext/Ast.hs
- compiler/GHC/Tc/Errors/Hole.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Head.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Utils/Concrete.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Tc/Zonk/Type.hs
- compiler/Setup.hs
- compiler/ghc.cabal.in
- libraries/ghc-boot/Setup.hs
- libraries/ghc-boot/ghc-boot.cabal.in
- rts/ThreadPaused.c
- + testsuite/tests/simplCore/should_compile/T26349.hs
- + testsuite/tests/simplCore/should_compile/T26349.stderr
- testsuite/tests/simplCore/should_compile/all.T
- testsuite/tests/simplCore/should_compile/rule2.stderr
- utils/genprimopcode/genprimopcode.cabal
Changes:
=====================================
cabal.project-reinstall
=====================================
@@ -59,6 +59,7 @@ constraints: ghc +internal-interpreter +dynamic-system-linke,
ghc-bin +internal-interpreter +threaded,
ghci +internal-interpreter,
haddock +in-ghc-tree,
+ haddock-api +in-ghc-tree,
any.array installed,
any.base installed,
any.deepseq installed,
@@ -68,6 +69,8 @@ constraints: ghc +internal-interpreter +dynamic-system-linke,
any.pretty installed,
any.template-haskell installed
+package *
+ happy-options: --strict
benchmarks: False
tests: False
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -41,7 +41,8 @@ module GHC.Core.Coercion (
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo,
mkFunCo, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
mkNakedFunCo,
- mkNakedForAllCo, mkForAllCo, mkForAllVisCos, mkHomoForAllCos,
+ mkNakedForAllCo, mkForAllCo, mkForAllVisCos,
+ mkHomoForAllCo, mkHomoForAllCos,
mkPhantomCo, mkAxiomCo,
mkHoleCo, mkUnivCo, mkSubCo,
mkProofIrrelCo,
@@ -980,7 +981,7 @@ mkForAllCo v visL visR kind_co co
= mkReflCo r (mkTyCoForAllTy v visL ty)
| otherwise
- = mkForAllCo_NoRefl v visL visR kind_co co
+ = mk_forall_co v visL visR kind_co co
-- mkForAllVisCos [tv{vis}] constructs a cast
-- forall tv. res ~R# forall tv{vis} res`.
@@ -1000,14 +1001,26 @@ mkHomoForAllCos vs orig_co
= foldr go orig_co vs
where
go :: ForAllTyBinder -> Coercion -> Coercion
- go (Bndr var vis) = mkForAllCo_NoRefl var vis vis MRefl
-
--- | Like 'mkForAllCo', but there is no need to check that the inner coercion isn't Refl;
--- the caller has done that. (For example, it is guaranteed in 'mkHomoForAllCos'.)
--- The kind of the tycovar should be the left-hand kind of the kind coercion.
-mkForAllCo_NoRefl :: TyCoVar -> ForAllTyFlag -> ForAllTyFlag
- -> KindMCoercion -> Coercion -> Coercion
-mkForAllCo_NoRefl tcv visL visR kind_co co
+ go (Bndr var vis) co = mk_forall_co var vis vis MRefl co
+
+mkHomoForAllCo :: TyVar -> Coercion -> Coercion
+-- Specialised for a single TyVar,
+-- and visibility of coreTyLamForAllTyFlag
+mkHomoForAllCo tv orig_co
+ | Just (ty, r) <- isReflCo_maybe orig_co
+ = mkReflCo r (mkForAllTy (Bndr tv vis) ty)
+ | otherwise
+ = mk_forall_co tv vis vis MRefl orig_co
+ where
+ vis = coreTyLamForAllTyFlag
+
+-- | `mk_forall_co` just builds a ForAllCo.
+-- With debug on, it checks invariants (e.g. he kind of the tycovar should
+-- be the left-hand kind of the kind coercion).
+-- Callers should have done any isReflCo short-cutting.
+mk_forall_co :: TyCoVar -> ForAllTyFlag -> ForAllTyFlag
+ -> KindMCoercion -> Coercion -> Coercion
+mk_forall_co tcv visL visR kind_co co
= assertGoodForAllCo tcv visL visR kind_co co $
assertPpr (not (isReflCo co && isReflMCo kind_co && visL == visR)) (ppr co) $
ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR
@@ -1769,7 +1782,7 @@ mkPiCos r vs co = foldr (mkPiCo r) co vs
-- | Make a forall 'Coercion', where both types related by the coercion
-- are quantified over the same variable.
mkPiCo :: Role -> Var -> Coercion -> Coercion
-mkPiCo r v co | isTyVar v = mkHomoForAllCos [Bndr v coreTyLamForAllTyFlag] co
+mkPiCo r v co | isTyVar v = mkHomoForAllCo v co
| isCoVar v = assert (not (v `elemVarSet` tyCoVarsOfCo co)) $
-- We didn't call mkForAllCo here because if v does not appear
-- in co, the argument coercion will be nominal. But here we
=====================================
compiler/GHC/Hs/Syn/Type.hs
=====================================
@@ -187,11 +187,13 @@ liftPRType :: (Type -> Type) -> PRType -> PRType
liftPRType f pty = (f (prTypeType pty), [])
hsWrapperType :: HsWrapper -> Type -> Type
+-- Return the type of (WrapExpr wrap e), given that e :: ty
hsWrapperType wrap ty = prTypeType $ go wrap (ty,[])
where
go WpHole = id
+ go (WpSubType w) = go w
go (w1 `WpCompose` w2) = go w1 . go w2
- go (WpFun _ w2 (Scaled m exp_arg)) = liftPRType $ \t ->
+ go (WpFun _ w2 (Scaled m exp_arg) _) = liftPRType $ \t ->
let act_res = funResultTy t
exp_res = hsWrapperType w2 act_res
in mkFunctionType m exp_arg exp_res
=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -1597,9 +1597,13 @@ dsHsWrapper hs_wrap thing_inside
ds_hs_wrapper :: HsWrapper
-> ((CoreExpr -> CoreExpr) -> DsM a)
-> DsM a
-ds_hs_wrapper wrap = go wrap
+ds_hs_wrapper hs_wrap
+ = go hs_wrap
where
go WpHole k = k $ \e -> e
+ go (WpSubType w) k = go (optSubTypeHsWrapper w) k
+ -- See (DSST3) in Note [Deep subsumption and WpSubType]
+ -- in GHC.Tc.Types.Evidence
go (WpTyApp ty) k = k $ \e -> App e (Type ty)
go (WpEvLam ev) k = k $ Lam ev
go (WpTyLam tv) k = k $ Lam tv
@@ -1612,13 +1616,13 @@ ds_hs_wrapper wrap = go wrap
go (WpCompose c1 c2) k = go c1 $ \w1 ->
go c2 $ \w2 ->
k (w1 . w2)
- go (WpFun c1 c2 st) k = -- See Note [Desugaring WpFun]
- do { x <- newSysLocalDs st
- ; go c1 $ \w1 ->
- go c2 $ \w2 ->
- let app f a = mkCoreApp (text "dsHsWrapper") f a
- arg = w1 (Var x)
- in k (\e -> (Lam x (w2 (app e arg)))) }
+ go (WpFun c1 c2 st _) k = -- See Note [Desugaring WpFun]
+ do { x <- newSysLocalDs st
+ ; go c1 $ \w1 ->
+ go c2 $ \w2 ->
+ let app f a = mkCoreApp (text "dsHsWrapper") f a
+ arg = w1 (Var x)
+ in k (\e -> (Lam x (w2 (app e arg)))) }
--------------------------------------
dsTcEvBinds_s :: [TcEvBinds] -> ([CoreBind] -> DsM a) -> DsM a
=====================================
compiler/GHC/HsToCore/Match.hs
=====================================
@@ -1240,7 +1240,7 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
-- equating different ways of writing a coercion)
wrap WpHole WpHole = True
wrap (WpCompose w1 w2) (WpCompose w1' w2') = wrap w1 w1' && wrap w2 w2'
- wrap (WpFun w1 w2 _) (WpFun w1' w2' _) = wrap w1 w1' && wrap w2 w2'
+ wrap (WpFun w1 w2 _ _) (WpFun w1' w2' _ _) = wrap w1 w1' && wrap w2 w2'
wrap (WpCast co) (WpCast co') = co `eqCoercion` co'
wrap (WpEvApp et1) (WpEvApp et2) = et1 `ev_term` et2
wrap (WpTyApp t) (WpTyApp t') = eqType t t'
=====================================
compiler/GHC/Iface/Ext/Ast.hs
=====================================
@@ -696,7 +696,7 @@ instance ToHie (LocatedA HsWrapper) where
(WpLet bs) -> toHie $ EvBindContext (mkScope osp) (getRealSpanA osp) (L osp bs)
(WpCompose a b) -> concatM $
[toHie (L osp a), toHie (L osp b)]
- (WpFun a b _) -> concatM $
+ (WpFun a b _ _) -> concatM $
[toHie (L osp a), toHie (L osp b)]
(WpEvLam a) ->
toHie $ C (EvidenceVarBind EvWrapperBind (mkScope osp) (getRealSpanA osp))
=====================================
compiler/GHC/Tc/Errors/Hole.hs
=====================================
@@ -823,9 +823,11 @@ tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates =
unfoldWrapper :: HsWrapper -> [Type]
unfoldWrapper = reverse . unfWrp'
- where unfWrp' (WpTyApp ty) = [ty]
- unfWrp' (WpCompose w1 w2) = unfWrp' w1 ++ unfWrp' w2
- unfWrp' _ = []
+ where
+ unfWrp' (WpTyApp ty) = [ty]
+ unfWrp' (WpSubType w) = unfWrp' w
+ unfWrp' (WpCompose w1 w2) = unfWrp' w1 ++ unfWrp' w2
+ unfWrp' _ = []
-- The real work happens here, where we invoke the type checker using
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -794,7 +794,7 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
= do { let herald = case fun_ctxt of
VAExpansion (OrigStmt{}) _ _ -> ExpectedFunTySyntaxOp DoOrigin tc_fun
_ -> ExpectedFunTyArg (HsExprTcThing tc_fun) (unLoc arg)
- ; (wrap, arg_ty, res_ty) <-
+ ; (fun_co, arg_ty, res_ty) <-
-- NB: matchActualFunTy does the rep-poly check.
-- For example, suppose we have f :: forall r (a::TYPE r). a -> Int
-- In an application (f x), we need 'x' to have a fixed runtime
@@ -805,7 +805,7 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
(n_val_args, fun_sigma) fun_ty
; arg' <- quickLookArg do_ql ctxt arg arg_ty
- ; let acc' = arg' : addArgWrap wrap acc
+ ; let acc' = arg' : addArgWrap (mkWpCastN fun_co) acc
; go (pos+1) acc' res_ty rest_args }
new_arg_ty :: LHsExpr GhcRn -> Int -> TcM (Scaled TcType)
=====================================
compiler/GHC/Tc/Gen/Head.hs
=====================================
@@ -765,13 +765,13 @@ tcInferOverLit lit@(OverLit { ol_val = val
thing = NameThing from_name
mb_thing = Just thing
herald = ExpectedFunTyArg thing (HsLit noExtField hs_lit)
- ; (wrap2, sarg_ty, res_ty) <- matchActualFunTy herald mb_thing (1, from_ty) from_ty
+ ; (co2, sarg_ty, res_ty) <- matchActualFunTy herald mb_thing (1, from_ty) from_ty
; co <- unifyType mb_thing (hsLitType hs_lit) (scaledThing sarg_ty)
-- See Note [Source locations for implicit function calls] in GHC.Iface.Ext.Ast
; let lit_expr = L (l2l loc) $ mkHsWrapCo co $
HsLit noExtField hs_lit
- from_expr = mkHsWrap (wrap2 <.> wrap1) $
+ from_expr = mkHsWrap (mkWpCastN co2 <.> wrap1) $
mkHsVar (L loc from_id)
witness = HsApp noExtField (L (l2l loc) from_expr) lit_expr
lit' = OverLit { ol_val = val
=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -699,7 +699,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
-- Expression must be a function
; let herald = ExpectedFunTyViewPat $ unLoc expr
- ; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma)
+ ; (expr_co1, Scaled _mult inf_arg_ty, inf_res_sigma)
<- matchActualFunTy herald (Just . HsExprRnThing $ unLoc expr) (1,expr_rho) expr_rho
-- See Note [View patterns and polymorphism]
-- expr_wrap1 :: expr_rho "->" (inf_arg_ty -> inf_res_sigma)
@@ -720,7 +720,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
-- NB: pat_ty comes from matchActualFunTy, so it has a
-- fixed RuntimeRep, as needed to call mkWpFun.
- expr_wrap = expr_wrap2' <.> expr_wrap1
+ expr_wrap = expr_wrap2' <.> mkWpCastN expr_co1
; return $ (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res) }
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -8,10 +8,11 @@ module GHC.Tc.Types.Evidence (
-- * HsWrapper
HsWrapper(..),
(<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpForAllCast,
- mkWpEvLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, mkWpEta,
+ mkWpEvLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, mkWpEta, mkWpSubType,
collectHsWrapBinders,
idHsWrapper, isIdHsWrapper,
pprHsWrapper, hsWrapDictBinders,
+ optSubTypeHsWrapper,
-- * Evidence bindings
TcEvBinds(..), EvBindsVar(..),
@@ -73,7 +74,7 @@ import GHC.Types.Unique.DFM
import GHC.Types.Unique.FM
import GHC.Types.Name( isInternalName )
import GHC.Types.Var
-import GHC.Types.Id( idScaledType )
+import GHC.Types.Id( idScaledType, idType )
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Basic
@@ -134,35 +135,128 @@ maybeSymCo NotSwapped co = co
************************************************************************
-}
--- We write wrap :: t1 ~> t2
--- if wrap[ e::t1 ] :: t2
+{- Note [Deep subsumption and WpSubType]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When making DeepSubsumption checks, we may end up with hard-to-spot identity wrappers.
+For example (#26349) suppose we have
+ (forall a. Eq a => a->a) -> Int <= (forall a. Eq a => a->a) -> Int
+The two types are equal so we should certainly get an identity wrapper. But we'll get
+tihs wrapper from `tcSubType`:
+ WpFun (WpTyLam a <.> WpEvLam dg <.> WpLet (dw=dg) <.> WpEvApp dw <.> WpTyApp a)
+ WpHole
+That elaborate wrapper is really just a no-op, but it's far from obvious. If we just
+desugar (HsWrap f wp) straightforwardly we'll get
+ \(g:forall a. Eq a => a -> a).
+ f (/\a. \(dg:Eq a). let dw=dg in g a dw)
+
+To recognise that as just `f`, we'd have to eta-reduce twice. But eta-reduction
+is not sound in general, so we'll end up retaining the lambdas. Two bad results:
+
+* Adding DeepSubsumption gratuitiously makes programs less efficient.
+
+* When the subsumption is on the LHS of a rule, or in a SPECIALISE pragma, we
+ may not be able to make a decent RULE at all, and will fail with "LHS of rule
+ is too complicated to desugar" (#26255)
+
+It'd be ideal to solve the problem at the source, by never generating those
+gruesome wrappers in the first place, but we can't do that because:
+
+* The WpTyLam and WpTyApp are introduced independently, not together, in `tcSubType`,
+ so we can't easily cancel them out. For example, even if we have
+ forall a. t1 <= forall a. t2
+ there is no guarantee that these are the "same" a. E.g.
+ forall a b. a -> b -> b <= forall x y. y -> x -> x
+ Similarly WpEvLam and WpEvApp
+
+* We have not yet done constraint solving so we don't know what evidence will
+ end up in those WpLet bindings.
+
+TL;DR we must generate the wrapper and then optimise it way if it turns out
+that it is a no-op. Here's our solution:
+
+(DSST1) Tag the wrappers generated from a subtype check with WpSubType. In normal
+ wrappers the binders of a WpTyLam or WpEvLam can scope over the "hole" of the
+ wrapper -- that is how we introduce type-lambdas and dictionary-lambda into the
+ terms! But in /subtype/ wrappers, these type/dictionary lambdas only scope over
+ the WpTyApp and WpEvApp nodes in the /same/ wrapper. That is what justifies us
+ eta-reducing the type/dictionary lambdas.
+
+ In short, (WpSubType wp) means the same as `wp`, but with the added promise that
+ the binders in `wp` do not scope over the hole.
+
+(DSST2) Avoid creating a WpSubType in the common WpHole case, using `mkWpSubType`.
+
+(DSST3) When desugaring, try eta-reduction on the payload of a WpSubType.
+ This is done in `GHC.HsToCore.Binds.dsHsWrapper` by the call to `optSubTypeHsWrapper`.
+
+ We don't attempt to optimise HsWrappers /other than/ subtype wrappers. Why not?
+ Because there aren't any useful optimsations we can do. (We could collapse
+ adjacent `WpCast`s perhaps, but that'll happen later automatically via `mkCast`.)
+
+ TL;DR:
+ * we /must/ optimise subtype-HsWrappers (that's the point of this Note!)
+ * there is little point in attempting to optimise any other HsWrappers
+
+Note [WpFun-RR-INVARIANT]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Given
+ wrap = WpFun wrap1 wrap2 sty1 ty2
+ where: wrap1 :: exp_arg ~~> act_arg
+ wrap2 :: act_res ~~> exp_res
+ wrap :: (act_arg -> act_res) ~~> (exp_arg -> exp_res)
+we have
+ WpFun-RR-INVARIANT:
+ the input (exp_arg) and output (act_arg) types of `wrap1`
+ both have a fixed runtime-rep
+
+Reason: We desugar wrap[e] into
+ \(x:exp_arg). wrap2[ e wrap1[x] ]
+And then, because of Note [Representation polymorphism invariants], we need:
+
+ * `exp_arg` must have a fixed runtime rep,
+ so that lambda obeys the the FRR rules
+
+ * `act_arg` must have a fixed runtime rep,
+ so the that application (e wrap1[x]) obeys the FRR tules
+
+Hence WpFun-INVARIANT.
+-}
+
data HsWrapper
+ -- NOTATION (~~>):
+ -- We write wrap :: t1 ~~> t2
+ -- if wrap[ e::t1 ] :: t2
= WpHole -- The identity coercion
+ | WpSubType HsWrapper
+ -- (WpSubType wp) is the same as `wp`, but with extra invariants
+ -- See Note [Deep subsumption and WpSubType] (DSST1)
+
| WpCompose HsWrapper HsWrapper
-- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
--
-- Hence (\a. []) `WpCompose` (\b. []) = (\a b. [])
-- But ([] a) `WpCompose` ([] b) = ([] b a)
--
- -- If wrap1 :: t2 ~> t3
- -- wrap2 :: t1 ~> t2
- --- Then (wrap1 `WpCompose` wrap2) :: t1 ~> t3
-
- | WpFun HsWrapper HsWrapper (Scaled TcTypeFRR)
- -- (WpFun wrap1 wrap2 (w, t1))[e] = \(x:_w exp_arg). wrap2[ e wrap1[x] ]
- -- So note that if e :: act_arg -> act_res
- -- wrap1 :: exp_arg ~> act_arg
- -- wrap2 :: act_res ~> exp_res
- -- then WpFun wrap1 wrap2 : (act_arg -> arg_res) ~> (exp_arg -> exp_res)
+ -- If wrap1 :: t2 ~~> t3
+ -- wrap2 :: t1 ~~> t2
+ --- Then (wrap1 `WpCompose` wrap2) :: t1 ~~> t3
+
+ | WpFun HsWrapper HsWrapper (Scaled TcTypeFRR) TcType
+ -- (WpFun wrap1 wrap2 (w, t1) t2)[e] = \(x:_w exp_arg). wrap2[ e wrap1[x] ]
+ --
+ -- INVARIANT: both input and output types of `wrap1` have a fixed runtime-rep
+ -- See Note [WpFun-RR-INVARIANT]
+ --
+ -- Typing rules:
+ -- If e :: act_arg -> act_res
+ -- wrap1 :: exp_arg ~~> act_arg
+ -- wrap2 :: act_res ~~> exp_res
+ -- then WpFun wrap1 wrap2 :: (act_arg -> act_res) ~~> (exp_arg -> exp_res)
-- This isn't the same as for mkFunCo, but it has to be this way
-- because we can't use 'sym' to flip around these HsWrappers
- -- The TcType is the "from" type of the first wrapper;
- -- it always a Type, not a Constraint
--
- -- NB: a WpFun is always for a (->) function arrow
- --
- -- Use 'mkWpFun' to construct such a wrapper.
+ -- NB: a WpFun is always for a (->) function arrow, never (=>)
| WpCast TcCoercionR -- A cast: [] `cast` co
-- Guaranteed not the identity coercion
@@ -212,50 +306,48 @@ WpCast c1 <.> WpCast c2 = WpCast (c2 `mkTransCo` c1)
--
-- NB: <.> behaves like function composition:
--
- -- WpCast c1 <.> WpCast c2 :: coercionLKind c2 ~> coercionRKind c1
+ -- WpCast c1 <.> WpCast c2 :: coercionLKind c2 ~~> coercionRKind c1
--
-- This is thus the same as WpCast (c2 ; c1) and not WpCast (c1 ; c2).
c1 <.> c2 = c1 `WpCompose` c2
--- | Smart constructor to create a 'WpFun' 'HsWrapper', which avoids introducing
--- a lambda abstraction if the two supplied wrappers are either identities or
--- casts.
---
--- PRECONDITION: either:
---
--- 1. both of the 'HsWrapper's are identities or casts, or
--- 2. both the "from" and "to" types of the first wrapper have a syntactically
--- fixed RuntimeRep (see Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete).
mkWpFun :: HsWrapper -> HsWrapper
-> Scaled TcTypeFRR -- ^ the "from" type of the first wrapper
-> TcType -- ^ Either "from" type or "to" type of the second wrapper
-- (used only when the second wrapper is the identity)
-> HsWrapper
-mkWpFun WpHole WpHole _ _ = WpHole
-mkWpFun WpHole (WpCast co2) (Scaled w t1) _ = WpCast (mk_wp_fun_co w (mkRepReflCo t1) co2)
-mkWpFun (WpCast co1) WpHole (Scaled w _) t2 = WpCast (mk_wp_fun_co w (mkSymCo co1) (mkRepReflCo t2))
-mkWpFun (WpCast co1) (WpCast co2) (Scaled w _) _ = WpCast (mk_wp_fun_co w (mkSymCo co1) co2)
-mkWpFun w_arg w_res t1 _ =
- -- In this case, we will desugar to a lambda
- --
- -- \x. w_res[ e w_arg[x] ]
- --
- -- To satisfy Note [Representation polymorphism invariants] in GHC.Core,
- -- it must be the case that both the lambda bound variable x and the function
- -- argument w_arg[x] have a fixed runtime representation, i.e. that both the
- -- "from" and "to" types of the first wrapper "w_arg" have a fixed runtime representation.
- --
- -- Unfortunately, we can't check this with an assertion here, because of
- -- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
- WpFun w_arg w_res t1
-
-mkWpEta :: [Id] -> HsWrapper -> HsWrapper
+-- ^ Smart constructor for `WpFun`
+-- Just removes clutter and optimises some common cases.
+--
+-- PRECONDITION: same as Note [WpFun-RR-INVARIANT]
+--
+-- Unfortunately, we can't check PRECONDITION with an assertion here, because of
+-- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
+mkWpFun w1 w2 st1@(Scaled m1 t1) t2
+ = case (w1,w2) of
+ (WpHole, WpHole) -> WpHole
+ (WpHole, WpCast co2) -> WpCast (mk_wp_fun_co m1 (mkRepReflCo t1) co2)
+ (WpCast co1, WpHole) -> WpCast (mk_wp_fun_co m1 (mkSymCo co1) (mkRepReflCo t2))
+ (WpCast co1, WpCast co2) -> WpCast (mk_wp_fun_co m1 (mkSymCo co1) co2)
+ (_, _) -> WpFun w1 w2 st1 t2
+
+mkWpSubType :: HsWrapper -> HsWrapper
+-- See (DSST2) in Note [Deep subsumption and WpSubType]
+mkWpSubType WpHole = WpHole
+mkWpSubType (WpCast co) = WpCast co
+mkWpSubType w = WpSubType w
+
+mkWpEta :: Type -> [Id] -> HsWrapper -> HsWrapper
-- (mkWpEta [x1, x2] wrap) [e]
-- = \x1. \x2. wrap[e x1 x2]
-- Just generates a bunch of WpFuns
-mkWpEta xs wrap = foldr eta_one wrap xs
+-- The incoming type is the type of the entire expression
+mkWpEta orig_fun_ty xs wrap = go orig_fun_ty xs
where
- eta_one x wrap = WpFun idHsWrapper wrap (idScaledType x)
+ go _ [] = wrap
+ go fun_ty (id:ids) = WpFun idHsWrapper (go res_ty ids) (idScaledType id) res_ty
+ where
+ res_ty = funResultTy fun_ty
mk_wp_fun_co :: Mult -> TcCoercionR -> TcCoercionR -> TcCoercionR
mk_wp_fun_co mult arg_co res_co
@@ -333,8 +425,9 @@ hsWrapDictBinders wrap = go wrap
where
go (WpEvLam dict_id) = unitBag dict_id
go (w1 `WpCompose` w2) = go w1 `unionBags` go w2
- go (WpFun _ w _) = go w
+ go (WpFun _ w _ _) = go w
go WpHole = emptyBag
+ go (WpSubType {}) = emptyBag -- See Note [Deep subsumption and WpSubType]
go (WpCast {}) = emptyBag
go (WpEvApp {}) = emptyBag
go (WpTyLam {}) = emptyBag
@@ -350,6 +443,7 @@ collectHsWrapBinders wrap = go wrap []
go :: HsWrapper -> [HsWrapper] -> ([Var], HsWrapper)
go (WpEvLam v) wraps = add_lam v (gos wraps)
go (WpTyLam v) wraps = add_lam v (gos wraps)
+ go (WpSubType w) wraps = go w wraps
go (WpCompose w1 w2) wraps = go w1 (w2:wraps)
go wrap wraps = ([], foldl' (<.>) wrap wraps)
@@ -358,6 +452,162 @@ collectHsWrapBinders wrap = go wrap []
add_lam v (vs,w) = (v:vs, w)
+
+optSubTypeHsWrapper :: HsWrapper -> HsWrapper
+-- This optimiser is used only on the payload of WpSubType
+-- It finds cases where the entire wrapper is a no-op
+-- See (DSST3) in Note [Deep subsumption and WpSubType]
+optSubTypeHsWrapper wrap
+ = opt wrap
+ where
+ opt :: HsWrapper -> HsWrapper
+ opt w = foldr (<.>) WpHole (opt1 w [])
+
+ opt1 :: HsWrapper -> [HsWrapper] -> [HsWrapper]
+ -- opt1 w ws = w <.> (foldr <.> WpHole ws)
+ -- INVARIANT: ws::[HsWrapper] is optimised
+ opt1 WpHole ws = ws
+ opt1 (WpSubType w) ws = opt1 w ws
+ opt1 (w1 `WpCompose` w2) ws = opt1 w1 (opt1 w2 ws)
+ opt1 (WpCast co) ws = opt_co co ws
+ opt1 (WpEvLam ev) ws = opt_ev_lam ev ws
+ opt1 (WpTyLam tv) ws = opt_ty_lam tv ws
+ opt1 (WpLet binds) ws = pushWpLet binds ws
+ opt1 (WpFun w1 w2 sty1 ty2) ws = opt_fun w1 w2 sty1 ty2 ws
+ opt1 w@(WpTyApp {}) ws = w : ws
+ opt1 w@(WpEvApp {}) ws = w : ws
+
+ -----------------
+ -- (WpTyLam a <.> WpTyApp a <.> w) = w
+ -- i.e. /\a. <hole> a --> <hole>
+ -- This is only valid if whatever fills the hole does not mention 'a'
+ -- But that's guaranteed in subtype-wrappers;
+ -- see (DSST1) in Note [Deep subsumption and WpSubType]
+ opt_ty_lam tv (WpTyApp ty : ws)
+ | Just tv' <- getTyVar_maybe ty
+ , tv==tv'
+ , all (tv `not_in`) ws
+ = ws
+
+ -- (WpTyLam a <.> WpCastCo co <.> w)
+ -- = WpCast (ForAllCo a co) (WpTyLam <.> w)
+ opt_ty_lam tv (WpCast co : ws)
+ = opt_co (mkHomoForAllCo tv co) (opt_ty_lam tv ws)
+
+ opt_ty_lam tv ws
+ = WpTyLam tv : ws
+
+ -----------------
+ -- (WpEvLam ev <.> WpEvAp ev <.> w) = w
+ -- Similar notes to WpTyLam
+ opt_ev_lam ev (WpEvApp ev_tm : ws)
+ | EvExpr (Var ev') <- ev_tm
+ , ev == ev'
+ , all (ev `not_in`) ws
+ = ws
+
+ -- (WpEvLam ev <.> WpCast co <.> w)
+ -- = WpCast (FunCo ev co) (WpEvLam <.> w)
+ opt_ev_lam ev (WpCast co : ws)
+ = opt_co fun_co (opt_ev_lam ev ws)
+ where
+ fun_co = mkFunCo Representational FTF_C_T
+ (mkNomReflCo ManyTy)
+ (mkRepReflCo (idType ev))
+ co
+
+ opt_ev_lam ev ws
+ = WpEvLam ev : ws
+
+ -----------------
+ -- WpCast co <.> WpCast co' <.> ws = WpCast (co;co') ws
+ opt_co co (WpCast co' : ws) = opt_co (co `mkTransCo` co') ws
+ opt_co co ws | isReflexiveCo co = ws
+ | otherwise = WpCast co : ws
+
+ ------------------
+ opt_fun w1 w2 sty1 ty2 ws
+ = case mkWpFun (opt w1) (opt w2) sty1 ty2 of
+ WpHole -> ws
+ WpCast co -> opt_co co ws
+ w -> w : ws
+
+ ------------------
+ -- Tiresome check that the lambda-bound type/evidence variable that we
+ -- want to eta-reduce isn't free in the rest of the wrapper
+ not_in :: TyVar -> HsWrapper -> Bool
+ not_in _ WpHole = True
+ not_in v (WpCast co) = not (anyFreeVarsOfCo (== v) co)
+ not_in v (WpTyApp ty) = not (anyFreeVarsOfType (== v) ty)
+ not_in v (WpFun w1 w2 _ _) = not_in v w1 && not_in v w2
+ not_in v (WpSubType w) = not_in v w
+ not_in v (WpCompose w1 w2) = not_in v w1 && not_in v w2
+ not_in v (WpEvApp (EvExpr e)) = not (v `elemVarSet` exprFreeVars e)
+ not_in _ (WpEvApp (EvTypeable {})) = False -- Giving up; conservative
+ not_in _ (WpEvApp (EvFun {})) = False -- Giving up; conservative
+ not_in _ (WpTyLam {}) = False -- Give up; conservative
+ not_in _ (WpEvLam {}) = False -- Ditto
+ not_in _ (WpLet {}) = False -- Ditto
+
+pushWpLet :: TcEvBinds -> [HsWrapper] -> [HsWrapper]
+-- See if we can transform
+-- WpLet binds <.> w1 <.> .. <.> wn --> w1' <.> .. <.> wn'
+-- by substitution.
+-- We do this just for the narrow case when
+-- - the `binds` are all just v=w, variables only
+-- - the wi are all WpTyApp, WpEvApp, or WpCast
+-- This is just enough to get us the eta-reductions that we seek
+pushWpLet tc_ev_binds ws
+ = case tc_ev_binds of
+ TcEvBinds {} -> pprPanic "pushWpLet" (ppr tc_ev_binds)
+ EvBinds binds
+ | isEmptyBag binds
+ -> ws
+ | Just env <- ev_bind_swizzle binds
+ -> case go env ws of
+ Just ws' -> ws'
+ Nothing -> bale_out
+ | otherwise
+ -> bale_out
+ where
+ bale_out = WpLet tc_ev_binds : ws
+
+ go :: IdEnv Id -> [HsWrapper] -> Maybe [HsWrapper]
+ go env (WpCast co : ws) = do { ws' <- go env ws
+ ; return (WpCast co : ws') }
+ go env (WpTyApp ty : ws) = do { ws' <- go env ws
+ ; return (WpTyApp ty : ws') }
+ go env (WpEvApp (EvExpr (Var v)) : ws)
+ = do { v' <- swizzle_id env v
+ ; ws' <- go env ws
+ ; return (WpEvApp (EvExpr (Var v')) : ws') }
+
+ go _ ws = case ws of
+ [] -> Just []
+ (_:_) -> Nothing -- Could not fully eliminate the WpLet
+
+ swizzle_id :: IdEnv Id -> Id -> Maybe Id
+ -- Nothing <=> ran out of fuel
+ -- This is just belt and braces; we should never build bottom evidence
+ swizzle_id env v = go 100 v
+ where
+ go :: Int -> EvId -> Maybe EvId
+ go fuel v
+ | fuel == 0 = Nothing
+ | Just v' <- lookupVarEnv env v = go (fuel-1) v'
+ | otherwise = Just v
+
+ ev_bind_swizzle :: Bag EvBind -> Maybe (IdEnv Id)
+ -- Succeeds only if the bindings are all var-to-var bindings
+ ev_bind_swizzle evbs = foldl' do_one (Just emptyVarEnv) evbs
+ where
+ do_one :: Maybe (IdEnv Id) -> EvBind -> Maybe (IdEnv Id)
+ do_one Nothing _ = Nothing
+ do_one (Just swizzle) (EvBind {eb_lhs = bndr, eb_rhs = rhs})
+ = case rhs of
+ EvExpr (Var v) -> Just (extendVarEnv swizzle bndr v)
+ _ -> Nothing
+
{-
************************************************************************
* *
@@ -1018,8 +1268,9 @@ pprHsWrapper wrap pp_thing_inside
-- True <=> appears in function application position
-- False <=> appears as body of let or lambda
help it WpHole = it
- help it (WpCompose f1 f2) = help (help it f2) f1
- help it (WpFun f1 f2 (Scaled w t1)) = add_parens $ text "\\(x" <> dcolon <> brackets (ppr w) <> ppr t1 <> text ")." <+>
+ help it (WpCompose w1 w2) = help (help it w2) w1
+ help it (WpSubType w) = no_parens $ text "subtype" <> braces (help it w False)
+ help it (WpFun f1 f2 (Scaled w t1) _) = add_parens $ text "\\(x" <> dcolon <> brackets (ppr w) <> ppr t1 <> text ")." <+>
help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False
help it (WpCast co) = add_parens $ sep [it False, nest 2 (text "|>"
<+> pprParendCo co)]
=====================================
compiler/GHC/Tc/Utils/Concrete.hs
=====================================
@@ -626,8 +626,12 @@ hasFixedRuntimeRep :: HasDebugCallStack
-- @ki@ is concrete, and @co :: ty ~# ty'@.
-- That is, @ty'@ has a syntactically fixed RuntimeRep
-- in the sense of Note [Fixed RuntimeRep].
-hasFixedRuntimeRep frr_ctxt ty =
- checkFRR_with (fmap (fmap coToMCo) . unifyConcrete_kind (fsLit "cx") . ConcreteFRR) frr_ctxt ty
+hasFixedRuntimeRep frr_ctxt ty
+ = checkFRR_with unify_conc frr_ctxt ty
+ where
+ unify_conc frr_orig ki
+ = do { co <- unifyConcrete_kind (fsLit "cx") (ConcreteFRR frr_orig) ki
+ ; return (coToMCo co) }
-- | Like 'hasFixedRuntimeRep', but we perform an eager syntactic check.
--
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -148,7 +148,7 @@ matchActualFunTy
-- (Both are used only for error messages)
-> TcRhoType
-- ^ Type to analyse: a TcRhoType
- -> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
+ -> TcM (TcCoercion, Scaled TcSigmaTypeFRR, TcSigmaType)
-- This function takes in a type to analyse (a RhoType) and returns
-- an argument type and a result type (splitting apart a function arrow).
-- The returned argument type is a SigmaType with a fixed RuntimeRep;
@@ -157,7 +157,7 @@ matchActualFunTy
-- See Note [matchActualFunTy error handling] for the first three arguments
-- If (wrap, arg_ty, res_ty) = matchActualFunTy ... fun_ty
--- then wrap :: fun_ty ~> (arg_ty -> res_ty)
+-- then wrap :: fun_ty ~~> (arg_ty -> res_ty)
-- and NB: res_ty is an (uninstantiated) SigmaType
matchActualFunTy herald mb_thing err_info fun_ty
@@ -172,13 +172,13 @@ matchActualFunTy herald mb_thing err_info fun_ty
-- hide the forall inside a meta-variable
go :: TcRhoType -- The type we're processing, perhaps after
-- expanding type synonyms
- -> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
+ -> TcM (TcCoercion, Scaled TcSigmaTypeFRR, TcSigmaType)
go ty | Just ty' <- coreView ty = go ty'
go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty })
= assert (isVisibleFunArg af) $
do { hasFixedRuntimeRep_syntactic (FRRExpectedFunTy herald 1) arg_ty
- ; return (idHsWrapper, Scaled w arg_ty, res_ty) }
+ ; return (mkNomReflCo fun_ty, Scaled w arg_ty, res_ty) }
go ty@(TyVarTy tv)
| isMetaTyVar tv
@@ -210,7 +210,7 @@ matchActualFunTy herald mb_thing err_info fun_ty
; res_ty <- newOpenFlexiTyVarTy
; let unif_fun_ty = mkScaledFunTys [arg_ty] res_ty
; co <- unifyType mb_thing fun_ty unif_fun_ty
- ; return (mkWpCastN co, arg_ty, res_ty) }
+ ; return (co, arg_ty, res_ty) }
------------
mk_ctxt :: TcType -> TidyEnv -> ZonkM (TidyEnv, ErrCtxtMsg)
@@ -249,8 +249,10 @@ matchActualFunTys :: ExpectedFunTyOrigin -- ^ See Note [Herald for matchExpected
-> Arity
-> TcSigmaType
-> TcM (HsWrapper, [Scaled TcSigmaTypeFRR], TcRhoType)
--- If matchActualFunTys n ty = (wrap, [t1,..,tn], res_ty)
--- then wrap : ty ~> (t1 -> ... -> tn -> res_ty)
+-- NB: Called only from `tcSynArgA`, and hence scheduled for destruction
+--
+-- If matchActualFunTys n fun_ty = (wrap, [t1,..,tn], res_ty)
+-- then wrap : fun_ty ~~> (t1 -> ... -> tn -> res_ty)
-- and res_ty is a RhoType
-- NB: the returned type is top-instantiated; it's a RhoType
matchActualFunTys herald ct_orig n_val_args_wanted top_ty
@@ -265,15 +267,13 @@ matchActualFunTys herald ct_orig n_val_args_wanted top_ty
go 0 _ fun_ty = return (idHsWrapper, [], fun_ty)
go n so_far fun_ty
- = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTy
- herald Nothing
- (n_val_args_wanted, top_ty)
- fun_ty
- ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1
+ = do { (co1, arg_ty1, res_ty1) <- matchActualFunTy herald Nothing
+ (n_val_args_wanted, top_ty) fun_ty
+ ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1
; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty
-- NB: arg_ty1 comes from matchActualFunTy, so it has
- -- a syntactically fixed RuntimeRep as needed to call mkWpFun.
- ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) }
+ -- a syntactically fixed RuntimeRep
+ ; return (wrap_fun2 <.> mkWpCastN co1, arg_ty1:arg_tys, res_ty) }
{-
************************************************************************
@@ -459,7 +459,7 @@ tcSkolemiseGeneral ds_flag ctxt top_ty expected_ty thing_inside
tcSkolemiseCompleteSig :: TcCompleteSig
-> ([ExpPatType] -> TcRhoType -> TcM result)
-> TcM (HsWrapper, result)
--- ^ The wrapper has type: spec_ty ~> expected_ty
+-- ^ The wrapper has type: spec_ty ~~> expected_ty
-- See Note [Skolemisation] for the differences between
-- tcSkolemiseCompleteSig and tcTopSkolemise
@@ -790,7 +790,7 @@ matchExpectedFunTys :: forall a.
-> ([ExpPatType] -> ExpRhoType -> TcM a)
-> TcM (HsWrapper, a)
-- If matchExpectedFunTys n ty = (wrap, _)
--- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
+-- then wrap : (t1 -> ... -> tn -> ty_r) ~~> ty,
-- where [t1, ..., tn], ty_r are passed to the thing_inside
--
-- Unconditionally concludes by skolemising any trailing invisible
@@ -865,12 +865,13 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
, ft_arg = arg_ty, ft_res = res_ty })
= assert (isVisibleFunArg af) $
do { let arg_pos = arity - n_req + 1 -- 1 for the first argument etc
- ; (arg_co, arg_ty) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty
+ ; (arg_co, arg_ty_frr) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty
+ ; let arg_sty_frr = Scaled mult arg_ty_frr
; (wrap_res, result) <- check (n_req - 1)
- (mkCheckExpFunPatTy (Scaled mult arg_ty) : rev_pat_tys)
+ (mkCheckExpFunPatTy arg_sty_frr : rev_pat_tys)
res_ty
; let wrap_arg = mkWpCastN arg_co
- fun_wrap = mkWpFun wrap_arg wrap_res (Scaled mult arg_ty) res_ty
+ fun_wrap = mkWpFun wrap_arg wrap_res arg_sty_frr res_ty
; return (fun_wrap, result) }
----------------------------
@@ -1407,7 +1408,7 @@ tcSubTypePat :: CtOrigin -> UserTypeCtxt
-- Used in patterns; polarity is backwards compared
-- to tcSubType
-- If wrap = tc_sub_type_et t1 t2
--- => wrap :: t1 ~> t2
+-- => wrap :: t1 ~~> t2
tcSubTypePat inst_orig ctxt (Check ty_actual) ty_expected
= tc_sub_type unifyTypeET inst_orig ctxt ty_actual ty_expected
@@ -1427,11 +1428,12 @@ tcSubTypeDS :: HsExpr GhcRn
-- DeepSubsumption <=> when checking, this type
-- is deeply skolemised
-> TcM HsWrapper
--- Only one call site, in GHC.Tc.Gen.App.tcApp
+-- Only one call site, in GHC.Tc.Gen.App.checkResultTy
tcSubTypeDS rn_expr act_rho exp_rho
- = tc_sub_type_deep Top (unifyExprType rn_expr) orig GenSigCtxt act_rho exp_rho
- where
- orig = exprCtOrigin rn_expr
+ = do { wrap <- tc_sub_type_deep Top (unifyExprType rn_expr)
+ (exprCtOrigin rn_expr)
+ GenSigCtxt act_rho exp_rho
+ ; return (mkWpSubType wrap) }
---------------
@@ -1456,7 +1458,7 @@ tcSubTypeSigma :: CtOrigin -- where did the actual type arise / why are we
-> TcSigmaType -> TcSigmaType -> TcM HsWrapper
-- External entry point, but no ExpTypes on either side
-- Checks that actual <= expected
--- Returns HsWrapper :: actual ~ expected
+-- Returns HsWrapper :: actual ~~> expected
tcSubTypeSigma orig ctxt ty_actual ty_expected
= tc_sub_type (unifyType Nothing) orig ctxt ty_actual ty_expected
@@ -1495,7 +1497,7 @@ tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify
-> TcM HsWrapper
-- Checks that actual_ty is more polymorphic than expected_ty
-- If wrap = tc_sub_type t1 t2
--- => wrap :: t1 ~> t2
+-- => wrap :: t1 ~~> t2
--
-- The "how to unify argument" is always a call to `uType TypeLevel orig`,
-- but with different ways of constructing the CtOrigin `orig` from
@@ -1504,7 +1506,8 @@ tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify
----------------------
tc_sub_type unify inst_orig ctxt ty_actual ty_expected
= do { ds_flag <- getDeepSubsumptionFlag
- ; tc_sub_type_ds Top ds_flag unify inst_orig ctxt ty_actual ty_expected }
+ ; wrap <- tc_sub_type_ds Top ds_flag unify inst_orig ctxt ty_actual ty_expected
+ ; return (mkWpSubType wrap) }
----------------------
tc_sub_type_ds :: Position p -- ^ position in the type (for error messages only)
@@ -1753,59 +1756,59 @@ we deal with function arrows. Suppose we have:
ty_actual = act_arg -> act_res
ty_expected = exp_arg -> exp_res
-To produce fun_wrap :: (act_arg -> act_res) ~> (exp_arg -> exp_res), we use
+To produce fun_wrap :: (act_arg -> act_res) ~~> (exp_arg -> exp_res), we use
the fact that the function arrow is contravariant in its argument type and
covariant in its result type. Thus we recursively perform subtype checks
on the argument types (with actual/expected switched) and the result types,
to get:
- arg_wrap :: exp_arg ~> act_arg -- NB: expected/actual have switched sides
- res_wrap :: act_res ~> exp_res
+ arg_wrap :: exp_arg ~~> act_arg -- NB: expected/actual have switched sides
+ res_wrap :: act_res ~~> exp_res
Then fun_wrap = mkWpFun arg_wrap res_wrap.
-Wrinkle [Representation-polymorphism checking during subtyping]
+Note [Representation-polymorphism checking during subtyping]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When doing deep subsumption in `tc_sub_type_deep`, looking under function arrows,
+we would usually build a `WpFun` HsWrapper. When desugared, we get eta-expansion:
- Inserting a WpFun HsWrapper amounts to impedance matching in deep subsumption
- via eta-expansion:
+ f ==> \(x :: exp_arg). res_wrap [ f (arg_wrap [x]) ]
- f ==> \ (x :: exp_arg) -> res_wrap [ f (arg_wrap [x]) ]
+Since we produce a lambda, we must enforce the representation polymorphism
+invariants described in Note [Representation polymorphism invariants] in GHC.Core.
+That is, we must ensure that both
+ - x (the lambda binder), and
+ - (arg_wrap [x]) (the function argument)
+have a fixed runtime representation.
- As we produce a lambda, we must enforce the representation polymorphism
- invariants described in Note [Representation polymorphism invariants] in GHC.Core.
- That is, we must ensure that both x (the lambda binder) and (arg_wrap [x]) (the function argument)
- have a fixed runtime representation.
+But we don't /always/ need to produce a `WpFun`: if both argument and result wrappers
+are merely coercions, we can produce a `WpCast co` instead of a `WpFun`. In that
+case there is no eta-expansion, and hence no need for FRR checks.
- Note however that desugaring mkWpFun does not always introduce a lambda: if
- both the argument and result HsWrappers are casts, then a FunCo cast suffices,
- in which case we should not perform representation-polymorphism checking.
+Here's a contrived example (there are undoubtedly more natural examples)
+(see testsuite/tests/rep-poly/NoEtaRequired):
- This means that, in the FunTy/FunTy case of tc_sub_type_deep, we can skip
- the representation-polymorphism checks if the produced argument and result
- wrappers are identities or casts.
- It is important to do so, otherwise we reject valid programs.
+ type Id :: k -> k
+ type family Id a where
- Here's a contrived example (there are undoubtedly more natural examples)
- (see testsuite/tests/rep-poly/NoEtaRequired):
+ type T :: TYPE r -> TYPE (Id r)
+ type family T a where
- type Id :: k -> k
- type family Id a where
+ test :: forall r (a :: TYPE r). a :~~: T a -> ()
+ test HRefl =
+ let
+ f :: (a -> a) -> ()
+ f _ = ()
+ g :: T a -> T a
+ g = undefined
+ in f g
- type T :: TYPE r -> TYPE (Id r)
- type family T a where
+We don't need to eta-expand `g` to make `f g` typecheck; a cast
+suffices. Hence we should not perform representation-polymorphism
+checks; they would fail here.
- test :: forall r (a :: TYPE r). a :~~: T a -> ()
- test HRefl =
- let
- f :: (a -> a) -> ()
- f _ = ()
- g :: T a -> T a
- g = undefined
- in f g
-
- We don't need to eta-expand `g` to make `f g` typecheck; a cast suffices.
- Hence we should not perform representation-polymorphism checks; they would
- fail here.
+All this is done by `mkWpFun_FRR`, which checks for the cast/cast case and
+returns a `FunCo` if so.
Note [Setting the argument context]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1947,7 +1950,7 @@ getDeepSubsumptionFlag = do { ds <- xoptM LangExt.DeepSubsumption
-- | 'tc_sub_type_deep' is where the actual work happens for deep subsumption.
--
-- Given @ty_actual@ (a sigma-type) and @ty_expected@ (deeply skolemised, i.e.
--- a deep rho type), it returns an 'HsWrapper' @wrap :: ty_actual ~> ty_expected@.
+-- a deep rho type), it returns an 'HsWrapper' @wrap :: ty_actual ~~> ty_expected@.
tc_sub_type_deep :: HasDebugCallStack
=> Position p -- ^ Position in the type (for error messages only)
-> (TcType -> TcType -> TcM TcCoercionN) -- ^ How to unify
@@ -1958,7 +1961,7 @@ tc_sub_type_deep :: HasDebugCallStack
-> TcM HsWrapper
-- If wrap = tc_sub_type_deep t1 t2
--- => wrap :: t1 ~> t2
+-- => wrap :: t1 ~~> t2
-- Here is where the work actually happens!
-- Precondition: ty_expected is deeply skolemised
@@ -2015,8 +2018,8 @@ tc_sub_type_deep pos unify inst_orig ctxt ty_actual ty_expected
; unify_wrap <- just_unify exp_funTy ty_e
; fun_wrap <- go_fun af1 act_mult act_arg act_res af1 exp_mult exp_arg exp_res
; return $ unify_wrap <.> fun_wrap
- -- unify_wrap :: exp_funTy ~> ty_e
- -- fun_wrap :: ty_a ~> exp_funTy
+ -- unify_wrap :: exp_funTy ~~> ty_e
+ -- fun_wrap :: ty_a ~~> exp_funTy
}
go1 ty_a (FunTy { ft_af = af2, ft_mult = exp_mult, ft_arg = exp_arg, ft_res = exp_res })
| isVisibleFunArg af2
@@ -2028,8 +2031,8 @@ tc_sub_type_deep pos unify inst_orig ctxt ty_actual ty_expected
; unify_wrap <- just_unify ty_a act_funTy
; fun_wrap <- go_fun af2 act_mult act_arg act_res af2 exp_mult exp_arg exp_res
; return $ fun_wrap <.> unify_wrap
- -- unify_wrap :: ty_a ~> act_funTy
- -- fun_wrap :: act_funTy ~> ty_e
+ -- unify_wrap :: ty_a ~~> act_funTy
+ -- fun_wrap :: act_funTy ~~> ty_e
}
-- Otherwise, revert to unification.
@@ -2064,17 +2067,28 @@ mkWpFun_FRR
-> Position p
-> FunTyFlag -> Type -> TcType -> Type -- actual FunTy
-> FunTyFlag -> Type -> TcType -> Type -- expected FunTy
- -> HsWrapper -- ^ exp_arg ~> act_arg
- -> HsWrapper -- ^ act_res ~> exp_res
- -> TcM HsWrapper -- ^ act_funTy ~> exp_funTy
+ -> HsWrapper -- ^ exp_arg ~~> act_arg
+ -> HsWrapper -- ^ act_res ~~> exp_res
+ -> TcM HsWrapper -- ^ (act_arg->act_res) ~~> (exp_arg->exp_res)
mkWpFun_FRR unify pos act_af act_mult act_arg act_res exp_af exp_mult exp_arg exp_res arg_wrap res_wrap
- = do { ((exp_arg_co, exp_arg_frr), (act_arg_co, _act_arg_frr)) <-
- if needs_frr_checks
- -- See Wrinkle [Representation-polymorphism checking during subtyping]
- then do { exp_frr_wrap <- hasFixedRuntimeRep (frr_ctxt True ) exp_arg
- ; act_frr_wrap <- hasFixedRuntimeRep (frr_ctxt False) act_arg
- ; return (exp_frr_wrap, act_frr_wrap) }
- else return ((mkNomReflCo exp_arg, exp_arg), (mkNomReflCo act_arg, act_arg))
+ | Just arg_co <- getWpCo_maybe arg_wrap act_arg -- arg_co :: exp_arg ~R# act_arg
+ , Just res_co <- getWpCo_maybe res_wrap act_res -- res_co :: act_res ~R# exp_res
+ = -- The argument and result wrappers are both hole or cast;
+ -- so we can make do with a FunCo
+ -- See Note [Representation-polymorphism checking during subtyping]
+ do { mult_co <- unify act_mult exp_mult
+ ; let the_co = mkFunCo2 Representational act_af exp_af mult_co (mkSymCo arg_co) res_co
+ ; return (mkWpCastR the_co) }
+
+ | otherwise
+ = -- We need a full WpFun, with the eta-expansion that it entails
+ -- And hence we must add fixed-runtime-rep checks so that the eta-expansion is OK
+ -- See Note [Representation-polymorphism checking during subtyping]
+ do { (exp_arg_co, exp_arg_frr) <- hasFixedRuntimeRep (frr_ctxt True ) exp_arg
+ ; (act_arg_co, _act_arg_frr) <- hasFixedRuntimeRep (frr_ctxt False) act_arg
+ -- exp_arg_frr, act_arg_frr :: Type have fixed runtime-reps
+ -- exp_arg_co :: exp_arg ~ exp_arg_frr Usually Refl
+ -- act_arg_co :: act_arg ~ act_arg_frr Usually Refl
-- Enforce equality of multiplicities (not the more natural sub-multiplicity).
-- See Note [Multiplicity in deep subsumption]
@@ -2083,46 +2097,36 @@ mkWpFun_FRR unify pos act_af act_mult act_arg act_res exp_af exp_mult exp_arg ex
-- equality to be Refl, but it might well not be (#26332).
; let
- exp_arg_fun_co =
+ exp_arg_fun_co = -- (exp_arg_frr -> exp_res) ~ (exp_arg -> exp_res)
mkFunCo Nominal exp_af
- (mkReflCo Nominal exp_mult)
+ (mkNomReflCo exp_mult)
(mkSymCo exp_arg_co)
- (mkReflCo Nominal exp_res)
- act_arg_fun_co =
+ (mkNomReflCo exp_res)
+ act_arg_fun_co = -- (act_arg -> act_res) ~ (act_arg_frr -> act_res)
mkFunCo Nominal act_af
act_arg_mult_co
act_arg_co
- (mkReflCo Nominal act_res)
- arg_wrap_frr =
+ (mkNomReflCo act_res)
+ arg_wrap_frr = -- exp_arg_frr ~~> act_arg_frr
mkWpCastN (mkSymCo exp_arg_co) <.> arg_wrap <.> mkWpCastN act_arg_co
- -- exp_arg_co :: exp_arg ~> exp_arg_frr
- -- act_arg_co :: act_arg ~> act_arg_frr
- -- arg_wrap :: exp_arg ~> act_arg
- -- arg_wrap_frr :: exp_arg_frr ~> act_arg_frr
- ; return $
- mkWpCastN exp_arg_fun_co
+ ; return $ -- Whole thing :: (act_arg->act_res) ~~> (exp_arg->exp_ress)
+ mkWpCastN exp_arg_fun_co -- (exp_ar_frr->exp_res) ~~> (exp_arg->exp_res)
<.>
mkWpFun arg_wrap_frr res_wrap (Scaled exp_mult exp_arg_frr) exp_res
- <.>
- mkWpCastN act_arg_fun_co
+ <.> -- (act_arg_frr->act_res) ~~> (exp_arg_frr->exp_res)
+ mkWpCastN act_arg_fun_co -- (act_arg->act_res) ~~> (act_arg_frr->act_res)
}
where
- needs_frr_checks :: Bool
- needs_frr_checks =
- not (hole_or_cast arg_wrap)
- ||
- not (hole_or_cast res_wrap)
- hole_or_cast :: HsWrapper -> Bool
- hole_or_cast WpHole = True
- hole_or_cast (WpCast {}) = True
- hole_or_cast _ = False
+ getWpCo_maybe :: HsWrapper -> Type -> Maybe CoercionR
+ -- See if a HsWrapper is just a coercion
+ getWpCo_maybe WpHole ty = Just (mkRepReflCo ty)
+ getWpCo_maybe (WpCast co) _ = Just co
+ getWpCo_maybe _ _ = Nothing
+
frr_ctxt :: Bool -> FixedRuntimeRepContext
- frr_ctxt is_exp_ty =
- FRRDeepSubsumption
- { frrDSExpected = is_exp_ty
- , frrDSPosition = pos
- }
+ frr_ctxt is_exp_ty = FRRDeepSubsumption { frrDSExpected = is_exp_ty
+ , frrDSPosition = pos }
-----------------------
deeplySkolemise :: SkolemInfo -> TcSigmaType
@@ -2146,9 +2150,9 @@ deeplySkolemise skol_info ty
; let tvs = binderVars bndrs
tvs1 = binderVars bndrs1
tv_prs1 = map tyVarName tvs `zip` bndrs1
- ; return ( mkWpEta ids1 (mkWpTyLams tvs1
- <.> mkWpEvLams ev_vars1
- <.> wrap)
+ ; return ( mkWpEta ty ids1 (mkWpTyLams tvs1
+ <.> mkWpEvLams ev_vars1
+ <.> wrap)
, tv_prs1 ++ tvs_prs2
, ev_vars1 ++ ev_vars2
, mkScaledFunTys arg_tys' rho ) }
@@ -2182,7 +2186,7 @@ deeplyInstantiate orig ty
; ids1 <- newSysLocalIds (fsLit "di") arg_tys'
; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
; (wrap2, rho2) <- go subst' rho
- ; return (mkWpEta ids1 (wrap2 <.> wrap1),
+ ; return (mkWpEta ty ids1 (wrap2 <.> wrap1),
mkScaledFunTys arg_tys' rho2) }
| otherwise
=====================================
compiler/GHC/Tc/Zonk/Type.hs
=====================================
@@ -1233,13 +1233,16 @@ zonk_cmd_top (HsCmdTop (CmdTopTc stack_tys ty ids) cmd)
-------------------------------------------------------------------------
zonkCoFn :: HsWrapper -> ZonkBndrTcM HsWrapper
zonkCoFn WpHole = return WpHole
+zonkCoFn (WpSubType w) = do { w' <- zonkCoFn w
+ ; return (WpSubType w') }
zonkCoFn (WpCompose c1 c2) = do { c1' <- zonkCoFn c1
; c2' <- zonkCoFn c2
; return (WpCompose c1' c2') }
-zonkCoFn (WpFun c1 c2 t1) = do { c1' <- zonkCoFn c1
- ; c2' <- zonkCoFn c2
- ; t1' <- noBinders $ zonkScaledTcTypeToTypeX t1
- ; return (WpFun c1' c2' t1') }
+zonkCoFn (WpFun c1 c2 t1 t2) = do { c1' <- zonkCoFn c1
+ ; c2' <- zonkCoFn c2
+ ; t1' <- noBinders $ zonkScaledTcTypeToTypeX t1
+ ; t2' <- noBinders $ zonkTcTypeToTypeX t2
+ ; return (WpFun c1' c2' t1' t2') }
zonkCoFn (WpCast co) = WpCast <$> noBinders (zonkCoToCo co)
zonkCoFn (WpEvLam ev) = WpEvLam <$> zonkEvBndrX ev
zonkCoFn (WpEvApp arg) = WpEvApp <$> noBinders (zonkEvTerm arg)
=====================================
compiler/Setup.hs
=====================================
@@ -1,4 +1,5 @@
{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE CPP #-}
module Main where
import Distribution.Simple
@@ -12,6 +13,8 @@ import Distribution.Simple.Program
import Distribution.Simple.Utils
import Distribution.Simple.Setup
import Distribution.Simple.PackageIndex
+import qualified Distribution.Simple.LocalBuildInfo as LBI
+
import System.IO
import System.Process
@@ -59,8 +62,9 @@ primopIncls =
ghcAutogen :: Verbosity -> LocalBuildInfo -> IO ()
ghcAutogen verbosity lbi@LocalBuildInfo{pkgDescrFile,withPrograms,componentNameMap,installedPkgs}
= do
+ let i = LBI.interpretSymbolicPathLBI lbi
-- Get compiler/ root directory from the cabal file
- let Just compilerRoot = takeDirectory <$> pkgDescrFile
+ let Just compilerRoot = takeDirectory . i <$> pkgDescrFile
-- Require the necessary programs
(gcc ,withPrograms) <- requireProgram normal gccProgram withPrograms
@@ -80,15 +84,19 @@ ghcAutogen verbosity lbi@LocalBuildInfo{pkgDescrFile,withPrograms,componentNameM
-- Call genprimopcode to generate *.hs-incl
forM_ primopIncls $ \(file,command) -> do
contents <- readProcess "genprimopcode" [command] primopsStr
- rewriteFileEx verbosity (buildDir lbi </> file) contents
+ rewriteFileEx verbosity (i (buildDir lbi) </> file) contents
-- Write GHC.Platform.Constants
- let platformConstantsPath = autogenPackageModulesDir lbi </> "GHC/Platform/Constants.hs"
+ let platformConstantsPath = i (autogenPackageModulesDir lbi) </> "GHC/Platform/Constants.hs"
targetOS = case lookup "target os" settings of
Nothing -> error "no target os in settings"
Just os -> os
createDirectoryIfMissingVerbose verbosity True (takeDirectory platformConstantsPath)
+#if MIN_VERSION_Cabal(3,14,0)
+ withTempFile "Constants_tmp.hs" $ \tmp h -> do
+#else
withTempFile (takeDirectory platformConstantsPath) "Constants_tmp.hs" $ \tmp h -> do
+#endif
hClose h
callProcess "deriveConstants" ["--gen-haskell-type","-o",tmp,"--target-os",targetOS]
renameFile tmp platformConstantsPath
@@ -103,7 +111,7 @@ ghcAutogen verbosity lbi@LocalBuildInfo{pkgDescrFile,withPrograms,componentNameM
_ -> error "Couldn't find unique ghc-internal library when building ghc"
-- Write GHC.Settings.Config
- configHsPath = autogenPackageModulesDir lbi </> "GHC/Settings/Config.hs"
+ configHsPath = i (autogenPackageModulesDir lbi) </> "GHC/Settings/Config.hs"
configHs = generateConfigHs cProjectUnitId cGhcInternalUnitId settings
createDirectoryIfMissingVerbose verbosity True (takeDirectory configHsPath)
rewriteFileEx verbosity configHsPath configHs
=====================================
compiler/ghc.cabal.in
=====================================
@@ -50,7 +50,7 @@ extra-source-files:
custom-setup
- setup-depends: base >= 3 && < 5, Cabal >= 1.6 && <3.14, directory, process, filepath, containers
+ setup-depends: base >= 3 && < 5, Cabal >= 1.6 && <3.16, directory, process, filepath, containers
Flag internal-interpreter
Description: Build with internal interpreter support.
=====================================
libraries/ghc-boot/Setup.hs
=====================================
@@ -10,6 +10,7 @@ import Distribution.Verbosity
import Distribution.Simple.Program
import Distribution.Simple.Utils
import Distribution.Simple.Setup
+import qualified Distribution.Simple.LocalBuildInfo as LBI
import System.IO
import System.Directory
@@ -32,12 +33,13 @@ main = defaultMainWithHooks ghcHooks
ghcAutogen :: Verbosity -> LocalBuildInfo -> IO ()
ghcAutogen verbosity lbi@LocalBuildInfo{..} = do
-- Get compiler/ root directory from the cabal file
- let Just compilerRoot = takeDirectory <$> pkgDescrFile
+ let Just compilerRoot = takeDirectory . i <$> pkgDescrFile
- let platformHostFile = "GHC/Platform/Host.hs"
- platformHostPath = autogenPackageModulesDir lbi </> platformHostFile
+ i = LBI.interpretSymbolicPathLBI lbi
+ platformHostFile = "GHC/Platform/Host.hs"
+ platformHostPath = i (autogenPackageModulesDir lbi) </> platformHostFile
ghcVersionFile = "GHC/Version.hs"
- ghcVersionPath = autogenPackageModulesDir lbi </> ghcVersionFile
+ ghcVersionPath = i (autogenPackageModulesDir lbi) </> ghcVersionFile
-- Get compiler settings
settings <- lookupEnv "HADRIAN_SETTINGS" >>= \case
=====================================
libraries/ghc-boot/ghc-boot.cabal.in
=====================================
@@ -28,7 +28,7 @@ build-type: Custom
extra-source-files: changelog.md
custom-setup
- setup-depends: base >= 3 && < 5, Cabal >= 1.6 && <3.14, directory, filepath
+ setup-depends: base >= 3 && < 5, Cabal >= 1.6 && <3.16, directory, filepath
source-repository head
type: git
=====================================
rts/ThreadPaused.c
=====================================
@@ -321,11 +321,12 @@ threadPaused(Capability *cap, StgTSO *tso)
if(frame_info == &stg_bh_upd_frame_info) {
// eager black hole: we do nothing
- // it should be a black hole that we own
+ // it should be a black hole (but we may not own it, as another
+ // thread could have raced us to claim it)
ASSERT(bh_info == &stg_BLACKHOLE_info ||
bh_info == &__stg_EAGER_BLACKHOLE_info ||
bh_info == &stg_CAF_BLACKHOLE_info);
- ASSERT(blackHoleOwner(bh) == tso || blackHoleOwner(bh) == NULL);
+
} else {
// lazy black hole
@@ -368,13 +369,15 @@ threadPaused(Capability *cap, StgTSO *tso)
// The payload of the BLACKHOLE points to the TSO
RELEASE_STORE(&((StgInd *)bh)->indirectee, (StgClosure *)tso);
SET_INFO_RELEASE(bh,&stg_BLACKHOLE_info);
+ }
- // .. and we need a write barrier, since we just mutated the closure:
- recordClosureMutated(cap,bh);
+ // We need a write barrier, since the closure was mutated (by
+ // threadPaused for lazy black holes, or the mutator for eager
+ // black holes).
+ recordClosureMutated(cap,bh);
- // We pretend that bh has just been created.
- LDV_RECORD_CREATE(bh);
- }
+ // We pretend that bh has just been created.
+ LDV_RECORD_CREATE(bh);
frame = (StgClosure *) ((StgUpdateFrame *)frame + 1);
if (prev_was_update_frame) {
=====================================
testsuite/tests/simplCore/should_compile/T26349.hs
=====================================
@@ -0,0 +1,11 @@
+{-# LANGUAGE DeepSubsumption, RankNTypes #-}
+module T26349 where
+
+{-# SPECIALIZE INLINE mapTCMT :: (forall b. IO b -> IO b) -> IO a -> IO a #-}
+mapTCMT :: (forall b. m b -> n b) -> m a -> n a
+mapTCMT f m = f m
+
+{-
+ We'll check
+ tcExpr (mapTCMT) (Check ((forall b. IO b -> IO b) -> IO a_sk -> IO a_sk))
+-}
=====================================
testsuite/tests/simplCore/should_compile/T26349.stderr
=====================================
@@ -0,0 +1,3 @@
+==================== Tidy Core rules ====================
+"USPEC mapTCMT @(*) @IO @IO @_"
+ forall (@a). mapTCMT @(*) @IO @IO @a = mapTCMT_$smapTCMT @a
=====================================
testsuite/tests/simplCore/should_compile/all.T
=====================================
@@ -559,3 +559,4 @@ test('T26051', [ grep_errmsg(r'\$wspecMe')
test('T26115', [grep_errmsg(r'DFun')], compile, ['-O -ddump-simpl -dsuppress-uniques'])
test('T26116', normal, compile, ['-O -ddump-rules'])
test('T26117', [grep_errmsg(r'==')], compile, ['-O -ddump-simpl -dsuppress-uniques'])
+test('T26349', normal, compile, ['-O -ddump-rules'])
=====================================
testsuite/tests/simplCore/should_compile/rule2.stderr
=====================================
@@ -10,18 +10,15 @@
==================== Grand total simplifier statistics ====================
-Total ticks: 13
+Total ticks: 11
-2 PreInlineUnconditionally
- 1 ds
- 1 f
+1 PreInlineUnconditionally 1 f
2 UnfoldingDone
1 GHC.Internal.Base.id
1 Roman.bar
1 RuleFired 1 foo/bar
1 LetFloatFromLet 1
-7 BetaReduction
- 1 ds
+6 BetaReduction
1 f
1 a
1 m
=====================================
utils/genprimopcode/genprimopcode.cabal
=====================================
@@ -32,4 +32,4 @@ Executable genprimopcode
Build-Depends: base >= 4 && < 5,
array
if flag(build-tool-depends)
- build-tool-depends: alex:alex >= 3.2.6, happy:happy >= 1.20.0
+ build-tool-depends: alex:alex >= 3.2.6, happy:happy >= 2.1.5 || == 1.20.0 || == 1.20.1.1
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/dc7cff8bff7d777f53eb8da22bc0f7…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/dc7cff8bff7d777f53eb8da22bc0f7…
You're receiving this email because of your account on gitlab.haskell.org.
1
0
[Git][ghc/ghc][wip/T26425] Be a little less eager to inline
by Simon Peyton Jones (@simonpj) 04 Nov '25
by Simon Peyton Jones (@simonpj) 04 Nov '25
04 Nov '25
Simon Peyton Jones pushed to branch wip/T26425 at Glasgow Haskell Compiler / GHC
Commits:
ec080d05 by Simon Peyton Jones at 2025-11-04T23:45:25+00:00
Be a little less eager to inline
- - - - -
1 changed file:
- compiler/GHC/Core/Opt/Simplify/Utils.hs
Changes:
=====================================
compiler/GHC/Core/Opt/Simplify/Utils.hs
=====================================
@@ -1032,8 +1032,8 @@ interestingArg env e = go env 0 e
| n > 0 = NonTrivArg -- Saturated or unknown call
| otherwise -- n==0, no value arguments; look for an interesting unfolding
= case idUnfolding v of
- OtherCon [] -> NonTrivArg -- It's evaluated, but that's all we know
- OtherCon _ -> ValueArg -- Evaluated and we know it isn't these constructors
+ OtherCon [] -> TrivArg -- It's evaluated, but that's all we know
+ OtherCon _ -> NonTrivArg -- Evaluated and we know it isn't these constructors
-- See Note [OtherCon and interestingArg]
DFunUnfolding {} -> ValueArg -- We konw that idArity=0
CoreUnfolding{ uf_cache = cache }
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ec080d05d53af029018ee11db9aeab1…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ec080d05d53af029018ee11db9aeab1…
You're receiving this email because of your account on gitlab.haskell.org.
1
0
[Git][ghc/ghc][wip/T26349] 2 commits: Add a HsWrapper optimiser
by Simon Peyton Jones (@simonpj) 04 Nov '25
by Simon Peyton Jones (@simonpj) 04 Nov '25
04 Nov '25
Simon Peyton Jones pushed to branch wip/T26349 at Glasgow Haskell Compiler / GHC
Commits:
ea55d5c5 by Simon Peyton Jones at 2025-11-04T22:56:38+00:00
Add a HsWrapper optimiser
This MR addresses #26349, by introduceing optSubTypeHsWrapper.
There is a long
Note [Deep subsumption and WpSubType]
in GHC.Tc.Types.Evidence that explains what is going on.
- - - - -
cf191e55 by Simon Peyton Jones at 2025-11-04T22:59:33+00:00
Improve mkWpFun_FRR
This commit ensures that `mkWpFun_FRR` directly produces a `FunCo` in
the cases where it can.
(Previously called `mkWpFun` which in turn optimised to a `FunCo`, but
that made the smarts in `mkWpFun` /essential/ rather than (as they
should be) optional.
- - - - -
17 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Hs/Syn/Type.hs
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/HsToCore/Match.hs
- compiler/GHC/Iface/Ext/Ast.hs
- compiler/GHC/Tc/Errors/Hole.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Head.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Utils/Concrete.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Tc/Zonk/Type.hs
- + testsuite/tests/simplCore/should_compile/T26349.hs
- + testsuite/tests/simplCore/should_compile/T26349.stderr
- testsuite/tests/simplCore/should_compile/all.T
- testsuite/tests/simplCore/should_compile/rule2.stderr
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -41,7 +41,8 @@ module GHC.Core.Coercion (
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo,
mkFunCo, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
mkNakedFunCo,
- mkNakedForAllCo, mkForAllCo, mkForAllVisCos, mkHomoForAllCos,
+ mkNakedForAllCo, mkForAllCo, mkForAllVisCos,
+ mkHomoForAllCo, mkHomoForAllCos,
mkPhantomCo, mkAxiomCo,
mkHoleCo, mkUnivCo, mkSubCo,
mkProofIrrelCo,
@@ -980,7 +981,7 @@ mkForAllCo v visL visR kind_co co
= mkReflCo r (mkTyCoForAllTy v visL ty)
| otherwise
- = mkForAllCo_NoRefl v visL visR kind_co co
+ = mk_forall_co v visL visR kind_co co
-- mkForAllVisCos [tv{vis}] constructs a cast
-- forall tv. res ~R# forall tv{vis} res`.
@@ -1000,14 +1001,26 @@ mkHomoForAllCos vs orig_co
= foldr go orig_co vs
where
go :: ForAllTyBinder -> Coercion -> Coercion
- go (Bndr var vis) = mkForAllCo_NoRefl var vis vis MRefl
-
--- | Like 'mkForAllCo', but there is no need to check that the inner coercion isn't Refl;
--- the caller has done that. (For example, it is guaranteed in 'mkHomoForAllCos'.)
--- The kind of the tycovar should be the left-hand kind of the kind coercion.
-mkForAllCo_NoRefl :: TyCoVar -> ForAllTyFlag -> ForAllTyFlag
- -> KindMCoercion -> Coercion -> Coercion
-mkForAllCo_NoRefl tcv visL visR kind_co co
+ go (Bndr var vis) co = mk_forall_co var vis vis MRefl co
+
+mkHomoForAllCo :: TyVar -> Coercion -> Coercion
+-- Specialised for a single TyVar,
+-- and visibility of coreTyLamForAllTyFlag
+mkHomoForAllCo tv orig_co
+ | Just (ty, r) <- isReflCo_maybe orig_co
+ = mkReflCo r (mkForAllTy (Bndr tv vis) ty)
+ | otherwise
+ = mk_forall_co tv vis vis MRefl orig_co
+ where
+ vis = coreTyLamForAllTyFlag
+
+-- | `mk_forall_co` just builds a ForAllCo.
+-- With debug on, it checks invariants (e.g. he kind of the tycovar should
+-- be the left-hand kind of the kind coercion).
+-- Callers should have done any isReflCo short-cutting.
+mk_forall_co :: TyCoVar -> ForAllTyFlag -> ForAllTyFlag
+ -> KindMCoercion -> Coercion -> Coercion
+mk_forall_co tcv visL visR kind_co co
= assertGoodForAllCo tcv visL visR kind_co co $
assertPpr (not (isReflCo co && isReflMCo kind_co && visL == visR)) (ppr co) $
ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR
@@ -1769,7 +1782,7 @@ mkPiCos r vs co = foldr (mkPiCo r) co vs
-- | Make a forall 'Coercion', where both types related by the coercion
-- are quantified over the same variable.
mkPiCo :: Role -> Var -> Coercion -> Coercion
-mkPiCo r v co | isTyVar v = mkHomoForAllCos [Bndr v coreTyLamForAllTyFlag] co
+mkPiCo r v co | isTyVar v = mkHomoForAllCo v co
| isCoVar v = assert (not (v `elemVarSet` tyCoVarsOfCo co)) $
-- We didn't call mkForAllCo here because if v does not appear
-- in co, the argument coercion will be nominal. But here we
=====================================
compiler/GHC/Hs/Syn/Type.hs
=====================================
@@ -187,11 +187,13 @@ liftPRType :: (Type -> Type) -> PRType -> PRType
liftPRType f pty = (f (prTypeType pty), [])
hsWrapperType :: HsWrapper -> Type -> Type
+-- Return the type of (WrapExpr wrap e), given that e :: ty
hsWrapperType wrap ty = prTypeType $ go wrap (ty,[])
where
go WpHole = id
+ go (WpSubType w) = go w
go (w1 `WpCompose` w2) = go w1 . go w2
- go (WpFun _ w2 (Scaled m exp_arg)) = liftPRType $ \t ->
+ go (WpFun _ w2 (Scaled m exp_arg) _) = liftPRType $ \t ->
let act_res = funResultTy t
exp_res = hsWrapperType w2 act_res
in mkFunctionType m exp_arg exp_res
=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -1597,9 +1597,13 @@ dsHsWrapper hs_wrap thing_inside
ds_hs_wrapper :: HsWrapper
-> ((CoreExpr -> CoreExpr) -> DsM a)
-> DsM a
-ds_hs_wrapper wrap = go wrap
+ds_hs_wrapper hs_wrap
+ = go hs_wrap
where
go WpHole k = k $ \e -> e
+ go (WpSubType w) k = go (optSubTypeHsWrapper w) k
+ -- See (DSST3) in Note [Deep subsumption and WpSubType]
+ -- in GHC.Tc.Types.Evidence
go (WpTyApp ty) k = k $ \e -> App e (Type ty)
go (WpEvLam ev) k = k $ Lam ev
go (WpTyLam tv) k = k $ Lam tv
@@ -1612,13 +1616,13 @@ ds_hs_wrapper wrap = go wrap
go (WpCompose c1 c2) k = go c1 $ \w1 ->
go c2 $ \w2 ->
k (w1 . w2)
- go (WpFun c1 c2 st) k = -- See Note [Desugaring WpFun]
- do { x <- newSysLocalDs st
- ; go c1 $ \w1 ->
- go c2 $ \w2 ->
- let app f a = mkCoreApp (text "dsHsWrapper") f a
- arg = w1 (Var x)
- in k (\e -> (Lam x (w2 (app e arg)))) }
+ go (WpFun c1 c2 st _) k = -- See Note [Desugaring WpFun]
+ do { x <- newSysLocalDs st
+ ; go c1 $ \w1 ->
+ go c2 $ \w2 ->
+ let app f a = mkCoreApp (text "dsHsWrapper") f a
+ arg = w1 (Var x)
+ in k (\e -> (Lam x (w2 (app e arg)))) }
--------------------------------------
dsTcEvBinds_s :: [TcEvBinds] -> ([CoreBind] -> DsM a) -> DsM a
=====================================
compiler/GHC/HsToCore/Match.hs
=====================================
@@ -1240,7 +1240,7 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
-- equating different ways of writing a coercion)
wrap WpHole WpHole = True
wrap (WpCompose w1 w2) (WpCompose w1' w2') = wrap w1 w1' && wrap w2 w2'
- wrap (WpFun w1 w2 _) (WpFun w1' w2' _) = wrap w1 w1' && wrap w2 w2'
+ wrap (WpFun w1 w2 _ _) (WpFun w1' w2' _ _) = wrap w1 w1' && wrap w2 w2'
wrap (WpCast co) (WpCast co') = co `eqCoercion` co'
wrap (WpEvApp et1) (WpEvApp et2) = et1 `ev_term` et2
wrap (WpTyApp t) (WpTyApp t') = eqType t t'
=====================================
compiler/GHC/Iface/Ext/Ast.hs
=====================================
@@ -696,7 +696,7 @@ instance ToHie (LocatedA HsWrapper) where
(WpLet bs) -> toHie $ EvBindContext (mkScope osp) (getRealSpanA osp) (L osp bs)
(WpCompose a b) -> concatM $
[toHie (L osp a), toHie (L osp b)]
- (WpFun a b _) -> concatM $
+ (WpFun a b _ _) -> concatM $
[toHie (L osp a), toHie (L osp b)]
(WpEvLam a) ->
toHie $ C (EvidenceVarBind EvWrapperBind (mkScope osp) (getRealSpanA osp))
=====================================
compiler/GHC/Tc/Errors/Hole.hs
=====================================
@@ -823,9 +823,11 @@ tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates =
unfoldWrapper :: HsWrapper -> [Type]
unfoldWrapper = reverse . unfWrp'
- where unfWrp' (WpTyApp ty) = [ty]
- unfWrp' (WpCompose w1 w2) = unfWrp' w1 ++ unfWrp' w2
- unfWrp' _ = []
+ where
+ unfWrp' (WpTyApp ty) = [ty]
+ unfWrp' (WpSubType w) = unfWrp' w
+ unfWrp' (WpCompose w1 w2) = unfWrp' w1 ++ unfWrp' w2
+ unfWrp' _ = []
-- The real work happens here, where we invoke the type checker using
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -794,7 +794,7 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
= do { let herald = case fun_ctxt of
VAExpansion (OrigStmt{}) _ _ -> ExpectedFunTySyntaxOp DoOrigin tc_fun
_ -> ExpectedFunTyArg (HsExprTcThing tc_fun) (unLoc arg)
- ; (wrap, arg_ty, res_ty) <-
+ ; (fun_co, arg_ty, res_ty) <-
-- NB: matchActualFunTy does the rep-poly check.
-- For example, suppose we have f :: forall r (a::TYPE r). a -> Int
-- In an application (f x), we need 'x' to have a fixed runtime
@@ -805,7 +805,7 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
(n_val_args, fun_sigma) fun_ty
; arg' <- quickLookArg do_ql ctxt arg arg_ty
- ; let acc' = arg' : addArgWrap wrap acc
+ ; let acc' = arg' : addArgWrap (mkWpCastN fun_co) acc
; go (pos+1) acc' res_ty rest_args }
new_arg_ty :: LHsExpr GhcRn -> Int -> TcM (Scaled TcType)
=====================================
compiler/GHC/Tc/Gen/Head.hs
=====================================
@@ -765,13 +765,13 @@ tcInferOverLit lit@(OverLit { ol_val = val
thing = NameThing from_name
mb_thing = Just thing
herald = ExpectedFunTyArg thing (HsLit noExtField hs_lit)
- ; (wrap2, sarg_ty, res_ty) <- matchActualFunTy herald mb_thing (1, from_ty) from_ty
+ ; (co2, sarg_ty, res_ty) <- matchActualFunTy herald mb_thing (1, from_ty) from_ty
; co <- unifyType mb_thing (hsLitType hs_lit) (scaledThing sarg_ty)
-- See Note [Source locations for implicit function calls] in GHC.Iface.Ext.Ast
; let lit_expr = L (l2l loc) $ mkHsWrapCo co $
HsLit noExtField hs_lit
- from_expr = mkHsWrap (wrap2 <.> wrap1) $
+ from_expr = mkHsWrap (mkWpCastN co2 <.> wrap1) $
mkHsVar (L loc from_id)
witness = HsApp noExtField (L (l2l loc) from_expr) lit_expr
lit' = OverLit { ol_val = val
=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -699,7 +699,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
-- Expression must be a function
; let herald = ExpectedFunTyViewPat $ unLoc expr
- ; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma)
+ ; (expr_co1, Scaled _mult inf_arg_ty, inf_res_sigma)
<- matchActualFunTy herald (Just . HsExprRnThing $ unLoc expr) (1,expr_rho) expr_rho
-- See Note [View patterns and polymorphism]
-- expr_wrap1 :: expr_rho "->" (inf_arg_ty -> inf_res_sigma)
@@ -720,7 +720,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
-- NB: pat_ty comes from matchActualFunTy, so it has a
-- fixed RuntimeRep, as needed to call mkWpFun.
- expr_wrap = expr_wrap2' <.> expr_wrap1
+ expr_wrap = expr_wrap2' <.> mkWpCastN expr_co1
; return $ (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res) }
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -8,10 +8,11 @@ module GHC.Tc.Types.Evidence (
-- * HsWrapper
HsWrapper(..),
(<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpForAllCast,
- mkWpEvLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, mkWpEta,
+ mkWpEvLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, mkWpEta, mkWpSubType,
collectHsWrapBinders,
idHsWrapper, isIdHsWrapper,
pprHsWrapper, hsWrapDictBinders,
+ optSubTypeHsWrapper,
-- * Evidence bindings
TcEvBinds(..), EvBindsVar(..),
@@ -73,7 +74,7 @@ import GHC.Types.Unique.DFM
import GHC.Types.Unique.FM
import GHC.Types.Name( isInternalName )
import GHC.Types.Var
-import GHC.Types.Id( idScaledType )
+import GHC.Types.Id( idScaledType, idType )
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Basic
@@ -134,35 +135,128 @@ maybeSymCo NotSwapped co = co
************************************************************************
-}
--- We write wrap :: t1 ~> t2
--- if wrap[ e::t1 ] :: t2
+{- Note [Deep subsumption and WpSubType]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When making DeepSubsumption checks, we may end up with hard-to-spot identity wrappers.
+For example (#26349) suppose we have
+ (forall a. Eq a => a->a) -> Int <= (forall a. Eq a => a->a) -> Int
+The two types are equal so we should certainly get an identity wrapper. But we'll get
+tihs wrapper from `tcSubType`:
+ WpFun (WpTyLam a <.> WpEvLam dg <.> WpLet (dw=dg) <.> WpEvApp dw <.> WpTyApp a)
+ WpHole
+That elaborate wrapper is really just a no-op, but it's far from obvious. If we just
+desugar (HsWrap f wp) straightforwardly we'll get
+ \(g:forall a. Eq a => a -> a).
+ f (/\a. \(dg:Eq a). let dw=dg in g a dw)
+
+To recognise that as just `f`, we'd have to eta-reduce twice. But eta-reduction
+is not sound in general, so we'll end up retaining the lambdas. Two bad results:
+
+* Adding DeepSubsumption gratuitiously makes programs less efficient.
+
+* When the subsumption is on the LHS of a rule, or in a SPECIALISE pragma, we
+ may not be able to make a decent RULE at all, and will fail with "LHS of rule
+ is too complicated to desugar" (#26255)
+
+It'd be ideal to solve the problem at the source, by never generating those
+gruesome wrappers in the first place, but we can't do that because:
+
+* The WpTyLam and WpTyApp are introduced independently, not together, in `tcSubType`,
+ so we can't easily cancel them out. For example, even if we have
+ forall a. t1 <= forall a. t2
+ there is no guarantee that these are the "same" a. E.g.
+ forall a b. a -> b -> b <= forall x y. y -> x -> x
+ Similarly WpEvLam and WpEvApp
+
+* We have not yet done constraint solving so we don't know what evidence will
+ end up in those WpLet bindings.
+
+TL;DR we must generate the wrapper and then optimise it way if it turns out
+that it is a no-op. Here's our solution:
+
+(DSST1) Tag the wrappers generated from a subtype check with WpSubType. In normal
+ wrappers the binders of a WpTyLam or WpEvLam can scope over the "hole" of the
+ wrapper -- that is how we introduce type-lambdas and dictionary-lambda into the
+ terms! But in /subtype/ wrappers, these type/dictionary lambdas only scope over
+ the WpTyApp and WpEvApp nodes in the /same/ wrapper. That is what justifies us
+ eta-reducing the type/dictionary lambdas.
+
+ In short, (WpSubType wp) means the same as `wp`, but with the added promise that
+ the binders in `wp` do not scope over the hole.
+
+(DSST2) Avoid creating a WpSubType in the common WpHole case, using `mkWpSubType`.
+
+(DSST3) When desugaring, try eta-reduction on the payload of a WpSubType.
+ This is done in `GHC.HsToCore.Binds.dsHsWrapper` by the call to `optSubTypeHsWrapper`.
+
+ We don't attempt to optimise HsWrappers /other than/ subtype wrappers. Why not?
+ Because there aren't any useful optimsations we can do. (We could collapse
+ adjacent `WpCast`s perhaps, but that'll happen later automatically via `mkCast`.)
+
+ TL;DR:
+ * we /must/ optimise subtype-HsWrappers (that's the point of this Note!)
+ * there is little point in attempting to optimise any other HsWrappers
+
+Note [WpFun-RR-INVARIANT]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Given
+ wrap = WpFun wrap1 wrap2 sty1 ty2
+ where: wrap1 :: exp_arg ~~> act_arg
+ wrap2 :: act_res ~~> exp_res
+ wrap :: (act_arg -> act_res) ~~> (exp_arg -> exp_res)
+we have
+ WpFun-RR-INVARIANT:
+ the input (exp_arg) and output (act_arg) types of `wrap1`
+ both have a fixed runtime-rep
+
+Reason: We desugar wrap[e] into
+ \(x:exp_arg). wrap2[ e wrap1[x] ]
+And then, because of Note [Representation polymorphism invariants], we need:
+
+ * `exp_arg` must have a fixed runtime rep,
+ so that lambda obeys the the FRR rules
+
+ * `act_arg` must have a fixed runtime rep,
+ so the that application (e wrap1[x]) obeys the FRR tules
+
+Hence WpFun-INVARIANT.
+-}
+
data HsWrapper
+ -- NOTATION (~~>):
+ -- We write wrap :: t1 ~~> t2
+ -- if wrap[ e::t1 ] :: t2
= WpHole -- The identity coercion
+ | WpSubType HsWrapper
+ -- (WpSubType wp) is the same as `wp`, but with extra invariants
+ -- See Note [Deep subsumption and WpSubType] (DSST1)
+
| WpCompose HsWrapper HsWrapper
-- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
--
-- Hence (\a. []) `WpCompose` (\b. []) = (\a b. [])
-- But ([] a) `WpCompose` ([] b) = ([] b a)
--
- -- If wrap1 :: t2 ~> t3
- -- wrap2 :: t1 ~> t2
- --- Then (wrap1 `WpCompose` wrap2) :: t1 ~> t3
-
- | WpFun HsWrapper HsWrapper (Scaled TcTypeFRR)
- -- (WpFun wrap1 wrap2 (w, t1))[e] = \(x:_w exp_arg). wrap2[ e wrap1[x] ]
- -- So note that if e :: act_arg -> act_res
- -- wrap1 :: exp_arg ~> act_arg
- -- wrap2 :: act_res ~> exp_res
- -- then WpFun wrap1 wrap2 : (act_arg -> arg_res) ~> (exp_arg -> exp_res)
+ -- If wrap1 :: t2 ~~> t3
+ -- wrap2 :: t1 ~~> t2
+ --- Then (wrap1 `WpCompose` wrap2) :: t1 ~~> t3
+
+ | WpFun HsWrapper HsWrapper (Scaled TcTypeFRR) TcType
+ -- (WpFun wrap1 wrap2 (w, t1) t2)[e] = \(x:_w exp_arg). wrap2[ e wrap1[x] ]
+ --
+ -- INVARIANT: both input and output types of `wrap1` have a fixed runtime-rep
+ -- See Note [WpFun-RR-INVARIANT]
+ --
+ -- Typing rules:
+ -- If e :: act_arg -> act_res
+ -- wrap1 :: exp_arg ~~> act_arg
+ -- wrap2 :: act_res ~~> exp_res
+ -- then WpFun wrap1 wrap2 :: (act_arg -> act_res) ~~> (exp_arg -> exp_res)
-- This isn't the same as for mkFunCo, but it has to be this way
-- because we can't use 'sym' to flip around these HsWrappers
- -- The TcType is the "from" type of the first wrapper;
- -- it always a Type, not a Constraint
--
- -- NB: a WpFun is always for a (->) function arrow
- --
- -- Use 'mkWpFun' to construct such a wrapper.
+ -- NB: a WpFun is always for a (->) function arrow, never (=>)
| WpCast TcCoercionR -- A cast: [] `cast` co
-- Guaranteed not the identity coercion
@@ -212,50 +306,48 @@ WpCast c1 <.> WpCast c2 = WpCast (c2 `mkTransCo` c1)
--
-- NB: <.> behaves like function composition:
--
- -- WpCast c1 <.> WpCast c2 :: coercionLKind c2 ~> coercionRKind c1
+ -- WpCast c1 <.> WpCast c2 :: coercionLKind c2 ~~> coercionRKind c1
--
-- This is thus the same as WpCast (c2 ; c1) and not WpCast (c1 ; c2).
c1 <.> c2 = c1 `WpCompose` c2
--- | Smart constructor to create a 'WpFun' 'HsWrapper', which avoids introducing
--- a lambda abstraction if the two supplied wrappers are either identities or
--- casts.
---
--- PRECONDITION: either:
---
--- 1. both of the 'HsWrapper's are identities or casts, or
--- 2. both the "from" and "to" types of the first wrapper have a syntactically
--- fixed RuntimeRep (see Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete).
mkWpFun :: HsWrapper -> HsWrapper
-> Scaled TcTypeFRR -- ^ the "from" type of the first wrapper
-> TcType -- ^ Either "from" type or "to" type of the second wrapper
-- (used only when the second wrapper is the identity)
-> HsWrapper
-mkWpFun WpHole WpHole _ _ = WpHole
-mkWpFun WpHole (WpCast co2) (Scaled w t1) _ = WpCast (mk_wp_fun_co w (mkRepReflCo t1) co2)
-mkWpFun (WpCast co1) WpHole (Scaled w _) t2 = WpCast (mk_wp_fun_co w (mkSymCo co1) (mkRepReflCo t2))
-mkWpFun (WpCast co1) (WpCast co2) (Scaled w _) _ = WpCast (mk_wp_fun_co w (mkSymCo co1) co2)
-mkWpFun w_arg w_res t1 _ =
- -- In this case, we will desugar to a lambda
- --
- -- \x. w_res[ e w_arg[x] ]
- --
- -- To satisfy Note [Representation polymorphism invariants] in GHC.Core,
- -- it must be the case that both the lambda bound variable x and the function
- -- argument w_arg[x] have a fixed runtime representation, i.e. that both the
- -- "from" and "to" types of the first wrapper "w_arg" have a fixed runtime representation.
- --
- -- Unfortunately, we can't check this with an assertion here, because of
- -- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
- WpFun w_arg w_res t1
-
-mkWpEta :: [Id] -> HsWrapper -> HsWrapper
+-- ^ Smart constructor for `WpFun`
+-- Just removes clutter and optimises some common cases.
+--
+-- PRECONDITION: same as Note [WpFun-RR-INVARIANT]
+--
+-- Unfortunately, we can't check PRECONDITION with an assertion here, because of
+-- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
+mkWpFun w1 w2 st1@(Scaled m1 t1) t2
+ = case (w1,w2) of
+ (WpHole, WpHole) -> WpHole
+ (WpHole, WpCast co2) -> WpCast (mk_wp_fun_co m1 (mkRepReflCo t1) co2)
+ (WpCast co1, WpHole) -> WpCast (mk_wp_fun_co m1 (mkSymCo co1) (mkRepReflCo t2))
+ (WpCast co1, WpCast co2) -> WpCast (mk_wp_fun_co m1 (mkSymCo co1) co2)
+ (_, _) -> WpFun w1 w2 st1 t2
+
+mkWpSubType :: HsWrapper -> HsWrapper
+-- See (DSST2) in Note [Deep subsumption and WpSubType]
+mkWpSubType WpHole = WpHole
+mkWpSubType (WpCast co) = WpCast co
+mkWpSubType w = WpSubType w
+
+mkWpEta :: Type -> [Id] -> HsWrapper -> HsWrapper
-- (mkWpEta [x1, x2] wrap) [e]
-- = \x1. \x2. wrap[e x1 x2]
-- Just generates a bunch of WpFuns
-mkWpEta xs wrap = foldr eta_one wrap xs
+-- The incoming type is the type of the entire expression
+mkWpEta orig_fun_ty xs wrap = go orig_fun_ty xs
where
- eta_one x wrap = WpFun idHsWrapper wrap (idScaledType x)
+ go _ [] = wrap
+ go fun_ty (id:ids) = WpFun idHsWrapper (go res_ty ids) (idScaledType id) res_ty
+ where
+ res_ty = funResultTy fun_ty
mk_wp_fun_co :: Mult -> TcCoercionR -> TcCoercionR -> TcCoercionR
mk_wp_fun_co mult arg_co res_co
@@ -333,8 +425,9 @@ hsWrapDictBinders wrap = go wrap
where
go (WpEvLam dict_id) = unitBag dict_id
go (w1 `WpCompose` w2) = go w1 `unionBags` go w2
- go (WpFun _ w _) = go w
+ go (WpFun _ w _ _) = go w
go WpHole = emptyBag
+ go (WpSubType {}) = emptyBag -- See Note [Deep subsumption and WpSubType]
go (WpCast {}) = emptyBag
go (WpEvApp {}) = emptyBag
go (WpTyLam {}) = emptyBag
@@ -350,6 +443,7 @@ collectHsWrapBinders wrap = go wrap []
go :: HsWrapper -> [HsWrapper] -> ([Var], HsWrapper)
go (WpEvLam v) wraps = add_lam v (gos wraps)
go (WpTyLam v) wraps = add_lam v (gos wraps)
+ go (WpSubType w) wraps = go w wraps
go (WpCompose w1 w2) wraps = go w1 (w2:wraps)
go wrap wraps = ([], foldl' (<.>) wrap wraps)
@@ -358,6 +452,162 @@ collectHsWrapBinders wrap = go wrap []
add_lam v (vs,w) = (v:vs, w)
+
+optSubTypeHsWrapper :: HsWrapper -> HsWrapper
+-- This optimiser is used only on the payload of WpSubType
+-- It finds cases where the entire wrapper is a no-op
+-- See (DSST3) in Note [Deep subsumption and WpSubType]
+optSubTypeHsWrapper wrap
+ = opt wrap
+ where
+ opt :: HsWrapper -> HsWrapper
+ opt w = foldr (<.>) WpHole (opt1 w [])
+
+ opt1 :: HsWrapper -> [HsWrapper] -> [HsWrapper]
+ -- opt1 w ws = w <.> (foldr <.> WpHole ws)
+ -- INVARIANT: ws::[HsWrapper] is optimised
+ opt1 WpHole ws = ws
+ opt1 (WpSubType w) ws = opt1 w ws
+ opt1 (w1 `WpCompose` w2) ws = opt1 w1 (opt1 w2 ws)
+ opt1 (WpCast co) ws = opt_co co ws
+ opt1 (WpEvLam ev) ws = opt_ev_lam ev ws
+ opt1 (WpTyLam tv) ws = opt_ty_lam tv ws
+ opt1 (WpLet binds) ws = pushWpLet binds ws
+ opt1 (WpFun w1 w2 sty1 ty2) ws = opt_fun w1 w2 sty1 ty2 ws
+ opt1 w@(WpTyApp {}) ws = w : ws
+ opt1 w@(WpEvApp {}) ws = w : ws
+
+ -----------------
+ -- (WpTyLam a <.> WpTyApp a <.> w) = w
+ -- i.e. /\a. <hole> a --> <hole>
+ -- This is only valid if whatever fills the hole does not mention 'a'
+ -- But that's guaranteed in subtype-wrappers;
+ -- see (DSST1) in Note [Deep subsumption and WpSubType]
+ opt_ty_lam tv (WpTyApp ty : ws)
+ | Just tv' <- getTyVar_maybe ty
+ , tv==tv'
+ , all (tv `not_in`) ws
+ = ws
+
+ -- (WpTyLam a <.> WpCastCo co <.> w)
+ -- = WpCast (ForAllCo a co) (WpTyLam <.> w)
+ opt_ty_lam tv (WpCast co : ws)
+ = opt_co (mkHomoForAllCo tv co) (opt_ty_lam tv ws)
+
+ opt_ty_lam tv ws
+ = WpTyLam tv : ws
+
+ -----------------
+ -- (WpEvLam ev <.> WpEvAp ev <.> w) = w
+ -- Similar notes to WpTyLam
+ opt_ev_lam ev (WpEvApp ev_tm : ws)
+ | EvExpr (Var ev') <- ev_tm
+ , ev == ev'
+ , all (ev `not_in`) ws
+ = ws
+
+ -- (WpEvLam ev <.> WpCast co <.> w)
+ -- = WpCast (FunCo ev co) (WpEvLam <.> w)
+ opt_ev_lam ev (WpCast co : ws)
+ = opt_co fun_co (opt_ev_lam ev ws)
+ where
+ fun_co = mkFunCo Representational FTF_C_T
+ (mkNomReflCo ManyTy)
+ (mkRepReflCo (idType ev))
+ co
+
+ opt_ev_lam ev ws
+ = WpEvLam ev : ws
+
+ -----------------
+ -- WpCast co <.> WpCast co' <.> ws = WpCast (co;co') ws
+ opt_co co (WpCast co' : ws) = opt_co (co `mkTransCo` co') ws
+ opt_co co ws | isReflexiveCo co = ws
+ | otherwise = WpCast co : ws
+
+ ------------------
+ opt_fun w1 w2 sty1 ty2 ws
+ = case mkWpFun (opt w1) (opt w2) sty1 ty2 of
+ WpHole -> ws
+ WpCast co -> opt_co co ws
+ w -> w : ws
+
+ ------------------
+ -- Tiresome check that the lambda-bound type/evidence variable that we
+ -- want to eta-reduce isn't free in the rest of the wrapper
+ not_in :: TyVar -> HsWrapper -> Bool
+ not_in _ WpHole = True
+ not_in v (WpCast co) = not (anyFreeVarsOfCo (== v) co)
+ not_in v (WpTyApp ty) = not (anyFreeVarsOfType (== v) ty)
+ not_in v (WpFun w1 w2 _ _) = not_in v w1 && not_in v w2
+ not_in v (WpSubType w) = not_in v w
+ not_in v (WpCompose w1 w2) = not_in v w1 && not_in v w2
+ not_in v (WpEvApp (EvExpr e)) = not (v `elemVarSet` exprFreeVars e)
+ not_in _ (WpEvApp (EvTypeable {})) = False -- Giving up; conservative
+ not_in _ (WpEvApp (EvFun {})) = False -- Giving up; conservative
+ not_in _ (WpTyLam {}) = False -- Give up; conservative
+ not_in _ (WpEvLam {}) = False -- Ditto
+ not_in _ (WpLet {}) = False -- Ditto
+
+pushWpLet :: TcEvBinds -> [HsWrapper] -> [HsWrapper]
+-- See if we can transform
+-- WpLet binds <.> w1 <.> .. <.> wn --> w1' <.> .. <.> wn'
+-- by substitution.
+-- We do this just for the narrow case when
+-- - the `binds` are all just v=w, variables only
+-- - the wi are all WpTyApp, WpEvApp, or WpCast
+-- This is just enough to get us the eta-reductions that we seek
+pushWpLet tc_ev_binds ws
+ = case tc_ev_binds of
+ TcEvBinds {} -> pprPanic "pushWpLet" (ppr tc_ev_binds)
+ EvBinds binds
+ | isEmptyBag binds
+ -> ws
+ | Just env <- ev_bind_swizzle binds
+ -> case go env ws of
+ Just ws' -> ws'
+ Nothing -> bale_out
+ | otherwise
+ -> bale_out
+ where
+ bale_out = WpLet tc_ev_binds : ws
+
+ go :: IdEnv Id -> [HsWrapper] -> Maybe [HsWrapper]
+ go env (WpCast co : ws) = do { ws' <- go env ws
+ ; return (WpCast co : ws') }
+ go env (WpTyApp ty : ws) = do { ws' <- go env ws
+ ; return (WpTyApp ty : ws') }
+ go env (WpEvApp (EvExpr (Var v)) : ws)
+ = do { v' <- swizzle_id env v
+ ; ws' <- go env ws
+ ; return (WpEvApp (EvExpr (Var v')) : ws') }
+
+ go _ ws = case ws of
+ [] -> Just []
+ (_:_) -> Nothing -- Could not fully eliminate the WpLet
+
+ swizzle_id :: IdEnv Id -> Id -> Maybe Id
+ -- Nothing <=> ran out of fuel
+ -- This is just belt and braces; we should never build bottom evidence
+ swizzle_id env v = go 100 v
+ where
+ go :: Int -> EvId -> Maybe EvId
+ go fuel v
+ | fuel == 0 = Nothing
+ | Just v' <- lookupVarEnv env v = go (fuel-1) v'
+ | otherwise = Just v
+
+ ev_bind_swizzle :: Bag EvBind -> Maybe (IdEnv Id)
+ -- Succeeds only if the bindings are all var-to-var bindings
+ ev_bind_swizzle evbs = foldl' do_one (Just emptyVarEnv) evbs
+ where
+ do_one :: Maybe (IdEnv Id) -> EvBind -> Maybe (IdEnv Id)
+ do_one Nothing _ = Nothing
+ do_one (Just swizzle) (EvBind {eb_lhs = bndr, eb_rhs = rhs})
+ = case rhs of
+ EvExpr (Var v) -> Just (extendVarEnv swizzle bndr v)
+ _ -> Nothing
+
{-
************************************************************************
* *
@@ -1018,8 +1268,9 @@ pprHsWrapper wrap pp_thing_inside
-- True <=> appears in function application position
-- False <=> appears as body of let or lambda
help it WpHole = it
- help it (WpCompose f1 f2) = help (help it f2) f1
- help it (WpFun f1 f2 (Scaled w t1)) = add_parens $ text "\\(x" <> dcolon <> brackets (ppr w) <> ppr t1 <> text ")." <+>
+ help it (WpCompose w1 w2) = help (help it w2) w1
+ help it (WpSubType w) = no_parens $ text "subtype" <> braces (help it w False)
+ help it (WpFun f1 f2 (Scaled w t1) _) = add_parens $ text "\\(x" <> dcolon <> brackets (ppr w) <> ppr t1 <> text ")." <+>
help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False
help it (WpCast co) = add_parens $ sep [it False, nest 2 (text "|>"
<+> pprParendCo co)]
=====================================
compiler/GHC/Tc/Utils/Concrete.hs
=====================================
@@ -626,8 +626,12 @@ hasFixedRuntimeRep :: HasDebugCallStack
-- @ki@ is concrete, and @co :: ty ~# ty'@.
-- That is, @ty'@ has a syntactically fixed RuntimeRep
-- in the sense of Note [Fixed RuntimeRep].
-hasFixedRuntimeRep frr_ctxt ty =
- checkFRR_with (fmap (fmap coToMCo) . unifyConcrete_kind (fsLit "cx") . ConcreteFRR) frr_ctxt ty
+hasFixedRuntimeRep frr_ctxt ty
+ = checkFRR_with unify_conc frr_ctxt ty
+ where
+ unify_conc frr_orig ki
+ = do { co <- unifyConcrete_kind (fsLit "cx") (ConcreteFRR frr_orig) ki
+ ; return (coToMCo co) }
-- | Like 'hasFixedRuntimeRep', but we perform an eager syntactic check.
--
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -148,7 +148,7 @@ matchActualFunTy
-- (Both are used only for error messages)
-> TcRhoType
-- ^ Type to analyse: a TcRhoType
- -> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
+ -> TcM (TcCoercion, Scaled TcSigmaTypeFRR, TcSigmaType)
-- This function takes in a type to analyse (a RhoType) and returns
-- an argument type and a result type (splitting apart a function arrow).
-- The returned argument type is a SigmaType with a fixed RuntimeRep;
@@ -157,7 +157,7 @@ matchActualFunTy
-- See Note [matchActualFunTy error handling] for the first three arguments
-- If (wrap, arg_ty, res_ty) = matchActualFunTy ... fun_ty
--- then wrap :: fun_ty ~> (arg_ty -> res_ty)
+-- then wrap :: fun_ty ~~> (arg_ty -> res_ty)
-- and NB: res_ty is an (uninstantiated) SigmaType
matchActualFunTy herald mb_thing err_info fun_ty
@@ -172,13 +172,13 @@ matchActualFunTy herald mb_thing err_info fun_ty
-- hide the forall inside a meta-variable
go :: TcRhoType -- The type we're processing, perhaps after
-- expanding type synonyms
- -> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
+ -> TcM (TcCoercion, Scaled TcSigmaTypeFRR, TcSigmaType)
go ty | Just ty' <- coreView ty = go ty'
go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty })
= assert (isVisibleFunArg af) $
do { hasFixedRuntimeRep_syntactic (FRRExpectedFunTy herald 1) arg_ty
- ; return (idHsWrapper, Scaled w arg_ty, res_ty) }
+ ; return (mkNomReflCo fun_ty, Scaled w arg_ty, res_ty) }
go ty@(TyVarTy tv)
| isMetaTyVar tv
@@ -210,7 +210,7 @@ matchActualFunTy herald mb_thing err_info fun_ty
; res_ty <- newOpenFlexiTyVarTy
; let unif_fun_ty = mkScaledFunTys [arg_ty] res_ty
; co <- unifyType mb_thing fun_ty unif_fun_ty
- ; return (mkWpCastN co, arg_ty, res_ty) }
+ ; return (co, arg_ty, res_ty) }
------------
mk_ctxt :: TcType -> TidyEnv -> ZonkM (TidyEnv, ErrCtxtMsg)
@@ -249,8 +249,10 @@ matchActualFunTys :: ExpectedFunTyOrigin -- ^ See Note [Herald for matchExpected
-> Arity
-> TcSigmaType
-> TcM (HsWrapper, [Scaled TcSigmaTypeFRR], TcRhoType)
--- If matchActualFunTys n ty = (wrap, [t1,..,tn], res_ty)
--- then wrap : ty ~> (t1 -> ... -> tn -> res_ty)
+-- NB: Called only from `tcSynArgA`, and hence scheduled for destruction
+--
+-- If matchActualFunTys n fun_ty = (wrap, [t1,..,tn], res_ty)
+-- then wrap : fun_ty ~~> (t1 -> ... -> tn -> res_ty)
-- and res_ty is a RhoType
-- NB: the returned type is top-instantiated; it's a RhoType
matchActualFunTys herald ct_orig n_val_args_wanted top_ty
@@ -265,15 +267,13 @@ matchActualFunTys herald ct_orig n_val_args_wanted top_ty
go 0 _ fun_ty = return (idHsWrapper, [], fun_ty)
go n so_far fun_ty
- = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTy
- herald Nothing
- (n_val_args_wanted, top_ty)
- fun_ty
- ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1
+ = do { (co1, arg_ty1, res_ty1) <- matchActualFunTy herald Nothing
+ (n_val_args_wanted, top_ty) fun_ty
+ ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1
; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty
-- NB: arg_ty1 comes from matchActualFunTy, so it has
- -- a syntactically fixed RuntimeRep as needed to call mkWpFun.
- ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) }
+ -- a syntactically fixed RuntimeRep
+ ; return (wrap_fun2 <.> mkWpCastN co1, arg_ty1:arg_tys, res_ty) }
{-
************************************************************************
@@ -459,7 +459,7 @@ tcSkolemiseGeneral ds_flag ctxt top_ty expected_ty thing_inside
tcSkolemiseCompleteSig :: TcCompleteSig
-> ([ExpPatType] -> TcRhoType -> TcM result)
-> TcM (HsWrapper, result)
--- ^ The wrapper has type: spec_ty ~> expected_ty
+-- ^ The wrapper has type: spec_ty ~~> expected_ty
-- See Note [Skolemisation] for the differences between
-- tcSkolemiseCompleteSig and tcTopSkolemise
@@ -790,7 +790,7 @@ matchExpectedFunTys :: forall a.
-> ([ExpPatType] -> ExpRhoType -> TcM a)
-> TcM (HsWrapper, a)
-- If matchExpectedFunTys n ty = (wrap, _)
--- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
+-- then wrap : (t1 -> ... -> tn -> ty_r) ~~> ty,
-- where [t1, ..., tn], ty_r are passed to the thing_inside
--
-- Unconditionally concludes by skolemising any trailing invisible
@@ -865,12 +865,13 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
, ft_arg = arg_ty, ft_res = res_ty })
= assert (isVisibleFunArg af) $
do { let arg_pos = arity - n_req + 1 -- 1 for the first argument etc
- ; (arg_co, arg_ty) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty
+ ; (arg_co, arg_ty_frr) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty
+ ; let arg_sty_frr = Scaled mult arg_ty_frr
; (wrap_res, result) <- check (n_req - 1)
- (mkCheckExpFunPatTy (Scaled mult arg_ty) : rev_pat_tys)
+ (mkCheckExpFunPatTy arg_sty_frr : rev_pat_tys)
res_ty
; let wrap_arg = mkWpCastN arg_co
- fun_wrap = mkWpFun wrap_arg wrap_res (Scaled mult arg_ty) res_ty
+ fun_wrap = mkWpFun wrap_arg wrap_res arg_sty_frr res_ty
; return (fun_wrap, result) }
----------------------------
@@ -1407,7 +1408,7 @@ tcSubTypePat :: CtOrigin -> UserTypeCtxt
-- Used in patterns; polarity is backwards compared
-- to tcSubType
-- If wrap = tc_sub_type_et t1 t2
--- => wrap :: t1 ~> t2
+-- => wrap :: t1 ~~> t2
tcSubTypePat inst_orig ctxt (Check ty_actual) ty_expected
= tc_sub_type unifyTypeET inst_orig ctxt ty_actual ty_expected
@@ -1427,11 +1428,12 @@ tcSubTypeDS :: HsExpr GhcRn
-- DeepSubsumption <=> when checking, this type
-- is deeply skolemised
-> TcM HsWrapper
--- Only one call site, in GHC.Tc.Gen.App.tcApp
+-- Only one call site, in GHC.Tc.Gen.App.checkResultTy
tcSubTypeDS rn_expr act_rho exp_rho
- = tc_sub_type_deep Top (unifyExprType rn_expr) orig GenSigCtxt act_rho exp_rho
- where
- orig = exprCtOrigin rn_expr
+ = do { wrap <- tc_sub_type_deep Top (unifyExprType rn_expr)
+ (exprCtOrigin rn_expr)
+ GenSigCtxt act_rho exp_rho
+ ; return (mkWpSubType wrap) }
---------------
@@ -1456,7 +1458,7 @@ tcSubTypeSigma :: CtOrigin -- where did the actual type arise / why are we
-> TcSigmaType -> TcSigmaType -> TcM HsWrapper
-- External entry point, but no ExpTypes on either side
-- Checks that actual <= expected
--- Returns HsWrapper :: actual ~ expected
+-- Returns HsWrapper :: actual ~~> expected
tcSubTypeSigma orig ctxt ty_actual ty_expected
= tc_sub_type (unifyType Nothing) orig ctxt ty_actual ty_expected
@@ -1495,7 +1497,7 @@ tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify
-> TcM HsWrapper
-- Checks that actual_ty is more polymorphic than expected_ty
-- If wrap = tc_sub_type t1 t2
--- => wrap :: t1 ~> t2
+-- => wrap :: t1 ~~> t2
--
-- The "how to unify argument" is always a call to `uType TypeLevel orig`,
-- but with different ways of constructing the CtOrigin `orig` from
@@ -1504,7 +1506,8 @@ tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify
----------------------
tc_sub_type unify inst_orig ctxt ty_actual ty_expected
= do { ds_flag <- getDeepSubsumptionFlag
- ; tc_sub_type_ds Top ds_flag unify inst_orig ctxt ty_actual ty_expected }
+ ; wrap <- tc_sub_type_ds Top ds_flag unify inst_orig ctxt ty_actual ty_expected
+ ; return (mkWpSubType wrap) }
----------------------
tc_sub_type_ds :: Position p -- ^ position in the type (for error messages only)
@@ -1753,59 +1756,59 @@ we deal with function arrows. Suppose we have:
ty_actual = act_arg -> act_res
ty_expected = exp_arg -> exp_res
-To produce fun_wrap :: (act_arg -> act_res) ~> (exp_arg -> exp_res), we use
+To produce fun_wrap :: (act_arg -> act_res) ~~> (exp_arg -> exp_res), we use
the fact that the function arrow is contravariant in its argument type and
covariant in its result type. Thus we recursively perform subtype checks
on the argument types (with actual/expected switched) and the result types,
to get:
- arg_wrap :: exp_arg ~> act_arg -- NB: expected/actual have switched sides
- res_wrap :: act_res ~> exp_res
+ arg_wrap :: exp_arg ~~> act_arg -- NB: expected/actual have switched sides
+ res_wrap :: act_res ~~> exp_res
Then fun_wrap = mkWpFun arg_wrap res_wrap.
-Wrinkle [Representation-polymorphism checking during subtyping]
+Note [Representation-polymorphism checking during subtyping]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When doing deep subsumption in `tc_sub_type_deep`, looking under function arrows,
+we would usually build a `WpFun` HsWrapper. When desugared, we get eta-expansion:
- Inserting a WpFun HsWrapper amounts to impedance matching in deep subsumption
- via eta-expansion:
+ f ==> \(x :: exp_arg). res_wrap [ f (arg_wrap [x]) ]
- f ==> \ (x :: exp_arg) -> res_wrap [ f (arg_wrap [x]) ]
+Since we produce a lambda, we must enforce the representation polymorphism
+invariants described in Note [Representation polymorphism invariants] in GHC.Core.
+That is, we must ensure that both
+ - x (the lambda binder), and
+ - (arg_wrap [x]) (the function argument)
+have a fixed runtime representation.
- As we produce a lambda, we must enforce the representation polymorphism
- invariants described in Note [Representation polymorphism invariants] in GHC.Core.
- That is, we must ensure that both x (the lambda binder) and (arg_wrap [x]) (the function argument)
- have a fixed runtime representation.
+But we don't /always/ need to produce a `WpFun`: if both argument and result wrappers
+are merely coercions, we can produce a `WpCast co` instead of a `WpFun`. In that
+case there is no eta-expansion, and hence no need for FRR checks.
- Note however that desugaring mkWpFun does not always introduce a lambda: if
- both the argument and result HsWrappers are casts, then a FunCo cast suffices,
- in which case we should not perform representation-polymorphism checking.
+Here's a contrived example (there are undoubtedly more natural examples)
+(see testsuite/tests/rep-poly/NoEtaRequired):
- This means that, in the FunTy/FunTy case of tc_sub_type_deep, we can skip
- the representation-polymorphism checks if the produced argument and result
- wrappers are identities or casts.
- It is important to do so, otherwise we reject valid programs.
+ type Id :: k -> k
+ type family Id a where
- Here's a contrived example (there are undoubtedly more natural examples)
- (see testsuite/tests/rep-poly/NoEtaRequired):
+ type T :: TYPE r -> TYPE (Id r)
+ type family T a where
- type Id :: k -> k
- type family Id a where
+ test :: forall r (a :: TYPE r). a :~~: T a -> ()
+ test HRefl =
+ let
+ f :: (a -> a) -> ()
+ f _ = ()
+ g :: T a -> T a
+ g = undefined
+ in f g
- type T :: TYPE r -> TYPE (Id r)
- type family T a where
+We don't need to eta-expand `g` to make `f g` typecheck; a cast
+suffices. Hence we should not perform representation-polymorphism
+checks; they would fail here.
- test :: forall r (a :: TYPE r). a :~~: T a -> ()
- test HRefl =
- let
- f :: (a -> a) -> ()
- f _ = ()
- g :: T a -> T a
- g = undefined
- in f g
-
- We don't need to eta-expand `g` to make `f g` typecheck; a cast suffices.
- Hence we should not perform representation-polymorphism checks; they would
- fail here.
+All this is done by `mkWpFun_FRR`, which checks for the cast/cast case and
+returns a `FunCo` if so.
Note [Setting the argument context]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1947,7 +1950,7 @@ getDeepSubsumptionFlag = do { ds <- xoptM LangExt.DeepSubsumption
-- | 'tc_sub_type_deep' is where the actual work happens for deep subsumption.
--
-- Given @ty_actual@ (a sigma-type) and @ty_expected@ (deeply skolemised, i.e.
--- a deep rho type), it returns an 'HsWrapper' @wrap :: ty_actual ~> ty_expected@.
+-- a deep rho type), it returns an 'HsWrapper' @wrap :: ty_actual ~~> ty_expected@.
tc_sub_type_deep :: HasDebugCallStack
=> Position p -- ^ Position in the type (for error messages only)
-> (TcType -> TcType -> TcM TcCoercionN) -- ^ How to unify
@@ -1958,7 +1961,7 @@ tc_sub_type_deep :: HasDebugCallStack
-> TcM HsWrapper
-- If wrap = tc_sub_type_deep t1 t2
--- => wrap :: t1 ~> t2
+-- => wrap :: t1 ~~> t2
-- Here is where the work actually happens!
-- Precondition: ty_expected is deeply skolemised
@@ -2015,8 +2018,8 @@ tc_sub_type_deep pos unify inst_orig ctxt ty_actual ty_expected
; unify_wrap <- just_unify exp_funTy ty_e
; fun_wrap <- go_fun af1 act_mult act_arg act_res af1 exp_mult exp_arg exp_res
; return $ unify_wrap <.> fun_wrap
- -- unify_wrap :: exp_funTy ~> ty_e
- -- fun_wrap :: ty_a ~> exp_funTy
+ -- unify_wrap :: exp_funTy ~~> ty_e
+ -- fun_wrap :: ty_a ~~> exp_funTy
}
go1 ty_a (FunTy { ft_af = af2, ft_mult = exp_mult, ft_arg = exp_arg, ft_res = exp_res })
| isVisibleFunArg af2
@@ -2028,8 +2031,8 @@ tc_sub_type_deep pos unify inst_orig ctxt ty_actual ty_expected
; unify_wrap <- just_unify ty_a act_funTy
; fun_wrap <- go_fun af2 act_mult act_arg act_res af2 exp_mult exp_arg exp_res
; return $ fun_wrap <.> unify_wrap
- -- unify_wrap :: ty_a ~> act_funTy
- -- fun_wrap :: act_funTy ~> ty_e
+ -- unify_wrap :: ty_a ~~> act_funTy
+ -- fun_wrap :: act_funTy ~~> ty_e
}
-- Otherwise, revert to unification.
@@ -2064,17 +2067,28 @@ mkWpFun_FRR
-> Position p
-> FunTyFlag -> Type -> TcType -> Type -- actual FunTy
-> FunTyFlag -> Type -> TcType -> Type -- expected FunTy
- -> HsWrapper -- ^ exp_arg ~> act_arg
- -> HsWrapper -- ^ act_res ~> exp_res
- -> TcM HsWrapper -- ^ act_funTy ~> exp_funTy
+ -> HsWrapper -- ^ exp_arg ~~> act_arg
+ -> HsWrapper -- ^ act_res ~~> exp_res
+ -> TcM HsWrapper -- ^ (act_arg->act_res) ~~> (exp_arg->exp_res)
mkWpFun_FRR unify pos act_af act_mult act_arg act_res exp_af exp_mult exp_arg exp_res arg_wrap res_wrap
- = do { ((exp_arg_co, exp_arg_frr), (act_arg_co, _act_arg_frr)) <-
- if needs_frr_checks
- -- See Wrinkle [Representation-polymorphism checking during subtyping]
- then do { exp_frr_wrap <- hasFixedRuntimeRep (frr_ctxt True ) exp_arg
- ; act_frr_wrap <- hasFixedRuntimeRep (frr_ctxt False) act_arg
- ; return (exp_frr_wrap, act_frr_wrap) }
- else return ((mkNomReflCo exp_arg, exp_arg), (mkNomReflCo act_arg, act_arg))
+ | Just arg_co <- getWpCo_maybe arg_wrap act_arg -- arg_co :: exp_arg ~R# act_arg
+ , Just res_co <- getWpCo_maybe res_wrap act_res -- res_co :: act_res ~R# exp_res
+ = -- The argument and result wrappers are both hole or cast;
+ -- so we can make do with a FunCo
+ -- See Note [Representation-polymorphism checking during subtyping]
+ do { mult_co <- unify act_mult exp_mult
+ ; let the_co = mkFunCo2 Representational act_af exp_af mult_co (mkSymCo arg_co) res_co
+ ; return (mkWpCastR the_co) }
+
+ | otherwise
+ = -- We need a full WpFun, with the eta-expansion that it entails
+ -- And hence we must add fixed-runtime-rep checks so that the eta-expansion is OK
+ -- See Note [Representation-polymorphism checking during subtyping]
+ do { (exp_arg_co, exp_arg_frr) <- hasFixedRuntimeRep (frr_ctxt True ) exp_arg
+ ; (act_arg_co, _act_arg_frr) <- hasFixedRuntimeRep (frr_ctxt False) act_arg
+ -- exp_arg_frr, act_arg_frr :: Type have fixed runtime-reps
+ -- exp_arg_co :: exp_arg ~ exp_arg_frr Usually Refl
+ -- act_arg_co :: act_arg ~ act_arg_frr Usually Refl
-- Enforce equality of multiplicities (not the more natural sub-multiplicity).
-- See Note [Multiplicity in deep subsumption]
@@ -2083,46 +2097,36 @@ mkWpFun_FRR unify pos act_af act_mult act_arg act_res exp_af exp_mult exp_arg ex
-- equality to be Refl, but it might well not be (#26332).
; let
- exp_arg_fun_co =
+ exp_arg_fun_co = -- (exp_arg_frr -> exp_res) ~ (exp_arg -> exp_res)
mkFunCo Nominal exp_af
- (mkReflCo Nominal exp_mult)
+ (mkNomReflCo exp_mult)
(mkSymCo exp_arg_co)
- (mkReflCo Nominal exp_res)
- act_arg_fun_co =
+ (mkNomReflCo exp_res)
+ act_arg_fun_co = -- (act_arg -> act_res) ~ (act_arg_frr -> act_res)
mkFunCo Nominal act_af
act_arg_mult_co
act_arg_co
- (mkReflCo Nominal act_res)
- arg_wrap_frr =
+ (mkNomReflCo act_res)
+ arg_wrap_frr = -- exp_arg_frr ~~> act_arg_frr
mkWpCastN (mkSymCo exp_arg_co) <.> arg_wrap <.> mkWpCastN act_arg_co
- -- exp_arg_co :: exp_arg ~> exp_arg_frr
- -- act_arg_co :: act_arg ~> act_arg_frr
- -- arg_wrap :: exp_arg ~> act_arg
- -- arg_wrap_frr :: exp_arg_frr ~> act_arg_frr
- ; return $
- mkWpCastN exp_arg_fun_co
+ ; return $ -- Whole thing :: (act_arg->act_res) ~~> (exp_arg->exp_ress)
+ mkWpCastN exp_arg_fun_co -- (exp_ar_frr->exp_res) ~~> (exp_arg->exp_res)
<.>
mkWpFun arg_wrap_frr res_wrap (Scaled exp_mult exp_arg_frr) exp_res
- <.>
- mkWpCastN act_arg_fun_co
+ <.> -- (act_arg_frr->act_res) ~~> (exp_arg_frr->exp_res)
+ mkWpCastN act_arg_fun_co -- (act_arg->act_res) ~~> (act_arg_frr->act_res)
}
where
- needs_frr_checks :: Bool
- needs_frr_checks =
- not (hole_or_cast arg_wrap)
- ||
- not (hole_or_cast res_wrap)
- hole_or_cast :: HsWrapper -> Bool
- hole_or_cast WpHole = True
- hole_or_cast (WpCast {}) = True
- hole_or_cast _ = False
+ getWpCo_maybe :: HsWrapper -> Type -> Maybe CoercionR
+ -- See if a HsWrapper is just a coercion
+ getWpCo_maybe WpHole ty = Just (mkRepReflCo ty)
+ getWpCo_maybe (WpCast co) _ = Just co
+ getWpCo_maybe _ _ = Nothing
+
frr_ctxt :: Bool -> FixedRuntimeRepContext
- frr_ctxt is_exp_ty =
- FRRDeepSubsumption
- { frrDSExpected = is_exp_ty
- , frrDSPosition = pos
- }
+ frr_ctxt is_exp_ty = FRRDeepSubsumption { frrDSExpected = is_exp_ty
+ , frrDSPosition = pos }
-----------------------
deeplySkolemise :: SkolemInfo -> TcSigmaType
@@ -2146,9 +2150,9 @@ deeplySkolemise skol_info ty
; let tvs = binderVars bndrs
tvs1 = binderVars bndrs1
tv_prs1 = map tyVarName tvs `zip` bndrs1
- ; return ( mkWpEta ids1 (mkWpTyLams tvs1
- <.> mkWpEvLams ev_vars1
- <.> wrap)
+ ; return ( mkWpEta ty ids1 (mkWpTyLams tvs1
+ <.> mkWpEvLams ev_vars1
+ <.> wrap)
, tv_prs1 ++ tvs_prs2
, ev_vars1 ++ ev_vars2
, mkScaledFunTys arg_tys' rho ) }
@@ -2182,7 +2186,7 @@ deeplyInstantiate orig ty
; ids1 <- newSysLocalIds (fsLit "di") arg_tys'
; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
; (wrap2, rho2) <- go subst' rho
- ; return (mkWpEta ids1 (wrap2 <.> wrap1),
+ ; return (mkWpEta ty ids1 (wrap2 <.> wrap1),
mkScaledFunTys arg_tys' rho2) }
| otherwise
=====================================
compiler/GHC/Tc/Zonk/Type.hs
=====================================
@@ -1233,13 +1233,16 @@ zonk_cmd_top (HsCmdTop (CmdTopTc stack_tys ty ids) cmd)
-------------------------------------------------------------------------
zonkCoFn :: HsWrapper -> ZonkBndrTcM HsWrapper
zonkCoFn WpHole = return WpHole
+zonkCoFn (WpSubType w) = do { w' <- zonkCoFn w
+ ; return (WpSubType w') }
zonkCoFn (WpCompose c1 c2) = do { c1' <- zonkCoFn c1
; c2' <- zonkCoFn c2
; return (WpCompose c1' c2') }
-zonkCoFn (WpFun c1 c2 t1) = do { c1' <- zonkCoFn c1
- ; c2' <- zonkCoFn c2
- ; t1' <- noBinders $ zonkScaledTcTypeToTypeX t1
- ; return (WpFun c1' c2' t1') }
+zonkCoFn (WpFun c1 c2 t1 t2) = do { c1' <- zonkCoFn c1
+ ; c2' <- zonkCoFn c2
+ ; t1' <- noBinders $ zonkScaledTcTypeToTypeX t1
+ ; t2' <- noBinders $ zonkTcTypeToTypeX t2
+ ; return (WpFun c1' c2' t1' t2') }
zonkCoFn (WpCast co) = WpCast <$> noBinders (zonkCoToCo co)
zonkCoFn (WpEvLam ev) = WpEvLam <$> zonkEvBndrX ev
zonkCoFn (WpEvApp arg) = WpEvApp <$> noBinders (zonkEvTerm arg)
=====================================
testsuite/tests/simplCore/should_compile/T26349.hs
=====================================
@@ -0,0 +1,11 @@
+{-# LANGUAGE DeepSubsumption, RankNTypes #-}
+module T26349 where
+
+{-# SPECIALIZE INLINE mapTCMT :: (forall b. IO b -> IO b) -> IO a -> IO a #-}
+mapTCMT :: (forall b. m b -> n b) -> m a -> n a
+mapTCMT f m = f m
+
+{-
+ We'll check
+ tcExpr (mapTCMT) (Check ((forall b. IO b -> IO b) -> IO a_sk -> IO a_sk))
+-}
=====================================
testsuite/tests/simplCore/should_compile/T26349.stderr
=====================================
@@ -0,0 +1,3 @@
+==================== Tidy Core rules ====================
+"USPEC mapTCMT @(*) @IO @IO @_"
+ forall (@a). mapTCMT @(*) @IO @IO @a = mapTCMT_$smapTCMT @a
=====================================
testsuite/tests/simplCore/should_compile/all.T
=====================================
@@ -559,3 +559,4 @@ test('T26051', [ grep_errmsg(r'\$wspecMe')
test('T26115', [grep_errmsg(r'DFun')], compile, ['-O -ddump-simpl -dsuppress-uniques'])
test('T26116', normal, compile, ['-O -ddump-rules'])
test('T26117', [grep_errmsg(r'==')], compile, ['-O -ddump-simpl -dsuppress-uniques'])
+test('T26349', normal, compile, ['-O -ddump-rules'])
=====================================
testsuite/tests/simplCore/should_compile/rule2.stderr
=====================================
@@ -10,18 +10,15 @@
==================== Grand total simplifier statistics ====================
-Total ticks: 13
+Total ticks: 11
-2 PreInlineUnconditionally
- 1 ds
- 1 f
+1 PreInlineUnconditionally 1 f
2 UnfoldingDone
1 GHC.Internal.Base.id
1 Roman.bar
1 RuleFired 1 foo/bar
1 LetFloatFromLet 1
-7 BetaReduction
- 1 ds
+6 BetaReduction
1 f
1 a
1 m
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a7c1c88a2d0cde2ae7fe75c14abd5d…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a7c1c88a2d0cde2ae7fe75c14abd5d…
You're receiving this email because of your account on gitlab.haskell.org.
1
0
[Git][ghc/ghc][wip/T24464] 16 commits: Refactor fundep solving
by Simon Peyton Jones (@simonpj) 04 Nov '25
by Simon Peyton Jones (@simonpj) 04 Nov '25
04 Nov '25
Simon Peyton Jones pushed to branch wip/T24464 at Glasgow Haskell Compiler / GHC
Commits:
fcf6331e by Richard Eisenberg at 2025-11-03T08:33:05+00:00
Refactor fundep solving
This commit is a large-scale refactor of the increasingly-messy code that
handles functional dependencies. It has virtually no effect on what compiles
but improves error messages a bit. And it does the groundwork for #23162.
The big picture is described in
Note [Overview of functional dependencies in type inference]
in GHC.Tc.Solver.FunDeps
* New module GHC.Tc.Solver.FunDeps contains all the fundep-handling
code for the constraint solver.
* Fundep-equalities are solved in a nested scope; they may generate
unifications but otherwise have no other effect.
See GHC.Tc.Solver.FunDeps.solveFunDeps
The nested needs to start from the Givens in the inert set, but
not the Wanteds; hence a new function `resetInertCans`, used in
`nestFunDepsTcS`.
* That in turn means that fundep equalities never show up in error
messages, so the complicated FunDepOrigin tracking can all disappear.
* We need to be careful about tracking unifications, so we kick out
constraints from the inert set after doing unifications. Unification
tracking has been majorly reformed: see Note [WhatUnifications] in
GHC.Tc.Utils.Unify.
A good consequence is that the hard-to-grok `resetUnificationFlag`
has been replaced with a simpler use of
`reportCoarseGrainUnifications`
Smaller things:
* Rename `FunDepEqn` to `FunDepEqns` since it contains multiple
type equalities.
Some compile time improvement
Metrics: compile_time/bytes allocated
Baseline
Test value New value Change
---------------------- --------------------------------------
T5030(normal) 173,839,232 148,115,248 -14.8% GOOD
hard_hole_fits(normal) 286,768,048 284,015,416 -1.0%
geo. mean -0.2%
minimum -14.8%
maximum +0.3%
Metric Decrease:
T5030
- - - - -
231adc30 by Simon Peyton Jones at 2025-11-03T08:33:05+00:00
QuickLook's tcInstFun should make instantiation variables directly
tcInstFun must make "instantiation variables", not regular
unification variables, when instantiating function types. That was
previously implemented by a hack: set the /ambient/ level to QLInstTyVar.
But the hack finally bit me, when I was refactoring WhatUnifications.
And it was always wrong: see the now-expunged (TCAPP2) note.
This commit does it right, by making tcInstFun call its own
instantiation functions. That entails a small bit of duplication,
but the result is much, much cleaner.
- - - - -
39d4a24b by Simon Peyton Jones at 2025-11-03T08:33:05+00:00
Build implication for constraints from (static e)
This commit addresses #26466, by buiding an implication for the
constraints arising from a (static e) form. The implication has
a special ic_info field of StaticFormSkol, which tells the constraint
solver to use an empty set of Givens.
See (SF3) in Note [Grand plan for static forms]
in GHC.Iface.Tidy.StaticPtrTable
This commit also reinstates an `assert` in GHC.Tc.Solver.Equality.
The test `StaticPtrTypeFamily` was failing with an assertion failure,
but it now works.
- - - - -
2e2aec1e by Simon Peyton Jones at 2025-11-03T08:33:05+00:00
Comments about defaulting representation equalities
- - - - -
52a4d1da by Simon Peyton Jones at 2025-11-03T08:33:05+00:00
Improve tracking of rewriter-sets
This refactor substantially improves the treatment of so-called
"rewriter-sets" in the constraint solver.
The story is described in the rewritten
Note [Wanteds rewrite Wanteds: rewriter-sets]
in GHC.Tc.Types.Constraint
Some highlights
* Trace the free coercion holes of a filled CoercionHole,
in CoercionPlusHoles. See Note [Coercion holes] (COH5)
This avoids taking having to take the free coercion variables
of a coercion when zonking a rewrriter-set
* Many knock on changes
* Make fillCoercionHole take CoercionPlusHoles as its argument
rather than to separate arguments.
* Similarly setEqIfWanted, setWantedE, wrapUnifierAndEmit.
* Be more careful about passing the correct CoHoleSet to
`rewriteEqEvidence` and friends
* Make kickOurAfterFillingCoercionHole more clever. See
new Note [Kick out after filling a coercion hole]
Smaller matters
* Rename RewriterSet to CoHoleSet
* Add special-case helper `rewriteEqEvidenceSwapOnly`
- - - - -
3e78e1ba by Simon Peyton Jones at 2025-11-03T08:33:05+00:00
Tidy up constraint solving for foralls
* In `can_eq_nc_forall` make sure to track Givens that are used
in the nested solve step.
* Tiny missing-swap bug-fix in `lookup_eq_in_qcis`
* Fix some leftover mess from
commit 14123ee646f2b9738a917b7cec30f9d3941c13de
Author: Simon Peyton Jones <simon.peytonjones(a)gmail.com>
Date: Wed Aug 20 00:35:48 2025 +0100
Solve forall-constraints via an implication, again
Specifically, trySolveImplication is now dead.
- - - - -
973f2c25 by Simon Peyton Jones at 2025-11-03T08:33:05+00:00
Do not treat CoercionHoles as free variables in coercions
This fixes a long-standing wart in the free-variable finder;
now CoercionHoles are no longer treated as a "free variable"
of a coercion.
I got big and unexpected performance regressions when making
this change. Turned out that CallArity didn't discover that
the free variable finder could be eta-expanded, which gave very
poor code.
So I re-used Note [The one-shot state monad trick] for Endo,
resulting in GHC.Utils.EndoOS. Very simple, big win.
- - - - -
c2b8a0f9 by Simon Peyton Jones at 2025-11-03T08:33:05+00:00
Update debug-tracing in CallArity
No effect on behaviour, and commented out anyway
- - - - -
9aa5ee99 by Simon Peyton Jones at 2025-11-03T08:33:28+00:00
Comments only -- remove dangling Note references
- - - - -
6683f183 by Simon Peyton Jones at 2025-11-03T08:33:28+00:00
Accept error message wibbles
- - - - -
3ba3d9f9 by Luite Stegeman at 2025-11-04T00:59:41-05:00
rts: fix eager black holes: record mutated closure and fix assertion
This fixes two problems with handling eager black holes, introduced
by a1de535f762bc23d4cf23a5b1853591dda12cdc9.
- the closure mutation must be recorded even for eager black holes,
since the mutator has mutated it before calling threadPaused
- The assertion that an unmarked eager black hole must be owned by
the TSO calling threadPaused is incorrect, since multiple threads
can race to claim the black hole.
fixes #26495
- - - - -
cd972168 by Simon Peyton Jones at 2025-11-04T16:07:57+00:00
Start at moving static forms straight to top level
Just for CI. Needs documentation.
- - - - -
ce741189 by Simon Peyton Jones at 2025-11-04T16:07:57+00:00
Wibble
- - - - -
2134952a by Simon Peyton Jones at 2025-11-04T16:07:57+00:00
Fix desugaring
- - - - -
40ab10aa by Simon Peyton Jones at 2025-11-04T16:07:57+00:00
Wibbles
- - - - -
4b67d5ad by Simon Peyton Jones at 2025-11-04T17:42:42+00:00
Work in progress [skip ci]
- - - - -
108 changed files:
- compiler/GHC/Core/Opt/CallArity.hs
- compiler/GHC/Core/Opt/Simplify/Iteration.hs
- compiler/GHC/Core/Opt/Simplify/Utils.hs
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Hs/Binds.hs
- compiler/GHC/Hs/Decls.hs
- compiler/GHC/Hs/Instances.hs
- compiler/GHC/Hs/Utils.hs
- compiler/GHC/HsToCore.hs
- compiler/GHC/HsToCore/Expr.hs
- compiler/GHC/HsToCore/Monad.hs
- compiler/GHC/HsToCore/Types.hs
- compiler/GHC/Iface/Tidy/StaticPtrTable.hs
- compiler/GHC/Runtime/Eval.hs
- compiler/GHC/Tc/Deriv.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Instance/FunDeps.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Default.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- + compiler/GHC/Tc/Solver/FunDeps.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Irred.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Rewrite.hs
- compiler/GHC/Tc/Solver/Solve.hs
- compiler/GHC/Tc/Solver/Solve.hs-boot
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Types.hs
- compiler/GHC/Tc/Types/BasicTypes.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Types/Origin.hs
- compiler/GHC/Tc/Utils/Concrete.hs
- compiler/GHC/Tc/Utils/Env.hs
- compiler/GHC/Tc/Utils/Instantiate.hs
- compiler/GHC/Tc/Utils/Monad.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Tc/Zonk/TcType.hs
- compiler/GHC/Tc/Zonk/Type.hs
- compiler/GHC/Types/Basic.hs
- compiler/GHC/Types/Unique/DSM.hs
- + compiler/GHC/Utils/EndoOS.hs
- compiler/ghc.cabal.in
- rts/ThreadPaused.c
- testsuite/tests/count-deps/CountDepsAst.stdout
- testsuite/tests/count-deps/CountDepsParser.stdout
- testsuite/tests/default/default-fail05.stderr
- testsuite/tests/dependent/should_fail/T13135_simple.stderr
- testsuite/tests/deriving/should_fail/T3621.stderr
- testsuite/tests/indexed-types/should_fail/T14369.stderr
- testsuite/tests/indexed-types/should_fail/T1897b.stderr
- testsuite/tests/linters/notes.stdout
- testsuite/tests/parser/should_fail/RecordDotSyntaxFail10.stderr
- testsuite/tests/parser/should_fail/RecordDotSyntaxFail13.stderr
- testsuite/tests/parser/should_fail/T20654a.stderr
- testsuite/tests/partial-sigs/should_fail/T14584a.stderr
- testsuite/tests/polykinds/T6068.stdout
- testsuite/tests/quantified-constraints/T15359.hs
- testsuite/tests/rep-poly/RepPolyNPlusK.stderr
- testsuite/tests/rep-poly/RepPolyRightSection.stderr
- testsuite/tests/rep-poly/T13233.stderr
- testsuite/tests/rep-poly/T19709b.stderr
- testsuite/tests/rep-poly/T23903.stderr
- testsuite/tests/typecheck/no_skolem_info/T13499.stderr
- testsuite/tests/typecheck/should_compile/T13651.hs
- − testsuite/tests/typecheck/should_compile/T13651.stderr
- + testsuite/tests/typecheck/should_compile/T14745.hs
- testsuite/tests/typecheck/should_compile/all.T
- testsuite/tests/typecheck/should_compile/hole_constraints_nested.stderr
- testsuite/tests/typecheck/should_compile/tc126.hs
- testsuite/tests/typecheck/should_fail/AmbigFDs.hs
- − testsuite/tests/typecheck/should_fail/AmbigFDs.stderr
- testsuite/tests/typecheck/should_fail/FD3.stderr
- testsuite/tests/typecheck/should_fail/FDsFromGivens2.stderr
- testsuite/tests/typecheck/should_fail/T13506.stderr
- testsuite/tests/typecheck/should_fail/T16512a.stderr
- testsuite/tests/typecheck/should_fail/T18851b.hs
- − testsuite/tests/typecheck/should_fail/T18851b.stderr
- testsuite/tests/typecheck/should_fail/T18851c.hs
- − testsuite/tests/typecheck/should_fail/T18851c.stderr
- testsuite/tests/typecheck/should_fail/T19415.stderr
- testsuite/tests/typecheck/should_fail/T19415b.stderr
- testsuite/tests/typecheck/should_fail/T22684.stderr
- + testsuite/tests/typecheck/should_fail/T23162a.hs
- + testsuite/tests/typecheck/should_fail/T23162a.stderr
- testsuite/tests/typecheck/should_fail/T25325.stderr
- testsuite/tests/typecheck/should_fail/T5246.stderr
- testsuite/tests/typecheck/should_fail/T5978.stderr
- testsuite/tests/typecheck/should_fail/T7368a.stderr
- testsuite/tests/typecheck/should_fail/T7696.stderr
- testsuite/tests/typecheck/should_fail/T8603.stderr
- testsuite/tests/typecheck/should_fail/T9612.stderr
- testsuite/tests/typecheck/should_fail/TcStaticPointersFail03.stderr
- testsuite/tests/typecheck/should_fail/all.T
- testsuite/tests/typecheck/should_fail/tcfail122.stderr
- testsuite/tests/typecheck/should_fail/tcfail143.stderr
The diff was not included because it is too large.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/07a053cbfc0b9263888787649503fc…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/07a053cbfc0b9263888787649503fc…
You're receiving this email because of your account on gitlab.haskell.org.
1
0