Commit ce97b729 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Expand given superclasses more eagerly

This patch fixes Trac #12175, another delicate corner case of
Note [Instance and Given overlap] in TcInteract.

In #12175 we were not expanding given superclasses eagerly
enough. It was easy to fix, and is actually rather neater than
before.

See Note [Eagerly expand given superclasses] in TcCanonical.
The main change is to move the eager expansion of given superclasses
to canClassNC.
parent a1b33596
......@@ -3,7 +3,7 @@
module TcCanonical(
canonicalize,
unifyDerived,
makeSuperClasses, mkGivensWithSuperClasses,
makeSuperClasses,
StopOrContinue(..), stopWith, continueWith
) where
......@@ -185,12 +185,23 @@ canEvNC ev
-}
canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
-- "NC" means "non-canonical"; that is, we have got here
-- from a NonCanonical constrataint, not from a CDictCan
-- Precondition: EvVar is class evidence
canClassNC ev cls tys = canClass ev cls tys (has_scs cls)
canClassNC ev cls tys
| isGiven ev -- See Note [Eagerly expand given superclasses]
= do { sc_cts <- mkStrictSuperClasses ev cls tys
; emitWork sc_cts
; canClass ev cls tys False }
| otherwise
= canClass ev cls tys (has_scs cls)
where
has_scs cls = not (null (classSCTheta cls))
canClass :: CtEvidence -> Class -> [Type] -> Bool -> TcS (StopOrContinue Ct)
canClass :: CtEvidence
-> Class -> [Type]
-> Bool -- True <=> un-explored superclasses
-> TcS (StopOrContinue Ct)
-- Precondition: EvVar is class evidence
canClass ev cls tys pend_sc
......@@ -249,15 +260,24 @@ Givens and Wanteds. But:
So here's the plan:
1. Generate superclasses for given (but not wanted) constraints;
see Note [Aggressively expand given superclasses]. However
stop if you encounter the same class twice. That is, expand
eagerly, but have a conservative termination condition: see
1. Eagerly generate superclasses for given (but not wanted)
constraints; see Note [Eagerly expand given superclasses].
This is done in canClassNC, when we take a non-canonical constraint
and cannonicalise it.
However stop if you encounter the same class twice. That is,
expand eagerly, but have a conservative termination condition: see
Note [Expanding superclasses] in TcType.
2. Solve the wanteds as usual, but do /no/ expansion of superclasses
in solveSimpleGivens or solveSimpleWanteds.
See Note [Danger of adding superclasses during solving]
2. Solve the wanteds as usual, but do no further expansion of
superclasses for canonical CDictCans in solveSimpleGivens or
solveSimpleWanteds; Note [Danger of adding superclasses during solving]
However, /do/ continue to eagerly expand superlasses for /given/
non-canonical constraints (canClassNC does this). As Trac #12175
showed, a type-family application can expand to a class constraint,
and we want to see its superclasses for just the same reason as
Note [Eagerly expand given superclasses].
3. If we have any remaining unsolved wanteds
(see Note [When superclasses help] in TcRnTypes)
......@@ -278,11 +298,11 @@ isPendingScDict holds).
When we take a CNonCanonical or CIrredCan, but end up classifying it
as a CDictCan, we set the cc_pend_sc flag to False.
Note [Aggressively expand given superclasses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In step (1) of Note [The superclass story], why do we aggressively
expand Given superclasses by one layer? Mainly because of some very
obscure cases like this:
Note [Eagerly expand given superclasses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In step (1) of Note [The superclass story], why do we eagerly expand
Given superclasses by one layer? Mainly because of some very obscure
cases like this:
instance Bad a => Eq (T a)
......@@ -294,6 +314,19 @@ instance declaration; but then we are stuck with (Bad a). Sigh.
This is really a case of non-confluent proofs, but to stop our users
complaining we expand one layer in advance.
Note [Instance and Given overlap] in TcInteract.
We also want to do this if we have
f :: F (T a) => blah
where
type instance F (T a) = Ord (T a)
So we may need to do a little work on the givens to expose the
class that has the superclasses. That's why the superclass
expansion for Givens happens in canClassNC.
Note [Why adding superclasses can help]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Examples of how adding superclasses can help:
......@@ -361,23 +394,6 @@ Mind you, now that Wanteds cannot rewrite Derived, I think this particular
situation can't happen.
-}
mkGivensWithSuperClasses :: CtLoc -> [EvId] -> TcS [Ct]
-- From a given EvId, make its Ct, plus the Ct's of its superclasses
-- See Note [The superclass story]
-- The loop-breaking here follows Note [Expanding superclasses] in TcType
--
-- Example: class D a => C a
-- class C [a] => D a
-- makeGivensWithSuperClasses (C x) will return (C x, D x, C[x])
-- i.e. up to and including the first repetition of C
mkGivensWithSuperClasses loc ev_ids = concatMapM go ev_ids
where
go ev_id = mk_superclasses emptyNameSet this_ev
where
this_ev = CtGiven { ctev_evar = ev_id
, ctev_pred = evVarPred ev_id
, ctev_loc = loc }
makeSuperClasses :: [Ct] -> TcS [Ct]
-- Returns strict superclasses, transitively, see Note [The superclasses story]
-- See Note [The superclass story]
......@@ -395,9 +411,14 @@ makeSuperClasses :: [Ct] -> TcS [Ct]
makeSuperClasses cts = concatMapM go cts
where
go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
= mk_strict_superclasses (unitNameSet (className cls)) ev cls tys
= mkStrictSuperClasses ev cls tys
go ct = pprPanic "makeSuperClasses" (ppr ct)
mkStrictSuperClasses :: CtEvidence -> Class -> [Type] -> TcS [Ct]
-- Return constraints for the strict superclasses of (c tys)
mkStrictSuperClasses ev cls tys
= mk_strict_superclasses (unitNameSet (className cls)) ev cls tys
mk_superclasses :: NameSet -> CtEvidence -> TcS [Ct]
-- Return this constraint, plus its superclasses, if any
mk_superclasses rec_clss ev
......
......@@ -1819,8 +1819,8 @@ Example, from the OutsideIn(X) paper:
g :: forall a. Q [a] => [a] -> Int
g x = wob x
This will generate the impliation constraint:
Q [a] => (Q [beta], R beta [a])
From 'g' we get the impliation constraint:
forall a. Q [a] => (Q [beta], R beta [a])
If we react (Q [beta]) with its top-level axiom, we end up with a
(P beta), which we have no way of discharging. On the other hand,
if we react R beta [a] with the top-level we get (beta ~ a), which
......@@ -1833,7 +1833,8 @@ The partial solution is that:
unifiable to this particular dictionary.
We treat any meta-tyvar as "unifiable" for this purpose,
*including* untouchable ones
*including* untouchable ones. But not skolems like 'a' in
the implication constraint above.
The end effect is that, much as we do for overlapping instances, we
delay choosing a class instance if there is a possibility of another
......@@ -1877,7 +1878,8 @@ Other notes:
and suppose we have -XNoMonoLocalBinds, so that we attempt to find the most
general type for 'v'. When generalising v's type we'll simplify its
Q [alpha] constraint, but we don't have Q [a] in the 'givens', so we
will use the instance declaration after all. Trac #11948 was a case in point
will use the instance declaration after all. Trac #11948 was a case
in point.
All of this is disgustingly delicate, so to discourage people from writing
simplifiable class givens, we warn about signatures that contain them;#
......
......@@ -73,7 +73,7 @@ module TcRnTypes(
isUserTypeErrorCt, getUserTypeErrorMsg,
ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
mkTcEqPredLikeEv,
mkNonCanonical, mkNonCanonicalCt,
mkNonCanonical, mkNonCanonicalCt, mkGivens,
ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
ctEvTerm, ctEvCoercion, ctEvId,
tyCoVarsOfCt, tyCoVarsOfCts,
......@@ -1498,6 +1498,14 @@ mkNonCanonical ev = CNonCanonical { cc_ev = ev }
mkNonCanonicalCt :: Ct -> Ct
mkNonCanonicalCt ct = CNonCanonical { cc_ev = cc_ev ct }
mkGivens :: CtLoc -> [EvId] -> [Ct]
mkGivens loc ev_ids
= map mk ev_ids
where
mk ev_id = mkNonCanonical (CtGiven { ctev_evar = ev_id
, ctev_pred = evVarPred ev_id
, ctev_loc = loc })
ctEvidence :: Ct -> CtEvidence
ctEvidence = cc_ev
......
......@@ -55,7 +55,7 @@ module TcSMonad (
getUnsolvedInerts,
removeInertCts, getPendingScDicts,
addInertCan, addInertEq, insertFunEq,
emitInsoluble, emitWorkNC,
emitInsoluble, emitWorkNC, emitWork,
-- The Model
InertModel, kickOutAfterUnification,
......
......@@ -30,7 +30,7 @@ import PrelNames
import TcErrors
import TcEvidence
import TcInteract
import TcCanonical ( makeSuperClasses, mkGivensWithSuperClasses )
import TcCanonical ( makeSuperClasses )
import TcMType as TcM
import TcRnMonad as TcM
import TcSMonad as TcS
......@@ -446,7 +446,7 @@ tcCheckSatisfiability given_ids
; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
; (res, _ev_binds) <- runTcS $
do { traceTcS "checkSatisfiability {" (ppr given_ids)
; given_cts <- mkGivensWithSuperClasses given_loc (bagToList given_ids)
; let given_cts = mkGivens given_loc (bagToList given_ids)
-- See Note [Superclasses and satisfiability]
; insols <- solveSimpleGivens given_cts
; insols <- try_harder insols
......@@ -558,7 +558,7 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
<- setTcLevel rhs_tclvl $
runTcSWithEvBinds False (Just ev_binds_var) $
do { let loc = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env
; psig_givens <- mkGivensWithSuperClasses loc psig_theta_vars
psig_givens = mkGivens loc psig_theta_vars
; _ <- solveSimpleGivens psig_givens
-- See Note [Add signature contexts as givens]
; solveWanteds wanteds }
......@@ -1216,9 +1216,9 @@ solveImplication imp@(Implic { ic_tclvl = tclvl
-- Solve the nested constraints
; ((no_given_eqs, given_insols, residual_wanted), used_tcvs)
<- nestImplicTcS m_ev_binds (mkVarSet (skols ++ given_ids)) tclvl $
do { let loc = mkGivenLoc tclvl info env
; givens_w_scs <- mkGivensWithSuperClasses loc given_ids
; given_insols <- solveSimpleGivens givens_w_scs
do { let loc = mkGivenLoc tclvl info env
givens = mkGivens loc given_ids
; given_insols <- solveSimpleGivens givens
; residual_wanted <- solveWanteds wanteds
-- solveWanteds, *not* solveWantedsAndDrop, because
......
{-# LANGUAGE ConstraintKinds, MultiParamTypeClasses, TypeFamilies,
UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
module T12175 where
import GHC.Exts
class Foo a
instance Foo a => Foo (a,b)
type family TElt r :: Constraint
type instance TElt r = (Foo r, ())
-- type TElt r = (Foo r, Eq r)
data CT r = CT [r]
toCT :: Foo r => CT r -> CT r
toCT = undefined
foo :: CT (a,b) -> (CT a, CT b)
foo = undefined
unzipT :: TElt (a,b) => CT (a,b) -> (CT a, CT b)
unzipT x = foo (toCT x)
{- Type checking for unzipT
[G] TElt (a,b)
--> {by rewrite} (Foo (a,b), ())
--> {by superclasses of tuple} Foo (a,b), ()
toCT @(a,b)
--> [W] Foo (a,b)
--> {by instance decl} Foo a (insoluble)
-}
......@@ -275,3 +275,4 @@ test('T11361', normal, compile, ['-dunique-increment=-1'])
# -dunique-increment=-1 doesn't work inside the file
test('T11361a', normal, compile_fail, [''])
test('T11581', normal, compile, [''])
test('T12175', 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