\begin{code}
module TcCanonical(
- mkCanonical, mkCanonicals, mkCanonicalFEV, canWanteds, canGivens,
- canOccursCheck, canEq
+ mkCanonical, mkCanonicals, mkCanonicalFEV, mkCanonicalFEVs, canWanteds, canGivens,
+ canOccursCheck, canEqToWorkList,
+ rewriteWithFunDeps
) where
#include "HsVersions.h"
import BasicTypes
import Type
import TcRnTypes
-
+import FunDeps
+import qualified TcMType as TcM
import TcType
import TcErrors
import Coercion
import TypeRep
import Name
import Var
+import VarEnv ( TidyEnv )
import Outputable
import Control.Monad ( unless, when, zipWithM, zipWithM_ )
import MonadUtils
import HsBinds
import TcSMonad
+import FastString
\end{code}
Note [Canonicalisation]
; return $ (mkCoVarCoercion cv, rhs_var, ct) }
else -- Derived or Wanted: make a new *unification* flatten variable
do { rhs_var <- newFlexiTcSTy (typeKind fam_ty)
- ; cv <- newWantedCoVar fam_ty rhs_var
+ ; cv <- newCoVar fam_ty rhs_var
; let ct = CFunEqCan { cc_id = cv
, cc_flavor = mkWantedFlavor fl
-- Always Wanted, not Derived
%************************************************************************
\begin{code}
-canWanteds :: [WantedEvVar] -> TcS CanonicalCts
-canWanteds = fmap andCCans . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev)
+canWanteds :: [WantedEvVar] -> TcS WorkList
+canWanteds = fmap unionWorkLists . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev)
-canGivens :: GivenLoc -> [EvVar] -> TcS CanonicalCts
+canGivens :: GivenLoc -> [EvVar] -> TcS WorkList
canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc)) givens
- ; return (andCCans ccs) }
+ ; return (unionWorkLists ccs) }
-mkCanonicals :: CtFlavor -> [EvVar] -> TcS CanonicalCts
-mkCanonicals fl vs = fmap andCCans (mapM (mkCanonical fl) vs)
+mkCanonicals :: CtFlavor -> [EvVar] -> TcS WorkList
+mkCanonicals fl vs = fmap unionWorkLists (mapM (mkCanonical fl) vs)
-mkCanonicalFEV :: FlavoredEvVar -> TcS CanonicalCts
+mkCanonicalFEV :: FlavoredEvVar -> TcS WorkList
mkCanonicalFEV (EvVarX ev fl) = mkCanonical fl ev
-mkCanonical :: CtFlavor -> EvVar -> TcS CanonicalCts
+mkCanonicalFEVs :: Bag FlavoredEvVar -> TcS WorkList
+mkCanonicalFEVs = foldrBagM canon_one emptyWorkList
+ where -- Preserves order (shouldn't be important, but curently
+ -- is important for the vectoriser)
+ canon_one fev wl = do { wl' <- mkCanonicalFEV fev
+ ; return (unionWorkList wl' wl) }
+
+mkCanonical :: CtFlavor -> EvVar -> TcS WorkList
mkCanonical fl ev = case evVarPred ev of
- ClassP clas tys -> canClass fl ev clas tys
- IParam ip ty -> canIP fl ev ip ty
- EqPred ty1 ty2 -> canEq fl ev ty1 ty2
+ ClassP clas tys -> canClassToWorkList fl ev clas tys
+ IParam ip ty -> canIPToWorkList fl ev ip ty
+ EqPred ty1 ty2 -> canEqToWorkList fl ev ty1 ty2
-canClass :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS CanonicalCts
-canClass fl v cn tys
+canClassToWorkList :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS WorkList
+canClassToWorkList fl v cn tys
= do { (xis,cos,ccs) <- flattenMany fl tys -- cos :: xis ~ tys
; let no_flattening_happened = isEmptyCCan ccs
dict_co = mkTyConCoercion (classTyCon cn) cos
-- Add the superclasses of this one here, See Note [Adding superclasses].
-- But only if we are not simplifying the LHS of a rule.
; sctx <- getTcSContext
- ; sc_cts <- if simplEqsOnly sctx then return emptyCCan
+ ; sc_cts <- if simplEqsOnly sctx then return emptyWorkList
else newSCWorkFromFlavored v_new fl cn xis
- ; return (sc_cts `andCCan` ccs `extendCCans` CDictCan { cc_id = v_new
- , cc_flavor = fl
- , cc_class = cn
- , cc_tyargs = xis }) }
+ ; return (sc_cts `unionWorkList`
+ workListFromEqs ccs `unionWorkList`
+ workListFromNonEq CDictCan { cc_id = v_new
+ , cc_flavor = fl
+ , cc_class = cn
+ , cc_tyargs = xis }) }
\end{code}
Note [Adding superclasses]
\begin{code}
-newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS CanonicalCts
+newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS WorkList
-- Returns superclasses, see Note [Adding superclasses]
newSCWorkFromFlavored ev orig_flavor cls xis
| isDerived orig_flavor
- = return emptyCCan -- Deriveds don't yield more superclasses because we will
- -- add them transitively in the case of wanteds.
+ = return emptyWorkList -- Deriveds don't yield more superclasses because we will
+ -- add them transitively in the case of wanteds.
| isGiven orig_flavor
= do { let sc_theta = immSuperClasses cls xis
; mkCanonicals flavor sc_vars }
| isEmptyVarSet (tyVarsOfTypes xis)
- = return emptyCCan -- Wanteds with no variables yield no deriveds.
- -- See Note [Improvement from Ground Wanteds]
+ = return emptyWorkList -- Wanteds with no variables yield no deriveds.
+ -- See Note [Improvement from Ground Wanteds]
| otherwise -- Wanted case, just add those SC that can lead to improvement.
= do { let sc_rec_theta = transSuperClasses cls xis
-canIP :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS CanonicalCts
+canIPToWorkList :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS WorkList
-- See Note [Canonical implicit parameter constraints] to see why we don't
-- immediately canonicalize (flatten) IP constraints.
-canIP fl v nm ty
- = return $ singleCCan $ CIPCan { cc_id = v
- , cc_flavor = fl
- , cc_ip_nm = nm
- , cc_ip_ty = ty }
+canIPToWorkList fl v nm ty
+ = return $ workListFromNonEq (CIPCan { cc_id = v
+ , cc_flavor = fl
+ , cc_ip_nm = nm
+ , cc_ip_ty = ty })
-----------------
+canEqToWorkList :: CtFlavor -> EvVar -> Type -> Type -> TcS WorkList
+canEqToWorkList fl cv ty1 ty2 = do { cts <- canEq fl cv ty1 ty2
+ ; return $ workListFromEqs cts }
+
canEq :: CtFlavor -> EvVar -> Type -> Type -> TcS CanonicalCts
canEq fl cv ty1 ty2
| tcEqType ty1 ty2 -- Dealing with equality here avoids
-- later spurious occurs checks for a~a
- = do { when (isWanted fl) (setWantedCoBind cv ty1)
+ = do { when (isWanted fl) (setCoBind cv ty1)
; return emptyCCan }
-- If one side is a variable, orient and flatten,
Just (t2a,t2b,t2c) <- splitCoPredTy_maybe s2
= do { (v1,v2,v3)
<- if isWanted fl then -- Wanted
- do { v1 <- newWantedCoVar t1a t2a
- ; v2 <- newWantedCoVar t1b t2b
- ; v3 <- newWantedCoVar t1c t2c
+ do { v1 <- newCoVar t1a t2a
+ ; v2 <- newCoVar t1b t2b
+ ; v3 <- newCoVar t1c t2c
; let res_co = mkCoPredCo (mkCoVarCoercion v1)
(mkCoVarCoercion v2) (mkCoVarCoercion v3)
- ; setWantedCoBind cv res_co
+ ; setCoBind cv res_co
; return (v1,v2,v3) }
else if isGiven fl then -- Given
let co_orig = mkCoVarCoercion cv
canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
= do { (argv, resv) <-
if isWanted fl then
- do { argv <- newWantedCoVar s1 s2
- ; resv <- newWantedCoVar t1 t2
- ; setWantedCoBind cv $
+ do { argv <- newCoVar s1 s2
+ ; resv <- newCoVar t1 t2
+ ; setCoBind cv $
mkFunCoercion (mkCoVarCoercion argv) (mkCoVarCoercion resv)
; return (argv,resv) }
canEq fl cv (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2))
| n1 == n2
= if isWanted fl then
- do { v <- newWantedCoVar t1 t2
- ; setWantedCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv)
+ do { v <- newCoVar t1 t2
+ ; setCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv)
; canEq fl v t1 t2 }
else return emptyCCan -- DV: How to decompose given IP coercions?
canEq fl cv (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2))
| c1 == c2
= if isWanted fl then
- do { vs <- zipWithM newWantedCoVar tys1 tys2
- ; setWantedCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs)
+ do { vs <- zipWithM newCoVar tys1 tys2
+ ; setCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs)
; andCCans <$> zipWith3M (canEq fl) vs tys1 tys2
}
else return emptyCCan
= -- Generate equalities for each of the corresponding arguments
do { argsv
<- if isWanted fl then
- do { argsv <- zipWithM newWantedCoVar tys1 tys2
- ; setWantedCoBind cv $
+ do { argsv <- zipWithM newCoVar tys1 tys2
+ ; setCoBind cv $
mkTyConCoercion tc1 (map mkCoVarCoercion argsv)
; return argsv }
, Just (s2,t2) <- tcSplitAppTy_maybe ty2
= do { (cv1,cv2) <-
if isWanted fl
- then do { cv1 <- newWantedCoVar s1 s2
- ; cv2 <- newWantedCoVar t1 t2
- ; setWantedCoBind cv $
+ then do { cv1 <- newCoVar s1 s2
+ ; cv2 <- newCoVar t1 t2
+ ; setCoBind cv $
mkAppCoercion (mkCoVarCoercion cv1) (mkCoVarCoercion cv2)
; return (cv1,cv2) }
= OtherCls ty
-- See note [Canonical ordering for equality constraints].
-reOrient :: TcsUntouchables -> TypeClassifier -> TypeClassifier -> Bool
+reOrient :: CtFlavor -> 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
--
-- Postcondition: After re-orienting, first arg is not OTherCls
-reOrient _untch (OtherCls {}) (FunCls {}) = True
-reOrient _untch (OtherCls {}) (FskCls {}) = True
-reOrient _untch (OtherCls {}) (VarCls {}) = True
-reOrient _untch (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun
+reOrient _fl (OtherCls {}) (FunCls {}) = True
+reOrient _fl (OtherCls {}) (FskCls {}) = True
+reOrient _fl (OtherCls {}) (VarCls {}) = True
+reOrient _fl (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun
+
+reOrient _fl (FunCls {}) (VarCls _tv) = False
+ -- But consider the following variation: isGiven fl && isMetaTyVar tv
-reOrient _untch (FunCls {}) (VarCls {}) = False
-- See Note [No touchables as FunEq RHS] in TcSMonad
-reOrient _untch (FunCls {}) _ = False -- Fun/Other on rhs
+reOrient _fl (FunCls {}) _ = False -- Fun/Other on rhs
-reOrient _untch (VarCls {}) (FunCls {}) = True
+reOrient _fl (VarCls {}) (FunCls {}) = True
-reOrient _untch (VarCls {}) (FskCls {}) = False
+reOrient _fl (VarCls {}) (FskCls {}) = False
-reOrient _untch (VarCls {}) (OtherCls {}) = False
-reOrient _untch (VarCls tv1) (VarCls tv2)
+reOrient _fl (VarCls {}) (OtherCls {}) = False
+reOrient _fl (VarCls tv1) (VarCls tv2)
| isMetaTyVar tv2 && not (isMetaTyVar tv1) = True
| otherwise = False
-- Just for efficiency, see CTyEqCan invariants
-reOrient _untch (FskCls {}) (VarCls tv2) = isMetaTyVar tv2
+reOrient _fl (FskCls {}) (VarCls tv2) = isMetaTyVar tv2
-- Just for efficiency, see CTyEqCan invariants
-reOrient _untch (FskCls {}) (FskCls {}) = False
-reOrient _untch (FskCls {}) (FunCls {}) = True
-reOrient _untch (FskCls {}) (OtherCls {}) = False
+reOrient _fl (FskCls {}) (FskCls {}) = False
+reOrient _fl (FskCls {}) (FunCls {}) = True
+reOrient _fl (FskCls {}) (OtherCls {}) = False
------------------
canEqLeaf :: TcsUntouchables
-- Preconditions:
-- * one of the two arguments is not OtherCls
-- * the two types are not equal (looking through synonyms)
-canEqLeaf untch fl cv cls1 cls2
+canEqLeaf _untch fl cv cls1 cls2
| cls1 `re_orient` cls2
= do { cv' <- if isWanted fl
- then do { cv' <- newWantedCoVar s2 s1
- ; setWantedCoBind cv $ mkSymCoercion (mkCoVarCoercion cv')
+ then do { cv' <- newCoVar s2 s1
+ ; setCoBind cv $ mkSymCoercion (mkCoVarCoercion cv')
; return cv' }
else if isGiven fl then
newGivenCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv))
= do { traceTcS "canEqLeaf" (ppr (unClassify cls1) $$ ppr (unClassify cls2))
; canEqLeafOriented fl cv cls1 s2 }
where
- re_orient = reOrient untch
+ re_orient = reOrient fl
s1 = unClassify cls1
s2 = unClassify cls2
; cv_new <- if no_flattening_happened then return cv
else if isGiven fl then return cv
else if isWanted fl then
- do { cv' <- newWantedCoVar (unClassify (FunCls fn xis1)) xi2
+ do { cv' <- newCoVar (unClassify (FunCls fn xis1)) xi2
-- cv' : F xis ~ xi2
; let -- fun_co :: F xis1 ~ F tys1
fun_co = mkTyConCoercion fn cos1
want_co = mkSymCoercion fun_co
`mkTransCoercion` mkCoVarCoercion cv'
`mkTransCoercion` co2
- ; setWantedCoBind cv want_co
+ ; setCoBind cv want_co
; return cv' }
else -- Derived
newDerivedId (EqPred (unClassify (FunCls fn xis1)) xi2)
; cv_new <- if no_flattening_happened then return cv
else if isGiven fl then return cv
else if isWanted fl then
- do { cv' <- newWantedCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2
- ; setWantedCoBind cv (mkCoVarCoercion cv' `mkTransCoercion` co)
+ do { cv' <- newCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2
+ ; setCoBind cv (mkCoVarCoercion cv' `mkTransCoercion` co)
; return cv' }
else -- Derived
newDerivedId (EqPred (mkTyVarTy tv) xi2')
itself, and so on.
+%************************************************************************
+%* *
+%* Functional dependencies, instantiation of equations
+%* *
+%************************************************************************
+
+When we spot an equality arising from a functional dependency,
+we now use that equality (a "wanted") to rewrite the work-item
+constraint right away. This avoids two dangers
+
+ Danger 1: If we send the original constraint on down the pipeline
+ it may react with an instance declaration, and in delicate
+ situations (when a Given overlaps with an instance) that
+ may produce new insoluble goals: see Trac #4952
+
+ Danger 2: If we don't rewrite the constraint, it may re-react
+ with the same thing later, and produce the same equality
+ again --> termination worries.
+To achieve this required some refactoring of FunDeps.lhs (nicer
+now!).
+
+\begin{code}
+rewriteWithFunDeps :: [Equation]
+ -> [Xi] -> CtFlavor
+ -> TcS (Maybe ([Xi], [Coercion], WorkList))
+rewriteWithFunDeps eqn_pred_locs xis fl
+ = do { fd_ev_poss <- mapM (instFunDepEqn fl) eqn_pred_locs
+ ; let fd_ev_pos :: [(Int,FlavoredEvVar)]
+ fd_ev_pos = concat fd_ev_poss
+ (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
+ ; fds <- mapM (\(_,fev) -> mkCanonicalFEV fev) fd_ev_pos
+ ; let fd_work = unionWorkLists fds
+ ; if isEmptyWorkList fd_work
+ then return Nothing
+ else return (Just (rewritten_xis, cos, fd_work)) }
+
+instFunDepEqn :: CtFlavor -- Precondition: Only Wanted or Derived
+ -> Equation
+ -> TcS [(Int, FlavoredEvVar)]
+-- Post: Returns the position index as well as the corresponding FunDep equality
+instFunDepEqn fl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
+ , fd_pred1 = d1, fd_pred2 = d2 })
+ = do { let tvs = varSetElems qtvs
+ ; tvs' <- mapM instFlexiTcS tvs
+ ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
+ ; mapM (do_one subst) eqs }
+ where
+ fl' = case fl of
+ Given _ -> panic "mkFunDepEqns"
+ Wanted loc -> Wanted (push_ctx loc)
+ Derived loc -> Derived (push_ctx loc)
+
+ push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
+
+ do_one subst (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
+ = do { let sty1 = substTy subst ty1
+ sty2 = substTy subst ty2
+ ; ev <- newCoVar sty1 sty2
+ ; return (i, mkEvVarX ev fl') }
+
+rewriteDictParams :: [(Int,FlavoredEvVar)] -- A set of coercions : (pos, ty' ~ ty)
+ -> [Type] -- A sequence of types: tys
+ -> [(Type,Coercion)] -- Returns : [(ty', co : ty' ~ ty)]
+rewriteDictParams param_eqs tys
+ = zipWith do_one tys [0..]
+ where
+ do_one :: Type -> Int -> (Type,Coercion)
+ do_one ty n = case lookup n param_eqs of
+ Just wev -> (get_fst_ty wev, mkCoVarCoercion (evVarOf wev))
+ Nothing -> (ty,ty) -- Identity
+
+ get_fst_ty wev = case evVarOfPred wev of
+ EqPred ty1 _ -> ty1
+ _ -> panic "rewriteDictParams: non equality fundep"
+
+mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
+ -> TcM (TidyEnv, SDoc)
+mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
+ = do { zpred1 <- TcM.zonkTcPredType pred1
+ ; zpred2 <- TcM.zonkTcPredType pred2
+ ; let { tpred1 = tidyPred tidy_env zpred1
+ ; tpred2 = tidyPred tidy_env zpred2 }
+ ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
+ nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
+ nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
+ ; return (tidy_env, msg) }
+\end{code}
\ No newline at end of file