Tidy up SigTv
[ghc-hetmet.git] / compiler / ghci / RtClosureInspect.hs
index 2d49ad7..b4068a7 100644 (file)
 -----------------------------------------------------------------------------
 
 module RtClosureInspect(
-  
-     cvObtainTerm,       -- :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Term
+     cvObtainTerm,      -- :: HscEnv -> Int -> Bool -> Maybe Type -> HValue -> IO Term
+     cvReconstructType,
+     improveRTTIType,
 
      Term(..),
-     pprTerm, 
-     cPprTerm, 
-     cPprTermBase,
-     termType,
-     foldTerm, 
-     TermFold(..), 
-     idTermFold, 
-     idTermFoldM,
-     isFullyEvaluated, 
-     isPointed,
-     isFullyEvaluatedTerm,
-     mapTermType,
-     termTyVars,
---     unsafeDeepSeq, 
-     reconstructType
- ) where 
+     isTerm, isSuspension, isPrim, isFun, isFunLike, isNewtypeWrap,
+     isFullyEvaluated, isFullyEvaluatedTerm,
+     termType, mapTermType, termTyVars,
+     foldTerm, TermFold(..), foldTermM, TermFoldM(..), idTermFold,
+     pprTerm, cPprTerm, cPprTermBase, CustomTermPrinter,
+
+--     unsafeDeepSeq,
+
+     Closure(..), getClosureData, ClosureType(..), isConstr, isIndirection
+ ) where
 
 #include "HsVersions.h"
 
 import ByteCodeItbls    ( StgInfoTable )
 import qualified ByteCodeItbls as BCI( StgInfoTable(..) )
-import ByteCodeLink     ( HValue )
-import HscTypes         ( HscEnv )
+import HscTypes
+import Linker
 
-import DataCon          
-import Type             
-import TcRnMonad        ( TcM, initTcPrintErrors, ioToTcRn, recoverM, writeMutVar )
+import DataCon
+import Type
+import qualified Unify as U
+import TypeRep         -- I know I know, this is cheating
+import Var
+import TcRnMonad
 import TcType
 import TcMType
 import TcUnify
-import TcGadt
-import TyCon           
-import Var
-import Name 
+import TcEnv
+
+import TyCon
+import Name
 import VarEnv
-import OccName
+import Util
+import ListSetOps
 import VarSet
-import {-#SOURCE#-} TcRnDriver ( tcRnRecoverDataCon )
-
-import TysPrim         
+import TysPrim
 import PrelNames
 import TysWiredIn
-
-import Constants
+import DynFlags
 import Outputable
-import Maybes
-import Panic
-import FiniteMap
+import FastString
+-- import Panic
+
+import Constants        ( wORD_SIZE )
 
 import GHC.Arr          ( Array(..) )
-import GHC.Ptr          ( Ptr(..), castPtr )
 import GHC.Exts
+import GHC.IO ( IO(..) )
 
 import Control.Monad
 import Data.Maybe
 import Data.Array.Base
-import Data.List        ( partition, nub )
-import Foreign
+import Data.Ix
+import Data.List
+import qualified Data.Sequence as Seq
+import Data.Monoid
+import Data.Sequence (viewl, ViewL(..))
+import Foreign hiding (unsafePerformIO)
+import System.IO.Unsafe
 
 ---------------------------------------------
 -- * A representation of semi evaluated Terms
 ---------------------------------------------
-{-
-  A few examples in this representation:
-
-  > Just 10 = Term Data.Maybe Data.Maybe.Just (Just 10) [Term Int I# (10) "10"]
 
-  > (('a',_,_),_,('b',_,_)) = 
-      Term ((Char,b,c),d,(Char,e,f)) (,,) (('a',_,_),_,('b',_,_))
-          [ Term (Char, b, c) (,,) ('a',_,_) [Term Char C# "a", Suspension, Suspension]
-          , Suspension
-          , Term (Char, e, f) (,,) ('b',_,_) [Term Char C# "b", Suspension, Suspension]]
--}
-
-data Term = Term { ty        :: Type 
-                 , dc        :: DataCon 
+data Term = Term { ty        :: RttiType
+                 , dc        :: Either String DataCon
+                               -- Carries a text representation if the datacon is
+                               -- not exported by the .hi file, which is the case 
+                               -- for private constructors in -O0 compiled libraries
                  , val       :: HValue 
                  , subTerms  :: [Term] }
 
-          | Prim { ty        :: Type
+          | Prim { ty        :: RttiType
                  , value     :: [Word] }
 
           | Suspension { ctype    :: ClosureType
-                       , mb_ty    :: Maybe Type
+                       , ty       :: RttiType
                        , val      :: HValue
                        , bound_to :: Maybe Name   -- Useful for printing
                        }
-
+          | NewtypeWrap{       -- At runtime there are no newtypes, and hence no
+                               -- newtype constructors. A NewtypeWrap is just a
+                               -- made-up tag saying "heads up, there used to be
+                               -- a newtype constructor here".
+                         ty           :: RttiType
+                       , dc           :: Either String DataCon
+                       , wrapped_term :: Term }
+          | RefWrap    {       -- The contents of a reference
+                         ty           :: RttiType
+                       , wrapped_term :: Term }
+
+isTerm, isSuspension, isPrim, isFun, isFunLike, isNewtypeWrap :: Term -> Bool
 isTerm Term{} = True
 isTerm   _    = False
 isSuspension Suspension{} = True
 isSuspension      _       = False
 isPrim Prim{} = True
 isPrim   _    = False
+isNewtypeWrap NewtypeWrap{} = True
+isNewtypeWrap _             = False
 
-termType t@(Suspension {}) = mb_ty t
-termType t = Just$ ty t
+isFun Suspension{ctype=Fun} = True
+isFun _ = False
+
+isFunLike s@Suspension{ty=ty} = isFun s || isFunTy ty
+isFunLike _ = False
+
+termType :: Term -> RttiType
+termType t = ty t
 
 isFullyEvaluatedTerm :: Term -> Bool
 isFullyEvaluatedTerm Term {subTerms=tt} = all isFullyEvaluatedTerm tt
-isFullyEvaluatedTerm Suspension {}      = False
 isFullyEvaluatedTerm Prim {}            = True
+isFullyEvaluatedTerm NewtypeWrap{wrapped_term=t} = isFullyEvaluatedTerm t
+isFullyEvaluatedTerm RefWrap{wrapped_term=t}     = isFullyEvaluatedTerm t
+isFullyEvaluatedTerm _                  = False
 
 instance Outputable (Term) where
- ppr = head . cPprTerm cPprTermBase
+ ppr t | Just doc <- cPprTerm cPprTermBase t = doc
+       | otherwise = panic "Outputable Term instance"
 
 -------------------------------------------------------------------------
 -- Runtime Closure Datatype and functions for retrieving closure related stuff
@@ -128,7 +144,9 @@ data ClosureType = Constr
                  | AP 
                  | PAP 
                  | Indirection Int 
-                 | Other Int
+                 | MutVar Int
+                 | MVar   Int
+                 | Other  Int
  deriving (Show, Eq)
 
 data Closure = Closure { tipe         :: ClosureType 
@@ -141,8 +159,9 @@ 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
 pAP_CODE = PAP
 #undef AP
@@ -152,33 +171,47 @@ getClosureData :: a -> IO Closure
 getClosureData a =
    case unpackClosure# a of 
      (# iptr, ptrs, nptrs #) -> do
-           itbl <- peek (Ptr iptr)
+           let iptr'
+                | ghciTablesNextToCode =
+                   Ptr iptr
+                | otherwise =
+                   -- the info pointer we get back from unpackClosure#
+                   -- is to the beginning of the standard info table,
+                   -- but the Storable instance for info tables takes
+                   -- into account the extra entry pointer when
+                   -- !ghciTablesNextToCode, so we must adjust here:
+                   Ptr iptr `plusPtr` negate wORD_SIZE
+           itbl <- peek iptr'
            let tipe = readCType (BCI.tipe itbl)
-               elems = BCI.ptrs itbl 
-               ptrsList = Array 0 (fromIntegral$ elems) ptrs
+               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)] ]
-           ptrsList `seq` return (Closure tipe (Ptr iptr) itbl ptrsList nptrs_data)
+           ASSERT(elems >= 0) return ()
+           ptrsList `seq` 
+            return (Closure tipe (Ptr iptr) itbl ptrsList nptrs_data)
 
 readCType :: Integral a => a -> ClosureType
-readCType i
+readCType i 
  | i >= CONSTR && i <= CONSTR_NOCAF_STATIC = Constr
  | i >= FUN    && i <= FUN_STATIC          = Fun
- | i >= THUNK  && i < THUNK_SELECTOR       = Thunk (fromIntegral i)
+ | i >= THUNK  && i < THUNK_SELECTOR       = Thunk i'
  | i == THUNK_SELECTOR                     = ThunkSelector
  | i == BLACKHOLE                          = Blackhole
- | i >= IND    && i <= IND_STATIC          = Indirection (fromIntegral i)
- | fromIntegral i == aP_CODE               = AP
+ | i >= IND    && i <= IND_STATIC          = Indirection i'
+ | i' == aP_CODE                           = AP
  | i == AP_STACK                           = AP
- | fromIntegral i == pAP_CODE              = PAP
- | otherwise                               = Other (fromIntegral i)
-
-isConstr, isIndirection :: ClosureType -> Bool
+ | i' == pAP_CODE                          = PAP
+ | i == MUT_VAR_CLEAN || i == MUT_VAR_DIRTY= MutVar i'
+ | i == MVAR_CLEAN    || i == MVAR_DIRTY   = MVar i'
+ | otherwise                               = Other  i'
+  where i' = fromIntegral i
+isConstr, isIndirection, isThunk :: ClosureType -> Bool
 isConstr Constr = True
 isConstr    _   = False
 
 isIndirection (Indirection _) = True
---isIndirection ThunkSelector = True
 isIndirection _ = False
 
 isThunk (Thunk _)     = True
@@ -192,161 +225,245 @@ isFullyEvaluated a = do
   case tipe closure of
     Constr -> do are_subs_evaluated <- amapM isFullyEvaluated (ptrs closure)
                  return$ and are_subs_evaluated
-    otherwise -> return False
+    _      -> return False
   where amapM f = sequence . amap' f
 
-amap' f (Array i0 i arr#) = map (\(I# i#) -> case indexArray# arr# i# of
-                                   (# e #) -> f e)
-                                [0 .. i - i0]
-
 -- TODO: Fix it. Probably the otherwise case is failing, trace/debug it
 {-
 unsafeDeepSeq :: a -> b -> b
 unsafeDeepSeq = unsafeDeepSeq1 2
  where unsafeDeepSeq1 0 a b = seq a $! b
-       unsafeDeepSeq1 i a b                -- 1st case avoids infinite loops for non reducible thunks
+       unsafeDeepSeq1 i a b   -- 1st case avoids infinite loops for non reducible thunks
         | not (isConstr tipe) = seq a $! unsafeDeepSeq1 (i-1) a b     
      -- | unsafePerformIO (isFullyEvaluated a) = b
         | otherwise = case unsafePerformIO (getClosureData a) of
                         closure -> foldl' (flip unsafeDeepSeq) b (ptrs closure)
         where tipe = unsafePerformIO (getClosureType a)
 -}
-isPointed :: Type -> Bool
-isPointed t | Just (t, _) <- splitTyConApp_maybe t = not$ isUnliftedTypeKind (tyConKind t)
-isPointed _ = True
-
-extractUnboxed  :: [Type] -> Closure -> [[Word]]
-extractUnboxed tt clos = go tt (nonPtrs clos)
-   where sizeofType t
-           | Just (tycon,_) <- splitTyConApp_maybe t
-           = ASSERT (isPrimTyCon tycon) sizeofTyCon tycon
-           | otherwise = pprPanic "Expected a TcTyCon" (ppr t)
-         go [] _ = []
-         go (t:tt) xx 
-           | (x, rest) <- splitAt (sizeofType t `div` wORD_SIZE) xx 
-           = x : go tt rest
-
-sizeofTyCon = sizeofPrimRep . tyConPrimRep
 
 -----------------------------------
 -- * Traversals for Terms
 -----------------------------------
+type TermProcessor a b = RttiType -> Either String DataCon -> HValue -> [a] -> b
+
+data TermFold a = TermFold { fTerm        :: TermProcessor a a
+                           , fPrim        :: RttiType -> [Word] -> a
+                           , fSuspension  :: ClosureType -> RttiType -> HValue
+                                            -> Maybe Name -> a
+                           , fNewtypeWrap :: RttiType -> Either String DataCon
+                                            -> a -> a
+                           , fRefWrap     :: RttiType -> a -> a
+                           }
+
 
-data TermFold a = TermFold { fTerm :: Type -> DataCon -> HValue -> [a] -> a
-                           , fPrim :: Type -> [Word] -> a
-                           , fSuspension :: ClosureType -> Maybe Type -> HValue -> Maybe Name -> a
+data TermFoldM m a =
+                   TermFoldM {fTermM        :: TermProcessor a (m a)
+                            , fPrimM        :: RttiType -> [Word] -> m a
+                            , fSuspensionM  :: ClosureType -> RttiType -> HValue
+                                             -> Maybe Name -> m a
+                            , fNewtypeWrapM :: RttiType -> Either String DataCon
+                                            -> a -> m a
+                            , fRefWrapM     :: RttiType -> a -> m a
                            }
 
 foldTerm :: TermFold a -> Term -> a
 foldTerm tf (Term ty dc v tt) = fTerm tf ty dc v (map (foldTerm tf) tt)
 foldTerm tf (Prim ty    v   ) = fPrim tf ty v
 foldTerm tf (Suspension ct ty v b) = fSuspension tf ct ty v b
+foldTerm tf (NewtypeWrap ty dc t)  = fNewtypeWrap tf ty dc (foldTerm tf t)
+foldTerm tf (RefWrap ty t)         = fRefWrap tf ty (foldTerm tf t)
+
+
+foldTermM :: Monad m => TermFoldM m a -> Term -> m a
+foldTermM tf (Term ty dc v tt) = mapM (foldTermM tf) tt >>= fTermM tf ty dc v
+foldTermM tf (Prim ty    v   ) = fPrimM tf ty v
+foldTermM tf (Suspension ct ty v b) = fSuspensionM tf ct ty v b
+foldTermM tf (NewtypeWrap ty dc t)  = foldTermM tf t >>=  fNewtypeWrapM tf ty dc
+foldTermM tf (RefWrap ty t)         = foldTermM tf t >>= fRefWrapM tf ty
 
 idTermFold :: TermFold Term
 idTermFold = TermFold {
               fTerm = Term,
               fPrim = Prim,
-              fSuspension = Suspension
+              fSuspension  = Suspension,
+              fNewtypeWrap = NewtypeWrap,
+              fRefWrap = RefWrap
                       }
-idTermFoldM :: Monad m => TermFold (m Term)
-idTermFoldM = TermFold {
-              fTerm       = \ty dc v tt -> sequence tt >>= return . Term ty dc v,
-              fPrim       = (return.). Prim,
-              fSuspension = (((return.).).). Suspension
-                       }
 
+mapTermType :: (RttiType -> Type) -> Term -> Term
 mapTermType f = foldTerm idTermFold {
           fTerm       = \ty dc hval tt -> Term (f ty) dc hval tt,
-          fSuspension = \ct mb_ty hval n ->
-                          Suspension ct (fmap f mb_ty) hval n }
-
+          fSuspension = \ct ty hval n ->
+                          Suspension ct (f ty) hval n,
+          fNewtypeWrap= \ty dc t -> NewtypeWrap (f ty) dc t,
+          fRefWrap    = \ty t -> RefWrap (f ty) t}
+
+mapTermTypeM :: Monad m =>  (RttiType -> m Type) -> Term -> m Term
+mapTermTypeM f = foldTermM TermFoldM {
+          fTermM       = \ty dc hval tt -> f ty >>= \ty' -> return $ Term ty'  dc hval tt,
+          fPrimM       = (return.) . Prim,
+          fSuspensionM = \ct ty hval n ->
+                          f ty >>= \ty' -> return $ Suspension ct ty' hval n,
+          fNewtypeWrapM= \ty dc t -> f ty >>= \ty' -> return $ NewtypeWrap ty' dc t,
+          fRefWrapM    = \ty t -> f ty >>= \ty' -> return $ RefWrap ty' t}
+
+termTyVars :: Term -> TyVarSet
 termTyVars = foldTerm TermFold {
             fTerm       = \ty _ _ tt   -> 
                           tyVarsOfType ty `plusVarEnv` concatVarEnv tt,
-            fSuspension = \_ mb_ty _ _ -> 
-                          maybe emptyVarEnv tyVarsOfType mb_ty,
-            fPrim       = \ _ _ -> emptyVarEnv }
+            fSuspension = \_ ty _ _ -> tyVarsOfType ty,
+            fPrim       = \ _ _ -> emptyVarEnv,
+            fNewtypeWrap= \ty _ t -> tyVarsOfType ty `plusVarEnv` t,
+            fRefWrap    = \ty t -> tyVarsOfType ty `plusVarEnv` t}
     where concatVarEnv = foldr plusVarEnv emptyVarEnv
+
 ----------------------------------
 -- Pretty printing of terms
 ----------------------------------
 
-app_prec::Int
-app_prec = 10
+type Precedence        = Int
+type TermPrinter       = Precedence -> Term ->   SDoc
+type TermPrinterM m    = Precedence -> Term -> m SDoc
+
+app_prec,cons_prec, max_prec ::Int
+max_prec  = 10
+app_prec  = max_prec
+cons_prec = 5 -- TODO Extract this info from GHC itself
+
+pprTerm :: TermPrinter -> TermPrinter
+pprTerm y p t | Just doc <- pprTermM (\p -> Just . y p) p t = doc
+pprTerm _ _ _ = panic "pprTerm"
+
+pprTermM, ppr_termM, pprNewtypeWrap :: Monad m => TermPrinterM m -> TermPrinterM m
+pprTermM y p t = pprDeeper `liftM` ppr_termM y p t
+
+ppr_termM y p Term{dc=Left dc_tag, subTerms=tt} = do
+  tt_docs <- mapM (y app_prec) tt
+  return$ cparen (not(null tt) && p >= app_prec) (text dc_tag <+> pprDeeperList fsep tt_docs)
+  
+ppr_termM y p Term{dc=Right dc, subTerms=tt} 
+{-  | dataConIsInfix dc, (t1:t2:tt') <- tt  --TODO fixity
+  = 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)
+
+ppr_termM y p t@NewtypeWrap{} = pprNewtypeWrap y p t
+ppr_termM y p RefWrap{wrapped_term=t}  = do
+  contents <- y app_prec t
+  return$ cparen (p >= app_prec) (text "GHC.Prim.MutVar#" <+> contents)
+  -- The constructor name is wired in here ^^^ for the sake of simplicity.
+  -- I don't think mutvars are going to change in a near future.
+  -- In any case this is solely a presentation matter: MutVar# is
+  -- a datatype with no constructors, implemented by the RTS
+  -- (hence there is no way to obtain a datacon and print it).
+ppr_termM _ _ t = ppr_termM1 t
+
+
+ppr_termM1 :: Monad m => Term -> m SDoc
+ppr_termM1 Prim{value=words, ty=ty} = 
+    return$ text$ repPrim (tyConAppTyCon ty) words
+ppr_termM1 Suspension{ty=ty, bound_to=Nothing} = 
+    return (char '_' <+> ifPprDebug (text "::" <> ppr ty))
+ppr_termM1 Suspension{ty=ty, bound_to=Just n}
+--  | Just _ <- splitFunTy_maybe ty = return$ ptext (sLit("<function>")
+  | otherwise = return$ parens$ ppr n <> text "::" <> ppr ty
+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}
+  | 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)
+pprNewtypeWrap _ _ _ = panic "pprNewtypeWrap"
+
+-------------------------------------------------------
+-- Custom Term Pretty Printers
+-------------------------------------------------------
+
+-- We can want to customize the representation of a 
+--  term depending on its type. 
+-- However, note that custom printers have to work with
+--  type representations, instead of directly with types.
+-- We cannot use type classes here, unless we employ some 
+--  typerep trickery (e.g. Weirich's RepLib tricks),
+--  which I didn't. Therefore, this code replicates a lot
+--  of what type classes provide for free.
+
+type CustomTermPrinter m = TermPrinterM m
+                         -> [Precedence -> Term -> (m (Maybe SDoc))]
+
+-- | Takes a list of custom printers with a explicit recursion knot and a term, 
+-- and returns the output of the first succesful printer, or the default printer
+cPprTerm :: Monad m => CustomTermPrinter m -> Term -> m SDoc
+cPprTerm printers_ = go 0 where
+  printers = printers_ go
+  go prec t = do
+    let default_ = Just `liftM` pprTermM go prec t
+        mb_customDocs = [pp prec t | pp <- printers] ++ [default_]
+    Just doc <- firstJustM mb_customDocs
+    return$ cparen (prec>app_prec+1) doc
 
-pprTerm :: Int -> Term -> SDoc
-pprTerm p Term{dc=dc, subTerms=tt} 
-{-  | dataConIsInfix dc, (t1:t2:tt') <- tt 
-  = parens (pprTerm1 True t1 <+> ppr dc <+> pprTerm1 True ppr t2) 
-    <+> hsep (map (pprTerm1 True) tt) 
--}
-  | null tt   = ppr dc
-  | otherwise = cparen (p >= app_prec) 
-                       (ppr dc <+> sep (map (pprTerm app_prec) tt))
-
-  where fixity   = undefined 
-
-pprTerm _ t = pprTerm1 t
-
-pprTerm1 Prim{value=words, ty=ty} = text$ repPrim (tyConAppTyCon ty) words
-pprTerm1 t@Term{} = pprTerm 0 t 
-pprTerm1 Suspension{bound_to=Nothing} =  char '_' -- <> ppr ct <> char '_'
-pprTerm1 Suspension{mb_ty=Just ty, bound_to=Just n}
-  | Just _ <- splitFunTy_maybe ty = ptext SLIT("<function>")
-  | otherwise = parens$ ppr n <> text "::" <> ppr ty 
-
-
-cPprTerm :: forall m. Monad m => ((Int->Term->m SDoc)->[Int->Term->m (Maybe SDoc)]) -> Term -> m SDoc
-cPprTerm custom = go 0 where
-  go prec t@Term{subTerms=tt, dc=dc} = do
-    let mb_customDocs = map (($t) . ($prec)) (custom go) :: [m (Maybe SDoc)]    
-    first_success <- firstJustM mb_customDocs
-    case first_success of
-      Just doc -> return$ cparen (prec>app_prec+1) doc
---    | dataConIsInfix dc, (t1:t2:tt') <- tt =
-      Nothing  -> do pprSubterms <- mapM (go (app_prec+1)) tt
-                     return$ cparen (prec >= app_prec) 
-                                    (ppr dc <+> sep pprSubterms)
-  go _ t = return$ pprTerm1 t
   firstJustM (mb:mbs) = mb >>= maybe (firstJustM mbs) (return . Just)
   firstJustM [] = return Nothing
 
-cPprTermBase :: Monad m => (Int->Term-> m SDoc)->[Int->Term->m (Maybe SDoc)]
-cPprTermBase pprP =
-  [ 
-    ifTerm isTupleDC            (\_ -> liftM (parens . hcat . punctuate comma) 
-                                 . mapM (pprP (-1)) . subTerms)
-  , ifTerm (isDC consDataCon)   (\ p Term{subTerms=[h,t]} -> doList p h t)
-  , ifTerm (isDC intDataCon)    (coerceShow$ \(a::Int)->a)
-  , ifTerm (isDC charDataCon)   (coerceShow$ \(a::Char)->a)
---  , ifTerm (isDC wordDataCon) (coerceShow$ \(a::Word)->a)
-  , ifTerm (isDC floatDataCon)  (coerceShow$ \(a::Float)->a)
-  , ifTerm (isDC doubleDataCon) (coerceShow$ \(a::Double)->a)
-  , ifTerm isIntegerDC          (coerceShow$ \(a::Integer)->a)
-  ] 
-     where ifTerm pred f p t = if pred t then liftM Just (f p t) else return Nothing
-           isIntegerDC Term{dc=dc} = 
-              dataConName dc `elem` [ smallIntegerDataConName
-                                    , largeIntegerDataConName] 
-           isTupleDC Term{dc=dc} = dc `elem` snd (unzip (elems boxedTupleArr))
-           isDC a_dc Term{dc=dc} = a_dc == dc
-           coerceShow f _ = return . text . show . f . unsafeCoerce# . val
-           --TODO pprinting of list terms is not lazy
-           doList p h t = do
-               let elems = h : getListTerms t
-                   isConsLast = termType(last elems) /= termType h
-               print_elems <- mapM (pprP 5) elems
+-- Default set of custom printers. Note that the recursion knot is explicit
+cPprTermBase :: 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 t -> doList p 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)
+  ]
+     where 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)
+
+           coerceShow f _p = return . text . show . f . unsafeCoerce# . val
+
+           --Note pprinting of list terms is not lazy
+           doList p (Term{subTerms=[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 >= 5) . hsep . punctuate (space<>colon) 
-                           $ print_elems
-                     else brackets (hcat$ punctuate comma print_elems)
-
-                where Just a /= Just b = not (a `coreEqType` b)
-                      _      /=   _    = True
-                      getListTerms Term{subTerms=[h,t]} = h : getListTerms t
-                      getListTerms t@Term{subTerms=[]}  = []
+                     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)
+           doList _ _ = panic "doList"
+
 
 repPrim :: TyCon -> [Word] -> String
 repPrim t = rep where 
@@ -376,6 +493,8 @@ repPrim t = rep where
     | t == tVarPrimTyCon  = "<tVar>"
     | otherwise = showSDoc (char '<' <> ppr t <> char '>')
     where build ww = unsafePerformIO $ withArray ww (peek . castPtr) 
+--   This ^^^ relies on the representation of Haskell heap values being 
+--   the same as in a C array. 
 
 -----------------------------------
 -- Type Reconstruction
@@ -398,259 +517,712 @@ Right hand sides are missing them. We can either (a) drop them from the lhs, or
 The function congruenceNewtypes takes a shot at (b)
 -}
 
+
+-- A (non-mutable) tau type containing
+-- existentially quantified tyvars.
+--    (since GHC type language currently does not support
+--     existentials, we leave these variables unquantified)
+type RttiType = Type
+
+-- An incomplete type as stored in GHCi:
+--  no polymorphism: no quantifiers & all tyvars are skolem.
+type GhciType = Type
+
+
 -- The Type Reconstruction monad
+--------------------------------
 type TR a = TcM a
 
 runTR :: HscEnv -> TR a -> IO a
-runTR hsc_env c = do 
-  mb_term <- initTcPrintErrors hsc_env iNTERACTIVE c
-  case mb_term of 
-    Nothing -> panic "Can't unify"
-    Just x -> return x
+runTR hsc_env thing = do
+  mb_val <- runTR_maybe hsc_env thing
+  case mb_val of
+    Nothing -> error "unable to :print the term"
+    Just x  -> return x
 
-trIO :: IO a -> TR a 
-trIO = liftTcM . ioToTcRn
+runTR_maybe :: HscEnv -> TR a -> IO (Maybe a)
+runTR_maybe hsc_env = fmap snd . initTc hsc_env HsSrcFile False  iNTERACTIVE
+
+traceTR :: SDoc -> TR ()
+traceTR = liftTcM . traceOptTcRn Opt_D_dump_rtti
 
-liftTcM = id
 
-newVar :: Kind -> TR TcTyVar
-newVar = liftTcM . newFlexiTyVar
+-- Semantically different to recoverM in TcRnMonad 
+-- recoverM retains the errors in the first action,
+--  whereas recoverTc here does not
+recoverTR :: TR a -> TR a -> TR a
+recoverTR recover thing = do 
+  (_,mb_res) <- tryTcErrs thing
+  case mb_res of 
+    Nothing  -> recover
+    Just res -> return res
 
--- | Returns the instantiated type scheme ty', and the substitution sigma 
---   such that sigma(ty') = ty 
-instScheme :: Type -> TR (TcType, TvSubst)
-instScheme ty | (tvs, rho) <- tcSplitForAllTys ty = liftTcM$ do
-   (tvs',theta,ty') <- tcInstType (mapM tcInstTyVar) ty
-   return (ty', zipTopTvSubst tvs' (mkTyVarTys tvs))
+trIO :: IO a -> TR a 
+trIO = liftTcM . liftIO
 
+liftTcM :: TcM a -> TR a
+liftTcM = id
+
+newVar :: Kind -> TR TcType
+newVar = liftTcM . newFlexiTyVarTy
+
+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
+-- t2 is expected to come from a datacon signature
+-- Before unification, congruenceNewtypes needs to
+-- do its magic.
 addConstraint :: TcType -> TcType -> TR ()
-addConstraint t1 t2  = congruenceNewtypes t1 t2 >>= uncurry unifyType 
-
-
-
--- Type & Term reconstruction 
-cvObtainTerm :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Term
-cvObtainTerm hsc_env force mb_ty hval = runTR hsc_env $ do
-   tv <- liftM mkTyVarTy (newVar argTypeKind)
-   case mb_ty of
-     Nothing -> go tv tv hval >>= zonkTerm
-     Just ty | isMonomorphic ty -> go ty ty hval >>= zonkTerm
-     Just ty -> do 
-              (ty',rev_subst) <- instScheme (sigmaType ty)
-              addConstraint tv ty'
-              term <- go tv tv hval >>= zonkTerm
-              --restore original Tyvars
-              return$ mapTermType (substTy rev_subst) term
+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]) $
+      do { (ty1, ty2) <- congruenceNewtypes actual expected
+         ; _  <- captureConstraints $ unifyType ty1 ty2
+         ; return () }
+     -- TOMDO: what about the coercion?
+     -- we should consider family instances
+
+
+-- 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 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 null old_tvs
+      then do
+        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 quant_old_ty
+              my_ty <- newVar argTypeKind
+              when (check1 quant_old_ty) (traceTR (text "check1 passed") >>
+                                          addConstraint my_ty old_ty')
+              term  <- go max_depth my_ty sigma_old_ty hval
+              new_ty <- zonkTcType (termType term)
+              if isMonomorphic new_ty || check2 (quantifyType new_ty) quant_old_ty
+                 then do
+                      traceTR (text "check2 passed")
+                      addConstraint new_ty old_ty'
+                      applyRevSubst rev_subst
+                      zterm' <- zonkTerm term
+                      return ((fixFunDictionaries . expandNewtypes) zterm')
+                 else do
+                      traceTR (text "check2 failed" <+> parens
+                                       (ppr term <+> text "::" <+> ppr new_ty))
+                      -- we have unsound types. Replace constructor types in
+                      -- subterms with tyvars
+                      zterm' <- mapTermTypeM
+                                 (\ty -> case tcSplitTyConApp_maybe ty of
+                                           Just (tc, _:_) | tc /= funTyCon
+                                               -> newVar argTypeKind
+                                           _   -> return ty)
+                                 term
+                      zonkTerm zterm'
+   traceTR (text "Term reconstruction completed." $$
+            text "Term obtained: " <> ppr term $$
+            text "Type obtained: " <> ppr (termType term))
+   return term
     where 
-  go tv ty a = do 
-    let monomorphic = not(isTyVarTy tv)   -- This is a convention. The ancestor tests for
-                                         -- monomorphism and passes a type instead of a tv
+  go :: Int -> Type -> Type -> HValue -> TcM Term
+  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
+    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 -> seq a $ go tv ty a
--- We always follow indirections 
-      Indirection _ -> go tv ty $! (ptrs clos ! 0)
+      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)
+-- We also follow references
+      MutVar _ | Just (tycon,[world,contents_ty]) <- tcSplitTyConApp_maybe old_ty
+             -> do
+                  -- Deal with the MutVar# primitive
+                  -- It does not have a constructor at all, 
+                  -- so we simulate the following one
+                  -- MutVar# :: contents_ty -> MutVar# s contents_ty
+         traceTR (text "Following a MutVar")
+         contents_tv <- newVar liftedTypeKind
+         contents <- trIO$ IO$ \w -> readMutVar# (unsafeCoerce# a) w
+         ASSERT(isUnliftedTypeKind $ typeKind my_ty) return ()
+         (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
+         return (RefWrap my_ty x)
+
  -- The interesting case
       Constr -> do
-        m_dc <- trIO$ tcRnRecoverDataCon hsc_env (infoPtr clos)
-        case m_dc of
-          Nothing -> panic "Can't find the DataCon for a term"
-          Just dc -> do 
-            let extra_args = length(dataConRepArgTys dc) - length(dataConOrigArgTys dc)
-                subTtypes  = matchSubTypes dc ty
-                (subTtypesP, subTtypesNP) = partition isPointed subTtypes
-            subTermTvs <- sequence
-                 [ if isMonomorphic t then return t else (mkTyVarTy `fmap` newVar k)
-                   | (t,k) <- zip subTtypesP (map typeKind subTtypesP)]
-            -- It is vital for newtype reconstruction that the unification step is done
-            --     right here, _before_ the subterms are RTTI reconstructed.
+        traceTR (text "entering a constructor " <>
+                      if monomorphic
+                        then parens (text "already monomorphic: " <> ppr my_ty)
+                        else Outputable.empty)
+        Right dcname <- dataConInfoPtrToName (infoPtr clos)
+        (_,mb_dc)    <- tryTcErrs (tcLookupDataCon dcname)
+        case mb_dc of
+          Nothing -> do -- This can happen for private constructors compiled -O0
+                        -- where the .hi descriptor does not export them
+                        -- In such case, we return a best approximation:
+                        --  ignore the unpointed args, and recover the pointeds
+                        -- This preserves laziness, and should be safe.
+                       let tag = showSDoc (ppr dcname)
+                       vars     <- replicateM (length$ elems$ ptrs clos) 
+                                              (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
+            subTermTvs    <- mapMif (not . isMonomorphic)
+                                    (\t -> newVar (typeKind t))
+                                    subTtypes
+            let (subTermsP, subTermsNP) = partition (\(ty,_) -> isLifted ty
+                                                             || isRefType ty)
+                                                    (zip subTtypes subTermTvs)
+                (subTtypesP,   subTermTvsP ) = unzip subTermsP
+                (subTtypesNP, _subTermTvsNP) = unzip subTermsNP
+
+            -- When we already have all the information, avoid solving
+            -- unnecessary constraints. Propagation of type information
+            -- to subterms is already being done via matching.
             when (not monomorphic) $ do
-                  let myType = mkFunTys (reOrderTerms subTermTvs subTtypesNP subTtypes) tv
-                  instScheme(dataConRepType dc) >>= addConstraint myType . fst
-            subTermsP <- sequence $ drop extra_args -- all extra arguments are pointed
-                  [ appArr (go tv t) (ptrs clos) i
-                   | (i,tv,t) <- zip3 [0..] subTermTvs subTtypesP]
+               let myType = mkFunTys subTermTvs my_ty
+               (signatureType,_) <- instScheme (mydataConType dc)
+            -- It is vital for newtype reconstruction that the unification step
+            -- is done right here, _before_ the subterms are RTTI reconstructed
+               addConstraint myType signatureType
+            subTermsP <- sequence
+                  [ appArr (go (pred max_depth) tv t) (ptrs clos) i
+                   | (i,tv,t) <- zip3 [0..] subTermTvsP subTtypesP]
             let unboxeds   = extractUnboxed subTtypesNP clos
-                subTermsNP = map (uncurry Prim) (zip subTtypesNP unboxeds)      
-                subTerms   = reOrderTerms subTermsP subTermsNP (drop extra_args subTtypes)
-            return (Term tv dc a subTerms)
+                subTermsNP = map (uncurry Prim) (zip 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.
-      otherwise -> 
-         return (Suspension (tipe clos) (Just tv) a Nothing)
+      tipe_clos ->
+         return (Suspension tipe_clos my_ty a Nothing)
 
   matchSubTypes dc ty
-    | Just (_,ty_args) <- splitTyConApp_maybe (repType ty) 
-    , null (dataConExTyVars dc)  --TODO Handle the case of extra existential tyvars
-    = dataConInstArgTys dc ty_args
-
+    | 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
 
--- This is used to put together pointed and nonpointed subterms in the 
---  correct order.
+  -- put together pointed and nonpointed subterms in the
+  --  correct order.
   reOrderTerms _ _ [] = []
   reOrderTerms pointed unpointed (ty:tys) 
-   | isPointed ty = ASSERT2(not(null pointed)
-                           , ptext SLIT("reOrderTerms") $$ (ppr pointed $$ ppr unpointed))
-                    head pointed : reOrderTerms (tail pointed) unpointed tys
+   | isLifted ty || isRefType 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") $$ (ppr pointed $$ ppr unpointed))
-                    head unpointed : reOrderTerms pointed (tail unpointed) tys
-
-
-
--- Fast, breadth-first version of obtainTerm that deals only with type reconstruction
-
-cvReconstructType :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Type
-cvReconstructType hsc_env force mb_ty hval = runTR hsc_env $ do
-   tv <- liftM mkTyVarTy (newVar argTypeKind)
-   case mb_ty of
-     Nothing -> search (isMonomorphic `fmap` zonkTcType tv) (++) [(tv, hval)] >> 
-                zonkTcType tv  -- TODO untested!
-     Just ty | isMonomorphic ty -> return ty
-     Just ty -> do 
-              (ty',rev_subst) <- instScheme (sigmaType ty)
-              addConstraint tv ty'
-              search (isMonomorphic `fmap` zonkTcType tv) (++) [(tv, hval)]
-              substTy rev_subst `fmap` zonkTcType tv
-    where 
+                           , ptext (sLit "reOrderTerms") $$ 
+                                       (ppr pointed $$ ppr unpointed))
+                    let (t:tt) = unpointed in t : reOrderTerms pointed tt tys
+
+  -- insert NewtypeWraps around newtypes
+  expandNewtypes = foldTerm idTermFold { fTerm = worker } where
+   worker ty dc hval tt
+     | Just (tc, args) <- tcSplitTyConApp_maybe ty
+     , isNewTyCon tc
+     , wrapped_type    <- newTyConInstRhs tc args
+     , Just dc'        <- tyConSingleDataCon_maybe tc
+     , t'              <- worker wrapped_type dc hval tt
+     = NewtypeWrap ty (Right dc') t'
+     | otherwise = Term ty dc hval tt
+
+
+   -- Avoid returning types where predicates have been expanded to dictionaries.
+  fixFunDictionaries = foldTerm idTermFold {fSuspension = worker} where
+      worker ct ty hval n | isFunTy ty = Suspension ct (dictsView ty) hval n
+                          | otherwise  = Suspension ct ty hval n
+
+
+-- 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@(old_tvs, _) = quantifyType old_ty
+   new_ty <-
+       if null old_tvs
+        then return old_ty
+        else do
+          (old_ty', rev_subst) <- instScheme sigma_old_ty
+          my_ty <- newVar argTypeKind
+          when (check1 sigma_old_ty) (traceTR (text "check1 passed") >>
+                                      addConstraint my_ty old_ty')
+          search (isMonomorphic `fmap` zonkTcType my_ty)
+                 (\(ty,a) -> go ty a)
+                 (Seq.singleton (my_ty, hval))
+                 max_depth
+          new_ty <- zonkTcType my_ty
+          if isMonomorphic new_ty || check2 (quantifyType new_ty) sigma_old_ty
+            then do
+                 traceTR (text "check2 passed" <+> ppr old_ty $$ ppr new_ty)
+                 addConstraint my_ty old_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)
+   return new_ty
+    where
 --  search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m ()
-  search stop combine []     = return ()
-  search stop combine ((t,a):jj) =  (jj `combine`) `fmap` go t a >>= 
-                                    unlessM stop . search stop combine
-
-   -- returns unification tasks, since we are going to want a breadth-first search
+  search _ _ _ 0 = traceTR (text "Failed to reconstruct a type after " <>
+                                int max_depth <> text " steps")
+  search stop expand l d =
+    case viewl l of 
+      EmptyL  -> return ()
+      x :< xx -> unlessM stop $ do
+                  new <- expand x
+                  search stop expand (xx `mappend` Seq.fromList new) $! (pred d)
+
+   -- returns unification tasks,since we are going to want a breadth-first search
   go :: Type -> HValue -> TR [(Type, HValue)]
-  go tv a = do 
+  go my_ty a = do
     clos <- trIO $ getClosureData a
     case tipe clos of
-      Indirection _ -> go tv $! (ptrs clos ! 0)
+      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
+         tv'   <- newVar liftedTypeKind
+         world <- newVar liftedTypeKind
+         addConstraint my_ty (mkTyConApp mutVarPrimTyCon [world,tv'])
+         return [(tv', contents)]
       Constr -> do
-        m_dc <- trIO$ tcRnRecoverDataCon hsc_env (infoPtr clos)
-        case m_dc of
-          Nothing -> panic "Can't find the DataCon for a term"
-          Just dc -> do 
-            let extra_args = length(dataConRepArgTys dc) - length(dataConOrigArgTys dc)
+        Right dcname <- dataConInfoPtrToName (infoPtr clos)
+        (_,mb_dc)    <- tryTcErrs (tcLookupDataCon dcname)
+        case mb_dc of
+          Nothing-> do
+                     --  TODO: Check this case
+            forM [0..length (elems $ ptrs clos)] $ \i -> do
+                        tv <- newVar liftedTypeKind
+                        return$ appArr (\e->(tv,e)) (ptrs clos) i
+
+          Just dc -> do
             subTtypes <- mapMif (not . isMonomorphic)
-                                (\t -> mkTyVarTy `fmap` newVar (typeKind t))
+                                (\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 tv
-            fst `fmap` instScheme(dataConRepType dc) >>= addConstraint myType
-            return $map (\(I# i#,t) -> case ptrs clos of 
-                                       (Array _ _ ptrs#) -> case indexArray# ptrs# i# of 
-                                                              (# e #) -> (t,e))
-                        (drop extra_args $ zip [0..] subTtypes)
-      otherwise -> return []
 
+            -- 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)
+            addConstraint myType signatureType
+            return $ [ appArr (\e->(t,e)) (ptrs clos) i
+                       | (i,t) <- zip [0..] (filter (isLifted |.| isRefType) subTtypes)]
+      _ -> 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 -> 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 -> 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
+  = ( (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
+        arg_tys    = [case a of
+                        PredTy p -> predTypeRep p
+                        _        -> a
+                     | a <- dataConRepArgTys dc]
+        res_ty     = dataConOrigResTy 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]
+
+-- Soundness checks
+--------------------
+{-
+This is not formalized anywhere, so hold to your seats!
+RTTI in the presence of newtypes can be a tricky and unsound business.
+
+Example:
+~~~~~~~~~
+Suppose we are doing RTTI for a partially evaluated
+closure t, the real type of which is t :: MkT Int, for
+
+   newtype MkT a = MkT [Maybe a]
+
+The table below shows the results of RTTI and the improvement
+calculated for different combinations of evaluatedness and :type t.
+Regard the two first columns as input and the next two as output.
+
+  # |     t     |  :type t  | rtti(t)  | improv.    | result
+    ------------------------------------------------------------
+  1 |     _     |    t b    |    a     | none       | OK
+  2 |     _     |   MkT b   |    a     | none       | OK
+  3 |     _     |   t Int   |    a     | none       | OK
+
+  If t is not evaluated at *all*, we are safe.
+
+  4 |  (_ : _)  |    t b    |   [a]    | t = []     | UNSOUND
+  5 |  (_ : _)  |   MkT b   |  MkT a   | none       | OK (compensating for the missing newtype)
+  6 |  (_ : _)  |   t Int   |  [Int]   | t = []     | UNSOUND
+
+  If a is a minimal whnf, we run into trouble. Note that
+  row 5 above does newtype enrichment on the ty_rtty parameter.
+
+  7 | (Just _:_)|    t b    |[Maybe a] | t = [],    | UNSOUND
+    |                       |          | b = Maybe a|
+
+  8 | (Just _:_)|   MkT b   |  MkT a   |  none      | OK
+  9 | (Just _:_)|   t Int   |   FAIL   |  none      | OK
+
+  And if t is any more evaluated than whnf, we are still in trouble.
+  Because constraints are solved in top-down order, when we reach the
+  Maybe subterm what we got is already unsound. This explains why the
+  row 9 fails to complete.
+
+  10 | (Just _:_)|  t Int  | [Maybe a]   |  FAIL    | OK
+  11 | (Just 1:_)|  t Int  | [Maybe Int] |  FAIL    | OK
+
+  We can undo the failure in row 9 by leaving out the constraint
+  coming from the type signature of t (i.e., the 2nd column).
+  Note that this type information is still used
+  to calculate the improvement. But we fail
+  when trying to calculate the improvement, as there is no unifier for
+  t Int = [Maybe a] or t Int = [Maybe Int].
+
+
+  Another set of examples with t :: [MkT (Maybe Int)]  \equiv  [[Maybe (Maybe Int)]]
+
+  # |     t     |    :type t    |  rtti(t)    | improvement | result
+    ---------------------------------------------------------------------
+  1 |(Just _:_) | [t (Maybe a)] | [[Maybe b]] | t = []      |
+    |           |               |             | b = Maybe a |
+
+The checks:
+~~~~~~~~~~~
+Consider a function obtainType that takes a value and a type and produces
+the Term representation and a substitution (the improvement).
+Assume an auxiliar rtti' function which does the actual job if recovering
+the type, but which may produce a false type.
+
+In pseudocode:
+
+  rtti' :: a -> IO Type  -- Does not use the static type information
+
+  obtainType :: a -> Type -> IO (Maybe (Term, Improvement))
+  obtainType v old_ty = do
+       rtti_ty <- rtti' v
+       if monomorphic rtti_ty || (check rtti_ty old_ty)
+        then ...
+         else return Nothing
+  where check rtti_ty old_ty = check1 rtti_ty &&
+                              check2 rtti_ty old_ty
+
+  check1 :: Type -> Bool
+  check2 :: Type -> Type -> Bool
+
+Now, if rtti' returns a monomorphic type, we are safe.
+If that is not the case, then we consider two conditions.
+
+
+1. To prevent the class of unsoundness displayed by
+   rows 4 and 7 in the example: no higher kind tyvars
+   accepted.
+
+  check1 (t a)   = NO
+  check1 (t Int) = NO
+  check1 ([] a)  = YES
+
+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 :: NewType -> OldType -> Bool
+  check2 a  _        = True
+  check2 [a] a       = True
+  check2 [a] (t Int) = False
+  check2 [a] (t a)   = False  -- By check1 we never reach this equation
+  check2 [Int] a     = True
+  check2 [Int] (t Int) = True
+  check2 [Maybe a]   (t Int) = False
+  check2 [Maybe Int] (t Int) = True
+  check2 (Maybe [a])   (m [Int]) = False
+  check2 (Maybe [Int]) (m [Int]) = True
+
+-}
+
+check1 :: QuantifiedType -> Bool
+check1 (tvs, _) = not $ any isHigherKind (map tyVarKind tvs)
+ where
+   isHigherKind = not . null . fst . splitKindFunTys
+
+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 (map quantifyType rttis) (map quantifyType olds)
+      _ | Just _ <- splitAppTy_maybe old_ty
+        -> isMonomorphicOnNonPhantomArgs rtti_ty
+      _ -> True
+  | otherwise = True
 
 -- Dealing with newtypes
+--------------------------
 {-
-   A parallel fold over two Type values, 
+ congruenceNewtypes does a parallel fold over two Type values, 
  compensating for missing newtypes on both sides. 
  This is necessary because newtypes are not present 
- in runtime, but since sometimes there is evidence 
- available we do our best to reconstruct them. 
-   Evidence can come from DataCon signatures or 
+ in runtime, but sometimes there is evidence available.
+   Evidence can come from DataCon signatures or
  from compile-time type inference.
-   I am using the words congruence and rewriting 
- because what we are doing here is an approximation 
- of unification modulo a set of equations, which would 
- come from newtype definitions. These should be the 
- equality coercions seen in System Fc. Rewriting 
- is performed, taking those equations as rules, 
- before launching unification.
-
-   It doesn't make sense to rewrite everywhere, 
- or we would end up with all newtypes. So we rewrite 
- only in presence of evidence.
-   The lhs comes from the heap structure of ptrs,nptrs. 
-   The rhs comes from a DataCon type signature. 
- Rewriting in the rhs is restricted to the result type.
+ What we are doing here is an approximation
+ of unification modulo a set of equations derived
+ from newtype definitions. These equations should be the
+ same as the equality coercions generated for newtypes
+ in System Fc. The idea is to perform a sort of rewriting,
+ taking those equations as rules, before launching unification.
+
+ The caller must ensure the following.
+ The 1st type (lhs) comes from the heap structure of ptrs,nptrs.
+ The 2nd type (rhs) comes from a DataCon type signature.
+ Rewriting (i.e. adding/removing a newtype wrapper) can happen
+ in both types, but in the rhs it is restricted to the result type.
 
    Note that it is very tricky to make this 'rewriting'
  work with the unification implemented by TcM, where
- substitutions are 'inlined'. The order in which 
- constraints are unified is vital for this (or I am 
- using TcM wrongly).
+ substitutions are operationally inlined. The order in which
+ constraints are unified is vital as we cannot modify
+ anything that has been touched by a previous unification step.
+Therefore, congruenceNewtypes is sound only if the types
+recovered by the RTTI mechanism are unified Top-Down.
 -}
-congruenceNewtypes ::  TcType -> TcType -> TcM (TcType,TcType)
-congruenceNewtypes = go True
-  where 
-   go rewriteRHS lhs rhs  
+congruenceNewtypes ::  TcType -> TcType -> TR (TcType,TcType)
+congruenceNewtypes lhs rhs = go lhs rhs >>= \rhs' -> return (lhs,rhs')
+ where
+   go l r
  -- TyVar lhs inductive case
-    | Just tv <- getTyVar_maybe lhs 
-    = recoverM (return (lhs,rhs)) $ do  
-         Indirect ty_v <- readMetaTyVar tv
-         (lhs', rhs') <- go rewriteRHS ty_v rhs
-         writeMutVar (metaTvRef tv) (Indirect lhs')
-         return (lhs, rhs')
- -- TyVar rhs inductive case
-    | Just tv <- getTyVar_maybe rhs 
-    = recoverM (return (lhs,rhs)) $ do  
+    | Just tv <- getTyVar_maybe l
+    , isTcTyVar tv
+    , isMetaTyVar tv
+    = recoverTR (return r) $ do
          Indirect ty_v <- readMetaTyVar tv
-         (lhs', rhs') <- go rewriteRHS lhs ty_v
-         writeMutVar (metaTvRef tv) (Indirect rhs')
-         return (lhs', rhs)
+         traceTR $ fsep [text "(congruence) Following indirect tyvar:",
+                          ppr tv, equals, ppr ty_v]
+         go ty_v r
 -- FunTy inductive case
-    | Just (l1,l2) <- splitFunTy_maybe lhs
-    , Just (r1,r2) <- splitFunTy_maybe rhs
-    = do (l2',r2') <- go True l2 r2
-         (l1',r1') <- go False l1 r1
-         return (mkFunTy l1' l2', mkFunTy r1' r2')
+    | Just (l1,l2) <- splitFunTy_maybe l
+    , Just (r1,r2) <- splitFunTy_maybe r
+    = do r2' <- go l2 r2
+         r1' <- go l1 r1
+         return (mkFunTy r1' r2')
 -- TyconApp Inductive case; this is the interesting bit.
-    | Just (tycon_l, args_l) <- splitNewTyConApp_maybe lhs
-    , Just (tycon_r, args_r) <- splitNewTyConApp_maybe rhs = do
-
-      let (tycon_l',args_l') = if isNewTyCon tycon_r && not(isNewTyCon tycon_l)
-                                then (tycon_r, rewrite tycon_r lhs)
-                                else (tycon_l, args_l)
-          (tycon_r',args_r') = if rewriteRHS && isNewTyCon tycon_l && not(isNewTyCon tycon_r)
-                                then (tycon_l, rewrite tycon_l rhs)
-                                else (tycon_r, args_r)
-      (args_l'', args_r'') <- unzip `liftM` zipWithM (go rewriteRHS) args_l' args_r'
-      return (mkTyConApp tycon_l' args_l'', mkTyConApp tycon_r' args_r'') 
-
-    | otherwise = return (lhs,rhs)
-
-    where rewrite newtyped_tc lame_tipe
-           | (tvs, tipe) <- newTyConRep newtyped_tc 
-           = case tcUnifyTys (const BindMe) [tipe] [lame_tipe] of
-               Just subst -> substTys subst (map mkTyVarTy tvs)
-               otherwise  -> panic "congruenceNewtypes: Can't unify a newtype"
+    | Just (tycon_l, _) <- tcSplitTyConApp_maybe lhs
+    , Just (tycon_r, _) <- tcSplitTyConApp_maybe rhs 
+    , tycon_l /= tycon_r 
+    = upgrade tycon_l r
+
+    | otherwise = return r
+
+    where upgrade :: TyCon -> Type -> TR Type
+          upgrade new_tycon ty
+            | not (isNewTyCon new_tycon) = do
+              traceTR (text "(Upgrade) Not matching newtype evidence: " <>
+                       ppr new_tycon <> text " for " <> ppr ty)
+              return ty 
+            | otherwise = do
+               traceTR (text "(Upgrade) upgraded " <> ppr ty <>
+                        text " in presence of newtype evidence " <> ppr new_tycon)
+               vars <- mapM (newVar . tyVarKind) (tyConTyVars new_tycon)
+               let ty' = mkTyConApp new_tycon vars
+               _ <- liftTcM (unifyType ty (repType ty'))
+        -- assumes that reptype doesn't ^^^^ touch tyconApp args 
+               return ty'
 
 
-------------------------------------------------------------------------------------
-
-isMonomorphic ty | (tvs, ty') <- splitForAllTys ty
-                 = null tvs && (isEmptyVarSet . tyVarsOfType) ty'
+zonkTerm :: Term -> TcM Term
+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') }
+
+--------------------------------------------------------------------------------
+-- Restore Class predicates out of a representation type
+dictsView :: Type -> Type
+-- dictsView ty = ty
+dictsView (FunTy (TyConApp tc_dict args) ty)
+  | Just c <- tyConClass_maybe tc_dict
+  = FunTy (PredTy (ClassP c args)) (dictsView ty)
+dictsView ty
+  | Just (tc_fun, [TyConApp tc_dict args, ty2]) <- tcSplitTyConApp_maybe ty
+  , Just c <- tyConClass_maybe tc_dict
+  = mkTyConApp tc_fun [PredTy (ClassP c args), dictsView ty2]
+dictsView ty = ty
+
+
+-- Use only for RTTI types
+isMonomorphic :: RttiType -> Bool
+isMonomorphic ty = noExistentials && noUniversals
+ where (tvs, _, ty')  = tcSplitSigmaTy ty
+       noExistentials = isEmptyVarSet (tyVarsOfType ty')
+       noUniversals   = null tvs
+
+-- Use only for RTTI types
+isMonomorphicOnNonPhantomArgs :: RttiType -> Bool
+isMonomorphicOnNonPhantomArgs ty
+  | Just (tc, all_args) <- tcSplitTyConApp_maybe (repType ty)
+  , phantom_vars  <- tyConPhantomTyVars tc
+  , concrete_args <- [ arg | (tyv,arg) <- tyConTyVars tc `zip` all_args
+                           , tyv `notElem` phantom_vars]
+  = all isMonomorphicOnNonPhantomArgs concrete_args
+  | Just (ty1, ty2) <- splitFunTy_maybe ty
+  = all isMonomorphicOnNonPhantomArgs [ty1,ty2]
+  | otherwise = isMonomorphic ty
+
+tyConPhantomTyVars :: TyCon -> [TyVar]
+tyConPhantomTyVars tc
+  | isAlgTyCon tc
+  , Just dcs <- tyConDataCons_maybe tc
+  , dc_vars  <- concatMap dataConUnivTyVars dcs
+  = tyConTyVars tc \\ dc_vars
+tyConPhantomTyVars _ = []
+
+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
-mapMif_ pred f []     = []
-mapMif_ pred f (x:xx) = (if pred x then f x else return x) : mapMif_ pred f xx
+  where
+   mapMif_ _ _ []     = []
+   mapMif_ pred f (x:xx) = (if pred x then f x else return x) : mapMif_ pred f xx
 
+unlessM :: Monad m => m Bool -> m () -> m ()
 unlessM condM acc = condM >>= \c -> unless c acc
 
+
 -- Strict application of f at index i
-appArr f (Array _ _ ptrs#) (I# i#) = case indexArray# ptrs# i# of 
-                                       (# e #) -> f e
+appArr :: Ix i => (e -> a) -> Array i e -> Int -> a
+appArr f a@(Array _ _ _ ptrs#) i@(I# i#)
+ = ASSERT2 (i < length(elems a), ppr(length$ elems a, i))
+   case indexArray# ptrs# i# of
+       (# e #) -> f e
 
-zonkTerm :: Term -> TcM Term
-zonkTerm = foldTerm idTermFoldM {
-              fTerm = \ty dc v tt -> sequence tt      >>= \tt ->
-                                     zonkTcType ty    >>= \ty' ->
-                                     return (Term ty' dc v tt)
-             ,fSuspension = \ct ty v b -> fmapMMaybe zonkTcType ty >>= \ty ->
-                                          return (Suspension ct ty v b)}  
+amap' :: (t -> b) -> Array Int t -> [b]
+amap' f (Array i0 i _ arr#) = map g [0 .. i - i0]
+    where g (I# i#) = case indexArray# arr# i# of
+                          (# e #) -> f e
 
 
--- Is this defined elsewhere?
--- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
-sigmaType ty = mkForAllTys (varSetElems$ tyVarsOfType (dropForAlls ty)) ty
+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)
+         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