From dd7522c3b14bce1af94bffd61c4d38e670f53495 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Mon, 7 May 2012 17:40:34 +0100 Subject: [PATCH] Yet another major refactoring of the constraint solver This is the result of Simon and Dimitrios doing a code walk through. There is no change in behaviour, but the structure is much better. Main changes: * Given constraints contain an EvTerm not an EvVar * Correspondingly, TcEvidence is a recursive types that uses EvTerms rather than EvVars * Rename CtFlavor to CtEvidence * Every CtEvidence has a ctev_pred field. And use record fields consistently for CtEvidence * The solved-constraint fields of InertSet (namely inert_solved and inert_solved_funeqs) contain CtEvidence, not Ct There is a long cascade of follow-on changes. --- compiler/coreSyn/CoreUtils.lhs | 10 +- compiler/deSugar/DsBinds.lhs | 55 ++- compiler/typecheck/Inst.lhs | 72 ++-- compiler/typecheck/TcCanonical.lhs | 252 ++++++------ compiler/typecheck/TcErrors.lhs | 48 ++- compiler/typecheck/TcEvidence.lhs | 68 ++-- compiler/typecheck/TcHsSyn.lhs | 29 +- compiler/typecheck/TcInstDcls.lhs | 4 +- compiler/typecheck/TcInteract.lhs | 369 ++++++++--------- compiler/typecheck/TcMType.lhs | 29 +- compiler/typecheck/TcRnTypes.lhs | 173 ++++---- compiler/typecheck/TcSMonad.lhs | 620 ++++++++++++++++------------- compiler/typecheck/TcSimplify.lhs | 50 +-- compiler/typecheck/TcUnify.lhs | 4 +- compiler/types/Coercion.lhs | 14 +- compiler/types/Type.lhs | 15 +- 16 files changed, 955 insertions(+), 857 deletions(-) diff --git a/compiler/coreSyn/CoreUtils.lhs b/compiler/coreSyn/CoreUtils.lhs index 8ec132f993..7858b20d54 100644 --- a/compiler/coreSyn/CoreUtils.lhs +++ b/compiler/coreSyn/CoreUtils.lhs @@ -187,15 +187,7 @@ mkCast (Coercion e_co) co -- The guard here checks that g has a (~#) on both sides, -- otherwise decomposeCo fails. Can in principle happen -- with unsafeCoerce - = Coercion new_co - where - -- g :: (s1 ~# s2) ~# (t1 ~# t2) - -- g1 :: s1 ~# t1 - -- g2 :: s2 ~# t2 - new_co = mkSymCo g1 `mkTransCo` e_co `mkTransCo` g2 - [_reflk, g1, g2] = decomposeCo 3 co - -- Remember, (~#) :: forall k. k -> k -> * - -- so it takes *three* arguments, not two + = Coercion (mkCoCast e_co co) mkCast (Cast expr co2) co = ASSERT(let { Pair from_ty _to_ty = coercionKind co; diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs index 8fc6bd91f3..9dd95cd4ac 100644 --- a/compiler/deSugar/DsBinds.lhs +++ b/compiler/deSugar/DsBinds.lhs @@ -726,39 +726,51 @@ sccEvBinds bs = stronglyConnCompFromEdgedVertices edges edges = foldrBag ((:) . mk_node) [] bs mk_node :: EvBind -> (EvBind, EvVar, [EvVar]) - mk_node b@(EvBind var term) = (b, var, evVarsOfTerm term) + mk_node b@(EvBind var term) = (b, var, varSetElems (evVarsOfTerm term)) --------------------------------------- dsEvTerm :: MonadThings m => EvTerm -> m CoreExpr dsEvTerm (EvId v) = return (Var v) -dsEvTerm (EvCast v co) - = return $ dsTcCoercion co $ mkCast (Var v) -- 'v' is always a lifted evidence variable so it is - -- unnecessary to call varToCoreExpr v here. +dsEvTerm (EvCast tm co) + = do { tm' <- dsEvTerm tm + ; return $ dsTcCoercion co $ mkCast tm' } + -- 'v' is always a lifted evidence variable so it is + -- unnecessary to call varToCoreExpr v here. + dsEvTerm (EvKindCast v co) - = return $ dsTcCoercion co $ (\_ -> Var v) + = do { v' <- dsEvTerm v + ; return $ dsTcCoercion co $ (\_ -> v') } -dsEvTerm (EvDFunApp df tys vars) = return (Var df `mkTyApps` tys `mkVarApps` vars) +dsEvTerm (EvDFunApp df tys tms) = do { tms' <- mapM dsEvTerm tms + ; return (Var df `mkTyApps` tys `mkApps` tms') } dsEvTerm (EvCoercion co) = return $ dsTcCoercion co mkEqBox dsEvTerm (EvTupleSel v n) - = ASSERT( isTupleTyCon tc ) - return $ - Case (Var v) (mkWildValBinder (varType v)) (tys !! n) [(DataAlt dc, xs, Var v')] - where - (tc, tys) = splitTyConApp (evVarPred v) - Just [dc] = tyConDataCons_maybe tc - v' = v `setVarType` ty_want - xs = map mkWildValBinder tys_before ++ v' : map mkWildValBinder tys_after - (tys_before, ty_want:tys_after) = splitAt n tys -dsEvTerm (EvTupleMk vs) = return $ Var (dataConWorkId dc) `mkTyApps` tys `mkVarApps` vs - where dc = tupleCon ConstraintTuple (length vs) - tys = map varType vs + = do { tm' <- dsEvTerm v + ; let scrut_ty = exprType tm' + (tc, tys) = splitTyConApp scrut_ty + Just [dc] = tyConDataCons_maybe tc + xs = mkTemplateLocals tys + the_x = xs !! n + ; ASSERT( isTupleTyCon tc ) + return $ + Case tm' (mkWildValBinder scrut_ty) (idType the_x) [(DataAlt dc, xs, Var the_x)] } + +dsEvTerm (EvTupleMk tms) + = do { tms' <- mapM dsEvTerm tms + ; let tys = map exprType tms' + ; return $ Var (dataConWorkId dc) `mkTyApps` tys `mkApps` tms' } + where + dc = tupleCon ConstraintTuple (length tms) + dsEvTerm (EvSuperClass d n) - = return $ Var sc_sel_id `mkTyApps` tys `App` Var d + = do { d' <- dsEvTerm d + ; let (cls, tys) = getClassPredTys (exprType d') + sc_sel_id = classSCSelId cls n -- Zero-indexed + ; return $ Var sc_sel_id `mkTyApps` tys `App` d' } where - sc_sel_id = classSCSelId cls n -- Zero-indexed - (cls, tys) = getClassPredTys (evVarPred d) + dsEvTerm (EvDelayedError ty msg) = return $ Var errorId `mkTyApps` [ty] `mkApps` [litMsg] where errorId = rUNTIME_ERROR_ID @@ -816,6 +828,7 @@ ds_tc_coercion subst tc_co go (TcNthCo n co) = mkNthCo n (go co) go (TcInstCo co ty) = mkInstCo (go co) ty go (TcLetCo bs co) = ds_tc_coercion (ds_co_binds bs) co + go (TcCastCo co1 co2) = mkCoCast (go co1) (go co2) go (TcCoVarCo v) = ds_ev_id subst v ds_co_binds :: TcEvBinds -> CvSubst diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index d8ba828d9a..0b4364b7ee 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -83,10 +83,11 @@ emitWanteds :: CtOrigin -> TcThetaType -> TcM [EvVar] emitWanteds origin theta = mapM (emitWanted origin) theta emitWanted :: CtOrigin -> TcPredType -> TcM EvVar -emitWanted origin pred = do { loc <- getCtLoc origin - ; ev <- newWantedEvVar pred - ; emitFlat (mkNonCanonical (Wanted loc ev)) - ; return ev } +emitWanted origin pred + = do { loc <- getCtLoc origin + ; ev <- newWantedEvVar pred + ; emitFlat (mkNonCanonical (Wanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev })) + ; return ev } newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId) -- Used when Name is the wired-in name for a wired-in class method, @@ -530,7 +531,7 @@ tyVarsOfCt (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys) tyVarsOfCt (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys tyVarsOfCt (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty tyVarsOfCt (CIrredEvCan { cc_ty = ty }) = tyVarsOfType ty -tyVarsOfCt (CNonCanonical { cc_flavor = fl }) = tyVarsOfType (ctFlavPred fl) +tyVarsOfCt (CNonCanonical { cc_ev = fl }) = tyVarsOfType (ctEvPred fl) tyVarsOfCDict :: Ct -> TcTyVarSet tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys @@ -564,24 +565,22 @@ tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet ---------------- Tidying ------------------------- tidyCt :: TidyEnv -> Ct -> Ct +-- Used only in error reporting -- Also converts it to non-canonical tidyCt env ct - = CNonCanonical { cc_flavor = tidy_flavor env (cc_flavor ct) + = CNonCanonical { cc_ev = tidy_flavor env (cc_ev ct) , cc_depth = cc_depth ct } - where tidy_flavor :: TidyEnv -> CtFlavor -> CtFlavor - tidy_flavor env (Given { flav_gloc = gloc, flav_evar = evar }) - = Given { flav_gloc = tidyGivenLoc env gloc - , flav_evar = tidyEvVar env evar } - tidy_flavor env (Solved { flav_gloc = gloc - , flav_evar = evar }) - = Solved { flav_gloc = tidyGivenLoc env gloc - , flav_evar = tidyEvVar env evar } - tidy_flavor env (Wanted { flav_wloc = wloc - , flav_evar = evar }) - = Wanted { flav_wloc = wloc -- Interesting: no tidying needed? - , flav_evar = tidyEvVar env evar } - tidy_flavor env (Derived { flav_wloc = wloc, flav_der_pty = pty }) - = Derived { flav_wloc = wloc, flav_der_pty = tidyType env pty } + where + tidy_flavor :: TidyEnv -> CtEvidence -> CtEvidence + -- NB: we do not tidy the ctev_evtm/var field because we don't + -- show it in error messages + tidy_flavor env ctev@(Given { ctev_gloc = gloc, ctev_pred = pred }) + = ctev { ctev_gloc = tidyGivenLoc env gloc + , ctev_pred = tidyType env pred } + tidy_flavor env ctev@(Wanted { ctev_pred = pred }) + = ctev { ctev_pred = tidyType env pred } + tidy_flavor env ctev@(Derived { ctev_pred = pred }) + = ctev { ctev_pred = tidyType env pred } tidyEvVar :: TidyEnv -> EvVar -> EvVar tidyEvVar env var = setVarType var (tidyType env (varType var)) @@ -604,6 +603,10 @@ tidySkolemInfo env (UnifyForAllSkol skol_tvs ty) tidySkolemInfo _ info = info ---------------- Substitution ------------------------- +-- This is used only in TcSimpify, for substituations that are *also* +-- reflected in the unification variables. So we don't substitute +-- in the evidence. + substCt :: TvSubst -> Ct -> Ct -- Conservatively converts it to non-canonical: -- Postcondition: if the constraint does not get rewritten @@ -611,9 +614,9 @@ substCt subst ct | pty <- ctPred ct , sty <- substTy subst pty = if sty `eqType` pty then - ct { cc_flavor = substFlavor subst (cc_flavor ct) } + ct { cc_ev = substFlavor subst (cc_ev ct) } else - CNonCanonical { cc_flavor = substFlavor subst (cc_flavor ct) + CNonCanonical { cc_ev = substFlavor subst (cc_ev ct) , cc_depth = cc_depth ct } substWC :: TvSubst -> WantedConstraints -> WantedConstraints @@ -637,21 +640,16 @@ substImplication subst implic@(Implic { ic_skols = tvs substEvVar :: TvSubst -> EvVar -> EvVar substEvVar subst var = setVarType var (substTy subst (varType var)) -substFlavor :: TvSubst -> CtFlavor -> CtFlavor -substFlavor subst (Given { flav_gloc = gloc, flav_evar = evar }) - = Given { flav_gloc = substGivenLoc subst gloc - , flav_evar = substEvVar subst evar } -substFlavor subst (Solved { flav_gloc = gloc, flav_evar = evar }) - = Solved { flav_gloc = substGivenLoc subst gloc - , flav_evar = substEvVar subst evar } - -substFlavor subst (Wanted { flav_wloc = wloc, flav_evar = evar }) - = Wanted { flav_wloc = wloc - , flav_evar = substEvVar subst evar } - -substFlavor subst (Derived { flav_wloc = wloc, flav_der_pty = pty }) - = Derived { flav_wloc = wloc - , flav_der_pty = substTy subst pty } +substFlavor :: TvSubst -> CtEvidence -> CtEvidence +substFlavor subst ctev@(Given { ctev_gloc = gloc, ctev_pred = pred }) + = ctev { ctev_gloc = substGivenLoc subst gloc + , ctev_pred = substTy subst pred } + +substFlavor subst ctev@(Wanted { ctev_pred = pred }) + = ctev { ctev_pred = substTy subst pred } + +substFlavor subst ctev@(Derived { ctev_pred = pty }) + = ctev { ctev_pred = substTy subst pty } substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc substGivenLoc subst (CtLoc skol span ctxt) diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index d293f0ea3b..2e87c9e2f2 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -173,26 +173,26 @@ EvBinds, so we are again good. -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ canonicalize :: Ct -> TcS StopOrContinue -canonicalize ct@(CNonCanonical { cc_flavor = fl, cc_depth = d }) +canonicalize ct@(CNonCanonical { cc_ev = fl, cc_depth = d }) = do { traceTcS "canonicalize (non-canonical)" (ppr ct) ; {-# SCC "canEvVar" #-} canEvVar d fl (classifyPredType (ctPred ct)) } canonicalize (CDictCan { cc_depth = d - , cc_flavor = fl + , cc_ev = fl , cc_class = cls , cc_tyargs = xis }) = {-# SCC "canClass" #-} canClass d fl cls xis -- Do not add any superclasses canonicalize (CTyEqCan { cc_depth = d - , cc_flavor = fl + , cc_ev = fl , cc_tyvar = tv , cc_rhs = xi }) = {-# SCC "canEqLeafTyVarLeftRec" #-} canEqLeafTyVarLeftRec d fl tv xi canonicalize (CFunEqCan { cc_depth = d - , cc_flavor = fl + , cc_ev = fl , cc_fun = fn , cc_tyargs = xis1 , cc_rhs = xi2 }) @@ -200,18 +200,18 @@ canonicalize (CFunEqCan { cc_depth = d canEqLeafFunEqLeftRec d fl (fn,xis1) xi2 canonicalize (CIPCan { cc_depth = d - , cc_flavor = fl + , cc_ev = fl , cc_ip_nm = nm , cc_ip_ty = xi }) = canIP d fl nm xi -canonicalize (CIrredEvCan { cc_flavor = fl +canonicalize (CIrredEvCan { cc_ev = fl , cc_depth = d , cc_ty = xi }) = canIrred d fl xi canEvVar :: SubGoalDepth - -> CtFlavor + -> CtEvidence -> PredTree -> TcS StopOrContinue -- Called only for non-canonical EvVars @@ -233,15 +233,16 @@ canEvVar d fl pred_classifier \begin{code} canTuple :: SubGoalDepth -- Depth - -> CtFlavor -> [PredType] -> TcS StopOrContinue + -> CtEvidence -> [PredType] -> TcS StopOrContinue canTuple d fl tys = do { traceTcS "can_pred" (text "TuplePred!") ; let xcomp = EvTupleMk xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..] - ; xCtFlavor fl tys (XEvTerm xcomp xdecomp) what_next } - where what_next fls = mapM_ add_to_work fls >> return Stop - add_to_work fl = addToWork $ canEvVar d fl (classifyPredType (ctFlavPred fl)) - + ; ctevs <- xCtFlavor fl tys (XEvTerm xcomp xdecomp) + ; mapM_ add_to_work ctevs + ; return Stop } + where + add_to_work fl = addToWork $ canEvVar d fl (classifyPredType (ctEvPred fl)) \end{code} @@ -253,7 +254,7 @@ canTuple d fl tys \begin{code} canIP :: SubGoalDepth -- Depth - -> CtFlavor + -> CtEvidence -> IPName Name -> Type -> TcS StopOrContinue -- Precondition: EvVar is implicit parameter evidence canIP d fl nm ty @@ -264,7 +265,7 @@ canIP d fl nm ty ; mb <- rewriteCtFlavor fl xi co ; case mb of Just new_fl -> let IPPred _ xi_in = classifyPredType xi - in continueWith $ CIPCan { cc_flavor = new_fl + in continueWith $ CIPCan { cc_ev = new_fl , cc_ip_nm = nm, cc_ip_ty = xi_in , cc_depth = d } Nothing -> return Stop } @@ -291,7 +292,7 @@ flattened in the first place to facilitate comparing them.) \begin{code} canClass, canClassNC :: SubGoalDepth -- Depth - -> CtFlavor + -> CtEvidence -> Class -> [Type] -> TcS StopOrContinue -- Precondition: EvVar is class evidence @@ -314,14 +315,14 @@ canClass d fl cls tys ; case mb of Just new_fl -> - let (ClassPred cls xis_for_dict) = classifyPredType (ctFlavPred new_fl) + let (ClassPred cls xis_for_dict) = classifyPredType (ctEvPred new_fl) in continueWith $ - CDictCan { cc_flavor = new_fl + CDictCan { cc_ev = new_fl , cc_tyargs = xis_for_dict, cc_class = cls, cc_depth = d } Nothing -> return Stop } emitSuperclasses :: Ct -> TcS StopOrContinue -emitSuperclasses ct@(CDictCan { cc_depth = d, cc_flavor = fl +emitSuperclasses ct@(CDictCan { cc_depth = d, cc_ev = fl , cc_tyargs = xis_new, cc_class = cls }) -- Add superclasses of this one here, See Note [Adding superclasses]. -- But only if we are not simplifying the LHS of a rule. @@ -399,20 +400,19 @@ happen. \begin{code} newSCWorkFromFlavored :: SubGoalDepth -- Depth - -> CtFlavor -> Class -> [Xi] -> TcS () + -> CtEvidence -> Class -> [Xi] -> TcS () -- Returns superclasses, see Note [Adding superclasses] newSCWorkFromFlavored d flavor cls xis | isDerived flavor = return () -- Deriveds don't yield more superclasses because we will -- add them transitively in the case of wanteds. - | isSolved flavor - = return () | isGiven flavor = do { let sc_theta = immSuperClasses cls xis xev = XEvTerm { ev_comp = panic "Can't compose for given!" - , ev_decomp = \x->zipWith (\_ i->EvSuperClass x i) sc_theta [0..] } - ; xCtFlavor flavor sc_theta xev (emit_sc_flavs d) } + , ev_decomp = \x -> zipWith (\_ i -> EvSuperClass x i) sc_theta [0..] } + ; ctevs <- xCtFlavor flavor sc_theta xev + ; emit_sc_flavs d ctevs } | isEmptyVarSet (tyVarsOfTypes xis) = return () -- Wanteds/Derived with no variables yield no deriveds. @@ -422,15 +422,17 @@ newSCWorkFromFlavored d flavor cls xis = do { let sc_rec_theta = transSuperClasses cls xis impr_theta = filter is_improvement_pty sc_rec_theta xev = panic "Derived's are not supposed to transform evidence!" - ; xCtFlavor (Derived (flav_wloc flavor) (ctFlavPred flavor)) impr_theta xev $ - emit_sc_flavs d } + der_ev = Derived { ctev_wloc = ctev_wloc flavor, ctev_pred = ctev_pred flavor } + ; ctevs <- xCtFlavor der_ev impr_theta xev + ; emit_sc_flavs d ctevs } -emit_sc_flavs :: SubGoalDepth -> [CtFlavor] -> TcS () +emit_sc_flavs :: SubGoalDepth -> [CtEvidence] -> TcS () emit_sc_flavs d fls = do { traceTcS "newSCWorkFromFlavored" $ text "Emitting superclass work:" <+> ppr sc_cts ; updWorkListTcS $ appendWorkListCt sc_cts } - where sc_cts = map (\fl -> CNonCanonical { cc_flavor = fl, cc_depth = d }) fls + where + sc_cts = map (\fl -> CNonCanonical { cc_ev = fl, cc_depth = d }) fls is_improvement_pty :: PredType -> Bool -- Either it's an equality, or has some functional dependency @@ -454,7 +456,7 @@ is_improvement_pty ty = go (classifyPredType ty) \begin{code} canIrred :: SubGoalDepth -- Depth - -> CtFlavor -> TcType -> TcS StopOrContinue + -> CtEvidence -> TcType -> TcS StopOrContinue -- Precondition: ty not a tuple and no other evidence form canIrred d fl ty = do { traceTcS "can_pred" (text "IrredPred = " <+> ppr ty) @@ -468,9 +470,9 @@ canIrred d fl ty Just new_fl | no_flattening -> continueWith $ - CIrredEvCan { cc_flavor = new_fl, cc_ty = xi, cc_depth = d } + CIrredEvCan { cc_ev = new_fl, cc_ty = xi, cc_depth = d } | otherwise - -> canEvVar d new_fl (classifyPredType (ctFlavPred new_fl)) + -> canEvVar d new_fl (classifyPredType (ctEvPred new_fl)) Nothing -> return Stop } \end{code} @@ -529,7 +531,7 @@ data FlattenMode = FMSubstOnly -- Flatten a bunch of types all at once. flattenMany :: SubGoalDepth -- Depth -> FlattenMode - -> CtFlavor -> [Type] -> TcS ([Xi], [TcCoercion]) + -> CtEvidence -> [Type] -> TcS ([Xi], [TcCoercion]) -- Coercions :: Xi ~ Type -- Returns True iff (no flattening happened) -- NB: The EvVar inside the flavor is unused, we merely want Given/Solved/Derived/Wanted info @@ -546,7 +548,7 @@ flattenMany d f ctxt tys -- constraints. See Note [Flattening] for more detail. flatten :: SubGoalDepth -- Depth -> FlattenMode - -> CtFlavor -> TcType -> TcS (Xi, TcCoercion) + -> CtEvidence -> TcType -> TcS (Xi, TcCoercion) -- Postcondition: Coercion :: Xi ~ TcType flatten d f ctxt ty | Just ty' <- tcView ty @@ -595,7 +597,8 @@ flatten d f fl (TyConApp tc tys) do { flat_cache <- getFlatCache ; case lookupTM fam_ty flat_cache of Just ct - | cc_flavor ct `canRewrite` fl + | let ctev = cc_ev ct + , ctev `canRewrite` fl -> -- You may think that we can just return (cc_rhs ct) but not so. -- return (mkTcCoVarCo (ctId ct), cc_rhs ct, []) -- The cached constraint resides in the cache so we have to flatten @@ -606,42 +609,42 @@ flatten d f fl (TyConApp tc tys) -- For now I say we don't keep it fully rewritten. do { traceTcS "flatten/flat-cache hit" $ ppr ct ; let rhs_xi = cc_rhs ct - ; (flat_rhs_xi,co) <- flatten (cc_depth ct) f (cc_flavor ct) rhs_xi - ; let final_co = mkTcCoVarCo (ctId ct) `mkTcTransCo` (mkTcSymCo co) + ; (flat_rhs_xi,co) <- flatten (cc_depth ct) f ctev rhs_xi + ; let final_co = evTermCoercion (ctEvTerm ctev) + `mkTcTransCo` mkTcSymCo co ; return (final_co, flat_rhs_xi,[]) } - _ | isGivenOrSolved fl -- Given or Solved: make new flatten skolem + _ | isGiven fl -- Given: make new flatten skolem -> do { traceTcS "flatten/flat-cache miss" $ empty ; rhs_xi_var <- newFlattenSkolemTy fam_ty - ; mg <- newGivenEvVar (mkTcEqPred fam_ty rhs_xi_var) - (EvCoercion (mkTcReflCo fam_ty)) - ; case mg of - Fresh eqv -> - do { let new_fl = Given (flav_gloc fl) eqv - ct = CFunEqCan { cc_flavor = new_fl - , cc_fun = tc - , cc_tyargs = xi_args - , cc_rhs = rhs_xi_var - , cc_depth = d } - -- Update the flat cache - ; updFlatCache ct - ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) } - Cached {} -> panic "flatten TyConApp, var must be fresh!" } + ; let co = mkTcReflCo fam_ty + new_fl = Given { ctev_gloc = ctev_gloc fl + , ctev_pred = mkTcEqPred fam_ty rhs_xi_var + , ctev_evtm = EvCoercion co } + ct = CFunEqCan { cc_ev = new_fl + , cc_fun = tc + , cc_tyargs = xi_args + , cc_rhs = rhs_xi_var + , cc_depth = d } + -- Update the flat cache + ; updFlatCache ct + ; return (co, rhs_xi_var, [ct]) } | otherwise -- Wanted or Derived: make new unification variable -> do { traceTcS "flatten/flat-cache miss" $ empty ; rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty) - ; mw <- newWantedEvVar (mkTcEqPred fam_ty rhs_xi_var) + ; let pred = mkTcEqPred fam_ty rhs_xi_var + wloc = ctev_wloc fl + ; mw <- newWantedEvVar wloc pred ; case mw of - Fresh eqv -> - do { let new_fl = Wanted (flav_wloc fl) eqv - ct = CFunEqCan { cc_flavor = new_fl + Fresh ctev -> + do { let ct = CFunEqCan { cc_ev = ctev , cc_fun = tc , cc_tyargs = xi_args , cc_rhs = rhs_xi_var , cc_depth = d } -- Update the flat cache: just an optimisation! ; updFlatCache ct - ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) } + ; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var, [ct]) } Cached {} -> panic "flatten TyConApp, var must be fresh!" } } -- Emit the flat constraints @@ -691,7 +694,7 @@ flatten d _f ctxt ty@(ForAllTy {}) \begin{code} flattenTyVar :: SubGoalDepth -> FlattenMode - -> CtFlavor -> TcTyVar -> TcS (Xi, TcCoercion) + -> CtEvidence -> TcTyVar -> TcS (Xi, TcCoercion) -- "Flattening" a type variable means to apply the substitution to it flattenTyVar d f ctxt tv = do { ieqs <- getInertEqs @@ -709,13 +712,15 @@ flattenTyVar d f ctxt tv Just (co,ty) -> do { (ty_final,co') <- flatten d f ctxt ty ; return (ty_final, co' `mkTcTransCo` mkTcSymCo co) } } - where tv_eq_subst subst tv - | Just ct <- lookupVarEnv subst tv - , cc_flavor ct `canRewrite` ctxt - = Just (mkTcCoVarCo (ctId ct),cc_rhs ct) - -- NB: even if ct is Derived we are not going to - -- touch the actual coercion so we are fine. - | otherwise = Nothing + where + tv_eq_subst subst tv + | Just ct <- lookupVarEnv subst tv + , let ctev = cc_ev ct + , ctev `canRewrite` ctxt + = Just (evTermCoercion (ctEvTerm ctev), cc_rhs ct) + -- NB: even if ct is Derived we are not going to + -- touch the actual coercion so we are fine. + | otherwise = Nothing \end{code} Note [Non-idempotent inert substitution] @@ -765,13 +770,13 @@ addToWork tcs_action = tcs_action >>= stop_or_emit \begin{code} canEqEvVarsCreated :: SubGoalDepth - -> [CtFlavor] -> TcS StopOrContinue + -> [CtEvidence] -> TcS StopOrContinue canEqEvVarsCreated _d [] = return Stop canEqEvVarsCreated d (quad:quads) = mapM_ (addToWork . do_quad) quads >> do_quad quad -- Add all but one to the work list -- and return the first (if any) for futher processing - where do_quad fl = let EqPred ty1 ty2 = classifyPredType $ ctFlavPred fl + where do_quad fl = let EqPred ty1 ty2 = classifyPredType $ ctEvPred fl in canEqNC d fl ty1 ty2 -- Note the "NC": these are fresh equalities so we must be -- careful to add their kind constraints @@ -779,7 +784,7 @@ canEqEvVarsCreated d (quad:quads) ------------------------- canEqNC, canEq :: SubGoalDepth - -> CtFlavor + -> CtEvidence -> Type -> Type -> TcS StopOrContinue canEqNC d fl ty1 ty2 @@ -790,7 +795,7 @@ canEq _d fl ty1 ty2 | eqType ty1 ty2 -- Dealing with equality here avoids -- later spurious occurs checks for a~a = if isWanted fl then - setEvBind (flav_evar fl) (EvCoercion (mkTcReflCo ty1)) >> return Stop + setEvBind (ctev_evar fl) (EvCoercion (mkTcReflCo ty1)) >> return Stop else return Stop @@ -823,11 +828,11 @@ canEq d fl ty1 ty2 -- Fail straight away for better error messages then canEqFailure d fl else - let xcomp xs = EvCoercion (mkTcTyConAppCo tc1 (map mkTcCoVarCo xs)) - xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (mkTcCoVarCo x)) tys1 [0..] - xev = XEvTerm xcomp xdecomp - in xCtFlavor fl (zipWith mkTcEqPred tys1 tys2) xev (canEqEvVarsCreated d) - + do { let xcomp xs = EvCoercion (mkTcTyConAppCo tc1 (map evTermCoercion xs)) + xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..] + xev = XEvTerm xcomp xdecomp + ; ctevs <- xCtFlavor fl (zipWith mkTcEqPred tys1 tys2) xev + ; canEqEvVarsCreated d ctevs } -- See Note [Equality between type applications] -- Note [Care with type applications] in TcUnify @@ -839,7 +844,7 @@ canEq d fl ty1 ty2 -- e.g. F a b ~ Maybe c canEq d fl s1@(ForAllTy {}) s2@(ForAllTy {}) | tcIsForAllTy s1, tcIsForAllTy s2 - , Wanted loc orig_ev <- fl + , Wanted { ctev_wloc = loc, ctev_evar = orig_ev } <- fl = do { let (tvs1,body1) = tcSplitForAllTys s1 (tvs2,body2) = tcSplitForAllTys s2 ; if not (equalLength tvs1 tvs2) then @@ -857,12 +862,12 @@ canEq d fl _ _ = canEqFailure d fl ------------------------ -- Type application canEqAppTy :: SubGoalDepth - -> CtFlavor + -> CtEvidence -> Type -> Type -> Type -> Type -> TcS StopOrContinue canEqAppTy d fl s1 t1 s2 t2 = ASSERT( not (isKind t1) && not (isKind t2) ) - if isGivenOrSolved fl then + if isGiven fl then do { traceTcS "canEq (app case)" $ text "Ommitting decomposition of given equality between: " <+> ppr (AppTy s1 t1) <+> text "and" <+> ppr (AppTy s2 t2) @@ -870,14 +875,14 @@ canEqAppTy d fl s1 t1 s2 t2 -- because we no longer have 'left' and 'right' ; return Stop } else - let xevcomp [x,y] = EvCoercion (mkTcAppCo (mkTcCoVarCo x) (mkTcCoVarCo y)) - xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen - xev = XEvTerm { ev_comp = xevcomp - , ev_decomp = error "canEqAppTy: can't happen" } - in xCtFlavor fl [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xev $ - canEqEvVarsCreated d - -canEqFailure :: SubGoalDepth -> CtFlavor -> TcS StopOrContinue + do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y)) + xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen + xev = XEvTerm { ev_comp = xevcomp + , ev_decomp = error "canEqAppTy: can't happen" } + ; ctevs <- xCtFlavor fl [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xev + ; canEqEvVarsCreated d ctevs } + +canEqFailure :: SubGoalDepth -> CtEvidence -> TcS StopOrContinue canEqFailure d fl = emitFrozenError fl d >> return Stop ------------------------ @@ -885,12 +890,12 @@ emitKindConstraint :: Ct -> TcS StopOrContinue emitKindConstraint ct = case ct of CTyEqCan { cc_depth = d - , cc_flavor = fl, cc_tyvar = tv + , cc_ev = fl, cc_tyvar = tv , cc_rhs = ty } -> emit_kind_constraint d fl (mkTyVarTy tv) ty CFunEqCan { cc_depth = d - , cc_flavor = fl + , cc_ev = fl , cc_fun = fn, cc_tyargs = xis1 , cc_rhs = xi2 } -> emit_kind_constraint d fl (mkTyConApp fn xis1) xi2 @@ -904,41 +909,43 @@ emitKindConstraint ct | otherwise = ASSERT( isKind k1 && isKind k2 ) do { kev <- - do { mw <- newWantedEvVar (mkEqPred k1 k2) + do { mw <- newWantedEvVar kind_co_wloc (mkEqPred k1 k2) ; case mw of - Cached x -> return x - Fresh x -> addToWork (canEq d (kind_co_fl x) k1 k2) >> return x } - ; let xcomp [x] = mkEvKindCast x (mkTcCoVarCo kev) + Cached ev_tm -> return ev_tm + Fresh ctev -> do { addToWork (canEq d ctev k1 k2) + ; return (ctEvTerm ctev) } } + + ; let xcomp [x] = mkEvKindCast x (evTermCoercion kev) xcomp _ = panic "emit_kind_constraint:can't happen" - xdecomp x = [mkEvKindCast x (mkTcCoVarCo kev)] + xdecomp x = [mkEvKindCast x (evTermCoercion kev)] xev = XEvTerm xcomp xdecomp - in xCtFlavor_cache False fl [mkTcEqPred ty1 ty2] xev what_next } + + ; ctevs <- xCtFlavor_cache False fl [mkTcEqPred ty1 ty2] xev -- Important: Do not cache original as Solved since we are supposed to -- solve /exactly/ the same constraint later! Example: -- (alpha :: kappa0) -- (T :: *) -- Equality is: (alpha ~ T), so we will emitConstraint (kappa0 ~ *) but -- we don't want to say that (alpha ~ T) is now Solved! - where - what_next [new_fl] = continueWith (ct { cc_flavor = new_fl }) - what_next _ = return Stop + ; case ctevs of + [] -> return Stop + [new_ctev] -> continueWith (ct { cc_ev = new_ctev }) + _ -> panic "emitKindConstraint" } + where k1 = typeKind ty1 k2 = typeKind ty2 ctxt = mkKindErrorCtxtTcS ty1 k1 ty2 k2 + -- Always create a Wanted kind equality even if -- you are decomposing a given constraint. -- NB: DV finds this reasonable for now. Maybe we have to revisit. - kind_co_fl x - | isGivenOrSolved fl - = let (CtLoc _sk_info src_span err_ctxt) = flav_gloc fl - orig = TypeEqOrigin (UnifyOrigin ty1 ty2) - ctloc = pushErrCtxtSameOrigin ctxt $ - CtLoc orig src_span err_ctxt - in Wanted ctloc x - | otherwise - = Wanted (pushErrCtxtSameOrigin ctxt (flav_wloc fl)) x - + kind_co_wloc = pushErrCtxtSameOrigin ctxt wanted_loc + wanted_loc = case fl of + Wanted { ctev_wloc = wloc } -> wloc + Derived { ctev_wloc = wloc } -> wloc + Given { ctev_gloc = gloc } -> setCtLocOrigin gloc orig + orig = TypeEqOrigin (UnifyOrigin ty1 ty2) \end{code} Note [Combining insoluble constraints] @@ -1106,7 +1113,7 @@ classify ty | Just ty' <- tcView ty = OtherCls ty -- See note [Canonical ordering for equality constraints]. -reOrient :: CtFlavor -> TypeClassifier -> TypeClassifier -> Bool +reOrient :: CtEvidence -> TypeClassifier -> TypeClassifier -> Bool -- (t1 `reOrient` t2) responds True -- iff we should flip to (t2~t1) -- We try to say False if possible, to minimise evidence generation @@ -1143,7 +1150,7 @@ reOrient _fl (FskCls {}) (OtherCls {}) = False ------------------ canEqLeaf :: SubGoalDepth -- Depth - -> CtFlavor + -> CtEvidence -> Type -> Type -> TcS StopOrContinue -- Canonicalizing "leaf" equality constraints which cannot be @@ -1156,13 +1163,16 @@ canEqLeaf :: SubGoalDepth -- Depth canEqLeaf d fl s1 s2 | cls1 `re_orient` cls2 = do { traceTcS "canEqLeaf (reorienting)" $ ppr fl <+> dcolon <+> pprEq s1 s2 - ; let xcomp [x] = EvCoercion (mkTcSymCo (mkTcCoVarCo x)) + ; let xcomp [x] = EvCoercion (mkTcSymCo (evTermCoercion x)) xcomp _ = panic "canEqLeaf: can't happen" - xdecomp x = [EvCoercion (mkTcSymCo (mkTcCoVarCo x))] + xdecomp x = [EvCoercion (mkTcSymCo (evTermCoercion x))] xev = XEvTerm xcomp xdecomp - what_next [fl] = canEqLeafOriented d fl s2 s1 - what_next _ = return Stop - ; xCtFlavor fl [mkTcEqPred s2 s1] xev what_next } + ; ctevs <- xCtFlavor fl [mkTcEqPred s2 s1] xev + ; case ctevs of + [] -> return Stop + [ctev] -> canEqLeafOriented d ctev s2 s1 + _ -> panic "canEqLeaf" } + | otherwise = do { traceTcS "canEqLeaf" $ ppr (mkTcEqPred s1 s2) ; canEqLeafOriented d fl s1 s2 } @@ -1172,7 +1182,7 @@ canEqLeaf d fl s1 s2 cls2 = classify s2 canEqLeafOriented :: SubGoalDepth -- Depth - -> CtFlavor + -> CtEvidence -> TcType -> TcType -> TcS StopOrContinue -- By now s1 will either be a variable or a type family application canEqLeafOriented d fl s1 s2 @@ -1184,10 +1194,10 @@ canEqLeafOriented d fl s1 s2 = canEqLeafTyVarLeftRec d fl tv s2 | otherwise = pprPanic "canEqLeafOriented" $ - text "Non-variable or non-family equality LHS" <+> ppr (ctFlavPred fl) + text "Non-variable or non-family equality LHS" <+> ppr (ctEvPred fl) canEqLeafFunEqLeftRec :: SubGoalDepth - -> CtFlavor + -> CtEvidence -> (TyCon,[TcType]) -> TcType -> TcS StopOrContinue canEqLeafFunEqLeftRec d fl (fn,tys1) ty2 -- fl :: F tys1 ~ ty2 = do { traceTcS "canEqLeafFunEqLeftRec" $ pprEq (mkTyConApp fn tys1) ty2 @@ -1210,7 +1220,7 @@ canEqLeafFunEqLeftRec d fl (fn,tys1) ty2 -- fl :: F tys1 ~ ty2 canEqLeafFunEqLeft :: SubGoalDepth -- Depth - -> CtFlavor + -> CtEvidence -> (TyCon,[Xi]) -> TcType -> TcS StopOrContinue -- Precondition: No more flattening is needed for the LHS @@ -1232,12 +1242,12 @@ canEqLeafFunEqLeft d fl (fn,xis1) s2 ; case mb of Nothing -> return Stop Just new_fl -> continueWith $ - CFunEqCan { cc_flavor = new_fl, cc_depth = d + CFunEqCan { cc_ev = new_fl, cc_depth = d , cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 } } canEqLeafTyVarLeftRec :: SubGoalDepth - -> CtFlavor + -> CtEvidence -> TcTyVar -> TcType -> TcS StopOrContinue canEqLeafTyVarLeftRec d fl tv s2 -- fl :: tv ~ s2 = do { traceTcS "canEqLeafTyVarLeftRec" $ pprEq (mkTyVarTy tv) s2 @@ -1262,7 +1272,7 @@ canEqLeafTyVarLeftRec d fl tv s2 -- fl :: tv ~ s2 Nothing -> canEq d new_fl xi1 s2 } canEqLeafTyVarLeft :: SubGoalDepth -- Depth - -> CtFlavor + -> CtEvidence -> TcTyVar -> TcType -> TcS StopOrContinue -- Precondition LHS is fully rewritten from inerts (but not RHS) canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2 @@ -1276,7 +1286,7 @@ canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2 -- Reflexivity exposed through flattening ; if tv_ty `eqType` xi2 then - when (isWanted fl) (setEvBind (flav_evar fl) (EvCoercion co2)) >> + when (isWanted fl) (setEvBind (ctev_evar fl) (EvCoercion co2)) >> return Stop else do -- Not reflexivity but maybe an occurs error @@ -1291,7 +1301,7 @@ canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2 ; case mb of Just new_fl -> if not_occ_err then continueWith $ - CTyEqCan { cc_flavor = new_fl, cc_depth = d + CTyEqCan { cc_ev = new_fl, cc_depth = d , cc_tyvar = tv, cc_rhs = xi2' } else canEqFailure d new_fl @@ -1307,7 +1317,7 @@ canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2 -- variable, then the same type is returned. -- -- Precondition: the two types are not equal (looking though synonyms) -canOccursCheck :: CtFlavor -> TcTyVar -> Xi -> TcS (Maybe Xi) +canOccursCheck :: CtEvidence -> TcTyVar -> Xi -> TcS (Maybe Xi) canOccursCheck _gw tv xi = return (expandAway tv xi) \end{code} diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs index 020d42c1ba..483de071d4 100644 --- a/compiler/typecheck/TcErrors.lhs +++ b/compiler/typecheck/TcErrors.lhs @@ -158,17 +158,15 @@ reportTidyWanteds ctxt insols flats implics deferToRuntime :: EvBindsVar -> ReportErrCtxt -> (ReportErrCtxt -> Ct -> TcM ErrMsg) -> Ct -> TcM () deferToRuntime ev_binds_var ctxt mk_err_msg ct - | fl <- cc_flavor ct - , Wanted loc _ <- fl + | Wanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev_id } <- cc_ev ct = do { err <- setCtLoc loc $ mk_err_msg ctxt ct - ; let ev_id = ctId ct -- Prec satisfied: Wanted - err_msg = pprLocErrMsg err + ; let err_msg = pprLocErrMsg err err_fs = mkFastString $ showSDoc $ err_msg $$ text "(deferred type error)" -- Create the binding - ; addTcEvBind ev_binds_var ev_id (EvDelayedError (idType ev_id) err_fs) + ; addTcEvBind ev_binds_var ev_id (EvDelayedError pred err_fs) -- And emit a warning ; reportWarning (makeIntoWarning err) } @@ -231,7 +229,7 @@ type Reporter = [Ct] -> TcM () mkReporter :: (Ct -> TcM ErrMsg) -> [Ct] -> TcM () -- Reports errors one at a time -mkReporter mk_err = mapM_ (\ct -> do { err <- setCtFlavorLoc (cc_flavor ct) $ +mkReporter mk_err = mapM_ (\ct -> do { err <- setCtFlavorLoc (cc_ev ct) $ mk_err ct; ; reportError err }) @@ -316,15 +314,15 @@ groupErrs mk_err (ct1 : rest) ; reportError err ; groupErrs mk_err others } where - flavor = cc_flavor ct1 + flavor = cc_ev ct1 cts = ct1 : friends (friends, others) = partition is_friend rest - is_friend friend = cc_flavor friend `same_group` flavor + is_friend friend = cc_ev friend `same_group` flavor - same_group :: CtFlavor -> CtFlavor -> Bool - same_group (Given l1 _) (Given l2 _) = same_loc l1 l2 - same_group (Derived l1 _) (Derived l2 _) = same_loc l1 l2 - same_group (Wanted l1 _) (Wanted l2 _) = same_loc l1 l2 + same_group :: CtEvidence -> CtEvidence -> Bool + same_group (Given {ctev_gloc = l1}) (Given {ctev_gloc = l2}) = same_loc l1 l2 + same_group (Wanted {ctev_wloc = l1}) (Wanted {ctev_wloc = l2}) = same_loc l1 l2 + same_group (Derived {ctev_wloc = l1}) (Derived {ctev_wloc = l2}) = same_loc l1 l2 same_group _ _ = False same_loc :: CtLoc o -> CtLoc o -> Bool @@ -425,7 +423,7 @@ mkEqErr _ [] = panic "mkEqErr" mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg -- Wanted constraints only! mkEqErr1 ctxt ct - = if isGivenOrSolved flav then + = if isGiven flav then let ctx2 = ctxt { cec_extra = cec_extra ctxt $$ inaccessible_msg flav } in mkEqErr_help ctx2 ct False ty1 ty2 else @@ -434,10 +432,11 @@ mkEqErr1 ctxt ct ; mk_err ctxt1 orig' } where - flav = cc_flavor ct + flav = cc_ev ct - inaccessible_msg (Given loc _) = hang (ptext (sLit "Inaccessible code in")) - 2 (ppr (ctLocOrigin loc)) + inaccessible_msg (Given { ctev_gloc = loc }) + = hang (ptext (sLit "Inaccessible code in")) + 2 (ppr (ctLocOrigin loc)) -- If a Solved then we should not report inaccessible code inaccessible_msg _ = empty @@ -571,7 +570,7 @@ misMatchOrCND :: ReportErrCtxt -> Ct -> Bool -> TcType -> TcType -> SDoc misMatchOrCND ctxt ct oriented ty1 ty2 | null givens || (isRigid ty1 && isRigid ty2) || - isGivenOrSolved (cc_flavor ct) + isGiven (cc_ev ct) -- If the equality is unconditionally insoluble -- or there is no context, don't report the context = misMatchMsg oriented ty1 ty2 @@ -1066,7 +1065,7 @@ solverDepthErrorTcS depth stack | null stack -- Shouldn't happen unless you say -fcontext-stack=0 = failWith msg | otherwise - = setCtFlavorLoc (cc_flavor top_item) $ + = setCtFlavorLoc (cc_ev top_item) $ do { zstack <- mapM zonkCt stack ; env0 <- tcInitTidyEnv ; let zstack_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet zstack @@ -1079,7 +1078,7 @@ solverDepthErrorTcS depth stack , ptext (sLit "Use -fcontext-stack=N to increase stack size to N") ] {- DV: Changing this because Derived's no longer have ids ... Kind of a corner case ... - = setCtFlavorLoc (cc_flavor top_item) $ + = setCtFlavorLoc (cc_ev top_item) $ do { ev_vars <- mapM (zonkEvVar . cc_id) stack ; env0 <- tcInitTidyEnv ; let tidy_env = tidyFreeTyVars env0 (tyVarsOfEvVars ev_vars) @@ -1092,7 +1091,7 @@ solverDepthErrorTcS depth stack -} -flattenForAllErrorTcS :: CtFlavor -> TcType -> TcM a +flattenForAllErrorTcS :: CtEvidence -> TcType -> TcM a flattenForAllErrorTcS fl ty = setCtFlavorLoc fl $ do { env0 <- tcInitTidyEnv @@ -1109,11 +1108,10 @@ flattenForAllErrorTcS fl ty %************************************************************************ \begin{code} -setCtFlavorLoc :: CtFlavor -> TcM a -> TcM a -setCtFlavorLoc (Wanted loc _) thing = setCtLoc loc thing -setCtFlavorLoc (Derived loc _) thing = setCtLoc loc thing -setCtFlavorLoc (Given loc _) thing = setCtLoc loc thing -setCtFlavorLoc (Solved loc _) thing = setCtLoc loc thing +setCtFlavorLoc :: CtEvidence -> TcM a -> TcM a +setCtFlavorLoc (Wanted { ctev_wloc = loc }) thing = setCtLoc loc thing +setCtFlavorLoc (Derived { ctev_wloc = loc }) thing = setCtLoc loc thing +setCtFlavorLoc (Given { ctev_gloc = loc }) thing = setCtLoc loc thing \end{code} %************************************************************************ diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs index 8ec0a5766b..2955676cdc 100644 --- a/compiler/typecheck/TcEvidence.lhs +++ b/compiler/typecheck/TcEvidence.lhs @@ -17,7 +17,7 @@ module TcEvidence ( EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, EvTerm(..), mkEvCast, evVarsOfTerm, mkEvKindCast, - EvLit(..), + EvLit(..), evTermCoercion, -- TcCoercion TcCoercion(..), @@ -36,7 +36,7 @@ import Var import PprCore () -- Instance OutputableBndr TyVar import TypeRep -- Knows type representation import TcType -import Type( tyConAppArgN, getEqPredTys_maybe, tyConAppTyCon_maybe ) +import Type( tyConAppArgN, getEqPredTys_maybe, tyConAppTyCon_maybe, getEqPredTys ) import TysPrim( funTyCon ) import TyCon import PrelNames @@ -102,6 +102,7 @@ data TcCoercion | TcSymCo TcCoercion | TcTransCo TcCoercion TcCoercion | TcNthCo Int TcCoercion + | TcCastCo TcCoercion TcCoercion -- co1 |> co2 | TcLetCo TcEvBinds TcCoercion deriving (Data.Data, Data.Typeable) @@ -199,6 +200,8 @@ tcCoercionKind co = go co where go (TcRefl ty) = Pair ty ty go (TcLetCo _ co) = go co + go (TcCastCo _ co) = case getEqPredTys (pSnd (go co)) of + (ty1,ty2) -> Pair ty1 ty2 go (TcTyConAppCo tc cos) = mkTyConApp tc <$> (sequenceA $ map go cos) go (TcAppCo co1 co2) = mkAppTy <$> go co1 <*> go co2 go (TcForAllCo tv co) = mkForAllTy tv <$> go co @@ -206,8 +209,8 @@ tcCoercionKind co = go co go (TcCoVarCo cv) = eqVarKind cv go (TcAxiomInstCo ax tys) = Pair (substTyWith (co_ax_tvs ax) tys (co_ax_lhs ax)) (substTyWith (co_ax_tvs ax) tys (co_ax_rhs ax)) - go (TcSymCo co) = swap $ go co - go (TcTransCo co1 co2) = Pair (pFst $ go co1) (pSnd $ go co2) + go (TcSymCo co) = swap (go co) + go (TcTransCo co1 co2) = Pair (pFst (go co1)) (pSnd (go co2)) go (TcNthCo d co) = tyConAppArgN d <$> go co -- c.f. Coercion.coercionKind @@ -219,7 +222,7 @@ eqVarKind cv | Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv) = ASSERT (tc `hasKey` eqTyConKey) Pair ty1 ty2 - | otherwise = panic "eqVarKind, non coercion variable" + | otherwise = pprPanic "eqVarKind, non coercion variable" (ppr cv <+> dcolon <+> ppr (varType cv)) coVarsOfTcCo :: TcCoercion -> VarSet -- Only works on *zonked* coercions, because of TcLetCo @@ -229,6 +232,7 @@ coVarsOfTcCo tc_co go (TcRefl _) = emptyVarSet go (TcTyConAppCo _ cos) = foldr (unionVarSet . go) emptyVarSet cos go (TcAppCo co1 co2) = go co1 `unionVarSet` go co2 + go (TcCastCo co1 co2) = go co1 `unionVarSet` go co2 go (TcForAllCo _ co) = go co go (TcInstCo co _) = go co go (TcCoVarCo v) = unitVarSet v @@ -289,6 +293,8 @@ ppr_co p (TcLetCo bs co) = maybeParen p TopPrec $ sep [ptext (sLit "let") <+> braces (ppr bs), ppr co] ppr_co p (TcAppCo co1 co2) = maybeParen p TyConPrec $ pprTcCo co1 <+> ppr_co TyConPrec co2 +ppr_co p (TcCastCo co1 co2) = maybeParen p FunPrec $ + ppr_co FunPrec co1 <+> ptext (sLit "|>") <+> ppr_co FunPrec co2 ppr_co p co@(TcForAllCo {}) = ppr_forall_co p co ppr_co p (TcInstCo co ty) = maybeParen p TyConPrec $ pprParendTcCo co <> ptext (sLit "@") <> pprType ty @@ -454,24 +460,24 @@ data EvTerm | EvCoercion TcCoercion -- (Boxed) coercion bindings - | EvCast EvVar TcCoercion -- d |> co + | EvCast EvTerm TcCoercion -- d |> co | EvDFunApp DFunId -- Dictionary instance application - [Type] [EvVar] + [Type] [EvTerm] - | EvTupleSel EvId Int -- n'th component of the tuple + | EvTupleSel EvTerm Int -- n'th component of the tuple, 0-indexed - | EvTupleMk [EvId] -- tuple built from this stuff + | EvTupleMk [EvTerm] -- tuple built from this stuff | EvDelayedError Type FastString -- Used with Opt_DeferTypeErrors -- See Note [Deferring coercion errors to runtime] -- in TcSimplify - | EvSuperClass DictId Int -- n'th superclass. Used for both equalities and + | EvSuperClass EvTerm Int -- n'th superclass. Used for both equalities and -- dictionaries, even though the former have no -- selector Id. We count up from _0_ - | EvKindCast EvVar TcCoercion -- See Note [EvKindCast] + | EvKindCast EvTerm TcCoercion -- See Note [EvKindCast] | EvLit EvLit -- Dictionary for class "SingI" for type lits. -- Note [EvLit] @@ -555,14 +561,14 @@ and another to make it into "SingI" evidence. \begin{code} -mkEvCast :: EvVar -> TcCoercion -> EvTerm +mkEvCast :: EvTerm -> TcCoercion -> EvTerm mkEvCast ev lco - | isTcReflCo lco = EvId ev + | isTcReflCo lco = ev | otherwise = EvCast ev lco -mkEvKindCast :: EvVar -> TcCoercion -> EvTerm +mkEvKindCast :: EvTerm -> TcCoercion -> EvTerm mkEvKindCast ev lco - | isTcReflCo lco = EvId ev + | isTcReflCo lco = ev | otherwise = EvKindCast ev lco emptyTcEvBinds :: TcEvBinds @@ -573,17 +579,27 @@ isEmptyTcEvBinds (EvBinds b) = isEmptyBag b isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds" -evVarsOfTerm :: EvTerm -> [EvVar] -evVarsOfTerm (EvId v) = [v] -evVarsOfTerm (EvCoercion co) = varSetElems (coVarsOfTcCo co) -evVarsOfTerm (EvDFunApp _ _ evs) = evs -evVarsOfTerm (EvTupleSel v _) = [v] -evVarsOfTerm (EvSuperClass v _) = [v] -evVarsOfTerm (EvCast v co) = v : varSetElems (coVarsOfTcCo co) -evVarsOfTerm (EvTupleMk evs) = evs -evVarsOfTerm (EvDelayedError _ _) = [] -evVarsOfTerm (EvKindCast v co) = v : varSetElems (coVarsOfTcCo co) -evVarsOfTerm (EvLit _) = [] +evTermCoercion :: EvTerm -> TcCoercion +-- Applied only to EvTerms of type (s~t) +evTermCoercion (EvId v) = mkTcCoVarCo v +evTermCoercion (EvCoercion co) = co +evTermCoercion (EvCast tm co) = TcCastCo (evTermCoercion tm) co +evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm) + +evVarsOfTerm :: EvTerm -> VarSet +evVarsOfTerm (EvId v) = unitVarSet v +evVarsOfTerm (EvCoercion co) = coVarsOfTcCo co +evVarsOfTerm (EvDFunApp _ _ evs) = evVarsOfTerms evs +evVarsOfTerm (EvTupleSel v _) = evVarsOfTerm v +evVarsOfTerm (EvSuperClass v _) = evVarsOfTerm v +evVarsOfTerm (EvCast tm co) = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co +evVarsOfTerm (EvTupleMk evs) = evVarsOfTerms evs +evVarsOfTerm (EvDelayedError _ _) = emptyVarSet +evVarsOfTerm (EvKindCast v co) = coVarsOfTcCo co `unionVarSet` evVarsOfTerm v +evVarsOfTerm (EvLit _) = emptyVarSet + +evVarsOfTerms :: [EvTerm] -> VarSet +evVarsOfTerms = foldr (unionVarSet . evVarsOfTerm) emptyVarSet \end{code} diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs index aec09e914d..9104016938 100644 --- a/compiler/typecheck/TcHsSyn.lhs +++ b/compiler/typecheck/TcHsSyn.lhs @@ -1095,21 +1095,24 @@ zonkEvTerm env (EvId v) = ASSERT2( isId v, ppr v ) return (EvId (zonkIdOcc env v)) zonkEvTerm env (EvCoercion co) = do { co' <- zonkTcLCoToLCo env co ; return (EvCoercion co') } -zonkEvTerm env (EvCast v co) = ASSERT( isId v) - do { co' <- zonkTcLCoToLCo env co - ; return (mkEvCast (zonkIdOcc env v) co') } - -zonkEvTerm env (EvKindCast v co) = ASSERT( isId v) - do { co' <- zonkTcLCoToLCo env co - ; return (mkEvKindCast (zonkIdOcc env v) co') } - -zonkEvTerm env (EvTupleSel v n) = return (EvTupleSel (zonkIdOcc env v) n) -zonkEvTerm env (EvTupleMk vs) = return (EvTupleMk (map (zonkIdOcc env) vs)) +zonkEvTerm env (EvCast tm co) = do { tm' <- zonkEvTerm env tm + ; co' <- zonkTcLCoToLCo env co + ; return (mkEvCast tm' co') } + +zonkEvTerm env (EvKindCast v co) = do { v' <- zonkEvTerm env v + ; co' <- zonkTcLCoToLCo env co + ; return (mkEvKindCast v' co') } + +zonkEvTerm env (EvTupleSel tm n) = do { tm' <- zonkEvTerm env tm + ; return (EvTupleSel tm' n) } +zonkEvTerm env (EvTupleMk tms) = do { tms' <- mapM (zonkEvTerm env) tms + ; return (EvTupleMk tms') } zonkEvTerm _ (EvLit l) = return (EvLit l) -zonkEvTerm env (EvSuperClass d n) = return (EvSuperClass (zonkIdOcc env d) n) +zonkEvTerm env (EvSuperClass d n) = do { d' <- zonkEvTerm env d + ; return (EvSuperClass d' n) } zonkEvTerm env (EvDFunApp df tys tms) = do { tys' <- zonkTcTypeToTypes env tys - ; let tms' = map (zonkEvVarOcc env) tms + ; tms' <- mapM (zonkEvTerm env) tms ; return (EvDFunApp (zonkIdOcc env df) tys' tms') } zonkEvTerm env (EvDelayedError ty msg) = do { ty' <- zonkTcTypeToType env ty @@ -1344,6 +1347,8 @@ zonkTcLCoToLCo env co go (TcAxiomInstCo ax tys) = do { tys' <- zonkTcTypeToTypes env tys; return (TcAxiomInstCo ax tys') } go (TcAppCo co1 co2) = do { co1' <- go co1; co2' <- go co2 ; return (mkTcAppCo co1' co2') } + go (TcCastCo co1 co2) = do { co1' <- go co1; co2' <- go co2 + ; return (TcCastCo co1' co2') } go (TcSymCo co) = do { co' <- go co; return (mkTcSymCo co') } go (TcNthCo n co) = do { co' <- go co; return (mkTcNthCo n co') } go (TcTransCo co1 co2) = do { co1' <- go co1; co2' <- go co2 diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs index 776689084f..bc217bb041 100644 --- a/compiler/typecheck/TcInstDcls.lhs +++ b/compiler/typecheck/TcInstDcls.lhs @@ -840,7 +840,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds }) mk_sc_ev_term sc | null inst_tv_tys , null dfun_ev_vars = EvId sc - | otherwise = EvDFunApp sc inst_tv_tys dfun_ev_vars + | otherwise = EvDFunApp sc inst_tv_tys (map EvId dfun_ev_vars) inst_tv_tys = mkTyVarTys inst_tyvars arg_wrapper = mkWpEvVarApps dfun_ev_vars <.> mkWpTyApps inst_tv_tys @@ -1141,7 +1141,7 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys ; self_dict <- newDict clas inst_tys ; let self_ev_bind = EvBind self_dict - (EvDFunApp dfun_id (mkTyVarTys tyvars) dfun_ev_vars) + (EvDFunApp dfun_id (mkTyVarTys tyvars) (map EvId dfun_ev_vars)) ; (meth_id, local_meth_sig) <- mkMethIds sig_fn clas tyvars dfun_ev_vars inst_tys sel_id diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index 884331dbcc..44d6a8d01f 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -31,7 +31,6 @@ import TyCon import Name import IParam -import TysWiredIn ( eqTyCon ) import FunDeps import TcEvidence @@ -46,7 +45,6 @@ import Maybes( orElse ) import Bag import Control.Monad ( foldM ) -import TrieMap import VarEnv import qualified Data.Traversable as Traversable @@ -106,8 +104,11 @@ solveInteractGiven :: GivenLoc -> [EvVar] -> TcS (Bag Implication) -- if this can happen in practice though. solveInteractGiven gloc evs = solveInteractCts (map mk_noncan evs) - where mk_noncan ev = CNonCanonical { cc_flavor = Given gloc ev - , cc_depth = 0 } + where + mk_noncan ev = CNonCanonical { cc_ev = Given { ctev_gloc = gloc + , ctev_evtm = EvId ev + , ctev_pred = evVarPred ev } + , cc_depth = 0 } -- The main solver loop implements Note [Basic Simplifier Plan] --------------------------------------------------------------- @@ -229,13 +230,13 @@ thePipeline = [ ("lookup-in-inerts", lookupInInertsStage) -------------------------------------------------------------------- lookupInInertsStage :: SimplifierStage lookupInInertsStage ct - | isWantedCt ct + | Wanted { ctev_evar = ev_id, ctev_pred = pred } <- cc_ev ct = do { is <- getTcSInerts - ; case lookupInInerts is (ctPred ct) of - Just ct_cached - | not (isDerivedCt ct_cached) - -> setEvBind (ctId ct) (EvId (ctId ct_cached)) >> - return Stop + ; case lookupInInerts is pred of + Just ctev + | not (isDerived ctev) + -> do { setEvBind ev_id (ctEvTerm ctev) + ; return Stop } _ -> continueWith ct } | otherwise -- I could do something like that for givens -- as well I suppose but it is not a big deal @@ -246,7 +247,6 @@ lookupInInertsStage ct ---------------------------------------------------------- canonicalizationStage :: SimplifierStage canonicalizationStage = TcCanonical.canonicalize - \end{code} ********************************************************************************* @@ -321,7 +321,7 @@ kickOutRewritableInerts ct ; new_ieqs <- {-# SCC "rewriteInertEqsFromInertEq" #-} rewriteInertEqsFromInertEq (cc_tyvar ct, - ct_coercion,cc_flavor ct) ieqs + ct_coercion,cc_ev ct) ieqs ; let upd_eqs is = is { inert_cans = new_ics } where ics = inert_cans is new_ics = ics { inert_eqs = new_ieqs } @@ -336,7 +336,7 @@ kickOutRewritableInerts ct ; traceTcS "Kick out" (ppr ct $$ ppr wl) ; updWorkListTcS (unionWorkList wl) } -rewriteInertEqsFromInertEq :: (TcTyVar, TcCoercion, CtFlavor) -- A new substitution +rewriteInertEqsFromInertEq :: (TcTyVar, TcCoercion, CtEvidence) -- A new substitution -> TyVarEnv Ct -- All the inert equalities -> TcS (TyVarEnv Ct) -- The new inert equalities rewriteInertEqsFromInertEq (subst_tv, _subst_co, subst_fl) ieqs @@ -366,7 +366,7 @@ rewriteInertEqsFromInertEq (subst_tv, _subst_co, subst_fl) ieqs | otherwise -- Just keep it there = return (Just ct) where - fl = cc_flavor ct + fl = cc_ev ct kick_out_rewritable :: Ct -> InertSet @@ -401,7 +401,7 @@ kick_out_rewritable ct is@(IS { inert_cans = -- inert_solved, inert_flat_cache and inert_solved_funeqs -- optimistically. But when we lookup we have to take the -- subsitution into account - fl = cc_flavor ct + fl = cc_ev ct tv = cc_tyvar ct (ips_out, ips_in) = partitionCCanMap rewritable ipmap @@ -412,7 +412,7 @@ kick_out_rewritable ct is@(IS { inert_cans = (irs_out, irs_in) = partitionBag rewritable irreds (fro_out, fro_in) = partitionBag rewritable frozen - rewritable ct = (fl `canRewrite` cc_flavor ct) && + rewritable ct = (fl `canRewrite` cc_ev ct) && (tv `elemVarSet` tyVarsOfCt ct) -- NB: tyVarsOfCt will return the type -- variables /and the kind variables/ that are @@ -461,9 +461,9 @@ data SPSolveResult = SPCantSolve -- touchable unification variable. -- See Note [Touchables and givens] trySpontaneousSolve :: WorkItem -> TcS SPSolveResult -trySpontaneousSolve workItem@(CTyEqCan { cc_flavor = gw +trySpontaneousSolve workItem@(CTyEqCan { cc_ev = gw , cc_tyvar = tv1, cc_rhs = xi, cc_depth = d }) - | isGivenOrSolved gw + | isGiven gw = return SPCantSolve | Just tv2 <- tcGetTyVar_maybe xi = do { tch1 <- isTouchableMetaTyVar tv1 @@ -488,7 +488,7 @@ trySpontaneousSolve _ = return SPCantSolve ---------------- trySpontaneousEqOneWay :: SubGoalDepth - -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult + -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult -- tv is a MetaTyVar, not untouchable trySpontaneousEqOneWay d gw tv xi | not (isSigTyVar tv) || isTyVarTy xi @@ -498,7 +498,7 @@ trySpontaneousEqOneWay d gw tv xi ---------------- trySpontaneousEqTwoWay :: SubGoalDepth - -> CtFlavor -> TcTyVar -> TcTyVar -> TcS SPSolveResult + -> CtEvidence -> TcTyVar -> TcTyVar -> TcS SPSolveResult -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here trySpontaneousEqTwoWay d gw tv1 tv2 @@ -585,10 +585,10 @@ unification variables as RHS of type family equations: F xis ~ alpha. ---------------- solveWithIdentity :: SubGoalDepth - -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult + -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult -- Solve with the identity coercion -- Precondition: kind(xi) is a sub-kind of kind(tv) --- Precondition: CtFlavor is Wanted or Derived +-- Precondition: CtEvidence is Wanted or Derived -- See [New Wanted Superclass Work] to see why solveWithIdentity -- must work for Derived as well as Wanted -- Returns: workItem where @@ -607,17 +607,18 @@ solveWithIdentity d wd tv xi -- cf TcUnify.uUnboundKVar ; setWantedTyBind tv xi' - ; let refl_xi = mkTcReflCo xi' + ; let refl_evtm = EvCoercion (mkTcReflCo xi') + refl_pred = mkTcEqPred tv_ty xi' ; when (isWanted wd) $ - setEvBind (flav_evar wd) (EvCoercion refl_xi) + setEvBind (ctev_evar wd) refl_evtm - ; ev_given <- newGivenEvVar (mkTcEqPred tv_ty xi') - (EvCoercion refl_xi) >>= (return . mn_thing) - ; let given_fl = Given (mkGivenLoc (flav_wloc wd) UnkSkol) ev_given + ; let given_fl = Given { ctev_gloc = mkGivenLoc (ctev_wloc wd) UnkSkol + , ctev_pred = refl_pred + , ctev_evtm = refl_evtm } ; return $ - SPSolved (CTyEqCan { cc_flavor = given_fl + SPSolved (CTyEqCan { cc_ev = given_fl , cc_tyvar = tv, cc_rhs = xi', cc_depth = d }) } \end{code} @@ -654,7 +655,7 @@ or, equivalently, then there is no reaction \begin{code} --- Interaction result of WorkItem <~> AtomicInert +-- Interaction result of WorkItem <~> Ct data InteractResult = IRWorkItemConsumed { ir_fire :: String } @@ -715,8 +716,8 @@ interactWithInertsStage wi doInteractWithInert :: Ct -> Ct -> TcS InteractResult -- Identical class constraints. doInteractWithInert - inertItem@(CDictCan { cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) - workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 }) + inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyargs = tys1 }) + workItem@(CDictCan { cc_ev = fl2, cc_class = cls2, cc_tyargs = tys2 }) | cls1 == cls2 = do { let pty1 = mkClassPred cls1 tys1 @@ -728,13 +729,13 @@ doInteractWithInert , text "workItem = " <+> ppr workItem ]) ; any_fundeps - <- if isGivenOrSolved fl1 && isGivenOrSolved fl2 then return Nothing + <- if isGiven fl1 && isGiven fl2 then return Nothing -- NB: We don't create fds for given (and even solved), have not seen a useful -- situation for these and even if we did we'd have to be very careful to only -- create Derived's and not Wanteds. else do { let fd_eqns = improveFromAnother inert_pred_loc work_item_pred_loc - ; wloc <- get_workitem_wloc fl2 + wloc = getWantedLoc fl2 ; rewriteWithFunDeps fd_eqns tys2 wloc } -- See Note [Efficient Orientation], [When improvement happens] @@ -745,23 +746,18 @@ doInteractWithInert | otherwise -> irKeepGoing "NOP" -- Actual Functional Dependencies - Just (_rewritten_tys2,_cos2,fd_work) + Just (_rewritten_tys2, fd_work) -- Standard thing: create derived fds and keep on going. Importantly we don't -- throw workitem back in the worklist because this can cause loops. See #5236. -> do { emitFDWorkAsDerived fd_work (cc_depth workItem) ; irKeepGoing "Cls/Cls (new fundeps)" } -- Just keep going without droping the inert } - where get_workitem_wloc (Wanted wl _) = return wl - get_workitem_wloc (Derived wl _) = return wl - get_workitem_wloc _ = pprPanic "Unexpected given workitem!" $ - vcat [ text "Work item =" <+> ppr workItem - , text "Inert item=" <+> ppr inertItem] - + -- Two pieces of irreducible evidence: if their types are *exactly identical* -- we can rewrite them. We can never improve using this: -- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not -- mean that (ty1 ~ ty2) -doInteractWithInert (CIrredEvCan { cc_flavor = ifl, cc_ty = ty1 }) +doInteractWithInert (CIrredEvCan { cc_ev = ifl, cc_ty = ty1 }) workItem@(CIrredEvCan { cc_ty = ty2 }) | ty1 `eqType` ty2 = solveOneFromTheOther "Irred/Irred" ifl workItem @@ -771,9 +767,9 @@ doInteractWithInert (CIrredEvCan { cc_flavor = ifl, cc_ty = ty1 }) -- that equates the type (this is "improvement"). -- However, we don't actually need the coercion evidence, -- so we just generate a fresh coercion variable that isn't used anywhere. -doInteractWithInert (CIPCan { cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) - workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 }) - | nm1 == nm2 && isGivenOrSolved wfl && isGivenOrSolved ifl +doInteractWithInert (CIPCan { cc_ev = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) + workItem@(CIPCan { cc_ev = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 }) + | nm1 == nm2 && isGiven wfl && isGiven ifl = -- See Note [Overriding implicit parameters] -- Dump the inert item, override totally with the new one -- Do not require type equality @@ -786,44 +782,43 @@ doInteractWithInert (CIPCan { cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) | nm1 == nm2 = -- See Note [When improvement happens] - do { mb_eqv <- newWantedEvVar (mkEqPred ty2 ty1) + do { mb_eqv <- newWantedEvVar new_wloc (mkEqPred ty2 ty1) -- co :: ty2 ~ ty1, see Note [Efficient orientation] ; cv <- case mb_eqv of Fresh eqv -> do { updWorkListTcS $ extendWorkListEq $ - CNonCanonical { cc_flavor = Wanted new_wloc eqv + CNonCanonical { cc_ev = eqv , cc_depth = cc_depth workItem } - ; return eqv } + ; return (ctEvTerm eqv) } Cached eqv -> return eqv ; case wfl of - Wanted {} -> - let ip_co = mkTcTyConAppCo (ipTyCon nm1) [mkTcCoVarCo cv] - in do { setEvBind (ctId workItem) $ - mkEvCast (flav_evar ifl) (mkTcSymCo ip_co) + Wanted { ctev_evar = ev_id } -> + let ip_co = mkTcTyConAppCo (ipTyCon nm1) [evTermCoercion cv] + in do { setEvBind ev_id $ + mkEvCast (ctEvTerm ifl) (mkTcSymCo ip_co) ; irWorkItemConsumed "IP/IP (solved by rewriting)" } _ -> pprPanic "Unexpected IP constraint" (ppr workItem) } - where new_wloc - | Wanted wl _ <- wfl = wl - | Derived wl _ <- wfl = wl - | Wanted wl _ <- ifl = wl - | Derived wl _ <- ifl = wl - | otherwise = panic "Solve IP: no WantedLoc!" - + where + new_wloc | isGiven wfl = getWantedLoc ifl + | otherwise = getWantedLoc wfl -doInteractWithInert ii@(CFunEqCan { cc_flavor = fl1, cc_fun = tc1 +doInteractWithInert ii@(CFunEqCan { cc_ev = fl1, cc_fun = tc1 , cc_tyargs = args1, cc_rhs = xi1, cc_depth = d1 }) - wi@(CFunEqCan { cc_flavor = fl2, cc_fun = tc2 + wi@(CFunEqCan { cc_ev = fl2, cc_fun = tc2 , cc_tyargs = args2, cc_rhs = xi2, cc_depth = d2 }) +{- ToDo: Check with Dimitrios | lhss_match , isSolved fl1 -- Inert is solved and we can simply ignore it -- when workitem is given/solved - , isGivenOrSolved fl2 + , isGiven fl2 = irInertConsumed "FunEq/FunEq" | lhss_match , isSolved fl2 -- Workitem is solved and we can ignore it when -- the inert is given/solved - , isGivenOrSolved fl1 + , isGiven fl1 = irWorkItemConsumed "FunEq/FunEq" +-} + | fl1 `canSolve` fl2 && lhss_match = do { traceTcS "interact with inerts: FunEq/FunEq" $ vcat [ text "workItem =" <+> ppr wi @@ -836,10 +831,12 @@ doInteractWithInert ii@(CFunEqCan { cc_flavor = fl1, cc_fun = tc1 -- xdecomp : (F args ~ xi2) -> [(xi2 ~ xi1)] xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` co1)] - ; xCtFlavor_cache False fl2 [mkTcEqPred xi2 xi1] xev $ what_next d2 + ; ctevs <- xCtFlavor_cache False fl2 [mkTcEqPred xi2 xi1] xev -- Why not simply xCtFlavor? See Note [Cache-caused loops] -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation] + ; add_to_work d2 ctevs ; irWorkItemConsumed "FunEq/FunEq" } + | fl2 `canSolve` fl1 && lhss_match = do { traceTcS "interact with inerts: FunEq/FunEq" $ vcat [ text "workItem =" <+> ppr wi @@ -847,25 +844,26 @@ doInteractWithInert ii@(CFunEqCan { cc_flavor = fl1, cc_fun = tc1 ; let xev = XEvTerm xcomp xdecomp -- xcomp : [(xi2 ~ xi1)] -> [(F args ~ xi1)] - xcomp [x] = EvCoercion (co2 `mkTcTransCo` mkTcCoVarCo x) + xcomp [x] = EvCoercion (co2 `mkTcTransCo` evTermCoercion x) xcomp _ = panic "No more goals!" -- xdecomp : (F args ~ xi1) -> [(xi2 ~ xi1)] - xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` mkTcCoVarCo x)] + xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` evTermCoercion x)] - ; xCtFlavor_cache False fl1 [mkTcEqPred xi2 xi1] xev $ what_next d1 + ; ctevs <- xCtFlavor_cache False fl1 [mkTcEqPred xi2 xi1] xev -- Why not simply xCtFlavor? See Note [Cache-caused loops] -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation] + ; add_to_work d1 ctevs ; irInertConsumed "FunEq/FunEq"} where + add_to_work d [ctev] = updWorkListTcS $ extendWorkListEq $ + CNonCanonical {cc_ev = ctev, cc_depth = d} + add_to_work _ _ = return () + lhss_match = tc1 == tc2 && eqTypes args1 args2 - what_next d [new_fl] - = updWorkListTcS $ - extendWorkListEq (CNonCanonical {cc_flavor=new_fl,cc_depth = d}) - what_next _ _ = return () - co1 = mkTcCoVarCo $ flav_evar fl1 - co2 = mkTcCoVarCo $ flav_evar fl2 - mk_sym_co x = mkTcSymCo (mkTcCoVarCo x) + co1 = evTermCoercion $ ctEvTerm fl1 + co2 = evTermCoercion $ ctEvTerm fl2 + mk_sym_co x = mkTcSymCo (evTermCoercion x) doInteractWithInert _ _ = irKeepGoing "NOP" @@ -905,7 +903,7 @@ solving. \begin{code} solveOneFromTheOther :: String -- Info - -> CtFlavor -- Inert + -> CtEvidence -- Inert -> Ct -- WorkItem -> TcS InteractResult -- Preconditions: @@ -920,22 +918,23 @@ solveOneFromTheOther info ifl workItem -- so it's safe to continue on from this point = irInertConsumed ("Solved[DI] " ++ info) - | isSolved ifl, isGivenOrSolved wfl +{- ToDo: Check with Dimitrios + | isSolved ifl, isGiven wfl -- Same if the inert is a GivenSolved -- just get rid of it = irInertConsumed ("Solved[SI] " ++ info) +-} | otherwise = ASSERT( ifl `canSolve` wfl ) -- Because of Note [The Solver Invariant], plus Derived dealt with - do { when (isWanted wfl) $ setEvBind wid (EvId iid) + do { case wfl of + Wanted { ctev_evar = ev_id } -> setEvBind ev_id (ctEvTerm ifl) + _ -> return () -- Overwrite the binding, if one exists -- If both are Given, we already have evidence; no need to duplicate ; irWorkItemConsumed ("Solved " ++ info) } where - wfl = cc_flavor workItem - wid = ctId workItem - iid = flav_evar ifl - + wfl = cc_ev workItem \end{code} Note [Superclasses and recursive dictionaries] @@ -1305,7 +1304,7 @@ now!). rewriteWithFunDeps :: [Equation] -> [Xi] -> WantedLoc - -> TcS (Maybe ([Xi], [TcCoercion], [(EvVar,WantedLoc)])) + -> TcS (Maybe ([Xi], [CtEvidence])) -- Not quite a WantedEvVar unfortunately -- Because our intention could be to make -- it derived at the end of the day @@ -1313,13 +1312,13 @@ rewriteWithFunDeps :: [Equation] -- Post: returns no trivial equalities (identities) and all EvVars returned are fresh rewriteWithFunDeps eqn_pred_locs xis wloc = do { fd_ev_poss <- mapM (instFunDepEqn wloc) eqn_pred_locs - ; let fd_ev_pos :: [(Int,(EqVar,WantedLoc))] + ; let fd_ev_pos :: [(Int,CtEvidence)] fd_ev_pos = concat fd_ev_poss - (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis) + rewritten_xis = rewriteDictParams fd_ev_pos xis ; if null fd_ev_pos then return Nothing - else return (Just (rewritten_xis, cos, map snd fd_ev_pos)) } + else return (Just (rewritten_xis, map snd fd_ev_pos)) } -instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,(EvVar,WantedLoc))] +instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,CtEvidence)] -- Post: Returns the position index as well as the corresponding FunDep equality instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs , fd_pred1 = d1, fd_pred2 = d2 }) @@ -1332,10 +1331,10 @@ instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs = let sty1 = Type.substTy subst ty1 sty2 = Type.substTy subst ty2 in if eqType sty1 sty2 then return ievs -- Return no trivial equalities - else do { mb_eqv <- newWantedEvVar (mkTcEqPred sty1 sty2) + else do { mb_eqv <- newDerived (push_ctx wl) (mkTcEqPred sty1 sty2) ; case mb_eqv of - Fresh eqv -> return $ (i,(eqv, push_ctx wl)):ievs - Cached {} -> return ievs } + Just ctev -> return $ (i,ctev):ievs + Nothing -> return ievs } -- We are eventually going to emit FD work back in the work list so -- it is important that we only return the /freshly created/ and not -- some existing equality! @@ -1355,34 +1354,30 @@ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])] ; return (tidy_env, msg) } -rewriteDictParams :: [(Int,(EqVar,WantedLoc))] -- A set of coercions : (pos, ty' ~ ty) - -> [Type] -- A sequence of types: tys - -> [(Type, TcCoercion)] -- Returns: [(ty', co : ty' ~ ty)] +rewriteDictParams :: [(Int,CtEvidence)] -- A set of coercions : (pos, ty' ~ ty) + -> [Type] -- A sequence of types: tys + -> [Type] rewriteDictParams param_eqs tys = zipWith do_one tys [0..] where - do_one :: Type -> Int -> (Type, TcCoercion) + do_one :: Type -> Int -> Type do_one ty n = case lookup n param_eqs of - Just wev -> (get_fst_ty wev, mkTcCoVarCo (fst wev)) - Nothing -> (ty, mkTcReflCo ty) -- Identity + Just wev -> get_fst_ty wev + Nothing -> ty - get_fst_ty (wev,_wloc) - | Just (ty1, _) <- getEqPredTys_maybe (evVarPred wev ) + get_fst_ty ctev + | Just (ty1, _) <- getEqPredTys_maybe (ctEvPred ctev) = ty1 | otherwise = panic "rewriteDictParams: non equality fundep!?" -emitFDWorkAsDerived :: [(EvVar,WantedLoc)] +emitFDWorkAsDerived :: [CtEvidence] -- All Derived -> SubGoalDepth -> TcS () emitFDWorkAsDerived evlocs d - = updWorkListTcS $ appendWorkListEqs fd_cts - where fd_cts = map mk_fd_ct evlocs - mk_fd_ct (v,wl) - = CNonCanonical { cc_flavor = Derived wl (evVarPred v) - , cc_depth = d } - - + = updWorkListTcS $ appendWorkListEqs (map mk_fd_ct evlocs) + where + mk_fd_ct der_ev = CNonCanonical { cc_ev = der_ev, cc_depth = d } \end{code} @@ -1432,11 +1427,11 @@ doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult -- Given dictionary -- See Note [Given constraint that matches an instance declaration] -doTopReact _inerts (CDictCan { cc_flavor = Given {} }) +doTopReact _inerts (CDictCan { cc_ev = Given {} }) = return NoTopInt -- NB: Superclasses already added since it's canonical -- Derived dictionary: just look for functional dependencies -doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc _pty +doTopReact _inerts workItem@(CDictCan { cc_ev = Derived loc _pty , cc_class = cls, cc_tyargs = xis }) = do { instEnvs <- getInstEnvs ; let fd_eqns = improveFromInstEnv instEnvs @@ -1444,7 +1439,7 @@ doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc _pty ; m <- rewriteWithFunDeps fd_eqns xis loc ; case m of Nothing -> return NoTopInt - Just (xis',_,fd_work) -> + Just (xis', fd_work) -> let workItem' = workItem { cc_tyargs = xis' } -- Deriveds are not supposed to have identity in do { emitFDWorkAsDerived fd_work (cc_depth workItem) @@ -1454,7 +1449,7 @@ doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc _pty } -- Wanted dictionary -doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc dict_id) +doTopReact inerts workItem@(CDictCan { cc_ev = fl@(Wanted { ctev_wloc = loc, ctev_evar = dict_id }) , cc_class = cls, cc_tyargs = xis , cc_depth = depth }) -- See Note [MATCHING-SYNONYMS] @@ -1470,108 +1465,103 @@ doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc dict_id) Nothing -> do { lkup_inst_res <- matchClassInst inerts cls xis loc ; case lkup_inst_res of - GenInst wtvs ev_term - -> let sfl = Solved (mkSolvedLoc loc UnkSkol) dict_id - in addToSolved (workItem { cc_flavor = sfl }) >> - doSolveFromInstance wtvs ev_term - NoInstance - -> return NoTopInt + GenInst wtvs ev_term -> do { addToSolved fl + ; doSolveFromInstance wtvs ev_term } + NoInstance -> return NoTopInt } -- Actual Functional Dependencies - Just (_xis',_cos,fd_work) -> + Just (_xis', fd_work) -> do { emitFDWorkAsDerived fd_work (cc_depth workItem) ; return SomeTopInt { tir_rule = "Dict/Top (fundeps)" , tir_new_item = ContinueWith workItem } } } - where doSolveFromInstance :: [EvVar] -> EvTerm -> TcS TopInteractResult - -- Precondition: evidence term matches the predicate workItem - doSolveFromInstance evs ev_term - | null evs - = do { traceTcS "doTopReact/found nullary instance for" $ - ppr dict_id - ; setEvBind dict_id ev_term - ; return $ - SomeTopInt { tir_rule = "Dict/Top (solved, no new work)" - , tir_new_item = Stop } } - | otherwise - = do { traceTcS "doTopReact/found non-nullary instance for" $ - ppr dict_id - ; setEvBind dict_id ev_term - ; let mk_new_wanted ev - = CNonCanonical { cc_flavor = fl { flav_evar = ev } - , cc_depth = depth + 1 } - ; updWorkListTcS (appendWorkListCt (map mk_new_wanted evs)) - ; return $ - SomeTopInt { tir_rule = "Dict/Top (solved, more work)" - , tir_new_item = Stop } - } + where + doSolveFromInstance :: [CtEvidence] -> EvTerm -> TcS TopInteractResult + -- Precondition: evidence term matches the predicate workItem + doSolveFromInstance evs ev_term + | null evs + = do { traceTcS "doTopReact/found nullary instance for" $ + ppr dict_id + ; setEvBind dict_id ev_term + ; return $ + SomeTopInt { tir_rule = "Dict/Top (solved, no new work)" + , tir_new_item = Stop } } + | otherwise + = do { traceTcS "doTopReact/found non-nullary instance for" $ + ppr dict_id + ; setEvBind dict_id ev_term + ; let mk_new_wanted ev + = CNonCanonical { cc_ev = ev + , cc_depth = depth + 1 } + ; updWorkListTcS (appendWorkListCt (map mk_new_wanted evs)) + ; return $ + SomeTopInt { tir_rule = "Dict/Top (solved, more work)" + , tir_new_item = Stop } + } -- Type functions -doTopReact _inerts (CFunEqCan { cc_flavor = fl }) +{- ToDo: Check with Dimitrios +doTopReact _inerts (CFunEqCan { cc_ev = fl }) | isSolved fl = return NoTopInt -- If Solved, no more interactions should happen +-} -- Otherwise, it's a Given, Derived, or Wanted -doTopReact _inerts workItem@(CFunEqCan { cc_flavor = fl, cc_depth = d +doTopReact _inerts workItem@(CFunEqCan { cc_ev = fl, cc_depth = d , cc_fun = tc, cc_tyargs = args, cc_rhs = xi }) = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS] ; case match_res of Nothing -> return NoTopInt Just (famInst, rep_tys) - -> do { mb_already_solved <- lkpFunEqCache (mkTyConApp tc args) + -> do { mb_already_solved <- lkpSolvedFunEqCache (mkTyConApp tc args) ; traceTcS "doTopReact: Family instance matches" $ vcat [ text "solved-fun-cache" <+> if isJust mb_already_solved then text "hit" else text "miss" , text "workItem =" <+> ppr workItem ] ; let (coe,rhs_ty) - | Just cached_ct <- mb_already_solved - = (mkTcCoVarCo (ctId cached_ct), - cc_rhs cached_ct) + | Just ctev <- mb_already_solved + , not (isDerived ctev) + = ASSERT( isEqPred (ctEvPred ctev) ) + (evTermCoercion (ctEvTerm ctev), snd (getEqPredTys (ctEvPred ctev))) | otherwise = let coe_ax = famInstAxiom famInst in (mkTcAxInstCo coe_ax rep_tys, mkAxInstRHS coe_ax rep_tys) - xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` mkTcCoVarCo x)] - xcomp [x] = EvCoercion (coe `mkTcTransCo` mkTcCoVarCo x) + xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` evTermCoercion x)] + xcomp [x] = EvCoercion (coe `mkTcTransCo` evTermCoercion x) xcomp _ = panic "No more goals!" xev = XEvTerm xcomp xdecomp - ; xCtFlavor fl [mkTcEqPred rhs_ty xi] xev what_next } } - where what_next [ct_flav] - = do { updWorkListTcS $ - extendWorkListEq (CNonCanonical { cc_flavor = ct_flav - , cc_depth = d+1 }) - ; cache_in_solved fl - ; return $ SomeTopInt { tir_rule = "Fun/Top" - , tir_new_item = Stop } } - what_next _ -- No subgoal (because it's cached) - = do { cache_in_solved fl - ; return $ SomeTopInt { tir_rule = "Fun/Top" - , tir_new_item = Stop } } - - cache_in_solved (Derived {}) = return () - cache_in_solved (Wanted wl ev) = - let sfl = Solved (mkSolvedLoc wl UnkSkol) ev - solved = workItem { cc_flavor = sfl } - in updFunEqCache solved >> addToSolved solved - cache_in_solved fl = - let sfl = Solved (flav_gloc fl) (flav_evar fl) - solved = workItem { cc_flavor = sfl } - in updFunEqCache solved >> addToSolved solved + ; ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev + ; case ctevs of + [ctev] -> updWorkListTcS $ extendWorkListEq $ + CNonCanonical { cc_ev = ctev + , cc_depth = d+1 } + ctevs -> -- No subgoal (because it's cached) + ASSERT( null ctevs) return () + + ; unless (isDerived fl) $ + do { addSolvedFunEq fl + ; addToSolved fl } + ; return $ SomeTopInt { tir_rule = "Fun/Top" + , tir_new_item = Stop } } } -- Any other work item does not react with any top-level equations doTopReact _inerts _workItem = return NoTopInt -lkpFunEqCache :: TcType -> TcS (Maybe Ct) -lkpFunEqCache fam_head +lkpSolvedFunEqCache :: TcType -> TcS (Maybe CtEvidence) +lkpSolvedFunEqCache fam_head = do { (_subst,_inscope) <- getInertEqs ; fun_cache <- getTcSInerts >>= (return . inert_solved_funeqs) ; traceTcS "lkpFunEqCache" $ vcat [ text "fam_head =" <+> ppr fam_head - , text "funeq cache =" <+> pprCtTypeMap (unCtFamHeadMap fun_cache) ] - ; rewrite_cached $ - lookupTM fam_head (unCtFamHeadMap fun_cache) } + , text "funeq cache =" <+> ppr fun_cache ] + ; return (lookupFamHead fun_cache fam_head) } + +{- ToDo; talk to Dimitrios. I have no idea what is happening here + + ; rewrite_cached (lookupFamHead fun_cache fam_head) } -- The two different calls do not seem to make a significant difference in -- terms of hit/miss rate for many memory-critical/performance tests but the -- latter blows up the space on the heap somehow ... It maybe the niFixTvSubst. @@ -1579,11 +1569,10 @@ lkpFunEqCache fam_head -- lookupTypeMap_mod subst cc_rhs fam_head (unCtFamHeadMap fun_cache) } where rewrite_cached Nothing = return Nothing - rewrite_cached (Just ct@(CFunEqCan { cc_flavor = fl, cc_depth = d + rewrite_cached (Just ct@(CFunEqCan { cc_ev = fl, cc_depth = d , cc_fun = tc, cc_tyargs = xis , cc_rhs = xi})) - = ASSERT (isSolved fl) - do { (xis_subst,cos) <- flattenMany d FMFullFlatten fl xis + = do { (xis_subst,cos) <- flattenMany d FMFullFlatten fl xis -- cos :: xis_subst ~ xis ; (xi_subst,co) <- flatten d FMFullFlatten fl xi -- co :: xi_subst ~ xi @@ -1607,27 +1596,14 @@ lkpFunEqCache fam_head -> return Nothing -- Strange: cached? Just fl' -> return $ - Just (CFunEqCan { cc_flavor = fl' + Just (CFunEqCan { cc_ev = fl' , cc_depth = d , cc_fun = tc , cc_tyargs = xis_subst , cc_rhs = xi_subst }) } rewrite_cached (Just other_ct) = pprPanic "lkpFunEqCache:not family equation!" $ ppr other_ct - -updFunEqCache :: Ct -> TcS () -updFunEqCache fun_eq@(CFunEqCan { cc_fun = tc, cc_tyargs = xis }) - = modifyInertTcS $ \inert -> ((), upd_inert inert) - where upd_inert inert - = let slvd = unCtFamHeadMap (inert_solved_funeqs inert) - in inert { inert_solved_funeqs = - CtFamHeadMap (alterTM key upd_funeqs slvd) } - upd_funeqs Nothing = Just fun_eq - upd_funeqs (Just _ct) = Just fun_eq - -- Or _ct? depends on which caches more steps of computation - key = mkTyConApp tc xis -updFunEqCache other = pprPanic "updFunEqCache:Non family equation" $ ppr other - +-} \end{code} @@ -1830,7 +1806,7 @@ NB: The desugarer needs be more clever to deal with equalities \begin{code} data LookupInstResult = NoInstance - | GenInst [EvVar] EvTerm + | GenInst [CtEvidence] EvTerm matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult @@ -1875,12 +1851,11 @@ matchClassInst inerts clas tys loc ; if null theta then return (GenInst [] (EvDFunApp dfun_id tys [])) else do - { evc_vars <- instDFunConstraints theta - ; let ev_vars = map mn_thing evc_vars - new_ev_vars = [mn_thing evc | evc <- evc_vars - , isFresh evc ] + { evc_vars <- instDFunConstraints loc theta + ; let new_ev_vars = freshGoals evc_vars -- new_ev_vars are only the real new variables that can be emitted - ; return $ GenInst new_ev_vars (EvDFunApp dfun_id tys ev_vars) } } + dfun_app = EvDFunApp dfun_id tys (getEvTerms evc_vars) + ; return $ GenInst new_ev_vars dfun_app } } } where givens_for_this_clas :: Cts @@ -1892,7 +1867,7 @@ matchClassInst inerts clas tys loc given_overlap untch = anyBag (matchable untch) givens_for_this_clas matchable untch (CDictCan { cc_class = clas_g, cc_tyargs = sys - , cc_flavor = fl }) + , cc_ev = fl }) | isGiven fl = ASSERT( clas_g == clas ) case tcUnifyTys (\tv -> if isTouchableMetaTyVar_InRange untch tv && diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 3ba80e3b0f..79b6b02950 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -627,29 +627,24 @@ zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol }) zonkCt :: Ct -> TcM Ct -- Zonking a Ct conservatively gives back a CNonCanonical zonkCt ct - = do { fl' <- zonkFlavor (cc_flavor ct) + = do { fl' <- zonkCtEvidence (cc_ev ct) ; return $ - CNonCanonical { cc_flavor = fl' + CNonCanonical { cc_ev = fl' , cc_depth = cc_depth ct } } zonkCts :: Cts -> TcM Cts zonkCts = mapBagM zonkCt -zonkFlavor :: CtFlavor -> TcM CtFlavor -zonkFlavor (Given loc evar) +zonkCtEvidence :: CtEvidence -> TcM CtEvidence +zonkCtEvidence ctev@(Given { ctev_gloc = loc, ctev_pred = pred }) = do { loc' <- zonkGivenLoc loc - ; evar' <- zonkEvVar evar - ; return (Given loc' evar') } -zonkFlavor (Solved loc evar) - = do { loc' <- zonkGivenLoc loc - ; evar' <- zonkEvVar evar - ; return (Solved loc' evar') } -zonkFlavor (Wanted loc evar) - = do { evar' <- zonkEvVar evar - ; return (Wanted loc evar') } -zonkFlavor (Derived loc pty) - = do { pty' <- zonkTcType pty - ; return (Derived loc pty') } - + ; pred' <- zonkTcType pred + ; return (ctev { ctev_gloc = loc', ctev_pred = pred'}) } +zonkCtEvidence ctev@(Wanted { ctev_pred = pred }) + = do { pred' <- zonkTcType pred + ; return (ctev { ctev_pred = pred' }) } +zonkCtEvidence ctev@(Derived { ctev_pred = pred }) + = do { pred' <- zonkTcType pred + ; return (ctev { ctev_pred = pred' }) } zonkGivenLoc :: GivenLoc -> TcM GivenLoc -- GivenLocs may have unification variables inside them! diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs index 6a79b738fd..d17d3e6a10 100644 --- a/compiler/typecheck/TcRnTypes.lhs +++ b/compiler/typecheck/TcRnTypes.lhs @@ -55,9 +55,9 @@ module TcRnTypes( singleCt, extendCts, isEmptyCts, isCTyEqCan, isCFunEqCan, isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe, isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt, - isGivenCt, isGivenOrSolvedCt, - ctWantedLoc, - SubGoalDepth, mkNonCanonical, ctPred, ctFlavPred, ctId, ctFlavId, + isGivenCt, + ctWantedLoc, ctEvidence, + SubGoalDepth, mkNonCanonical, ctPred, ctEvPred, ctEvTerm, ctEvId, WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC, andWC, addFlats, addImplics, mkFlatWC, @@ -70,9 +70,9 @@ module TcRnTypes( SkolemInfo(..), - CtFlavor(..), pprFlavorArising, - mkSolvedLoc, mkGivenLoc, - isWanted, isGivenOrSolved, isGiven, isSolved, + CtEvidence(..), pprFlavorArising, + mkGivenLoc, + isWanted, isGiven, isDerived, getWantedLoc, getGivenLoc, canSolve, canRewrite, -- Pretty printing @@ -89,7 +89,7 @@ module TcRnTypes( import HsSyn import HscTypes -import TcEvidence( EvBind, EvBindsVar ) +import TcEvidence import Type import Class ( Class ) import TyCon ( TyCon ) @@ -850,7 +850,7 @@ type SubGoalDepth = Int -- An ever increasing number used to restrict data Ct -- Atomic canonical constraints = CDictCan { -- e.g. Num xi - cc_flavor :: CtFlavor, + cc_ev :: CtEvidence, cc_class :: Class, cc_tyargs :: [Xi], @@ -860,14 +860,14 @@ data Ct | CIPCan { -- ?x::tau -- See note [Canonical implicit parameter constraints]. - cc_flavor :: CtFlavor, + cc_ev :: CtEvidence, cc_ip_nm :: IPName Name, - cc_ip_ty :: TcTauType, -- Not a Xi! See same not as above + cc_ip_ty :: TcTauType, -- Not a Xi! See same not as above cc_depth :: SubGoalDepth -- See Note [WorkList] } | CIrredEvCan { -- These stand for yet-unknown predicates - cc_flavor :: CtFlavor, + cc_ev :: CtEvidence, cc_ty :: Xi, -- cc_ty is flat hence it may only be of the form (tv xi1 xi2 ... xin) -- Since, if it were a type constructor application, that'd make the -- whole constraint a CDictCan, CIPCan, or CTyEqCan. And it can't be @@ -881,7 +881,7 @@ data Ct -- * typeKind xi `compatKind` typeKind tv -- See Note [Spontaneous solving and kind compatibility] -- * We prefer unification variables on the left *JUST* for efficiency - cc_flavor :: CtFlavor, + cc_ev :: CtEvidence, cc_tyvar :: TcTyVar, cc_rhs :: Xi, @@ -891,7 +891,7 @@ data Ct | CFunEqCan { -- F xis ~ xi -- Invariant: * isSynFamilyTyCon cc_fun -- * typeKind (F xis) `compatKind` typeKind xi - cc_flavor :: CtFlavor, + cc_ev :: CtEvidence, cc_fun :: TyCon, -- A type function cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated cc_rhs :: Xi, -- *never* over-saturated (because if so @@ -902,18 +902,24 @@ data Ct } | CNonCanonical { -- See Note [NonCanonical Semantics] - cc_flavor :: CtFlavor, + cc_ev :: CtEvidence, cc_depth :: SubGoalDepth } \end{code} \begin{code} -mkNonCanonical :: CtFlavor -> Ct -mkNonCanonical flav = CNonCanonical { cc_flavor = flav, cc_depth = 0} +mkNonCanonical :: CtEvidence -> Ct +mkNonCanonical flav = CNonCanonical { cc_ev = flav, cc_depth = 0} + +ctEvidence :: Ct -> CtEvidence +ctEvidence = cc_ev ctPred :: Ct -> PredType -ctPred (CNonCanonical { cc_flavor = fl }) = ctFlavPred fl +ctPred ct = ctEvPred (cc_ev ct) +-- ToDo Check with Dimitrios +{- +ctPred (CNonCanonical { cc_ev = fl }) = ctEvPred fl ctPred (CDictCan { cc_class = cls, cc_tyargs = xis }) = mkClassPred cls xis ctPred (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) @@ -923,18 +929,13 @@ ctPred (CFunEqCan { cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 }) ctPred (CIPCan { cc_ip_nm = nm, cc_ip_ty = xi }) = mkIPPred nm xi ctPred (CIrredEvCan { cc_ty = xi }) = xi - - -ctId :: Ct -> EvVar --- Precondition: not a derived! -ctId ct = ctFlavId (cc_flavor ct) - +-} \end{code} %************************************************************************ %* * - CtFlavor + CtEvidence The "flavor" of a canonical constraint %* * %************************************************************************ @@ -942,20 +943,17 @@ ctId ct = ctFlavId (cc_flavor ct) \begin{code} ctWantedLoc :: Ct -> WantedLoc -- Only works for Wanted/Derived -ctWantedLoc ct = ASSERT2( not (isGivenOrSolved (cc_flavor ct)), ppr ct ) - getWantedLoc (cc_flavor ct) +ctWantedLoc ct = ASSERT2( not (isGiven (cc_ev ct)), ppr ct ) + getWantedLoc (cc_ev ct) isWantedCt :: Ct -> Bool -isWantedCt = isWanted . cc_flavor +isWantedCt = isWanted . cc_ev isGivenCt :: Ct -> Bool -isGivenCt = isGiven . cc_flavor +isGivenCt = isGiven . cc_ev isDerivedCt :: Ct -> Bool -isDerivedCt = isDerived . cc_flavor - -isGivenOrSolvedCt :: Ct -> Bool -isGivenOrSolvedCt = isGivenOrSolved . cc_flavor +isDerivedCt = isDerived . cc_ev isCTyEqCan :: Ct -> Bool isCTyEqCan (CTyEqCan {}) = True @@ -989,7 +987,7 @@ isCNonCanonical _ = False \begin{code} instance Outputable Ct where - ppr ct = ppr (cc_flavor ct) <+> + ppr ct = ppr (cc_ev ct) <+> braces (ppr (cc_depth ct)) <+> parens (text ct_sort) where ct_sort = case ct of CTyEqCan {} -> "CTyEqCan" @@ -1229,86 +1227,80 @@ pprWantedsWithLocs wcs %* * %************************************************************************ +Note [Evidence field of CtEvidence] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +During constraint solving we never look at the type of ctev_evtm, or +ctev_evar; instead we look at the cte_pred field. The evtm/evar field +may be un-zonked. + \begin{code} -data CtFlavor - = Given { flav_gloc :: GivenLoc, flav_evar :: EvVar } - -- Trully given, not depending on subgoals +data CtEvidence -- Rename to CtEvidence + = Given { ctev_gloc :: GivenLoc + , ctev_pred :: TcPredType + , ctev_evtm :: EvTerm } -- See Note [Evidence field of CtEvidence] + -- Truly given, not depending on subgoals -- NB: Spontaneous unifications belong here -- DV TODOs: (i) Consider caching actual evidence _term_ -- (ii) Revisit Note [Optimizing Spontaneously Solved Coercions] - | Solved { flav_gloc :: GivenLoc, flav_evar :: EvVar } - -- Originally wanted, but now we've produced and - -- bound some partial evidence for this constraint. - -- NB: Evidence may rely on yet-wanted constraints or other solved or given - - | Wanted { flav_wloc :: WantedLoc, flav_evar :: EvVar } + | Wanted { ctev_wloc :: WantedLoc + , ctev_pred :: TcPredType + , ctev_evar :: EvVar } -- See Note [Evidence field of CtEvidence] -- Wanted goal - | Derived { flav_wloc :: WantedLoc, flav_der_pty :: TcPredType } + | Derived { ctev_wloc :: WantedLoc + , ctev_pred :: TcPredType } -- A goal that we don't really have to solve and can't immediately - -- rewrite anything other than a derived (there's no evidence variable!) + -- rewrite anything other than a derived (there's no evidence!) -- but if we do manage to solve it may help in solving other goals. -ctFlavPred :: CtFlavor -> TcPredType +ctEvPred :: CtEvidence -> TcPredType -- The predicate of a flavor -ctFlavPred (Given _ evar) = evVarPred evar -ctFlavPred (Solved _ evar) = evVarPred evar -ctFlavPred (Wanted _ evar) = evVarPred evar -ctFlavPred (Derived { flav_der_pty = pty }) = pty - -ctFlavId :: CtFlavor -> EvVar --- Precondition: can't be derived -ctFlavId (Derived _ pty) - = pprPanic "ctFlavId: derived constraint cannot have id" $ - text "pty =" <+> ppr pty -ctFlavId fl = flav_evar fl - -instance Outputable CtFlavor where +ctEvPred = ctev_pred + +ctEvTerm :: CtEvidence -> EvTerm +ctEvTerm (Given { ctev_evtm = tm }) = tm +ctEvTerm (Wanted { ctev_evar = ev }) = EvId ev +ctEvTerm ctev@(Derived {}) = pprPanic "ctEvTerm: derived constraint cannot have id" + (ppr ctev) + +ctEvId :: CtEvidence -> TcId +ctEvId (Wanted { ctev_evar = ev }) = ev +ctEvId ctev = pprPanic "ctEvId:" (ppr ctev) + +instance Outputable CtEvidence where ppr fl = case fl of - (Given _ evar) -> ptext (sLit "[G]") <+> ppr evar <+> ppr_pty - (Solved _ evar) -> ptext (sLit "[S]") <+> ppr evar <+> ppr_pty - (Wanted _ evar) -> ptext (sLit "[W]") <+> ppr evar <+> ppr_pty - (Derived {}) -> ptext (sLit "[D]") <+> text "_" <+> ppr_pty - where ppr_pty = dcolon <+> ppr (ctFlavPred fl) + Given {} -> ptext (sLit "[G]") <+> ppr (ctev_evtm fl) <+> ppr_pty + Wanted {} -> ptext (sLit "[W]") <+> ppr (ctev_evar fl) <+> ppr_pty + Derived {} -> ptext (sLit "[D]") <+> text "_" <+> ppr_pty + where ppr_pty = dcolon <+> ppr (ctEvPred fl) -getWantedLoc :: CtFlavor -> WantedLoc +getWantedLoc :: CtEvidence -> WantedLoc -- Precondition: Wanted or Derived -getWantedLoc fl = flav_wloc fl +getWantedLoc fl = ctev_wloc fl -getGivenLoc :: CtFlavor -> GivenLoc --- Precondition: Given or Solved -getGivenLoc fl = flav_gloc fl +getGivenLoc :: CtEvidence -> GivenLoc +-- Precondition: Given +getGivenLoc fl = ctev_gloc fl -pprFlavorArising :: CtFlavor -> SDoc -pprFlavorArising (Given gl _) = pprArisingAt gl -pprFlavorArising (Solved gl _) = pprArisingAt gl -pprFlavorArising (Wanted wl _) = pprArisingAt wl -pprFlavorArising (Derived wl _) = pprArisingAt wl +pprFlavorArising :: CtEvidence -> SDoc +pprFlavorArising (Given { ctev_gloc = gl }) = pprArisingAt gl +pprFlavorArising ctev = pprArisingAt (ctev_wloc ctev) -isWanted :: CtFlavor -> Bool +isWanted :: CtEvidence -> Bool isWanted (Wanted {}) = True isWanted _ = False -isGivenOrSolved :: CtFlavor -> Bool -isGivenOrSolved (Given {}) = True -isGivenOrSolved (Solved {}) = True -isGivenOrSolved _ = False - -isSolved :: CtFlavor -> Bool -isSolved (Solved {}) = True -isSolved _ = False - -isGiven :: CtFlavor -> Bool -isGiven (Given {}) = True +isGiven :: CtEvidence -> Bool +isGiven (Given {}) = True isGiven _ = False -isDerived :: CtFlavor -> Bool +isDerived :: CtEvidence -> Bool isDerived (Derived {}) = True isDerived _ = False -canSolve :: CtFlavor -> CtFlavor -> Bool +canSolve :: CtEvidence -> CtEvidence -> Bool -- canSolve ctid1 ctid2 -- The constraint ctid1 can be used to solve ctid2 -- "to solve" means a reaction where the active parts of the two constraints match. @@ -1325,18 +1317,13 @@ canSolve (Wanted {}) (Wanted {}) = True canSolve (Derived {}) (Derived {}) = True -- Derived can't solve wanted/given canSolve _ _ = False -- No evidence for a derived, anyway -canRewrite :: CtFlavor -> CtFlavor -> Bool +canRewrite :: CtEvidence -> CtEvidence -> Bool -- canRewrite ct1 ct2 -- The equality constraint ct1 can be used to rewrite inside ct2 canRewrite = canSolve - mkGivenLoc :: WantedLoc -> SkolemInfo -> GivenLoc mkGivenLoc wl sk = setCtLocOrigin wl sk - -mkSolvedLoc :: WantedLoc -> SkolemInfo -> GivenLoc -mkSolvedLoc wl sk = setCtLocOrigin wl sk - \end{code} %************************************************************************ diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index ca7cf88fd1..5b7d650dc8 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -24,15 +24,13 @@ module TcSMonad ( Ct(..), Xi, tyVarsOfCt, tyVarsOfCts, tyVarsOfCDicts, emitFrozenError, - isWanted, isGivenOrSolved, isDerived, - isGivenOrSolvedCt, isGivenCt, - isWantedCt, isDerivedCt, pprFlavorArising, + isWanted, isDerived, + isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising, isFlexiTcsTv, canRewrite, canSolve, - mkSolvedLoc, mkGivenLoc, - ctWantedLoc, + mkGivenLoc, ctWantedLoc, TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality traceFireTcS, bumpStepCountTcS, doWithInert, @@ -42,16 +40,17 @@ module TcSMonad ( SimplContext(..), isInteractive, performDefaulting, -- Getting and setting the flattening cache - getFlatCache, updFlatCache, addToSolved, + getFlatCache, updFlatCache, addToSolved, addSolvedFunEq, deferTcSForAllEq, setEvBind, XEvTerm(..), - MaybeNew (..), isFresh, - xCtFlavor, -- Transform a CtFlavor during a step + MaybeNew (..), isFresh, freshGoals, getEvTerms, + + xCtFlavor, -- Transform a CtEvidence during a step rewriteCtFlavor, -- Specialized version of xCtFlavor for coercions - newWantedEvVar, newGivenEvVar, instDFunConstraints, newKindConstraint, + newWantedEvVar, instDFunConstraints, newKindConstraint, newDerived, xCtFlavor_cache, rewriteCtFlavor_cache, @@ -68,12 +67,14 @@ module TcSMonad ( -- Inerts InertSet(..), InertCans(..), getInertEqs, getCtCoercion, - emptyInert, getTcSInerts, lookupInInerts, updInertSet, extractUnsolved, + emptyInert, getTcSInerts, lookupInInerts, + extractUnsolved, extractUnsolvedTcS, modifyInertTcS, updInertSetTcS, partitionCCanMap, partitionEqMap, getRelevantCts, extractRelevantInerts, - CCanMap (..), CtTypeMap, CtFamHeadMap(..), CtPredMap(..), - pprCtTypeMap, partCtFamHeadMap, + CCanMap(..), CtTypeMap, CtFamHeadMap, CtPredMap, + PredMap, FamHeadMap, + partCtFamHeadMap, lookupFamHead, instDFunType, -- Instantiation @@ -136,14 +137,12 @@ import TcRnTypes import Unique import UniqFM -import Maybes ( orElse ) +import Maybes ( orElse, catMaybes ) import Control.Monad( when ) import StaticFlags( opt_PprStyle_Debug ) import Data.IORef -import Data.List ( find ) -import Control.Monad ( zipWithM ) import TrieMap \end{code} @@ -298,11 +297,10 @@ emptyCCanMap = CCanMap { cts_given = emptyUFM, cts_derived = emptyUFM, cts_wante updCCanMap:: Uniquable a => (a,Ct) -> CCanMap a -> CCanMap a updCCanMap (a,ct) cmap - = case cc_flavor ct of + = case cc_ev ct of Wanted {} -> cmap { cts_wanted = insert_into (cts_wanted cmap) } Given {} -> cmap { cts_given = insert_into (cts_given cmap) } Derived {} -> cmap { cts_derived = insert_into (cts_derived cmap) } - Solved {} -> panic "updCCanMap update with solved!" where insert_into m = addToUFM_C unionBags m a (singleCt ct) @@ -319,13 +317,24 @@ getRelevantCts a cmap where lookup map = lookupUFM map a `orElse` emptyCts -lookupCCanMap :: Uniquable a => a -> (Ct -> Bool) -> CCanMap a -> Maybe Ct -lookupCCanMap a p map - = let possible_cts = lookupUFM (cts_given map) a `orElse` - lookupUFM (cts_wanted map) a `orElse` - lookupUFM (cts_derived map) a `orElse` emptyCts - in find p (bagToList possible_cts) +lookupCCanMap :: Uniquable a => a -> (CtEvidence -> Bool) -> CCanMap a -> Maybe CtEvidence +lookupCCanMap a pick_me map + = findEvidence pick_me possible_cts + where + possible_cts = lookupUFM (cts_given map) a `plus` ( + lookupUFM (cts_wanted map) a `plus` ( + lookupUFM (cts_derived map) a `plus` emptyCts)) + plus Nothing cts2 = cts2 + plus (Just cts1) cts2 = cts1 `unionBags` cts2 + +findEvidence :: (CtEvidence -> Bool) -> Cts -> Maybe CtEvidence +findEvidence pick_me cts + = foldrBag pick Nothing cts + where + pick :: Ct -> Maybe CtEvidence -> Maybe CtEvidence + pick ct deflt | let ctev = cc_ev ct, pick_me ctev = Just ctev + | otherwise = deflt partitionCCanMap :: (Ct -> Bool) -> CCanMap a -> (Cts,CCanMap a) -- All constraints that /match/ the predicate go in the bag, the rest remain in the map @@ -360,27 +369,33 @@ extractUnsolvedCMap cmap = -- Maps from PredTypes to Constraints -type CtTypeMap = TypeMap Ct -newtype CtPredMap = - CtPredMap { unCtPredMap :: CtTypeMap } -- Indexed by TcPredType -newtype CtFamHeadMap = - CtFamHeadMap { unCtFamHeadMap :: CtTypeMap } -- Indexed by family head +type CtTypeMap = TypeMap Ct +type CtPredMap = PredMap Ct +type CtFamHeadMap = FamHeadMap Ct + +newtype PredMap a = PredMap { unPredMap :: TypeMap a } -- Indexed by TcPredType +newtype FamHeadMap a = FamHeadMap { unFamHeadMap :: TypeMap a } -- Indexed by family head -pprCtTypeMap :: TypeMap Ct -> SDoc -pprCtTypeMap ctmap = ppr (foldTM (:) ctmap []) +instance Outputable a => Outputable (PredMap a) where + ppr (PredMap m) = ppr (foldTM (:) m []) + +instance Outputable a => Outputable (FamHeadMap a) where + ppr (FamHeadMap m) = ppr (foldTM (:) m []) ctTypeMapCts :: TypeMap Ct -> Cts ctTypeMapCts ctmap = foldTM (\ct cts -> extendCts cts ct) ctmap emptyCts +lookupFamHead :: FamHeadMap a -> TcType -> Maybe a +lookupFamHead (FamHeadMap m) key = lookupTM key m partCtFamHeadMap :: (Ct -> Bool) -> CtFamHeadMap -> (Cts, CtFamHeadMap) partCtFamHeadMap f ctmap = let (cts,tymap_final) = foldTM upd_acc tymap_inside (emptyBag, tymap_inside) - in (cts, CtFamHeadMap tymap_final) + in (cts, FamHeadMap tymap_final) where - tymap_inside = unCtFamHeadMap ctmap + tymap_inside = unFamHeadMap ctmap upd_acc ct (cts,acc_map) | f ct = (extendCts cts ct, alterTM ct_key (\_ -> Nothing) acc_map) | otherwise = (cts,acc_map) @@ -388,8 +403,6 @@ partCtFamHeadMap f ctmap = ty1 | otherwise = panic "partCtFamHeadMap, encountered non equality!" - - \end{code} %************************************************************************ @@ -400,9 +413,7 @@ partCtFamHeadMap f ctmap %************************************************************************ \begin{code} - - --- All Given (fully known) or Wanted or Derived, never Solved +-- All Given (fully known) or Wanted or Derived -- See Note [Detailed InertCans Invariants] for more data InertCans = IC { inert_eqs :: TyVarEnv Ct @@ -467,29 +478,51 @@ The InertCans represents a collection of constraints with the following properti occurs errors. 9 Given family or dictionary constraints don't mention touchable unification variables -\begin{code} +Note [Solved constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~ +When we take a step to simplify a constraint 'c', we call the original constraint "solved". +For example: Wanted: ev :: [s] ~ [t] + New goal: ev1 :: s ~ t + Then 'ev' is now "solved". + +The reason for all this is simply to avoid re-solving goals we have solved already. + +* A solved Wanted may depend on as-yet-unsolved goals, so (for example) we should not + use it to rewrite a Given; in that sense the solved goal is still a Wanted + +* A solved Given is just given + +* A solved Derived is possible; purpose is to avoid creating tons of identical + Derived goals. + +\begin{code} -- The Inert Set data InertSet = IS { inert_cans :: InertCans - -- Canonical Given,Wanted,Solved + -- Canonical Given, Wanted, Derived (no Solved) + -- Sometimes called "the inert set" + , inert_frozen :: Cts -- Frozen errors (as non-canonicals) - , inert_solved :: CtPredMap - -- Solved constraints (for caching): - -- (i) key is by predicate type - -- (ii) all of 'Solved' flavor, may or may not be canonicals - -- (iii) we use this field for avoiding creating newEvVars , inert_flat_cache :: CtFamHeadMap -- All ``flattening equations'' are kept here. -- Always canonical CTyFunEqs (Given or Wanted only!) - -- Key is by family head. We used this field during flattening only - , inert_solved_funeqs :: CtFamHeadMap - -- Memoized Solved family equations co :: F xis ~ xi - -- Stored not necessarily as fully rewritten; we'll do that lazily - -- when we lookup + -- Key is by family head. We use this field during flattening only + -- Not necessarily inert wrt top-level equations (or inert_cans) + + , inert_solved_funeqs :: FamHeadMap CtEvidence -- Of form co :: F xis ~ xi + , inert_solved :: PredMap CtEvidence -- All others + -- These two fields constitute a cache of solved (only!) constraints + -- See Note [Solved constraints] + -- * Constraints of form (F xis ~ xi) live in inert_solved_funeqs, + -- all the others are in inert_solved + -- * Used to avoid creating a new EvVar when we have a new goal that we + -- have solvedin the past + -- * Stored not necessarily as fully rewritten + -- (ToDo: rewrite lazily when we lookup) } @@ -498,7 +531,7 @@ instance Outputable InertCans where , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts ics))) , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips ics))) , vcat (map ppr (Bag.bagToList $ - ctTypeMapCts (unCtFamHeadMap $ inert_funeqs ics))) + ctTypeMapCts (unFamHeadMap $ inert_funeqs ics))) , vcat (map ppr (Bag.bagToList $ inert_irreds ics)) ] @@ -508,7 +541,7 @@ instance Outputable InertSet where braces (vcat (map ppr (Bag.bagToList $ inert_frozen is))) , text "Solved and cached" <+> int (foldTypeMap (\_ x -> x+1) 0 - (unCtPredMap $ inert_solved is)) <+> + (unPredMap $ inert_solved is)) <+> text "more constraints" ] emptyInert :: InertSet @@ -517,28 +550,27 @@ emptyInert , inert_eq_tvs = emptyInScopeSet , inert_dicts = emptyCCanMap , inert_ips = emptyCCanMap - , inert_funeqs = CtFamHeadMap emptyTM + , inert_funeqs = FamHeadMap emptyTM , inert_irreds = emptyCts } , inert_frozen = emptyCts - , inert_flat_cache = CtFamHeadMap emptyTM - , inert_solved = CtPredMap emptyTM - , inert_solved_funeqs = CtFamHeadMap emptyTM } + , inert_flat_cache = FamHeadMap emptyTM + , inert_solved = PredMap emptyTM + , inert_solved_funeqs = FamHeadMap emptyTM } -type AtomicInert = Ct - -updInertSet :: InertSet -> AtomicInert -> InertSet --- Add a new inert element to the inert set. -updInertSet is item - | isSolved (cc_flavor item) - -- Solved items go in their special place - = let pty = ctPred item +updSolvedSet :: InertSet -> CtEvidence -> InertSet +updSolvedSet is item + = let pty = ctEvPred item upd_solved Nothing = Just item upd_solved (Just _existing_solved) = Just item -- .. or Just existing_solved? Is this even possible to happen? in is { inert_solved = - CtPredMap $ - alterTM pty upd_solved (unCtPredMap $ inert_solved is) } + PredMap $ + alterTM pty upd_solved (unPredMap $ inert_solved is) } + +updInertSet :: InertSet -> Ct -> InertSet +-- Add a new inert element to the inert set. +updInertSet is item | isCNonCanonical item -- NB: this may happen if we decide to kick some frozen error -- out to rewrite him. Frozen errors are just NonCanonicals @@ -548,7 +580,7 @@ updInertSet is item -- A canonical Given, Wanted, or Derived = is { inert_cans = upd_inert_cans (inert_cans is) item } - where upd_inert_cans :: InertCans -> AtomicInert -> InertCans + where upd_inert_cans :: InertCans -> Ct -> InertCans -- Precondition: item /is/ canonical upd_inert_cans ics item | isCTyEqCan item @@ -578,14 +610,14 @@ updInertSet is item upd_funeqs Nothing = Just item upd_funeqs (Just _already_there) = panic "updInertSet: item already there!" - in ics { inert_funeqs = CtFamHeadMap + in ics { inert_funeqs = FamHeadMap (alterTM fam_head upd_funeqs $ - (unCtFamHeadMap $ inert_funeqs ics)) } + (unFamHeadMap $ inert_funeqs ics)) } | otherwise = pprPanic "upd_inert set: can't happen! Inserting " $ ppr item -updInertSetTcS :: AtomicInert -> TcS () +updInertSetTcS :: Ct -> TcS () -- Add a new item in the inerts of the monad updInertSetTcS item = do { traceTcS "updInertSetTcs {" $ @@ -596,6 +628,32 @@ updInertSetTcS item ; traceTcS "updInertSetTcs }" $ empty } +addToSolved :: CtEvidence -> TcS () +-- Add a new item in the solved set of the monad +addToSolved item + | isIPPred (ctEvPred item) -- Never cache "solved" implicit parameters (not sure why!) + = return () + | otherwise + = do { traceTcS "updSolvedSetTcs {" $ + text "Trying to insert new solved item:" <+> ppr item + + ; modifyInertTcS (\is -> ((), updSolvedSet is item)) + + ; traceTcS "updSolvedSetTcs }" $ empty } + +addSolvedFunEq :: CtEvidence -> TcS () +addSolvedFunEq fun_eq + = modifyInertTcS $ \inert -> ((), upd_inert inert) + where + upd_inert inert + = let slvd = unFamHeadMap (inert_solved_funeqs inert) + in inert { inert_solved_funeqs = + FamHeadMap (alterTM key upd_funeqs slvd) } + upd_funeqs Nothing = Just fun_eq + upd_funeqs (Just _ct) = Just fun_eq + -- Or _ct? depends on which caches more steps of computation + key = ctEvPred fun_eq + modifyInertTcS :: (InertSet -> (a,InertSet)) -> TcS a -- Modify the inert set with the supplied function modifyInertTcS upd @@ -606,20 +664,10 @@ modifyInertTcS upd ; return a } -addToSolved :: Ct -> TcS () --- Don't do any caching for IP preds because of delicate shadowing -addToSolved ct - | isIPPred (ctPred ct) - = return () - | otherwise - = ASSERT ( isSolved (cc_flavor ct) ) - updInertSetTcS ct - extractUnsolvedTcS :: TcS (Cts,Cts) -- Extracts frozen errors and remaining unsolved and sets the -- inert set to be the remaining! -extractUnsolvedTcS = - modifyInertTcS extractUnsolved +extractUnsolvedTcS = modifyInertTcS extractUnsolved extractUnsolved :: InertSet -> ((Cts,Cts), InertSet) -- Postcondition @@ -660,22 +708,20 @@ extractUnsolved (IS { inert_cans = IC { inert_eqs = eqs -- At some point, I used to flush all the solved, in -- fear of evidence loops. But I think we are safe, -- flushing is why T3064 had become slower - , inert_solved = solved -- CtPredMap emptyTM - , inert_flat_cache = flat_cache -- CtFamHeadMap emptyTM - , inert_solved_funeqs = funeq_cache -- CtFamHeadMap emptyTM + , inert_solved = solved -- PredMap emptyTM + , inert_flat_cache = flat_cache -- FamHeadMap emptyTM + , inert_solved_funeqs = funeq_cache -- FamHeadMap emptyTM } in ((frozen, unsolved), is_solved) - where solved_eqs = filterVarEnv_Directly (\_ ct -> isGivenOrSolvedCt ct) eqs + where solved_eqs = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs unsolved_eqs = foldVarEnv (\ct cts -> cts `extendCts` ct) emptyCts $ eqs `minusVarEnv` solved_eqs - (unsolved_irreds, solved_irreds) = Bag.partitionBag (not.isGivenOrSolvedCt) irreds + (unsolved_irreds, solved_irreds) = Bag.partitionBag (not.isGivenCt) irreds (unsolved_ips, solved_ips) = extractUnsolvedCMap ips (unsolved_dicts, solved_dicts) = extractUnsolvedCMap dicts - - (unsolved_funeqs, solved_funeqs) = - partCtFamHeadMap (not . isGivenOrSolved . cc_flavor) funeqs + (unsolved_funeqs, solved_funeqs) = partCtFamHeadMap (not . isGivenCt) funeqs unsolved = unsolved_eqs `unionBags` unsolved_irreds `unionBags` unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs @@ -697,7 +743,7 @@ extractRelevantInerts wi in (cts, ics { inert_dicts = dict_map }) extract_ics_relevants ct@(CFunEqCan {}) ics = let (cts,feqs_map) = - let funeq_map = unCtFamHeadMap $ inert_funeqs ics + let funeq_map = unFamHeadMap $ inert_funeqs ics fam_head = mkTyConApp (cc_fun ct) (cc_tyargs ct) lkp = lookupTM fam_head funeq_map new_funeq_map = alterTM fam_head xtm funeq_map @@ -706,7 +752,7 @@ extractRelevantInerts wi in case lkp of Nothing -> (emptyCts, funeq_map) Just ct -> (singleCt ct, new_funeq_map) - in (cts, ics { inert_funeqs = CtFamHeadMap feqs_map }) + in (cts, ics { inert_funeqs = FamHeadMap feqs_map }) extract_ics_relevants (CIPCan { cc_ip_nm = nm } ) ics = let (cts, ips_map) = getRelevantCts nm (inert_ips ics) in (cts, ics { inert_ips = ips_map }) @@ -716,36 +762,40 @@ extractRelevantInerts wi extract_ics_relevants _ ics = (emptyCts,ics) -lookupInInerts :: InertSet -> TcPredType -> Maybe Ct +lookupInInerts :: InertSet -> TcPredType -> Maybe CtEvidence -- Is this exact predicate type cached in the solved or canonicals of the InertSet lookupInInerts (IS { inert_solved = solved, inert_cans = ics }) pty = case lookupInSolved solved pty of - Just ct -> return ct - Nothing -> lookupInInertCans ics pty + Just ctev -> return ctev + Nothing -> lookupInInertCans ics pty -lookupInSolved :: CtPredMap -> TcPredType -> Maybe Ct +lookupInSolved :: PredMap CtEvidence -> TcPredType -> Maybe CtEvidence -- Returns just if exactly this predicate type exists in the solved. -lookupInSolved tm pty = lookupTM pty $ unCtPredMap tm +lookupInSolved tm pty = lookupTM pty $ unPredMap tm -lookupInInertCans :: InertCans -> TcPredType -> Maybe Ct +lookupInInertCans :: InertCans -> TcPredType -> Maybe CtEvidence -- Returns Just if exactly this pred type exists in the inert canonicals lookupInInertCans ics pty - = lkp_ics (classifyPredType pty) - where lkp_ics (ClassPred cls _) - = lookupCCanMap cls (\ct -> ctPred ct `eqType` pty) (inert_dicts ics) - lkp_ics (EqPred ty1 _ty2) - | Just tv <- getTyVar_maybe ty1 - , Just ct <- lookupVarEnv (inert_eqs ics) tv - , ctPred ct `eqType` pty - = Just ct - lkp_ics (EqPred ty1 _ty2) -- Family equation - | Just _ <- splitTyConApp_maybe ty1 - , Just ct <- lookupTM ty1 (unCtFamHeadMap $ inert_funeqs ics) - , ctPred ct `eqType` pty - = Just ct - lkp_ics (IrredPred {}) - = find (\ct -> ctPred ct `eqType` pty) (bagToList (inert_irreds ics)) - lkp_ics _ = Nothing -- NB: No caching for IPs + = case (classifyPredType pty) of + ClassPred cls _ + -> lookupCCanMap cls (\ct -> ctEvPred ct `eqType` pty) (inert_dicts ics) + + EqPred ty1 _ty2 + | Just tv <- getTyVar_maybe ty1 -- Tyvar equation + , Just ct <- lookupVarEnv (inert_eqs ics) tv + , let ctev = ctEvidence ct + , ctEvPred ctev `eqType` pty + -> Just ctev + + | Just _ <- splitTyConApp_maybe ty1 -- Family equation + , Just ct <- lookupTM ty1 (unFamHeadMap $ inert_funeqs ics) + , let ctev = ctEvidence ct + , ctEvPred ctev `eqType` pty + -> Just ctev + + IrredPred {} -> findEvidence (\ct -> ctEvPred ct `eqType` pty) (inert_irreds ics) + + _other -> Nothing -- NB: No caching for IPs \end{code} @@ -1038,13 +1088,13 @@ emitTcSImplication :: Implication -> TcS () emitTcSImplication imp = updTcSImplics (consBag imp) -emitFrozenError :: CtFlavor -> SubGoalDepth -> TcS () +emitFrozenError :: CtEvidence -> SubGoalDepth -> TcS () -- Emits a non-canonical constraint that will stand for a frozen error in the inerts. emitFrozenError fl depth - = do { traceTcS "Emit frozen error" (ppr (ctFlavPred fl)) + = do { traceTcS "Emit frozen error" (ppr (ctEvPred fl)) ; inert_ref <- getTcSInertsRef ; inerts <- wrapTcS (TcM.readTcRef inert_ref) - ; let ct = CNonCanonical { cc_flavor = fl + ; let ct = CNonCanonical { cc_ev = fl , cc_depth = depth } inerts_new = inerts { inert_frozen = extendCts (inert_frozen inerts) ct } ; wrapTcS (TcM.writeTcRef inert_ref inerts_new) } @@ -1059,24 +1109,23 @@ getTcEvBinds :: TcS EvBindsVar getTcEvBinds = TcS (return . tcs_ev_binds) getFlatCache :: TcS CtTypeMap -getFlatCache = getTcSInerts >>= (return . unCtFamHeadMap . inert_flat_cache) +getFlatCache = getTcSInerts >>= (return . unFamHeadMap . inert_flat_cache) updFlatCache :: Ct -> TcS () -- Pre: constraint is a flat family equation (equal to a flatten skolem) -updFlatCache flat_eq@(CFunEqCan { cc_flavor = fl, cc_fun = tc, cc_tyargs = xis }) +updFlatCache flat_eq@(CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = xis }) = modifyInertTcS upd_inert_cache - where upd_inert_cache is = ((), is { inert_flat_cache = CtFamHeadMap new_fc }) + where upd_inert_cache is = ((), is { inert_flat_cache = FamHeadMap new_fc }) where new_fc = alterTM pred_key upd_cache fc - fc = unCtFamHeadMap $ inert_flat_cache is + fc = unFamHeadMap $ inert_flat_cache is pred_key = mkTyConApp tc xis - upd_cache (Just ct) | cc_flavor ct `canSolve` fl = Just ct + upd_cache (Just ct) | cc_ev ct `canSolve` fl = Just ct upd_cache (Just _ct) = Just flat_eq upd_cache Nothing = Just flat_eq updFlatCache other_ct = pprPanic "updFlatCache: non-family constraint" $ ppr other_ct - getUntouchables :: TcS TcsUntouchables getUntouchables = TcS (return . tcs_untch) @@ -1296,142 +1345,176 @@ instFlexiTcSHelper tvname tvkind -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ data XEvTerm = - XEvTerm { ev_comp :: [EvVar] -> EvTerm + XEvTerm { ev_comp :: [EvTerm] -> EvTerm -- How to compose evidence - , ev_decomp :: EvVar -> [EvTerm] + , ev_decomp :: EvTerm -> [EvTerm] -- How to decompose evidence } -data MaybeNew a = Fresh { mn_thing :: a } - | Cached { mn_thing :: a } +data MaybeNew = Fresh CtEvidence | Cached EvTerm -isFresh :: MaybeNew a -> Bool +isFresh :: MaybeNew -> Bool isFresh (Fresh {}) = True isFresh _ = False +getEvTerm :: MaybeNew -> EvTerm +getEvTerm (Fresh ctev) = ctEvTerm ctev +getEvTerm (Cached tm) = tm + +getEvTerms :: [MaybeNew] -> [EvTerm] +getEvTerms = map getEvTerm + +freshGoals :: [MaybeNew] -> [CtEvidence] +freshGoals mns = [ ctev | Fresh ctev <- mns ] + setEvBind :: EvVar -> EvTerm -> TcS () -setEvBind ev t +setEvBind the_ev t = do { tc_evbinds <- getTcEvBinds - ; wrapTcS $ TcM.addTcEvBind tc_evbinds ev t + ; wrapTcS $ TcM.addTcEvBind tc_evbinds the_ev t - ; traceTcS "setEvBind" $ vcat [ text "ev =" <+> ppr ev + ; traceTcS "setEvBind" $ vcat [ text "ev =" <+> ppr the_ev , text "t =" <+> ppr t ] #ifndef DEBUG ; return () } #else ; binds <- getTcEvBindsMap - ; let cycle = any (reaches binds) (evVarsOfTerm t) + ; let cycle = reaches_tm binds t ; when cycle (fail_if_co_loop binds) } where fail_if_co_loop binds - = do { traceTcS "Cycle in evidence binds" $ vcat [ text "evvar =" <+> ppr ev + = do { traceTcS "Cycle in evidence binds" $ vcat [ text "evvar =" <+> ppr the_ev , ppr (evBindMapBinds binds) ] - ; when (isEqVar ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!")) } + ; when (isEqVar the_ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!")) } + + reaches_tm :: EvBindMap -> EvTerm -> Bool + -- Does any free variable of 'tm' reach 'the_ev' + reaches_tm ebm tm = foldVarSet ((||) . reaches ebm) False (evVarsOfTerm tm) reaches :: EvBindMap -> Var -> Bool - -- Does this evvar reach ev? - reaches ebm ev0 = go ev0 - where go ev0 - | ev0 == ev = True - | Just (EvBind _ evtrm) <- lookupEvBind ebm ev0 - = any go (evVarsOfTerm evtrm) - | otherwise = False + -- Does this evvar reach the_ev? + reaches ebm ev + | ev == the_ev = True + | Just (EvBind _ evtrm) <- lookupEvBind ebm ev = reaches_tm ebm evtrm + | otherwise = False #endif -newGivenEvVar :: TcPredType -> EvTerm -> TcS (MaybeNew EvVar) -newGivenEvVar pty evterm - = do { is <- getTcSInerts - ; case lookupInInerts is pty of - Just ct | isGivenOrSolvedCt ct - -> return (Cached (ctId ct)) - _ -> do { new_ev <- wrapTcS $ TcM.newEvVar pty - ; setEvBind new_ev evterm - ; return (Fresh new_ev) } } - -newWantedEvVar :: TcPredType -> TcS (MaybeNew EvVar) -newWantedEvVar pty +newWantedEvVar :: WantedLoc -> TcPredType -> TcS MaybeNew +newWantedEvVar loc pty = do { is <- getTcSInerts ; case lookupInInerts is pty of - Just ct | not (isDerivedCt ct) - -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ct - ; return (Cached (ctId ct)) } + 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 - ; return (Fresh new_ev) } } - -newDerived :: TcPredType -> TcS (MaybeNew TcPredType) -newDerived pty + ; let ctev = Wanted { ctev_wloc = loc + , ctev_pred = pty + , ctev_evar = new_ev } + ; return (Fresh ctev) } } + +newDerived :: WantedLoc -> TcPredType -> TcS (Maybe CtEvidence) +-- Returns Nothing if cached, +-- Just pred if not cached +newDerived loc pty = do { is <- getTcSInerts ; case lookupInInerts is pty of - Just {} -> return (Cached pty) - _ -> return (Fresh pty) } + Just {} -> return Nothing + _ -> return (Just Derived { ctev_wloc = loc + , ctev_pred = pty }) } -newKindConstraint :: TcTyVar -> Kind -> TcS (MaybeNew EvVar) +newKindConstraint :: WantedLoc -> TcTyVar -> Kind -> TcS MaybeNew -- Create new wanted CoVar that constrains the type to have the specified kind. -newKindConstraint tv knd +newKindConstraint loc tv knd = do { ty_k <- wrapTcS (instFlexiTcSHelper (tyVarName tv) knd) - ; newWantedEvVar (mkTcEqPred (mkTyVarTy tv) ty_k) } - -instDFunConstraints :: TcThetaType -> TcS [MaybeNew EvVar] -instDFunConstraints = mapM newWantedEvVar + ; newWantedEvVar loc (mkTcEqPred (mkTyVarTy tv) ty_k) } +instDFunConstraints :: WantedLoc -> TcThetaType -> TcS [MaybeNew] +instDFunConstraints wl = mapM (newWantedEvVar wl) +\end{code} -xCtFlavor :: CtFlavor -- Original flavor + +Note [xCFlavor] +~~~~~~~~~~~~~~~ +A call might look like this: + + xCtFlavor ev subgoal-preds evidence-transformer + + ev is Given => use ev_decomp to create new Givens for subgoal-preds, + and return them + + ev is Wanted => create new wanteds for subgoal-preds, + use ev_comp to bind ev, + return fresh wanteds (ie ones not cached in inert_cans or solved) + + ev is Derived => create new deriveds for subgoal-preds + (unless cached in inert_cans or solved) + +Note: The [CtEvidence] returned is a subset of the subgoal-preds passed in + Ones that are already cached are not returned + +Example + ev : Tree a b ~ Tree c d + xCtFlavor ev [a~c, b~d] (XEvTerm { ev_comp = \[c1 c2]. c1 c2 + , ev_decomp = \c. [nth 1 c, nth 2 c] }) + (\fresh-goals. stuff) + +\begin{code} +xCtFlavor :: CtEvidence -- Original flavor -> [TcPredType] -- New predicate types -> XEvTerm -- Instructions about how to manipulate evidence - -> ([CtFlavor] -> TcS a) -- What to do with any remaining /fresh/ goals! - -> TcS a + -> TcS [CtEvidence] xCtFlavor = xCtFlavor_cache True - xCtFlavor_cache :: Bool -- True = if wanted add to the solved bag! - -> CtFlavor -- Original flavor + -> CtEvidence -- Original flavor -> [TcPredType] -- New predicate types -> XEvTerm -- Instructions about how to manipulate evidence - -> ([CtFlavor] -> TcS a) -- What to do with any remaining /fresh/ goals! - -> TcS a -xCtFlavor_cache _ (Given { flav_gloc = gl, flav_evar = evar }) ptys xev cont_with - = do { let ev_trms = ev_decomp xev evar - ; new_evars <- zipWithM newGivenEvVar ptys ev_trms - ; cont_with $ - map (\x -> Given gl (mn_thing x)) (filter isFresh new_evars) } + -> TcS [CtEvidence] +xCtFlavor_cache _ (Given { ctev_gloc = gl, ctev_evtm = tm }) ptys xev + = return [ Given { ctev_gloc = gl, ctev_pred = pred, ctev_evtm = sub_tm } + | (pred, sub_tm) <- zipEqual "xCtFlavor" ptys (ev_decomp xev tm) ] + -- ToDo: consider creating new evidence variables for superclasses -xCtFlavor_cache cache (Wanted { flav_wloc = wl, flav_evar = evar }) ptys xev cont_with - = do { new_evars <- mapM newWantedEvVar ptys - ; let evars = map mn_thing new_evars - evterm = ev_comp xev evars - ; setEvBind evar evterm - ; let solved_flav = Solved { flav_gloc = mkSolvedLoc wl UnkSkol - , flav_evar = evar } - ; when cache $ addToSolved (mkNonCanonical solved_flav) - ; cont_with $ - map (\x -> Wanted wl (mn_thing x)) (filter isFresh new_evars) } - -xCtFlavor_cache _ (Derived { flav_wloc = wl }) ptys _xev cont_with - = do { ders <- mapM newDerived ptys - ; cont_with $ - map (\x -> Derived wl (mn_thing x)) (filter isFresh ders) } +xCtFlavor_cache cache ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar }) ptys xev + = do { new_evars <- mapM (newWantedEvVar wl) ptys + ; setEvBind evar (ev_comp xev (getEvTerms new_evars)) + + -- Add the now-solved wanted constraint to the cache + ; when cache $ addToSolved ctev + + ; return (freshGoals new_evars) } - -- I am not sure I actually want to do this (e.g. from recanonicalizing a solved?) - -- but if we plan to use xCtFlavor for rewriting as well then I might as well add a case -xCtFlavor_cache _ (Solved { flav_gloc = gl, flav_evar = evar }) ptys xev cont_with - = do { let ev_trms = ev_decomp xev evar - ; new_evars <- zipWithM newGivenEvVar ptys ev_trms - ; cont_with $ - map (\x -> Solved gl (mn_thing x)) (filter isFresh new_evars) } - -rewriteCtFlavor :: CtFlavor +xCtFlavor_cache _ (Derived { ctev_wloc = wl }) ptys _xev + = do { ders <- mapM (newDerived wl) ptys + ; return (catMaybes ders) } + +----------------------------- +rewriteCtFlavor :: CtEvidence -> TcPredType -- new predicate -> TcCoercion -- new ~ old - -> TcS (Maybe CtFlavor) --- rewriteCtFlavor old_fl new_pred co --- Main purpose: create a new identity (flavor) for new_pred; --- unless new_pred is cached already --- * Returns a new_fl : new_pred, with same wanted/given/derived flag as old_fl --- * If old_fl was wanted, create a binding for old_fl, in terms of new_fl --- * If old_fl was given, AND not cached, create a binding for new_fl, in terms of old_fl --- * Returns Nothing if new_fl is already cached + -> TcS (Maybe CtEvidence) +{- + rewriteCtFlavor old_fl new_pred co +Main purpose: create a new identity (flavor) for new_pred; + unless new_pred is cached already +* Returns a new_fl : new_pred, with same wanted/given/derived flag as old_fl +* If old_fl was wanted, create a binding for old_fl, in terms of new_fl +* If old_fl was given, AND not cached, create a binding for new_fl, in terms of old_fl +* Returns Nothing if new_fl is already cached + + + Old evidence New predicate is Return new evidence + flavour of same flavor + ------------------------------------------------------------------- + Wanted Already solved or in inert Nothing + or Derived Not Just new_evidence + + Given Already in inert Nothing + Not Just new_evidence + + Solved NEVER HAPPENS +-} rewriteCtFlavor = rewriteCtFlavor_cache True -- Returns Just new_fl iff either (i) 'co' is reflexivity @@ -1439,40 +1522,40 @@ rewriteCtFlavor = rewriteCtFlavor_cache True -- In either case, there is nothing new to do with new_fl rewriteCtFlavor_cache :: Bool - -> CtFlavor + -> CtEvidence -> TcPredType -- new predicate -> TcCoercion -- new ~ old - -> TcS (Maybe CtFlavor) + -> TcS (Maybe CtEvidence) -- If derived, don't even look at the coercion -- NB: this allows us to sneak away with ``error'' thunks for -- coercions that come from derived ids (which don't exist!) -rewriteCtFlavor_cache _cache (Derived wl _pty_orig) pty_new _co - = newDerived pty_new >>= from_mn - where from_mn (Cached {}) = return Nothing - from_mn (Fresh {}) = return $ Just (Derived wl pty_new) +rewriteCtFlavor_cache _cache (Derived { ctev_wloc = wl }) pty_new _co + = newDerived wl pty_new -rewriteCtFlavor_cache cache fl pty co - | isTcReflCo co - -- If just reflexivity then you may re-use the same variable as optimization - = if ctFlavPred fl `eqType` pty then - -- E.g. for type synonyms we want to use the original type - -- since it's not flattened to report better error messages. - return $ Just fl - else - -- E.g. because we rewrite with a spontaneously solved one - return (Just $ case fl of - Derived wl _pty_orig -> Derived wl pty - Given gl ev -> Given gl (setVarType ev pty) - Wanted wl ev -> Wanted wl (setVarType ev pty) - Solved gl ev -> Solved gl (setVarType ev pty)) - | otherwise - = xCtFlavor_cache cache fl [pty] (XEvTerm ev_comp ev_decomp) cont - where ev_comp [x] = mkEvCast x co - ev_comp _ = panic "Coercion can only have one subgoal" - ev_decomp x = [mkEvCast x (mkTcSymCo co)] - cont [] = return Nothing - cont [fl] = return $ Just fl - cont _ = panic "At most one constraint can be subgoal of coercion!" +rewriteCtFlavor_cache _cache (Given { ctev_gloc = gl, ctev_evtm = old_tm }) pty_new co + = return (Just (Given { ctev_gloc = gl, ctev_pred = pty_new, ctev_evtm = new_tm })) + where + new_tm = mkEvCast old_tm (mkTcSymCo co) -- mkEvCase optimises ReflCo + +rewriteCtFlavor_cache cache ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar, ctev_pred = pty_old }) pty_new co + | isTcReflCo co -- If just reflexivity then you may re-use the same variable + = return (Just (if pty_old `eqType` pty_new + then ctev + else ctev { ctev_pred = pty_new })) + -- If the old and new types compare equal (eqType looks through synonyms) + -- then retain the old type, so that error messages come out mentioning synonyms + + | otherwise + = do { new_evar <- newWantedEvVar wl pty_new + ; setEvBind evar (mkEvCast (getEvTerm new_evar) co) + + -- Add the now-solved wanted constraint to the cache + ; when cache $ addToSolved ctev + + ; case new_evar of + Fresh ctev -> return (Just ctev) + _ -> return Nothing } + -- Matching and looking up classes and family instances @@ -1537,29 +1620,29 @@ deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2) phi1 = Type.substTy subst1 body1 phi2 = Type.substTy (zipTopTvSubst tvs2 tys) body2 skol_info = UnifyForAllSkol skol_tvs phi1 - ; mev <- newWantedEvVar (mkTcEqPred phi1 phi2) - ; let new_fl = Wanted loc (mn_thing mev) - new_ct = mkNonCanonical new_fl - new_co = mkTcCoVarCo (mn_thing mev) - ; coe_inside <- if isFresh mev then - do { ev_binds_var <- wrapTcS $ TcM.newTcEvBinds - ; let ev_binds = TcEvBinds ev_binds_var - ; lcl_env <- wrapTcS $ TcM.getLclTypeEnv - ; loc <- wrapTcS $ TcM.getCtLoc skol_info - ; let wc = WC { wc_flat = singleCt new_ct - , wc_impl = emptyBag - , wc_insol = emptyCts } - imp = Implic { ic_untch = all_untouchables - , ic_env = lcl_env - , ic_skols = skol_tvs - , ic_given = [] - , ic_wanted = wc - , ic_insol = False - , ic_binds = ev_binds_var - , ic_loc = loc } - ; updTcSImplics (consBag imp) - ; return (TcLetCo ev_binds new_co) } - else (return new_co) + ; mev <- newWantedEvVar loc (mkTcEqPred phi1 phi2) + ; coe_inside <- case mev of + Cached ev_tm -> return (evTermCoercion ev_tm) + Fresh ctev -> do { ev_binds_var <- wrapTcS $ TcM.newTcEvBinds + ; let ev_binds = TcEvBinds ev_binds_var + new_ct = mkNonCanonical ctev + new_co = evTermCoercion (ctEvTerm ctev) + ; lcl_env <- wrapTcS $ TcM.getLclTypeEnv + ; loc <- wrapTcS $ TcM.getCtLoc skol_info + ; let wc = WC { wc_flat = singleCt new_ct + , wc_impl = emptyBag + , wc_insol = emptyCts } + imp = Implic { ic_untch = all_untouchables + , ic_env = lcl_env + , ic_skols = skol_tvs + , ic_given = [] + , ic_wanted = wc + , ic_insol = False + , ic_binds = ev_binds_var + , ic_loc = loc } + ; updTcSImplics (consBag imp) + ; return (TcLetCo ev_binds new_co) } + ; setEvBind orig_ev $ EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs) } @@ -1573,7 +1656,6 @@ deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2) -- Rewriting with respect to the inert equalities -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \begin{code} - getInertEqs :: TcS (TyVarEnv Ct, InScopeSet) getInertEqs = do { inert <- getTcSInerts ; let ics = inert_cans inert @@ -1581,11 +1663,14 @@ getInertEqs = do { inert <- getTcSInerts getCtCoercion :: EvBindMap -> Ct -> TcCoercion -- Precondition: A CTyEqCan which is either Wanted or Given, never Derived or Solved! -getCtCoercion bs ct +getCtCoercion _bs ct + = ASSERT( not (isDerivedCt ct) ) + evTermCoercion (ctEvTerm (ctEvidence ct)) +{- ToDo: check with Dimitrios that we can dump this stuff = case lookupEvBind bs cc_id of -- Given and bound to a coercion term Just (EvBind _ (EvCoercion co)) -> co - -- NB: The constraint could have been rewritten due to spontaneous + -- NB: The constraint could have been rewritten due to spontaneous -- unifications but because we are optimizing away mkRefls the evidence -- variable may still have type (alpha ~ [beta]). The constraint may -- however have a more accurate type (alpha ~ [Int]) (where beta ~ Int has @@ -1596,6 +1681,9 @@ getCtCoercion bs ct _ -> mkTcCoVarCo (setVarType cc_id (ctPred ct)) - where cc_id = ctId ct - + where + cc_id = ctId ct +-} \end{code} + + diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index e6a4fd2f79..f97347a305 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -558,7 +558,7 @@ simplifyRule name lhs_wanted rhs_wanted -- variables; hence NoUntouchables ; (resid_wanted, _) <- runTcS (SimplInfer doc) untch emptyInert emptyWorkList $ - solveWanteds zonked_all + solveWanteds zonked_all ; zonked_lhs <- zonkWC lhs_wanted @@ -579,7 +579,8 @@ simplifyRule name lhs_wanted rhs_wanted vcat [ text "zonked_lhs" <+> ppr zonked_lhs , text "q_cts" <+> ppr q_cts ] - ; return (map ctId (bagToList q_cts), zonked_lhs { wc_flat = non_q_cts }) } + ; return ( map (ctEvId . ctEvidence) (bagToList q_cts) + , zonked_lhs { wc_flat = non_q_cts }) } \end{code} @@ -784,10 +785,11 @@ solveNestedImplications implics where givens_from_wanteds = foldrBag get_wanted [] get_wanted cc rest_givens | pushable_wanted cc - = let fl = cc_flavor cc - wloc = flav_wloc fl - gfl = Given (mkGivenLoc wloc UnkSkol) (flav_evar fl) - this_given = cc { cc_flavor = gfl } + = let fl = ctEvidence cc + gfl = Given { ctev_gloc = setCtLocOrigin (ctev_wloc fl) UnkSkol + , ctev_evtm = EvId (ctev_evar fl) + , ctev_pred = ctev_pred fl } + this_given = cc { cc_ev = gfl } in this_given : rest_givens | otherwise = rest_givens @@ -1025,20 +1027,20 @@ solveCTyFunEqs cts ; return (niFixTvSubst ni_subst, unsolved_can_cts) } where - solve_one (Wanted _ cv,tv,ty) + solve_one (Wanted { ctev_evar = cv }, tv, ty) = setWantedTyBind tv ty >> setEvBind cv (EvCoercion (mkTcReflCo ty)) solve_one (Derived {}, tv, ty) = setWantedTyBind tv ty solve_one arg = pprPanic "solveCTyFunEqs: can't solve a /given/ family equation!" $ ppr arg ------------ -type FunEqBinds = (TvSubstEnv, [(CtFlavor, TcTyVar, TcType)]) +type FunEqBinds = (TvSubstEnv, [(CtEvidence, TcTyVar, TcType)]) -- The TvSubstEnv is not idempotent, but is loop-free -- See Note [Non-idempotent substitution] in Unify emptyFunEqBinds :: FunEqBinds emptyFunEqBinds = (emptyVarEnv, []) -extendFunEqBinds :: FunEqBinds -> CtFlavor -> TcTyVar -> TcType -> FunEqBinds +extendFunEqBinds :: FunEqBinds -> CtEvidence -> TcTyVar -> TcType -> FunEqBinds extendFunEqBinds (tv_subst, cv_binds) fl tv ty = (extendVarEnv tv_subst tv ty, (fl, tv, ty):cv_binds) @@ -1052,7 +1054,7 @@ getSolvableCTyFunEqs untch cts dflt_funeq :: (Cts, FunEqBinds) -> Ct -> (Cts, FunEqBinds) dflt_funeq (cts_in, feb@(tv_subst, _)) - (CFunEqCan { cc_flavor = fl + (CFunEqCan { cc_ev = fl , cc_fun = tc , cc_tyargs = xis , cc_rhs = xi }) @@ -1071,7 +1073,7 @@ getSolvableCTyFunEqs untch cts , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis)) -- Occurs check: see Note [Solving Family Equations], Point 2 - = ASSERT ( not (isGivenOrSolved fl) ) + = ASSERT ( not (isGiven fl) ) (cts_in, extendFunEqBinds feb fl tv (mkTyConApp tc xis)) dflt_funeq (cts_in, fun_eq_binds) ct @@ -1210,16 +1212,16 @@ defaultTyVar untch the_tv , not (k `eqKind` default_k) = tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting] do { let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk - ; eqv <- TcSMonad.newKindConstraint the_tv default_k + ; eqv <- TcSMonad.newKindConstraint loc the_tv default_k ; case eqv of Fresh x -> return $ unitBag $ - CNonCanonical { cc_flavor = Wanted loc x, cc_depth = 0 } + CNonCanonical { cc_ev = x, cc_depth = 0 } Cached _ -> return emptyBag } {- DELETEME if isNewEvVar eqv then return $ unitBag (CNonCanonical { cc_id = evc_the_evvar eqv - , cc_flavor = fl, cc_depth = 0 }) + , cc_ev = fl, cc_depth = 0 }) else return emptyBag } -} @@ -1300,13 +1302,12 @@ disambigGroup (default_ty:default_tys) group ; success <- tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting] do { derived_eq <- tryTcS $ -- I need a new tryTcS because we will call solveInteractCts below! - do { md <- newDerived (mkTcEqPred (mkTyVarTy the_tv) default_ty) + do { md <- newDerived (ctev_wloc the_fl) + (mkTcEqPred (mkTyVarTy the_tv) default_ty) + -- ctev_wloc because constraint is not Given! ; case md of - Cached _ -> return [] - Fresh pty -> - -- flav_wloc because constraint is not Given/Solved! - let dfl = Derived (flav_wloc the_fl) pty - in return [ CNonCanonical { cc_flavor = dfl, cc_depth = 0 } ] } + Nothing -> return [] + Just ctev -> return [ mkNonCanonical ctev ] } ; traceTcS "disambigGroup (solving) {" (text "trying to solve constraints along with default equations ...") @@ -1335,7 +1336,7 @@ disambigGroup (default_ty:default_tys) group ; disambigGroup default_tys group } } where ((the_ct,the_tv):_) = group - the_fl = cc_flavor the_ct + the_fl = cc_ev the_ct wanteds = map fst group \end{code} @@ -1365,9 +1366,12 @@ newFlatWanteds :: CtOrigin -> ThetaType -> TcM [Ct] newFlatWanteds orig theta = do { loc <- getCtLoc orig ; mapM (inst_to_wanted loc) theta } - where inst_to_wanted loc pty + where + inst_to_wanted loc pty = do { v <- TcMType.newWantedEvVar pty ; return $ - CNonCanonical { cc_flavor = Wanted loc v + CNonCanonical { cc_ev = Wanted { ctev_evar = v + , ctev_wloc = loc + , ctev_pred = pty } , cc_depth = 0 } } \end{code} diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 0b2429842d..c44ce31f2e 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -533,7 +533,9 @@ uType_defer items ty1 ty2 = ASSERT( not (null items) ) do { eqv <- newEq ty1 ty2 ; loc <- getCtLoc (TypeEqOrigin (last items)) - ; emitFlat $ mkNonCanonical (Wanted loc eqv) + ; let ctev = Wanted { ctev_wloc = loc, ctev_evar = eqv + , ctev_pred = mkTcEqPred ty1 ty2 } + ; emitFlat $ mkNonCanonical ctev -- Error trace only -- NB. do *not* call mkErrInfo unless tracing is on, because diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index 1360baca6b..42e54ba47b 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -30,7 +30,7 @@ module Coercion ( -- ** Constructing coercions mkReflCo, mkCoVarCo, mkAxInstCo, mkAxInstRHS, - mkPiCo, mkPiCos, + mkPiCo, mkPiCos, mkCoCast, mkSymCo, mkTransCo, mkNthCo, mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo, mkForAllCo, mkUnsafeCo, @@ -672,6 +672,18 @@ mkPiCos vs co = foldr mkPiCo co vs mkPiCo :: Var -> Coercion -> Coercion mkPiCo v co | isTyVar v = mkForAllCo v co | otherwise = mkFunCo (mkReflCo (varType v)) co + +mkCoCast :: Coercion -> Coercion -> Coercion +-- (mkCoCast (c :: s1 ~# t1) (g :: (s1 ~# t1) ~# (s2 ~# t2) +mkCoCast c g + = mkSymCo g1 `mkTransCo` c `mkTransCo` g2 + where + -- g :: (s1 ~# s2) ~# (t1 ~# t2) + -- g1 :: s1 ~# t1 + -- g2 :: s2 ~# t2 + [_reflk, g1, g2] = decomposeCo 3 g + -- Remember, (~#) :: forall k. k -> k -> * + -- so it takes *three* arguments, not two \end{code} %************************************************************************ diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs index e0de629da6..f81aebbfcd 100644 --- a/compiler/types/Type.lhs +++ b/compiler/types/Type.lhs @@ -973,14 +973,17 @@ getClassPredTys_maybe ty = case splitTyConApp_maybe ty of _ -> Nothing getEqPredTys :: PredType -> (Type, Type) -getEqPredTys ty = case getEqPredTys_maybe ty of - Just (ty1, ty2) -> (ty1, ty2) - Nothing -> pprPanic "getEqPredTys" (ppr ty) +getEqPredTys ty + = case splitTyConApp_maybe ty of + Just (tc, (_ : ty1 : ty2 : tys)) -> ASSERT( tc `hasKey` eqTyConKey && null tys ) + (ty1, ty2) + _ -> pprPanic "getEqPredTys" (ppr ty) getEqPredTys_maybe :: PredType -> Maybe (Type, Type) -getEqPredTys_maybe ty = case splitTyConApp_maybe ty of - Just (tc, [_, ty1, ty2]) | tc `hasKey` eqTyConKey -> Just (ty1, ty2) - _ -> Nothing +getEqPredTys_maybe ty + = case splitTyConApp_maybe ty of + Just (tc, [_, ty1, ty2]) | tc `hasKey` eqTyConKey -> Just (ty1, ty2) + _ -> Nothing getIPPredTy_maybe :: PredType -> Maybe (IPName Name, Type) getIPPredTy_maybe ty = case splitTyConApp_maybe ty of -- GitLab