Introducing a datatype for WorkLists that properly prioritizes equalities.
[ghc.git] / compiler / typecheck / TcCanonical.lhs
index 861b262..59cc736 100644 (file)
@@ -1,7 +1,8 @@
 \begin{code}
 module TcCanonical(
-    mkCanonical, mkCanonicals, mkCanonicalFEV, canWanteds, canGivens,
-    canOccursCheck, canEq
+    mkCanonical, mkCanonicals, mkCanonicalFEV, mkCanonicalFEVs, canWanteds, canGivens,
+    canOccursCheck, canEqToWorkList,
+    rewriteWithFunDeps
  ) where
 
 #include "HsVersions.h"
@@ -9,7 +10,8 @@ module TcCanonical(
 import BasicTypes
 import Type
 import TcRnTypes
-
+import FunDeps
+import qualified TcMType as TcM
 import TcType
 import TcErrors
 import Coercion
@@ -18,6 +20,7 @@ import TyCon
 import TypeRep
 import Name
 import Var
+import VarEnv          ( TidyEnv )
 import Outputable
 import Control.Monad    ( unless, when, zipWithM, zipWithM_ )
 import MonadUtils
@@ -28,6 +31,7 @@ import Bag
 
 import HsBinds
 import TcSMonad
+import FastString
 \end{code}
 
 Note [Canonicalisation]
@@ -158,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
@@ -214,28 +218,35 @@ flattenPred ctxt (EqPred ty1 ty2)
 %************************************************************************
 
 \begin{code}
-canWanteds :: [WantedEvVar] -> TcS CanonicalCts 
-canWanteds = fmap andCCans . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev)
+canWanteds :: [WantedEvVar] -> TcS WorkList
+canWanteds = fmap unionWorkLists . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev)
 
-canGivens :: GivenLoc -> [EvVar] -> TcS CanonicalCts
+canGivens :: GivenLoc -> [EvVar] -> TcS WorkList
 canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc)) givens
-                          ; return (andCCans ccs) }
+                          ; return (unionWorkLists ccs) }
 
-mkCanonicals :: CtFlavor -> [EvVar] -> TcS CanonicalCts 
-mkCanonicals fl vs = fmap andCCans (mapM (mkCanonical fl) vs)
+mkCanonicals :: CtFlavor -> [EvVar] -> TcS WorkList
+mkCanonicals fl vs = fmap unionWorkLists (mapM (mkCanonical fl) vs)
 
-mkCanonicalFEV :: FlavoredEvVar -> TcS CanonicalCts
+mkCanonicalFEV :: FlavoredEvVar -> TcS WorkList
 mkCanonicalFEV (EvVarX ev fl) = mkCanonical fl ev
 
-mkCanonical :: CtFlavor -> EvVar -> TcS CanonicalCts
+mkCanonicalFEVs :: Bag FlavoredEvVar -> TcS WorkList
+mkCanonicalFEVs = foldrBagM canon_one emptyWorkList
+  where        -- Preserves order (shouldn't be important, but curently
+               --                  is important for the vectoriser)
+    canon_one fev wl = do { wl' <- mkCanonicalFEV fev
+                          ; return (unionWorkList wl' wl) }
+
+mkCanonical :: CtFlavor -> EvVar -> TcS WorkList
 mkCanonical fl ev = case evVarPred ev of 
-                        ClassP clas tys -> canClass fl ev clas tys 
-                        IParam ip ty    -> canIP    fl ev ip ty
-                        EqPred ty1 ty2  -> canEq    fl ev ty1 ty2 
+                        ClassP clas tys -> canClassToWorkList fl ev clas tys 
+                        IParam ip ty    -> canIPToWorkList    fl ev ip ty 
+                        EqPred ty1 ty2  -> canEqToWorkList    fl ev ty1 ty2 
                          
 
-canClass :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS CanonicalCts 
-canClass fl v cn tys 
+canClassToWorkList :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS WorkList
+canClassToWorkList fl v cn tys 
   = do { (xis,cos,ccs) <- flattenMany fl tys  -- cos :: xis ~ tys
        ; let no_flattening_happened = isEmptyCCan ccs
              dict_co = mkTyConCoercion (classTyCon cn) cos
@@ -252,13 +263,15 @@ canClass fl v cn tys
        -- Add the superclasses of this one here, See Note [Adding superclasses]. 
        -- But only if we are not simplifying the LHS of a rule. 
        ; sctx <- getTcSContext
-       ; sc_cts <- if simplEqsOnly sctx then return emptyCCan 
+       ; sc_cts <- if simplEqsOnly sctx then return emptyWorkList
                    else newSCWorkFromFlavored v_new fl cn xis
 
-       ; return (sc_cts `andCCan` ccs `extendCCans` CDictCan { cc_id     = v_new
-                                                             , cc_flavor = fl
-                                                             , cc_class  = cn 
-                                                             , cc_tyargs = xis }) }
+       ; return (sc_cts `unionWorkList` 
+                 workListFromEqs ccs `unionWorkList` 
+                 workListFromNonEq CDictCan { cc_id     = v_new
+                                           , cc_flavor = fl
+                                           , cc_class  = cn 
+                                           , cc_tyargs = xis }) }
 \end{code}
 
 Note [Adding superclasses]
@@ -326,12 +339,12 @@ happen.
 
 \begin{code}
 
-newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS CanonicalCts
+newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS WorkList
 -- Returns superclasses, see Note [Adding superclasses]
 newSCWorkFromFlavored ev orig_flavor cls xis 
   | isDerived orig_flavor 
-  = return emptyCCan  -- Deriveds don't yield more superclasses because we will
-                      -- add them transitively in the case of wanteds. 
+  = return emptyWorkList  -- Deriveds don't yield more superclasses because we will
+                          -- add them transitively in the case of wanteds. 
 
   | isGiven orig_flavor 
   = do { let sc_theta = immSuperClasses cls xis 
@@ -341,8 +354,8 @@ newSCWorkFromFlavored ev orig_flavor cls xis
        ; mkCanonicals flavor sc_vars }
 
   | isEmptyVarSet (tyVarsOfTypes xis) 
-  = return emptyCCan -- Wanteds with no variables yield no deriveds.
-                     -- See Note [Improvement from Ground Wanteds]
+  = return emptyWorkList -- Wanteds with no variables yield no deriveds.
+                         -- See Note [Improvement from Ground Wanteds]
 
   | otherwise -- Wanted case, just add those SC that can lead to improvement. 
   = do { let sc_rec_theta = transSuperClasses cls xis 
@@ -362,21 +375,25 @@ is_improvement_pty _ = False
 
 
 
-canIP :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS CanonicalCts
+canIPToWorkList :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS WorkList
 -- See Note [Canonical implicit parameter constraints] to see why we don't 
 -- immediately canonicalize (flatten) IP constraints. 
-canIP fl v nm ty 
-  = return $ singleCCan $ CIPCan { cc_id = v
-                                 , cc_flavor = fl
-                                 , cc_ip_nm = nm
-                                 , cc_ip_ty = ty } 
+canIPToWorkList fl v nm ty 
+  = return $ workListFromNonEq (CIPCan { cc_id = v
+                                      , cc_flavor = fl
+                                      , cc_ip_nm = nm
+                                      , cc_ip_ty = ty })
 
 -----------------
+canEqToWorkList :: CtFlavor -> EvVar -> Type -> Type -> TcS WorkList
+canEqToWorkList fl cv ty1 ty2 = do { cts <- canEq fl cv ty1 ty2 
+                         ; return $ workListFromEqs cts }
+
 canEq :: CtFlavor -> EvVar -> Type -> Type -> TcS CanonicalCts 
 canEq fl cv ty1 ty2 
   | tcEqType ty1 ty2   -- Dealing with equality here avoids
                        -- later spurious occurs checks for a~a
-  = do { when (isWanted fl) (setWantedCoBind cv ty1)
+  = do { when (isWanted fl) (setCoBind cv ty1)
        ; return emptyCCan }
 
 -- If one side is a variable, orient and flatten, 
@@ -404,12 +421,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 
@@ -435,9 +452,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) } 
 
@@ -459,16 +476,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 
@@ -488,8 +505,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 } 
 
@@ -509,9 +526,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) } 
 
@@ -731,8 +748,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))
@@ -770,7 +787,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
@@ -778,7 +795,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)
@@ -816,8 +833,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')
@@ -991,4 +1008,91 @@ a.  If this turns out to be impossible, we next try expanding F
 itself, and so on.
 
 
+%************************************************************************
+%*                                                                      *
+%*          Functional dependencies, instantiation of equations
+%*                                                                      *
+%************************************************************************
 
+When we spot an equality arising from a functional dependency,
+we now use that equality (a "wanted") to rewrite the work-item
+constraint right away.  This avoids two dangers
+
+ Danger 1: If we send the original constraint on down the pipeline
+           it may react with an instance declaration, and in delicate
+          situations (when a Given overlaps with an instance) that
+          may produce new insoluble goals: see Trac #4952
+
+ Danger 2: If we don't rewrite the constraint, it may re-react
+           with the same thing later, and produce the same equality
+           again --> termination worries.
+
+To achieve this required some refactoring of FunDeps.lhs (nicer
+now!).  
+
+\begin{code}
+rewriteWithFunDeps :: [Equation]
+                   -> [Xi] -> CtFlavor
+                   -> TcS (Maybe ([Xi], [Coercion], WorkList))
+rewriteWithFunDeps eqn_pred_locs xis fl
+ = do { fd_ev_poss <- mapM (instFunDepEqn fl) eqn_pred_locs
+      ; let fd_ev_pos :: [(Int,FlavoredEvVar)]
+            fd_ev_pos = concat fd_ev_poss
+            (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
+      ; fds <- mapM (\(_,fev) -> mkCanonicalFEV fev) fd_ev_pos
+      ; let fd_work = unionWorkLists fds
+      ; if isEmptyWorkList fd_work 
+        then return Nothing
+        else return (Just (rewritten_xis, cos, fd_work)) }
+
+instFunDepEqn :: CtFlavor -- Precondition: Only Wanted or Derived
+              -> Equation
+              -> TcS [(Int, FlavoredEvVar)]
+-- Post: Returns the position index as well as the corresponding FunDep equality
+instFunDepEqn fl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
+                        , fd_pred1 = d1, fd_pred2 = d2 })
+  = do { let tvs = varSetElems qtvs
+       ; tvs' <- mapM instFlexiTcS tvs
+       ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
+       ; mapM (do_one subst) eqs }
+  where 
+    fl' = case fl of 
+             Given _     -> panic "mkFunDepEqns"
+             Wanted  loc -> Wanted  (push_ctx loc)
+             Derived loc -> Derived (push_ctx loc)
+
+    push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
+
+    do_one subst (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
+       = do { let sty1 = substTy subst ty1
+                  sty2 = substTy subst ty2
+            ; ev <- newCoVar sty1 sty2
+            ; return (i, mkEvVarX ev fl') }
+
+rewriteDictParams :: [(Int,FlavoredEvVar)] -- A set of coercions : (pos, ty' ~ ty)
+                  -> [Type]                -- A sequence of types: tys
+                  -> [(Type,Coercion)]     -- Returns            : [(ty', co : ty' ~ ty)]
+rewriteDictParams param_eqs tys
+  = zipWith do_one tys [0..]
+  where
+    do_one :: Type -> Int -> (Type,Coercion)
+    do_one ty n = case lookup n param_eqs of
+                    Just wev -> (get_fst_ty wev, mkCoVarCoercion (evVarOf wev))
+                    Nothing  -> (ty,ty)                -- Identity
+
+    get_fst_ty wev = case evVarOfPred wev of
+                          EqPred ty1 _ -> ty1
+                          _ -> panic "rewriteDictParams: non equality fundep"
+
+mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
+         -> TcM (TidyEnv, SDoc)
+mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
+  = do  { zpred1 <- TcM.zonkTcPredType pred1
+        ; zpred2 <- TcM.zonkTcPredType pred2
+       ; let { tpred1 = tidyPred tidy_env zpred1
+              ; tpred2 = tidyPred tidy_env zpred2 }
+       ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
+                         nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]), 
+                         nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
+       ; return (tidy_env, msg) }
+\end{code}
\ No newline at end of file