summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRichard Eisenberg <rae@richarde.dev>2021-03-23 16:48:20 -0400
committerRyan Scott <rscott@galois.com>2021-04-13 10:13:00 -0400
commit1f2681a91f2076765a884e5d3d5dcf92c54c0f33 (patch)
tree4a955222a2ff41e41d0e14a3a7ee7a5d52ef8760
parent0298f14bddb36c44329f4dcecd2e1355e9a9eaad (diff)
downloadhaskell-1f2681a91f2076765a884e5d3d5dcf92c54c0f33.tar.gz
Kick out fewer equalities by thinking harder
Close #17672. By scratching our heads quite hard, we realized that we should never kick out Given/Nominal equalities. This commit tweaks the kick-out conditions accordingly. See also Note [K4] which describes what is going on. This does not fix a known misbehavior, but it should be a small improvement in both practice (kicking out is bad, and we now do less of it) and theory (a Given/Nominal should behave just like a filled-in metavariable, which has no notion of kicking out).
-rw-r--r--compiler/GHC/Tc/Solver/Monad.hs68
-rw-r--r--compiler/GHC/Tc/Types/Constraint.hs3
2 files changed, 44 insertions, 27 deletions
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 6ddecbe58f..e7e58f6599 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -1005,14 +1005,14 @@ Main Theorem [Stability under extension]
AND (K2): guarantees inertness of the new substitution
{ (K2a) not (fs >= fs)
- OR (K2b) lhs1 is a tyvar AND fs >= fw
- OR (K2c) lhs not in s }
+ OR (K2b) lhs not in s }
AND (K3) See Note [K3: completeness of solving]
{ (K3a) If the role of fs is nominal: s /= lhs
(K3b) If the role of fs is representational:
s is not of form (lhs t1 .. tn) } }
+ OR (K4) lhs1 is a tyvar AND fs >= fw
Conditions (T1-T3) are established by the canonicaliser
Conditions (K1-K3) are established by GHC.Tc.Solver.Monad.kickOutRewritable
@@ -1068,22 +1068,24 @@ The idea is that
(NB: we could strengten K1) in this way too, but see K3.
- - (K2b): See Note [K2b].
-
- - (K2c): if a not in s, we have no further opportunity to apply the
- work item, similar to (K2b)
+ - (K2b): if lhs not in s, we have no further opportunity to apply the
+ work item
NB: Dimitrios has a PDF that does this in more detail
+* Lemma (L3). Suppose we have f* such that, for all f, f* >= f. Then
+ if we are adding lhs -fw-> t (where T1, T2, and T3 hold), we will keep a -f*-> s.
+ Proof. K4 holds; thus, we keep.
+
Key lemma to make it watertight.
Under the conditions of the Main Theorem,
forall f st fw >= f, a is not in S^k(f,t), for any k
Also, consider roles more carefully. See Note [Flavours with roles]
-Note [K2b]
-~~~~~~~~~~
-K2b is a "keep" condition of Note [Extending the inert equalities].
+Note [K4]
+~~~~~~~~~
+K4 is a "keep" condition of Note [Extending the inert equalities].
Here is the scenario:
* We are considering adding (lhs -fw-> t) to the inert set S.
@@ -1091,19 +1093,16 @@ Here is the scenario:
* We know S(fw, lhs) = lhs, S(fw, t) = t, and lhs is not rewritable in t. These
are (T1), (T2), and (T3).
* We further know fw >= fs. (If not, then we short-circuit via (K0).)
-* lhs is not rewritable in lhs1. That is (lhs -fw-> t)(fs, lhs1) = lhs1, where
- we are applying (lhs -fw-> t) as a generalised substitution.
- (Definition [Generalised substitution])
-K2b says that we may keep lhs1 -fs-> s in S if:
+K4 says that we may keep lhs1 -fs-> s in S if:
lhs1 is a tyvar AND fs >= fw
Let's consider the two possible shapes of lhs1 (which, recall, is a CanEqLHS:
either a tyvar or an exactly-saturated type family application).
+ lhs1 is a tyvar a:
- * We know lhs /= a, because we said that lhs is not rewritable in lhs1 (= a).
* If fs >= fw, we know a is not rewritable in t, because of (T2).
+ * We further know lhs /= a, because of (T1).
* Accordingly, a use of the new inert item lhs -fw-> t cannot create the conditions
for a use of a -fs-> s (precisely because t does not mention a).
@@ -1135,12 +1134,25 @@ either a tyvar or an exactly-saturated type family application).
cannot allow an equality with an LHS of a to fire. This is not the case for
type family applications.
-Bottom line: K2b can keep only inerts with tyvars on the left. Put differently,
-K2b will never prevent an inert with a type family on the left from being kicked
+Bottom line: K4 can keep only inerts with tyvars on the left. Put differently,
+K4 will never prevent an inert with a type family on the left from being kicked
out.
-Getting this wrong (that is, allowing K2b to apply to situations with the type
-family on the left) led to #19042.
+Consequence: We never kick out a Given/Nominal equality with a tyvar on the left.
+This is Lemma (L3) of Note [Extending the inert equalities]. It is good because
+it means we can effectively model the mutable filling of metavariables with
+Given/Nominal equalities. That is: it should be the case that we could rewrite
+our solver never to fill in a metavariable; instead, it would "solve" a wanted
+like alpha ~ Int by turning it into a Given, allowing it to be used in rewriting.
+We would want the solver to behave the same whether it uses metavariables or
+Givens. And (L3) says that no Given/Nominals over tyvars are ever kicked out,
+just like we never unfill a metavariable. Nice.
+
+Getting this wrong (that is, allowing K4 to apply to situations with the type
+family on the left) led to #19042. (At that point, K4 was known as K2b.)
+
+Originally, this condition was part of K2, but #17672 suggests it should be
+a top-level K condition.
Note [K3: completeness of solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1195,8 +1207,8 @@ representational inert out. And then, we'd miss solving the inert, which
now reduced to reflexivity.
The solution here is to kick out representational inerts whenever the
-tyvar of a work item is "exposed", where exposed means being at the
-head of the top-level application chain (a t1 .. tn). See
+lhs of a work item is "exposed", where exposed means being at the
+head of the top-level application chain (lhs t1 .. tn). See
is_can_eq_lhs_head. This is encoded in (K3b).
Beware: if we make this test succeed too often, we kick out too much,
@@ -1979,10 +1991,16 @@ kick_out_rewritable new_fr new_lhs
kick_out_eq (CEqCan { cc_lhs = lhs, cc_rhs = rhs_ty
, cc_ev = ev, cc_eq_rel = eq_rel })
| not (fr_may_rewrite fs)
- = False -- Keep it in the inert set if the new thing can't rewrite it
+ = False -- (K0) Keep it in the inert set if the new thing can't rewrite it
+
+ | TyVarLHS _ <- lhs
+ , fs `eqMayRewriteFR` new_fr
+ = False -- (K4) Keep it in the inert set if the LHS is a tyvar and
+ -- it can rewrite the work item. See Note [K4]
-- Below here (fr_may_rewrite fs) is True
- | fr_can_rewrite_ty eq_rel (canEqLHSType lhs) = True -- (K1)
+ | fr_can_rewrite_ty eq_rel (canEqLHSType lhs)
+ = True -- (K1)
-- The above check redundantly checks the role & flavour,
-- but it's very convenient
@@ -1993,10 +2011,8 @@ kick_out_rewritable new_fr new_lhs
where
fs = (ctEvFlavour ev, eq_rel)
kick_out_for_inertness
- = (fs `eqMayRewriteFR` fs) -- (K2a)
- && (case lhs of TyVarLHS _ -> not (fs `eqMayRewriteFR` new_fr)
- _ -> True) -- (K2b) See Note [K2b].
- && fr_can_rewrite_ty eq_rel rhs_ty -- (K2c)
+ = (fs `eqMayRewriteFR` fs) -- (K2a)
+ && fr_can_rewrite_ty eq_rel rhs_ty -- (K2b)
kick_out_for_completeness -- (K3) and Note [K3: completeness of solving]
= case eq_rel of
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index b28064bd66..bf594637a9 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -1702,7 +1702,8 @@ we can; straight from the Wanteds during improvement. And from a Derived
ReprEq we could conceivably get a Derived NomEq improvement (by decomposing
a type constructor with Nomninal role), and hence unify.
-This restriction bites, in an obscure scenario:
+This restriction that (Derived, NomEq) cannot rewrite (Derived, ReprEq) bites,
+in an obscure scenario:
data T a
type role T nominal