Merge branch 'master' of http://darcs.haskell.org/ghc

14 files changed, 447 insertions, 371 deletions

diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs
index d44943c347..7cc58583dd 100644
--- a/compiler/deSugar/DsBinds.lhs
+++ b/compiler/deSugar/DsBinds.lhs
@@ -683,7 +683,9 @@ dsEvTerm (EvId v) = Var v
 
 dsEvTerm (EvCast v co) 
   = dsTcCoercion co $ mkCast (Var v) -- 'v' is always a lifted evidence variable so it is
-                                    -- unnecessary to call varToCoreExpr v here.
+                                     -- unnecessary to call varToCoreExpr v here.
+dsEvTerm (EvKindCast v co)
+  = dsTcCoercion co $ (\_ -> Var v)
 
 dsEvTerm (EvDFunApp df tys vars) = Var df `mkTyApps` tys `mkVarApps` vars
 dsEvTerm (EvCoercion co)         = dsTcCoercion co mkEqBox
diff --git a/compiler/main/GHC.hs b/compiler/main/GHC.hs
index 34aacc2113..df670f1d63 100644
--- a/compiler/main/GHC.hs
+++ b/compiler/main/GHC.hs
@@ -84,9 +84,9 @@ module GHC (
 
         -- * Interactive evaluation
         getBindings, getInsts, getPrintUnqual,
-        findModule,
-        lookupModule,
+        findModule, lookupModule,
 #ifdef GHCI
+        isModuleTrusted,
         setContext, getContext, 
         getNamesInScope,
         getRdrNamesInScope,
@@ -1247,26 +1247,32 @@ lookupModule mod_name Nothing = withSession $ \hsc_env -> do
         Found _ m -> return m
         err       -> noModError (hsc_dflags hsc_env) noSrcSpan mod_name err
 
-lookupLoadedHomeModule  :: GhcMonad m => ModuleName -> m (Maybe Module)
+lookupLoadedHomeModule :: GhcMonad m => ModuleName -> m (Maybe Module)
 lookupLoadedHomeModule mod_name = withSession $ \hsc_env ->
   case lookupUFM (hsc_HPT hsc_env) mod_name of
     Just mod_info      -> return (Just (mi_module (hm_iface mod_info)))
     _not_a_home_module -> return Nothing
 
 #ifdef GHCI
+-- | Check that a module is safe to import (according to Safe Haskell).
+--
+-- We return True to indicate the import is safe and False otherwise
+-- although in the False case an error may be thrown first.
+isModuleTrusted :: GhcMonad m => Module -> m Bool
+isModuleTrusted m = withSession $ \hsc_env ->
+    liftIO $ hscCheckSafe hsc_env m noSrcSpan
+
 getHistorySpan :: GhcMonad m => History -> m SrcSpan
 getHistorySpan h = withSession $ \hsc_env ->
-                          return$ InteractiveEval.getHistorySpan hsc_env h
+    return $ InteractiveEval.getHistorySpan hsc_env h
 
 obtainTermFromVal :: GhcMonad m => Int ->  Bool -> Type -> a -> m Term
-obtainTermFromVal bound force ty a =
-    withSession $ \hsc_env ->
-      liftIO $ InteractiveEval.obtainTermFromVal hsc_env bound force ty a
+obtainTermFromVal bound force ty a = withSession $ \hsc_env ->
+    liftIO $ InteractiveEval.obtainTermFromVal hsc_env bound force ty a
 
 obtainTermFromId :: GhcMonad m => Int -> Bool -> Id -> m Term
-obtainTermFromId bound force id =
-    withSession $ \hsc_env ->
-      liftIO $ InteractiveEval.obtainTermFromId hsc_env bound force id
+obtainTermFromId bound force id = withSession $ \hsc_env ->
+    liftIO $ InteractiveEval.obtainTermFromId hsc_env bound force id
 
 #endif
 
diff --git a/compiler/main/HscMain.hs b/compiler/main/HscMain.hs
index c705526118..2882816c0b 100644
--- a/compiler/main/HscMain.hs
+++ b/compiler/main/HscMain.hs
@@ -206,6 +206,9 @@ instance Monad Hsc where
 instance MonadIO Hsc where
     liftIO io = Hsc $ \_ w -> do a <- io; return (a, w)
 
+instance Functor Hsc where
+    fmap f m = m >>= \a -> return $ f a
+
 runHsc :: HscEnv -> Hsc a -> IO a
 runHsc hsc_env (Hsc hsc) = do
     (a, w) <- hsc hsc_env emptyBag
@@ -911,20 +914,18 @@ hscCheckSafeImports tcg_env = do
             text "Rule \"" <> ftext n <> text "\" ignored" $+$
             text "User defined rules are disabled under Safe Haskell"
 
--- | Validate that safe imported modules are actually safe.
--- For modules in the HomePackage (the package the module we
--- are compiling in resides) this just involves checking its
--- trust type is 'Safe' or 'Trustworthy'. For modules that
--- reside in another package we also must check that the
--- external pacakge is trusted. See the Note [Safe Haskell
--- Trust Check] above for more information.
+-- | Validate that safe imported modules are actually safe.  For modules in the
+-- HomePackage (the package the module we are compiling in resides) this just
+-- involves checking its trust type is 'Safe' or 'Trustworthy'. For modules
+-- that reside in another package we also must check that the external pacakge
+-- is trusted. See the Note [Safe Haskell Trust Check] above for more
+-- information.
 --
--- The code for this is quite tricky as the whole algorithm
--- is done in a few distinct phases in different parts of the
--- code base. See RnNames.rnImportDecl for where package trust
--- dependencies for a module are collected and unioned.
--- Specifically see the Note [RnNames . Tracking Trust Transitively]
--- and the Note [RnNames . Trust Own Package].
+-- The code for this is quite tricky as the whole algorithm is done in a few
+-- distinct phases in different parts of the code base. See
+-- RnNames.rnImportDecl for where package trust dependencies for a module are
+-- collected and unioned.  Specifically see the Note [RnNames . Tracking Trust
+-- Transitively] and the Note [RnNames . Trust Own Package].
 checkSafeImports :: DynFlags -> TcGblEnv -> Hsc TcGblEnv
 checkSafeImports dflags tcg_env
     = do
@@ -941,7 +942,7 @@ checkSafeImports dflags tcg_env
         clearWarnings
         logWarnings oldErrs
 
-        -- See the Note [ Safe Haskell Inference]
+        -- See the Note [Safe Haskell Inference]
         case (not $ isEmptyBag errs) of
 
             -- We have errors!
@@ -953,7 +954,7 @@ checkSafeImports dflags tcg_env
 
             -- All good matey!
             False -> do
-                when (packageTrustOn dflags) $ checkPkgTrust pkg_reqs
+                when (packageTrustOn dflags) $ checkPkgTrust dflags pkg_reqs
                 -- add in trusted package requirements for this module
                 let new_trust = emptyImportAvails { imp_trust_pkgs = catMaybes pkgs }
                 return tcg_env { tcg_imports = imp_info `plusImportAvails` new_trust }
@@ -984,46 +985,33 @@ checkSafeImports dflags tcg_env
     
     -- easier interface to work with
     checkSafe (_, _, False) = return Nothing
-    checkSafe (m, l, True ) = hscCheckSafe' dflags m l
-
-    -- Here we check the transitive package trust requirements are OK still.
-    checkPkgTrust :: [PackageId] -> Hsc ()
-    checkPkgTrust pkgs =
-        case errors of
-            [] -> return ()
-            _  -> (liftIO . throwIO . mkSrcErr . listToBag) errors
-        where
-            errors = catMaybes $ map go pkgs
-            go pkg
-                | trusted $ getPackageDetails (pkgState dflags) pkg
-                = Nothing
-                | otherwise
-                = Just $ mkPlainErrMsg noSrcSpan
-                       $ text "The package (" <> ppr pkg <> text ") is required"
-                      <> text " to be trusted but it isn't!"
+    checkSafe (m, l, True ) = fst `fmap` hscCheckSafe' dflags m l
 
 -- | Check that a module is safe to import.
 --
--- We return a package id if the safe import is OK and a Nothing otherwise
--- with the reason for the failure printed out.
-hscCheckSafe :: HscEnv -> Module -> SrcSpan -> IO (Maybe PackageId)
+-- We return True to indicate the import is safe and False otherwise
+-- although in the False case an exception may be thrown first.
+hscCheckSafe :: HscEnv -> Module -> SrcSpan -> IO Bool
 hscCheckSafe hsc_env m l = runHsc hsc_env $ do
     dflags <- getDynFlags
-    hscCheckSafe' dflags m l
+    pkgs <- snd `fmap` hscCheckSafe' dflags m l
+    when (packageTrustOn dflags) $ checkPkgTrust dflags pkgs
+    errs <- getWarnings
+    return $ isEmptyBag errs
 
-hscCheckSafe' :: DynFlags -> Module -> SrcSpan -> Hsc (Maybe PackageId)
+hscCheckSafe' :: DynFlags -> Module -> SrcSpan -> Hsc (Maybe PackageId, [PackageId])
 hscCheckSafe' dflags m l = do
-    tw <- isModSafe m l
+    (tw, pkgs) <- isModSafe m l
     case tw of
-        False              -> return Nothing
-        True | isHomePkg m -> return Nothing
-             | otherwise   -> return $ Just $ modulePackageId m
+        False              -> return (Nothing, pkgs)
+        True | isHomePkg m -> return (Nothing, pkgs)
+             | otherwise   -> return (Just $ modulePackageId m, pkgs)
   where
-    -- Is a module trusted? Return Nothing if True, or a String if it isn't,
-    -- containing the reason it isn't. Also return if the module trustworthy
-    -- (true) or safe (false) so we know if we should check if the package
-    -- itself is trusted in the future.
-    isModSafe :: Module -> SrcSpan -> Hsc (Bool)
+    -- Is a module trusted? If not, throw or log errors depending on the type.
+    -- Return (regardless of trusted or not) if the trust type requires the
+    -- modules own package be trusted and a list of other packages required to
+    -- be trusted (these later ones haven't been checked)
+    isModSafe :: Module -> SrcSpan -> Hsc (Bool, [PackageId])
     isModSafe m l = do
         iface <- lookup' m
         case iface of
@@ -1040,11 +1028,14 @@ hscCheckSafe' dflags m l = do
                     safeM = trust `elem` [Sf_SafeInfered, Sf_Safe, Sf_Trustworthy]
                     -- check package is trusted
                     safeP = packageTrusted trust trust_own_pkg m
+                    -- pkg trust reqs
+                    pkgRs = map fst $ filter snd $ dep_pkgs $ mi_deps iface'
                 case (safeM, safeP) of
                     -- General errors we throw but Safe errors we log
-                    (True, True ) -> return $ trust == Sf_Trustworthy
+                    (True, True ) -> return (trust == Sf_Trustworthy, pkgRs)
                     (True, False) -> liftIO . throwIO $ pkgTrustErr
-                    (False, _   ) -> logWarnings modTrustErr >> return (trust == Sf_Trustworthy)
+                    (False, _   ) -> logWarnings modTrustErr >>
+                                     return (trust == Sf_Trustworthy, pkgRs)
 
                 where
                     pkgTrustErr = mkSrcErr $ unitBag $ mkPlainErrMsg l $ ppr m
@@ -1055,11 +1046,10 @@ hscCheckSafe' dflags m l = do
                         <+> text "can't be safely imported!"
                         <+> text "The module itself isn't safe."
 
-    -- | Check the package a module resides in is trusted.
-    -- Safe compiled modules are trusted without requiring
-    -- that their package is trusted. For trustworthy modules,
-    -- modules in the home package are trusted but otherwise
-    -- we check the package trust flag.
+    -- | Check the package a module resides in is trusted. Safe compiled
+    -- modules are trusted without requiring that their package is trusted. For
+    -- trustworthy modules, modules in the home package are trusted but
+    -- otherwise we check the package trust flag.
     packageTrusted :: SafeHaskellMode -> Bool -> Module -> Bool
     packageTrusted _ _ _
         | not (packageTrustOn dflags)     = True
@@ -1077,13 +1067,40 @@ hscCheckSafe' dflags m l = do
         let pkgIfaceT = eps_PIT hsc_eps
             homePkgT  = hsc_HPT hsc_env
             iface     = lookupIfaceByModule dflags homePkgT pkgIfaceT m
+#ifdef GHCI
+        -- the 'lookupIfaceByModule' method will always fail when calling from GHCi
+        -- as the compiler hasn't filled in the various module tables
+        -- so we need to call 'getModuleInterface' to load from disk
+        iface' <- case iface of
+            Just _  -> return iface
+            Nothing -> snd `fmap` (liftIO $ getModuleInterface hsc_env m)
+        return iface'
+#else 
         return iface
+#endif
+
 
     isHomePkg :: Module -> Bool
     isHomePkg m
         | thisPackage dflags == modulePackageId m = True
         | otherwise                               = False
 
+-- | Check the list of packages are trusted.
+checkPkgTrust :: DynFlags -> [PackageId] -> Hsc ()
+checkPkgTrust dflags pkgs =
+    case errors of
+        [] -> return ()
+        _  -> (liftIO . throwIO . mkSrcErr . listToBag) errors
+    where
+        errors = catMaybes $ map go pkgs
+        go pkg
+            | trusted $ getPackageDetails (pkgState dflags) pkg
+            = Nothing
+            | otherwise
+            = Just $ mkPlainErrMsg noSrcSpan
+                   $ text "The package (" <> ppr pkg <> text ") is required"
+                  <> text " to be trusted but it isn't!"
+
 -- | Set module to unsafe and wipe trust information.
 --
 -- Make sure to call this method to set a module to infered unsafe,
diff --git a/compiler/rename/RnNames.lhs b/compiler/rename/RnNames.lhs
index 090a17747f..a09509754e 100644
--- a/compiler/rename/RnNames.lhs
+++ b/compiler/rename/RnNames.lhs
@@ -60,12 +60,14 @@ and packages. Doing this without caching any trust information would be very
 slow as we would need to touch all packages and interface files a module depends
 on. To avoid this we make use of the property that if a modules Safe Haskell
 mode changes, this triggers a recompilation from that module in the dependcy
-graph. So we can just worry mostly about direct imports. There is one trust
-property that can change for a package though without recompliation being
-triggered, package trust. So we must check that all packages a module
-tranitively depends on to be trusted are still trusted when we are compiling
-this module (as due to recompilation avoidance some modules below may not be
-considered trusted any more without recompilation being triggered).
+graph. So we can just worry mostly about direct imports.
+
+There is one trust property that can change for a package though without
+recompliation being triggered: package trust. So we must check that all
+packages a module tranitively depends on to be trusted are still trusted when
+we are compiling this module (as due to recompilation avoidance some modules
+below may not be considered trusted any more without recompilation being
+triggered).
 
 We handle this by augmenting the existing transitive list of packages a module M
 depends on with a bool for each package that says if it must be trusted when the
@@ -110,7 +112,7 @@ haskell at all and simply imports B, should A inherit all the the trust
 requirements from B? Should A now also require that a package p is trusted since
 B required it?
 
-We currently say no but I saying yes also makes sense. The difference is, if a
+We currently say no but saying yes also makes sense. The difference is, if a
 module M that doesn't use Safe Haskell imports a module N that does, should all
 the trusted package requirements be dropped since M didn't declare that it cares
 about Safe Haskell (so -XSafe is more strongly associated with the module doing
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index afd9093c52..dce91b1f02 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -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
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index 893cd7a9ed..8e86afc5dd 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -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
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
index 0511aa1051..87aaa3238d 100644
--- a/compiler/typecheck/TcEvidence.lhs
+++ b/compiler/typecheck/TcEvidence.lhs
@@ -16,7 +16,7 @@ module TcEvidence (
 

   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, 

 

-  EvTerm(..), mkEvCast, evVarsOfTerm,

+  EvTerm(..), mkEvCast, evVarsOfTerm, mkEvKindCast,

 

   -- TcCoercion

   TcCoercion(..), 

@@ -447,27 +447,43 @@ evBindMapBinds bs
 data EvBind = EvBind EvVar EvTerm

 

 data EvTerm

-  = EvId EvId                  -- Term-level variable-to-variable bindings

-                               -- (no coercion variables! they come via EvCoercion)

+  = EvId EvId                    -- Term-level variable-to-variable bindings

+                                 -- (no coercion variables! they come via EvCoercion)

 

-  | EvCoercion TcCoercion      -- (Boxed) coercion bindings

+  | EvCoercion TcCoercion        -- (Boxed) coercion bindings

 

-  | EvCast EvVar TcCoercion    -- d |> co

+  | EvCast EvVar TcCoercion      -- d |> co

 

-  | EvDFunApp DFunId           -- Dictionary instance application

+  | EvDFunApp DFunId             -- Dictionary instance application

        [Type] [EvVar]

 

-  | EvTupleSel EvId  Int       -- n'th component of the tuple

+  | EvTupleSel EvId  Int         -- n'th component of the tuple

 

-  | EvTupleMk [EvId]           -- tuple built from this stuff

-

-  | EvSuperClass DictId Int    -- n'th superclass. Used for both equalities and

-                               -- dictionaries, even though the former have no

-                               -- selector Id.  We count up from _0_

+  | EvTupleMk [EvId]             -- tuple built from this stuff

 

+  | EvSuperClass DictId Int      -- n'th superclass. Used for both equalities and

+                                 -- dictionaries, even though the former have no

+                                 -- selector Id.  We count up from _0_

+  | EvKindCast EvVar TcCoercion  -- See Note [EvKindCast]

+           

   deriving( Data.Data, Data.Typeable)

 \end{code}

 

+Note [EvKindCast] 

+~~~~~~~~~~~~~~~~~ 

+

+EvKindCast g kco is produced when we have a constraint (g : s1 ~ s2) 

+but the kinds of s1 and s2 (k1 and k2 respectively) don't match but 

+are rather equal by a coercion. You may think that this coercion will

+always turn out to be ReflCo, so why is this needed? Because sometimes

+we will want to defer kind errors until the runtime and in these cases

+that coercion will be an 'error' term, which we want to evaluate rather

+than silently forget about!

+

+The relevant (and only) place where such a coercion is produced in 

+the simplifier is in emit_kind_constraint in TcCanonical.

+

+

 Note [EvBinds/EvTerm]

 ~~~~~~~~~~~~~~~~~~~~~

 How evidence is created and updated. Bindings for dictionaries,

@@ -492,6 +508,11 @@ mkEvCast ev lco
   | isTcReflCo lco = EvId ev

   | otherwise      = EvCast ev lco

 

+mkEvKindCast :: EvVar -> TcCoercion -> EvTerm

+mkEvKindCast ev lco

+  | isTcReflCo lco = EvId ev

+  | otherwise      = EvKindCast ev lco

+

 emptyTcEvBinds :: TcEvBinds

 emptyTcEvBinds = EvBinds emptyBag

 

@@ -508,6 +529,7 @@ evVarsOfTerm (EvTupleSel v _)    = [v]
 evVarsOfTerm (EvSuperClass v _)  = [v]

 evVarsOfTerm (EvCast v co)       = v : varSetElems (coVarsOfTcCo co)

 evVarsOfTerm (EvTupleMk evs)     = evs

+evVarsOfTerm (EvKindCast v co)   = v : varSetElems (coVarsOfTcCo co)

 \end{code}

 

 

@@ -561,6 +583,7 @@ instance Outputable EvBind where
 instance Outputable EvTerm where

   ppr (EvId v)           = ppr v

   ppr (EvCast v co)      = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co

+  ppr (EvKindCast v co)  = ppr v <+> (ptext (sLit "`kind-cast`")) <+> pprParendTcCo co

   ppr (EvCoercion co)    = ptext (sLit "CO") <+> ppr co

   ppr (EvTupleSel v n)   = ptext (sLit "tupsel") <> parens (ppr (v,n))

   ppr (EvTupleMk vs)     = ptext (sLit "tupmk") <+> ppr vs

diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index eca79984af..3e18da52cc 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -933,14 +933,23 @@ zonk_pat env (TuplePat pats boxed ty)
 	; (env', pats') <- zonkPats env pats
 	; return (env', TuplePat pats' boxed ty') }
 
-zonk_pat env p@(ConPatOut { pat_ty = ty, pat_dicts = evs, pat_binds = binds, pat_args = args })
-  = ASSERT( all isImmutableTyVar (pat_tvs p) ) 
+zonk_pat env p@(ConPatOut { pat_ty = ty, pat_tvs = tyvars
+                          , pat_dicts = evs, pat_binds = binds
+                          , pat_args = args })
+  = ASSERT( all isImmutableTyVar tyvars ) 
     do	{ new_ty <- zonkTcTypeToType env ty
-	; (env1, new_evs) <- zonkEvBndrsX env evs
+        ; (env0, new_tyvars) <- zonkTyBndrsX env tyvars
+          -- Must zonk the existential variables, because their
+          -- /kind/ need potential zonking.
+          -- cf typecheck/should_compile/tc221.hs
+	; (env1, new_evs) <- zonkEvBndrsX env0 evs
 	; (env2, new_binds) <- zonkTcEvBinds env1 binds
 	; (env', new_args) <- zonkConStuff env2 args
-	; returnM (env', p { pat_ty = new_ty, pat_dicts = new_evs, 
-			     pat_binds = new_binds, pat_args = new_args }) }
+	; returnM (env', p { pat_ty = new_ty, 
+                             pat_tvs = new_tyvars,
+                             pat_dicts = new_evs, 
+			     pat_binds = new_binds, 
+                             pat_args = new_args }) }
 
 zonk_pat env (LitPat lit) = return (env, LitPat lit)
 
@@ -1038,15 +1047,22 @@ zonkRule env (HsRule name act (vars{-::[RuleBndr TcId]-}) lhs fv_lhs rhs fv_rhs)
                              (varSetElemsKvsFirst unbound_tkvs)
                            ++ new_bndrs
 
-       ; return (HsRule name act final_bndrs new_lhs fv_lhs new_rhs fv_rhs) }
+       ; return $ 
+         HsRule name act final_bndrs new_lhs fv_lhs new_rhs fv_rhs }
   where
    zonk_bndr env (RuleBndr (L loc v)) 
-      = do { (env', v') <- zonk_it env v; return (env', RuleBndr (L loc v')) }
+      = do { (env', v') <- zonk_it env v
+           ; return (env', RuleBndr (L loc v')) }
    zonk_bndr _ (RuleBndrSig {}) = panic "zonk_bndr RuleBndrSig"
 
    zonk_it env v
-     | isId v     = do { v' <- zonkIdBndr env v; return (extendIdZonkEnv1 env v', v') }
-     | otherwise  = ASSERT( isImmutableTyVar v) return (env, v)
+     | isId v     = do { v' <- zonkIdBndr env v
+                       ; return (extendIdZonkEnv1 env v', v') }
+     | otherwise  = ASSERT( isImmutableTyVar v)
+                    zonkTyBndrX env v
+                    -- DV: used to be return (env,v) but that is plain 
+                    -- wrong because we may need to go inside the kind 
+                    -- of v and zonk there!
 \end{code}
 
 \begin{code}
@@ -1089,6 +1105,11 @@ zonkEvTerm env (EvCoercion co)    = do { co' <- zonkTcLCoToLCo env co
 zonkEvTerm env (EvCast v co)      = ASSERT( isId v) 
                                     do { co' <- zonkTcLCoToLCo env co
                                        ; return (mkEvCast (zonkIdOcc env v) co') }
+
+zonkEvTerm env (EvKindCast v co) = ASSERT( isId v) 
+                                    do { co' <- zonkTcLCoToLCo env co
+                                       ; return (mkEvKindCast (zonkIdOcc env v) co') }
+
 zonkEvTerm env (EvTupleSel v n)   = return (EvTupleSel (zonkIdOcc env v) n)
 zonkEvTerm env (EvTupleMk vs)     = return (EvTupleMk (map (zonkIdOcc env) vs))
 zonkEvTerm env (EvSuperClass d n) = return (EvSuperClass (zonkIdOcc env d) n)
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 45e89a8274..b0eca45ebf 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -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
diff --git a/compiler/typecheck/TcRnMonad.lhs b/compiler/typecheck/TcRnMonad.lhs
index 381d5355d1..08125d75d0 100644
--- a/compiler/typecheck/TcRnMonad.lhs
+++ b/compiler/typecheck/TcRnMonad.lhs
@@ -23,6 +23,8 @@ import Module
 import RdrName
 import Name
 import Type
+import Kind ( isSuperKind )
+
 import TcType
 import InstEnv
 import FamInstEnv
@@ -1042,8 +1044,13 @@ captureUntouchables thing_inside
        ; return (res, TouchableRange low_meta high_meta) }
 
 isUntouchable :: TcTyVar -> TcM Bool
-isUntouchable tv = do { env <- getLclEnv
-                      ; return (varUnique tv < tcl_untch env) }
+isUntouchable tv
+    -- Kind variables are always touchable
+  | isSuperKind (tyVarKind tv) 
+  = return False
+  | otherwise 
+  = do { env <- getLclEnv
+       ; return (varUnique tv < tcl_untch env) }
 
 getLclTypeEnv :: TcM TcTypeEnv
 getLclTypeEnv = do { env <- getLclEnv; return (tcl_env env) }
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index ab26fa1e09..b85a892651 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -66,7 +66,8 @@ module TcRnTypes(
         Implication(..),
         CtLoc(..), ctLocSpan, ctLocOrigin, setCtLocOrigin,
 	CtOrigin(..), EqOrigin(..), 
-        WantedLoc, GivenLoc, GivenKind(..), pushErrCtxt,
+        WantedLoc, GivenLoc, GivenKind(..), pushErrCtxt, 
+        pushErrCtxtSameOrigin,
 
 	SkolemInfo(..),
 
@@ -1296,6 +1297,10 @@ setCtLocOrigin (CtLoc _ s c) o = CtLoc o s c
 pushErrCtxt :: orig -> ErrCtxt -> CtLoc orig -> CtLoc orig
 pushErrCtxt o err (CtLoc _ s errs) = CtLoc o s (err:errs)
 
+pushErrCtxtSameOrigin :: ErrCtxt -> CtLoc orig -> CtLoc orig
+-- Just add information w/o updating the origin!
+pushErrCtxtSameOrigin err (CtLoc o s errs) = CtLoc o s (err:errs)
+
 pprArising :: CtOrigin -> SDoc
 -- Used for the main, top-level error message
 -- We've done special processing for TypeEq and FunDep origins
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 60efee53fb..aabc7372e1 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -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
diff --git a/compiler/types/TypeRep.lhs b/compiler/types/TypeRep.lhs
index 3458b632c5..26526abbf0 100644
--- a/compiler/types/TypeRep.lhs
+++ b/compiler/types/TypeRep.lhs
@@ -274,7 +274,7 @@ isLiftedTypeKind _                = False
 \begin{code}  
 tyVarsOfType :: Type -> VarSet
 -- ^ NB: for type synonyms tyVarsOfType does /not/ expand the synonym
--- tyVarsOfType returns only the free *type* variables of a type
+-- tyVarsOfType returns only the free variables of a type
 -- For example, tyVarsOfType (a::k) returns {a}, not including the
 -- kind variable {k}
 tyVarsOfType (TyVarTy v)         = unitVarSet v
diff --git a/ghc/InteractiveUI.hs b/ghc/InteractiveUI.hs
index 978cb06c5d..cc4be40f44 100644
--- a/ghc/InteractiveUI.hs
+++ b/ghc/InteractiveUI.hs
@@ -1412,23 +1412,39 @@ isSafeModule m = do
                                     (GHC.moduleNameString $ GHC.moduleName m))
 
     let iface' = fromJust iface
-        trust  = showPpr $ getSafeMode $ GHC.mi_trust iface'
-        pkg    = if packageTrusted dflags m then "trusted" else "untrusted"
-        (good, bad) = tallyPkgs dflags $
-                        map fst $ filter snd $ dep_pkgs $ GHC.mi_deps iface'
+
+        trust = showPpr $ getSafeMode $ GHC.mi_trust iface'
+        pkgT  = packageTrusted dflags m
+        pkg   = if pkgT then "trusted" else "untrusted"
+        (good', bad') = tallyPkgs dflags $
+                            map fst $ filter snd $ dep_pkgs $ GHC.mi_deps iface'
+        (good, bad) = case GHC.mi_trust_pkg iface' of
+                          True | pkgT -> (modulePackageId m:good', bad')
+                          True        -> (good', modulePackageId m:bad')
+                          False       -> (good', bad')
 
     liftIO $ putStrLn $ "Trust type is (Module: " ++ trust ++ ", Package: " ++ pkg ++ ")"
-    when (not $ null good)
+    liftIO $ putStrLn $ "Package Trust: "
+                            ++ (if packageTrustOn dflags then "On" else "Off")
+
+    when (packageTrustOn dflags && not (null good))
          (liftIO $ putStrLn $ "Trusted package dependencies (trusted): " ++
                         (intercalate ", " $ map packageIdString good))
-    if (null bad)
-        then liftIO $ putStrLn $ mname ++ " is trusted!"
-        else do
+
+    case goodTrust (getSafeMode $ GHC.mi_trust iface') of
+        True | (null bad || not (packageTrustOn dflags)) ->
+            liftIO $ putStrLn $ mname ++ " is trusted!"
+
+        True -> do
             liftIO $ putStrLn $ "Trusted package dependencies (untrusted): "
                         ++ (intercalate ", " $ map packageIdString bad)
             liftIO $ putStrLn $ mname ++ " is NOT trusted!"
 
+        False -> liftIO $ putStrLn $ mname ++ " is NOT trusted!"
+
   where
+    goodTrust t = t `elem` [Sf_Safe, Sf_SafeInfered, Sf_Trustworthy]
+
     mname = GHC.moduleNameString $ GHC.moduleName m
 
     packageTrusted dflags md
@@ -1567,8 +1583,9 @@ moduleCmd str
           '-':stuff -> rest remModulesFromContext stuff
           stuff     -> rest setContext            stuff
 
-    rest op stuff = (op as bs, words stuff)
-       where (as,bs) = partitionWith starred strs
+    rest op stuff = (op as bs, stuffs)
+       where (as,bs) = partitionWith starred stuffs
+             stuffs  = words stuff
 
     sensible ('*':m) = looksLikeModuleName m
     sensible m       = looksLikeModuleName m
@@ -1618,12 +1635,23 @@ setContext starred not_starred = do
   setGHCContextFromGHCiState
 
 checkAdd :: Bool -> String -> GHCi InteractiveImport
-checkAdd star mstr
-  | star      = do m <- wantInterpretedModule mstr
-                   return (IIModule m)
-  | otherwise = do m <- lookupModule mstr
-                   return (IIDecl (simpleImportDecl (moduleName m)))
-
+checkAdd star mstr = do
+  dflags <- getDynFlags 
+  case safeLanguageOn dflags of
+    True | star -> ghcError $ CmdLineError "can't use * imports with Safe Haskell"
+
+    True -> do m <- lookupModule mstr
+               s <- GHC.isModuleTrusted m
+               case s of
+                 True  -> return $ IIDecl (simpleImportDecl $ moduleName m)
+                 False -> ghcError $ CmdLineError $ "can't import " ++ mstr
+                                                 ++ " as it isn't trusted."
+
+    False | star -> do m <- wantInterpretedModule mstr
+                       return $ IIModule m
+
+    False -> do m <- lookupModule mstr
+                return $ IIDecl (simpleImportDecl $ moduleName m)
 
 -- | Sets the GHC context from the GHCi state.  The GHC context is
 -- always set this way, we never modify it incrementally.