module TcCanonical(
mkCanonical, mkCanonicals, mkCanonicalFEV, mkCanonicalFEVs, canWanteds, canGivens,
canOccursCheck, canEqToWorkList,
- rewriteWithFunDeps
+ rewriteWithFunDeps, mkCanonicalFDAsDerived, mkCanonicalFDAsWanted
) where
#include "HsVersions.h"
import Var
import VarEnv ( TidyEnv )
import Outputable
-import Control.Monad ( unless, when, zipWithM, zipWithM_ )
+import Control.Monad ( unless, when, zipWithM, zipWithM_, foldM )
import MonadUtils
import Control.Applicative ( (<|>) )
up a bit; right now we waste a lot of energy traversing the same types
multiple times.
+
\begin{code}
+
-- Flatten a bunch of types all at once.
flattenMany :: CtFlavor -> [Type] -> TcS ([Xi], [Coercion], CanonicalCts)
-- Coercions :: Xi ~ Type
-- Preserve type synonyms if possible
-- We can tell if ty' is function-free by
-- whether there are any floated constraints
- ; if isEmptyCCan ccs then
+ ; if isReflCo co then
return (ty, mkReflCo ty, emptyCCan)
else
return (xi, co, ccs) }
-- Otherwise, it's a type function application, and we have to
-- flatten it away as well, and generate a new given equality constraint
-- between the application and a newly generated flattening skolem variable.
- | otherwise
+ | otherwise
= ASSERT( tyConArity tc <= length tys ) -- Type functions are saturated
do { (xis, cos, ccs) <- flattenMany fl tys
; let (xi_args, xi_rest) = splitAt (tyConArity tc) xis
-- The type function might be *over* saturated
-- in which case the remaining arguments should
-- be dealt with by AppTys
- fam_ty = mkTyConApp tc xi_args
- fam_co = mkReflCo fam_ty -- identity
-
- ; (ret_co, rhs_var, ct) <-
- if isGiven fl then
- do { rhs_var <- newFlattenSkolemTy fam_ty
- ; cv <- newGivenCoVar fam_ty rhs_var fam_co
- ; let ct = CFunEqCan { cc_id = cv
- , cc_flavor = fl -- Given
- , cc_fun = tc
- , cc_tyargs = xi_args
- , cc_rhs = rhs_var }
- ; return $ (mkCoVarCo cv, rhs_var, ct) }
- else -- Derived or Wanted: make a new *unification* flatten variable
- do { rhs_var <- newFlexiTcSTy (typeKind fam_ty)
- ; cv <- newCoVar fam_ty rhs_var
- ; let ct = CFunEqCan { cc_id = cv
- , cc_flavor = mkWantedFlavor fl
- -- Always Wanted, not Derived
- , cc_fun = tc
- , cc_tyargs = xi_args
- , cc_rhs = rhs_var }
- ; return $ (mkCoVarCo cv, rhs_var, ct) }
-
+ fam_ty = mkTyConApp tc xi_args
+ ; (ret_co, rhs_var, ct) <-
+ do { is_cached <- lookupFlatCacheMap tc xi_args fl
+ ; case is_cached of
+ Just (rhs_var,ret_co,_fl) -> return (ret_co, rhs_var, emptyCCan)
+ Nothing
+ | isGivenOrSolved fl ->
+ do { rhs_var <- newFlattenSkolemTy fam_ty
+ ; cv <- newGivenCoVar fam_ty rhs_var (mkReflCo fam_ty)
+ ; let ct = CFunEqCan { cc_id = cv
+ , cc_flavor = fl -- Given
+ , cc_fun = tc
+ , cc_tyargs = xi_args
+ , cc_rhs = rhs_var }
+ ; let ret_co = mkCoVarCo cv
+ ; updateFlatCacheMap tc xi_args rhs_var fl ret_co
+ ; return $ (ret_co, rhs_var, singleCCan ct) }
+ | otherwise ->
+ -- Derived or Wanted: make a new *unification* flatten variable
+ do { rhs_var <- newFlexiTcSTy (typeKind fam_ty)
+ ; cv <- newCoVar fam_ty rhs_var
+ ; let ct = CFunEqCan { cc_id = cv
+ , cc_flavor = mkWantedFlavor fl
+ -- Always Wanted, not Derived
+ , cc_fun = tc
+ , cc_tyargs = xi_args
+ , cc_rhs = rhs_var }
+ ; let ret_co = mkCoVarCo cv
+ ; updateFlatCacheMap tc xi_args rhs_var fl ret_co
+ ; return $ (ret_co, rhs_var, singleCCan ct) } }
; return ( foldl AppTy rhs_var xi_rest
- , foldl mkAppCo
- (mkSymCo ret_co
- `mkTransCo` mkTyConAppCo tc cos_args)
- cos_rest
- , ccs `extendCCans` ct) }
-
+ , foldl AppCo (mkSymCo ret_co
+ `mkTransCo` mkTyConAppCo tc cos_args)
+ cos_rest
+ , ccs `andCCan` ct) }
flatten ctxt (PredTy pred)
= do { (pred', co, ccs) <- flattenPred ctxt pred
canWanteds = fmap unionWorkLists . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev)
canGivens :: GivenLoc -> [EvVar] -> TcS WorkList
-canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc)) givens
+canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc GivenOrig)) givens
; return (unionWorkLists ccs) }
mkCanonicals :: CtFlavor -> [EvVar] -> TcS WorkList
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 -> canClassToWorkList fl ev clas 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
+ ; let no_flattening_happened = all isReflCo cos
dict_co = mkTyConAppCo (classTyCon cn) cos
- ; v_new <- if no_flattening_happened then return v
- else if isGiven fl then return v
+ ; v_new <- if no_flattening_happened then return v
+ else if isGivenOrSolved fl then return v
-- The cos are all identities if fl=Given,
-- hence nothing to do
else do { v' <- newDictVar cn xis -- D xis
; when (isWanted fl) $ setDictBind v (EvCast v' dict_co)
- ; when (isGiven fl) $ setDictBind v' (EvCast v (mkSymCo dict_co))
+ ; when (isGivenOrSolved fl) $ setDictBind v' (EvCast v (mkSymCo dict_co))
-- NB: No more setting evidence for derived now
; return v' }
Here's an example that demonstrates why we chose to NOT add
superclasses during simplification: [Comes from ticket #4497]
-
+
class Num (RealOf t) => Normed t
type family RealOf x
= 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
- flavor = orig_flavor
- ; sc_vars <- mapM newEvVar sc_theta
- ; _ <- zipWithM_ setEvBind sc_vars [EvSuperClass ev n | n <- [0..]]
- ; mkCanonicals flavor sc_vars }
-
- | isEmptyVarSet (tyVarsOfTypes xis)
+ | Just gk <- isGiven_maybe orig_flavor
+ = case gk of
+ GivenOrig -> do { let sc_theta = immSuperClasses cls xis
+ flavor = orig_flavor
+ ; sc_vars <- mapM newEvVar sc_theta
+ ; _ <- zipWithM_ setEvBind sc_vars [EvSuperClass ev n | n <- [0..]]
+ ; mkCanonicals flavor sc_vars }
+ GivenSolved -> return emptyWorkList
+ -- Seems very dangerous to add the superclasses for dictionaries that may be
+ -- partially solved because we may end up with evidence loops.
+
+ | isEmptyVarSet (tyVarsOfTypes xis)
= return emptyWorkList -- Wanteds with no variables yield no deriveds.
-- See Note [Improvement from Ground Wanteds]
; setCoBind cv $
mkFunCo (mkCoVarCo argv) (mkCoVarCo resv)
; return (argv,resv) }
-
- else if isGiven fl then
+ else if isGivenOrSolved fl then
let [arg,res] = decomposeCo 2 (mkCoVarCo cv)
in do { argv <- newGivenCoVar s1 s2 arg
; resv <- newGivenCoVar t1 t2 res
do { argsv <- zipWithM newCoVar tys1 tys2
; setCoBind cv $
mkTyConAppCo tc1 (map mkCoVarCo argsv)
- ; return argsv }
-
- else if isGiven fl then
- let cos = decomposeCo (length tys1) (mkCoVarCo cv)
+ ; return argsv }
+ else if isGivenOrSolved fl then
+ let cos = decomposeCo (length tys1) (mkCoVarCo cv)
in zipWith3M newGivenCoVar tys1 tys2 cos
else -- Derived
then do { cv' <- newCoVar s2 s1
; setCoBind cv $ mkSymCo (mkCoVarCo cv')
; return cv' }
- else if isGiven fl then
+ else if isGivenOrSolved fl then
newGivenCoVar s2 s1 (mkSymCo (mkCoVarCo cv))
else -- Derived
newDerivedId (EqPred s2 s1)
; (xi2, co2, ccs2) <- flatten fl s2 -- Flatten entire RHS
-- co2 :: xi2 ~ s2
; let ccs = ccs1 `andCCan` ccs2
- no_flattening_happened = isEmptyCCan ccs
- ; cv_new <- if no_flattening_happened then return cv
- else if isGiven fl then return cv
+ no_flattening_happened = all isReflCo (co2:cos1)
+ ; cv_new <- if no_flattening_happened then return cv
+ else if isGivenOrSolved fl then return cv
else if isWanted fl then
do { cv' <- newCoVar (unClassify (FunCls fn xis1)) xi2
-- cv' : F xis ~ xi2
; case mxi2' of {
Nothing -> canEqFailure fl cv ;
Just xi2' ->
- do { let no_flattening_happened = isEmptyCCan ccs2
- ; cv_new <- if no_flattening_happened then return cv
- else if isGiven fl then return cv
+ do { let no_flattening_happened = isReflCo co
+ ; cv_new <- if no_flattening_happened then return cv
+ else if isGivenOrSolved fl then return cv
else if isWanted fl then
do { cv' <- newCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2
; setCoBind cv (mkCoVarCo cv' `mkTransCo` co)
\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)]
+ -> [Xi]
+ -> WantedLoc
+ -> TcS (Maybe ([Xi], [Coercion], [(EvVar,WantedLoc)]))
+ -- Not quite a WantedEvVar unfortunately
+ -- Because our intention could be to make
+ -- it derived at the end of the day
+-- NB: The flavor of the returned EvVars will be decided by the caller
+-- Post: returns no trivial equalities (identities)
+rewriteWithFunDeps eqn_pred_locs xis wloc
+ = do { fd_ev_poss <- mapM (instFunDepEqn wloc) eqn_pred_locs
+ ; let fd_ev_pos :: [(Int,(EvVar,WantedLoc))]
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)]
+ ; if null fd_ev_pos then return Nothing
+ else return (Just (rewritten_xis, cos, map snd fd_ev_pos)) }
+
+instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,(EvVar,WantedLoc))]
-- Post: Returns the position index as well as the corresponding FunDep equality
-instFunDepEqn fl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
+instFunDepEqn wl (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 }
+ ; foldM (do_one subst) [] eqs }
where
- fl' = case fl of
- Given _ -> panic "mkFunDepEqns"
- Wanted loc -> Wanted (push_ctx loc)
- Derived loc -> Derived (push_ctx loc)
-
+ do_one subst ievs (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
+ = 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 { ev <- newCoVar sty1 sty2
+ ; let wl' = push_ctx wl
+ ; return $ (i,(ev,wl')):ievs }
+
+ push_ctx :: WantedLoc -> WantedLoc
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 = Type.substTy subst ty1
- sty2 = Type.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, mkCoVarCo (evVarOf wev))
- Nothing -> (ty, mkReflCo 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 :: (TcPredType, SDoc)
+ -> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc)
mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
= do { zpred1 <- TcM.zonkTcPredType pred1
; zpred2 <- TcM.zonkTcPredType pred2
nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
; return (tidy_env, msg) }
+
+rewriteDictParams :: [(Int,(EvVar,WantedLoc))] -- 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, mkCoVarCo (fst wev))
+ Nothing -> (ty, mkReflCo ty) -- Identity
+
+ get_fst_ty (wev,_wloc)
+ | EqPred ty1 _ <- evVarPred wev
+ = ty1
+ | otherwise
+ = panic "rewriteDictParams: non equality fundep!?"
+
+mkCanonicalFDAsWanted :: [(EvVar,WantedLoc)] -> TcS WorkList
+mkCanonicalFDAsWanted evlocs
+ = do { ws <- mapM can_as_wanted evlocs
+ ; return (unionWorkLists ws) }
+ where can_as_wanted (ev,loc) = mkCanonicalFEV (EvVarX ev (Wanted loc))
+
+
+mkCanonicalFDAsDerived :: [(EvVar,WantedLoc)] -> TcS WorkList
+mkCanonicalFDAsDerived evlocs
+ = do { ws <- mapM can_as_derived evlocs
+ ; return (unionWorkLists ws) }
+ where can_as_derived (ev,loc) = mkCanonicalFEV (EvVarX ev (Derived loc))
+
+
\end{code}
\ No newline at end of file
projects / ghc-hetmet.git / blobdiff