diff options
| -rw-r--r-- | compiler/typecheck/TcCanonical.hs | 15 | ||||
| -rw-r--r-- | compiler/typecheck/TcErrors.hs | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcInteract.hs | 5 | ||||
| -rw-r--r-- | compiler/typecheck/TcRnTypes.hs | 109 | ||||
| -rw-r--r-- | compiler/typecheck/TcSMonad.hs | 109 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T14763.hs | 34 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 1 |
7 files changed, 148 insertions, 127 deletions
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 868d785b18..5618824ed5 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -1700,11 +1700,16 @@ is embarrassing. See #11198 for more tales of destruction. The reason for this odd behavior is much the same as Note [Wanteds do not rewrite Wanteds] in TcRnTypes: note that the -new `co` is a Wanted. The solution is then not to use `co` to "rewrite" --- that is, cast -- `w`, but instead to keep `w` heterogeneous and irreducible. -Given that we're not using `co`, there is no reason to collect evidence -for it, so `co` is born a Derived. When the Derived is solved (by unification), -the original wanted (`w`) will get kicked out. +new `co` is a Wanted. + + The solution is then not to use `co` to "rewrite" -- that is, cast + -- `w`, but instead to keep `w` heterogeneous and + irreducible. Given that we're not using `co`, there is no reason to + collect evidence for it, so `co` is born a Derived, with a CtOrigin + of KindEqOrigin. + +When the Derived is solved (by unification), the original wanted (`w`) +will get kicked out. Note that, if we had [G] co1 :: k ~ Type available, then none of this code would trigger, because flattening would have rewritten k to Type. That is, diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index fb27b4ed7c..8d2238a985 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -700,7 +700,7 @@ we'll complain about f :: ((Int ~ Bool) => a -> a) -> Int which arguably is OK. It's more debatable for g :: (Int ~ Bool) => Int -> Int -but it's tricky to distinguish these cases to we don't report +but it's tricky to distinguish these cases so we don't report either. The bottom line is this: find_gadt_match looks for an enclosing diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 9a2f64d672..d0bcddf19f 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -686,7 +686,7 @@ interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble }) -- which can happen with solveOneFromTheOther, so that -- we get distinct error messages with -fdefer-type-errors -- See Note [Do not add duplicate derived insolubles] - , not (isDroppableDerivedCt workItem) + , not (isDroppableCt workItem) = continueWith workItem | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w @@ -1882,7 +1882,8 @@ improveTopFunEqs ev fam_tc args fsk , ppr eqns ]) ; mapM_ (unifyDerived loc Nominal) eqns } where - loc = ctEvLoc ev + loc = ctEvLoc ev -- ToDo: this location is wrong; it should be FunDepOrigin2 + -- See Trac #14778 improve_top_fun_eqs :: FamInstEnvs -> TyCon -> [TcType] -> TcType diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index 5e52496696..d2c8dd8a43 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -87,7 +87,7 @@ module TcRnTypes( addInsols, insolublesOnly, addSimples, addImplics, tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, tyCoVarsOfWCList, insolubleWantedCt, insolubleEqCt, - isDroppableDerivedLoc, isDroppableDerivedCt, insolubleImplic, + isDroppableCt, insolubleImplic, arisesFromGivens, Implication(..), newImplication, @@ -1931,13 +1931,10 @@ dropDerivedSimples simples = mapMaybeBag dropDerivedCt simples dropDerivedCt :: Ct -> Maybe Ct dropDerivedCt ct = case ctEvFlavour ev of - Given -> Just ct -- Presumably insoluble; keep Wanted WOnly -> Just (ct' { cc_ev = ev_wd }) Wanted _ -> Just ct' - Derived | isDroppableDerivedLoc (ctLoc ct) - -> Nothing - | otherwise - -> Just ct + _ | isDroppableCt ct -> Nothing + | otherwise -> Just ct where ev = ctEvidence ct ev_wd = ev { ctev_nosh = WDeriv } @@ -1953,26 +1950,41 @@ we might miss some fundeps. Trac #13662 showed this up. See Note [The superclass story] in TcCanonical. -} -isDroppableDerivedCt :: Ct -> Bool -isDroppableDerivedCt ct - | isDerivedCt ct = isDroppableDerivedLoc (ctLoc ct) - | otherwise = False - -isDroppableDerivedLoc :: CtLoc -> Bool --- See Note [Dropping derived constraints] -isDroppableDerivedLoc loc - = case ctLocOrigin loc of - HoleOrigin {} -> False - KindEqOrigin {} -> False - GivenOrigin {} -> False - - -- See Note [Dropping derived constraints] - -- For fundeps, drop wanted/wanted interactions - FunDepOrigin2 {} -> False - FunDepOrigin1 _ loc1 _ loc2 - | isGivenLoc loc1 || isGivenLoc loc2 -> False - | otherwise -> True - _ -> True +isDroppableCt :: Ct -> Bool +isDroppableCt ct + = isDerived ev && not keep_deriv + -- Drop only derived constraints, and then only if they + -- obey Note [Dropping derived constraints] + where + ev = ctEvidence ct + loc = ctEvLoc ev + orig = ctLocOrigin loc + + keep_deriv + = case ct of + CHoleCan {} -> True + CIrredCan { cc_insol = insoluble } + -> keep_eq insoluble + _ -> keep_eq False + + keep_eq definitely_insoluble + | isGivenOrigin orig -- Arising only from givens + = definitely_insoluble -- Keep only definitely insoluble + | otherwise + = case orig of + KindEqOrigin {} -> True -- Why? + + -- See Note [Dropping derived constraints] + -- For fundeps, drop wanted/wanted interactions + FunDepOrigin2 {} -> True -- Top-level/Wanted + FunDepOrigin1 _ loc1 _ loc2 + | g1 || g2 -> True -- Given/Wanted errors: keep all + | otherwise -> False -- Wanted/Wanted errors: discard + where + g1 = isGivenLoc loc1 + g2 = isGivenLoc loc2 + + _ -> False arisesFromGivens :: Ct -> Bool arisesFromGivens ct @@ -1995,30 +2007,43 @@ isGivenOrigin _ = False In general we discard derived constraints at the end of constraint solving; see dropDerivedWC. For example - * If we have an unsolved [W] (Ord a), we don't want to complain about - an unsolved [D] (Eq a) as well. + * Superclasses: if we have an unsolved [W] (Ord a), we don't want to + complain about an unsolved [D] (Eq a) as well. * If we have [W] a ~ Int, [W] a ~ Bool, improvement will generate - [D] Int ~ Bool, and we don't want to report that because it's incomprehensible. - That is why we don't rewrite wanteds with wanteds! + [D] Int ~ Bool, and we don't want to report that because it's + incomprehensible. That is why we don't rewrite wanteds with wanteds! -But (tiresomely) we do keep *some* Derived insolubles: +But (tiresomely) we do keep *some* Derived constraints: * Type holes are derived constraints, because they have no evidence and we want to keep them, so we get the error report - * Insoluble derived equalities (e.g. [D] Int ~ Bool) may arise from - functional dependency interactions: - - Given or Wanted interacting with an instance declaration (FunDepOrigin2) - - Given/Given interactions (FunDepOrigin1); this reflects unreachable code + * Insoluble kind equalities (e.g. [D] * ~ (* -> *)), with + KindEqOrigin, may arise from a type equality a ~ Int#, say. See + Note [Equalities with incompatible kinds] in TcCanonical. + + * We keep most derived equalities arising from functional dependencies + - Given/Given interactions (subset of FunDepOrigin1): + The definitely-insoluble ones reflect unreachable code. + + Others not-definitely-insoluble ones like [D] a ~ Int do not + reflect unreachable code; indeed if fundeps generated proofs, it'd + be a useful equality. See Trac #14763. So we discard them. + + - Given/Wanted interacGiven or Wanted interacting with an + instance declaration (FunDepOrigin2) + - Given/Wanted interactions (FunDepOrigin1); see Trac #9612 - But for Wanted/Wanted interactions we do /not/ want to report an - error (Trac #13506). Consider [W] C Int Int, [W] C Int Bool, with - a fundep on class C. We don't want to report an insoluble Int~Bool; - c.f. "wanteds do not rewrite wanteds". + - But for Wanted/Wanted interactions we do /not/ want to report an + error (Trac #13506). Consider [W] C Int Int, [W] C Int Bool, with + a fundep on class C. We don't want to report an insoluble Int~Bool; + c.f. "wanteds do not rewrite wanteds". + +To distinguish these cases we use the CtOrigin. -Moreover, we keep *all* derived insolubles under some circumstances: +NB: we keep *all* derived insolubles under some circumstances: * They are looked at by simplifyInfer, to decide whether to generalise. Example: [W] a ~ Int, [W] a ~ Bool @@ -2026,8 +2051,6 @@ Moreover, we keep *all* derived insolubles under some circumstances: and we want simplifyInfer to see that, even though we don't ultimately want to generate an (inexplicable) error message from it -To distinguish these cases we use the CtOrigin. - ************************************************************************ * * @@ -3301,7 +3324,7 @@ data CtOrigin -- visible.) Only used for prioritizing error messages. } - | KindEqOrigin + | KindEqOrigin -- See Note [Equalities with incompatible kinds] in TcCanonical. TcType (Maybe TcType) -- A kind equality arising from unifying these two types CtOrigin -- originally arising from this (Maybe TypeOrKind) -- the level of the eq this arises from diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 0b1d6e4cbd..0db75095f1 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -5,7 +5,7 @@ module TcSMonad ( -- The work list WorkList(..), isEmptyWorkList, emptyWorkList, - extendWorkListNonEq, extendWorkListCt, extendWorkListDerived, + extendWorkListNonEq, extendWorkListCt, extendWorkListCts, extendWorkListEq, extendWorkListFunEq, appendWorkList, extendWorkListImplic, selectNextWorkItem, @@ -36,7 +36,7 @@ module TcSMonad ( setEvBind, setWantedEq, setEqIfWanted, setWantedEvTerm, setWantedEvBind, setEvBindIfWanted, newEvVar, newGivenEvVar, newGivenEvVars, - emitNewDerived, emitNewDeriveds, emitNewDerivedEq, + emitNewDeriveds, emitNewDerivedEq, checkReductionDepth, getInstEnvs, getFamInstEnvs, -- Getting the environments @@ -191,7 +191,8 @@ consider using this depth for prioritization as well in the future. As a simple form of priority queue, our worklist separates out * equalities (wl_eqs); see Note [Prioritise equalities] -* non-equality deriveds (wl_derivs); see Note [Process derived items last] +* type-function equalities (wl_funeqs) +* all the rest (wl_rest) Note [Prioritise equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -202,10 +203,6 @@ It's very important to process equalities /first/: and then kicking it out later. That's extra work compared to just doing the equality first. -* (Derived equalities) Notwithstanding Note [Process derived items - last], we want to process /Derived/ equalities eagerly, for the - (Efficiency) reason above. - * (Avoiding fundep iteration) As Trac #14723 showed, it's possible to get non-termination if we - Emit the Derived fundep equalities for a class constraint, @@ -216,15 +213,21 @@ It's very important to process equalities /first/: equalities in the work-list), but generates yet more fundeps Solution: prioritise derived equalities over class constraints -* (Class equalities) We need to prioritise equalities even if they are - hidden inside a class constraint; see Note [Prioritise class - equalities] +* (Class equalities) We need to prioritise equalities even if they + are hidden inside a class constraint; + see Note [Prioritise class equalities] * (Kick-out) We want to apply this priority scheme to kicked-out constraints too (see the call to extendWorkListCt in kick_out_rewritable E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become homo-kinded when kicked out, and hence we want to priotitise it. +* (Derived equalities) Originally we tried to postpone processing + Derived equalities, in the hope that we might never need to deal + with them at all; but in fact we must process Derived equalities + eagerly, partly for the (Efficiency) reason, and more importantly + for (Avoiding fundep iteration). + Note [Prioritise class equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We prioritise equalities in the solver (see selectWorkItem). But class @@ -241,13 +244,6 @@ So we arrange to put these particular class constraints in the wl_eqs. NB: since we do not currently apply the substitution to the inert_solved_dicts, the knot-tying still seems a bit fragile. But this makes it better. - -Note [Process derived items last] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We can often solve all goals without processing *any* derived constraints. -The derived constraints are just there to help us if we get stuck. So -we keep them in a separate list. - -} -- See Note [WorkList priorities] @@ -263,29 +259,23 @@ data WorkList , wl_rest :: [Ct] - , wl_deriv :: [CtEvidence] - -- Implicitly non-canonical - -- No equalities in here (they are in wl_eqs) - -- See Note [Process derived items last] - , wl_implics :: Bag Implication -- See Note [Residual implications] } appendWorkList :: WorkList -> WorkList -> WorkList appendWorkList (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1 - , wl_deriv = ders1, wl_implics = implics1 }) + , wl_implics = implics1 }) (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2 - , wl_deriv = ders2, wl_implics = implics2 }) + , wl_implics = implics2 }) = WL { wl_eqs = eqs1 ++ eqs2 , wl_funeqs = funeqs1 ++ funeqs2 , wl_rest = rest1 ++ rest2 - , wl_deriv = ders1 ++ ders2 , wl_implics = implics1 `unionBags` implics2 } workListSize :: WorkList -> Int -workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_deriv = ders, wl_rest = rest }) - = length eqs + length funeqs + length rest + length ders +workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest }) + = length eqs + length funeqs + length rest workListWantedCount :: WorkList -> Int -- Count the things we need to solve @@ -302,9 +292,6 @@ workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest }) extendWorkListEq :: Ct -> WorkList -> WorkList extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl } -extendWorkListEqs :: [Ct] -> WorkList -> WorkList -extendWorkListEqs cts wl = wl { wl_eqs = cts ++ wl_eqs wl } - extendWorkListFunEq :: Ct -> WorkList -> WorkList extendWorkListFunEq ct wl = wl { wl_funeqs = ct : wl_funeqs wl } @@ -312,15 +299,9 @@ extendWorkListNonEq :: Ct -> WorkList -> WorkList -- Extension by non equality extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl } -extendWorkListDerived :: CtLoc -> CtEvidence -> WorkList -> WorkList -extendWorkListDerived loc ev wl - | isDroppableDerivedLoc loc = wl { wl_deriv = ev : wl_deriv wl } - | otherwise = extendWorkListEq (mkNonCanonical ev) wl - -extendWorkListDeriveds :: CtLoc -> [CtEvidence] -> WorkList -> WorkList -extendWorkListDeriveds loc evs wl - | isDroppableDerivedLoc loc = wl { wl_deriv = evs ++ wl_deriv wl } - | otherwise = extendWorkListEqs (map mkNonCanonical evs) wl +extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList +extendWorkListDeriveds evs wl + = extendWorkListCts (map mkNonCanonical evs) wl extendWorkListImplic :: Bag Implication -> WorkList -> WorkList extendWorkListImplic implics wl = wl { wl_implics = implics `unionBags` wl_implics wl } @@ -350,12 +331,12 @@ extendWorkListCts cts wl = foldr extendWorkListCt wl cts isEmptyWorkList :: WorkList -> Bool isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs - , wl_rest = rest, wl_deriv = ders, wl_implics = implics }) - = null eqs && null rest && null funeqs && isEmptyBag implics && null ders + , wl_rest = rest, wl_implics = implics }) + = null eqs && null rest && null funeqs && isEmptyBag implics emptyWorkList :: WorkList emptyWorkList = WL { wl_eqs = [], wl_rest = [] - , wl_funeqs = [], wl_deriv = [], wl_implics = emptyBag } + , wl_funeqs = [], wl_implics = emptyBag } selectWorkItem :: WorkList -> Maybe (Ct, WorkList) -- See Note [Prioritise equalities] @@ -370,39 +351,23 @@ getWorkList :: TcS WorkList getWorkList = do { wl_var <- getTcSWorkListRef ; wrapTcS (TcM.readTcRef wl_var) } -selectDerivedWorkItem :: WorkList -> Maybe (Ct, WorkList) -selectDerivedWorkItem wl@(WL { wl_deriv = ders }) - | ev:evs <- ders = Just (mkNonCanonical ev, wl { wl_deriv = evs }) - | otherwise = Nothing - selectNextWorkItem :: TcS (Maybe Ct) -- Pick which work item to do next -- See Note [Prioritise equalities] --- See Note [Process derived items last] selectNextWorkItem = do { wl_var <- getTcSWorkListRef ; wl <- wrapTcS (TcM.readTcRef wl_var) - - ; let try :: Maybe (Ct,WorkList) -> TcS (Maybe Ct) -> TcS (Maybe Ct) - try mb_work do_this_if_fail - | Just (ct, new_wl) <- mb_work - = do { checkReductionDepth (ctLoc ct) (ctPred ct) - ; wrapTcS (TcM.writeTcRef wl_var new_wl) - ; return (Just ct) } - | otherwise - = do_this_if_fail - - ; try (selectWorkItem wl) $ - - do { ics <- getInertCans - ; if inert_count ics == 0 - then return Nothing - else try (selectDerivedWorkItem wl) (return Nothing) } } + ; case selectWorkItem wl of { + Nothing -> return Nothing ; + Just (ct, new_wl) -> + do { checkReductionDepth (ctLoc ct) (ctPred ct) + ; wrapTcS (TcM.writeTcRef wl_var new_wl) + ; return (Just ct) } } } -- Pretty printing instance Outputable WorkList where ppr (WL { wl_eqs = eqs, wl_funeqs = feqs - , wl_rest = rest, wl_implics = implics, wl_deriv = ders }) + , wl_rest = rest, wl_implics = implics }) = text "WL" <+> (braces $ vcat [ ppUnless (null eqs) $ text "Eqs =" <+> vcat (map ppr eqs) @@ -410,8 +375,6 @@ instance Outputable WorkList where text "Funeqs =" <+> vcat (map ppr feqs) , ppUnless (null rest) $ text "Non-eqs =" <+> vcat (map ppr rest) - , ppUnless (null ders) $ - text "Derived =" <+> vcat (map ppr ders) , ppUnless (isEmptyBag implics) $ ifPprDebug (text "Implics =" <+> vcat (map ppr (bagToList implics))) (text "(Implics omitted)") @@ -2690,7 +2653,7 @@ buildImplication skol_info skol_tvs givens (TcS thing_inside) do { env <- TcM.getLclEnv ; ev_binds_var <- TcM.newTcEvBinds ; let wc = ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) && - null (wl_deriv wl) && null (wl_implics wl), ppr wl ) + null (wl_implics wl), ppr wl ) WC { wc_simple = listToCts eqs , wc_impl = emptyBag } imp = newImplication { ic_tclvl = new_tclvl @@ -3184,12 +3147,6 @@ newWantedNC loc pty | otherwise = newWantedEvVarNC loc pty -emitNewDerived :: CtLoc -> TcPredType -> TcS () -emitNewDerived loc pred - = do { ev <- newDerivedNC loc pred - ; traceTcS "Emitting new derived" (ppr ev) - ; updWorkListTcS (extendWorkListDerived loc ev) } - emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS () emitNewDeriveds loc preds | null preds @@ -3197,7 +3154,7 @@ emitNewDeriveds loc preds | otherwise = do { evs <- mapM (newDerivedNC loc) preds ; traceTcS "Emitting new deriveds" (ppr evs) - ; updWorkListTcS (extendWorkListDeriveds loc evs) } + ; updWorkListTcS (extendWorkListDeriveds evs) } emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS () -- Create new equality Derived and put it in the work list @@ -3206,7 +3163,7 @@ emitNewDerivedEq loc role ty1 ty2 = do { ev <- newDerivedNC loc (mkPrimEqPredRole role ty1 ty2) ; traceTcS "Emitting new derived equality" (ppr ev $$ pprCtLoc loc) ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) } - -- Very important: put in the wl_eqs, /not/ wl_derivs + -- Very important: put in the wl_eqs -- See Note [Prioritise equalities] (Avoiding fundep iteration) newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence diff --git a/testsuite/tests/typecheck/should_compile/T14763.hs b/testsuite/tests/typecheck/should_compile/T14763.hs new file mode 100644 index 0000000000..1af13f65cb --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T14763.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +module T14763 where + +data Value a = Value a + +data SomeValue expr where + SomeValue :: Esqueleto query expr backend => expr (Value a) -> SomeValue expr + +class Esqueleto (query :: * -> *) (expr :: * -> *) backend + | query -> expr backend, expr -> query backend + +data SqlQuery a + +data SqlBackend + +data SqlExpr a where + ECompositeKey :: SqlExpr (Value a) + +instance Esqueleto SqlQuery SqlExpr SqlBackend + +match' :: SomeValue SqlExpr -> a +match' (SomeValue ECompositeKey) = undefined + +-- This is tricky becauuse we get a Given constraint +-- [G] Esqueleto query SqlExpr backend +-- where query and backend are existential. +-- Then fundeps with the top-level instance specify +-- [D] query ~ SqlQuery +-- [D] backend ~ SqlBackend +-- And that is not an error! +-- (Nor can we exploit it, though.) diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index a3aae5ee2b..c5c106ab15 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -593,3 +593,4 @@ test('T13032', normal, compile, ['']) test('T14273', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions']) test('T14732', normal, compile, ['']) test('T14774', [], run_command, ['$MAKE -s --no-print-directory T14774']) +test('T14763', normal, compile, ['']) |