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

Merge branch 'tc-untouchables' of http://darcs.haskell.org/ghc into tc-untouchables

parents 316d3edc b3f2f732
......@@ -177,7 +177,9 @@ tcLookupFamInst tycon tys
| otherwise
= do { instEnv <- tcGetFamInstEnvs
; let mb_match = lookupFamInstEnv instEnv tycon tys
; traceTc "lookupFamInst" ((ppr tycon <+> ppr tys) $$ pprTvBndrs (varSetElems (tyVarsOfTypes tys)) $$ ppr mb_match $$ ppr instEnv)
-- ; traceTc "lookupFamInst" ((ppr tycon <+> ppr tys) $$
-- pprTvBndrs (varSetElems (tyVarsOfTypes tys)) $$
-- ppr mb_match $$ ppr instEnv)
; case mb_match of
[] -> return Nothing
((fam_inst, rep_tys):_)
......
......@@ -247,20 +247,15 @@ canClassNC d ev cls tys
`andWhenContinue` emitSuperclasses
canClass d ev cls tys
= do { -- sctx <- getTcSContext
; (xis, cos) <- flattenMany d FMFullFlatten (ctEvFlavour ev) tys
= do { (xis, cos) <- flattenMany d FMFullFlatten (ctEvFlavour ev) tys
; let co = mkTcTyConAppCo (classTyCon cls) cos
xi = mkClassPred cls xis
; mb <- rewriteCtFlavor ev xi co
; case mb of
Just new_ev ->
let (ClassPred cls xis_for_dict) = classifyPredType (ctEvPred new_ev)
in continueWith $
CDictCan { cc_ev = new_ev, cc_loc = d
, cc_tyargs = xis_for_dict, cc_class = cls }
Nothing -> return Stop }
Nothing -> return Stop
Just new_ev -> continueWith $
CDictCan { cc_ev = new_ev, cc_loc = d
, cc_tyargs = xis, cc_class = cls } }
emitSuperclasses :: Ct -> TcS StopOrContinue
emitSuperclasses ct@(CDictCan { cc_loc = d, cc_ev = ev
......@@ -567,24 +562,22 @@ flatten loc f ctxt (TyConApp tc tys)
, cc_tyargs = xi_args
, cc_rhs = rhs_ty
, cc_loc = loc }
; updWorkListTcS $ extendWorkListEq ct
; updWorkListTcS $ extendWorkListFunEq ct
; return (co, rhs_ty) }
| otherwise -- Wanted or Derived: make new unification variable
-> do { traceTcS "flatten/flat-cache miss" $ empty
; rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
; let pred = mkTcEqPred fam_ty rhs_xi_var
; mw <- newWantedEvVar pred
; case mw of
Fresh ctev ->
do { let ct = CFunEqCan { cc_ev = ctev
, cc_fun = tc
, cc_tyargs = xi_args
, cc_rhs = rhs_xi_var
, cc_loc = loc }
; updWorkListTcS $ extendWorkListEq ct
; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var) }
Cached {} -> panic "flatten TyConApp, var must be fresh!" }
; ctev <- newWantedEvVarNC (mkTcEqPred fam_ty rhs_xi_var)
-- NC (no-cache) version because we've already
-- looked in the solved goals an inerts (lookupFlatEqn)
; let ct = CFunEqCan { cc_ev = ctev
, cc_fun = tc
, cc_tyargs = xi_args
, cc_rhs = rhs_xi_var
, cc_loc = loc }
; updWorkListTcS $ extendWorkListFunEq ct
; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var) }
}
-- Emit the flat constraints
; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable
......@@ -1071,19 +1064,15 @@ reOrient :: CtEvidence -> TypeClassifier -> TypeClassifier -> Bool
-- We try to say False if possible, to minimise evidence generation
--
-- Postcondition: After re-orienting, first arg is not OTherCls
reOrient _ev (OtherCls {}) (FunCls {}) = True
reOrient _ev (OtherCls {}) (VarCls {}) = True
reOrient _ev (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun
reOrient _ev (OtherCls {}) cls2 = ASSERT( case cls2 of { OtherCls {} -> False; _ -> True } )
True -- One must be Var/Fun
reOrient _ev (FunCls {}) (VarCls _tv) = False
reOrient _ev (FunCls {}) _ = False -- Fun/Other on rhs
-- But consider the following variation: isGiven ev && isMetaTyVar tv
-- See Note [No touchables as FunEq RHS] in TcSMonad
reOrient _ev (FunCls {}) _ = False -- Fun/Other on rhs
reOrient _ev (VarCls {}) (FunCls {}) = True
reOrient _ev (VarCls {}) (OtherCls {}) = False
reOrient _ev (VarCls {}) (FunCls {}) = True
reOrient _ev (VarCls {}) (OtherCls {}) = False
reOrient _ev (VarCls tv1) (VarCls tv2)
| isMetaTyVar tv2 && not (isMetaTyVar tv1) = True
| otherwise = False
......@@ -1153,7 +1142,7 @@ canEqLeafFunEq loc ev fn tys1 ty2 -- ev :: F tys1 ~ ty2
Nothing -> return Stop ;
Just new_ev
| isTcReflCo xco -> continueWith new_ct
| otherwise -> do { updWorkListTcS (extendWorkListEq new_ct); return Stop }
| otherwise -> do { updWorkListTcS (extendWorkListFunEq new_ct); return Stop }
where
new_ct = CFunEqCan { cc_ev = new_ev, cc_loc = loc
, cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 } } }
......
......@@ -296,11 +296,10 @@ spontaneousSolveStage workItem
SPSolved new_tv
-- Post: tv ~ xi is now in TyBinds, no need to put in inerts as well
-- see Note [Spontaneously solved in TyBinds]
-> do { bumpStepCountTcS
; traceFireTcS workItem $
ptext (sLit "Spontaneously solved:") <+> ppr workItem
; kickOutRewritable Given new_tv
; return Stop } }
-> do { traceFireTcS workItem $
ptext (sLit "Spontaneously solved:") <+> ppr workItem
; kickOutRewritable Given new_tv
; return Stop } }
\end{code}
Note [Spontaneously solved in TyBinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -649,19 +648,16 @@ interactWithInertsStage wi
, ptext (sLit "WorkItem =") <+> ppr wi ]
; case ir of
IRWorkItemConsumed { ir_fire = rule }
-> do { bumpStepCountTcS
; traceFireTcS wi (mk_msg rule (text "WorkItemConsumed"))
-> do { traceFireTcS wi (mk_msg rule (text "WorkItemConsumed"))
; insertInertItemTcS atomic_inert
; return Stop }
IRReplace { ir_fire = rule }
-> do { bumpStepCountTcS
; traceFireTcS atomic_inert
-> do { traceFireTcS atomic_inert
(mk_msg rule (text "InertReplace"))
; insertInertItemTcS wi
; return Stop }
IRInertConsumed { ir_fire = rule }
-> do { bumpStepCountTcS
; traceFireTcS atomic_inert
-> do { traceFireTcS atomic_inert
(mk_msg rule (text "InertItemConsumed"))
; return (ContinueWith wi) }
IRKeepGoing {} -- Should we do a bumpStepCountTcS? No for now.
......@@ -726,8 +722,9 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
, cc_tyargs = args1, cc_rhs = xi1, cc_loc = d1 })
wi@(CFunEqCan { cc_ev = ev2, cc_fun = tc2
, cc_tyargs = args2, cc_rhs = xi2, cc_loc = d2 })
| fl1 `canSolve` fl2 && lhss_match
= do { traceTcS "interact with inerts: FunEq/FunEq" $
| fl1 `canSolve` fl2
= ASSERT( lhss_match ) -- extractRelevantInerts ensures this
do { traceTcS "interact with inerts: FunEq/FunEq" $
vcat [ text "workItem =" <+> ppr wi
, text "inertItem=" <+> ppr ii ]
......@@ -744,8 +741,9 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
; emitWorkNC d2 ctevs
; return (IRWorkItemConsumed "FunEq/FunEq") }
| fl2 `canSolve` fl1 && lhss_match
= do { traceTcS "interact with inerts: FunEq/FunEq" $
| fl2 `canSolve` fl1
= ASSERT( lhss_match ) -- extractRelevantInerts ensures this
do { traceTcS "interact with inerts: FunEq/FunEq" $
vcat [ text "workItem =" <+> ppr wi
, text "inertItem=" <+> ppr ii ]
......@@ -1027,7 +1025,7 @@ So our problem is this
We may add the given in the inert set, along with its superclasses
[assuming we don't fail because there is a matching instance, see
tryTopReact, given case ]
topReactionsStage, given case ]
Inert:
d0 :_g Foo t
WorkList
......@@ -1339,20 +1337,14 @@ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
*********************************************************************************
\begin{code}
topReactionsStage :: SimplifierStage
topReactionsStage workItem
= tryTopReact workItem
tryTopReact :: WorkItem -> TcS StopOrContinue
tryTopReact wi
topReactionsStage :: WorkItem -> TcS StopOrContinue
topReactionsStage wi
= do { inerts <- getTcSInerts
; tir <- doTopReact inerts wi
; case tir of
NoTopInt -> return (ContinueWith wi)
SomeTopInt rule what_next
-> do { bumpStepCountTcS
; traceFireTcS wi $
-> do { traceFireTcS wi $
vcat [ ptext (sLit "Top react:") <+> text rule
, text "WorkItem =" <+> ppr wi ]
; return what_next } }
......@@ -1440,18 +1432,18 @@ doTopReactFunEq :: Ct -> CtEvidence -> TyCon -> [Xi] -> Xi
-> CtLoc -> TcS TopInteractResult
doTopReactFunEq ct fl fun_tc args xi loc
= ASSERT (isSynFamilyTyCon fun_tc) -- No associated data families have
-- reached that far
-- First look in the cache of solved funeqs
-- reached this far
-- Look in the cache of solved funeqs
do { fun_eq_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
; case lookupFamHead fun_eq_cache fam_ty of {
Just (CFunEqCan { cc_ev = ctev, cc_rhs = rhs_ty })
-> ASSERT( not (isDerived ctev) )
succeed_with "Fun/Cache" (evTermCoercion (ctEvTerm ctev)) rhs_ty ;
Just {} -> pprPanic "doTopReactFunEq" (ppr ct) ;
Nothing ->
-- No cached solved, so look up in top-level instances
Just (CFunEqCan { cc_ev = ctev, cc_rhs = rhs_ty })
| ctEvFlavour ctev `canRewrite` ctEvFlavour fl
-> ASSERT( not (isDerived ctev) )
succeed_with "Fun/Cache" (evTermCoercion (ctEvTerm ctev)) rhs_ty ;
Just ct' -> pprPanic "doTopReactFunEq" (ppr ct') ;
Nothing ->
-- Look up in top-level instances
do { match_res <- matchFam fun_tc args -- See Note [MATCHING-SYNONYMS]
; case match_res of {
Nothing -> return NoTopInt ;
......@@ -1462,7 +1454,7 @@ doTopReactFunEq ct fl fun_tc args xi loc
unless (isDerived fl) (addSolvedFunEq ct fam_ty)
; let coe_ax = famInstAxiom famInst
; succeed_with "Fun/Top"(mkTcAxInstCo coe_ax rep_tys)
; succeed_with "Fun/Top" (mkTcAxInstCo coe_ax rep_tys)
(mkAxInstRHS coe_ax rep_tys) } } } } }
where
fam_ty = mkTyConApp fun_tc args
......
......@@ -155,17 +155,17 @@ newWantedEvVars theta = mapM newWantedEvVar theta
newEvVar :: TcPredType -> TcM EvVar
-- Creates new *rigid* variables for predicates
newEvVar ty = do { name <- newName (predTypeOccName ty)
newEvVar ty = do { name <- newSysName (predTypeOccName ty)
; return (mkLocalId name ty) }
newEq :: TcType -> TcType -> TcM EvVar
newEq ty1 ty2
= do { name <- newName (mkVarOccFS (fsLit "cobox"))
= do { name <- newSysName (mkVarOccFS (fsLit "cobox"))
; return (mkLocalId name (mkTcEqPred ty1 ty2)) }
newDict :: Class -> [TcType] -> TcM DictId
newDict cls tys
= do { name <- newName (mkDictOcc (getOccName cls))
= do { name <- newSysName (mkDictOcc (getOccName cls))
; return (mkLocalId name (mkClassPred cls tys)) }
predTypeOccName :: PredType -> OccName
......@@ -679,7 +679,7 @@ zonkFlats binds_var untch cts
, not (tv `elemVarSet` tyVarsOfType ty_lhs)
-- , Just ty_lhs' <- occurCheck tv ty_lhs
= ASSERT2( isWantedCt orig_ct, ppr orig_ct )
ASSERT2( case orig_ct of { CFunEqCan {} -> True; _ -> False }, ppr orig_ct )
ASSERT2( case tcSplitTyConApp_maybe ty_lhs of { Just (tc,_) -> isSynFamilyTyCon tc; _ -> False }, ppr orig_ct )
do { writeMetaTyVar tv ty_lhs
; let evterm = EvCoercion (mkTcReflCo ty_lhs)
evvar = ctev_evar (cc_ev zct)
......
......@@ -376,6 +376,11 @@ newName occ
; loc <- getSrcSpanM
; return (mkInternalName uniq occ loc) }
newSysName :: OccName -> TcM Name
newSysName occ
= do { uniq <- newUnique
; return (mkSystemName uniq occ) }
newSysLocalIds :: FastString -> [TcType] -> TcRnIf gbl lcl [TcId]
newSysLocalIds fs tys
= do { us <- newUniqueSupply
......
......@@ -13,7 +13,8 @@ module TcSMonad (
WorkList(..), isEmptyWorkList, emptyWorkList,
workListFromEq, workListFromNonEq, workListFromCt,
extendWorkListEq, extendWorkListNonEq, extendWorkListCt,
extendWorkListEq, extendWorkListFunEq,
extendWorkListNonEq, extendWorkListCt,
extendWorkListCts, extendWorkListEqs, appendWorkList, selectWorkItem,
withWorkList,
......@@ -31,7 +32,7 @@ module TcSMonad (
mkGivenLoc,
TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality
traceFireTcS, bumpStepCountTcS,
traceFireTcS,
tryTcS, nestTcS, nestImplicTcS, recoverTcS,
wrapErrTcS, wrapWarnTcS,
......@@ -46,7 +47,7 @@ module TcSMonad (
xCtFlavor, -- Transform a CtEvidence during a step
rewriteCtFlavor, -- Specialized version of xCtFlavor for coercions
newWantedEvVar, instDFunConstraints,
newWantedEvVar, newWantedEvVarNC, instDFunConstraints,
newDerived,
-- Creation of evidence variables
......@@ -167,8 +168,8 @@ mkKindErrorCtxtTcS ty1 ki1 ty2 ki2
%* *
%************************************************************************
Note [WorkList]
~~~~~~~~~~~~~~~
Note [WorkList priorities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
A WorkList contains canonical and non-canonical items (of all flavors).
Notice that each Ct now has a simplification depth. We may
consider using this depth for prioritization as well in the future.
......@@ -179,6 +180,7 @@ so that it's easier to deal with them first, but the separation
is not strictly necessary. Notice that non-canonical constraints
are also parts of the worklist.
Note [NonCanonical Semantics]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note that canonical constraints involve a CNonCanonical constructor. In the worklist
......@@ -219,7 +221,7 @@ extractDeque (DQ [] bs) = case reverse bs of
(a:as) -> Just (DQ as [], a)
[] -> panic "extractDeque"
-- See Note [WorkList]
-- See Note [WorkList priorities]
data WorkList = WorkList { wl_eqs :: [Ct]
, wl_funeqs :: Deque Ct
, wl_rest :: [Ct]
......@@ -237,10 +239,14 @@ extendWorkListEq :: Ct -> WorkList -> WorkList
-- Extension by equality
extendWorkListEq ct wl
| Just {} <- isCFunEqCan_Maybe ct
= wl { wl_funeqs = insertDeque ct (wl_funeqs wl) }
= extendWorkListFunEq ct wl
| otherwise
= wl { wl_eqs = ct : wl_eqs wl }
extendWorkListFunEq :: Ct -> WorkList -> WorkList
extendWorkListFunEq ct wl
= wl { wl_funeqs = insertDeque ct (wl_funeqs wl) }
extendWorkListEqs :: [Ct] -> WorkList -> WorkList
-- Append a list of equalities
extendWorkListEqs cts wl = foldr extendWorkListEq wl cts
......@@ -954,17 +960,14 @@ traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
instance HasDynFlags TcS where
getDynFlags = wrapTcS getDynFlags
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
; n <- TcM.readTcRef ref
; TcM.writeTcRef ref (n+1) }
traceFireTcS :: Ct -> SDoc -> TcS ()
-- Dump a rule-firing trace
-- Dump a rule-firing trace, and bumpt the counter
traceFireTcS ct doc
= TcS $ \env ->
TcM.ifDOptM Opt_D_dump_cs_trace $
do { n <- TcM.readTcRef (tcs_count env)
do { let count_ref = tcs_count env
; n <- TcM.readTcRef count_ref
; TcM.writeTcRef count_ref (n+1)
; let msg = int n <> brackets (int (ctLocDepth (cc_loc ct))) <+> doc
; TcM.dumpTcRn msg }
......@@ -1404,6 +1407,12 @@ newGivenEvVar pred rhs
; setEvBind new_ev rhs
; return (CtGiven { ctev_pred = pred, ctev_evtm = EvId new_ev }) }
newWantedEvVarNC :: TcPredType -> TcS CtEvidence
-- Don't look up in the solved/inerts; we know it's not there
newWantedEvVarNC pty
= do { new_ev <- wrapTcS $ TcM.newEvVar pty
; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev })}
newWantedEvVar :: TcPredType -> TcS MaybeNew
newWantedEvVar pty
= do { mb_ct <- lookupInInerts pty
......@@ -1411,10 +1420,8 @@ newWantedEvVar pty
Just ctev | not (isDerived ctev)
-> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
; return (Cached (ctEvTerm ctev)) }
_ -> do { new_ev <- wrapTcS $ TcM.newEvVar pty
; traceTcS "newWantedEvVar/cache miss" $ ppr new_ev
; let ctev = CtWanted { ctev_pred = pty
, ctev_evar = new_ev }
_ -> do { ctev <- newWantedEvVarNC pty
; traceTcS "newWantedEvVar/cache miss" $ ppr ctev
; return (Fresh ctev) } }
newDerived :: TcPredType -> TcS (Maybe CtEvidence)
......@@ -1471,7 +1478,7 @@ See Note [Coercion evidence terms] in TcEvidence.
\begin{code}
xCtFlavor :: CtEvidence -- Original flavor
xCtFlavor :: CtEvidence -- Original flavor
-> [TcPredType] -- New predicate types
-> XEvTerm -- Instructions about how to manipulate evidence
-> TcS [CtEvidence]
......
......@@ -1013,18 +1013,21 @@ happy to have types of kind Constraint on either end of an arrow.
matchExpectedFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
-- Like unifyFunTy, but does not fail; instead just returns Nothing
matchExpectedFunKind (TyVarTy kvar) = do
maybe_kind <- readMetaTyVar kvar
case maybe_kind of
Indirect fun_kind -> matchExpectedFunKind fun_kind
Flexi ->
do { arg_kind <- newMetaKindVar
; res_kind <- newMetaKindVar
; writeMetaTyVar kvar (mkArrowKind arg_kind res_kind)
; return (Just (arg_kind,res_kind)) }
matchExpectedFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind))
matchExpectedFunKind _ = return Nothing
matchExpectedFunKind (FunTy arg_kind res_kind)
= return (Just (arg_kind,res_kind))
matchExpectedFunKind (TyVarTy kvar)
| isTcTyVar kvar, isMetaTyVar kvar
= do { maybe_kind <- readMetaTyVar kvar
; case maybe_kind of
Indirect fun_kind -> matchExpectedFunKind fun_kind
Flexi ->
do { arg_kind <- newMetaKindVar
; res_kind <- newMetaKindVar
; writeMetaTyVar kvar (mkArrowKind arg_kind res_kind)
; return (Just (arg_kind,res_kind)) } }
matchExpectedFunKind _ = return Nothing
-----------------
unifyKindX :: TcKind -- k1 (actual)
......
......@@ -418,10 +418,11 @@ ppr_co p co@(ForAllCo {}) = ppr_forall_co p co
ppr_co _ (CoVarCo cv) = parenSymOcc (getOccName cv) (ppr cv)
ppr_co p (AxiomInstCo con cos) = pprTypeNameApp p ppr_co (getName con) cos
ppr_co p (TransCo co1 co2) = maybeParen p FunPrec $
ppr_co FunPrec co1
<+> ptext (sLit ";")
<+> ppr_co FunPrec co2
ppr_co p co@(TransCo {}) = maybeParen p FunPrec $
case trans_co_list co [] of
[] -> panic "ppr_co"
(co:cos) -> sep ( ppr_co FunPrec co
: [ char ';' <+> ppr_co FunPrec co | co <- cos])
ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
pprParendCo co <> ptext (sLit "@") <> pprType ty
......@@ -431,6 +432,10 @@ ppr_co p (SymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo c
ppr_co p (NthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <> int n) [pprParendCo co]
ppr_co p (LRCo sel co) = pprPrefixApp p (ppr sel) [pprParendCo co]
trans_co_list :: Coercion -> [Coercion] -> [Coercion]
trans_co_list (TransCo co1 co2) cos = trans_co_list co1 (trans_co_list co2 cos)
trans_co_list co cos = co : cos
instance Outputable LeftOrRight where
ppr CLeft = ptext (sLit "Left")
ppr CRight = ptext (sLit "Right")
......
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