Now the constraint simplifier solves kind constraints as well.
authorDimitrios Vytiniotis <dimitris@microsoft.com>
Thu, 22 Dec 2011 11:46:53 +0000 (11:46 +0000)
committerDimitrios Vytiniotis <dimitris@microsoft.com>
Thu, 22 Dec 2011 11:46:53 +0000 (11:46 +0000)
compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcErrors.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcSMonad.lhs

index afd9093..dce91b1 100644 (file)
@@ -8,9 +8,6 @@
 
 module TcCanonical(
     canonicalize,
-    canOccursCheck, canEq, canEvVar,
-    rewriteWithFunDeps,
-    emitFDWorkAsWanted, emitFDWorkAsDerived,
     StopOrContinue (..)
  ) where
 
@@ -19,8 +16,6 @@ module TcCanonical(
 import BasicTypes ( IPName )
 import TcErrors
 import TcRnTypes
-import FunDeps
-import qualified TcMType as TcM
 import TcType
 import Type
 import Kind
@@ -32,7 +27,7 @@ import Name ( Name )
 import Var
 import VarEnv
 import Outputable
-import Control.Monad    ( when, unless, zipWithM, foldM )
+import Control.Monad    ( when, unless, zipWithM )
 import MonadUtils
 import Control.Applicative ( (<|>) )
 
@@ -42,7 +37,6 @@ import TcSMonad
 import FastString
 
 import Data.Maybe ( isNothing )
-import Pair ( pSnd )
 
 \end{code}
 
@@ -204,11 +198,13 @@ canonicalize (CIrredEvCan { cc_id = ev, cc_flavor = fl
 
 canEvVar :: EvVar -> PredTree 
          -> SubGoalDepth -> CtFlavor -> TcS StopOrContinue
+-- Called only for non-canonical EvVars 
 canEvVar ev pred_classifier d fl 
   = case pred_classifier of
       ClassPred cls tys -> canClass d fl ev cls tys 
                                         `andWhenContinue` emit_superclasses
-      EqPred ty1 ty2    -> canEq    d fl ev ty1 ty2
+      EqPred ty1 ty2    -> canEq    d fl ev ty1 ty2 
+                                        `andWhenContinue` emit_kind_constraint
       IPPred nm ty      -> canIP    d fl ev nm ty
       IrredPred ev_ty   -> canIrred d fl ev ev_ty
       TuplePred tys     -> canTuple d fl ev tys
@@ -219,9 +215,58 @@ canEvVar ev pred_classifier d fl
           = do { sctxt <- getTcSContext
                ; unless (simplEqsOnly sctxt) $ 
                         newSCWorkFromFlavored d v_new fl cls xis_new
+               -- Arguably we should "seq" the coercions if they are derived, 
+               -- as we do below for emit_kind_constraint, to allow errors in
+               -- superclasses to be executed if deferred to runtime! 
                ; continueWith ct }
         emit_superclasses _ = panic "emit_superclasses of non-class!"
 
+        emit_kind_constraint ct@(CTyEqCan { cc_id = ev, cc_depth = d
+                                          , cc_flavor = fl, cc_tyvar = tv
+                                          , cc_rhs = ty })
+          = do_emit_kind_constraint ct ev d fl (mkTyVarTy tv) ty
+
+        emit_kind_constraint ct@(CFunEqCan { cc_id = ev, cc_depth = d
+                                           , cc_flavor = fl
+                                           , cc_fun = fn, cc_tyargs = xis1
+                                           , cc_rhs = xi2 })
+          = do_emit_kind_constraint ct ev d fl (mkTyConApp fn xis1) xi2
+        emit_kind_constraint ct = continueWith ct
+
+        do_emit_kind_constraint ct eqv d fl ty1 ty2 
+           | compatKind k1 k2 = continueWith ct
+           | otherwise
+           = do { keqv <- forceNewEvVar kind_co_fl (mkEqPred (k1,k2))
+                ; eqv' <- forceNewEvVar fl (mkEqPred (ty1,ty2))
+                ; _fl <- case fl of
+                   Wanted {}-> setEvBind eqv
+                                (mkEvKindCast eqv' (mkTcCoVarCo keqv)) fl
+                   Given {} -> setEvBind eqv'
+                                (mkEvKindCast eqv (mkTcCoVarCo keqv)) fl
+                   Derived {} -> return fl
+
+                ; canEq_ d kind_co_fl keqv k1 k2 -- Emit kind equality
+                ; continueWith (ct { cc_id = eqv' }) }
+           where k1 = typeKind ty1
+                 k2 = typeKind ty2
+                 ctxt = mkKindErrorCtxtTcS ty1 k1 ty2 k2
+                 -- Always create a Wanted kind equality even if 
+                 -- you are decomposing a given constraint.
+                 -- NB: DV finds this reasonable for now. Maybe we 
+                 --  have to revisit.
+                 kind_co_fl
+                   | Given (CtLoc _sk_info src_span err_ctxt) _ <- fl
+                   = let orig = TypeEqOrigin (UnifyOrigin ty1 ty2)
+                         ctloc = pushErrCtxtSameOrigin ctxt $
+                                 CtLoc orig src_span err_ctxt
+                     in Wanted ctloc
+                   | Wanted ctloc <- fl
+                   = Wanted (pushErrCtxtSameOrigin ctxt ctloc)
+                   | Derived ctloc <- fl
+                   = Derived (pushErrCtxtSameOrigin ctxt ctloc)
+                   | otherwise 
+                   = panic "do_emit_kind_constraint: non-CtLoc inside!"
+
 
 -- Tuple canonicalisation
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -555,26 +600,28 @@ flatten :: SubGoalDepth -- Depth
 flatten d ctxt ty 
   | Just ty' <- tcView ty
   = do { (xi, co) <- flatten d ctxt ty'
-       ; return (xi,co) }
-       
-       -- DV: The following is tedious to do but maybe we should return to this
-       -- Preserve type synonyms if possible
-       -- ; if no_flattening
-       --   then return (xi, mkTcReflCo xi,no_flattening) -- Importantly, not xi!
-       --   else return (xi,co,no_flattening) 
-       -- }
-
-flatten d ctxt v@(TyVarTy _)
+       ; return (xi,co) } 
+
+flatten d ctxt (TyVarTy tv)
   = do { ieqs <- getInertEqs
-       ; let co = liftInertEqsTy ieqs ctxt v           -- co : v ~ ty
-             ty = pSnd (tcCoercionKind co)
-       ; if v `eqType` ty then
-             return (ty,mkTcReflCo ty)
-         else -- NB recursive call. Why? See Note [Non-idempotent inert substitution]
-              -- Actually I believe that applying the substition only *twice* will suffice
-         
-             do { (ty_final,co') <- flatten d ctxt ty  -- co' : ty_final ~ ty
-                ; return (ty_final,co' `mkTcTransCo` mkTcSymCo co) } }
+       ; let mco = tv_eq_subst (fst ieqs) tv  -- co : v ~ ty
+       ; case mco of -- Done, but make sure the kind is zonked
+           Nothing -> 
+               do { let knd = tyVarKind tv
+                  ; (new_knd,_kind_co) <- flatten d ctxt knd
+                  ; let ty = mkTyVarTy (setVarType tv new_knd)
+                  ; return (ty, mkTcReflCo ty) }
+           -- NB recursive call. 
+           -- Why? See Note [Non-idempotent inert substitution]
+           -- Actually, I think applying the substition just twice will suffice
+           Just (co,ty) -> 
+               do { (ty_final,co') <- flatten d ctxt ty
+                  ; return (ty_final, co' `mkTcTransCo` mkTcSymCo co) } }  
+  where tv_eq_subst subst tv
+          | Just (ct,co) <- lookupVarEnv subst tv
+          , cc_flavor ct `canRewrite` ctxt
+          = Just (co,cc_rhs ct)
+          | otherwise = Nothing
 
 \end{code}
 
@@ -1106,28 +1153,17 @@ canEqLeafOriented :: SubGoalDepth -- Depth
                   -> TcType -> TcType -> TcS StopOrContinue
 -- By now s1 will either be a variable or a type family application
 canEqLeafOriented d fl eqv s1 s2
-  | let k1 = typeKind s1
-  , let k2 = typeKind s2
-  -- Establish kind invariants for CFunEqCan and CTyEqCan
-  = do { are_compat <- compatKindTcS k1 k2
-       ; can_unify <- if not are_compat
-                      then unifyKindTcS s1 s2 k1 k2
-                      else return False
-         -- If the kinds cannot be unified or are not compatible, don't fail
-         -- right away; instead, emit a frozen error
-       ; if (not are_compat && not can_unify) then
-             canEqFailure d fl eqv
-         else can_eq_kinds_ok d fl eqv s1 s2 }
-
-  where can_eq_kinds_ok d fl eqv s1 s2
+  = can_eq_split_lhs d fl eqv s1 s2
+  where can_eq_split_lhs d fl eqv s1 s2
           | Just (fn,tys1) <- splitTyConApp_maybe s1
           = canEqLeafFunEqLeftRec d fl eqv (fn,tys1) s2
           | Just tv <- getTyVar_maybe s1
           = canEqLeafTyVarLeftRec d fl eqv tv s2
           | otherwise
           = pprPanic "canEqLeafOriented" $
-            text "Non-variable or non-family equality LHS" <+> ppr eqv <+> 
-                                                       dcolon <+> ppr (evVarPred eqv)
+            text "Non-variable or non-family equality LHS" <+> 
+                 ppr eqv <+> dcolon <+> ppr (evVarPred eqv)
+
 canEqLeafFunEqLeftRec :: SubGoalDepth
                       -> CtFlavor 
                       -> EqVar 
@@ -1471,117 +1507,3 @@ we first try expanding each of the ti to types which no longer contain
 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] 
-                   -> WantedLoc 
-                   -> TcS (Maybe ([Xi], [TcCoercion], [(EvVar,WantedLoc)])) 
-                                           -- Not quite a WantedEvVar unfortunately
-                                           -- Because our intention could be to make 
-                                           -- it derived at the end of the day
--- NB: The flavor of the returned EvVars will be decided by the caller
--- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
-rewriteWithFunDeps eqn_pred_locs xis wloc
- = do { fd_ev_poss <- mapM (instFunDepEqn wloc) eqn_pred_locs
-      ; let fd_ev_pos :: [(Int,(EqVar,WantedLoc))]
-            fd_ev_pos = concat fd_ev_poss
-            (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
-      ; if null fd_ev_pos then return Nothing
-        else return (Just (rewritten_xis, cos, map snd fd_ev_pos)) }
-
-instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,(EvVar,WantedLoc))]
--- Post: Returns the position index as well as the corresponding FunDep equality
-instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
-                        , fd_pred1 = d1, fd_pred2 = d2 })
-  = do { let tvs = varSetElems qtvs
-       ; tvs' <- mapM instFlexiTcS tvs  -- IA0_TODO: we might need to do kind substitution
-       ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
-       ; foldM (do_one subst) [] eqs }
-  where 
-    do_one subst ievs (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
-       = let sty1 = Type.substTy subst ty1 
-             sty2 = Type.substTy subst ty2 
-         in if eqType sty1 sty2 then return ievs -- Return no trivial equalities
-            else do { eqv <- newEqVar (Derived wl) sty1 sty2 -- Create derived or cached by deriveds
-                    ; let wl' = push_ctx wl 
-                    ; if isNewEvVar eqv then 
-                          return $ (i,(evc_the_evvar eqv,wl')):ievs 
-                      else -- We are eventually going to emit FD work back in the work list so 
-                           -- it is important that we only return the /freshly created/ and not 
-                           -- some existing equality!
-                          return ievs }
-
-    push_ctx :: WantedLoc -> WantedLoc 
-    push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
-
-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 = tidyType tidy_env zpred1
-              ; tpred2 = tidyType 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) }
-
-rewriteDictParams :: [(Int,(EqVar,WantedLoc))] -- A set of coercions : (pos, ty' ~ ty)
-                  -> [Type]                    -- A sequence of types: tys
-                  -> [(Type, TcCoercion)]      -- Returns: [(ty', co : ty' ~ ty)]
-rewriteDictParams param_eqs tys
-  = zipWith do_one tys [0..]
-  where
-    do_one :: Type -> Int -> (Type, TcCoercion)
-    do_one ty n = case lookup n param_eqs of
-                    Just wev -> (get_fst_ty wev, mkTcCoVarCo (fst wev))
-                    Nothing  -> (ty,             mkTcReflCo ty)        -- Identity
-
-    get_fst_ty (wev,_wloc) 
-      | Just (ty1, _) <- getEqPredTys_maybe (evVarPred wev )
-      = ty1
-      | otherwise 
-      = panic "rewriteDictParams: non equality fundep!?"
-
-        
-emitFDWork :: Bool
-           -> [(EvVar,WantedLoc)] 
-           -> SubGoalDepth -> TcS () 
-emitFDWork as_wanted evlocs d 
-  = updWorkListTcS $ appendWorkListEqs fd_cts
-  where fd_cts = map mk_fd_ct evlocs 
-        mk_fl wl = if as_wanted then (Wanted wl) else (Derived wl)
-        mk_fd_ct (v,wl) = CNonCanonical { cc_id = v
-                                        , cc_flavor = mk_fl wl 
-                                        , cc_depth = d }
-
-emitFDWorkAsDerived, emitFDWorkAsWanted :: [(EvVar,WantedLoc)] 
-                                        -> SubGoalDepth 
-                                        -> TcS () 
-emitFDWorkAsDerived = emitFDWork False
-emitFDWorkAsWanted  = emitFDWork True 
-
-\end{code}
\ No newline at end of file
index 893cd7a..8e86afc 100644 (file)
@@ -23,6 +23,7 @@ import TcSMonad
 import TcType
 import TypeRep
 import Type
+import Kind ( isKind )
 import Class
 import Unify ( tcMatchTys )
 import Inst
@@ -465,8 +466,12 @@ addExtraInfo ctxt ty1 ty2
     extra2 = typeExtraInfoMsg (cec_encl ctxt) ty2
 
 misMatchMsg :: TcType -> TcType -> SDoc           -- Types are already tidy
-misMatchMsg ty1 ty2 = sep [ ptext (sLit "Couldn't match type") <+> quotes (ppr ty1)
-                         , nest 15 $ ptext (sLit "with") <+> quotes (ppr ty2)]
+misMatchMsg ty1 ty2 
+  = sep [ ptext cm_ty_or_knd <+> quotes (ppr ty1)
+       , nest 15 $ ptext (sLit "with") <+> quotes (ppr ty2)]
+  where cm_ty_or_knd
+          | isKind ty1 = sLit "Couldn't match kind"
+          | otherwise  = sLit "Couldn't match type"
 
 kindErrorMsg :: TcType -> TcType -> SDoc   -- Types are already tidy
 kindErrorMsg ty1 ty2
index 45e89a8..b0eca45 100644 (file)
@@ -37,6 +37,8 @@ import FunDeps
 import TcEvidence
 import Outputable
 
+import TcMType ( zonkTcPredType )
+
 import TcRnTypes
 import TcErrors
 import TcSMonad
@@ -431,7 +433,16 @@ kick_out_rewritable ct (IS { inert_eqs    = eqmap
     (fro_out,   fro_in)   = partitionBag rewritable frozen
 
     rewritable ct = (fl `canRewrite` cc_flavor ct)  &&
-                    (tv `elemVarSet` tyVarsOfCt ct)
+                    (tv `elemVarSet` tyVarsOfCt ct) 
+                    -- NB: tyVarsOfCt will return the type 
+                    --     variables /and the kind variables/ that are 
+                    --     directly visible in the type. Hence we will
+                    --     have exposed all the rewriting we care about
+                    --     to make the most precise kinds visible for 
+                    --     matching classes etc. No need to kick out 
+                    --     constraints that mention type variables whose
+                    --     kinds could contain this variable!
+
 \end{code}
 
 Note [Delicate equality kick-out]
@@ -500,15 +511,9 @@ trySpontaneousSolve _ = return SPCantSolve
 trySpontaneousEqOneWay :: SubGoalDepth 
                        -> EqVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
 -- tv is a MetaTyVar, not untouchable
-trySpontaneousEqOneWay d eqv gw tv xi  
-  | not (isSigTyVar tv) || isTyVarTy xi 
-  = do { let kxi = typeKind xi -- NB: 'xi' is fully rewritten according to the inerts 
-                               -- so we have its more specific kind in our hands
-       ; is_sub_kind <- kxi `isSubKindTcS` tyVarKind tv
-       ; if is_sub_kind then
-             solveWithIdentity d eqv gw tv xi
-         else return SPCantSolve
-       }
+trySpontaneousEqOneWay d eqv gw tv xi
+  | not (isSigTyVar tv) || isTyVarTy xi
+  = solveWithIdentity d eqv gw tv xi
   | otherwise -- Still can't solve, sig tyvar and non-variable rhs
   = return SPCantSolve
 
@@ -518,13 +523,10 @@ trySpontaneousEqTwoWay :: SubGoalDepth
 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
 
 trySpontaneousEqTwoWay d eqv gw tv1 tv2
-  = do { k1_sub_k2 <- k1 `isSubKindTcS` k2
+  = do { let k1_sub_k2 = k1 `isSubKind` k2
        ; if k1_sub_k2 && nicer_to_update_tv2
          then solveWithIdentity d eqv gw tv2 (mkTyVarTy tv1)
-         else do
-       { k2_sub_k1 <- k2 `isSubKindTcS` k1
-       ; MASSERT( k2_sub_k1 )  -- they were unified in TcCanonical
-       ; solveWithIdentity d eqv gw tv1 (mkTyVarTy tv2) } }
+         else solveWithIdentity d eqv gw tv1 (mkTyVarTy tv2) }
   where
     k1 = tyVarKind tv1
     k2 = tyVarKind tv2
@@ -771,7 +773,6 @@ doInteractWithInert
                                               , text "Inert item=" <+> ppr inertItem
                                               ]
 
-
 -- Two pieces of irreducible evidence: if their types are *exactly identical* we can
 -- rewrite them. We can never improve using this: if we want ty1 :: Constraint and have
 -- ty2 :: Constraint it clearly does not mean that (ty1 ~ ty2)
@@ -1262,6 +1263,116 @@ When we react a family instance with a type family equation in the work list
 we keep the synonym-using RHS without expansion. 
 
 
+%************************************************************************
+%*                                                                      *
+%*          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] 
+                   -> WantedLoc 
+                   -> TcS (Maybe ([Xi], [TcCoercion], [(EvVar,WantedLoc)])) 
+                                           -- Not quite a WantedEvVar unfortunately
+                                           -- Because our intention could be to make 
+                                           -- it derived at the end of the day
+-- NB: The flavor of the returned EvVars will be decided by the caller
+-- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
+rewriteWithFunDeps eqn_pred_locs xis wloc
+ = do { fd_ev_poss <- mapM (instFunDepEqn wloc) eqn_pred_locs
+      ; let fd_ev_pos :: [(Int,(EqVar,WantedLoc))]
+            fd_ev_pos = concat fd_ev_poss
+            (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
+      ; if null fd_ev_pos then return Nothing
+        else return (Just (rewritten_xis, cos, map snd fd_ev_pos)) }
+
+instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,(EvVar,WantedLoc))]
+-- Post: Returns the position index as well as the corresponding FunDep equality
+instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
+                        , fd_pred1 = d1, fd_pred2 = d2 })
+  = do { let tvs = varSetElems qtvs
+       ; tvs' <- mapM instFlexiTcS tvs  -- IA0_TODO: we might need to do kind substitution
+       ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
+       ; foldM (do_one subst) [] eqs }
+  where 
+    do_one subst ievs (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
+       = let sty1 = Type.substTy subst ty1 
+             sty2 = Type.substTy subst ty2 
+         in if eqType sty1 sty2 then return ievs -- Return no trivial equalities
+            else do { eqv <- newEqVar (Derived wl) sty1 sty2 -- Create derived or cached by deriveds
+                    ; let wl' = push_ctx wl 
+                    ; if isNewEvVar eqv then 
+                          return $ (i,(evc_the_evvar eqv,wl')):ievs 
+                      else -- We are eventually going to emit FD work back in the work list so 
+                           -- it is important that we only return the /freshly created/ and not 
+                           -- some existing equality!
+                          return ievs }
+
+    push_ctx :: WantedLoc -> WantedLoc 
+    push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
+
+mkEqnMsg :: (TcPredType, SDoc) 
+         -> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc)
+mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
+  = do  { zpred1 <- zonkTcPredType pred1
+        ; zpred2 <- zonkTcPredType pred2
+       ; let { tpred1 = tidyType tidy_env zpred1
+              ; tpred2 = tidyType 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) }
+
+rewriteDictParams :: [(Int,(EqVar,WantedLoc))] -- A set of coercions : (pos, ty' ~ ty)
+                  -> [Type]                    -- A sequence of types: tys
+                  -> [(Type, TcCoercion)]      -- Returns: [(ty', co : ty' ~ ty)]
+rewriteDictParams param_eqs tys
+  = zipWith do_one tys [0..]
+  where
+    do_one :: Type -> Int -> (Type, TcCoercion)
+    do_one ty n = case lookup n param_eqs of
+                    Just wev -> (get_fst_ty wev, mkTcCoVarCo (fst wev))
+                    Nothing  -> (ty,             mkTcReflCo ty)        -- Identity
+
+    get_fst_ty (wev,_wloc) 
+      | Just (ty1, _) <- getEqPredTys_maybe (evVarPred wev )
+      = ty1
+      | otherwise 
+      = panic "rewriteDictParams: non equality fundep!?"
+
+        
+emitFDWorkAsDerived :: [(EvVar,WantedLoc)] 
+                    -> SubGoalDepth -> TcS () 
+emitFDWorkAsDerived evlocs d 
+  = updWorkListTcS $ appendWorkListEqs fd_cts
+  where fd_cts = map mk_fd_ct evlocs 
+        mk_fd_ct (v,wl) = CNonCanonical { cc_id = v
+                                        , cc_flavor = Derived wl 
+                                        , cc_depth = d }
+
+
+\end{code}
+
+
+
+
 *********************************************************************************
 *                                                                               * 
                        The top-reaction Stage
@@ -1500,6 +1611,7 @@ Then it is solvable, but its very hard to detect this on the spot.
 It's exactly the same with implicit parameters, except that the
 "aggressive" approach would be much easier to implement.
 
+
 Note [When improvement happens]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We fire an improvement rule when
index 60efee5..aabc737 100644 (file)
@@ -60,7 +60,7 @@ module TcSMonad (
 
         -- Inerts 
     InertSet(..), 
-    getInertEqs, liftInertEqsTy, getCtCoercion,
+    getInertEqs, getCtCoercion,
     emptyInert, getTcSInerts, updInertSet, extractUnsolved,
     extractUnsolvedTcS, modifyInertTcS,
     updInertSetTcS, partitionCCanMap, partitionEqMap,
@@ -72,7 +72,7 @@ module TcSMonad (
     instDFunConstraints,          
     newFlexiTcSTy, instFlexiTcS,
 
-    compatKind, compatKindTcS, isSubKindTcS, unifyKindTcS,
+    compatKind, mkKindErrorCtxtTcS,
 
     TcsUntouchables,
     isTouchableMetaTyVar,
@@ -104,7 +104,7 @@ import qualified TcRnMonad as TcM
 import qualified TcMType as TcM
 import qualified TcEnv as TcM 
        ( checkWellStaged, topIdLvl, tcGetDefaultTys )
-import {-# SOURCE #-} qualified TcUnify as TcM ( unifyKindEq, mkKindErrorCtxt )
+import {-# SOURCE #-} qualified TcUnify as TcM ( mkKindErrorCtxt )
 import Kind
 import TcType
 import DynFlags
@@ -113,7 +113,6 @@ import Type
 import TcEvidence
 import Class
 import TyCon
-import TypeRep 
 
 import Name
 import Var
@@ -145,23 +144,12 @@ import TrieMap
 compatKind :: Kind -> Kind -> Bool
 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 
 
-compatKindTcS :: Kind -> Kind -> TcS Bool
--- Because kind unification happens during constraint solving, we have
--- to make sure that two kinds are zonked before we compare them.
-compatKindTcS k1 k2 = wrapTcS (TcM.compatKindTcM k1 k2)
-
-isSubKindTcS :: Kind -> Kind -> TcS Bool
-isSubKindTcS k1 k2 = wrapTcS (TcM.isSubKindTcM k1 k2)
-
-unifyKindTcS :: Type -> Type     -- Context
-             -> Kind -> Kind     -- Corresponding kinds
-             -> TcS Bool
-unifyKindTcS ty1 ty2 ki1 ki2
-  = wrapTcS $ TcM.addErrCtxtM ctxt $ do
-      (_errs, mb_r) <- TcM.tryTc (TcM.unifyKindEq ki1 ki2)
-      return (maybe False (const True) mb_r)
-  where 
-    ctxt = TcM.mkKindErrorCtxt ty1 ki1 ty2 ki2
+mkKindErrorCtxtTcS :: Type -> Kind 
+                   -> Type -> Kind 
+                   -> ErrCtxt
+mkKindErrorCtxtTcS ty1 ki1 ty2 ki2
+  = (False,TcM.mkKindErrorCtxt ty1 ty2 ki1 ki2)
+
 \end{code}
 
 %************************************************************************
@@ -1506,67 +1494,5 @@ getCtCoercion ct
                 -- Instead we use the most accurate type, given by ctPred c
   where maybe_given = isGiven_maybe (cc_flavor ct)
 
--- See Note [LiftInertEqs]
-liftInertEqsTy :: (TyVarEnv (Ct, TcCoercion),InScopeSet)
-                 -> CtFlavor
-                 -> PredType -> TcCoercion
-liftInertEqsTy (subst,inscope) fl pty
-  = ty_cts_subst subst inscope fl pty
-
-
-ty_cts_subst :: TyVarEnv (Ct, TcCoercion)
-             -> InScopeSet -> CtFlavor -> Type -> TcCoercion
-ty_cts_subst subst inscope fl ty 
-  = go ty 
-  where 
-        go ty = go' ty
-
-        go' (TyVarTy tv)      = tyvar_cts_subst tv `orElse` mkTcReflCo (TyVarTy tv)
-        go' (AppTy ty1 ty2)   = mkTcAppCo (go ty1) (go ty2) 
-        go' (TyConApp tc tys) = mkTcTyConAppCo tc (map go tys)  
-
-        go' (ForAllTy v ty)   = mkTcForAllCo v' $! co
-                             where 
-                               (subst',inscope',v') = upd_tyvar_bndr subst inscope v
-                               co = ty_cts_subst subst' inscope' fl ty 
-
-        go' (FunTy ty1 ty2)   = mkTcFunCo (go ty1) (go ty2)
-
-
-        tyvar_cts_subst tv  
-          | Just (ct,co) <- lookupVarEnv subst tv, cc_flavor ct `canRewrite` fl  
-          = Just co -- Warn: use cached, not cc_id directly, because of alpha-renamings!
-          | otherwise = Nothing 
-
-        upd_tyvar_bndr subst inscope v 
-          = (new_subst, (inscope `extendInScopeSet` new_v), new_v)
-          where new_subst 
-                    | no_change = delVarEnv subst v
-                        -- Otherwise we have to extend the environment with /something/. 
-                        -- But we do not want to monadically create a new EvVar. So, we
-                        -- create an 'unused_ct' but we cache reflexivity as the 
-                        -- associated coercion. 
-                    | otherwise = extendVarEnv subst v (unused_ct, mkTcReflCo (TyVarTy new_v))
-
-                no_change = new_v == v 
-                new_v     = uniqAway inscope v 
-
-                unused_ct = CTyEqCan { cc_id     = unused_evvar
-                                     , cc_flavor = fl -- canRewrite is reflexive.
-                                     , cc_tyvar  = v 
-                                     , cc_rhs    = mkTyVarTy new_v 
-                                     , cc_depth  = unused_depth }
-                unused_depth = panic "ty_cts_subst: This depth should not be accessed!"
-                unused_evvar = panic "ty_cts_subst: This var is just an alpha-renaming!"
-\end{code}
-
-Note [LiftInertEqsTy]
-~~~~~~~~~~~~~~~~~~~~~~~ 
-The function liftInertEqPred behaves almost like liftCoSubst (in
-Coercion), but accepts a map TyVarEnv (Ct,Coercion) instead of a
-LiftCoSubst. This data structure is more convenient to use since we
-must apply the inert substitution /only/ if the inert equality 
-`canRewrite` the work item. There's admittedly some duplication of 
-functionality but it would be more tedious to cache and maintain 
-different flavors of LiftCoSubst structures in the inerts. 
 
+\end{code}
\ No newline at end of file