Commit d1796b52 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com

Fix another fundep error (fixes Trac #4969)

If I had a pound for every hour Dimitrios and I have spent
making functional dependencies work right, we'd be rich!

We had stupidly caused a 'wanted' to be rewritten by a 'derived', with
resulting abject failure.  As well as fixing the bug, this patch
refactors some more, adds useful assert and comments.
parent 4c53d93a
......@@ -162,7 +162,7 @@ flatten fl (TyConApp tc tys)
; return $ (mkCoVarCoercion cv, rhs_var, ct) }
else -- Derived or Wanted: make a new *unification* flatten variable
do { rhs_var <- newFlexiTcSTy (typeKind fam_ty)
; cv <- newWantedCoVar fam_ty rhs_var
; cv <- newCoVar fam_ty rhs_var
; let ct = CFunEqCan { cc_id = cv
, cc_flavor = mkWantedFlavor fl
-- Always Wanted, not Derived
......@@ -380,7 +380,7 @@ canEq :: CtFlavor -> EvVar -> Type -> Type -> TcS CanonicalCts
canEq fl cv ty1 ty2
| tcEqType ty1 ty2 -- Dealing with equality here avoids
-- later spurious occurs checks for a~a
= do { when (isWanted fl) (setWantedCoBind cv ty1)
= do { when (isWanted fl) (setCoBind cv ty1)
; return emptyCCan }
-- If one side is a variable, orient and flatten,
......@@ -408,12 +408,12 @@ canEq fl cv s1 s2
Just (t2a,t2b,t2c) <- splitCoPredTy_maybe s2
= do { (v1,v2,v3)
<- if isWanted fl then -- Wanted
do { v1 <- newWantedCoVar t1a t2a
; v2 <- newWantedCoVar t1b t2b
; v3 <- newWantedCoVar t1c t2c
do { v1 <- newCoVar t1a t2a
; v2 <- newCoVar t1b t2b
; v3 <- newCoVar t1c t2c
; let res_co = mkCoPredCo (mkCoVarCoercion v1)
(mkCoVarCoercion v2) (mkCoVarCoercion v3)
; setWantedCoBind cv res_co
; setCoBind cv res_co
; return (v1,v2,v3) }
else if isGiven fl then -- Given
let co_orig = mkCoVarCoercion cv
......@@ -439,9 +439,9 @@ canEq fl cv s1 s2
canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
= do { (argv, resv) <-
if isWanted fl then
do { argv <- newWantedCoVar s1 s2
; resv <- newWantedCoVar t1 t2
; setWantedCoBind cv $
do { argv <- newCoVar s1 s2
; resv <- newCoVar t1 t2
; setCoBind cv $
mkFunCoercion (mkCoVarCoercion argv) (mkCoVarCoercion resv)
; return (argv,resv) }
......@@ -463,16 +463,16 @@ canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
canEq fl cv (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2))
| n1 == n2
= if isWanted fl then
do { v <- newWantedCoVar t1 t2
; setWantedCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv)
do { v <- newCoVar t1 t2
; setCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv)
; canEq fl v t1 t2 }
else return emptyCCan -- DV: How to decompose given IP coercions?
canEq fl cv (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2))
| c1 == c2
= if isWanted fl then
do { vs <- zipWithM newWantedCoVar tys1 tys2
; setWantedCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs)
do { vs <- zipWithM newCoVar tys1 tys2
; setCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs)
; andCCans <$> zipWith3M (canEq fl) vs tys1 tys2
}
else return emptyCCan
......@@ -492,8 +492,8 @@ canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2)
= -- Generate equalities for each of the corresponding arguments
do { argsv
<- if isWanted fl then
do { argsv <- zipWithM newWantedCoVar tys1 tys2
; setWantedCoBind cv $
do { argsv <- zipWithM newCoVar tys1 tys2
; setCoBind cv $
mkTyConCoercion tc1 (map mkCoVarCoercion argsv)
; return argsv }
......@@ -513,9 +513,9 @@ canEq fl cv ty1 ty2
, Just (s2,t2) <- tcSplitAppTy_maybe ty2
= do { (cv1,cv2) <-
if isWanted fl
then do { cv1 <- newWantedCoVar s1 s2
; cv2 <- newWantedCoVar t1 t2
; setWantedCoBind cv $
then do { cv1 <- newCoVar s1 s2
; cv2 <- newCoVar t1 t2
; setCoBind cv $
mkAppCoercion (mkCoVarCoercion cv1) (mkCoVarCoercion cv2)
; return (cv1,cv2) }
......@@ -735,8 +735,8 @@ canEqLeaf :: TcsUntouchables
canEqLeaf _untch fl cv cls1 cls2
| cls1 `re_orient` cls2
= do { cv' <- if isWanted fl
then do { cv' <- newWantedCoVar s2 s1
; setWantedCoBind cv $ mkSymCoercion (mkCoVarCoercion cv')
then do { cv' <- newCoVar s2 s1
; setCoBind cv $ mkSymCoercion (mkCoVarCoercion cv')
; return cv' }
else if isGiven fl then
newGivenCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv))
......@@ -774,7 +774,7 @@ canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1
; cv_new <- if no_flattening_happened then return cv
else if isGiven fl then return cv
else if isWanted fl then
do { cv' <- newWantedCoVar (unClassify (FunCls fn xis1)) xi2
do { cv' <- newCoVar (unClassify (FunCls fn xis1)) xi2
-- cv' : F xis ~ xi2
; let -- fun_co :: F xis1 ~ F tys1
fun_co = mkTyConCoercion fn cos1
......@@ -782,7 +782,7 @@ canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1
want_co = mkSymCoercion fun_co
`mkTransCoercion` mkCoVarCoercion cv'
`mkTransCoercion` co2
; setWantedCoBind cv want_co
; setCoBind cv want_co
; return cv' }
else -- Derived
newDerivedId (EqPred (unClassify (FunCls fn xis1)) xi2)
......@@ -820,8 +820,8 @@ canEqLeafTyVarLeft fl cv tv s2 -- cv : tv ~ s2
; cv_new <- if no_flattening_happened then return cv
else if isGiven fl then return cv
else if isWanted fl then
do { cv' <- newWantedCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2
; setWantedCoBind cv (mkCoVarCoercion cv' `mkTransCoercion` co)
do { cv' <- newCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2
; setCoBind cv (mkCoVarCoercion cv' `mkTransCoercion` co)
; return cv' }
else -- Derived
newDerivedId (EqPred (mkTyVarTy tv) xi2')
......
This diff is collapsed.
......@@ -26,7 +26,7 @@ module TcMType (
--------------------------------
-- Creating new evidence variables
newEvVar, newCoVar, newEvVars,
newWantedCoVar, writeWantedCoVar, readWantedCoVar,
writeWantedCoVar, readWantedCoVar,
newIP, newDict, newSilentGiven, isSilentEvVar,
newWantedEvVar, newWantedEvVars,
......@@ -129,16 +129,13 @@ newEvVars :: TcThetaType -> TcM [EvVar]
newEvVars theta = mapM newEvVar theta
newWantedEvVar :: TcPredType -> TcM EvVar
newWantedEvVar (EqPred ty1 ty2) = newWantedCoVar ty1 ty2
newWantedEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
newWantedEvVar (ClassP cls tys) = newDict cls tys
newWantedEvVar (IParam ip ty) = newIP ip ty
newWantedEvVars :: TcThetaType -> TcM [EvVar]
newWantedEvVars theta = mapM newWantedEvVar theta
newWantedCoVar :: TcType -> TcType -> TcM CoVar
newWantedCoVar ty1 ty2 = newCoVar ty1 ty2
--------------
newEvVar :: TcPredType -> TcM EvVar
-- Creates new *rigid* variables for predicates
......
......@@ -26,13 +26,12 @@ module TcSMonad (
SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
-- Creation of evidence variables
newEvVar, newCoVar, newWantedCoVar, newGivenCoVar,
newEvVar, newCoVar, newGivenCoVar,
newDerivedId,
newIPVar, newDictVar, newKindConstraint,
-- Setting evidence variables
setWantedCoBind,
setIPBind, setDictBind, setEvBind,
setCoBind, setIPBind, setDictBind, setEvBind,
setWantedTyBind,
......@@ -290,12 +289,14 @@ canSolve :: CtFlavor -> CtFlavor -> Bool
-- active(tv ~ xi) = tv
-- active(D xis) = D xis
-- active(IP nm ty) = nm
--
-- NB: either (a `canSolve` b) or (b `canSolve` a) must hold
-----------------------------------------
canSolve (Given {}) _ = True
canSolve (Derived {}) (Wanted {}) = False -- DV: changing the semantics
canSolve (Derived {}) (Derived {}) = True -- DV: changing the semantics of derived
canSolve (Wanted {}) (Derived {}) = True
canSolve (Wanted {}) (Wanted {}) = True
canSolve _ _ = False
canSolve (Derived {}) (Derived {}) = True -- Important: derived can't solve wanted/given
canSolve _ _ = False -- (There is no *evidence* for a derived.)
canRewrite :: CtFlavor -> CtFlavor -> Bool
-- canRewrite ctid1 ctid2
......@@ -548,10 +549,8 @@ getTcEvBindsBag
= do { EvBindsVar ev_ref _ <- getTcEvBinds
; wrapTcS $ TcM.readTcRef ev_ref }
setWantedCoBind :: CoVar -> Coercion -> TcS ()
setWantedCoBind cv co
= setEvBind cv (EvCoercion co)
-- Was: wrapTcS $ TcM.writeWantedCoVar cv co
setCoBind :: CoVar -> Coercion -> TcS ()
setCoBind cv co = setEvBind cv (EvCoercion co)
setWantedTyBind :: TcTyVar -> TcType -> TcS ()
-- Add a type binding
......@@ -706,7 +705,7 @@ newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
newKindConstraint tv knd
= do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
; let ty_k = mkTyVarTy tv_k
; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
; co_var <- newCoVar (mkTyVarTy tv) ty_k
; return co_var }
instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
......@@ -737,9 +736,6 @@ newGivenCoVar ty1 ty2 co
; setEvBind cv (EvCoercion co)
; return cv }
newWantedCoVar :: TcType -> TcType -> TcS EvVar
newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
newCoVar :: TcType -> TcType -> TcS EvVar
newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
......
......@@ -982,7 +982,7 @@ solveCTyFunEqs cts
; return (niFixTvSubst ni_subst, unsolved_can_cts) }
where
solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setWantedCoBind cv ty
solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setCoBind cv ty
------------
type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
......
......@@ -520,7 +520,7 @@ uType, uType_np, uType_defer
-- See Note [Deferred unification]
uType_defer (item : origin) ty1 ty2
= wrapEqCtxt origin $
do { co_var <- newWantedCoVar ty1 ty2
do { co_var <- newCoVar ty1 ty2
; loc <- getCtLoc (TypeEqOrigin item)
; emitFlat (mkEvVarX co_var loc)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment