Commit ff82387d authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Decompose wanted repr. eqs. when no matchable givens.

This is pursuant to a conversion with SPJ, where we agreed that
the logic behind Note [Instance and Given overlap] in TcInteract
applied to newtype decomposition for representational equality.

There is no bug report or test case, as tickling this kind of thing
is quite hard to do!
parent 66440396
......@@ -33,6 +33,7 @@ import DataCon ( dataConName )
import Pair
import Util
import Bag
import MonadUtils ( zipWith3M, zipWith3M_ )
import Data.List ( zip4 )
import BasicTypes
......@@ -655,13 +656,16 @@ canDecomposableTyConApp :: CtEvidence -> EqRel
canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
| tc1 == tc2
, length tys1 == length tys2
= if eq_rel == NomEq || ctEvFlavour ev /= Given || isDistinctTyCon tc1
-- See Note [Decomposing newtypes]
then do { traceTcS "canDecomposableTyConApp"
(ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
; stopWith ev "Decomposed TyConApp" }
else canEqFailure ev eq_rel ty1 ty2
= do { inerts <- getTcSInerts
; if eq_rel == NomEq -- NomEq doesn't care about newtype vs. data
|| isDistinctTyCon tc1 -- always good to decompose non-newtypes
|| (ctEvFlavour ev /= Given && isEmptyBag (matchableGivens loc pred inerts))
-- See Note [Decomposing newtypes]
then do { traceTcS "canDecomposableTyConApp"
(ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
; stopWith ev "Decomposed TyConApp" }
else canEqFailure ev eq_rel ty1 ty2 }
-- Fail straight away for better error messages
-- See Note [Use canEqFailure in canDecomposableTyConApp]
......@@ -673,6 +677,9 @@ canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
ty1 = mkTyConApp tc1 tys1
ty2 = mkTyConApp tc2 tys2
loc = ctEvLoc ev
pred = ctEvPred ev
{-
Note [Use canEqFailure in canDecomposableTyConApp]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -701,13 +708,15 @@ As explained in Note [NthCo and newtypes] in Coercion, we can't use
NthCo on representational coercions over newtypes. So we avoid doing
so.
But is it sensible to decompose *Wanted* constraints over newtypes?
Yes. By the time we reach canDecomposableTyConApp, we know that any
newtypes that can be unwrapped have been. So, without importing more
constructors, say, we know there is no way forward other than decomposition.
So we take the one route we have available. This *does* mean that
importing a newtype's constructor might make code that previously
compiled fail to do so. (If that newtype is perversely recursive, say.)
But is it sensible to decompose *Wanted* constraints over newtypes? Yes, as
long as there are no Givens that might (later) influence Coercible solving.
(See Note [Instance and Given overlap] in TcInteract.) By the time we reach
canDecomposableTyConApp, we know that any newtypes that can be unwrapped have
been. So, without importing more constructors, say, we know there is no way
forward other than decomposition. So we take the one route we have available.
This *does* mean that importing a newtype's constructor might make code that
previously compiled fail to do so. (If that newtype is perversely recursive,
say.)
-}
canDecomposableTyConAppOK :: CtEvidence -> EqRel
......
......@@ -15,7 +15,6 @@ import TcFlatten
import VarSet
import Type
import Kind ( isKind, isConstraintKind )
import Unify
import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
import CoAxiom(sfInteractTop, sfInteractInert)
......@@ -568,15 +567,6 @@ solveOneFromTheOther ev_i ev_w
has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev))
prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
-- See Note [Solving superclass constraints] in TcInstDcls
prohibitedSuperClassSolve from_loc solve_loc
| GivenOrigin (InstSC given_size) <- ctLocOrigin from_loc
, ScOrigin wanted_size <- ctLocOrigin solve_loc
= given_size >= wanted_size
| otherwise
= False
{-
Note [Replacement vs keeping]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -1636,33 +1626,14 @@ matchClassInst :: DynFlags -> InertSet -> Class -> [Type] -> CtLoc -> TcS Lookup
-- instances. See Note [Instance and Given overlap]
matchClassInst dflags inerts clas tys loc
| not (xopt Opt_IncoherentInstances dflags)
, let matchable_givens = matchableGivens loc pred inerts
, not (isEmptyBag matchable_givens)
= do { traceTcS "Delaying instance application" $
vcat [ text "Work item=" <+> pprType (mkClassPred clas tys)
, text "Relevant given dictionaries="
<+> ppr matchable_givens ]
vcat [ text "Work item=" <+> pprType pred
, text "Potential matching givens:" <+> ppr matchable_givens ]
; return NoInstance }
where
matchable_givens :: Cts
matchable_givens = filterBag matchable_given $
findDictsByClass (inert_dicts $ inert_cans inerts) clas
matchable_given ct
| CDictCan { cc_class = clas_g, cc_tyargs = sys, cc_ev = fl } <- ct
, CtGiven { ctev_loc = loc_g } <- fl
, Just {} <- tcUnifyTys bind_meta_tv tys sys
, not (prohibitedSuperClassSolve loc_g loc)
= ASSERT( clas_g == clas ) True
matchable_given _ = False
bind_meta_tv :: TcTyVar -> BindFlag
-- Any meta tyvar may be unified later, so we treat it as
-- bindable when unifying with givens. That ensures that we
-- conservatively assume that a meta tyvar might get unified with
-- something that matches the 'given', until demonstrated
-- otherwise.
bind_meta_tv tv | isMetaTyVar tv = BindMe
| otherwise = Skolem
pred = mkClassPred clas tys
matchClassInst _ _ clas [ ty ] _
| className clas == knownNatClassName
......
......@@ -9,7 +9,7 @@ module TcSMonad (
extendWorkListCts, appendWorkList,
selectNextWorkItem,
workListSize, workListWantedCount,
updWorkListTcS,
updWorkListTcS,
-- The TcS monad
TcS, runTcS, runTcSWithEvBinds,
......@@ -42,6 +42,7 @@ module TcSMonad (
getNoGivenEqs, setInertCans,
getInertEqs, getInertCans, getInertModel, getInertGivens,
emptyInert, getTcSInerts, setTcSInerts, takeGivenInsolubles,
matchableGivens, prohibitedSuperClassSolve,
getUnsolvedInerts,
removeInertCts,
addInertCan, addInertEq, insertFunEq,
......@@ -115,6 +116,7 @@ import Kind
import TcType
import DynFlags
import Type
import Unify
import TcEvidence
import Class
......@@ -1653,6 +1655,56 @@ getNoGivenEqs tclvl skol_tvs
FlatSkol {} -> not (tv `elemVarSet` local_fsks)
_ -> False
-- | Returns Given constraints that might,
-- potentially, match the given pred. This is used when checking to see if a
-- Given might overlap with an instance. See Note [Instance and Given overlap]
-- in TcInteract.
matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
matchableGivens loc_w pred (IS { inert_cans = inert_cans })
= filterBag matchable_given all_relevant_givens
where
-- just look in class constraints and irreds. matchableGivens does get called
-- for ~R constraints, but we don't need to look through equalities, because
-- canonical equalities are used for rewriting. We'll only get caught by
-- non-canonical -- that is, irreducible -- equalities.
all_relevant_givens :: Cts
all_relevant_givens
| Just (clas, _) <- getClassPredTys_maybe pred
= findDictsByClass (inert_dicts inert_cans) clas
`unionBags` inert_irreds inert_cans
| otherwise
= inert_irreds inert_cans
matchable_given :: Ct -> Bool
matchable_given ct
| CtGiven { ctev_loc = loc_g } <- ctev
, Just _ <- tcUnifyTys bind_meta_tv [ctEvPred ctev] [pred]
, not (prohibitedSuperClassSolve loc_g loc_w)
= True
| otherwise
= False
where
ctev = cc_ev ct
bind_meta_tv :: TcTyVar -> BindFlag
-- Any meta tyvar may be unified later, so we treat it as
-- bindable when unifying with givens. That ensures that we
-- conservatively assume that a meta tyvar might get unified with
-- something that matches the 'given', until demonstrated
-- otherwise.
bind_meta_tv tv | isMetaTyVar tv = BindMe
| otherwise = Skolem
prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
-- See Note [Solving superclass constraints] in TcInstDcls
prohibitedSuperClassSolve from_loc solve_loc
| GivenOrigin (InstSC given_size) <- ctLocOrigin from_loc
, ScOrigin wanted_size <- ctLocOrigin solve_loc
= given_size >= wanted_size
| otherwise
= False
{-
Note [When does an implication have given equalities?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -2175,7 +2227,7 @@ checkForCyclicBinds ev_binds
is_co_bind (EvBind { eb_lhs = b }) = isEqVar b
edges :: [(EvBind, EvVar, [EvVar])]
edges = [(bind, bndr, varSetElems (evVarsOfTerm rhs))
edges = [(bind, bndr, varSetElems (evVarsOfTerm rhs))
| bind@(EvBind { eb_lhs = bndr, eb_rhs = rhs }) <- bagToList ev_binds]
#endif
......@@ -2816,4 +2868,3 @@ deferTcSForAllEq role loc (tvs1,body1) (tvs2,body2)
; return (TcLetCo ev_binds new_co) }
; return $ EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs) }
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