[Git][ghc/ghc][wip/cfuneqcan-refactor] Improve comments
Richard Eisenberg
gitlab at gitlab.haskell.org
Wed Nov 25 20:02:22 UTC 2020
Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC
Commits:
57609069 by Richard Eisenberg at 2020-11-25T15:00:36-05:00
Improve comments
- - - - -
5 changed files:
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -3939,6 +3939,8 @@ more. So I use a HACK:
Result works fine, but it may eventually bite us.
+See also Note [Do not simplify ConstraintHoles] in GHC.Tc.Solver for
+information about how these are printed.
************************************************************************
* *
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -2120,7 +2120,8 @@ the example for why (partial-sigs/should_compile/T12844):
GHC correctly infers that the extra-constraints wildcard on `bar`
should be (Head rngs ~ '(r, r'), Foo rngs). It then adds this constraint
-as a Given on the implication constraint for `bar`. The Hole for
+as a Given on the implication constraint for `bar`. (This implication is
+created by mkResidualConstraints in simplifyInfer.) The Hole for
the _ is stored within the implication's WantedConstraints.
When simplifyHoles is called, that constraint is already assumed as
a Given. Simplifying with respect to it turns it into
@@ -2135,6 +2136,9 @@ is simple: just don't simplify extra-constraints wildcards.
This is the only reason we need to track ConstraintHole separately
from TypeHole in HoleSort.
+See also Note [Extra-constraint holes in partial type signatures]
+in GHC.Tc.Gen.HsType.
+
Note [Tracking redundant constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
With Opt_WarnRedundantConstraints, GHC can report which
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -2524,38 +2524,39 @@ Wrinkles:
must be sure to kick out any such CIrredCan constraints that mention coercion holes
when those holes get filled in, so that the unification step can now proceed.
- (2a) We must now kick out any constraints that mention a newly-filled-in
- coercion hole, but only if there are no more remaining coercion
- holes. This is done in kickOutAfterFillingCoercionHole. The extra
- check that there are no more remaining holes avoids needless work
- when rewriting evidence (which fills coercion holes) and aids
- efficiency.
-
- Moreover, kicking out when there are remaining unfilled holes can
- cause a loop in the solver in this case:
- [W] w1 :: (ty1 :: F a) ~ (ty2 :: s)
- After canonicalisation, we discover that this equality is heterogeneous.
- So we emit
- [W] co_abc :: F a ~ s
- and preserve the original as
- [W] w2 :: (ty1 |> co_abc) ~ ty2 (blocked on co_abc)
- Then, co_abc comes becomes the work item. It gets swapped in
- canEqCanLHS2 and then back again in canEqTyVarFunEq. We thus get
- co_abc := sym co_abd, and then co_abd := sym co_abe, with
- [W] co_abe :: F a ~ s
- This process has filled in co_abc. Suppose w2 were kicked out.
- When it gets processed,
- would get this whole chain going again. The solution is to
- kick out a blocked constraint only when the result of filling
- in the blocking coercion involves no further blocking coercions.
- Alternatively, we could be careful not to do unnecessary swaps during
- canonicalisation, but that seems hard to do, in general.
+ The kicking out is done in kickOutAfterFillingCoercionHole.
+
+ However, we must be careful: we kick out only when no coercion holes are
+ left. The holes in the type are stored in the BlockedCIS CtIrredStatus.
+ The extra check that there are no more remaining holes avoids
+ needless work when rewriting evidence (which fills coercion holes) and
+ aids efficiency.
+
+ Moreover, kicking out when there are remaining unfilled holes can
+ cause a loop in the solver in this case:
+ [W] w1 :: (ty1 :: F a) ~ (ty2 :: s)
+ After canonicalisation, we discover that this equality is heterogeneous.
+ So we emit
+ [W] co_abc :: F a ~ s
+ and preserve the original as
+ [W] w2 :: (ty1 |> co_abc) ~ ty2 (blocked on co_abc)
+ Then, co_abc comes becomes the work item. It gets swapped in
+ canEqCanLHS2 and then back again in canEqTyVarFunEq. We thus get
+ co_abc := sym co_abd, and then co_abd := sym co_abe, with
+ [W] co_abe :: F a ~ s
+ This process has filled in co_abc. Suppose w2 were kicked out.
+ When it gets processed,
+ would get this whole chain going again. The solution is to
+ kick out a blocked constraint only when the result of filling
+ in the blocking coercion involves no further blocking coercions.
+ Alternatively, we could be careful not to do unnecessary swaps during
+ canonicalisation, but that seems hard to do, in general.
(3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the
algorithm detailed here, producing [W] co :: k2 ~ k1, and adding
[W] (a :: k1) ~ ((rhs |> co) :: k1) to the irreducibles. Some time
later, we solve co, and fill in co's coercion hole. This kicks out
- the irreducible as described in (2a).
+ the irreducible as described in (2).
But now, during canonicalization, we see the cast
and remove it, in canEqCast. By the time we get into canEqCanLHS, the equality
is heterogeneous again, and the process repeats.
@@ -2832,9 +2833,10 @@ Details:
they originally stood for (e.g. cbv1 := TF a, cbv2 := TF Int),
not what may be in a rewritten constraint.
- Not breaking cycles fursther makes sense, because
- we only want to break cycles for user-written loopy Givens, and
- a CycleBreakerTv certainly isn't user-written.
+ Not breaking cycles further (which would mean changing TF cbv1 to cbv3
+ and TF cbv2 to cbv4) makes sense, because we only want to break cycles
+ for user-written loopy Givens, and a CycleBreakerTv certainly isn't
+ user-written.
NB: This same situation (an equality like b ~ Maybe (F b)) can arise with
Wanteds, but we have no concrete case incentivising special treatment. It
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -1817,7 +1817,7 @@ kickOutAfterUnification new_tv
; setInertCans ics2
; return n_kicked }
--- See Wrinkle (2a) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
+-- See Wrinkle (2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
kickOutAfterFillingCoercionHole :: CoercionHole -> Coercion -> TcS ()
kickOutAfterFillingCoercionHole hole filled_co
= do { ics <- getInertCans
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -298,7 +298,7 @@ data CtIrredStatus
| BlockedCIS HoleSet
-- this constraint is blocked on the coercion hole(s) listed
-- See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
- -- Wrinkle (4a). Why store the HoleSet? See Wrinkle (2a) of that
+ -- Wrinkle (4a). Why store the HoleSet? See Wrinkle (2) of that
-- same Note.
-- INVARIANT: A BlockedCIS is a homogeneous equality whose
-- left hand side can fit in a CanEqLHS.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/57609069ed365114b38487c97706f3151064b1fa
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/57609069ed365114b38487c97706f3151064b1fa
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201125/2211c3b4/attachment-0001.html>
More information about the ghc-commits
mailing list