Commit 6edafe3b authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Fix isDroppableCt (Trac #14763)

When finishing up an implication constraint, it's a bit tricky to
decide which Derived constraints to retain (for error reporting) and
which to discard.  I got this wrong in commit
   f20cf982
   (Remove wc_insol from WantedConstraints)

The particular problem in Trac #14763 was that we were reporting as an
error a fundep-generated constraint
  (ex ~ T)
where 'ex' is an existentially-bound variable in a pattern match.
But this isn't really an error at all.

This patch fixes the problem. Indeed, since I had to understand
this rather tricky code, I took the opportunity to clean it up
and document better.  See
  isDroppableCt :: Ct -> Bool
and Note [Dropping derived constraints]

I also removed wl_deriv altogether from the WorkList data type.  It
was there in the hope of gaining efficiency by not even processing
lots of derived constraints, but it has turned out that most derived
constraints (notably equalities) must be processed anyway; see
Note [Prioritise equalities] in TcSMonad.

The two are coupled because to decide which constraints to put in
wl_deriv I was using another variant of isDroppableCt.  Now it's much
simpler -- and perhaps even more efficient too.
parent 059596df
......@@ -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,
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
{-# 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.)
......@@ -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, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment