| Opt_D_dump_rn_stats
| Opt_D_dump_opt_cmm
| Opt_D_dump_simpl_stats
+ | Opt_D_dump_cs_trace -- Constraint solver in type checker
| Opt_D_dump_tc_trace
| Opt_D_dump_if_trace
| Opt_D_dump_splices
, Flag "ddump-worker-wrapper" (setDumpFlag Opt_D_dump_worker_wrapper)
, Flag "ddump-rn-trace" (setDumpFlag Opt_D_dump_rn_trace)
, Flag "ddump-if-trace" (setDumpFlag Opt_D_dump_if_trace)
+ , Flag "ddump-cs-trace" (setDumpFlag Opt_D_dump_cs_trace)
, Flag "ddump-tc-trace" (setDumpFlag Opt_D_dump_tc_trace)
, Flag "ddump-splices" (setDumpFlag Opt_D_dump_splices)
, Flag "ddump-rn-stats" (setDumpFlag Opt_D_dump_rn_stats)
\begin{code}
module TcCanonical(
mkCanonical, mkCanonicals, mkCanonicalFEV, canWanteds, canGivens,
- canOccursCheck, canEq
+ canOccursCheck, canEq,
+ rewriteWithFunDeps
) where
#include "HsVersions.h"
import BasicTypes
import Type
import TcRnTypes
-
+import FunDeps
+import qualified TcMType as TcM
import TcType
import TcErrors
import Coercion
import TypeRep
import Name
import Var
+import VarEnv ( TidyEnv )
import Outputable
import Control.Monad ( unless, when, zipWithM, zipWithM_ )
import MonadUtils
import HsBinds
import TcSMonad
+import FastString
\end{code}
Note [Canonicalisation]
itself, and so on.
+%************************************************************************
+%* *
+%* Functional dependencies, instantiation of equations
+%* *
+%************************************************************************
+\begin{code}
+rewriteWithFunDeps :: [Equation]
+ -> [Xi] -> CtFlavor
+ -> TcS (Maybe ([Xi], [Coercion], CanonicalCts))
+rewriteWithFunDeps eqn_pred_locs xis fl
+ = do { fd_ev_poss <- mapM (instFunDepEqn fl) eqn_pred_locs
+ ; let fd_ev_pos :: [(Int,FlavoredEvVar)]
+ fd_ev_pos = concat fd_ev_poss
+ (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
+ ; fds <- mapM (\(_,fev) -> mkCanonicalFEV fev) fd_ev_pos
+ ; let fd_work = unionManyBags fds
+ ; if isEmptyBag fd_work
+ then return Nothing
+ else return (Just (rewritten_xis, cos, fd_work)) }
+
+instFunDepEqn :: CtFlavor -- Precondition: Only Wanted or Derived
+ -> Equation
+ -> TcS [(Int, FlavoredEvVar)]
+-- Post: Returns the position index as well as the corresponding FunDep equality
+instFunDepEqn fl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
+ , fd_pred1 = d1, fd_pred2 = d2 })
+ = do { let tvs = varSetElems qtvs
+ ; tvs' <- mapM instFlexiTcS tvs
+ ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
+ ; mapM (do_one subst) eqs }
+ where
+ fl' = case fl of
+ Given _ -> panic "mkFunDepEqns"
+ Wanted loc -> Wanted (push_ctx loc)
+ Derived loc -> Derived (push_ctx loc)
+
+ push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
+
+ do_one subst (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
+ = do { let sty1 = substTy subst ty1
+ sty2 = substTy subst ty2
+ ; ev <- newCoVar sty1 sty2
+ ; return (i, mkEvVarX ev fl') }
+
+rewriteDictParams :: [(Int,FlavoredEvVar)] -- A set of coercions : (pos, ty' ~ ty)
+ -> [Type] -- A sequence of types: tys
+ -> [(Type,Coercion)] -- Returns : [(ty', co : ty' ~ ty)]
+rewriteDictParams param_eqs tys
+ = zipWith do_one tys [0..]
+ where
+ do_one :: Type -> Int -> (Type,Coercion)
+ do_one ty n = case lookup n param_eqs of
+ Just wev -> (get_fst_ty wev, mkCoVarCoercion (evVarOf wev))
+ Nothing -> (ty,ty) -- Identity
+
+ get_fst_ty wev = case evVarOfPred wev of
+ EqPred ty1 _ -> ty1
+ _ -> panic "rewriteDictParams: non equality fundep"
+
+mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
+ -> TcM (TidyEnv, SDoc)
+mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
+ = do { zpred1 <- TcM.zonkTcPredType pred1
+ ; zpred2 <- TcM.zonkTcPredType pred2
+ ; let { tpred1 = tidyPred tidy_env zpred1
+ ; tpred2 = tidyPred tidy_env zpred2 }
+ ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
+ nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
+ nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
+ ; return (tidy_env, msg) }
+\end{code}
\ No newline at end of file
import HsBinds
import Inst( tyVarsOfEvVar )
-import InstEnv
import Class
import TyCon
import Name
, ptext (sLit "new work =") <+> ppr work <> comma
, ptext (sLit "stop =") <+> ppr stop])
-type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
+type SubGoalDepth = Int -- Starts at zero; used to limit infinite
+ -- recursion of sub-goals
+type SimplifierStage = SubGoalDepth -> WorkItem -> InertSet -> TcS StageResult
-- Combine a sequence of simplifier 'stages' to create a pipeline
-runSolverPipeline :: [(String, SimplifierStage)]
- -> InertSet -> WorkItem
+runSolverPipeline :: SubGoalDepth
+ -> [(String, SimplifierStage)]
+ -> InertSet -> WorkItem
-> TcS (InertSet, WorkList)
-- Precondition: non-empty list of stages
-runSolverPipeline pipeline inerts workItem
+runSolverPipeline depth pipeline inerts workItem
= do { traceTcS "Start solver pipeline" $
vcat [ ptext (sLit "work item =") <+> ppr workItem
, ptext (sLit "inerts =") <+> ppr inerts]
; let itr_in = SR { sr_inerts = inerts
- , sr_new_work = emptyWorkList
- , sr_stop = ContinueWith workItem }
+ , sr_new_work = emptyWorkList
+ , sr_stop = ContinueWith workItem }
; itr_out <- run_pipeline pipeline itr_in
; let new_inert
= case sr_stop itr_out of
(SR { sr_new_work = accum_work
, sr_inerts = inerts
, sr_stop = ContinueWith work_item })
- = do { itr <- stage work_item inerts
+ = do { itr <- stage depth work_item inerts
; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr }
; run_pipeline stages itr' }
-- new inert set which has assimilated the new information.
solveOneWithDepth :: (Int, Int, [WorkItem])
-> InertSet -> WorkItem -> TcS InertSet
-solveOneWithDepth (max_depth, n, stack) inert work
- = do { traceTcS0 (indent ++ "Solving {") (ppr work)
- ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
+solveOneWithDepth (max_depth, depth, stack) inert work
+ = do { traceFireTcS depth (text "Solving {" <+> ppr work)
+ ; (new_inert, new_work) <- runSolverPipeline depth thePipeline inert work
- ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
-
-- Recursively solve the new work generated
-- from workItem, with a greater depth
- ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
+ ; res_inert <- solveInteractWithDepth (max_depth, depth+1, work:stack)
new_inert new_work
- ; traceTcS0 (indent ++ "Done }") (ppr work)
+ ; traceFireTcS depth (text "Done }" <+> ppr work)
+
; return res_inert }
- where
- indent = replicate (2*n) ' '
thePipeline :: [(String,SimplifierStage)]
thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
\begin{code}
spontaneousSolveStage :: SimplifierStage
-spontaneousSolveStage workItem inerts
+spontaneousSolveStage depth workItem inerts
= do { mSolve <- trySpontaneousSolve workItem
; case mSolve of
-- its status change. This in turn may produce more work.
-- We do this *right now* (rather than just putting workItem'
-- back into the work-list) because we've solved
- -> do { (new_inert, new_work) <- runSolverPipeline
+ -> do { bumpStepCountTcS
+ ; traceFireTcS depth (ptext (sLit "Spontaneous (w/d)") <+> ppr workItem)
+ ; (new_inert, new_work) <- runSolverPipeline depth
[ ("recursive interact with inert eqs", interactWithInertEqsStage)
, ("recursive interact with inerts", interactWithInertsStage)
] inerts workItem'
| otherwise
-> -- Original was given; he must then be inert all right, and
-- workList' are all givens from flattening
- return $ SR { sr_new_work = emptyWorkList
- , sr_inerts = inerts `updInertSet` workItem'
- , sr_stop = Stop }
+ do { bumpStepCountTcS
+ ; traceFireTcS depth (ptext (sLit "Spontaneous (g)") <+> ppr workItem)
+ ; return $ SR { sr_new_work = emptyWorkList
+ , sr_inerts = inerts `updInertSet` workItem'
+ , sr_stop = Stop } }
SPError -> -- Return with no new work
return $ SR { sr_new_work = emptyWorkList
, sr_inerts = inerts
| otherwise
= do { tch1 <- isTouchableMetaTyVar tv1
; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi
- else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem)
+ else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:"
+ (ppr workItem)
; return SPCantSolve }
}
, ir_new_work :: WorkList
-- new work items to add to the WorkList
+
+ , ir_fire :: Maybe String -- Tells whether a rule fired, and if so what
}
-- What to do with the inert reactant.
-data InertAction = KeepInert
- | DropInert
- | KeepTransformedInert CanonicalCt -- Keep a slightly transformed inert
-
-mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
-mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork
+data InertAction = KeepInert | DropInert
-mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
-mkIRStop keep newWork = return $ IR Stop keep newWork
+mkIRContinue :: String -> WorkItem -> InertAction -> WorkList -> TcS InteractResult
+mkIRContinue rule wi keep newWork
+ = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = keep
+ , ir_new_work = newWork, ir_fire = Just rule }
-dischargeWorkItem :: Monad m => m InteractResult
-dischargeWorkItem = mkIRStop KeepInert emptyWorkList
+mkIRStop :: String -> WorkList -> TcS InteractResult
+mkIRStop rule newWork
+ = return $ IR { ir_stop = Stop, ir_inert_action = KeepInert
+ , ir_new_work = newWork, ir_fire = Just rule }
noInteraction :: Monad m => WorkItem -> m InteractResult
-noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
+noInteraction wi
+ = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = KeepInert
+ , ir_new_work = emptyWorkList, ir_fire = Nothing }
data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
-- See Note [Efficient Orientation]
-- interact the WorkItem with the entire equalities of the InertSet
interactWithInertEqsStage :: SimplifierStage
-interactWithInertEqsStage workItem inert
- = Bag.foldlBagM interactNext initITR (inert_eqs inert)
+interactWithInertEqsStage depth workItem inert
+ = Bag.foldlBagM (interactNext depth) initITR (inert_eqs inert)
where
initITR = SR { sr_inerts = inert { inert_eqs = emptyCCan }
, sr_new_work = emptyWorkList
-- "Other" constraints it contains!
interactWithInertsStage :: SimplifierStage
-interactWithInertsStage workItem inert
+interactWithInertsStage depth workItem inert
= let (relevant, inert_residual) = getISRelevant workItem inert
initITR = SR { sr_inerts = inert_residual
, sr_new_work = emptyWorkList
, sr_stop = ContinueWith workItem }
- in Bag.foldlBagM interactNext initITR relevant
+ in Bag.foldlBagM (interactNext depth) initITR relevant
where
getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet)
getISRelevant (CFrozenErr {}) is = (emptyCCan, is)
, inert_ips = emptyCCanMap
, inert_funeqs = emptyCCanMap })
-interactNext :: StageResult -> AtomicInert -> TcS StageResult
-interactNext it inert
- | ContinueWith workItem <- sr_stop it
- = do { let inerts = sr_inerts it
-
- ; ir <- interactWithInert inert workItem
-
- -- New inerts depend on whether we KeepInert or not and must
- -- be updated with FD improvement information from the interaction result (ir)
- ; let inerts_new = case ir_inert_action ir of
- KeepInert -> inerts `updInertSet` inert
- DropInert -> inerts
- KeepTransformedInert inert' -> inerts `updInertSet` inert'
+interactNext :: SubGoalDepth -> StageResult -> AtomicInert -> TcS StageResult
+interactNext depth it inert
+ | ContinueWith work_item <- sr_stop it
+ = do { let inerts = sr_inerts it
+
+ ; IR { ir_new_work = new_work, ir_inert_action = inert_action
+ , ir_fire = fire_info, ir_stop = stop }
+ <- interactWithInert inert work_item
+
+ ; let mk_msg rule
+ = text rule <+> keep_doc
+ <+> vcat [ ptext (sLit "Inert =") <+> ppr inert
+ , ptext (sLit "Work =") <+> ppr work_item
+ , ppUnless (isEmptyBag new_work) $
+ ptext (sLit "New =") <+> ppr new_work ]
+ keep_doc = case inert_action of
+ KeepInert -> ptext (sLit "[keep]")
+ DropInert -> ptext (sLit "[drop]")
+ ; case fire_info of
+ Just rule -> do { bumpStepCountTcS
+ ; traceFireTcS depth (mk_msg rule) }
+ Nothing -> return ()
+
+ -- New inerts depend on whether we KeepInert or not
+ ; let inerts_new = case inert_action of
+ KeepInert -> inerts `updInertSet` inert
+ DropInert -> inerts
; return $ SR { sr_inerts = inerts_new
- , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
- , sr_stop = ir_stop ir } }
+ , sr_new_work = sr_new_work it `unionWorkLists` new_work
+ , sr_stop = stop } }
| otherwise
= return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
doInteractWithInert
(CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
- workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
+ workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
| cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
= solveOneFromTheOther (d1,fl1) workItem
= -- See Note [When improvement happens]
do { let pty1 = ClassP cls1 tys1
pty2 = ClassP cls2 tys2
- work_item_pred_loc = (pty2, pprFlavorArising fl2)
inert_pred_loc = (pty1, pprFlavorArising fl1)
- loc = combineCtLoc fl1 fl2
- eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
- -- See Note [Efficient Orientation]
-
- ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs
- ; fd_work <- mapM mkCanonicalFEV derived_evs
- -- See Note [Generating extra equalities]
-
- ; mkIRContinue workItem KeepInert (unionManyBags fd_work)
- }
+ work_item_pred_loc = (pty2, pprFlavorArising fl2)
+ fd_eqns = improveFromAnother
+ inert_pred_loc -- the template
+ work_item_pred_loc -- the one we aim to rewrite
+ -- See Note [Efficient Orientation]
+
+ ; m <- rewriteWithFunDeps fd_eqns tys2 fl2
+ ; case m of
+ Nothing -> noInteraction workItem
+ Just (rewritten_tys2, cos2, fd_work)
+
+ | tcEqTypes tys1 rewritten_tys2
+ -> -- Solve him on the spot in this case
+ do { let dict_co = mkTyConCoercion (classTyCon cls1) cos2
+ ; when (isWanted fl2) $ setDictBind d2 (EvCast d1 dict_co)
+ ; mkIRStop "Cls/Cls fundep (solved)" fd_work }
+
+ | isWanted fl2
+ -> -- We could not quite solve him, but we stil rewrite him
+ -- Example: class C a b c | a -> b
+ -- Given: C Int Bool x, Wanted: C Int beta y
+ -- Then rewrite the wanted to C Int Bool y
+ -- but note that is still not identical to the given
+ -- The important thing is that the rewritten constraint is
+ -- inert wrt the given.
+ -- In fact, it is inert wrt all the previous inerts too, so
+ -- we can keep on going rather than sending it back to the work list
+ do { let dict_co = mkTyConCoercion (classTyCon cls1) cos2
+ ; d2' <- newDictVar cls1 rewritten_tys2
+ ; setDictBind d2 (EvCast d2' dict_co)
+ ; let workItem' = workItem { cc_id = d2', cc_tyargs = rewritten_tys2 }
+ ; mkIRContinue "Cls/Cls fundep (partial)" workItem' KeepInert fd_work }
+
+ | otherwise
+ -> ASSERT (isDerived fl2) -- Derived constraints have no evidence,
+ -- so just produce the rewritten constraint
+ let workItem' = workItem { cc_tyargs = rewritten_tys2 }
+ in mkIRContinue "Cls/Cls fundep" workItem' KeepInert fd_work
+ }
-- Class constraint and given equality: use the equality to rewrite
-- the class constraint.
= do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
-- Continue with rewritten Dictionary because we can only be in the
-- interactWithEqsStage, so the dictionary is inert.
- ; mkIRContinue rewritten_dict KeepInert emptyWorkList }
+ ; mkIRContinue "Eq/Cls" rewritten_dict KeepInert emptyWorkList }
doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
| wfl `canRewrite` ifl
, tv `elemVarSet` tyVarsOfTypes xis
= do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
- ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) }
+ ; mkIRContinue "Cls/Eq" workItem DropInert (workListFromCCan rewritten_dict) }
-- Class constraint and given equality: use the equality to rewrite
-- the class constraint.
| ifl `canRewrite` wfl
, tv `elemVarSet` tyVarsOfType ty
= do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
- ; mkIRContinue rewritten_ip KeepInert emptyWorkList }
+ ; mkIRContinue "Eq/IP" rewritten_ip KeepInert emptyWorkList }
doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
| wfl `canRewrite` ifl
, tv `elemVarSet` tyVarsOfType ty
= do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
- ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) }
+ ; mkIRContinue "IP/Eq" workItem DropInert (workListFromCCan rewritten_ip) }
-- Two implicit parameter constraints. If the names are the same,
-- but their types are not, we generate a wanted type equality
= -- See Note [Overriding implicit parameters]
-- Dump the inert item, override totally with the new one
-- Do not require type equality
- mkIRContinue workItem DropInert emptyWorkList
+ -- For example, given let ?x::Int = 3 in let ?x::Bool = True in ...
+ -- we must *override* the outer one with the inner one
+ mkIRContinue "IP/IP override" workItem DropInert emptyWorkList
| nm1 == nm2 && ty1 `tcEqType` ty2
= solveOneFromTheOther (id1,ifl) workItem
do { co_var <- newWantedCoVar ty2 ty1 -- See Note [Efficient Orientation]
; let flav = Wanted (combineCtLoc ifl wfl)
; cans <- mkCanonical flav co_var
- ; mkIRContinue workItem KeepInert cans }
-
-
+ ; mkIRContinue "IP/IP fundep" workItem KeepInert cans }
-- Never rewrite a given with a wanted equality, and a type function
-- equality can never rewrite an equality. We rewrite LHS *and* RHS
| ifl `canRewrite` wfl
, tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well
= do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
- ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) }
+ ; mkIRStop "Eq/FunEq" (workListFromCCan rewritten_funeq) }
-- Must Stop here, because we may no longer be inert after the rewritting.
-- Inert: function equality, work item: equality
| wfl `canRewrite` ifl
, tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well
= do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
- ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) }
+ ; mkIRContinue "FunEq/Eq" workItem DropInert (workListFromCCan rewritten_funeq) }
-- One may think that we could (KeepTransformedInert rewritten_funeq)
-- but that is wrong, because it may end up not being inert with respect
-- to future inerts. Example:
, cc_tyargs = args2, cc_rhs = xi2 })
| fl1 `canSolve` fl2 && lhss_match
= do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
- ; mkIRStop KeepInert cans }
+ ; mkIRStop "FunEq/FunEq" cans }
| fl2 `canSolve` fl1 && lhss_match
= do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
- ; mkIRContinue workItem DropInert cans }
+ ; mkIRContinue "FunEq/FunEq" workItem DropInert cans }
where
lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
-- Check for matching LHS
| fl1 `canSolve` fl2 && tv1 == tv2
= do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
- ; mkIRStop KeepInert cans }
+ ; mkIRStop "Eq/Eq lhs" cans }
| fl2 `canSolve` fl1 && tv1 == tv2
= do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
- ; mkIRContinue workItem DropInert cans }
+ ; mkIRContinue "Eq/Eq lhs" workItem DropInert cans }
+
-- Check for rewriting RHS
| fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
= do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
- ; mkIRStop KeepInert rewritten_eq }
+ ; mkIRStop "Eq/Eq rhs" rewritten_eq }
+
| fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
= do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
- ; mkIRContinue workItem DropInert rewritten_eq }
+ ; mkIRContinue "Eq/Eq rhs" workItem DropInert rewritten_eq }
doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
(CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
| fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
= do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
- ; mkIRStop KeepInert rewritten_frozen }
+ ; mkIRStop "Frozen/Eq" rewritten_frozen }
doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
workItem@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
| fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
= do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
- ; mkIRContinue workItem DropInert rewritten_frozen }
+ ; mkIRContinue "Frozen/Eq" workItem DropInert rewritten_frozen }
-- Fall-through case for all other situations
doInteractWithInert _ workItem = noInteraction workItem
co2b' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2b -- ty2b ~ ty2b[xi1/tv1]
solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
--- First argument inert, second argument workitem. They both represent
+-- First argument inert, second argument work-item. They both represent
-- wanted/given/derived evidence for the *same* predicate so we try here to
-- discharge one directly from the other.
--
-- Precondition: value evidence only (implicit parameters, classes)
-- not coercion
solveOneFromTheOther (iid,ifl) workItem
+ | isDerived wfl
+ = mkIRStop "Solved (derived)" emptyWorkList
+
| ifl `canSolve` wfl
= do { when (isWanted wfl) $ setEvBind wid (EvId iid)
-- Overwrite the binding, if one exists
-- For Givens, which are lambda-bound, nothing to overwrite,
- ; dischargeWorkItem }
+ ; mkIRStop "Solved" emptyWorkList }
+
| wfl `canSolve` ifl
= do { when (isWanted ifl) $ setEvBind iid (EvId wid)
- ; mkIRContinue workItem DropInert emptyWorkList }
+ ; mkIRContinue "Solved inert" workItem DropInert emptyWorkList }
- | otherwise -- One of the two is Derived, we can just throw it away,
- -- preferrably the work item.
- = if isDerived wfl then dischargeWorkItem
- else mkIRContinue workItem DropInert emptyWorkList
+ | otherwise -- The inert item is Derived, we can just throw it away,
+ = mkIRContinue "Discard derived inert" workItem DropInert emptyWorkList
where
wfl = cc_flavor workItem
-- arising from top-level instances.
topReactionsStage :: SimplifierStage
-topReactionsStage workItem inerts
+topReactionsStage depth workItem inerts
= do { tir <- tryTopReact workItem
; case tir of
NoTopInt ->
, sr_new_work = emptyWorkList
, sr_stop = ContinueWith workItem }
SomeTopInt tir_new_work tir_new_inert ->
- return $ SR { sr_inerts = inerts
- , sr_new_work = tir_new_work
- , sr_stop = tir_new_inert
- }
+ do { bumpStepCountTcS
+ ; traceFireTcS depth (ptext (sLit "Top react")
+ <+> vcat [ ptext (sLit "Work =") <+> ppr workItem
+ , ptext (sLit "New =") <+> ppr tir_new_work ])
+ ; return $ SR { sr_inerts = inerts
+ , sr_new_work = tir_new_work
+ , sr_stop = tir_new_inert
+ } }
}
tryTopReact :: WorkItem -> TcS TopInteractResult
= return NoTopInt -- NB: Superclasses already added since it's canonical
-- Derived dictionary: just look for functional dependencies
-doTopReact workItem@(CDictCan { cc_flavor = Derived loc
+doTopReact workItem@(CDictCan { cc_flavor = fl@(Derived loc)
, cc_class = cls, cc_tyargs = xis })
- = do { fd_work <- findClassFunDeps cls xis loc
- ; if isEmptyWorkList fd_work then
- return NoTopInt
- else return $ SomeTopInt { tir_new_work = fd_work
- , tir_new_inert = ContinueWith workItem } }
+ = do { instEnvs <- getInstEnvs
+ ; let fd_eqns = improveFromInstEnv instEnvs
+ (ClassP cls xis, pprArisingAt loc)
+ ; m <- rewriteWithFunDeps fd_eqns xis fl
+ ; case m of
+ Nothing -> return NoTopInt
+ Just (xis',_,fd_work) ->
+ let workItem' = workItem { cc_tyargs = xis' }
+ -- Deriveds are not supposed to have identity (cc_id is unused!)
+ in return $ SomeTopInt { tir_new_work = fd_work
+ , tir_new_inert = ContinueWith workItem' } }
+
-- Wanted dictionary
-doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
- , cc_class = cls, cc_tyargs = xis })
+doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc)
+ , cc_class = cls, cc_tyargs = xis })
= do { -- See Note [MATCHING-SYNONYMS]
; lkp_inst_res <- matchClassInst cls xis loc
- ; case lkp_inst_res of
- NoInstance ->
- do { traceTcS "doTopReact/ no class instance for" (ppr dv)
- ; fd_work <- findClassFunDeps cls xis loc
- ; return $ SomeTopInt
- { tir_new_work = fd_work
- , tir_new_inert = ContinueWith workItem } }
-
- GenInst wtvs ev_term -> -- Solved
+ ; case lkp_inst_res of
+ NoInstance ->
+ do { traceTcS "doTopReact/ no class instance for" (ppr dv)
+
+ ; instEnvs <- getInstEnvs
+ ; let fd_eqns = improveFromInstEnv instEnvs
+ (ClassP cls xis, pprArisingAt loc)
+ ; m <- rewriteWithFunDeps fd_eqns xis fl
+ ; case m of
+ Nothing -> return NoTopInt
+ Just (xis',cos,fd_work) ->
+ do { let dict_co = mkTyConCoercion (classTyCon cls) cos
+ ; dv'<- newDictVar cls xis'
+ ; setDictBind dv (EvCast dv' dict_co)
+ ; let workItem' = CDictCan { cc_id = dv', cc_flavor = fl,
+ cc_class = cls, cc_tyargs = xis' }
+ ; return $
+ SomeTopInt { tir_new_work = singleCCan workItem' `andCCan` fd_work
+ , tir_new_inert = Stop } } }
+
+ GenInst wtvs ev_term -- Solved
-- No need to do fundeps stuff here; the instance
-- matches already so we won't get any more info
-- from functional dependencies
- do { traceTcS "doTopReact/ found class instance for" (ppr dv)
- ; setDictBind dv ev_term
- ; inst_work <- canWanteds wtvs
- ; if null wtvs
+ | null wtvs
+ -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv)
+ ; setDictBind dv ev_term
-- Solved in one step and no new wanted work produced.
-- i.e we directly matched a top-level instance
-- No point in caching this in 'inert'; hence Stop
- then return $ SomeTopInt { tir_new_work = emptyWorkList
- , tir_new_inert = Stop }
-
- -- Solved and new wanted work produced, you may cache the
- -- (tentatively solved) dictionary as Given! (used to be: Derived)
- else do { let solved = makeSolvedByInst workItem
- ; return $ SomeTopInt
- { tir_new_work = inst_work
- , tir_new_inert = ContinueWith solved } }
- } }
+ ; return $ SomeTopInt { tir_new_work = emptyWorkList
+ , tir_new_inert = Stop } }
+
+ | otherwise
+ -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv)
+ ; setDictBind dv ev_term
+ -- Solved and new wanted work produced, you may cache the
+ -- (tentatively solved) dictionary as Given! (used to be: Derived)
+ ; let solved = workItem { cc_flavor = given_fl }
+ given_fl = Given (setCtLocOrigin loc UnkSkol)
+ ; inst_work <- canWanteds wtvs
+ ; return $ SomeTopInt { tir_new_work = inst_work
+ , tir_new_inert = ContinueWith solved } }
+ }
-- Type functions
doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
-- Any other work item does not react with any top-level equations
doTopReact _workItem = return NoTopInt
-
-----------------------
-findClassFunDeps :: Class -> [Xi] -> WantedLoc -> TcS WorkList
--- Look for a fundep reaction beween the wanted item
--- and a top-level instance declaration
-findClassFunDeps cls xis loc
- = do { instEnvs <- getInstEnvs
- ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
- (ClassP cls xis, pprArisingAt loc)
- ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs
- -- NB: fundeps generate some wanted equalities, but
- -- we don't use their evidence for anything
- ; cts <- mapM mkCanonicalFEV derived_evs
- ; return $ unionManyBags cts }
\end{code}
-- superclasses.
instance Outputable CtFlavor where
- ppr (Given _) = ptext (sLit "[Given]")
- ppr (Wanted _) = ptext (sLit "[Wanted]")
- ppr (Derived {}) = ptext (sLit "[Derived]")
-
+ ppr (Given {}) = ptext (sLit "[G]")
+ ppr (Wanted {}) = ptext (sLit "[W]")
+ ppr (Derived {}) = ptext (sLit "[D]")
pprFlavorArising :: CtFlavor -> SDoc
pprFlavorArising (Derived wl ) = pprArisingAt wl
pprFlavorArising (Wanted wl) = pprArisingAt wl
CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts,
deCanonicalise, mkFrozenError,
- makeSolvedByInst,
isWanted, isGiven, isDerived,
isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
combineCtLoc, mkGivenFlavor, mkWantedFlavor,
getWantedLoc,
- TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality
+ TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality
+ traceFireTcS, bumpStepCountTcS,
tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
instDFunTypes, -- Instantiation
instDFunConstraints,
- newFlexiTcSTy,
+ newFlexiTcSTy, instFlexiTcS,
compatKind,
matchClass, matchFam, MatchInstResult (..),
checkWellStagedDFun,
warnTcS,
- pprEq, -- Smaller utils, re-exported from TcM
+ pprEq -- Smaller utils, re-exported from TcM
-- TODO (DV): these are only really used in the
-- instance matcher in TcSimplify. I am wondering
-- if the whole instance matcher simply belongs
-- here
-
-
- mkDerivedFunDepEqns -- Instantiation of 'Equations' from FunDeps
-
) where
#include "HsVersions.h"
import HsBinds -- for TcEvBinds stuff
import Id
-import FunDeps
import TcRnTypes
compatKind :: Kind -> Kind -> Bool
compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
-makeSolvedByInst :: CanonicalCt -> CanonicalCt
--- Record that a constraint is now solved
--- Wanted -> Given
--- Given, Derived -> no-op
-makeSolvedByInst ct
- | Wanted loc <- cc_flavor ct
- = ct { cc_flavor = Given (setCtLocOrigin loc UnkSkol) }
- | otherwise -- Only called on wanteds
- = pprPanic "makeSolvedByInst" (ppr ct)
-
deCanonicalise :: CanonicalCt -> FlavoredEvVar
deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
tcs_context :: SimplContext,
- tcs_untch :: TcsUntouchables
+ tcs_untch :: TcsUntouchables,
+
+ tcs_ic_depth :: Int, -- Implication nesting depth
+ tcs_count :: IORef Int -- Global step count
}
type TcsUntouchables = (Untouchables,TcTyVarSet)
traceTcS :: String -> SDoc -> TcS ()
traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
-traceTcS0 :: String -> SDoc -> TcS ()
-traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
+bumpStepCountTcS :: TcS ()
+bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
+ ; n <- TcM.readTcRef ref
+ ; TcM.writeTcRef ref (n+1) }
+
+traceFireTcS :: Int -> SDoc -> TcS ()
+-- Dump a rule-firing trace
+traceFireTcS depth doc
+ = TcS $ \env ->
+ TcM.ifDOptM Opt_D_dump_cs_trace $
+ do { n <- TcM.readTcRef (tcs_count env)
+ ; let msg = int n
+ <> text (replicate (tcs_ic_depth env) '>')
+ <> brackets (int depth) <+> doc
+ ; TcM.dumpTcRn msg }
runTcS :: SimplContext
-> Untouchables -- Untouchables
runTcS context untouch tcs
= do { ty_binds_var <- TcM.newTcRef emptyVarEnv
; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
+ ; step_count <- TcM.newTcRef 0
; let env = TcSEnv { tcs_ev_binds = ev_binds_var
, tcs_ty_binds = ty_binds_var
, tcs_context = context
, tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
+ , tcs_count = step_count
+ , tcs_ic_depth = 0
}
-- Run the computation
; ty_binds <- TcM.readTcRef ty_binds_var
; mapM_ do_unification (varEnvElts ty_binds)
+#ifdef DEBUG
+ ; count <- TcM.readTcRef step_count
+ ; TcM.dumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count)
+#endif
-- And return
; ev_binds <- TcM.readTcRef evb_ref
; return (res, evBindMapBinds ev_binds) }
do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
-nestImplicTcS ref untch (TcS thing_inside)
- = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds,
- tcs_context = ctxt } ->
+nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
+ = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
+ , tcs_untch = (_outer_range, outer_tcs)
+ , tcs_count = count
+ , tcs_ic_depth = idepth
+ , tcs_context = ctxt } ->
let
+ inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
+ -- The inner_range should be narrower than the outer one
+ -- (thus increasing the set of untouchables) but
+ -- the inner Tcs-untouchables must be unioned with the
+ -- outer ones!
nest_env = TcSEnv { tcs_ev_binds = ref
, tcs_ty_binds = ty_binds
- , tcs_untch = untch
+ , tcs_untch = inner_untch
+ , tcs_count = count
+ , tcs_ic_depth = idepth+1
, tcs_context = ctxtUnderImplic ctxt }
in
thing_inside nest_env
-- DV: We never return MatchInstMany, since tcLookupFamInst never returns
-- multiple matches. Check.
}
-
-
--- Functional dependencies, instantiation of equations
--------------------------------------------------------
-
-mkDerivedFunDepEqns :: WantedLoc
- -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
- -> TcS [FlavoredEvVar] -- All Derived
-mkDerivedFunDepEqns _ [] = return []
-mkDerivedFunDepEqns loc eqns
- = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
- ; evvars <- mapM to_work_item eqns
- ; return $ concat evvars }
- where
- to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [FlavoredEvVar]
- to_work_item ((qtvs, pairs), d1, d2)
- = do { let tvs = varSetElems qtvs
- ; tvs' <- mapM instFlexiTcS tvs
- ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
- loc' = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
- flav = Derived loc'
- ; mapM (do_one subst flav) pairs }
-
- do_one subst flav (ty1, ty2)
- = do { let sty1 = substTy subst ty1
- sty2 = substTy subst ty2
- ; ev <- newCoVar sty1 sty2
- ; return (mkEvVarX ev flav) }
-
-pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
-pprEquationDoc (eqn, (p1, _), (p2, _))
- = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
-
-mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
- -> TcM (TidyEnv, SDoc)
-mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
- = do { pred1' <- TcM.zonkTcPredType pred1
- ; pred2' <- TcM.zonkTcPredType pred2
- ; let { pred1'' = tidyPred tidy_env pred1'
- ; pred2'' = tidyPred tidy_env pred2' }
- ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
- nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
- nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
- ; return (tidy_env, msg) }
\end{code}
\begin{code}
module FunDeps (
- Equation, pprEquation,
+ FDEq (..),
+ Equation(..), pprEquation,
oclose, improveFromInstEnv, improveFromAnother,
checkInstCoverage, checkFunDeps,
pprFundeps
%************************************************************************
+Each functional dependency with one variable in the RHS is responsible
+for generating a single equality. For instance:
+ class C a b | a -> b
+The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha
+ FDEq { fd_pos = 1
+ , fd_ty_left = Bool
+ , fd_ty_right = alpha }
+However notice that a functional dependency may have more than one variable
+in the RHS which will create more than one FDEq. Example:
+ class C a b c | a -> b c
+ [Wanted] C Int alpha alpha
+ [Wanted] C Int Bool beta
+Will generate:
+ fd1 = FDEq { fd_pos = 1, fd_ty_left = alpha, fd_ty_right = Bool } and
+ fd2 = FDEq { fd_pos = 2, fd_ty_left = alpha, fd_ty_right = beta }
+
+We record the paremeter position so that can immediately rewrite a constraint
+using the produced FDEqs and remove it from our worklist.
+
+
+INVARIANT: Corresponding types aren't already equal
+That is, there exists at least one non-identity equality in FDEqs.
+
+Assume:
+ class C a b c | a -> b c
+ instance C Int x x
+And: [Wanted] C Int Bool alpha
+We will /match/ the LHS of fundep equations, producing a matching substitution
+and create equations for the RHS sides. In our last example we'd have generated:
+ ({x}, [fd1,fd2])
+where
+ fd1 = FDEq 1 Bool x
+ fd2 = FDEq 2 alpha x
+To ``execute'' the equation, make fresh type variable for each tyvar in the set,
+instantiate the two types with these fresh variables, and then unify or generate
+a new constraint. In the above example we would generate a new unification
+variable 'beta' for x and produce the following constraints:
+ [Wanted] (Bool ~ beta)
+ [Wanted] (alpha ~ beta)
+
+Notice the subtle difference between the above class declaration and:
+ class C a b c | a -> b, a -> c
+where we would generate:
+ ({x},[fd1]),({x},[fd2])
+This means that the template variable would be instantiated to different
+unification variables when producing the FD constraints.
+
+Finally, the position parameters will help us rewrite the wanted constraint ``on the spot''
+
\begin{code}
-type Equation = (TyVarSet, [(Type, Type)])
--- These pairs of types should be equal, for some
--- substitution of the tyvars in the tyvar set
--- INVARIANT: corresponding types aren't already equal
-
--- It's important that we have a *list* of pairs of types. Consider
--- class C a b c | a -> b c where ...
--- instance C Int x x where ...
--- Then, given the constraint (C Int Bool v) we should improve v to Bool,
--- via the equation ({x}, [(Bool,x), (v,x)])
--- This would not happen if the class had looked like
--- class C a b c | a -> b, a -> c
-
--- To "execute" the equation, make fresh type variable for each tyvar in the set,
--- instantiate the two types with these fresh variables, and then unify.
---
--- For example, ({a,b}, (a,Int,b), (Int,z,Bool))
--- We unify z with Int, but since a and b are quantified we do nothing to them
--- We usually act on an equation by instantiating the quantified type varaibles
--- to fresh type variables, and then calling the standard unifier.
+type Pred_Loc = (PredType, SDoc) -- SDoc says where the Pred comes from
-pprEquation :: Equation -> SDoc
-pprEquation (qtvs, pairs)
- = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
- nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (t1,t2) <- pairs])]
+data Equation
+ = FDEqn { fd_qtvs :: TyVarSet -- Instantiate these to fresh unification vars
+ , fd_eqs :: [FDEq] -- and then make these equal
+ , fd_pred1, fd_pred2 :: Pred_Loc } -- The Equation arose from
+ -- combining these two constraints
+
+data FDEq = FDEq { fd_pos :: Int -- We use '0' for the first position
+ , fd_ty_left :: Type
+ , fd_ty_right :: Type }
\end{code}
Given a bunch of predicates that must hold, such as
\begin{code}
-type Pred_Loc = (PredType, SDoc) -- SDoc says where the Pred comes from
+instFD_WithPos :: FunDep TyVar -> [TyVar] -> [Type] -> ([Type], [(Int,Type)])
+-- Returns a FunDep between the types accompanied along with their
+-- position (<=0) in the types argument list.
+instFD_WithPos (ls,rs) tvs tys
+ = (map (snd . lookup) ls, map lookup rs)
+ where
+ ind_tys = zip [0..] tys
+ env = zipVarEnv tvs ind_tys
+ lookup tv = lookupVarEnv_NF env tv
-improveFromInstEnv :: (Class -> [Instance])
- -> Pred_Loc
- -> [(Equation,Pred_Loc,Pred_Loc)]
--- Improvement from top-level instances
-improveFromInstEnv _inst_env pred
- = improveOne _inst_env pred [] -- TODO: Refactor to directly use instance_eqnd?
+zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true
+ -> [Type]
+ -> [(Int,Type)]
+ -> [FDEq]
+-- Create a list of FDEqs from two lists of types, making sure
+-- that the types are not equal.
+zipAndComputeFDEqs discard (ty1:tys1) ((i2,ty2):tys2)
+ | discard ty1 ty2 = zipAndComputeFDEqs discard tys1 tys2
+ | otherwise = FDEq { fd_pos = i2
+ , fd_ty_left = ty1
+ , fd_ty_right = ty2 } : zipAndComputeFDEqs discard tys1 tys2
+zipAndComputeFDEqs _ _ _ = []
+
+-- Improve a class constraint from another class constraint
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+improveFromAnother :: Pred_Loc -- Template item (usually given, or inert)
+ -> Pred_Loc -- Workitem [that can be improved]
+ -> [Equation]
+-- Post: FDEqs always oriented from the other to the workitem
+-- Equations have empty quantified variables
+improveFromAnother pred1@(ClassP cls1 tys1, _) pred2@(ClassP cls2 tys2, _)
+ | tys1 `lengthAtLeast` 2 && cls1 == cls2
+ = [ FDEqn { fd_qtvs = emptyVarSet, fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2 }
+ | let (cls_tvs, cls_fds) = classTvsFds cls1
+ , fd <- cls_fds
+ , let (ltys1, rs1) = instFD fd cls_tvs tys1
+ (ltys2, irs2) = instFD_WithPos fd cls_tvs tys2
+ , tcEqTypes ltys1 ltys2 -- The LHSs match
+ , let eqs = zipAndComputeFDEqs tcEqType rs1 irs2
+ , not (null eqs) ]
+
+improveFromAnother _ _ = []
+
+
+-- Improve a class constraint from instance declarations
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+pprEquation :: Equation -> SDoc
+pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs })
+ = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
+ nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (FDEq _ t1 t2) <- pairs])]
-improveFromAnother :: Pred_Loc
+improveFromInstEnv :: (InstEnv,InstEnv)
-> Pred_Loc
- -> [(Equation, Pred_Loc, Pred_Loc)]
--- Improvement from another local (given or wanted) constraint
-improveFromAnother pred1 pred2
- = improveOne (\_ -> []) pred1 [pred2] -- TODO: Refactor to directly use pairwise_eqns?
-
-
-improveOne :: (Class -> [Instance]) -- Gives instances for given class
- -> Pred_Loc -- Do improvement triggered by this
- -> [Pred_Loc] -- Current constraints
- -> [(Equation,Pred_Loc,Pred_Loc)] -- Derived equalities that must also hold
- -- (NB the above INVARIANT for type Equation)
- -- The Pred_Locs explain which two predicates were
- -- combined (for error messages)
--- Just do improvement triggered by a single, distinguised predicate
-
-improveOne _inst_env pred@(IParam ip ty, _) preds
- = [ ((emptyVarSet, [(ty,ty2)]), pred, p2)
- | p2@(IParam ip2 ty2, _) <- preds
- , ip==ip2
- , not (ty `tcEqType` ty2)]
-
-improveOne inst_env pred@(ClassP cls tys, _) preds
+ -> [Equation] -- Needs to be an Equation because
+ -- of quantified variables
+-- Post: Equations oriented from the template (matching instance) to the workitem!
+improveFromInstEnv _inst_env (pred,_loc)
+ | not (isClassPred pred)
+ = panic "improveFromInstEnv: not a class predicate"
+improveFromInstEnv inst_env pred@(ClassP cls tys, _)
| tys `lengthAtLeast` 2
- = instance_eqns ++ pairwise_eqns
- -- NB: we put the instance equations first. This biases the
- -- order so that we first improve individual constraints against the
- -- instances (which are perhaps in a library and less likely to be
- -- wrong; and THEN perform the pairwise checks.
- -- The other way round, it's possible for the pairwise check to succeed
- -- and cause a subsequent, misleading failure of one of the pair with an
- -- instance declaration. See tcfail143.hs for an example
- where
- (cls_tvs, cls_fds) = classTvsFds cls
- instances = inst_env cls
- rough_tcs = roughMatchTcs tys
-
- -- NOTE that we iterate over the fds first; they are typically
- -- empty, which aborts the rest of the loop.
- pairwise_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
- pairwise_eqns -- This group comes from pairwise comparison
- = [ (eqn, pred, p2)
- | fd <- cls_fds
- , p2@(ClassP cls2 tys2, _) <- preds
- , cls == cls2
- , eqn <- checkClsFD emptyVarSet fd cls_tvs tys tys2
- ]
-
- instance_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
- instance_eqns -- This group comes from comparing with instance decls
- = [ (eqn, p_inst, pred)
- | fd <- cls_fds -- Iterate through the fundeps first,
+ = [ FDEqn { fd_qtvs = qtvs, fd_eqs = eqs, fd_pred1 = p_inst, fd_pred2=pred }
+ | fd <- cls_fds -- Iterate through the fundeps first,
-- because there often are none!
- , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
+ , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
-- Trim the rough_tcs based on the head of the fundep.
-- Remember that instanceCantMatch treats both argumnents
-- symmetrically, so it's ok to trim the rough_tcs,
-- rather than trimming each inst_tcs in turn
- , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst,
- is_tcs = inst_tcs }) <- instances
- , not (instanceCantMatch inst_tcs trimmed_tcs)
- , eqn <- checkClsFD qtvs fd cls_tvs tys_inst tys
- , let p_inst = (mkClassPred cls tys_inst,
- sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd)
- , ptext (sLit "in the instance declaration at")
- <+> ppr (getSrcLoc ispec)])
- ]
-
-improveOne _ _ _
- = []
+ , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst,
+ is_tcs = inst_tcs }) <- instances
+ , not (instanceCantMatch inst_tcs trimmed_tcs)
+ , let p_inst = (mkClassPred cls tys_inst,
+ sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd)
+ , ptext (sLit "in the instance declaration at")
+ <+> ppr (getSrcLoc ispec)])
+ , (qtvs, eqs) <- checkClsFD qtvs fd cls_tvs tys_inst tys -- NB: orientation
+ , not (null eqs)
+ ]
+ where
+ (cls_tvs, cls_fds) = classTvsFds cls
+ instances = classInstances inst_env cls
+ rough_tcs = roughMatchTcs tys
+improveFromInstEnv _ _ = []
checkClsFD :: TyVarSet -- Quantified type variables; see note below
-> FunDep TyVar -> [TyVar] -- One functional dependency from the class
-> [Type] -> [Type]
- -> [Equation]
+ -> [(TyVarSet, [FDEq])]
checkClsFD qtvs fd clas_tvs tys1 tys2
-- 'qtvs' are the quantified type variables, the ones which an be instantiated
length tys1 == length clas_tvs
, ppr tys1 <+> ppr tys2 )
- case tcUnifyTys bind_fn ls1 ls2 of
+ case tcUnifyTys bind_fn ltys1 ltys2 of
Nothing -> []
- Just subst | isJust (tcUnifyTys bind_fn rs1' rs2')
- -- Don't include any equations that already hold.
+ Just subst | isJust (tcUnifyTys bind_fn rtys1' rtys2')
+ -- Don't include any equations that already hold.
-- Reason: then we know if any actual improvement has happened,
-- in which case we need to iterate the solver
- -- In making this check we must taking account of the fact that any
- -- qtvs that aren't already instantiated can be instantiated to anything
+ -- In making this check we must taking account of the fact that any
+ -- qtvs that aren't already instantiated can be instantiated to anything
-- at all
- -> []
-
- | otherwise -- Aha! A useful equation
- -> [ (qtvs', zip rs1' rs2')]
+ -- NB: We can't do this 'is-useful-equation' check element-wise
+ -- because of:
+ -- class C a b c | a -> b c
+ -- instance C Int x x
+ -- [Wanted] C Int alpha Int
+ -- We would get that x -> alpha (isJust) and x -> Int (isJust)
+ -- so we would produce no FDs, which is clearly wrong.
+ -> []
+
+ | otherwise
+ -> [(qtvs', fdeqs)]
-- We could avoid this substTy stuff by producing the eqn
-- (qtvs, ls1++rs1, ls2++rs2)
-- which will re-do the ls1/ls2 unification when the equation is
-- executed. What we're doing instead is recording the partial
-- work of the ls1/ls2 unification leaving a smaller unification problem
- where
- rs1' = substTys subst rs1
- rs2' = substTys subst rs2
+ where
+ rtys1' = map (substTy subst) rtys1
+ irs2' = map (\(i,x) -> (i,substTy subst x)) irs2
+ rtys2' = map snd irs2'
+
+ fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' irs2'
+ -- Don't discard anything!
+ -- We could discard equal types but it's an overkill to call
+ -- tcEqType again, since we know for sure that /at least one/
+ -- equation in there is useful)
+
qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs
- -- qtvs' are the quantified type variables
- -- that have not been substituted out
- --
- -- Eg. class C a b | a -> b
- -- instance C Int [y]
- -- Given constraint C Int z
- -- we generate the equation
- -- ({y}, [y], z)
+ -- qtvs' are the quantified type variables
+ -- that have not been substituted out
+ --
+ -- Eg. class C a b | a -> b
+ -- instance C Int [y]
+ -- Given constraint C Int z
+ -- we generate the equation
+ -- ({y}, [y], z)
where
bind_fn tv | tv `elemVarSet` qtvs = BindMe
| otherwise = Skolem
- (ls1, rs1) = instFD fd clas_tvs tys1
- (ls2, rs2) = instFD fd clas_tvs tys2
+ (ltys1, rtys1) = instFD fd clas_tvs tys1
+ (ltys2, irs2) = instFD_WithPos fd clas_tvs tys2
+\end{code}
+
+\begin{code}
instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
+-- A simpler version of instFD_WithPos to be used in checking instance coverage etc.
instFD (ls,rs) tvs tys
= (map lookup ls, map lookup rs)
where
env = zipVarEnv tvs tys
lookup tv = lookupVarEnv_NF env tv
-\end{code}
-\begin{code}
checkInstCoverage :: Class -> [Type] -> Bool
-- Check that the Coverage Condition is obeyed in an instance decl
-- For example, if we have