diff options
| -rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 173 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Types/Constraint.hs | 53 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 6 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T19042.hs | 24 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 1 |
5 files changed, 205 insertions, 52 deletions
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 3c1d9eacff..6dcc660570 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -916,21 +916,22 @@ binary relation with the following properties (R1) >= is transitive (R2) If f1 >= f, and f2 >= f, then either f1 >= f2 or f2 >= f1 + (See Note [Why R2?].) -Lemma. If f1 >= f then f1 >= f1 -Proof. By property (R2), with f1=f2 +Lemma (L0). If f1 >= f then f1 >= f1 +Proof. By property (R2), with f1=f2 Definition [Generalised substitution] -A "generalised substitution" S is a set of triples (t0 -f-> t), where - t0 is a type variable or an exactly-saturated type family application - (that is, t0 is a CanEqLHS) +A "generalised substitution" S is a set of triples (lhs -f-> t), where + lhs is a type variable or an exactly-saturated type family application + (that is, lhs is a CanEqLHS) t is a type f is a flavour such that - (WF1) if (t0 -f1-> t1) in S - (t0' -f2-> t2) in S - then either not (f1 >= f2) or t0 does not appear within t0' - (WF2) if (t0 -f-> t) is in S, then t /= t0 + (WF1) if (lhs1 -f1-> t1) in S + (lhs2 -f2-> t2) in S + then (f1 >= f2) implies that lhs1 does not appear within lhs2 + (WF2) if (lhs -f-> t) is in S, then t /= lhs Definition [Applying a generalised substitution] If S is a generalised substitution @@ -939,7 +940,7 @@ If S is a generalised substitution See also Note [Flavours with roles]. Theorem: S(f,t0) is well defined as a function. -Proof: Suppose (t0 -f1-> t1) and (t0 -f2-> t2) are both in S, +Proof: Suppose (lhs -f1-> t1) and (lhs -f2-> t2) are both in S, and f1 >= f and f2 >= f Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1) @@ -965,52 +966,69 @@ Note that inertness is not the same as idempotence. To apply S to a type, you may have to apply it recursively. But inertness does guarantee that this recursive use will terminate. +Note [Why R2?] +~~~~~~~~~~~~~~ +R2 states that, if we have f1 >= f and f2 >= f, then either f1 >= f2 or f2 >= +f1. If we do not have R2, we will easily fall into a loop. + +To see why, imagine we have f1 >= f, f2 >= f, and that's it. Then, let our +inert set S = {a -f1-> b, b -f2-> a}. Computing S(f,a) does not terminate. And +yet, we have a hard time noticing an occurs-check problem when building S, as +the two equalities cannot rewrite one another. + +R2 actually restricts our ability to accept user-written programs. See Note +[Deriveds do rewrite Deriveds] in GHC.Tc.Types.Constraint for an example. + Note [Extending the inert equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Main Theorem [Stability under extension] Suppose we have a "work item" - t0 -fw-> t + lhs -fw-> t and an inert generalised substitution S, - THEN the extended substitution T = S+(t0 -fw-> t) + THEN the extended substitution T = S+(lhs -fw-> t) is an inert generalised substitution PROVIDED - (T1) S(fw,t0) = t0 -- LHS of work-item is a fixpoint of S(fw,_) - (T2) S(fw,t) = t -- RHS of work-item is a fixpoint of S(fw,_) - (T3) t0 not in t -- No occurs check in the work item - - AND, for every (t0' -fs-> s) in S: + (T1) S(fw,lhs) = lhs -- LHS of work-item is a fixpoint of S(fw,_) + (T2) S(fw,t) = t -- RHS of work-item is a fixpoint of S(fw,_) + (T3) lhs not in t -- No occurs check in the work item + -- If lhs is a type family application, we require only that + -- lhs is not *rewritable* in t. See Note [CEqCan occurs check] + -- in GHC.Tc.Types.Constraint + + AND, for every (lhs1 -fs-> s) in S: (K0) not (fw >= fs) - Reason: suppose we kick out (a -fs-> s), - and add (t0 -fw-> t) to the inert set. + Reason: suppose we kick out (lhs1 -fs-> s), + and add (lhs -fw-> t) to the inert set. The latter can't rewrite the former, so the kick-out achieved nothing - OR { (K1) t0 is not rewritable in t0'. That is, t0 does not occur - in t0' (except perhaps in a cast or coercion). + -- From here, we can assume fw >= fs + OR { (K1) lhs is not rewritable in lhs1. That is, lhs does not occur + in lhs1 (except perhaps in a cast or coercion). Reason: if fw >= fs, WF1 says we can't have both - t0 -fw-> t and F t0 -fs-> s + lhs0 -fw-> t and F lhs0 -fs-> s AND (K2): guarantees inertness of the new substitution { (K2a) not (fs >= fs) - OR (K2b) fs >= fw - OR (K2d) t0 not in s } + OR (K2b) lhs1 is a tyvar AND fs >= fw + OR (K2c) lhs not in s } AND (K3) See Note [K3: completeness of solving] - { (K3a) If the role of fs is nominal: s /= t0 + { (K3a) If the role of fs is nominal: s /= lhs (K3b) If the role of fs is representational: - s is not of form (t0 t1 .. tn) } } + s is not of form (lhs t1 .. tn) } } Conditions (T1-T3) are established by the canonicaliser Conditions (K1-K3) are established by GHC.Tc.Solver.Monad.kickOutRewritable The idea is that -* (T1-2) are guaranteed by exhaustively rewriting the work-item +* T1 and T2 are guaranteed by exhaustively rewriting the work-item with S(fw,_). -* T3 is guaranteed by a simple occurs-check on the work item. - This is done during canonicalisation, in canEqCanLHSFinish; invariant - (TyEq:OC) of CEqCan. +* T3 is guaranteed by an occurs-check on the work item. + This is done during canonicalisation, in canEqOK and checkTypeEq; invariant + (TyEq:OC) of CEqCan. See also Note [CEqCan occurs check] in GHC.Tc.Types.Constraint. * (K1-3) are the "kick-out" criteria. (As stated, they are really the "keep" criteria.) If the current inert S contains a triple that does @@ -1025,45 +1043,39 @@ The idea is that * Assume we have G>=G, G>=W and that's all. Then, when performing a unification we add a new given a -G-> ty. But doing so does NOT require us to kick out an inert wanted that mentions a, because of (K2a). This - is a common case, hence good not to kick out. + is a common case, hence good not to kick out. See also (K2a) below. * Lemma (L2): if not (fw >= fw), then K0 holds and we kick out nothing Proof: using Definition [Can-rewrite relation], fw can't rewrite anything - and so K0 holds. Intuitively, since fw can't rewrite anything, + and so K0 holds. Intuitively, since fw can't rewrite anything (Lemma (L0)), adding it cannot cause any loops This is a common case, because Wanteds cannot rewrite Wanteds. It's used to avoid even looking for constraint to kick out. * Lemma (L1): The conditions of the Main Theorem imply that there is no - (t0 -fs-> t) in S, s.t. (fs >= fw). + (lhs -fs-> t) in S, s.t. (fs >= fw). Proof. Suppose the contrary (fs >= fw). Then because of (T1), - S(fw,t0)=t0. But since fs>=fw, S(fw,t0) = s, hence s=t0. But now we - have (t0 -fs-> t0) in S, which contradicts (WF2). + S(fw,lhs)=lhs. But since fs>=fw, S(fw,lhs) = t, hence t=lhs. But now we + have (lhs -fs-> lhs) in S, which contradicts (WF2). * The extended substitution satisfies (WF1) and (WF2) - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1). - (T3) guarantees (WF2). -* (K2) is about inertness. Intuitively, any infinite chain T^0(f,t), - T^1(f,t), T^2(f,T).... must pass through the new work item infinitely +* (K2) is about inertness. Intuitively, any infinite chain S^0(f,t), + S^1(f,t), S^2(f,t).... must pass through the new work item infinitely often, since the substitution without the work item is inert; and must pass through at least one of the triples in S infinitely often. - - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f), - and hence this triple never plays a role in application S(f,a). + - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f) + (this is Lemma (L0)), and hence this triple never plays a role in application S(f,t). It is always safe to extend S with such a triple. (NB: we could strengten K1) in this way too, but see K3. - - (K2b): If this holds then, by (T2), b is not in t. So applying the - work item does not generate any new opportunities for applying S - - - (K2c): If this holds, we can't pass through this triple infinitely - often, because if we did then fs>=f, fw>=f, hence by (R2) - * either fw>=fs, contradicting K2c - * or fs>=fw; so by the argument in K2b we can't have a loop + - (K2b): See Note [K2b]. - - (K2d): if a not in s, we hae no further opportunity to apply the + - (K2c): if a not in s, we have no further opportunity to apply the work item, similar to (K2b) NB: Dimitrios has a PDF that does this in more detail @@ -1074,6 +1086,67 @@ Key lemma to make it watertight. Also, consider roles more carefully. See Note [Flavours with roles] +Note [K2b] +~~~~~~~~~~ +K2b 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. +* S already has (lhs1 -fs-> s). +* 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: + 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). + * 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). + + * Now, suppose not (fs >= fw). It might be the case that t mentions a, and this + can cause a loop. Example: + + Work: [G] b ~ a + Inert: [D] a ~ b + + (where G >= G, G >= D, and D >= D) + If we don't kick out the inert, then we get a loop on e.g. [D] a ~ Int. + + * Note that the above example is different if the inert is a Given G, because + (T1) won't hold. + ++ lhs1 is a type family application F tys: + * Presume fs >= fw. Thus, F tys is not rewritable in t, because of (T2). + * Can the use of lhs -fw-> t create the conditions for a use of F tys -fs-> s? + Yes! This can happen if t appears within tys. + + Here is an example: + + Work: [G] a ~ Int + Inert: [G] F Int ~ F a + + Now, if we have [W] F a ~ Bool, we will rewrite ad infinitum on the left-hand + side. The key reason why K2b works in the tyvar case is that tyvars are atomic: + if the right-hand side of an equality does not mention a variable a, then it + 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 +out. + +Getting this wrong (that is, allowing K2b to apply to situations with the type +family on the left) led to #19042. + Note [K3: completeness of solving] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ (K3) is not necessary for the extended substitution @@ -1926,9 +1999,9 @@ kick_out_rewritable new_fr new_lhs fs = (ctEvFlavour ev, eq_rel) kick_out_for_inertness = (fs `eqMayRewriteFR` fs) -- (K2a) - && not (fs `eqMayRewriteFR` new_fr) -- (K2b) - && fr_can_rewrite_ty eq_rel rhs_ty -- (K2d) - -- (K2c) is guaranteed by the first guard of keep_eq + && (case lhs of TyVarLHS _ -> not (fs `eqMayRewriteFR` new_fr) + _ -> True) -- (K2b) See Note [K2b]. + && fr_can_rewrite_ty eq_rel rhs_ty -- (K2c) 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 03aff4fff4..27a7a3abbf 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -142,7 +142,9 @@ We thus perform an occurs-check. There is, of course, some subtlety: already inert, with all type family redexes reduced. So a simple syntactic check is just fine. -The occurs check is performed in GHC.Tc.Utils.Unify.checkTypeEq. +The occurs check is performed in GHC.Tc.Utils.Unify.checkTypeEq +and forms condition T3 in Note [Extending the inert equalities] +in GHC.Tc.Solver.Monad. -} @@ -1708,6 +1710,55 @@ I thought maybe we could never get Derived ReprEq constraints, but 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: + + data T a + type role T nominal + + type family F a + + g :: forall b a. (F a ~ T a, Coercible (F a) (T b)) => () + g = () + + f :: forall a. (F a ~ T a) => () + f = g @a + +The problem is in the body of f. We have + + [G] F a ~N T a + [WD] F alpha ~N T alpha + [WD] F alpha ~R T a + +The Wanteds aren't of use, so let's just look at Deriveds: + + [G] F a ~N T a + [D] F alpha ~N T alpha + [D] F alpha ~R T a + +As written, this makes no progress, and GHC errors. But, if we +allowed D/N to rewrite D/R, the first D could rewrite the second: + + [G] F a ~N T a + [D] F alpha ~N T alpha + [D] T alpha ~R T a + +Now we decompose the second D to get + + [D] alpha ~N a + +noting the role annotation on T. This causes (alpha := a), and then +everything else unlocks. + +What to do? We could "decompose" nominal equalities into nominal-only +("NO") equalities and representational ones, where a NO equality rewrites +only nominals. That is, when considering whether [D] F alpha ~N T alpha +should rewrite [D] F alpha ~R T a, we could require splitting the first D +into [D] F alpha ~NO T alpha, [D] F alpha ~R T alpha. Then, we use the R +half of the split to rewrite the second D, and off we go. This splitting +would allow the split-off R equality to be rewritten by other equalities, +thus avoiding the problem in Note [Why R2?] in GHC.Tc.Solver.Monad. + -} eqCanRewrite :: EqRel -> EqRel -> Bool diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index c928433a0e..c7d2b3e09d 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -890,7 +890,10 @@ anyRewritableTyVar :: Bool -- Ignore casts and coercions -> TcType -> Bool anyRewritableTyVar ignore_cos role pred = any_rewritable ignore_cos role pred - (\ _ _ _ -> False) -- don't check tyconapps + (\ _ _ _ -> False) -- no special check for tyconapps + -- (this False is ORed with other results, so it + -- really means "do nothing special"; the arguments + -- are still inspected) (\ _ -> False) -- don't expand synonyms -- NB: No need to expand synonyms, because we can find -- all free variables of a synonym by looking at its @@ -931,6 +934,7 @@ this case) is nominal, the work item can't actually rewrite the inert item. Moreover, if we were to kick out the inert item the exact same situation would re-occur and we end up with an infinite loop in which each kicks out the other (#14363). + -} {- ********************************************************************* diff --git a/testsuite/tests/typecheck/should_compile/T19042.hs b/testsuite/tests/typecheck/should_compile/T19042.hs new file mode 100644 index 0000000000..61be41e75c --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T19042.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +module T19042 where + +import Data.Functor +import Data.Typeable + +type family N a + +data StyledPlot n where + StyledPlot :: Typeable p => p -> StyledPlot (N p) + +styledPlot :: forall p f. + (Typeable p, Applicative f) + => (p -> f p) + -> StyledPlot (N p) -> f (StyledPlot (N p)) +styledPlot f s@(StyledPlot p) = + case eq p of + Just Refl -> f p <&> \p' -> StyledPlot p' + Nothing -> pure s + where eq :: Typeable a => a -> Maybe (a :~: p) + eq _ = eqT diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 5e22d3332a..71cd232870 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -722,6 +722,7 @@ test('T18036a', normal, compile, ['']) test('T17873', normal, compile, ['']) test('T18129', expect_broken(18129), compile, ['']) test('T18185', normal, compile, ['']) +test('T19042', normal, compile, ['']) test('ExplicitSpecificityA1', normal, compile, ['']) test('ExplicitSpecificityA2', normal, compile, ['']) test('ExplicitSpecificity4', normal, compile, ['']) |