import TcType
import Class
import Unify
import HscTypes
import Id
import Name
- import Var
+ import Var ( Var, TyVar, EvVar, varType, setVarType )
import VarEnv
import VarSet
import PrelNames
instCallConstraints origin (EqPred ty1 ty2 : preds) -- Try short-cut
= do { traceTc "instCallConstraints" $ ppr (EqPred ty1 ty2)
- ; coi <- unifyType ty1 ty2
+ ; co <- unifyType ty1 ty2
; co_fn <- instCallConstraints origin preds
- ; let co = case coi of
- IdCo ty -> ty
- ACo co -> co
; return (co_fn <.> WpEvApp (EvCoercion co)) }
instCallConstraints origin (pred : preds)
= EvVarX (tidyEvVar env v) (tidyFlavor env fl)
tidyFlavor :: TidyEnv -> CtFlavor -> CtFlavor
-tidyFlavor env (Given loc) = Given (tidyGivenLoc env loc)
+tidyFlavor env (Given loc gk) = Given (tidyGivenLoc env loc) gk
tidyFlavor _ fl = fl
tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc
= EvVarX (substEvVar subst v) (substFlavor subst fl)
substFlavor :: TvSubst -> CtFlavor -> CtFlavor
-substFlavor subst (Given loc) = Given (substGivenLoc subst loc)
-substFlavor _ fl = fl
+substFlavor subst (Given loc gk) = Given (substGivenLoc subst loc) gk
+substFlavor _ fl = fl
substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
substGivenLoc subst (CtLoc skol span ctxt) = CtLoc (substSkolemInfo subst skol) span ctxt
substSkolemInfo subst (SigSkol cx ty) = SigSkol cx (substTy subst ty)
substSkolemInfo subst (InferSkol ids) = InferSkol (mapSnd (substTy subst) ids)
substSkolemInfo _ info = info
- \end{code}
+ \end{code}
#include "HsVersions.h"
import BasicTypes
- import Type
+ import Id ( evVarPred )
+ import TcErrors
import TcRnTypes
import FunDeps
import qualified TcMType as TcM
import TcType
- import TcErrors
+ import Type
import Coercion
import Class
import TyCon
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 isIdentityCoercion co then
- return (ty, ty, emptyCCan)
- ; if isEmptyCCan ccs then
++ ; if isReflCo co then
+ return (ty, mkReflCo ty, emptyCCan)
else
return (xi, co, ccs) }
flatten _ v@(TyVarTy _)
- = return (v, v, emptyCCan)
+ = return (v, mkReflCo v, emptyCCan)
flatten ctxt (AppTy ty1 ty2)
= do { (xi1,co1,c1) <- flatten ctxt ty1
; (xi2,co2,c2) <- flatten ctxt ty2
- ; return (mkAppTy xi1 xi2, mkAppCoercion co1 co2, c1 `andCCan` c2) }
+ ; return (mkAppTy xi1 xi2, mkAppCo co1 co2, c1 `andCCan` c2) }
flatten ctxt (FunTy ty1 ty2)
= do { (xi1,co1,c1) <- flatten ctxt ty1
; (xi2,co2,c2) <- flatten ctxt ty2
- ; return (mkFunTy xi1 xi2, mkFunCoercion co1 co2, c1 `andCCan` c2) }
+ ; return (mkFunTy xi1 xi2, mkFunCo co1 co2, c1 `andCCan` c2) }
flatten fl (TyConApp tc tys)
-- For a normal type constructor or data family application, we just
-- recursively flatten the arguments.
| not (isSynFamilyTyCon tc)
= do { (xis,cos,ccs) <- flattenMany fl tys
- ; return (mkTyConApp tc xis, mkTyConCoercion tc cos, ccs) }
+ ; return (mkTyConApp tc xis, mkTyConAppCo tc cos, 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 = fam_ty -- identity
- 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 fam_co
++ ; 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 = mkCoVarCoercion cv
++ ; 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 = mkCoVarCoercion cv
++ ; 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 AppTy (mkSymCoercion ret_co
- `mkTransCoercion` mkTyConCoercion tc cos_args) cos_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
; return (PredTy pred', co, ccs) }
tv_set = mkVarSet tvs
; unless (isEmptyBag bad_eqs)
(flattenForAllErrorTcS ctxt ty bad_eqs)
- ; return (mkForAllTys tvs rho', mkForAllTys tvs co, ccs) }
+ ; return (mkForAllTys tvs rho', foldr mkForAllCo co tvs, ccs) }
---------------
flattenPred :: CtFlavor -> TcPredType -> TcS (TcPredType, Coercion, CanonicalCts)
flattenPred ctxt (ClassP cls tys)
= do { (tys', cos, ccs) <- flattenMany ctxt tys
- ; return (ClassP cls tys', mkClassPPredCo cls cos, ccs) }
+ ; return (ClassP cls tys', mkPredCo $ ClassP cls cos, ccs) }
flattenPred ctxt (IParam nm ty)
= do { (ty', co, ccs) <- flatten ctxt ty
- ; return (IParam nm ty', mkIParamPredCo nm co, ccs) }
- -- TODO: Handling of coercions between EqPreds must be revisited once the New Coercion API is ready!
+ ; return (IParam nm ty', mkPredCo $ IParam nm co, ccs) }
flattenPred ctxt (EqPred ty1 ty2)
= do { (ty1', co1, ccs1) <- flatten ctxt ty1
; (ty2', co2, ccs2) <- flatten ctxt ty2
- ; return (EqPred ty1' ty2', mkEqPredCo co1 co2, ccs1 `andCCan` ccs2) }
-
+ ; return (EqPred ty1' ty2', mkPredCo $ EqPred co1 co2, ccs1 `andCCan` ccs2) }
\end{code}
%************************************************************************
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 = all isIdentityCoercion cos
- dict_co = mkTyConCoercion (classTyCon cn) cos
- ; 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 (isGivenOrSolved fl) $ setDictBind v' (EvCast v (mkSymCoercion 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]
canEq :: CtFlavor -> EvVar -> Type -> Type -> TcS CanonicalCts
canEq fl cv ty1 ty2
- | tcEqType ty1 ty2 -- Dealing with equality here avoids
+ | eqType ty1 ty2 -- Dealing with equality here avoids
-- later spurious occurs checks for a~a
- = do { when (isWanted fl) (setCoBind cv ty1)
+ = do { when (isWanted fl) (setCoBind cv (mkReflCo ty1))
; return emptyCCan }
-- If one side is a variable, orient and flatten,
; canEqLeaf untch fl cv (classify ty1) (classify ty2) }
-- NB: don't use VarCls directly because tv1 or tv2 may be scolems!
- canEq fl cv (TyConApp fn tys) ty2
- | isSynFamilyTyCon fn, length tys == tyConArity fn
- = do { untch <- getUntouchables
- ; canEqLeaf untch fl cv (FunCls fn tys) (classify ty2) }
- canEq fl cv ty1 (TyConApp fn tys)
- | isSynFamilyTyCon fn, length tys == tyConArity fn
- = do { untch <- getUntouchables
- ; canEqLeaf untch fl cv (classify ty1) (FunCls fn tys) }
-
- canEq fl cv s1 s2
- | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe s1,
- Just (t2a,t2b,t2c) <- splitCoPredTy_maybe s2
- = do { (v1,v2,v3)
- <- if isWanted fl then -- Wanted
- do { v1 <- newCoVar t1a t2a
- ; v2 <- newCoVar t1b t2b
- ; v3 <- newCoVar t1c t2c
- ; let res_co = mkCoPredCo (mkCoVarCoercion v1)
- (mkCoVarCoercion v2) (mkCoVarCoercion v3)
- ; setCoBind cv res_co
- ; return (v1,v2,v3) }
- else if isGivenOrSolved fl then -- Given
- let co_orig = mkCoVarCoercion cv
- coa = mkCsel1Coercion co_orig
- cob = mkCsel2Coercion co_orig
- coc = mkCselRCoercion co_orig
- in do { v1 <- newGivenCoVar t1a t2a coa
- ; v2 <- newGivenCoVar t1b t2b cob
- ; v3 <- newGivenCoVar t1c t2c coc
- ; return (v1,v2,v3) }
- else -- Derived
- do { v1 <- newDerivedId (EqPred t1a t2a)
- ; v2 <- newDerivedId (EqPred t1b t2b)
- ; v3 <- newDerivedId (EqPred t1c t2c)
- ; return (v1,v2,v3) }
- ; cc1 <- canEq fl v1 t1a t2a
- ; cc2 <- canEq fl v2 t1b t2b
- ; cc3 <- canEq fl v3 t1c t2c
- ; return (cc1 `andCCan` cc2 `andCCan` cc3) }
-
-
-- Split up an equality between function types into two equalities.
canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
= do { (argv, resv) <-
do { argv <- newCoVar s1 s2
; resv <- newCoVar t1 t2
; setCoBind cv $
- mkFunCoercion (mkCoVarCoercion argv) (mkCoVarCoercion resv)
+ mkFunCo (mkCoVarCo argv) (mkCoVarCo resv)
; return (argv,resv) }
--
- else if isGiven fl then
+ else if isGivenOrSolved fl then
- let [arg,res] = decomposeCo 2 (mkCoVarCoercion cv)
+ let [arg,res] = decomposeCo 2 (mkCoVarCo cv)
in do { argv <- newGivenCoVar s1 s2 arg
; resv <- newGivenCoVar t1 t2 res
; return (argv,resv) }
; cc2 <- canEq fl resv t1 t2
; return (cc1 `andCCan` cc2) }
- canEq fl cv (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2))
- | n1 == n2
- = if isWanted fl then
- 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 newCoVar tys1 tys2
- ; setCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs)
- ; andCCans <$> zipWith3M (canEq fl) vs tys1 tys2
- }
- else return emptyCCan
- -- How to decompose given dictionary (and implicit parameter) coercions?
- -- You may think that the following is right:
- -- let cos = decomposeCo (length tys1) (mkCoVarCoercion cv)
- -- in zipWith3M newGivOrDerCoVar tys1 tys2 cos
- -- But this assumes that the coercion is a type constructor-based
- -- coercion, and not a PredTy (ClassP cn cos) coercion. So we chose
- -- to not decompose these coercions. We have to get back to this
- -- when we clean up the Coercion API.
+ canEq fl cv (TyConApp fn tys) ty2
+ | isSynFamilyTyCon fn, length tys == tyConArity fn
+ = do { untch <- getUntouchables
+ ; canEqLeaf untch fl cv (FunCls fn tys) (classify ty2) }
+ canEq fl cv ty1 (TyConApp fn tys)
+ | isSynFamilyTyCon fn, length tys == tyConArity fn
+ = do { untch <- getUntouchables
+ ; canEqLeaf untch fl cv (classify ty1) (FunCls fn tys) }
canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2)
- | isAlgTyCon tc1 && isAlgTyCon tc2
+ | isDecomposableTyCon tc1 && isDecomposableTyCon tc2
, tc1 == tc2
, length tys1 == length tys2
= -- Generate equalities for each of the corresponding arguments
<- if isWanted fl then
do { argsv <- zipWithM newCoVar tys1 tys2
; setCoBind cv $
- mkTyConCoercion tc1 (map mkCoVarCoercion argsv)
- ; return argsv }
-
- else if isGivenOrSolved fl then
- let cos = decomposeCo (length tys1) (mkCoVarCoercion 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
canEq fl cv ty1 ty2
| Just (s1,t1) <- tcSplitAppTy_maybe ty1
, Just (s2,t2) <- tcSplitAppTy_maybe ty2
- = do { (cv1,cv2) <-
- if isWanted fl
- then do { cv1 <- newCoVar s1 s2
- ; cv2 <- newCoVar t1 t2
- ; setCoBind cv $
- mkAppCoercion (mkCoVarCoercion cv1) (mkCoVarCoercion cv2)
- ; return (cv1,cv2) }
-
- else if isGivenOrSolved fl then
- let co1 = mkLeftCoercion $ mkCoVarCoercion cv
- co2 = mkRightCoercion $ mkCoVarCoercion cv
- in do { cv1 <- newGivenCoVar s1 s2 co1
- ; cv2 <- newGivenCoVar t1 t2 co2
- ; return (cv1,cv2) }
- else -- Derived
- do { cv1 <- newDerivedId (EqPred s1 s2)
- ; cv2 <- newDerivedId (EqPred t1 t2)
- ; return (cv1,cv2) }
-
- ; cc1 <- canEq fl cv1 s1 s2
- ; cc2 <- canEq fl cv2 t1 t2
- ; return (cc1 `andCCan` cc2) }
+ = if isWanted fl
+ then do { cv1 <- newCoVar s1 s2
+ ; cv2 <- newCoVar t1 t2
+ ; setCoBind cv $
+ mkAppCo (mkCoVarCo cv1) (mkCoVarCo cv2)
+ ; cc1 <- canEq fl cv1 s1 s2
+ ; cc2 <- canEq fl cv2 t1 t2
+ ; return (cc1 `andCCan` cc2) }
+
+ else if isDerived fl
+ then do { cv1 <- newDerivedId (EqPred s1 s2)
+ ; cv2 <- newDerivedId (EqPred t1 t2)
+ ; cc1 <- canEq fl cv1 s1 s2
+ ; cc2 <- canEq fl cv2 t1 t2
+ ; return (cc1 `andCCan` cc2) }
+
+ else return emptyCCan -- We cannot decompose given applications
+ -- because we no longer have 'left' and 'right'
canEq fl cv s1@(ForAllTy {}) s2@(ForAllTy {})
| tcIsForAllTy s1, tcIsForAllTy s2,
| cls1 `re_orient` cls2
= do { cv' <- if isWanted fl
then do { cv' <- newCoVar s2 s1
- ; setCoBind cv $ mkSymCoercion (mkCoVarCoercion cv')
+ ; setCoBind cv $ mkSymCo (mkCoVarCo cv')
; return cv' }
- else if isGiven fl then
+ else if isGivenOrSolved fl then
- newGivenCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv))
+ newGivenCoVar s2 s1 (mkSymCo (mkCoVarCo cv))
else -- Derived
newDerivedId (EqPred s2 s1)
; canEqLeafOriented fl cv' cls2 s1 }
; (xi2, co2, ccs2) <- flatten fl s2 -- Flatten entire RHS
-- co2 :: xi2 ~ s2
; let ccs = ccs1 `andCCan` ccs2
- no_flattening_happened = all isIdentityCoercion (co2:cos1)
- 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
; let -- fun_co :: F xis1 ~ F tys1
- fun_co = mkTyConCoercion fn cos1
+ fun_co = mkTyConAppCo fn cos1
-- want_co :: F tys1 ~ s2
- want_co = mkSymCoercion fun_co
- `mkTransCoercion` mkCoVarCoercion cv'
- `mkTransCoercion` co2
+ want_co = mkSymCo fun_co
+ `mkTransCo` mkCoVarCo cv'
+ `mkTransCo` co2
; setCoBind cv want_co
; return cv' }
else -- Derived
; case mxi2' of {
Nothing -> canEqFailure fl cv ;
Just xi2' ->
- do { let no_flattening_happened = isIdentityCoercion co
- 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 (mkCoVarCoercion cv' `mkTransCoercion` co)
+ ; setCoBind cv (mkCoVarCo cv' `mkTransCo` co)
; return cv' }
else -- Derived
newDerivedId (EqPred (mkTyVarTy tv) xi2')
expandAway tv ty@(ForAllTy {})
= let (tvs,rho) = splitForAllTys ty
tvs_knds = map tyVarKind tvs
- in if tv `elemVarSet` tyVarsOfTypes tvs_knds then
+ in if tv `elemVarSet` tyVarsOfTypes tvs_knds then
-- Can't expand away the kinds unless we create
-- fresh variables which we don't want to do at this point.
Nothing
; mapM (do_one subst) eqs }
where
fl' = case fl of
- Given _ -> panic "mkFunDepEqns"
+ 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
+ = do { let sty1 = Type.substTy subst ty1
+ sty2 = Type.substTy subst ty2
; ev <- newCoVar sty1 sty2
; return (i, mkEvVarX ev fl') }
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
+ 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
import TcType
import TypeRep
import Type( isTyVarTy )
+import Unify ( tcMatchTys )
-
import Inst
import InstEnv
import TyCon
import Name
import NameEnv
- import Id ( idType )
+ import Id ( idType, evVarPred )
import Var
import VarSet
import VarEnv
-- because they are unconditionally wrong
-- Moreover, if any of the insolubles are givens, stop right there
-- ignoring nested errors, because the code is inaccessible
- = do { let (given, other) = partitionBag (isGiven . evVarX) insols
+ = do { let (given, other) = partitionBag (isGivenOrSolved . evVarX) insols
insol_implics = filterBag ic_insol implics
; if isEmptyBag given
then do { mapBagM_ (reportInsoluble ctxt) other
| otherwise
= pprPanic "reportInsoluble" (pprEvVarWithType ev)
where
- inaccessible_msg | Given loc <- flav
+ inaccessible_msg | Given loc GivenOrig <- flav
+ -- If a GivenSolved then we should not report inaccessible code
= hang (ptext (sLit "Inaccessible code in"))
2 (ppr (ctLocOrigin loc))
| otherwise = empty
where
first_loc = evVarX (head ev_vars)
ppr_one (EvVarX v loc)
- = parens (pprPred (evVarPred v)) <+> pprArisingAt loc
+ = parens (pprPredTy (evVarPred v)) <+> pprArisingAt loc
addErrorReport :: ReportErrCtxt -> SDoc -> TcM ()
addErrorReport ctxt msg = addErrTcM (cec_tidy ctxt, msg $$ cec_extra ctxt)
ty1 ty2
-- If the types in the error message are the same as the types we are unifying,
-- don't add the extra expected/actual message
- | act `tcEqType` ty1 && exp `tcEqType` ty2 = empty
- | exp `tcEqType` ty1 && act `tcEqType` ty2 = empty
+ | act `eqType` ty1 && exp `eqType` ty2 = empty
+ | exp `eqType` ty1 && act `eqType` ty2 = empty
| otherwise = mkExpectedActualMsg act exp
getWantedEqExtra orig _ _ = pprArising orig
couldNotDeduce givens (wanteds, orig)
= vcat [ hang (ptext (sLit "Could not deduce") <+> pprTheta wanteds)
2 (pprArising orig)
- , vcat pp_givens ]
- where
- pp_givens
- = case givens of
+ , vcat (pp_givens givens)]
+
+pp_givens :: [([EvVar], GivenLoc)] -> [SDoc]
+pp_givens givens
+ = case givens of
[] -> []
(g:gs) -> ppr_given (ptext (sLit "from the context")) g
: map (ppr_given (ptext (sLit "or from"))) gs
-
- ppr_given herald (gs,loc)
- = hang (herald <+> pprEvVarTheta gs)
- 2 (sep [ ptext (sLit "bound by") <+> ppr (ctLocOrigin loc)
- , ptext (sLit "at") <+> ppr (ctLocSpan loc)])
+ where ppr_given herald (gs,loc)
+ = hang (herald <+> pprEvVarTheta gs)
+ 2 (sep [ ptext (sLit "bound by") <+> ppr (ctLocOrigin loc)
+ , ptext (sLit "at") <+> ppr (ctLocSpan loc)])
addExtraInfo :: ReportErrCtxt -> TcType -> TcType -> ReportErrCtxt
-- Add on extra info about the types themselves
mk_overlap_msg (matches, unifiers)
= ASSERT( not (null matches) )
vcat [ addArising orig (ptext (sLit "Overlapping instances for")
- <+> pprPred pred)
+ <+> pprPredTy pred)
, sep [ptext (sLit "Matching instances") <> colon,
nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])]
+
+ , if not (null overlapping_givens) then
+ sep [ptext (sLit "Matching givens (or their superclasses)") <> colon, nest 2 (vcat overlapping_givens)]
+ else empty
+
+ , if null overlapping_givens && isSingleton matches && null unifiers then
+ -- Intuitively, some given matched the wanted in their flattened or rewritten (from given equalities)
+ -- form but the matcher can't figure that out because the constraints are non-flat and non-rewritten
+ -- so we simply report back the whole given context. Accelerate Smart.hs showed this problem.
+ sep [ptext (sLit "There exists a (perhaps superclass) match") <> colon, nest 2 (vcat (pp_givens givens))]
+ else empty
+
, if not (isSingleton matches)
then -- Two or more matches
empty
else -- One match, plus some unifiers
ASSERT( not (null unifiers) )
parens (vcat [ptext (sLit "The choice depends on the instantiation of") <+>
- quotes (pprWithCommas ppr (varSetElems (tyVarsOfPred pred))),
- ptext (sLit "To pick the first instance above, use -XIncoherentInstances"),
- ptext (sLit "when compiling the other instance declarations")])]
+ quotes (pprWithCommas ppr (varSetElems (tyVarsOfPred pred))),
+ if null (overlapping_givens) then
+ vcat [ ptext (sLit "To pick the first instance above, use -XIncoherentInstances"),
+ ptext (sLit "when compiling the other instance declarations")]
+ else empty])]
where
ispecs = [ispec | (ispec, _) <- matches]
+ givens = getUserGivens ctxt
+ overlapping_givens = unifiable_givens givens
+
+ unifiable_givens [] = []
+ unifiable_givens (gg:ggs)
+ | Just ggdoc <- matchable gg
+ = ggdoc : unifiable_givens ggs
+ | otherwise
+ = unifiable_givens ggs
+
+ matchable (evvars,gloc)
+ = case ev_vars_matching of
+ [] -> Nothing
+ _ -> Just $ hang (pprTheta ev_vars_matching)
+ 2 (sep [ ptext (sLit "bound by") <+> ppr (ctLocOrigin gloc)
+ , ptext (sLit "at") <+> ppr (ctLocSpan gloc)])
+ where ev_vars_matching = filter ev_var_matches (map evVarPred evvars)
+ ev_var_matches (ClassP clas' tys')
+ | clas' == clas
+ , Just _ <- tcMatchTys (tyVarsOfTypes tys) tys tys'
+ = True
+ ev_var_matches (ClassP clas' tys') =
+ any ev_var_matches (immSuperClasses clas' tys')
+ ev_var_matches _ = False
+
+
reportOverlap _ _ _ _ = panic "reportOverlap" -- Not a ClassP
----------------------
\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 (Wanted loc) thing = setCtLoc loc thing
+setCtFlavorLoc (Derived loc) thing = setCtLoc loc thing
+setCtFlavorLoc (Given loc _gk) thing = setCtLoc loc thing
\end{code}
%************************************************************************
import TcRnMonad
import TcMType
import TcType
+ import BuildTyCl
import Inst
import InstEnv
import FamInst
import FamInstEnv
- import MkCore ( nO_METHOD_BINDING_ERROR_ID )
import TcDeriv
import TcEnv
import RnSource ( addTcgDUs )
import TcHsType
import TcUnify
+ import MkCore ( nO_METHOD_BINDING_ERROR_ID )
import Type
import Coercion
import TyCon
import DataCon
import Class
import Var
+ import Pair
import VarSet
import CoreUtils ( mkPiTypes )
import CoreUnfold ( mkDFunUnfolding )
| isTyVarTy ty = return ()
| otherwise = addErrTc $ mustBeVarArgErr ty
checkIndex ty (Just instTy)
- | ty `tcEqType` instTy = return ()
- | otherwise = addErrTc $ wrongATArgErr ty instTy
+ | ty `eqType` instTy = return ()
+ | otherwise = addErrTc $ wrongATArgErr ty instTy
listToNameSet = addListToNameSet emptyNameSet
tv1 `sameLexeme` tv2 =
nameOccName (tyVarName tv1) == nameOccName (tyVarName tv2)
in
- extendTvSubst (substSameTyVar tvs replacingTvs) tv replacement
+ TcType.extendTvSubst (substSameTyVar tvs replacingTvs) tv replacement
+ \end{code}
+
+
+ %************************************************************************
+ %* *
+ Type checking family instances
+ %* *
+ %************************************************************************
+
+ Family instances are somewhat of a hybrid. They are processed together with
+ class instance heads, but can contain data constructors and hence they share a
+ lot of kinding and type checking code with ordinary algebraic data types (and
+ GADTs).
+
+ \begin{code}
+ tcFamInstDecl :: TopLevelFlag -> LTyClDecl Name -> TcM TyThing
+ tcFamInstDecl top_lvl (L loc decl)
+ = -- Prime error recovery, set source location
+ setSrcSpan loc $
+ tcAddDeclCtxt decl $
+ do { -- type family instances require -XTypeFamilies
+ -- and can't (currently) be in an hs-boot file
+ ; type_families <- xoptM Opt_TypeFamilies
+ ; is_boot <- tcIsHsBoot -- Are we compiling an hs-boot file?
+ ; checkTc type_families $ badFamInstDecl (tcdLName decl)
+ ; checkTc (not is_boot) $ badBootFamInstDeclErr
+
+ -- Perform kind and type checking
+ ; tc <- tcFamInstDecl1 decl
+ ; checkValidTyCon tc -- Remember to check validity;
+ -- no recursion to worry about here
+
+ -- Check that toplevel type instances are not for associated types.
+ ; when (isTopLevel top_lvl && isAssocFamily tc)
+ (addErr $ assocInClassErr (tcdName decl))
+
+ ; return (ATyCon tc) }
+
+ isAssocFamily :: TyCon -> Bool -- Is an assocaited type
+ isAssocFamily tycon
+ = case tyConFamInst_maybe tycon of
+ Nothing -> panic "isAssocFamily: no family?!?"
+ Just (fam, _) -> isTyConAssoc fam
+
+ assocInClassErr :: Name -> SDoc
+ assocInClassErr name
+ = ptext (sLit "Associated type") <+> quotes (ppr name) <+>
+ ptext (sLit "must be inside a class instance")
+
+
+
+ tcFamInstDecl1 :: TyClDecl Name -> TcM TyCon
+
+ -- "type instance"
+ tcFamInstDecl1 (decl@TySynonym {tcdLName = L loc tc_name})
+ = kcIdxTyPats decl $ \k_tvs k_typats resKind family ->
+ do { -- check that the family declaration is for a synonym
+ checkTc (isFamilyTyCon family) (notFamily family)
+ ; checkTc (isSynTyCon family) (wrongKindOfFamily family)
+
+ ; -- (1) kind check the right-hand side of the type equation
+ ; k_rhs <- kcCheckLHsType (tcdSynRhs decl) (EK resKind EkUnk)
+ -- ToDo: the ExpKind could be better
+
+ -- we need the exact same number of type parameters as the family
+ -- declaration
+ ; let famArity = tyConArity family
+ ; checkTc (length k_typats == famArity) $
+ wrongNumberOfParmsErr famArity
+
+ -- (2) type check type equation
+ ; tcTyVarBndrs k_tvs $ \t_tvs -> do { -- turn kinded into proper tyvars
+ ; t_typats <- mapM tcHsKindedType k_typats
+ ; t_rhs <- tcHsKindedType k_rhs
+
+ -- (3) check the well-formedness of the instance
+ ; checkValidTypeInst t_typats t_rhs
+
+ -- (4) construct representation tycon
+ ; rep_tc_name <- newFamInstTyConName tc_name t_typats loc
+ ; buildSynTyCon rep_tc_name t_tvs (SynonymTyCon t_rhs)
+ (typeKind t_rhs)
+ NoParentTyCon (Just (family, t_typats))
+ }}
+
+ -- "newtype instance" and "data instance"
+ tcFamInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name,
+ tcdCons = cons})
+ = kcIdxTyPats decl $ \k_tvs k_typats resKind fam_tycon ->
+ do { -- check that the family declaration is for the right kind
+ checkTc (isFamilyTyCon fam_tycon) (notFamily fam_tycon)
+ ; checkTc (isAlgTyCon fam_tycon) (wrongKindOfFamily fam_tycon)
+
+ ; -- (1) kind check the data declaration as usual
+ ; k_decl <- kcDataDecl decl k_tvs
+ ; let k_ctxt = tcdCtxt k_decl
+ k_cons = tcdCons k_decl
+
+ -- result kind must be '*' (otherwise, we have too few patterns)
+ ; checkTc (isLiftedTypeKind resKind) $ tooFewParmsErr (tyConArity fam_tycon)
+
+ -- (2) type check indexed data type declaration
+ ; tcTyVarBndrs k_tvs $ \t_tvs -> do { -- turn kinded into proper tyvars
+ ; unbox_strict <- doptM Opt_UnboxStrictFields
+
+ -- kind check the type indexes and the context
+ ; t_typats <- mapM tcHsKindedType k_typats
+ ; stupid_theta <- tcHsKindedContext k_ctxt
+
+ -- (3) Check that
+ -- (a) left-hand side contains no type family applications
+ -- (vanilla synonyms are fine, though, and we checked for
+ -- foralls earlier)
+ ; mapM_ checkTyFamFreeness t_typats
+
+ ; dataDeclChecks tc_name new_or_data stupid_theta k_cons
+
+ -- (4) construct representation tycon
+ ; rep_tc_name <- newFamInstTyConName tc_name t_typats loc
+ ; let ex_ok = True -- Existentials ok for type families!
+ ; fixM (\ rep_tycon -> do
+ { let orig_res_ty = mkTyConApp fam_tycon t_typats
+ ; data_cons <- tcConDecls unbox_strict ex_ok rep_tycon
+ (t_tvs, orig_res_ty) k_cons
+ ; tc_rhs <-
+ case new_or_data of
+ DataType -> return (mkDataTyConRhs data_cons)
+ NewType -> ASSERT( not (null data_cons) )
+ mkNewTyConRhs rep_tc_name rep_tycon (head data_cons)
+ ; buildAlgTyCon rep_tc_name t_tvs stupid_theta tc_rhs Recursive
+ False h98_syntax NoParentTyCon (Just (fam_tycon, t_typats))
+ -- We always assume that indexed types are recursive. Why?
+ -- (1) Due to their open nature, we can never be sure that a
+ -- further instance might not introduce a new recursive
+ -- dependency. (2) They are always valid loop breakers as
+ -- they involve a coercion.
+ })
+ }}
+ where
+ h98_syntax = case cons of -- All constructors have same shape
+ L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
+ _ -> True
+
+ tcFamInstDecl1 d = pprPanic "tcFamInstDecl1" (ppr d)
+
+ -- Kind checking of indexed types
+ -- -
+
+ -- Kind check type patterns and kind annotate the embedded type variables.
+ --
+ -- * Here we check that a type instance matches its kind signature, but we do
+ -- not check whether there is a pattern for each type index; the latter
+ -- check is only required for type synonym instances.
+
+ kcIdxTyPats :: TyClDecl Name
+ -> ([LHsTyVarBndr Name] -> [LHsType Name] -> Kind -> TyCon -> TcM a)
+ -- ^^kinded tvs ^^kinded ty pats ^^res kind
+ -> TcM a
+ kcIdxTyPats decl thing_inside
+ = kcHsTyVars (tcdTyVars decl) $ \tvs ->
+ do { let tc_name = tcdLName decl
+ ; fam_tycon <- tcLookupLocatedTyCon tc_name
+ ; let { (kinds, resKind) = splitKindFunTys (tyConKind fam_tycon)
+ ; hs_typats = fromJust $ tcdTyPats decl }
+
+ -- we may not have more parameters than the kind indicates
+ ; checkTc (length kinds >= length hs_typats) $
+ tooManyParmsErr (tcdLName decl)
+
+ -- type functions can have a higher-kinded result
+ ; let resultKind = mkArrowKinds (drop (length hs_typats) kinds) resKind
+ ; typats <- zipWithM kcCheckLHsType hs_typats
+ [ EK kind (EkArg (ppr tc_name) n)
+ | (kind,n) <- kinds `zip` [1..]]
+ ; thing_inside tvs typats resultKind fam_tycon
+ }
\end{code}
addErrCtxt (instDeclCtxt2 (idType dfun_id)) $
do { -- Instantiate the instance decl with skolem constants
; (inst_tyvars, dfun_theta, inst_head) <- tcSkolDFunType (idType dfun_id)
+ -- We instantiate the dfun_id with superSkolems.
+ -- See Note [Subtle interaction of recursion and overlap]
+ -- and Note [Binding when looking up instances]
; let (clas, inst_tys) = tcSplitDFunHead inst_head
(class_tyvars, sc_theta, _, op_items) = classBigSig clas
sc_theta' = substTheta (zipOpenTvSubst class_tyvars inst_tys) sc_theta
listToBag meth_binds)
}
where
- skol_info = InstSkol -- See Note [Subtle interaction of recursion and overlap]
+ skol_info = InstSkol
dfun_ty = idType dfun_id
dfun_id = instanceDFunId ispec
loc = getSrcSpan dfun_id
; return (sc_dict, DFunConstArg (Var sc_dict)) }
where
find _ [] = Nothing
- find i (ev:evs) | pred `tcEqPred` evVarPred ev = Just (ev, i)
- | otherwise = find (i+1) evs
+ find i (ev:evs) | pred `eqPred` evVarPred ev = Just (ev, i)
+ | otherwise = find (i+1) evs
------------------------------
tcSpecInstPrags :: DFunId -> InstBindings Name
inst_tvs = fst (tcSplitForAllTys (idType dfun_id))
Just (init_inst_tys, _) = snocView inst_tys
- rep_ty = fst (coercionKind co) -- [p]
+ rep_ty = pFst (coercionKind co) -- [p]
rep_pred = mkClassPred clas (init_inst_tys ++ [rep_ty])
-- co : [p] ~ T p
- co = substTyWith inst_tvs (mkTyVarTys tyvars) $
- case coi of { IdCo ty -> ty ;
- ACo co -> mkSymCoercion co }
+ co = substCoWithTys inst_tvs (mkTyVarTys tyvars) $
+ mkSymCo coi
----------------
tc_item :: (TcEvBinds, EvVar) -> (Id, DefMeth) -> TcM (TcId, LHsBind TcId)
----------------
mk_op_wrapper :: Id -> EvVar -> HsWrapper
mk_op_wrapper sel_id rep_d
- = WpCast (substTyWith sel_tvs (init_inst_tys ++ [co]) local_meth_ty)
+ = WpCast (liftCoSubstWith sel_tvs (map mkReflCo init_inst_tys ++ [co])
+ local_meth_ty)
<.> WpEvApp (EvId rep_d)
<.> mkWpTyApps (init_inst_tys ++ [rep_ty])
where
, ptext (sLit "Found") <+> quotes (ppr ty)
<+> ptext (sLit "but expected") <+> quotes (ppr instTy)
]
+
+ tooManyParmsErr :: Located Name -> SDoc
+ tooManyParmsErr tc_name
+ = ptext (sLit "Family instance has too many parameters:") <+>
+ quotes (ppr tc_name)
+
+ tooFewParmsErr :: Arity -> SDoc
+ tooFewParmsErr arity
+ = ptext (sLit "Family instance has too few parameters; expected") <+>
+ ppr arity
+
+ wrongNumberOfParmsErr :: Arity -> SDoc
+ wrongNumberOfParmsErr exp_arity
+ = ptext (sLit "Number of parameters must match family declaration; expected")
+ <+> ppr exp_arity
+
+ badBootFamInstDeclErr :: SDoc
+ badBootFamInstDeclErr
+ = ptext (sLit "Illegal family instance in hs-boot file")
+
+ notFamily :: TyCon -> SDoc
+ notFamily tycon
+ = vcat [ ptext (sLit "Illegal family instance for") <+> quotes (ppr tycon)
+ , nest 2 $ parens (ppr tycon <+> ptext (sLit "is not an indexed type family"))]
+
+ wrongKindOfFamily :: TyCon -> SDoc
+ wrongKindOfFamily family
+ = ptext (sLit "Wrong category of family instance; declaration was for a")
+ <+> kindOfFamily
+ where
+ kindOfFamily | isSynTyCon family = ptext (sLit "type synonym")
+ | isAlgTyCon family = ptext (sLit "data type")
+ | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
\end{code}
import TcCanonical
import VarSet
import Type
+import Unify
import Id
import Var
import Outputable
import TcRnTypes
+import TcMType ( isSilentEvVar )
import TcErrors
import TcSMonad
import Bag
will be marked as solved right before being pushed into the inert set.
See note [Touchables and givens].
- 8 No Given constraint mentions a touchable unification variable,
- except if the
+ 8 No Given constraint mentions a touchable unification variable, but
+ Given/Solved may do so.
+
+ 9 Given constraints will also have their superclasses in the inert set,
+ but Given/Solved will not.
Note that 6 and 7 are /not/ enforced by canonicalization but rather by
insertion in the inert list, ie by TcInteract.
, inert_funeqs = solved_funeqs }
in (is_solved, unsolved)
- where (unsolved_eqs, solved_eqs) = Bag.partitionBag (not.isGivenCt) eqs
+ where (unsolved_eqs, solved_eqs) = Bag.partitionBag (not.isGivenOrSolvedCt) eqs
(unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is)
(unsolved_dicts, solved_dicts) = extractUnsolvedCMap (inert_dicts is)
(unsolved_funeqs, solved_funeqs) = extractUnsolvedCMap (inert_funeqs is)
map mk_given evs
; return inert_ret }
where
- flav = Given gloc
+ flav = Given gloc GivenOrig
mk_given ev = mkEvVarX ev flav
solveInteractWanted :: InertSet -> [WantedEvVar] -> TcS InertSet
discharge_ct :: CanonicalCt -> TcS Bool -> TcS Bool
discharge_ct ct _rest
- | evVarPred (cc_id ct) `tcEqPred` the_pred
+ | evVarPred (cc_id ct) `eqPred` the_pred
, cc_flavor ct `canSolve` fl
- -- DV: No special care should be taken for Given/Solveds, we will
- -- never encounter a Given entering the constraint bag after a Given/Solved
- = do { when (isWanted fl) $ set_ev_bind ev (cc_id ct)
+ = do { when (isWanted fl) $ setEvBind ev (evVarTerm (cc_id ct))
-- Deriveds need no evidence
-- For Givens, we already have evidence, and we don't need it twice
; return True }
- where
- set_ev_bind x y
- | EqPred {} <- evVarPred y = setEvBind x (EvCoercion (mkCoVarCoercion y))
- | otherwise = setEvBind x (EvId y)
discharge_ct _ct rest = rest
\end{code}
, sr_stop = ContinueWith workItem }
SPSolved workItem'
- | not (isGivenCt workItem)
+ | not (isGivenOrSolvedCt workItem)
-- Original was wanted or derived but we have now made him
-- given so we have to interact him with the inerts due to
-- its status change. This in turn may produce more work.
-- See Note [Touchables and givens]
trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi })
- | isGiven gw
+ | isGivenOrSolved gw
= return SPCantSolve
| Just tv2 <- tcGetTyVar_maybe xi
= do { tch1 <- isTouchableMetaTyVar tv1
]
; setWantedTyBind tv xi
- ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi xi
+ ; let refl_xi = mkReflCo xi
+ ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi refl_xi
- ; when (isWanted wd) (setCoBind cv xi)
+ ; when (isWanted wd) (setCoBind cv refl_xi)
-- We don't want to do this for Derived, that's why we use 'when (isWanted wd)'
-
; return $ SPSolved (CTyEqCan { cc_id = cv_given
- , cc_flavor = mkGivenFlavor wd UnkSkol
+ , cc_flavor = mkSolvedFlavor wd UnkSkol
, cc_tyvar = tv, cc_rhs = xi }) }
\end{code}
doInteractWithInert
inertItem@(CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
- | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
+ | cls1 == cls2 && eqTypes tys1 tys2
= solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem
- | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
+ | cls1 == cls2 && (not (isGivenOrSolved fl1 && isGivenOrSolved fl2))
= -- See Note [When improvement happens]
do { let pty1 = ClassP cls1 tys1
pty2 = ClassP cls2 tys2
; case m of
Nothing -> noInteraction workItem
Just (rewritten_tys2, cos2, fd_work)
- | tcEqTypes tys1 rewritten_tys2
+ | eqTypes tys1 rewritten_tys2
-> -- Solve him on the spot in this case
case fl2 of
Given {} -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem)
workListFromNonEq workItem' `unionWorkList` fd_work }
where
- dict_co = mkTyConCoercion (classTyCon cls1) cos2
+ dict_co = mkTyConAppCo (classTyCon cls1) cos2
}
-- Class constraint and given equality: use the equality to rewrite
-- so we just generate a fresh coercion variable that isn't used anywhere.
doInteractWithInert (CIPCan { cc_id = id1, 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 && isGiven wfl && isGiven ifl
+ | nm1 == nm2 && isGivenOrSolved wfl && isGivenOrSolved ifl
= -- See Note [Overriding implicit parameters]
-- Dump the inert item, override totally with the new one
-- Do not require type equality
-- we must *override* the outer one with the inner one
mkIRContinue "IP/IP override" workItem DropInert emptyWorkList
- | nm1 == nm2 && ty1 `tcEqType` ty2
+ | nm1 == nm2 && ty1 `eqType` ty2
= solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem
| nm1 == nm2
Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem)
Wanted {} ->
do { setIPBind (cc_id workItem) $
- EvCast id1 (mkSymCoercion (mkCoVarCoercion co_var))
+ EvCast id1 (mkSymCo (mkCoVarCo co_var))
; mkIRStopK "IP/IP interaction (solved)" cans }
}
, cc_tyargs = args1, cc_rhs = xi1 })
workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
, cc_tyargs = args2, cc_rhs = xi2 })
- | tc1 == tc2 && and (zipWith tcEqType args1 args2)
++ | tc1 == tc2 && and (zipWith eqType args1 args2)
+ , Just GivenSolved <- isGiven_maybe fl1
+ = mkIRContinue "Funeq/Funeq" workItem DropInert emptyWorkList
- | tc1 == tc2 && and (zipWith tcEqType args1 args2)
++ | tc1 == tc2 && and (zipWith eqType args1 args2)
+ , Just GivenSolved <- isGiven_maybe fl2
+ = mkIRStopK "Funeq/Funeq" emptyWorkList
+
| fl1 `canSolve` fl2 && lhss_match
- = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
+ = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCo cv1,xi1) (cv2,fl2,xi2)
; mkIRStopK "FunEq/FunEq" cans }
| fl2 `canSolve` fl1 && lhss_match
- = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
+ = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
; mkIRContinue "FunEq/FunEq" workItem DropInert cans }
where
- lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
+ lhss_match = tc1 == tc2 && eqTypes args1 args2
doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
-- Check for matching LHS
| fl1 `canSolve` fl2 && tv1 == tv2
- = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
+ = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCo cv1,xi1) (cv2,fl2,xi2)
; mkIRStopK "Eq/Eq lhs" cans }
| fl2 `canSolve` fl1 && tv1 == tv2
- = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
+ = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
; mkIRContinue "Eq/Eq lhs" workItem DropInert cans }
-- Check for rewriting RHS
-- Equational Rewriting
rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
- = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
+ = do { let cos = map (liftCoSubstWith [tv] [mkCoVarCo cv]) xis -- xis[tv] ~ xis[xi]
args = substTysWith [tv] [xi] xis
con = classTyCon cl
- dict_co = mkTyConCoercion con cos
+ dict_co = mkTyConAppCo con cos
; dv' <- newDictVar cl args
; case gw of
- Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
+ Wanted {} -> setDictBind dv (EvCast dv' (mkSymCo dict_co))
Given {} -> setDictBind dv' (EvCast dv dict_co)
Derived {} -> return () -- Derived dicts we don't set any evidence
rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
- = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
- ty' = substTyWith [tv] [xi] ty
+ = do { let ip_co = liftCoSubstWith [tv] [mkCoVarCo cv] ty -- ty[tv] ~ t[xi]
+ ty' = substTyWith [tv] [xi] ty
; ipid' <- newIPVar nm ty'
; case gw of
- Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
+ Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCo ip_co))
Given {} -> setIPBind ipid' (EvCast ipid ip_co)
Derived {} -> return () -- Derived ips: we don't set any evidence
rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) -- cv2 :: F args ~ xi2
- = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
- args' = substTysWith [tv] [xi1] args
- fun_co = mkTyConCoercion tc arg_cos -- fun_co :: F args ~ F args'
+ = do { let co_subst = liftCoSubstWith [tv] [mkCoVarCo cv1]
+ arg_cos = map co_subst args
+ args' = substTysWith [tv] [xi1] args
+ fun_co = mkTyConAppCo tc arg_cos -- fun_co :: F args ~ F args'
xi2' = substTyWith [tv] [xi1] xi2
- xi2_co = substTyWith [tv] [mkCoVarCoercion cv1] xi2 -- xi2_co :: xi2 ~ xi2'
+ xi2_co = co_subst xi2 -- xi2_co :: xi2 ~ xi2'
; cv2' <- newCoVar (mkTyConApp tc args') xi2'
; case gw of
- Wanted {} -> setCoBind cv2 (fun_co `mkTransCoercion`
- mkCoVarCoercion cv2' `mkTransCoercion`
- mkSymCoercion xi2_co)
- Given {} -> setCoBind cv2' (mkSymCoercion fun_co `mkTransCoercion`
- mkCoVarCoercion cv2 `mkTransCoercion`
+ Wanted {} -> setCoBind cv2 (fun_co `mkTransCo`
+ mkCoVarCo cv2' `mkTransCo`
+ mkSymCo xi2_co)
+ Given {} -> setCoBind cv2' (mkSymCo fun_co `mkTransCo`
+ mkCoVarCo cv2 `mkTransCo`
xi2_co)
Derived {} -> return ()
rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
| Just tv2' <- tcGetTyVar_maybe xi2'
, tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
- = do { when (isWanted gw) (setCoBind cv2 (mkSymCoercion co2'))
+ = do { when (isWanted gw) (setCoBind cv2 (mkSymCo co2'))
; return emptyWorkList }
| otherwise
= do { cv2' <- newCoVar (mkTyVarTy tv2) xi2'
; case gw of
- Wanted {} -> setCoBind cv2 $ mkCoVarCoercion cv2' `mkTransCoercion`
- mkSymCoercion co2'
- Given {} -> setCoBind cv2' $ mkCoVarCoercion cv2 `mkTransCoercion`
+ Wanted {} -> setCoBind cv2 $ mkCoVarCo cv2' `mkTransCo`
+ mkSymCo co2'
+ Given {} -> setCoBind cv2' $ mkCoVarCo cv2 `mkTransCo`
co2'
Derived {} -> return ()
; canEqToWorkList gw cv2' (mkTyVarTy tv2) xi2' }
where
xi2' = substTyWith [tv1] [xi1] xi2
- co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
+ co2' = liftCoSubstWith [tv1] [mkCoVarCo cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
-- Used to ineract two equalities of the following form:
= do { cv2' <- newCoVar xi2 xi1
; case gw of
Wanted {} -> setCoBind cv2 $
- co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
+ co1 `mkTransCo` mkSymCo (mkCoVarCo cv2')
Given {} -> setCoBind cv2' $
- mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
+ mkSymCo (mkCoVarCo cv2) `mkTransCo` co1
Derived {} -> return ()
; mkCanonical gw cv2' }
= do { cv2' <- newCoVar xi1 xi2
; case gw of
Wanted {} -> setCoBind cv2 $
- co1 `mkTransCoercion` mkCoVarCoercion cv2'
+ co1 `mkTransCo` mkCoVarCo cv2'
Given {} -> setCoBind cv2' $
- mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
+ mkSymCo co1 `mkTransCo` mkCoVarCo cv2
Derived {} -> return ()
; mkCanonical gw cv2' }
rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
= do { cv2' <- newCoVar ty2a' ty2b' -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1]
; case fl2 of
- Wanted {} -> setCoBind cv2 $ co2a' `mkTransCoercion`
- mkCoVarCoercion cv2' `mkTransCoercion`
- mkSymCoercion co2b'
+ Wanted {} -> setCoBind cv2 $ co2a' `mkTransCo`
+ mkCoVarCo cv2' `mkTransCo`
+ mkSymCo co2b'
- Given {} -> setCoBind cv2' $ mkSymCoercion co2a' `mkTransCoercion`
- mkCoVarCoercion cv2 `mkTransCoercion`
+ Given {} -> setCoBind cv2' $ mkSymCo co2a' `mkTransCo`
+ mkCoVarCo cv2 `mkTransCo`
co2b'
Derived {} -> return ()
ty2a' = substTyWith [tv1] [xi1] ty2a
ty2b' = substTyWith [tv1] [xi1] ty2b
- co2a' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2a -- ty2a ~ ty2a[xi1/tv1]
- co2b' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2b -- ty2b ~ ty2b[xi1/tv1]
+ co2a' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2a -- ty2a ~ ty2a[xi1/tv1]
+ co2b' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2b -- ty2b ~ ty2b[xi1/tv1]
solveOneFromTheOther :: String -> (EvTerm, CtFlavor) -> CanonicalCt -> TcS InteractResult
-- First argument inert, second argument work-item. They both represent
-- so it's safe to continue on from this point
= mkIRContinue ("Solved[DI] " ++ info) workItem DropInert emptyWorkList
+ | Just GivenSolved <- isGiven_maybe ifl, isGivenOrSolved wfl
+ -- Same if the inert is a GivenSolved -- just get rid of it
+ = mkIRContinue ("Solved[SI] " ++ info) workItem DropInert emptyWorkList
+
| otherwise
= ASSERT( ifl `canSolve` wfl )
-- Because of Note [The Solver Invariant], plus Derived dealt with
-- only reacted with functional dependencies
-- arising from top-level instances.
-topReactionsStage :: SimplifierStage
-topReactionsStage depth workItem inerts
- = do { tir <- tryTopReact workItem
- ; case tir of
- NoTopInt ->
- return $ SR { sr_inerts = inerts
- , sr_new_work = emptyWorkList
- , sr_stop = ContinueWith workItem }
- SomeTopInt tir_new_work tir_new_inert ->
+topReactionsStage :: SimplifierStage
+topReactionsStage depth workItem inerts
+ = do { tir <- tryTopReact inerts workItem
+ -- NB: we pass the inerts as well. See Note [Instance and Given overlap]
+ ; case tir of
+ NoTopInt ->
+ return $ SR { sr_inerts = inerts
+ , sr_new_work = emptyWorkList
+ , sr_stop = ContinueWith workItem }
+ SomeTopInt tir_new_work tir_new_inert ->
do { bumpStepCountTcS
; traceFireTcS depth (ptext (sLit "Top react")
<+> vcat [ ptext (sLit "Work =") <+> ppr workItem
, ptext (sLit "New =") <+> ppr tir_new_work ])
- ; return $ SR { sr_inerts = inerts
+ ; return $ SR { sr_inerts = inerts
, sr_new_work = tir_new_work
, sr_stop = tir_new_inert
} }
}
-tryTopReact :: WorkItem -> TcS TopInteractResult
-tryTopReact workitem
+tryTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
+tryTopReact inerts workitem
= do { -- A flag controls the amount of interaction allowed
-- See Note [Simplifying RULE lhs constraints]
ctxt <- getTcSContext
; if allowedTopReaction (simplEqsOnly ctxt) workitem
then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
- ; doTopReact workitem }
+ ; doTopReact inerts workitem }
else return NoTopInt
}
allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
allowedTopReaction _ _ = True
-doTopReact :: WorkItem -> TcS TopInteractResult
+doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
-- The work item does not react with the inert set, so try interaction with top-level instances
-- NB: The place to add superclasses in *not* in doTopReact stage. Instead superclasses are
-- added in the worklist as part of the canonicalisation process.
-- Given dictionary
-- See Note [Given constraint that matches an instance declaration]
-doTopReact (CDictCan { cc_flavor = Given {} })
+doTopReact _inerts (CDictCan { cc_flavor = Given {} })
= return NoTopInt -- NB: Superclasses already added since it's canonical
-- Derived dictionary: just look for functional dependencies
-doTopReact workItem@(CDictCan { cc_flavor = fl@(Derived loc)
- , cc_class = cls, cc_tyargs = xis })
+doTopReact _inerts workItem@(CDictCan { cc_flavor = fl@(Derived loc)
+ , cc_class = cls, cc_tyargs = xis })
= do { instEnvs <- getInstEnvs
; let fd_eqns = improveFromInstEnv instEnvs
(ClassP cls xis, pprArisingAt loc)
, tir_new_inert = ContinueWith workItem' } }
-- Wanted dictionary
-doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc)
- , cc_class = cls, cc_tyargs = xis })
+doTopReact inerts workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc)
+ , cc_class = cls, cc_tyargs = xis })
= do { -- See Note [MATCHING-SYNONYMS]
- ; lkp_inst_res <- matchClassInst cls xis loc
+ ; lkp_inst_res <- matchClassInst inerts cls xis loc
; case lkp_inst_res of
NoInstance ->
do { traceTcS "doTopReact/ no class instance for" (ppr dv)
; case m of
Nothing -> return NoTopInt
Just (xis',cos,fd_work) ->
- do { let dict_co = mkTyConCoercion (classTyCon cls) cos
+ do { let dict_co = mkTyConAppCo (classTyCon cls) cos
; dv'<- newDictVar cls xis'
; setDictBind dv (EvCast dv' dict_co)
; let workItem' = CDictCan { cc_id = dv', cc_flavor = fl,
-- matches already so we won't get any more info
-- from functional dependencies
| null wtvs
- -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv)
+ -> do { traceTcS "doTopReact/found nullary class instance for" (ppr dv)
; setDictBind dv ev_term
-- Solved in one step and no new wanted work produced.
-- i.e we directly matched a top-level instance
, tir_new_inert = Stop } }
| otherwise
- -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv)
+ -> do { traceTcS "doTopReact/found non-nullary class instance for" (ppr dv)
; setDictBind dv ev_term
-- Solved and new wanted work produced, you may cache the
- -- (tentatively solved) dictionary as Given! (used to be: Derived)
- ; let solved = workItem { cc_flavor = given_fl }
- given_fl = Given (setCtLocOrigin loc UnkSkol)
+ -- (tentatively solved) dictionary as Solved given.
+ ; let solved = workItem { cc_flavor = solved_fl }
+ solved_fl = mkSolvedFlavor fl UnkSkol
; inst_work <- canWanteds wtvs
; return $ SomeTopInt { tir_new_work = inst_work
, tir_new_inert = ContinueWith solved } }
}
-- Type functions
-doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
- , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
+doTopReact _inerts (CFunEqCan { cc_flavor = fl })
+ | Just GivenSolved <- isGiven_maybe fl
+ = return NoTopInt -- If Solved, no more interactions should happen
+
+-- Otherwise, it's a Given, Derived, or Wanted
+doTopReact _inerts workItem@(CFunEqCan { cc_id = cv, cc_flavor = fl
+ , 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
- MatchInstNo
- -> return NoTopInt
+ MatchInstNo -> return NoTopInt
MatchInstSingle (rep_tc, rep_tys)
-> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
-- RHS of a type function, so that it never
-- appears in an error message
-- See Note [Type synonym families] in TyCon
- coe = mkTyConApp coe_tc rep_tys
- coe = mkAxInstCo coe_tc rep_tys
- ; cv' <- case fl of
- Wanted {} -> do { cv' <- newCoVar rhs_ty xi
- ; setCoBind cv $
- coe `mkTransCo`
- mkCoVarCo cv'
- ; return cv' }
- Given {} -> newGivenCoVar xi rhs_ty $
- mkSymCo (mkCoVarCo cv) `mkTransCo` coe
- Derived {} -> newDerivedId (EqPred xi rhs_ty)
- ; can_cts <- mkCanonical fl cv'
- ; return $ SomeTopInt can_cts Stop }
++ coe = mkAxInstCo coe_tc rep_tys
+ ; case fl of
+ Wanted {} -> do { cv' <- newCoVar rhs_ty xi
- ; setCoBind cv $
- coe `mkTransCoercion` mkCoVarCoercion cv'
++ ; setCoBind cv $ coe `mkTransCo` mkCoVarCo cv'
+ ; can_cts <- mkCanonical fl cv'
+ ; let solved = workItem { cc_flavor = solved_fl }
+ solved_fl = mkSolvedFlavor fl UnkSkol
+ ; if isEmptyWorkList can_cts then
+ return (SomeTopInt can_cts Stop) -- No point in caching
+ else return $
+ SomeTopInt { tir_new_work = can_cts
+ , tir_new_inert = ContinueWith solved }
+ }
+ Given {} -> do { cv' <- newGivenCoVar xi rhs_ty $
- mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
++ mkSymCo (mkCoVarCo cv) `mkTransCo` coe
+ ; can_cts <- mkCanonical fl cv'
+ ; return $
+ SomeTopInt { tir_new_work = can_cts
+ , tir_new_inert = Stop }
+ }
+ Derived {} -> do { cv' <- newDerivedId (EqPred xi rhs_ty)
+ ; can_cts <- mkCanonical fl cv'
+ ; return $
+ SomeTopInt { tir_new_work = can_cts
+ , tir_new_inert = Stop }
+ }
+ }
_
-> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
}
-- Any other work item does not react with any top-level equations
-doTopReact _workItem = return NoTopInt
+doTopReact _inerts _workItem = return NoTopInt
\end{code}
= NoInstance
| GenInst [WantedEvVar] EvTerm
-matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
-matchClassInst clas tys loc
+matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult
+matchClassInst inerts clas tys loc
= do { let pred = mkClassPred clas tys
; mb_result <- matchClass clas tys
+ ; untch <- getUntouchables
; case mb_result of
MatchInstNo -> return NoInstance
- MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
+ MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
-- we learn more about the reagent
- MatchInstSingle (dfun_id, mb_inst_tys) ->
+ MatchInstSingle (_,_)
+ | given_overlap untch ->
+ do { traceTcS "Delaying instance application" $
- vcat [ text "Workitem=" <+> pprPred (ClassP clas tys)
++ vcat [ text "Workitem=" <+> pprPredTy (ClassP clas tys)
+ , text "Silents and their superclasses=" <+> ppr silents_and_their_scs
+ , text "All given dictionaries=" <+> ppr all_given_dicts ]
+ ; return NoInstance -- see Note [Instance and Given overlap]
+ }
+
+ MatchInstSingle (dfun_id, mb_inst_tys) ->
do { checkWellStagedDFun pred dfun_id loc
-- It's possible that not all the tyvars are in
-- (presumably there's a functional dependency in class C)
-- Hence mb_inst_tys :: Either TyVar TcType
- ; tys <- instDFunTypes mb_inst_tys
+ ; tys <- instDFunTypes mb_inst_tys
; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
; if null theta then
return (GenInst [] (EvDFunApp dfun_id tys []))
; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }
}
}
+ where given_overlap :: TcsUntouchables -> Bool
+ given_overlap untch
+ = foldlBag (\r d -> r || matchable untch d) False all_given_dicts
+
+ matchable untch (CDictCan { cc_class = clas', cc_tyargs = sys, cc_flavor = fl })
+ | Just GivenOrig <- isGiven_maybe fl
+ , clas' == clas
+ , does_not_originate_in_a_silent clas' sys
+ = case tcUnifyTys (\tv -> if isTouchableMetaTyVar_InRange untch tv &&
+ tv `elemVarSet` tyVarsOfTypes tys
+ then BindMe else Skolem) tys sys of
+ -- We can't learn anything more about any variable at this point, so the only
+ -- cause of overlap can be by an instantiation of a touchable unification
+ -- variable. Hence we only bind touchable unification variables. In addition,
+ -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions.
+ Nothing -> False
+ Just _ -> True
+ | otherwise = False -- No overlap with a solved, already been taken care of
+ -- by the overlap check with the instance environment.
+ matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
+
+ does_not_originate_in_a_silent clas sys
+ -- UGLY: See Note [Silent parameters overlapping]
- = null $ filter (tcEqPred (ClassP clas sys)) silents_and_their_scs
++ = null $ filter (eqPred (ClassP clas sys)) silents_and_their_scs
+
+ silents_and_their_scs
+ = foldlBag (\acc rvnt -> case rvnt of
+ CDictCan { cc_id = d, cc_class = c, cc_tyargs = s }
+ | isSilentEvVar d -> (ClassP c s) : (transSuperClasses c s) ++ acc
+ _ -> acc) [] all_given_dicts
+
+ -- TODO:
+ -- When silent parameters will go away we should simply select from
+ -- the given map of the inert set.
+ all_given_dicts = Map.fold unionBags emptyCCan (cts_given $ inert_dicts inerts)
+
\end{code}
+
+Note [Silent parameters overlapping]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+DV 12/05/2011:
+The long-term goal is to completely remove silent superclass
+parameters when checking instance declarations. But until then we must
+make sure that we never prevent the application of an instance
+declaration because of a potential match from a silent parameter --
+after all we are supposed to have solved that silent parameter from
+some instance, anyway! In effect silent parameters behave more like
+Solved than like Given.
+
+A concrete example appears in typecheck/SilentParametersOverlapping.hs
+
+Note [Instance and Given overlap]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Assume that we have an inert set that looks as follows:
+ [Given] D [Int]
+And an instance declaration:
+ instance C a => D [a]
+A new wanted comes along of the form:
+ [Wanted] D [alpha]
+
+One possibility is to apply the instance declaration which will leave us
+with an unsolvable goal (C alpha). However, later on a new constraint may
+arise (for instance due to a functional dependency between two later dictionaries),
+that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha])
+will be transformed to [Wanted] D [Int], which could have been discharged by the given.
+
+The solution is that in matchClassInst and eventually in topReact, we get back with
+a matching instance, only when there is no Given in the inerts which is unifiable to
+this particular dictionary.
+
+The end effect is that, much as we do for overlapping instances, we delay choosing a
+class instance if there is a possibility of another instance OR a given to match our
+constraint later on. This fixes bugs #4981 and #5002.
+
+This is arguably not easy to appear in practice due to our aggressive prioritization
+of equality solving over other constraints, but it is possible. I've added a test case
+in typecheck/should-compile/GivenOverlapping.hs
+
+Moreover notice that our goals here are different than the goals of the top-level
+overlapping checks. There we are interested in validating the following principle:
+
+ If we inline a function f at a site where the same global instance environment
+ is available as the instance environment at the definition site of f then we
+ should get the same behaviour.
+
+But for the Given Overlap check our goal is just related to completeness of
+constraint solving.
+
+
+
+
--------------------------------
-- Creating new evidence variables
newEvVar, newCoVar, newEvVars,
- writeWantedCoVar, readWantedCoVar,
newIP, newDict, newSilentGiven, isSilentEvVar,
newWantedEvVar, newWantedEvVars,
-- Checking type validity
Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
SourceTyCtxt(..), checkValidTheta,
- checkValidInstance,
- checkValidTypeInst, checkTyFamFreeness,
+ checkValidInstHead, checkValidInstance,
+ checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
arityErr,
growPredTyVars, growThetaTyVars, validDerivPred,
--------------------------------
-- Zonking
zonkType, mkZonkTcTyVar, zonkTcPredType,
- zonkTcTypeCarefully,
- skolemiseUnboundMetaTyVar,
+ zonkTcTypeCarefully, skolemiseUnboundMetaTyVar,
zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
zonkQuantifiedTyVar, zonkQuantifiedTyVars,
zonkTcType, zonkTcTypes, zonkTcThetaType,
import TypeRep
import TcType
import Type
- import Coercion
import Class
import TyCon
import Var
newCoVar :: TcType -> TcType -> TcM CoVar
newCoVar ty1 ty2
- = do { name <- newName (mkTyVarOccFS (fsLit "co"))
+ = do { name <- newName (mkVarOccFS (fsLit "co"))
; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
newIP :: IPName Name -> TcType -> TcM IpId
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
readMutVar (metaTvRef tyvar)
- readWantedCoVar :: CoVar -> TcM MetaDetails
- readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar )
- readMutVar (metaTvRef covar)
-
isFilledMetaTyVar :: TyVar -> TcM Bool
-- True of a filled-in (Indirect) meta type variable
isFilledMetaTyVar tv
= WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
return ()
- writeWantedCoVar :: CoVar -> Coercion -> TcM ()
- writeWantedCoVar cv co = writeMetaTyVar cv co
-
--------------------
writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
-- Here the tyvar is for error checking only;
zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) }
zonkFlavor :: CtFlavor -> TcM CtFlavor
-zonkFlavor (Given loc) = do { loc' <- zonkGivenLoc loc; return (Given loc') }
-zonkFlavor fl = return fl
+zonkFlavor (Given loc gk) = do { loc' <- zonkGivenLoc loc; return (Given loc' gk) }
+zonkFlavor fl = return fl
zonkGivenLoc :: GivenLoc -> TcM GivenLoc
-- GivenLocs may have unification variables inside them!
-- The two interesting cases!
go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
- | otherwise = liftM TyVarTy $
- zonkTyVar zonk_tc_tyvar tyvar
+ | otherwise = return (TyVarTy tyvar)
-- Ordinary (non Tc) tyvars occur inside quantified types
go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
ty' <- go ty
- tyvar' <- zonkTyVar zonk_tc_tyvar tyvar
+ tyvar' <- return tyvar
return (ForAllTy tyvar' ty')
go_pred (ClassP c tys) = do tys' <- mapM go tys
; case cts of
Flexi -> unbound_var_fn tyvar
Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
-
- -- Zonk the kind of a non-TC tyvar in case it is a coercion variable
- -- (their kind contains types).
- zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for a TcTyVar
- -> TyVar -> TcM TyVar
- zonkTyVar zonk_tc_tyvar tv
- | isCoVar tv
- = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv)
- ; return $ setTyVarKind tv kind }
- | otherwise = return tv
\end{code}
warnTc (notNull dups) (dupPredWarn dups)
mapM_ (check_pred_ty dflags ctxt) theta
where
- (_,dups) = removeDups tcCmpPred theta
+ (_,dups) = removeDups cmpPred theta
-------------------------
check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
ambigErr :: PredType -> SDoc
ambigErr pred
- = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
+ = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPredTy pred),
nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
ptext (sLit "must be reachable from the type after the '=>'"))]
\end{code}
2 (ppr pred)
badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
- badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPred pred
- eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPred pred
+ badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPredTy pred
+ eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPredTy pred
$$
parens (ptext (sLit "Use -XTypeFamilies to permit this"))
predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"),
- nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
+ nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)]
dupPredWarn :: [[PredType]] -> SDoc
- dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
+ dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPredTy (map head dups)
arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
arityErr kind name n m
predUndecErr :: PredType -> SDoc -> SDoc
predUndecErr pred msg = sep [msg,
- nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
+ nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)]
nomoreMsg, smallerMsg, undecidableMsg :: SDoc
nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
Implication(..),
CtLoc(..), ctLocSpan, ctLocOrigin, setCtLocOrigin,
CtOrigin(..), EqOrigin(..),
- WantedLoc, GivenLoc, pushErrCtxt,
+ WantedLoc, GivenLoc, GivenKind(..), pushErrCtxt,
- SkolemInfo(..),
+ SkolemInfo(..),
- CtFlavor(..), pprFlavorArising, isWanted, isGiven, isDerived,
+ CtFlavor(..), pprFlavorArising, isWanted,
+ isGivenOrSolved, isGiven_maybe,
+ isDerived,
FlavoredEvVar,
-- Pretty printing
import HsSyn
import HscTypes
import Type
+ import Id ( evVarPred )
import Class ( Class )
import DataCon ( DataCon, dataConUserType )
import TcType
-- plus which bit is currently being examined
if_tv_env :: UniqFM TyVar, -- Nested tyvar bindings
+ -- (and coercions)
if_id_env :: UniqFM Id -- Nested id binding
}
\end{code}
%************************************************************************
%* *
Wanted constraints
-
These are forced to be in TcRnTypes because
TcLclEnv mentions WantedConstraints
WantedConstraint mentions CtLoc
pprEvVarTheta ev_vars = pprTheta (map evVarPred ev_vars)
pprEvVarWithType :: EvVar -> SDoc
- pprEvVarWithType v = ppr v <+> dcolon <+> pprPred (evVarPred v)
+ pprEvVarWithType v = ppr v <+> dcolon <+> pprPredTy (evVarPred v)
pprWantedsWithLocs :: WantedConstraints -> SDoc
pprWantedsWithLocs wcs
\begin{code}
data CtFlavor
- = Given GivenLoc -- We have evidence for this constraint in TcEvBinds
- | Derived WantedLoc
- -- We have evidence for this constraint in TcEvBinds;
- -- *however* this evidence can contain wanteds, so
- -- it's valid only provisionally to the solution of
- -- these wanteds
- | Wanted WantedLoc -- We have no evidence bindings for this constraint.
-
--- data DerivedOrig = DerSC | DerInst | DerSelf
--- Deriveds are either superclasses of other wanteds or deriveds, or partially
--- solved wanteds from instances, or 'self' dictionaries containing yet wanted
--- superclasses.
+ = Given GivenLoc GivenKind -- We have evidence for this constraint in TcEvBinds
+ | Derived WantedLoc -- Derived's are just hints for unifications
+ | Wanted WantedLoc -- We have no evidence bindings for this constraint.
+
+data GivenKind
+ = GivenOrig -- Originates in some given, such as signature or pattern match
+ | GivenSolved -- Is given as result of being solved, maybe provisionally on
+ -- some other wanted constraints.
instance Outputable CtFlavor where
- ppr (Given {}) = ptext (sLit "[G]")
- ppr (Wanted {}) = ptext (sLit "[W]")
- ppr (Derived {}) = ptext (sLit "[D]")
+ ppr (Given _ GivenOrig) = ptext (sLit "[G]")
+ ppr (Given _ GivenSolved) = ptext (sLit "[S]") -- Print [S] for Given/Solved's
+ ppr (Wanted {}) = ptext (sLit "[W]")
+ ppr (Derived {}) = ptext (sLit "[D]")
+
pprFlavorArising :: CtFlavor -> SDoc
-pprFlavorArising (Derived wl ) = pprArisingAt wl
+pprFlavorArising (Derived wl) = pprArisingAt wl
pprFlavorArising (Wanted wl) = pprArisingAt wl
-pprFlavorArising (Given gl) = pprArisingAt gl
+pprFlavorArising (Given gl _) = pprArisingAt gl
isWanted :: CtFlavor -> Bool
isWanted (Wanted {}) = True
isWanted _ = False
-isGiven :: CtFlavor -> Bool
-isGiven (Given {}) = True
-isGiven _ = False
+isGivenOrSolved :: CtFlavor -> Bool
+isGivenOrSolved (Given {}) = True
+isGivenOrSolved _ = False
+
+isGiven_maybe :: CtFlavor -> Maybe GivenKind
+isGiven_maybe (Given _ gk) = Just gk
+isGiven_maybe _ = Nothing
isDerived :: CtFlavor -> Bool
isDerived (Derived {}) = True
CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts,
deCanonicalise, mkFrozenError,
- isWanted, isGiven, isDerived,
- isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
+ isWanted, isGivenOrSolved, isDerived,
+ isGivenOrSolvedCt, isGivenCt_maybe,
+ isWantedCt, isDerivedCt, pprFlavorArising,
isFlexiTcsTv,
canRewrite, canSolve,
- combineCtLoc, mkGivenFlavor, mkWantedFlavor,
+ combineCtLoc, mkSolvedFlavor, mkGivenFlavor,
+ mkWantedFlavor,
getWantedLoc,
TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality
setWantedTyBind,
+ lookupFlatCacheMap, updateFlatCacheMap,
+
getInstEnvs, getFamInstEnvs, -- Getting the environments
getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
import qualified TcMType as TcM
import qualified TcEnv as TcM
( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
+ import Kind
import TcType
import DynFlags
import Bag
import MonadUtils
import VarSet
+ import Pair
import FastString
import HsBinds -- for TcEvBinds stuff
import TcRnTypes
import Data.IORef
+import qualified Data.Map as Map
+
#ifdef DEBUG
import StaticFlags( opt_PprStyle_Debug )
import Control.Monad( when )
ppr (CIPCan ip fl ip_nm ty)
= ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
ppr (CTyEqCan co fl tv ty)
- = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
+ = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyVarTy tv) ty)
ppr (CFunEqCan co fl tc tys ty)
- = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
+ = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyConApp tc tys) ty)
ppr (CFrozenErr co fl)
= ppr fl <+> pprEvVarWithType co
\end{code}
isWantedCt :: CanonicalCt -> Bool
isWantedCt ct = isWanted (cc_flavor ct)
isDerivedCt :: CanonicalCt -> Bool
isDerivedCt ct = isDerived (cc_flavor ct)
+isGivenCt_maybe :: CanonicalCt -> Maybe GivenKind
+isGivenCt_maybe ct = isGiven_maybe (cc_flavor ct)
+
+isGivenOrSolvedCt :: CanonicalCt -> Bool
+isGivenOrSolvedCt ct = isGivenOrSolved (cc_flavor ct)
+
+
canSolve :: CtFlavor -> CtFlavor -> Bool
-- canSolve ctid1 ctid2
-- The constraint ctid1 can be used to solve ctid2
combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
-- Precondition: At least one of them should be wanted
-combineCtLoc (Wanted loc) _ = loc
-combineCtLoc _ (Wanted loc) = loc
-combineCtLoc (Derived loc ) _ = loc
-combineCtLoc _ (Derived loc ) = loc
+combineCtLoc (Wanted loc) _ = loc
+combineCtLoc _ (Wanted loc) = loc
+combineCtLoc (Derived loc ) _ = loc
+combineCtLoc _ (Derived loc ) = loc
combineCtLoc _ _ = panic "combineCtLoc: both given"
-mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
-mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
-mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
-mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
+mkSolvedFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
+-- To be called when we actually solve a wanted/derived (perhaps leaving residual goals)
+mkSolvedFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenSolved
+mkSolvedFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) GivenSolved
+mkSolvedFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
+mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
+mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenOrig
+mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) GivenOrig
+mkGivenFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
mkWantedFlavor :: CtFlavor -> CtFlavor
mkWantedFlavor (Wanted loc) = Wanted loc
mkWantedFlavor (Derived loc) = Wanted loc
-mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
+mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavor" (ppr fl)
\end{code}
%************************************************************************
tcs_untch :: TcsUntouchables,
- tcs_ic_depth :: Int, -- Implication nesting depth
- tcs_count :: IORef Int -- Global step count
+ tcs_ic_depth :: Int, -- Implication nesting depth
+ tcs_count :: IORef Int, -- Global step count
+
+ tcs_flat_map :: IORef FlatCache
}
+data FlatCache
+ = FlatCache { givenFlatCache :: Map.Map FunEqHead (TcType,Coercion,CtFlavor)
+ -- Invariant: all CtFlavors here satisfy isGiven
+ , wantedFlatCache :: Map.Map FunEqHead (TcType,Coercion,CtFlavor) }
+ -- Invariant: all CtFlavors here satisfy isWanted
+
+emptyFlatCache :: FlatCache
+emptyFlatCache
+ = FlatCache { givenFlatCache = Map.empty, wantedFlatCache = Map.empty }
+
+newtype FunEqHead = FunEqHead (TyCon,[Xi])
+
+instance Eq FunEqHead where
- FunEqHead (tc1,xis1) == FunEqHead (tc2,xis2) = tc1 == tc2 && tcEqTypes xis1 xis2
++ FunEqHead (tc1,xis1) == FunEqHead (tc2,xis2) = tc1 == tc2 && eqTypes xis1 xis2
+
+instance Ord FunEqHead where
+ FunEqHead (tc1,xis1) `compare` FunEqHead (tc2,xis2)
+ = case compare tc1 tc2 of
- EQ -> tcCmpTypes xis1 xis2
++ EQ -> cmpTypes xis1 xis2
+ other -> other
+
type TcsUntouchables = (Untouchables,TcTyVarSet)
-- Like the TcM Untouchables,
-- but records extra TcsTv variables generated during simplification
= do { ty_binds_var <- TcM.newTcRef emptyVarEnv
; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
; step_count <- TcM.newTcRef 0
+ ; flat_cache_var <- TcM.newTcRef emptyFlatCache
; let env = TcSEnv { tcs_ev_binds = ev_binds_var
, tcs_ty_binds = ty_binds_var
, tcs_context = context
, tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
, tcs_count = step_count
, tcs_ic_depth = 0
+ , tcs_flat_map = flat_cache_var
}
-- Run the computation
, tcs_untch = (_outer_range, outer_tcs)
, tcs_count = count
, tcs_ic_depth = idepth
- , tcs_context = ctxt } ->
- let
- inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
+ , tcs_context = ctxt
+ , tcs_flat_map = orig_flat_cache_var
+ } ->
+ do { let inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
-- The inner_range should be narrower than the outer one
-- (thus increasing the set of untouchables) but
-- the inner Tcs-untouchables must be unioned with the
-- outer ones!
- nest_env = TcSEnv { tcs_ev_binds = ref
- , tcs_ty_binds = ty_binds
- , tcs_untch = inner_untch
- , tcs_count = count
- , tcs_ic_depth = idepth+1
- , tcs_context = ctxtUnderImplic ctxt }
- in
- thing_inside nest_env
+
+ ; orig_flat_cache <- TcM.readTcRef orig_flat_cache_var
+ ; flat_cache_var <- TcM.newTcRef orig_flat_cache
+ -- One could be more conservative as well:
+ -- ; flat_cache_var <- TcM.newTcRef emptyFlatCache
+
+ -- Consider copying the results the tcs_flat_map of the
+ -- incomping constraint, but we must make sure that we
+ -- have pushed everything in, which seems somewhat fragile
+ ; let nest_env = TcSEnv { tcs_ev_binds = ref
+ , tcs_ty_binds = ty_binds
+ , tcs_untch = inner_untch
+ , tcs_count = count
+ , tcs_ic_depth = idepth+1
+ , tcs_context = ctxtUnderImplic ctxt
+ , tcs_flat_map = flat_cache_var }
+ ; thing_inside nest_env }
recoverTcS :: TcS a -> TcS a -> TcS a
recoverTcS (TcS recovery_code) (TcS thing_inside)
ctxtUnderImplic ctxt = ctxt
tryTcS :: TcS a -> TcS a
--- Like runTcS, but from within the TcS monad
+-- Like runTcS, but from within the TcS monad
-- Ignore all the evidence generated, and do not affect caller's evidence!
-tryTcS tcs
+tryTcS tcs
= TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
; ev_binds_var <- TcM.newTcEvBinds
+ ; flat_cache_var <- TcM.newTcRef emptyFlatCache
; let env1 = env { tcs_ev_binds = ev_binds_var
- , tcs_ty_binds = ty_binds_var }
- ; unTcS tcs env1 })
+ , tcs_ty_binds = ty_binds_var
+ , tcs_flat_map = flat_cache_var }
+ ; unTcS tcs env1 })
-- Update TcEvBinds
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
+getFlatCacheMapVar :: TcS (IORef FlatCache)
+getFlatCacheMapVar
+ = TcS (return . tcs_flat_map)
+
+lookupFlatCacheMap :: TyCon -> [Xi] -> CtFlavor
+ -> TcS (Maybe (TcType,Coercion,CtFlavor))
+-- For givens, we lookup in given flat cache
+lookupFlatCacheMap tc xis (Given {})
+ = do { cache_ref <- getFlatCacheMapVar
+ ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
+ ; return $ Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) }
+-- For wanteds, we first lookup in givenFlatCache.
+-- If we get nothing back then we lookup in wantedFlatCache.
+lookupFlatCacheMap tc xis (Wanted {})
+ = do { cache_ref <- getFlatCacheMapVar
+ ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
+ ; case Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) of
+ Nothing -> return $ Map.lookup (FunEqHead (tc,xis)) (wantedFlatCache cache_map)
+ other -> return other }
+lookupFlatCacheMap _tc _xis (Derived {}) = return Nothing
+
+updateFlatCacheMap :: TyCon -> [Xi]
+ -> TcType -> CtFlavor -> Coercion -> TcS ()
+updateFlatCacheMap _tc _xis _tv (Derived {}) _co
+ = return () -- Not caching deriveds
+updateFlatCacheMap tc xis ty fl co
+ = do { cache_ref <- getFlatCacheMapVar
+ ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
+ ; let new_cache_map
+ | isGivenOrSolved fl
+ = cache_map { givenFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,co,fl) $
+ givenFlatCache cache_map }
+ | isWanted fl
+ = cache_map { wantedFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,co,fl) $
+ wantedFlatCache cache_map }
+ | otherwise = pprPanic "updateFlatCacheMap, met Derived!" $ empty
+ ; wrapTcS $ TcM.writeTcRef cache_ref new_cache_map }
+
getTcEvBindsBag :: TcS EvBindMap
getTcEvBindsBag
= do { EvBindsVar ev_ref _ <- getTcEvBinds
; wrapTcS $ TcM.readTcRef ev_ref }
+
setCoBind :: CoVar -> Coercion -> TcS ()
setCoBind cv co = setEvBind cv (EvCoercion co)
bind_lvl = TcM.topIdLvl dfun_id
pprEq :: TcType -> TcType -> SDoc
- pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
+ pprEq ty1 ty2 = pprPredTy $ mkEqPred (ty1,ty2)
isTouchableMetaTyVar :: TcTyVar -> TcS Bool
isTouchableMetaTyVar tv
\begin{code}
module TcSimplify(
simplifyInfer,
- simplifyDefault, simplifyDeriv,
+ simplifyDefault, simplifyDeriv,
simplifyRule, simplifyTop, simplifyInteractive
) where
import TcSMonad
import TcInteract
import Inst
- import Unify( niFixTvSubst, niSubstTvSet )
+ import Id ( evVarPred )
+ import Unify ( niFixTvSubst, niSubstTvSet )
import Var
import VarSet
import VarEnv
+ import Coercion
import TypeRep
import Name
unsolved_implics
}
-givensFromWanteds :: CanonicalCts -> Bag FlavoredEvVar
--- Extract the *wanted* ones from CanonicalCts
--- and make them into *givens*
-givensFromWanteds = foldrBag getWanted emptyBag
+givensFromWanteds :: SimplContext -> CanonicalCts -> Bag FlavoredEvVar
+-- Extract the Wanted ones from CanonicalCts and conver to
+-- Givens; not Given/Solved, see Note [Preparing inert set for implications]
+givensFromWanteds _ctxt = foldrBag getWanted emptyBag
where
getWanted :: CanonicalCt -> Bag FlavoredEvVar -> Bag FlavoredEvVar
getWanted cc givens
- | not (isCFrozenErr cc)
- , Wanted loc <- cc_flavor cc
- , let given = mkEvVarX (cc_id cc) (Given (setCtLocOrigin loc UnkSkol))
- = given `consBag` givens
- | otherwise
- = givens -- We are not helping anyone by pushing a Derived in!
- -- Because if we could not solve it to start with
- -- we are not going to do either inside the impl constraint
-
+ | pushable_wanted cc
+ = let given = mkEvVarX (cc_id cc) (mkGivenFlavor (cc_flavor cc) UnkSkol)
+ in given `consBag` givens -- and not mkSolvedFlavor,
+ -- see Note [Preparing inert set for implications]
+ | otherwise = givens
+
+ pushable_wanted :: CanonicalCt -> Bool
+ pushable_wanted cc
+ | not (isCFrozenErr cc)
+ , isWantedCt cc
+ = isEqPred (evVarPred (cc_id cc)) -- see Note [Preparing inert set for implications]
+ | otherwise = False
+
solveNestedImplications :: InertSet -> CanonicalCts
-> Bag Implication
-> TcS (Bag FlavoredEvVar, Bag Implication)
| otherwise
= do { -- See Note [Preparing inert set for implications]
-- Push the unsolved wanteds inwards, but as givens
- let pushed_givens = givensFromWanteds unsolved_cans
+
+ ; simpl_ctx <- getTcSContext
+
+ ; let pushed_givens = givensFromWanteds simpl_ctx unsolved_cans
tcs_untouchables = filterVarSet isFlexiTcsTv $
tyVarsOfEvVarXs pushed_givens
-- See Note [Extra TcsTv untouchables]
; traceTcS "solveWanteds: preparing inerts for implications {"
(vcat [ppr tcs_untouchables, ppr pushed_givens])
-
- ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens
+
+ ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens
; traceTcS "solveWanteds: } now doing nested implications {" $
vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
given because the resulting set is not inert. Hence we have to do a
'solveInteract' step first.
+Finally, note that we convert them to [Given] and NOT [Given/Solved].
+The reason is that Given/Solved are weaker than Givens and may be discarded.
+As an example consider the inference case, where we may have, the following
+original constraints:
+ [Wanted] F Int ~ Int
+ (F Int ~ a => F Int ~ a)
+If we convert F Int ~ Int to [Given/Solved] instead of Given, then the next
+given (F Int ~ a) is going to cause the Given/Solved to be ignored, casting
+the (F Int ~ a) insoluble. Hence we should really convert the residual
+wanteds to plain old Given.
+
+We need only push in unsolved equalities both in checking mode and inference mode:
+
+ (1) In checking mode we should not push given dictionaries in because of
+example LongWayOverlapping.hs, where we might get strange overlap
+errors between far-away constraints in the program. But even in
+checking mode, we must still push type family equations. Consider:
+
+ type instance F True a b = a
+ type instance F False a b = b
+
+ [w] F c a b ~ gamma
+ (c ~ True) => a ~ gamma
+ (c ~ False) => b ~ gamma
+
+Since solveCTyFunEqs happens at the very end of solving, the only way to solve
+the two implications is temporarily consider (F c a b ~ gamma) as Given (NB: not
+merely Given/Solved because it has to interact with the top-level instance
+environment) and push it inside the implications. Now, when we come out again at
+the end, having solved the implications solveCTyFunEqs will solve this equality.
+
+ (2) In inference mode, we recheck the final constraint in checking mode and
+hence we will be able to solve inner implications from top-level quantified
+constraints nonetheless.
+
+
Note [Extra TcsTv untouchables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Furthemore, we record the inert set simplifier-generated unification
; return (niFixTvSubst ni_subst, unsolved_can_cts) }
where
- solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setCoBind cv ty
+ solve_one (cv,tv,ty) = do { setWantedTyBind tv ty
+ ; setCoBind cv (mkReflCo ty) }
------------
type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
, not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
-- Occurs check: see Note [Solving Family Equations], Point 2
- = ASSERT ( not (isGiven fl) )
+ = ASSERT ( not (isGivenOrSolved fl) )
(cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis))
dflt_funeq (cts_in, fun_eq_binds) ct
projects / ghc-hetmet.git / commitdiff