Clean up the debugger code

In particular there is much less fiddly skolemisation now
Things are not *quite* right (break001 and 006 still fail), 
but they are *much* better than before.

9 files changed, 194 insertions, 230 deletions

diff --git a/compiler/ghci/Debugger.hs b/compiler/ghci/Debugger.hs
index 504dc1dfbd..9f38313901 100644
--- a/compiler/ghci/Debugger.hs
+++ b/compiler/ghci/Debugger.hs
@@ -52,15 +52,12 @@ pprintClosureCommand bindThings force str = do
   let ids = [id | AnId id <- tythings]
 
   -- Obtain the terms and the recovered type information
-  (terms, substs0) <- unzip `liftM` mapM go ids
+  (subst, terms) <- mapAccumLM go emptyTvSubst ids
 
   -- Apply the substitutions obtained after recovering the types
   modifySession $ \hsc_env ->
-    let (substs, skol_vars) = unzip$ map skolemiseSubst substs0
-        hsc_ic' = foldr (flip substInteractiveContext)
-                        (extendInteractiveContext (hsc_IC hsc_env) [] (unionVarSets skol_vars))
-                        substs
-     in hsc_env{hsc_IC = hsc_ic'}
+    hsc_env{hsc_IC = substInteractiveContext (hsc_IC hsc_env) subst}
+
   -- Finally, print the Terms
   unqual  <- GHC.getPrintUnqual
   docterms <- mapM showTerm terms
@@ -70,9 +67,10 @@ pprintClosureCommand bindThings force str = do
                     docterms)
  where
    -- Do the obtainTerm--bindSuspensions-computeSubstitution dance
-   go :: GhcMonad m => Id -> m (Term, TvSubst)
-   go id = do
-       term_    <- GHC.obtainTermFromId maxBound force id
+   go :: GhcMonad m => TvSubst -> Id -> m (TvSubst, Term)
+   go subst id = do
+       let id' = id `setIdType` substTy subst (idType id) 
+       term_    <- GHC.obtainTermFromId maxBound force id'
        term     <- tidyTermTyVars term_
        term'    <- if bindThings &&
                       False == isUnliftedTypeKind (termType term)
@@ -82,19 +80,18 @@ pprintClosureCommand bindThings force str = do
      --  Then, we extract a substitution,
      --  mapping the old tyvars to the reconstructed types.
        let reconstructed_type = termType term
-       mb_subst <- withSession $ \hsc_env ->
-                     liftIO $ improveRTTIType hsc_env (idType id) (reconstructed_type)
-       maybe (return ())
-             (\subst -> traceOptIf Opt_D_dump_rtti
-                   (fsep $ [text "RTTI Improvement for", ppr id,
-                           text "is the substitution:" , ppr subst]))
-             mb_subst
-       return (term', fromMaybe emptyTvSubst mb_subst)
+       hsc_env <- getSession
+       case (improveRTTIType hsc_env (idType id) (reconstructed_type)) of
+         Nothing     -> return (subst, term')
+         Just subst' -> do { traceOptIf Opt_D_dump_rtti
+                               (fsep $ [text "RTTI Improvement for", ppr id,
+                                text "is the substitution:" , ppr subst'])
+                           ; return (subst `unionTvSubst` subst', term')}
 
    tidyTermTyVars :: GhcMonad m => Term -> m Term
    tidyTermTyVars t =
      withSession $ \hsc_env -> do
-     let env_tvs      = ic_tyvars (hsc_IC hsc_env)
+     let env_tvs      = tyVarsOfTypes (map idType (ic_tmp_ids (hsc_IC hsc_env)))
          my_tvs       = termTyVars t
          tvs          = env_tvs `minusVarSet` my_tvs
          tyvarOccName = nameOccName . tyVarName
@@ -115,10 +112,9 @@ bindSuspensions t = do
       availNames_var  <- liftIO $ newIORef availNames
       (t', stuff)     <- liftIO $ foldTerm (nameSuspensionsAndGetInfos availNames_var) t
       let (names, tys, hvals) = unzip3 stuff
-          (tys', skol_vars)   = unzip $ map skolemiseTy tys
       let ids = [ mkVanillaGlobal name ty 
-                | (name,ty) <- zip names tys']
-          new_ic = extendInteractiveContext ictxt ids (unionVarSets skol_vars)
+                | (name,ty) <- zip names tys]
+          new_ic = extendInteractiveContext ictxt ids
       liftIO $ extendLinkEnv (zip names hvals)
       modifySession $ \_ -> hsc_env {hsc_IC = new_ic }
       return t'
diff --git a/compiler/ghci/RtClosureInspect.hs b/compiler/ghci/RtClosureInspect.hs
index 6075cbaecc..b281695985 100644
--- a/compiler/ghci/RtClosureInspect.hs
+++ b/compiler/ghci/RtClosureInspect.hs
@@ -20,9 +20,7 @@ module RtClosureInspect(
 
 --     unsafeDeepSeq,
 
-     Closure(..), getClosureData, ClosureType(..), isConstr, isIndirection,
-
-     sigmaType
+     Closure(..), getClosureData, ClosureType(..), isConstr, isIndirection
  ) where
 
 #include "HsVersions.h"
@@ -34,6 +32,7 @@ import Linker
 
 import DataCon
 import Type
+import qualified Unify as U
 import TypeRep         -- I know I know, this is cheating
 import Var
 import TcRnMonad
@@ -572,13 +571,29 @@ liftTcM = id
 newVar :: Kind -> TR TcType
 newVar = liftTcM . newFlexiTyVarTy
 
--- | Returns the instantiated type scheme ty', and the substitution sigma 
---   such that sigma(ty') = ty 
-instScheme :: Type -> TR (TcType, TvSubst)
-instScheme ty = liftTcM$ do
-   (tvs, _, _)  <- tcInstType return ty
-   (tvs',_,ty') <- tcInstType (mapM tcInstTyVar) ty
-   return (ty', zipTopTvSubst tvs' (mkTyVarTys tvs))
+type RttiInstantiation = [(TyVar, TcTyVar)]
+   -- Assoicates the debugger-world type variables (which are skolems)
+   -- to typechecker-world meta type variables (which are mutable,
+   -- and may be refined)
+
+-- | Returns the instantiated type scheme ty', and the 
+--   mapping from old to new (instantiated) type variables
+instScheme :: QuantifiedType -> TR (TcType, RttiInstantiation)
+instScheme (tvs, ty) 
+  = liftTcM $ do { (tvs', _, subst) <- tcInstTyVars tvs
+                 ; return (substTy subst ty, tvs `zip` tvs') }
+
+applyRevSubst :: RttiInstantiation -> TR ()
+-- Apply the *reverse* substitution in-place to any un-filled-in
+-- meta tyvars.  This recovers the original debugger-world variable
+-- unless it has been refined by new information from the heap
+applyRevSubst pairs = liftTcM (mapM_ do_pair pairs)
+  where
+    do_pair (rtti_tv, tc_tv)
+      = do { tc_ty <- zonkTcTyVar tc_tv
+           ; case tcGetTyVar_maybe tc_ty of
+               Just tv | isMetaTyVar tv -> writeMetaTyVar tv (mkTyVarTy rtti_tv)
+               _                        -> return () }
 
 -- Adds a constraint of the form t1 == t2
 -- t1 is expected to come from walking the heap
@@ -589,9 +604,10 @@ addConstraint :: TcType -> TcType -> TR ()
 addConstraint actual expected = do
     traceTR (text "add constraint:" <+> fsep [ppr actual, equals, ppr expected])
     recoverTR (traceTR $ fsep [text "Failed to unify", ppr actual,
-                                    text "with", ppr expected])
-              (congruenceNewtypes actual expected >>=
-                           (captureConstraints . uncurry unifyType) >> return ())
+                                    text "with", ppr expected]) $
+      do { (ty1, ty2) <- congruenceNewtypes actual expected
+         ; _  <- captureConstraints $ unifyType ty1 ty2
+         ; return () }
      -- TOMDO: what about the coercion?
      -- we should consider family instances
 
@@ -603,30 +619,32 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
   -- we quantify existential tyvars as universal,
   -- as this is needed to be able to manipulate
   -- them properly
-   let sigma_old_ty = sigmaType old_ty
+   let quant_old_ty@(old_tvs, old_tau) = quantifyType old_ty
+       sigma_old_ty = mkForAllTys old_tvs old_tau
    traceTR (text "Term reconstruction started with initial type " <> ppr old_ty)
    term <-
-     if isMonomorphic sigma_old_ty
+     if null old_tvs
       then do
-        new_ty <- go max_depth sigma_old_ty sigma_old_ty hval >>= zonkTerm
-        return $ fixFunDictionaries $ expandNewtypes new_ty
+        term  <- go max_depth sigma_old_ty sigma_old_ty hval
+        term' <- zonkTerm term
+        return $ fixFunDictionaries $ expandNewtypes term'
       else do
-              (old_ty', rev_subst) <- instScheme sigma_old_ty
+              (old_ty', rev_subst) <- instScheme quant_old_ty
               my_ty <- newVar argTypeKind
-              when (check1 sigma_old_ty) (traceTR (text "check1 passed") >>
+              when (check1 quant_old_ty) (traceTR (text "check1 passed") >>
                                           addConstraint my_ty old_ty')
               term  <- go max_depth my_ty sigma_old_ty hval
-              zterm <- zonkTerm term
-              let new_ty = termType zterm
-              if isMonomorphic new_ty || check2 (sigmaType new_ty) sigma_old_ty
+              new_ty <- zonkTcType (termType term)
+              if isMonomorphic new_ty || check2 (quantifyType new_ty) quant_old_ty
                  then do
                       traceTR (text "check2 passed")
-                      addConstraint (termType term) old_ty'
+                      addConstraint new_ty old_ty'
+                      applyRevSubst rev_subst
                       zterm' <- zonkTerm term
-                      return ((fixFunDictionaries . expandNewtypes . mapTermType (substTy rev_subst)) zterm')
+                      return ((fixFunDictionaries . expandNewtypes) zterm')
                  else do
                       traceTR (text "check2 failed" <+> parens
-                                       (ppr zterm <+> text "::" <+> ppr new_ty))
+                                       (ppr term <+> text "::" <+> ppr new_ty))
                       -- we have unsound types. Replace constructor types in
                       -- subterms with tyvars
                       zterm' <- mapTermTypeM
@@ -634,7 +652,7 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
                                            Just (tc, _:_) | tc /= funTyCon
                                                -> newVar argTypeKind
                                            _   -> return ty)
-                                 zterm
+                                 term
                       zonkTerm zterm'
    traceTR (text "Term reconstruction completed." $$
             text "Term obtained: " <> ppr term $$
@@ -676,7 +694,7 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
          contents_tv <- newVar liftedTypeKind
          contents <- trIO$ IO$ \w -> readMutVar# (unsafeCoerce# a) w
          ASSERT(isUnliftedTypeKind $ typeKind my_ty) return ()
-         (mutvar_ty,_) <- instScheme $ sigmaType $ mkFunTy 
+         (mutvar_ty,_) <- instScheme $ quantifyType $ mkFunTy 
                             contents_ty (mkTyConApp tycon [world,contents_ty])
          addConstraint (mkFunTy contents_tv my_ty) mutvar_ty
          x <- go (pred max_depth) contents_tv contents_ty contents
@@ -780,9 +798,9 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
 cvReconstructType :: HscEnv -> Int -> GhciType -> HValue -> IO (Maybe Type)
 cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
    traceTR (text "RTTI started with initial type " <> ppr old_ty)
-   let sigma_old_ty = sigmaType old_ty
+   let sigma_old_ty@(old_tvs, _) = quantifyType old_ty
    new_ty <-
-       if isMonomorphic sigma_old_ty
+       if null old_tvs
         then return old_ty
         else do
           (old_ty', rev_subst) <- instScheme sigma_old_ty
@@ -794,12 +812,12 @@ cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
                  (Seq.singleton (my_ty, hval))
                  max_depth
           new_ty <- zonkTcType my_ty
-          if isMonomorphic new_ty || check2 (sigmaType new_ty) sigma_old_ty
+          if isMonomorphic new_ty || check2 (quantifyType new_ty) sigma_old_ty
             then do
-                 traceTR (text "check2 passed")
+                 traceTR (text "check2 passed" <+> ppr old_ty $$ ppr new_ty)
                  addConstraint my_ty old_ty'
-                 new_ty' <- zonkTcType my_ty
-                 return (substTy rev_subst new_ty')
+                 applyRevSubst rev_subst
+                 zonkRttiType new_ty
             else traceTR (text "check2 failed" <+> parens (ppr new_ty)) >>
                  return old_ty
    traceTR (text "RTTI completed. Type obtained:" <+> ppr new_ty)
@@ -846,7 +864,7 @@ cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
             -- It is vital for newtype reconstruction that the unification step
             -- is done right here, _before_ the subterms are RTTI reconstructed
             let myType         = mkFunTys subTtypes my_ty
-            (signatureType,_) <- instScheme(mydataConType dc)
+            (signatureType,_) <- instScheme (mydataConType dc)
             addConstraint myType signatureType
             return $ [ appArr (\e->(t,e)) (ptrs clos) i
                        | (i,t) <- zip [0..] (filter (isLifted |.| isRefType) subTtypes)]
@@ -856,36 +874,23 @@ cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
 -- improveType <base_type> <rtti_type>
 -- The types can contain skolem type variables, which need to be treated as normal vars.
 -- In particular, we want them to unify with things.
-improveRTTIType :: HscEnv -> RttiType -> RttiType -> IO (Maybe TvSubst)
-improveRTTIType hsc_env _ty rtti_ty = runTR_maybe hsc_env $ do
-    traceTR (text "improveRttiType" <+> fsep [ppr _ty, ppr rtti_ty])
-    (ty_tvs,  _, _)   <- tcInstType return ty
-    (ty_tvs', _, ty') <- tcInstType (mapM tcInstTyVar) ty
-    (_, _, rtti_ty')  <- tcInstType (mapM tcInstTyVar) (sigmaType rtti_ty)
-    _ <- captureConstraints (unifyType rtti_ty' ty')
-    tvs1_contents     <- zonkTcTyVars ty_tvs'
-    let subst = (uncurry zipTopTvSubst . unzip)
-                 [(tv,ty) | (tv,ty) <- zip ty_tvs tvs1_contents
-                          , getTyVar_maybe ty /= Just tv
-                          --, not(isTyVarTy ty)
-                          ]
-    return subst
- where ty = sigmaType _ty
+improveRTTIType :: HscEnv -> RttiType -> RttiType -> Maybe TvSubst
+improveRTTIType _ base_ty new_ty
+  = U.tcUnifyTys (const U.BindMe) [base_ty] [new_ty]
 
 myDataConInstArgTys :: DataCon -> [Type] -> [Type]
 myDataConInstArgTys dc args
     | null (dataConExTyVars dc) && null (dataConEqTheta dc) = dataConInstArgTys dc args
     | otherwise = dataConRepArgTys dc
 
-mydataConType :: DataCon -> Type
+mydataConType :: DataCon -> QuantifiedType
 -- ^ Custom version of DataCon.dataConUserType where we
 --    - remove the equality constraints
 --    - use the representation types for arguments, including dictionaries
 --    - keep the original result type
 mydataConType  dc
-  = mkForAllTys ((univ_tvs `minusList` map fst eq_spec) ++ ex_tvs) $
-    mkFunTys arg_tys $
-    res_ty
+  = ( (univ_tvs `minusList` map fst eq_spec) ++ ex_tvs
+    , mkFunTys arg_tys res_ty )
   where univ_tvs   = dataConUnivTyVars dc
         ex_tvs     = dataConExTyVars dc
         eq_spec    = dataConEqSpec dc
@@ -1017,24 +1022,21 @@ If that is not the case, then we consider two conditions.
 
 -}
 
-check1 :: Type -> Bool
-check1 ty | (tvs, _, _) <- tcSplitSigmaTy ty = not $ any isHigherKind (map tyVarKind tvs)
+check1 :: QuantifiedType -> Bool
+check1 (tvs, _) = not $ any isHigherKind (map tyVarKind tvs)
  where
    isHigherKind = not . null . fst . splitKindFunTys
 
-check2 :: Type -> Type -> Bool
-check2 sigma_rtti_ty sigma_old_ty
+check2 :: QuantifiedType -> QuantifiedType -> Bool
+check2 (_, rtti_ty) (_, old_ty)
   | Just (_, rttis) <- tcSplitTyConApp_maybe rtti_ty
   = case () of
       _ | Just (_,olds) <- tcSplitTyConApp_maybe old_ty
-        -> and$ zipWith check2 rttis olds
+        -> and$ zipWith check2 (map quantifyType rttis) (map quantifyType olds)
       _ | Just _ <- splitAppTy_maybe old_ty
         -> isMonomorphicOnNonPhantomArgs rtti_ty
       _ -> True
   | otherwise = True
-  where (_, _ , rtti_ty) = tcSplitSigmaTy sigma_rtti_ty
-        (_, _ , old_ty)  = tcSplitSigmaTy sigma_old_ty
-
 
 -- Dealing with newtypes
 --------------------------
@@ -1072,6 +1074,8 @@ congruenceNewtypes lhs rhs = go lhs rhs >>= \rhs' -> return (lhs,rhs')
    go l r
  -- TyVar lhs inductive case
     | Just tv <- getTyVar_maybe l
+    , isTcTyVar tv
+    , isMetaTyVar tv
     = recoverTR (return r) $ do
          Indirect ty_v <- readMetaTyVar tv
          traceTR $ fsep [text "(congruence) Following indirect tyvar:",
@@ -1108,17 +1112,26 @@ congruenceNewtypes lhs rhs = go lhs rhs >>= \rhs' -> return (lhs,rhs')
 
 
 zonkTerm :: Term -> TcM Term
-zonkTerm = foldTermM TermFoldM{
-              fTermM = \ty dc v tt -> zonkTcType ty    >>= \ty' ->
-                                      return (Term ty' dc v tt)
-             ,fSuspensionM = \ct ty v b -> zonkTcType ty >>= \ty ->
-                                           return (Suspension ct ty v b)
-             ,fNewtypeWrapM= \ty dc t -> zonkTcType ty >>= \ty' ->
-                                         return$ NewtypeWrap ty' dc t
-             ,fRefWrapM    = \ty t ->
-                               return RefWrap `ap` zonkTcType ty `ap` return t
-             ,fPrimM       = (return.) . Prim
-             }
+zonkTerm = foldTermM (TermFoldM
+             { fTermM = \ty dc v tt -> zonkRttiType ty    >>= \ty' ->
+                                       return (Term ty' dc v tt)
+             , fSuspensionM  = \ct ty v b -> zonkRttiType ty >>= \ty ->
+                                             return (Suspension ct ty v b)
+             , fNewtypeWrapM = \ty dc t -> zonkRttiType ty >>= \ty' ->
+                                           return$ NewtypeWrap ty' dc t
+             , fRefWrapM     = \ty t -> return RefWrap  `ap` 
+                                        zonkRttiType ty `ap` return t
+             , fPrimM        = (return.) . Prim })
+
+zonkRttiType :: TcType -> TcM Type
+-- Zonk the type, replacing any unbound Meta tyvars
+-- by skolems, safely out of Meta-tyvar-land
+zonkRttiType = zonkType (mkZonkTcTyVar zonk_unbound_meta) 
+  where
+    zonk_unbound_meta tv 
+      = ASSERT( isTcTyVar tv )
+        do { tv' <- skolemiseUnboundMetaTyVar RuntimeUnkSkol tv
+           ; return (mkTyVarTy tv') }
 
 --------------------------------------------------------------------------------
 -- Restore Class predicates out of a representation type
@@ -1137,7 +1150,7 @@ dictsView ty = ty
 -- Use only for RTTI types
 isMonomorphic :: RttiType -> Bool
 isMonomorphic ty = noExistentials && noUniversals
- where (tvs, _, ty')     = tcSplitSigmaTy ty
+ where (tvs, _, ty')  = tcSplitSigmaTy ty
        noExistentials = isEmptyVarSet (tyVarsOfType ty')
        noUniversals   = null tvs
 
@@ -1161,11 +1174,11 @@ tyConPhantomTyVars tc
   = tyConTyVars tc \\ dc_vars
 tyConPhantomTyVars _ = []
 
--- Is this defined elsewhere?
--- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
-sigmaType :: Type -> Type
-sigmaType ty = mkSigmaTy (varSetElems$ tyVarsOfType ty) [] ty
+type QuantifiedType = ([TyVar], Type)   -- Make the free type variables explicit
 
+quantifyType :: Type -> QuantifiedType
+-- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
+quantifyType ty = (varSetElems (tyVarsOfType ty), ty)
 
 mapMif :: Monad m => (a -> Bool) -> (a -> m a) -> [a] -> m [a]
 mapMif pred f xx = sequence $ mapMif_ pred f xx
diff --git a/compiler/main/HscMain.lhs b/compiler/main/HscMain.lhs
index 0daab4aa51..42ed3e4598 100644
--- a/compiler/main/HscMain.lhs
+++ b/compiler/main/HscMain.lhs
@@ -46,9 +46,10 @@ import CorePrep		( corePrepExpr )
 import Desugar          ( deSugarExpr )
 import SimplCore        ( simplifyExpr )
 import TcRnDriver	( tcRnStmt, tcRnExpr, tcRnType ) 
-import Type		( Type )
+import Type		( Type, tyVarsOfTypes )
 import PrelNames	( iNTERACTIVE )
 import {- Kind parts of -} Type		( Kind )
+import Id      	     	( idType )
 import CoreLint		( lintUnfolding )
 import DsMeta		( templateHaskellNames )
 import SrcLoc		( SrcSpan, noSrcLoc, interactiveSrcLoc, srcLocSpan, noSrcSpan, unLoc )
@@ -1046,7 +1047,7 @@ compileExpr hsc_env srcspan ds_expr
 		-- ToDo: improve SrcLoc
 	; if lint_on then 
                 let ictxt = hsc_IC hsc_env
-                    tyvars = varSetElems (ic_tyvars ictxt)
+                    tyvars = varSetElems (tyVarsOfTypes (map idType (ic_tmp_ids ictxt)))
                 in
 		case lintUnfolding noSrcLoc tyvars prepd_expr of
 		   Just err -> pprPanic "compileExpr" err
diff --git a/compiler/main/HscTypes.lhs b/compiler/main/HscTypes.lhs
index f88ef35845..1124f995aa 100644
--- a/compiler/main/HscTypes.lhs
+++ b/compiler/main/HscTypes.lhs
@@ -123,7 +123,6 @@ import FamInstEnv	( FamInstEnv, FamInst )
 import Rules		( RuleBase )
 import CoreSyn		( CoreBind )
 import VarEnv
-import VarSet
 import Var
 import Id
 import Type		
@@ -1132,15 +1131,9 @@ data InteractiveContext
 	ic_rn_gbl_env :: GlobalRdrEnv,	-- ^ The contexts' cached 'GlobalRdrEnv', built from
 					-- 'ic_toplev_scope' and 'ic_exports'
 
-	ic_tmp_ids :: [Id],             -- ^ Names bound during interaction with the user.
+	ic_tmp_ids :: [Id]              -- ^ Names bound during interaction with the user.
                                         -- Later Ids shadow earlier ones with the same OccName.
 
-        ic_tyvars :: TyVarSet           -- ^ Skolem type variables free in
-                                        -- 'ic_tmp_ids'.  These arise at
-                                        -- breakpoints in a polymorphic 
-                                        -- context, where we have only partial
-                                        -- type information.
-
 #ifdef GHCI
         , ic_resume :: [Resume]         -- ^ The stack of breakpoint contexts
 #endif
@@ -1154,8 +1147,7 @@ emptyInteractiveContext
   = InteractiveContext { ic_toplev_scope = [],
 			 ic_exports = [],
 			 ic_rn_gbl_env = emptyGlobalRdrEnv,
-			 ic_tmp_ids = [],
-                         ic_tyvars = emptyVarSet
+			 ic_tmp_ids = []
 #ifdef GHCI
                          , ic_resume = []
 #endif
@@ -1169,29 +1161,20 @@ icPrintUnqual dflags ictxt = mkPrintUnqualified dflags (ic_rn_gbl_env ictxt)
 extendInteractiveContext
         :: InteractiveContext
         -> [Id]
-        -> TyVarSet
         -> InteractiveContext
-extendInteractiveContext ictxt ids tyvars
-  = ictxt { ic_tmp_ids =  snub((ic_tmp_ids ictxt \\ ids) ++ ids),
+extendInteractiveContext ictxt ids
+  = ictxt { ic_tmp_ids =  snub ((ic_tmp_ids ictxt \\ ids) ++ ids)
                           -- NB. must be this way around, because we want
                           -- new ids to shadow existing bindings.
-            ic_tyvars   = ic_tyvars ictxt `unionVarSet` tyvars }
+          }
     where snub = map head . group . sort
 
 substInteractiveContext :: InteractiveContext -> TvSubst -> InteractiveContext
 substInteractiveContext ictxt subst | isEmptyTvSubst subst = ictxt
-substInteractiveContext ictxt@InteractiveContext{ic_tmp_ids=ids} subst =
-   let ids'     = map (\id -> id `setIdType` substTy subst (idType id)) ids
-       subst_dom= varEnvKeys$ getTvSubstEnv subst
-       subst_ran= varEnvElts$ getTvSubstEnv subst
-       new_tvs  = [ tv | Just tv <- map getTyVar_maybe subst_ran]  
-       ic_tyvars'= (`delVarSetListByKey` subst_dom) 
-                 . (`extendVarSetList`   new_tvs)
-                   $ ic_tyvars ictxt
-    in ictxt { ic_tmp_ids = ids'
-             , ic_tyvars   = ic_tyvars' }
-
-          where delVarSetListByKey = foldl' delVarSetByKey
+substInteractiveContext ictxt@InteractiveContext{ic_tmp_ids=ids} subst 
+  = ictxt { ic_tmp_ids = map subst_ty ids }
+  where
+   subst_ty id = id `setIdType` substTy subst (idType id)
 \end{code}
 
 %************************************************************************
diff --git a/compiler/main/InteractiveEval.hs b/compiler/main/InteractiveEval.hs
index 687c63c085..4161d9811c 100644
--- a/compiler/main/InteractiveEval.hs
+++ b/compiler/main/InteractiveEval.hs
@@ -29,8 +29,7 @@ module InteractiveEval (
 	showModule,
         isModuleInterpreted,
 	compileExpr, dynCompileExpr,
-        Term(..), obtainTermFromId, obtainTermFromVal, reconstructType,
-        skolemiseSubst, skolemiseTy
+        Term(..), obtainTermFromId, obtainTermFromVal, reconstructType
 #endif
         ) where
 
@@ -110,7 +109,7 @@ data Resume
        resumeThreadId  :: ThreadId,     -- thread running the computation
        resumeBreakMVar :: MVar (),   
        resumeStatMVar  :: MVar Status,
-       resumeBindings  :: ([Id], TyVarSet),
+       resumeBindings  :: [Id],
        resumeFinalIds  :: [Id],         -- [Id] to bind on completion
        resumeApStack   :: HValue,       -- The object from which we can get
                                         -- value of the free variables.
@@ -223,7 +222,7 @@ runStmt expr step =
                 liftIO $ sandboxIO dflags' statusMVar thing_to_run
               
         let ic = hsc_IC hsc_env
-            bindings = (ic_tmp_ids ic, ic_tyvars ic)
+            bindings = ic_tmp_ids ic
 
         case step of
           RunAndLogSteps ->
@@ -261,7 +260,7 @@ emptyHistory :: BoundedList History
 emptyHistory = nilBL 50 -- keep a log of length 50
 
 handleRunStatus :: GhcMonad m =>
-                   String-> ([Id], TyVarSet) -> [Id]
+                   String-> [Id] -> [Id]
                 -> MVar () -> MVar Status -> Status -> BoundedList History
                 -> m RunResult
 handleRunStatus expr bindings final_ids breakMVar statusMVar status
@@ -275,9 +274,12 @@ handleRunStatus expr bindings final_ids breakMVar statusMVar status
         (hsc_env1, names, span) <- liftIO $ bindLocalsAtBreakpoint hsc_env apStack
                                                                mb_info
         let
-            resume = Resume expr tid breakMVar statusMVar 
-                              bindings final_ids apStack mb_info span 
-                              (toListBL history) 0
+            resume = Resume { resumeStmt = expr, resumeThreadId = tid
+                            , resumeBreakMVar = breakMVar, resumeStatMVar = statusMVar 
+                            , resumeBindings = bindings, resumeFinalIds = final_ids
+                            , resumeApStack = apStack, resumeBreakInfo = mb_info 
+                            , resumeSpan = span, resumeHistory = toListBL history
+                            , resumeHistoryIx = 0 }
             hsc_env2 = pushResume hsc_env1 resume
         --
         modifySession (\_ -> hsc_env2)
@@ -287,9 +289,7 @@ handleRunStatus expr bindings final_ids breakMVar statusMVar status
 	    Left e -> return (RunException e)
 	    Right hvals -> do
                 hsc_env <- getSession
-                let final_ic = extendInteractiveContext (hsc_IC hsc_env)
-                                        final_ids emptyVarSet
-                        -- the bound Ids never have any free TyVars
+                let final_ic = extendInteractiveContext (hsc_IC hsc_env) final_ids 
                     final_names = map idName final_ids
                 liftIO $ Linker.extendLinkEnv (zip final_names hvals)
                 hsc_env' <- liftIO $ rttiEnvironment hsc_env{hsc_IC=final_ic}
@@ -297,7 +297,7 @@ handleRunStatus expr bindings final_ids breakMVar statusMVar status
                 return (RunOk final_names)
 
 traceRunStatus :: GhcMonad m =>
-                  String -> ([Id], TyVarSet) -> [Id]
+                  String -> [Id] -> [Id]
                -> MVar () -> MVar Status -> Status -> BoundedList History
                -> m RunResult
 traceRunStatus expr bindings final_ids
@@ -457,9 +457,8 @@ resume canLogSpan step
         -- unbind the temporary locals by restoring the TypeEnv from
         -- before the breakpoint, and drop this Resume from the
         -- InteractiveContext.
-        let (resume_tmp_ids, resume_tyvars) = resumeBindings r
+        let resume_tmp_ids = resumeBindings r
             ic' = ic { ic_tmp_ids  = resume_tmp_ids,
-                       ic_tyvars   = resume_tyvars,
                        ic_resume   = rs }
         modifySession (\_ -> hsc_env{ hsc_IC = ic' })
         
@@ -471,8 +470,11 @@ resume canLogSpan step
         
         when (isStep step) $ liftIO setStepFlag
         case r of 
-          Resume expr tid breakMVar statusMVar bindings 
-              final_ids apStack info span hist _ -> do
+          Resume { resumeStmt = expr, resumeThreadId = tid
+                 , resumeBreakMVar = breakMVar, resumeStatMVar = statusMVar
+                 , resumeBindings = bindings, resumeFinalIds = final_ids
+                 , resumeApStack = apStack, resumeBreakInfo = info, resumeSpan = span
+                 , resumeHistory = hist } -> do
                withVirtualCWD $ do
                 withBreakAction (isStep step) (hsc_dflags hsc_env) 
                                         breakMVar statusMVar $ do
@@ -563,10 +565,9 @@ bindLocalsAtBreakpoint hsc_env apStack Nothing = do
        e_name    = mkInternalName (getUnique e_fs) (mkTyVarOccFS e_fs) span
        e_tyvar   = mkTcTyVar e_name liftedTypeKind (SkolemTv RuntimeUnkSkol)
        exn_id    = Id.mkVanillaGlobal exn_name (mkTyVarTy e_tyvar)
-       new_tyvars = unitVarSet e_tyvar
 
        ictxt0 = hsc_IC hsc_env
-       ictxt1 = extendInteractiveContext ictxt0 [exn_id] new_tyvars
+       ictxt1 = extendInteractiveContext ictxt0 [exn_id]
 
        span = mkGeneralSrcSpan (fsLit "<exception thrown>")
    --
@@ -616,9 +617,6 @@ bindLocalsAtBreakpoint hsc_env apStack (Just info) = do
        result_id   = Id.mkVanillaGlobal result_name result_ty 
 
    -- for each Id we're about to bind in the local envt:
-   --    - skolemise the type variables in its type, so they can't
-   --      be randomly unified with other types.  These type variables
-   --      can only be resolved by type reconstruction in RtClosureInspect
    --    - tidy the type variables
    --    - globalise the Id (Ids are supposed to be Global, apparently).
    --
@@ -627,12 +625,11 @@ bindLocalsAtBreakpoint hsc_env apStack (Just info) = do
 
        all_ids | result_ok = result_id : new_ids
                | otherwise = new_ids
-       (id_tys, tyvarss) = mapAndUnzip (skolemiseTy.idType) all_ids
+       id_tys = map idType all_ids
        (_,tidy_tys) = tidyOpenTypes emptyTidyEnv id_tys
-       new_tyvars = unionVarSets tyvarss             
        final_ids = zipWith setIdType all_ids tidy_tys
        ictxt0 = hsc_IC hsc_env
-       ictxt1 = extendInteractiveContext ictxt0 final_ids new_tyvars
+       ictxt1 = extendInteractiveContext ictxt0 final_ids
 
    Linker.extendLinkEnv [ (name,hval) | (name, Just hval) <- zip names mb_hValues ]
    when result_ok $ Linker.extendLinkEnv [(result_name, unsafeCoerce# apStack)]
@@ -664,7 +661,7 @@ rttiEnvironment hsc_env@HscEnv{hsc_IC=ic} = do
    hsc_env' <- foldM improveTypes hsc_env (map idName incompletelyTypedIds)
    return hsc_env'
     where
-     noSkolems = null . filter isSkolemTyVar . varSetElems . tyVarsOfType . idType
+     noSkolems = isEmptyVarSet . tyVarsOfType . idType
      improveTypes hsc_env@HscEnv{hsc_IC=ic} name = do
       let InteractiveContext{ic_tmp_ids=tmp_ids} = ic
           Just id = find (\i -> idName i == name) tmp_ids
@@ -676,8 +673,7 @@ rttiEnvironment hsc_env@HscEnv{hsc_IC=ic} = do
            case mb_new_ty of
              Nothing -> return hsc_env
              Just new_ty -> do
-              mb_subst <- improveRTTIType hsc_env old_ty new_ty
-              case mb_subst of
+              case improveRTTIType hsc_env old_ty new_ty of
                Nothing -> return $
                         WARN(True, text (":print failed to calculate the "
                                            ++ "improvement for a type")) hsc_env
@@ -686,32 +682,10 @@ rttiEnvironment hsc_env@HscEnv{hsc_IC=ic} = do
                       printForUser stderr alwaysQualify $
                       fsep [text "RTTI Improvement for", ppr id, equals, ppr subst]
 
-                 let (subst', skols) = skolemiseSubst subst
-                     ic' = extendInteractiveContext
-                               (substInteractiveContext ic subst') [] skols
+                 let ic' = extendInteractiveContext
+                               (substInteractiveContext ic subst) []
                  return hsc_env{hsc_IC=ic'}
 
-skolemiseSubst :: TvSubst -> (TvSubst, TyVarSet)
-skolemiseSubst subst = let
-    varenv               = getTvSubstEnv subst
-    all_together         = mapVarEnv skolemiseTy varenv
-    (varenv', skol_vars) = ( mapVarEnv fst all_together
-                           , map snd (varEnvElts all_together))
-    in (subst `setTvSubstEnv` varenv', unionVarSets skol_vars)
-                        
-
-skolemiseTy :: Type -> (Type, TyVarSet)
-skolemiseTy ty = (substTy subst ty, mkVarSet new_tyvars)
-  where env           = mkVarEnv (zip tyvars new_tyvar_tys)
-        subst         = mkTvSubst emptyInScopeSet env
-        tyvars        = varSetElems (tyVarsOfType ty)
-        new_tyvars    = map skolemiseTyVar tyvars
-        new_tyvar_tys = map mkTyVarTy new_tyvars
-
-skolemiseTyVar :: TyVar -> TyVar
-skolemiseTyVar tyvar = mkTcTyVar (tyVarName tyvar) (tyVarKind tyvar) 
-                                 (SkolemTv RuntimeUnkSkol)
-
 getIdValFromApStack :: HValue -> Int -> IO (Maybe HValue)
 getIdValFromApStack apStack (I# stackDepth) = do
    case getApStackVal# apStack (stackDepth +# 1#) of
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index f3485a26cf..d45d774cda 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -50,7 +50,7 @@ module TcMType (
   --------------------------------
   -- Zonking
   zonkType, mkZonkTcTyVar, zonkTcPredType, 
-  zonkTcTypeCarefully,
+  zonkTcTypeCarefully, skolemiseUnboundMetaTyVar,
   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
   zonkTcType, zonkTcTypes, zonkTcThetaType,
@@ -134,17 +134,6 @@ newWantedEvVars theta = mapM newWantedEvVar theta
 newWantedCoVar :: TcType -> TcType -> TcM CoVar 
 newWantedCoVar ty1 ty2 = newCoVar ty1 ty2
 
--- We used to create a mutable co-var
-{-
--- A wanted coercion variable is a MetaTyVar
--- that can be filled in with its binding
-  = do { uniq <- newUnique 
-       ; ref <- newMutVar Flexi 
-       ; let name = mkSysTvName uniq (fsLit "c")
-             kind = mkPredTy (EqPred ty1 ty2) 
-       ; return (mkTcTyVar name kind (MetaTv TauTv ref)) }
--}
-
 --------------
 newEvVar :: TcPredType -> TcM EvVar
 -- Creates new *rigid* variables for predicates
@@ -488,10 +477,10 @@ zonkTcTypeCarefully ty
       | otherwise
       = ASSERT( isTcTyVar tv )
     	case tcTyVarDetails tv of
-    	  SkolemTv {}    -> return (TyVarTy tv)
+    	  SkolemTv {}  -> return (TyVarTy tv)
     	  FlatSkol ty  -> zonkType (zonk_tv env_tvs) ty
-    	  MetaTv _ ref   -> do { cts <- readMutVar ref
-			       ; case cts of    
+    	  MetaTv _ ref -> do { cts <- readMutVar ref
+		             ; case cts of    
 			           Flexi       -> return (TyVarTy tv)
 			           Indirect ty -> zonkType (zonk_tv env_tvs) ty }
 
@@ -504,11 +493,11 @@ zonkTcTyVar :: TcTyVar -> TcM TcType
 zonkTcTyVar tv
   = ASSERT2( isTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
-      SkolemTv {}    -> return (TyVarTy tv)
+      SkolemTv {}  -> return (TyVarTy tv)
       FlatSkol ty  -> zonkTcType ty
-      MetaTv _ ref   -> do { cts <- readMutVar ref
-			   ; case cts of    
-			       Flexi       -> return (TyVarTy tv)
+      MetaTv _ ref -> do { cts <- readMutVar ref
+		         ; case cts of    
+		               Flexi       -> return (TyVarTy tv)
 			       Indirect ty -> zonkTcType ty }
 
 zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
@@ -548,8 +537,6 @@ zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
 
 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
--- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
---
 -- The quantified type variables often include meta type variables
 -- we want to freeze them into ordinary type variables, and
 -- default their kind (e.g. from OpenTypeKind to TypeKind)
@@ -560,35 +547,39 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 --
 -- We leave skolem TyVars alone; they are immutable.
 zonkQuantifiedTyVar tv
-  | ASSERT2( isTcTyVar tv, ppr tv ) 
-    isSkolemTyVar tv 
-  = do { kind <- zonkTcType (tyVarKind tv)
-       ; return $ setTyVarKind tv kind
-       }
+  = ASSERT2( isTcTyVar tv, ppr tv ) 
+    case tcTyVarDetails tv of
+      FlatSkol {} -> pprPanic "zonkQuantifiedTyVar" (ppr tv)
+      SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
+                        ; return $ setTyVarKind tv kind }
 	-- It might be a skolem type variable, 
 	-- for example from a user type signature
 
-  | otherwise	-- It's a meta-type-variable
-  = do	{ details <- readMetaTyVar tv
-
-	-- Create the new, frozen, skolem type variable
-        -- We zonk to a skolem, not to a regular TcVar
-        -- See Note [Zonking to Skolem]
-        ; uniq <- newUnique  -- Remove it from TcMetaTyVar unique land
+      MetaTv _ _ref -> 
+#ifdef DEBUG               
+			-- [Sept 04] Check for non-empty.  
+		 	-- See note [Silly Type Synonym]
+                      (readMutVar _ref >>= \cts -> 
+                       case cts of 
+                             Flexi -> return ()
+                             Indirect ty -> WARN( True, ppr tv $$ ppr ty ) 
+                                            return ()) >>
+#endif
+                      skolemiseUnboundMetaTyVar UnkSkol tv 
+                             
+skolemiseUnboundMetaTyVar :: SkolemInfo -> TcTyVar -> TcM TyVar
+-- We have a Meta tyvar with a ref-cell inside it
+-- Skolemise it, including giving it a new Name, so that
+--   we are totally out of Meta-tyvar-land
+-- We create a skolem TyVar, not a regular TyVar
+--   See Note [Zonking to Skolem]
+skolemiseUnboundMetaTyVar skol_info tv
+  = ASSERT2( isMetaTyVar tv, ppr tv ) 
+    do	{ uniq <- newUnique  -- Remove it from TcMetaTyVar unique land
 	; let final_kind = defaultKind (tyVarKind tv)
               final_name = setNameUnique (tyVarName tv) uniq
-	      final_tv   = mkSkolTyVar final_name final_kind UnkSkol
-
-	-- Bind the meta tyvar to the new tyvar
-	; case details of
-	    Indirect ty -> WARN( True, ppr tv $$ ppr ty ) 
-			   return ()
-		-- [Sept 04] I don't think this should happen
-		-- See note [Silly Type Synonym]
-
-	    Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
-
-	-- Return the new tyvar
+	      final_tv   = mkSkolTyVar final_name final_kind skol_info
+	; writeMetaTyVar tv (mkTyVarTy final_tv)
 	; return final_tv }
 \end{code}
 
@@ -693,10 +684,8 @@ simplifier knows how to deal with.
 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 --	type variable and zonks the kind too
 
-zonkType :: (TcTyVar -> TcM Type) 	-- What to do with unbound mutable type variables
-					-- see zonkTcType, and zonkTcTypeToType
-         -> TcType
-	 -> TcM Type
+zonkType :: (TcTyVar -> TcM Type)  -- What to do with TcTyVars
+         -> TcType -> TcM Type
 zonkType zonk_tc_tyvar ty
   = go ty
   where
@@ -736,7 +725,7 @@ zonkType zonk_tc_tyvar ty
                                   ty2' <- go ty2
                                   return (EqPred ty1' ty2')
 
-mkZonkTcTyVar :: (TcTyVar -> TcM Type)	-- What to do for an unbound mutable var
+mkZonkTcTyVar :: (TcTyVar -> TcM Type)	-- What to do for an *mutable Flexi* var
  	      -> TcTyVar -> TcM TcType
 mkZonkTcTyVar unbound_var_fn tyvar 
   = ASSERT( isTcTyVar tyvar )
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index b20d32eec3..194deb9a29 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -123,7 +123,8 @@ module TcType (
   -- Type substitutions
   TvSubst(..), 	-- Representation visible to a few friends
   TvSubstEnv, emptyTvSubst, substEqSpec,
-  mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
+  mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, 
+  mkTopTvSubst, notElemTvSubst, unionTvSubst,
   getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, lookupTyVar,
   extendTvSubst, extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
   substTy, substTys, substTyWith, substTheta, substTyVar, substTyVars, substTyVarBndr,
diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs
index fa5f46aa84..8ff78fbccf 100644
--- a/compiler/types/Type.lhs
+++ b/compiler/types/Type.lhs
@@ -105,7 +105,7 @@ module Type (
 	getTvSubstEnv, setTvSubstEnv, zapTvSubstEnv, getTvInScope, 
         extendTvInScope, extendTvInScopeList,
  	extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv,
-        isEmptyTvSubst,
+        isEmptyTvSubst, unionTvSubst,
 
 	-- ** Performing substitution on types
 	substTy, substTys, substTyWith, substTysWith, substTheta, 
@@ -1320,6 +1320,13 @@ extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
 extendTvSubstList (TvSubst in_scope env) tvs tys 
   = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
 
+unionTvSubst :: TvSubst -> TvSubst -> TvSubst
+-- Works when the ranges are disjoint
+unionTvSubst (TvSubst in_scope1 env1) (TvSubst in_scope2 env2)
+  = ASSERT( not (env1 `intersectsVarEnv` env2) )
+    TvSubst (in_scope1 `unionInScope` in_scope2)
+            (env1      `plusVarEnv`   env2)
+
 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
 -- the types given; but it's just a thunk so with a bit of luck
 -- it'll never be evaluated
diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index de5ac49c2d..2f2cfb8927 100644
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -380,7 +380,7 @@ dataConCannotMatch tys con
 \begin{code}
 tcUnifyTys :: (TyVar -> BindFlag)
 	   -> [Type] -> [Type]
-	   -> Maybe TvSubst	-- A regular one-shot substitution
+	   -> Maybe TvSubst	-- A regular one-shot (idempotent) substitution
 -- The two types may have common type variables, and indeed do so in the
 -- second call to tcUnifyTys in FunDeps.checkClsFD
 --