Introducing:
authorDimitrios Vytiniotis <dimitris@microsoft.com>
Tue, 17 May 2011 16:24:50 +0000 (17:24 +0100)
committerDimitrios Vytiniotis <dimitris@microsoft.com>
Tue, 17 May 2011 16:24:50 +0000 (17:24 +0100)
   1) Postponing the application of instances when there
      is a possibility of a given matching. With the addition
      of prioritizing equalities this fixes #5002 and #4981.

   2) Implemented caching of flattening in constraint
      simplification. This improves efficiency (fixes #5030)

   3) Simplified pushing of unsolved wanteds
      (now pushing only equalities) inside implications.

compiler/typecheck/Inst.lhs
compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcErrors.lhs
compiler/typecheck/TcInstDcls.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcRnTypes.lhs
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcSimplify.lhs

index bbdf21b..05edde4 100644 (file)
@@ -551,7 +551,7 @@ tidyFlavoredEvVar env (EvVarX v fl)
   = 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
@@ -595,8 +595,8 @@ substFlavoredEvVar subst (EvVarX v fl)
   = 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
index 59cc736..435cfc4 100644 (file)
@@ -92,6 +92,7 @@ expansions contain any type function applications would speed things
 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)
@@ -139,7 +140,7 @@ flatten fl (TyConApp tc tys)
   -- 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
@@ -148,33 +149,40 @@ flatten fl (TyConApp tc tys)
                 -- in which case the remaining arguments should
                 -- be dealt with by AppTys
                fam_ty = mkTyConApp tc xi_args 
-               fam_co = 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 $ (mkCoVarCoercion 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 $ (mkCoVarCoercion cv, rhs_var, ct) }
-
+               fam_co = fam_ty -- identity
+         ; (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
+                               ; 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 
+                               ; 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
+                               ; 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
-                  , ccs `extendCCans` ct) }
+                                   `mkTransCoercion` mkTyConCoercion tc cos_args) cos_rest
+                  , ccs `andCCan` ct) }
 
 
 flatten ctxt (PredTy pred) 
@@ -222,7 +230,7 @@ canWanteds :: [WantedEvVar] -> TcS WorkList
 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
@@ -238,6 +246,7 @@ mkCanonicalFEVs = foldrBagM canon_one emptyWorkList
     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 
@@ -250,13 +259,13 @@ 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
-       ; v_new <- if no_flattening_happened then return v
-                  else if isGiven fl        then return v
+       ; v_new <- if no_flattening_happened  then return v
+                  else if isGivenOrSolved fl then return v
                          -- The cos are all identities if fl=Given,
                          -- hence nothing to do
                   else do { v' <- newDictVar cn xis  -- D xis
                           ; when (isWanted fl) $ setDictBind v  (EvCast v' dict_co)
-                          ; when (isGiven fl)  $ setDictBind v' (EvCast v (mkSymCoercion dict_co))
+                          ; when (isGivenOrSolved fl) $ setDictBind v' (EvCast v (mkSymCoercion dict_co))
                                  -- NB: No more setting evidence for derived now 
                           ; return v' }
 
@@ -320,7 +329,7 @@ For Deriveds:
 
 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
 
@@ -346,14 +355,18 @@ newSCWorkFromFlavored ev orig_flavor cls xis
   = 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]
 
@@ -428,7 +441,7 @@ canEq fl cv s1 s2
                                         (mkCoVarCoercion v2) (mkCoVarCoercion v3)
                        ; setCoBind cv res_co
                        ; return (v1,v2,v3) }
-                else if isGiven fl then               -- Given 
+                else if isGivenOrSolved fl then       -- Given 
                          let co_orig = mkCoVarCoercion cv 
                              coa = mkCsel1Coercion co_orig
                              cob = mkCsel2Coercion co_orig
@@ -458,7 +471,7 @@ canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
                       mkFunCoercion (mkCoVarCoercion argv) (mkCoVarCoercion resv) 
                     ; return (argv,resv) } 
 
-             else if isGiven fl then 
+             else if isGivenOrSolved fl then 
                       let [arg,res] = decomposeCo 2 (mkCoVarCoercion cv) 
                       in do { argv <- newGivenCoVar s1 s2 arg 
                             ; resv <- newGivenCoVar t1 t2 res
@@ -510,7 +523,7 @@ canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2)
                          mkTyConCoercion tc1 (map mkCoVarCoercion argsv)
                        ; return argsv } 
 
-                else if isGiven fl then 
+                else if isGivenOrSolved fl then 
                     let cos = decomposeCo (length tys1) (mkCoVarCoercion cv) 
                     in zipWith3M newGivenCoVar tys1 tys2 cos
 
@@ -532,7 +545,7 @@ canEq fl cv ty1 ty2
                        mkAppCoercion (mkCoVarCoercion cv1) (mkCoVarCoercion cv2) 
                      ; return (cv1,cv2) } 
 
-             else if isGiven fl then 
+             else if isGivenOrSolved fl then 
                     let co1 = mkLeftCoercion  $ mkCoVarCoercion cv 
                         co2 = mkRightCoercion $ mkCoVarCoercion cv
                     in do { cv1 <- newGivenCoVar s1 s2 co1 
@@ -751,7 +764,7 @@ canEqLeaf _untch fl cv cls1 cls2
                 then do { cv' <- newCoVar s2 s1 
                         ; setCoBind cv $ mkSymCoercion (mkCoVarCoercion cv') 
                         ; return cv' } 
-                else if isGiven fl then 
+                else if isGivenOrSolved fl then
                          newGivenCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv))
                 else -- Derived
                     newDerivedId (EqPred s2 s1)
@@ -784,8 +797,8 @@ canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2         -- cv : F tys1
                                                  -- co2  :: xi2 ~ s2
        ; let ccs = ccs1 `andCCan` ccs2
              no_flattening_happened = isEmptyCCan ccs
-       ; cv_new <- if no_flattening_happened then return cv
-                   else if isGiven fl        then return cv
+       ; 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
@@ -830,8 +843,8 @@ canEqLeafTyVarLeft fl cv tv s2       -- cv : tv ~ s2
            Nothing   -> canEqFailure fl cv ;
            Just xi2' ->
     do { let no_flattening_happened = isEmptyCCan ccs2
-       ; cv_new <- if no_flattening_happened then return cv
-                   else if isGiven fl        then return cv
+       ; 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)
@@ -1057,7 +1070,7 @@ instFunDepEqn fl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
        ; 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)
 
index 645c43a..0383e76 100644 (file)
@@ -16,6 +16,7 @@ import TcSMonad
 import TcType
 import TypeRep
 import Type( isTyVarTy )
+import Unify ( tcMatchTys )
 
 import Inst
 import InstEnv
@@ -106,7 +107,7 @@ reportTidyWanteds ctxt (WC { wc_flat = flats, wc_insol = insols, wc_impl = impli
                        -- 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
@@ -154,7 +155,8 @@ reportInsoluble ctxt (EvVarX ev flav)
   | 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
@@ -420,18 +422,18 @@ couldNotDeduce :: [([EvVar], GivenLoc)] -> (ThetaType, CtOrigin) -> SDoc
 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
@@ -577,6 +579,18 @@ reportOverlap ctxt inst_envs orig pred@(ClassP clas tys)
                                <+> pprPred 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
@@ -584,11 +598,39 @@ reportOverlap ctxt inst_envs orig pred@(ClassP clas tys)
                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")])]
+                             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
 
 ----------------------
@@ -834,9 +876,9 @@ flattenForAllErrorTcS fl ty _bad_eqs
 
 \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}
 
 %************************************************************************
index 3bb27a7..ecdda43 100644 (file)
@@ -621,6 +621,9 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
     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
@@ -699,7 +702,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
                  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
index fb6929a..46eece8 100644 (file)
@@ -12,6 +12,7 @@ import BasicTypes
 import TcCanonical
 import VarSet
 import Type
+import Unify
 
 import Id 
 import Var
@@ -30,6 +31,7 @@ import Coercion
 import Outputable
 
 import TcRnTypes
+import TcMType ( isSilentEvVar )
 import TcErrors
 import TcSMonad
 import Bag
@@ -68,8 +70,11 @@ An InertSet is a bag of canonical constraints, with the following invariants:
     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. 
@@ -192,7 +197,7 @@ extractUnsolved is@(IS {inert_eqs = eqs})
                         , 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) 
@@ -327,7 +332,7 @@ solveInteractGiven inert gloc evs
                            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
@@ -410,6 +415,8 @@ dischargeFromCCans cans ev fl
     discharge_ct ct _rest
       | evVarPred (cc_id ct) `tcEqPred` 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) 
                 -- Deriveds need no evidence
                 -- For Givens, we already have evidence, and we don't need it twice 
@@ -531,7 +538,7 @@ spontaneousSolveStage depth workItem inerts
                            , 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.
@@ -572,7 +579,7 @@ data SPSolveResult = SPCantSolve | SPSolved WorkItem | SPError
 --                 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
@@ -729,9 +736,8 @@ solveWithIdentity cv wd tv xi
 
        ; when (isWanted wd) (setCoBind cv 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}
 
@@ -931,7 +937,7 @@ doInteractWithInert
   | cls1 == cls2 && (and $ zipWith tcEqType 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
@@ -1035,7 +1041,7 @@ doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_i
 -- 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
@@ -1096,6 +1102,13 @@ doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
                                , 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) 
+  , Just GivenSolved <- isGiven_maybe fl1 
+  = mkIRContinue "Funeq/Funeq" workItem DropInert emptyWorkList
+  | tc1 == tc2 && and (zipWith tcEqType 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) 
        ; mkIRStopK "FunEq/FunEq" cans } 
@@ -1291,6 +1304,10 @@ solveOneFromTheOther info (ev_term,ifl) workItem
                  -- 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
@@ -1665,33 +1682,34 @@ data TopInteractResult
                                         -- 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 
        } 
 
@@ -1699,7 +1717,7 @@ allowedTopReaction :: Bool -> WorkItem -> Bool
 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. 
@@ -1707,12 +1725,12 @@ doTopReact :: WorkItem -> TcS TopInteractResult
 
 -- 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)
@@ -1726,10 +1744,10 @@ doTopReact workItem@(CDictCan { cc_flavor = fl@(Derived 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)
@@ -1755,7 +1773,7 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc)
                   -- 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
@@ -1764,25 +1782,29 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc)
                                          , 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)
@@ -1791,24 +1813,40 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
                            -- appears in an error message
                             -- See Note [Type synonym families] in TyCon
                          coe = mkTyConApp coe_tc rep_tys 
-                   ; cv' <- case fl of
-                              Wanted {} -> do { cv' <- newCoVar rhs_ty xi
-                                              ; setCoBind cv $ 
-                                                    coe `mkTransCoercion`
-                                                      mkCoVarCoercion cv'
-                                              ; return cv' }
-                              Given {}   -> newGivenCoVar xi rhs_ty $ 
-                                            mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe 
-                              Derived {} -> newDerivedId (EqPred xi rhs_ty)
-                   ; can_cts <- mkCanonical fl cv'
-                   ; return $ SomeTopInt can_cts Stop }
+                   ; case fl of
+                       Wanted {} -> do { cv' <- newCoVar rhs_ty xi
+                                       ; setCoBind cv $ 
+                                         coe `mkTransCoercion` mkCoVarCoercion 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 
+                                      ; 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}
 
 
@@ -2012,15 +2050,25 @@ data LookupInstResult
   = 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) 
+                            , 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
@@ -2029,7 +2077,7 @@ matchClassInst clas tys loc
        -- (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 []))
@@ -2039,4 +2087,94 @@ matchClassInst clas tys loc
                      ; 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
+
+         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. 
+
+
+
+
index 1d163aa..fb5d8fb 100644 (file)
@@ -627,8 +627,8 @@ zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
 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!
index e511532..40f6a8d 100644 (file)
@@ -40,11 +40,13 @@ module TcRnTypes(
         Implication(..),
         CtLoc(..), ctLocSpan, ctLocOrigin, setCtLocOrigin,
        CtOrigin(..), EqOrigin(..), 
-        WantedLoc, GivenLoc, pushErrCtxt,
+        WantedLoc, GivenLoc, GivenKind(..), pushErrCtxt,
 
         SkolemInfo(..),
 
-        CtFlavor(..), pprFlavorArising, isWanted, isGiven, isDerived,
+        CtFlavor(..), pprFlavorArising, isWanted, 
+        isGivenOrSolved, isGiven_maybe,
+        isDerived,
         FlavoredEvVar,
 
        -- Pretty printing
@@ -923,35 +925,37 @@ pprWantedEvVar        (EvVarX v _)   = pprEvVarWithType v
 
 \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
index 63b3bb8..8a63e86 100644 (file)
@@ -15,13 +15,15 @@ module TcSMonad (
     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 
@@ -39,6 +41,8 @@ module TcSMonad (
 
     setWantedTyBind,
 
+    lookupFlatCacheMap, updateFlatCacheMap,
+
     getInstEnvs, getFamInstEnvs,                -- Getting the environments
     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
     getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
@@ -104,6 +108,8 @@ import Id
 import TcRnTypes
 import Data.IORef
 
+import qualified Data.Map as Map
+
 #ifdef DEBUG
 import StaticFlags( opt_PprStyle_Debug )
 import Control.Monad( when )
@@ -333,11 +339,16 @@ getWantedLoc ct
 
 isWantedCt :: CanonicalCt -> Bool
 isWantedCt ct = isWanted (cc_flavor ct)
-isGivenCt :: CanonicalCt -> Bool
-isGivenCt ct = isGiven (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 
@@ -362,22 +373,27 @@ canRewrite = canSolve
 
 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}
 
 %************************************************************************
@@ -412,10 +428,33 @@ data TcSEnv
                      
       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
+
+instance Ord FunEqHead where
+  FunEqHead (tc1,xis1) `compare` FunEqHead (tc2,xis2) 
+    = case compare tc1 tc2 of 
+        EQ    -> tcCmpTypes xis1 xis2
+        other -> other
+
 type TcsUntouchables = (Untouchables,TcTyVarSet)
 -- Like the TcM Untouchables, 
 -- but records extra TcsTv variables generated during simplification
@@ -512,12 +551,14 @@ runTcS context untouch tcs
   = 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
@@ -544,21 +585,29 @@ nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
                   , 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 -- 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)
@@ -572,14 +621,16 @@ ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule")
 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 
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -602,12 +653,51 @@ getTcSTyBinds = TcS (return . tcs_ty_binds)
 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)
 
index cf41372..0b9bfaf 100644 (file)
@@ -747,22 +747,26 @@ solve_wanteds inert wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol =
                                   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)
@@ -772,15 +776,18 @@ solveNestedImplications just_given_inert unsolved_cans implics
   | 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
@@ -931,6 +938,42 @@ We were not able to solve (a ~w [beta]) but we can't just assume it as
 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
@@ -1029,7 +1072,7 @@ getSolvableCTyFunEqs untch cts
 
       , 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