SafeHaskell: Even more fixing to work with safe base
[ghc.git] / compiler / ghci / RtClosureInspect.hs
index 164b9c5..8e2c92c 100644 (file)
@@ -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
@@ -51,16 +50,14 @@ import TysPrim
 import PrelNames
 import TysWiredIn
 import DynFlags
-import Outputable
+import Outputable as Ppr
 import FastString
-import Panic
-
 import Constants        ( wORD_SIZE )
-
-import GHC.Arr          ( Array(..) )
+import GHC.Arr.Unsafe   ( Array(..) )
 import GHC.Exts
-import GHC.IOBase ( IO(IO) )
+import GhcIO ( IO(..) )
 
+import StaticFlags( opt_PprStyle_Debug )
 import Control.Monad
 import Data.Maybe
 import Data.Array.Base
@@ -68,11 +65,10 @@ import Data.Ix
 import Data.List
 import qualified Data.Sequence as Seq
 import Data.Monoid
-import Data.Sequence hiding (null, length, index, take, drop, splitAt, reverse)
+import Data.Sequence (viewl, ViewL(..))
 import Foreign
 import System.IO.Unsafe
 
-import System.IO
 ---------------------------------------------
 -- * A representation of semi evaluated Terms
 ---------------------------------------------
@@ -160,7 +156,7 @@ data Closure = Closure { tipe         :: ClosureType
 instance Outputable ClosureType where
   ppr = text . show 
 
-#include "../includes/ClosureTypes.h"
+#include "../includes/rts/storage/ClosureTypes.h"
 
 aP_CODE, pAP_CODE :: Int
 aP_CODE = AP
@@ -187,7 +183,7 @@ getClosureData a =
                elems = fromIntegral (BCI.ptrs itbl)
                ptrsList = Array 0 (elems - 1) elems ptrs
                nptrs_data = [W# (indexWordArray# nptrs i)
-                              | I# i <- [0.. fromIntegral (BCI.nptrs itbl)] ]
+                              | I# i <- [0.. fromIntegral (BCI.nptrs itbl)-1] ]
            ASSERT(elems >= 0) return ()
            ptrsList `seq` 
             return (Closure tipe (Ptr iptr) itbl ptrsList nptrs_data)
@@ -347,10 +343,17 @@ ppr_termM y p Term{dc=Right dc, subTerms=tt}
   = parens (ppr_term1 True t1 <+> ppr dc <+> ppr_term1 True ppr t2) 
     <+> hsep (map (ppr_term1 True) tt) 
 -} -- TODO Printing infix constructors properly
-  | null tt   = return$ ppr dc
-  | otherwise = do
-         tt_docs <- mapM (y app_prec) tt
-         return$ cparen (p >= app_prec) (ppr dc <+> pprDeeperList fsep tt_docs)
+  | null sub_terms_to_show
+  = return (ppr dc)
+  | otherwise 
+  = do { tt_docs <- mapM (y app_prec) sub_terms_to_show
+       ; return $ cparen (p >= app_prec) $
+         sep [ppr dc, nest 2 (pprDeeperList fsep tt_docs)] }
+  where
+    sub_terms_to_show  -- Don't show the dictionary arguments to 
+                       -- constructors unless -dppr-debug is on
+      | opt_PprStyle_Debug = tt
+      | otherwise = dropList (dataConTheta dc) tt
 
 ppr_termM y p t@NewtypeWrap{} = pprNewtypeWrap y p t
 ppr_termM y p RefWrap{wrapped_term=t}  = do
@@ -376,12 +379,12 @@ ppr_termM1 Term{}        = panic "ppr_termM1 - Term"
 ppr_termM1 RefWrap{}     = panic "ppr_termM1 - RefWrap"
 ppr_termM1 NewtypeWrap{} = panic "ppr_termM1 - NewtypeWrap"
 
-pprNewtypeWrap y p NewtypeWrap{ty=ty, wrapped_term=t} 
+pprNewtypeWrap y p NewtypeWrap{ty=ty, wrapped_term=t}
   | Just (tc,_) <- tcSplitTyConApp_maybe ty
   , ASSERT(isNewTyCon tc) True
   , Just new_dc <- tyConSingleDataCon_maybe tc = do 
-         real_term <- y max_prec t
-         return$ cparen (p >= app_prec) (ppr new_dc <+> real_term)
+             real_term <- y max_prec t
+             return $ cparen (p >= app_prec) (ppr new_dc <+> real_term)
 pprNewtypeWrap _ _ _ = panic "pprNewtypeWrap"
 
 -------------------------------------------------------
@@ -415,54 +418,70 @@ cPprTerm printers_ = go 0 where
   firstJustM [] = return Nothing
 
 -- Default set of custom printers. Note that the recursion knot is explicit
-cPprTermBase :: Monad m => CustomTermPrinter m
+cPprTermBase :: forall m. Monad m => CustomTermPrinter m
 cPprTermBase y =
   [ ifTerm (isTupleTy.ty) (\_p -> liftM (parens . hcat . punctuate comma) 
                                       . mapM (y (-1))
                                       . subTerms)
   , ifTerm (\t -> isTyCon listTyCon (ty t) && subTerms t `lengthIs` 2)
-           (\ p Term{subTerms=[h,t]} -> doList p h t)
-  , ifTerm (isTyCon intTyCon    . ty) (coerceShow$ \(a::Int)->a)
-  , ifTerm (isTyCon charTyCon   . ty) (coerceShow$ \(a::Char)->a)
-  , ifTerm (isTyCon floatTyCon  . ty) (coerceShow$ \(a::Float)->a)
-  , ifTerm (isTyCon doubleTyCon . ty) (coerceShow$ \(a::Double)->a)
-  , ifTerm (isIntegerTy         . ty) (coerceShow$ \(a::Integer)->a)
+           ppr_list
+  , ifTerm (isTyCon intTyCon    . ty) ppr_int
+  , ifTerm (isTyCon charTyCon   . ty) ppr_char
+  , ifTerm (isTyCon floatTyCon  . ty) ppr_float
+  , ifTerm (isTyCon doubleTyCon . ty) ppr_double
+  , ifTerm (isIntegerTy         . ty) ppr_integer
   ]
-     where ifTerm pred f prec t@Term{}
-               | pred t    = Just `liftM` f prec t
-           ifTerm _ _ _ _  = return Nothing
-
-           isIntegerTy ty  = fromMaybe False $ do
-             (tc,_) <- tcSplitTyConApp_maybe ty 
-             return (tyConName tc == integerTyConName)
-
-           isTupleTy ty    = fromMaybe False $ do 
-             (tc,_) <- tcSplitTyConApp_maybe ty 
-             return (isBoxedTupleTyCon tc)
-
-           isTyCon a_tc ty = fromMaybe False $ do 
-             (tc,_) <- tcSplitTyConApp_maybe ty
-             return (a_tc == tc)
-
-           coerceShow f _p = return . text . show . f . unsafeCoerce# . val
-
-           --Note pprinting of list terms is not lazy
-           doList p h t = do
-               let elems      = h : getListTerms t
-                   isConsLast = not(termType(last elems) `coreEqType` termType h)
-               print_elems <- mapM (y cons_prec) elems
-               return$ if isConsLast
-                     then cparen (p >= cons_prec) 
-                        . pprDeeperList fsep 
-                        . punctuate (space<>colon)
-                        $ print_elems
-                     else brackets (pprDeeperList fcat$
-                                         punctuate comma print_elems)
-
-                where getListTerms Term{subTerms=[h,t]} = h : getListTerms t
-                      getListTerms Term{subTerms=[]}    = []
-                      getListTerms t@Suspension{}       = [t]
-                      getListTerms t = pprPanic "getListTerms" (ppr t)
+ where 
+   ifTerm :: (Term -> Bool)
+          -> (Precedence -> Term -> m SDoc)
+          -> Precedence -> Term -> m (Maybe SDoc)
+   ifTerm pred f prec t@Term{}
+       | pred t    = Just `liftM` f prec t
+   ifTerm _ _ _ _  = return Nothing
+
+   isTupleTy ty    = fromMaybe False $ do 
+     (tc,_) <- tcSplitTyConApp_maybe ty 
+     return (isBoxedTupleTyCon tc)
+
+   isTyCon a_tc ty = fromMaybe False $ do 
+     (tc,_) <- tcSplitTyConApp_maybe ty
+     return (a_tc == tc)
+
+   isIntegerTy ty = fromMaybe False $ do
+     (tc,_) <- tcSplitTyConApp_maybe ty
+     return (tyConName tc == integerTyConName)
+
+   ppr_int, ppr_char, ppr_float, ppr_double, ppr_integer 
+      :: Precedence -> Term -> m SDoc
+   ppr_int     _ v = return (Ppr.int     (unsafeCoerce# (val v)))
+   ppr_char    _ v = return (Ppr.char '\'' <> Ppr.char (unsafeCoerce# (val v)) <> Ppr.char '\'')
+   ppr_float   _ v = return (Ppr.float   (unsafeCoerce# (val v)))
+   ppr_double  _ v = return (Ppr.double  (unsafeCoerce# (val v)))
+   ppr_integer _ v = return (Ppr.integer (unsafeCoerce# (val v)))
+
+   --Note pprinting of list terms is not lazy
+   ppr_list :: Precedence -> Term -> m SDoc
+   ppr_list p (Term{subTerms=[h,t]}) = do
+       let elems      = h : getListTerms t
+           isConsLast = not(termType(last elems) `eqType` termType h)
+          is_string  = all (isCharTy . ty) elems
+
+       print_elems <- mapM (y cons_prec) elems
+       if is_string
+        then return (Ppr.doubleQuotes (Ppr.text (unsafeCoerce# (map val elems))))
+        else if isConsLast
+        then return $ cparen (p >= cons_prec) 
+                    $ pprDeeperList fsep 
+                    $ punctuate (space<>colon) print_elems
+        else return $ brackets 
+                    $ pprDeeperList fcat
+                    $ punctuate comma print_elems
+
+        where getListTerms Term{subTerms=[h,t]} = h : getListTerms t
+              getListTerms Term{subTerms=[]}    = []
+              getListTerms t@Suspension{}       = [t]
+              getListTerms t = pprPanic "getListTerms" (ppr t)
+   ppr_list _ _ = panic "doList"
 
 
 repPrim :: TyCon -> [Word] -> String
@@ -517,8 +536,6 @@ Right hand sides are missing them. We can either (a) drop them from the lhs, or
 The function congruenceNewtypes takes a shot at (b)
 -}
 
--- The Type Reconstruction monad
-type TR a = TcM a
 
 -- A (non-mutable) tau type containing
 -- existentially quantified tyvars.
@@ -529,20 +546,17 @@ type RttiType = Type
 -- An incomplete type as stored in GHCi:
 --  no polymorphism: no quantifiers & all tyvars are skolem.
 type GhciType = Type
-{-
-runTR :: HscEnv -> TR a -> IO a
-runTR hsc_env c = do
-  mb_term <- runTR_maybe hsc_env c
-  case mb_term of 
-    Nothing -> panic "RTTI: Failed to reconstruct a term"
-    Just x  -> return x
--}
+
+
+-- The Type Reconstruction monad
+--------------------------------
+type TR a = TcM a
 
 runTR :: HscEnv -> TR a -> IO a
 runTR hsc_env thing = do
   mb_val <- runTR_maybe hsc_env thing
   case mb_val of
-    Nothing -> error "RTTI error: probably due to :forcing an undefined"
+    Nothing -> error "unable to :print the term"
     Just x  -> return x
 
 runTR_maybe :: HscEnv -> TR a -> IO (Maybe a)
@@ -569,15 +583,40 @@ liftTcM :: TcM a -> TR a
 liftTcM = id
 
 newVar :: Kind -> TR TcType
-newVar = liftTcM . liftM mkTyVarTy . newBoxyTyVar
-
--- | 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))
+newVar = liftTcM . newFlexiTyVarTy
+
+instTyVars :: [TyVar] -> TR ([TcTyVar], [TcType], TvSubst)
+-- Instantiate fresh mutable type variables from some TyVars
+-- This function preserves the print-name, which helps error messages
+instTyVars = liftTcM . tcInstTyVars
+
+type RttiInstantiation = [(TcTyVar, TyVar)]
+   -- Associates the typechecker-world meta type variables 
+   -- (which are mutable and may be refined), to their 
+   -- debugger-world RuntimeUnk counterparts.
+   -- If the TcTyVar has not been refined by the runtime type
+   -- elaboration, then we want to turn it back into the
+   -- original RuntimeUnk
+
+-- | Returns the instantiated type scheme ty', and the 
+--   mapping from new (instantiated) -to- old (skolem) type variables
+instScheme :: QuantifiedType -> TR (TcType, RttiInstantiation)
+instScheme (tvs, ty) 
+  = liftTcM $ do { (tvs', _, subst) <- tcInstTyVars tvs
+                 ; let rtti_inst = [(tv',tv) | (tv',tv) <- tvs' `zip` tvs]
+                 ; return (substTy subst ty, rtti_inst) }
+
+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 (tc_tv, rtti_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
@@ -586,44 +625,49 @@ instScheme ty = liftTcM$ do
 -- do its magic.
 addConstraint :: TcType -> TcType -> TR ()
 addConstraint actual expected = do
-    traceTR $ fsep [text "add constraint:", ppr actual, equals, ppr expected]
+    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 >>=
-                           uncurry boxyUnify >> 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
 
--- Type & Term reconstruction 
+
+-- Type & Term reconstruction
+------------------------------
 cvObtainTerm :: HscEnv -> Int -> Bool -> RttiType -> HValue -> IO Term
 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
@@ -631,28 +675,37 @@ 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. Term obtained: " <> ppr term)
+   traceTR (text "Term reconstruction completed." $$
+            text "Term obtained: " <> ppr term $$
+            text "Type obtained: " <> ppr (termType term))
    return term
     where 
+
   go :: Int -> Type -> Type -> HValue -> TcM Term
+   -- [SPJ May 11] I don't understand the difference between my_ty and old_ty
+
   go max_depth _ _ _ | seq max_depth False = undefined
   go 0 my_ty _old_ty a = do
+    traceTR (text "Gave up reconstructing a term after" <>
+                  int max_depth <> text " steps")
     clos <- trIO $ getClosureData a
     return (Suspension (tipe clos) my_ty a Nothing)
-  go max_depth my_ty old_ty a = do 
+  go max_depth my_ty old_ty a = do
     let monomorphic = not(isTyVarTy my_ty)   
     -- This ^^^ is a convention. The ancestor tests for
     -- monomorphism and passes a type instead of a tv
     clos <- trIO $ getClosureData a
     case tipe clos of
 -- Thunks we may want to force
--- NB. this won't attempt to force a BLACKHOLE.  Even with :force, we never
--- force blackholes, because it would almost certainly result in deadlock,
--- and showing the '_' is more useful.
       t | isThunk t && force -> traceTR (text "Forcing a " <> text (show t)) >>
                                 seq a (go (pred max_depth) my_ty old_ty a)
+-- Blackholes are indirections iff the payload is not TSO or BLOCKING_QUEUE.  So we
+-- treat them like indirections; if the payload is TSO or BLOCKING_QUEUE, we'll end up
+-- showing '_' which is what we want.
+      Blackhole -> do traceTR (text "Following a BLACKHOLE")
+                      appArr (go max_depth my_ty old_ty) (ptrs clos) 0
 -- We always follow indirections
       Indirection i -> do traceTR (text "Following an indirection" <> parens (int i) )
                           go max_depth my_ty old_ty $! (ptrs clos ! 0)
@@ -667,7 +720,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
@@ -675,7 +728,10 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
 
  -- The interesting case
       Constr -> do
-        traceTR (text "entering a constructor")
+        traceTR (text "entering a constructor " <>
+                      if monomorphic
+                        then parens (text "already monomorphic: " <> ppr my_ty)
+                        else Ppr.empty)
         Right dcname <- dataConInfoPtrToName (infoPtr clos)
         (_,mb_dc)    <- tryTcErrs (tcLookupDataCon dcname)
         case mb_dc of
@@ -684,60 +740,39 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
                         -- In such case, we return a best approximation:
                         --  ignore the unpointed args, and recover the pointeds
                         -- This preserves laziness, and should be safe.
+                      traceTR (text "Nothing" <+> ppr dcname)
                        let tag = showSDoc (ppr dcname)
                        vars     <- replicateM (length$ elems$ ptrs clos) 
-                                              (newVar (liftedTypeKind))
+                                              (newVar liftedTypeKind)
                        subTerms <- sequence [appArr (go (pred max_depth) tv tv) (ptrs clos) i 
                                               | (i, tv) <- zip [0..] vars]
                        return (Term my_ty (Left ('<' : tag ++ ">")) a subTerms)
           Just dc -> do
-            let subTtypes  = matchSubTypes dc old_ty
-                (subTtypesP, subTtypesNP) = partition (isLifted |.| isRefType) subTtypes
-            subTermTvs    <- mapMif (not . isMonomorphic)
-                                    (\t -> newVar (typeKind t))
-                                    subTtypes
-            -- It is vital for newtype reconstruction that the unification step
-            -- is done right here, _before_ the subterms are RTTI reconstructed
-            when (not monomorphic) $ do
-
-                       -- When we already have all the information, avoid solving
-                       -- unnecessary constraints. Propagation of type information
-                       -- to subterms is already being done via matching.
-               let myType = mkFunTys subTermTvs my_ty
-               (signatureType,_) <- instScheme (rttiView $ dataConUserType dc)
-               addConstraint myType signatureType
+            traceTR (text "Just" <+> ppr dc)
+            subTtypes <- getDataConArgTys dc my_ty
+            let (subTtypesP, subTtypesNP) = partition isPtrType subTtypes
             subTermsP <- sequence
-                  [ appArr (go (pred max_depth) tv t) (ptrs clos) i
-                   | (i,tv,t) <- zip3 [0..] subTermTvs subTtypesP]
+                  [ appArr (go (pred max_depth) ty ty) (ptrs clos) i
+                  | (i,ty) <- zip [0..] subTtypesP]
             let unboxeds   = extractUnboxed subTtypesNP clos
-                subTermsNP = map (uncurry Prim) (zip subTtypesNP unboxeds)      
+                subTermsNP = zipWith Prim subTtypesNP unboxeds
                 subTerms   = reOrderTerms subTermsP subTermsNP subTtypes
             return (Term my_ty (Right dc) a subTerms)
+
 -- The otherwise case: can be a Thunk,AP,PAP,etc.
       tipe_clos ->
          return (Suspension tipe_clos my_ty a Nothing)
 
-  matchSubTypes dc ty
-    | ty' <- repType ty     -- look through newtypes
-    , Just (tc,ty_args) <- tcSplitTyConApp_maybe ty'
-    , dc `elem` tyConDataCons tc
-      -- It is necessary to check that dc is actually a constructor for tycon tc,
-      -- because it may be the case that tc is a recursive newtype and tcSplitTyConApp
-      -- has not removed it. In that case, we happily give up and don't match
-    = myDataConInstArgTys dc ty_args
-    | otherwise = dataConRepArgTys dc
-
   -- put together pointed and nonpointed subterms in the
   --  correct order.
   reOrderTerms _ _ [] = []
   reOrderTerms pointed unpointed (ty:tys) 
-   | isLifted ty || isRefType ty
-                  = ASSERT2(not(null pointed)
+   | isPtrType ty = ASSERT2(not(null pointed)
                             , ptext (sLit "reOrderTerms") $$ 
                                         (ppr pointed $$ ppr unpointed))
                     let (t:tt) = pointed in t : reOrderTerms tt unpointed tys
    | otherwise    = ASSERT2(not(null unpointed)
-                           , ptext (sLit "Reorderterms") $$ 
+                           , ptext (sLit "reOrderTerms") $$ 
                                        (ppr pointed $$ ppr unpointed))
                     let (t:tt) = unpointed in t : reOrderTerms pointed tt tys
 
@@ -760,12 +795,13 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
 
 
 -- Fast, breadth-first Type reconstruction
+------------------------------------------
 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
@@ -777,12 +813,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)
@@ -801,8 +837,10 @@ cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
    -- returns unification tasks,since we are going to want a breadth-first search
   go :: Type -> HValue -> TR [(Type, HValue)]
   go my_ty a = do
+    traceTR (text "go" <+> ppr my_ty)
     clos <- trIO $ getClosureData a
     case tipe clos of
+      Blackhole -> appArr (go my_ty) (ptrs clos) 0 -- carefully, don't eval the TSO
       Indirection _ -> go my_ty $! (ptrs clos ! 0)
       MutVar _ -> do
          contents <- trIO$ IO$ \w -> readMutVar# (unsafeCoerce# a) w
@@ -812,6 +850,7 @@ cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
          return [(tv', contents)]
       Constr -> do
         Right dcname <- dataConInfoPtrToName (infoPtr clos)
+        traceTR (text "Constr1" <+> ppr dcname)
         (_,mb_dc)    <- tryTcErrs (tcLookupDataCon dcname)
         case mb_dc of
           Nothing-> do
@@ -821,52 +860,50 @@ cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
                         return$ appArr (\e->(tv,e)) (ptrs clos) i
 
           Just dc -> do
-            subTtypes <- mapMif (not . isMonomorphic)
-                                (\t -> newVar (typeKind t))
-                                (dataConRepArgTys dc)
-
-            -- 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(rttiView $ dataConUserType dc)
-            addConstraint myType signatureType
-            return $ [ appArr (\e->(t,e)) (ptrs clos) i
-                       | (i,t) <- zip [0..] (filter (isLifted |.| isRefType) subTtypes)]
+            arg_tys <- getDataConArgTys dc my_ty
+           traceTR (text "Constr2" <+> ppr dcname <+> ppr arg_tys)
+            return $ [ appArr (\e-> (ty,e)) (ptrs clos) i
+                     | (i,ty) <- zip [0..] (filter isPtrType arg_tys)]
       _ -> return []
 
 -- Compute the difference between a base type and the type found by RTTI
 -- 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 $ fsep [text "improveRttiType", 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)
-    boxyUnify 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
-
-myDataConInstArgTys :: DataCon -> [Type] -> [Type]
-myDataConInstArgTys dc args
-    | null (dataConExTyVars dc) && null (dataConEqTheta dc) = dataConInstArgTys dc args
-    | otherwise = dataConRepArgTys dc
-
-isRefType :: Type -> Bool
-isRefType ty
-   | Just (tc, _) <- tcSplitTyConApp_maybe ty' = isRefTyCon tc
-   | otherwise = False
-  where ty'= repType ty
-
-isRefTyCon :: TyCon -> Bool
-isRefTyCon tc = tc `elem` [mutVarPrimTyCon, mVarPrimTyCon, tVarPrimTyCon]
+improveRTTIType :: HscEnv -> RttiType -> RttiType -> Maybe TvSubst
+improveRTTIType _ base_ty new_ty
+  = U.tcUnifyTys (const U.BindMe) [base_ty] [new_ty]
+
+getDataConArgTys :: DataCon -> Type -> TR [Type]
+-- Given the result type ty of a constructor application (D a b c :: ty) 
+-- return the types of the arguments.  This is RTTI-land, so 'ty' might
+-- not be fully known.  Moreover, the arg types might involve existentials;
+-- if so, make up fresh RTTI type variables for them
+getDataConArgTys dc con_app_ty
+  = do { (_, ex_tys, _) <- instTyVars ex_tvs
+       ; let rep_con_app_ty = repType con_app_ty
+       ; ty_args <- case tcSplitTyConApp_maybe rep_con_app_ty of
+                       Just (tc, ty_args) | dataConTyCon dc == tc
+                          -> ASSERT( univ_tvs `equalLength` ty_args) 
+                              return ty_args
+                      _   -> do { (_, ty_args, subst) <- instTyVars univ_tvs
+                                ; let res_ty = substTy subst (dataConOrigResTy dc)
+                                 ; addConstraint rep_con_app_ty res_ty
+                                 ; return ty_args }
+               -- It is necessary to check dataConTyCon dc == tc
+               -- because it may be the case that tc is a recursive
+               -- newtype and tcSplitTyConApp has not removed it. In
+               -- that case, we happily give up and don't match
+       ; let subst = zipTopTvSubst (univ_tvs ++ ex_tvs) (ty_args ++ ex_tys)
+       ; return (substTys subst (dataConRepArgTys dc)) }
+  where
+    univ_tvs = dataConUnivTyVars dc
+    ex_tvs   = dataConExTyVars dc
+
+isPtrType :: Type -> Bool
+isPtrType ty = case typePrimRep ty of
+                 PtrRep -> True
+                 _      -> False
 
 -- Soundness checks
 --------------------
@@ -967,7 +1004,7 @@ If that is not the case, then we consider two conditions.
 2. To prevent the class of unsoundness shown by row 6,
    the rtti type should be structurally more
    defined than the old type we are comparing it to.
-  check2 :: OldType -> NewTy            pe -> Bool
+  check2 :: NewType -> OldType -> Bool
   check2 a  _        = True
   check2 [a] a       = True
   check2 [a] (t Int) = False
@@ -981,24 +1018,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
 --------------------------
@@ -1036,6 +1070,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:",
@@ -1064,34 +1100,40 @@ congruenceNewtypes lhs rhs = go lhs rhs >>= \rhs' -> return (lhs,rhs')
             | otherwise = do
                traceTR (text "(Upgrade) upgraded " <> ppr ty <>
                         text " in presence of newtype evidence " <> ppr new_tycon)
-               vars <- mapM (newVar . tyVarKind) (tyConTyVars new_tycon)
+               (_, vars, _) <- instTyVars (tyConTyVars new_tycon)
                let ty' = mkTyConApp new_tycon vars
-               liftTcM (boxyUnify ty (repType ty'))
+               _ <- liftTcM (unifyType ty (repType ty'))
         -- assumes that reptype doesn't ^^^^ touch tyconApp args 
                return ty'
 
 
 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 tv RuntimeUnk
+            -- This is where RuntimeUnks are born: 
+            -- otherwise-unconstrained unification variables are
+            -- turned into RuntimeUnks as they leave the
+            -- typechecker's monad
+           ; return (mkTyVarTy tv') }
 
 --------------------------------------------------------------------------------
--- representation types for thetas
-rttiView :: Type -> Type
-rttiView ty | Just ty' <- coreView ty  = rttiView ty'
-rttiView ty
-  | (tvs, theta, tau) <- tcSplitSigmaTy ty
-  =  mkForAllTys tvs (mkFunTys [predTypeRep p | p <- theta, isClassPred p] tau)
-
 -- Restore Class predicates out of a representation type
 dictsView :: Type -> Type
 -- dictsView ty = ty
@@ -1108,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
 
@@ -1132,17 +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
 
-
-mapMif :: Monad m => (a -> Bool) -> (a -> m a) -> [a] -> m [a]
-mapMif pred f xx = sequence $ mapMif_ pred f xx
-  where
-   mapMif_ _ _ []     = []
-   mapMif_ pred f (x:xx) = (if pred x then f x else return x) : mapMif_ pred f xx
+quantifyType :: Type -> QuantifiedType
+-- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
+quantifyType ty = (varSetElems (tyVarsOfType ty), ty)
 
 unlessM :: Monad m => m Bool -> m () -> m ()
 unlessM condM acc = condM >>= \c -> unless c acc
@@ -1160,24 +1196,10 @@ amap' f (Array i0 i _ arr#) = map g [0 .. i - i0]
     where g (I# i#) = case indexArray# arr# i# of
                           (# e #) -> f e
 
-
-isLifted :: Type -> Bool
-isLifted =  not . isUnLiftedType
-
 extractUnboxed  :: [Type] -> Closure -> [[Word]]
 extractUnboxed tt clos = go tt (nonPtrs clos)
-   where sizeofType t
-           | Just (tycon,_) <- tcSplitTyConApp_maybe t
-           = ASSERT (isPrimTyCon tycon) sizeofTyCon tycon
-           | otherwise = pprPanic "Expected a TcTyCon" (ppr t)
+   where sizeofType t = primRepSizeW (typePrimRep t)
          go [] _ = []
          go (t:tt) xx 
            | (x, rest) <- splitAt (sizeofType t) xx
            = x : go tt rest
-
-sizeofTyCon :: TyCon -> Int -- in *words*
-sizeofTyCon = primRepSizeW . tyConPrimRep
-
-
-(|.|) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
-(f |.| g) x = f x || g x
\ No newline at end of file