wibble
[ghc-hetmet.git] / compiler / ghci / RtClosureInspect.hs
index 09afa00..dae9260 100644 (file)
@@ -6,13 +6,6 @@
 --
 -----------------------------------------------------------------------------
 
-{-# OPTIONS -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
---     http://hackage.haskell.org/trac/ghc/wiki/CodingStyle#Warnings
--- for details
-
 module RtClosureInspect(
   
      cvObtainTerm,      -- :: HscEnv -> Int -> Bool -> Maybe Type -> HValue -> IO Term
@@ -24,6 +17,7 @@ module RtClosureInspect(
      pprTerm, 
      cPprTerm, 
      cPprTermBase,
+     CustomTermPrinter,
      termType,
      foldTerm, 
      TermFold(..), 
@@ -52,23 +46,24 @@ import qualified ByteCodeItbls as BCI( StgInfoTable(..) )
 import HscTypes         ( HscEnv )
 import Linker
 
-import DataCon          
-import Type             
-import TcRnMonad        ( TcM, initTc, ioToTcRn, 
-                          tryTcErrs)
+import DataCon
+import Type
+import Var
+import TcRnMonad        ( TcM, initTc, ioToTcRn,
+                          tryTcErrs, traceTc)
 import TcType
 import TcMType
 import TcUnify
 import TcGadt
 import TcEnv
 import DriverPhases
-import TyCon           
-import Name 
+import TyCon
+import Name
 import VarEnv
 import Util
 import VarSet
 
-import TysPrim         
+import TysPrim
 import PrelNames
 import TysWiredIn
 
@@ -83,6 +78,7 @@ import GHC.Exts
 import Control.Monad
 import Data.Maybe
 import Data.Array.Base
+import Data.Ix
 import Data.List        ( partition )
 import qualified Data.Sequence as Seq
 import Data.Monoid
@@ -107,8 +103,6 @@ import System.IO.Unsafe
 
 data Term = Term { ty        :: Type 
                  , dc        :: Either String DataCon
-                               -- The heap datacon. If ty is a newtype,
-                               -- this is NOT the newtype datacon.
                                -- Empty if the datacon aint exported by the .hi
                                -- (private constructors in -O0 libraries)
                  , val       :: HValue 
@@ -122,14 +116,19 @@ data Term = Term { ty        :: Type
                        , val      :: HValue
                        , bound_to :: Maybe Name   -- Useful for printing
                        }
+          | NewtypeWrap{ ty           :: Type
+                       , dc           :: Either String DataCon
+                       , wrapped_term :: Term }
 
-isTerm, isSuspension, isPrim :: Term -> Bool
+isTerm, isSuspension, isPrim, isNewtypeWrap :: Term -> Bool
 isTerm Term{} = True
 isTerm   _    = False
 isSuspension Suspension{} = True
 isSuspension      _       = False
 isPrim Prim{} = True
 isPrim   _    = False
+isNewtypeWrap NewtypeWrap{} = True
+isNewtypeWrap _             = False
 
 termType :: Term -> Maybe Type
 termType t@(Suspension {}) = mb_ty t
@@ -137,8 +136,9 @@ termType t = Just$ 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 _                  = False
 
 instance Outputable (Term) where
  ppr = head . cPprTerm cPprTermBase
@@ -169,6 +169,7 @@ instance Outputable ClosureType where
 
 #include "../includes/ClosureTypes.h"
 
+aP_CODE, pAP_CODE :: Int
 aP_CODE = AP
 pAP_CODE = PAP
 #undef AP
@@ -178,13 +179,21 @@ getClosureData :: a -> IO Closure
 getClosureData a =
    case unpackClosure# a of 
      (# iptr, ptrs, nptrs #) -> do
+#ifndef GHCI_TABLES_NEXT_TO_CODE
+           -- 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 !tablesNextToCode, so we must adjust here:
+           itbl <- peek (Ptr iptr `plusPtr` negate wORD_SIZE)
+#else
            itbl <- peek (Ptr iptr)
+#endif
            let tipe = readCType (BCI.tipe itbl)
                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)] ]
-           ASSERT(fromIntegral elems >= 0) return ()
+           ASSERT(elems >= 0) return ()
            ptrsList `seq` 
             return (Closure tipe (Ptr iptr) itbl ptrsList nptrs_data)
 
@@ -220,9 +229,10 @@ 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' :: (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
@@ -255,41 +265,49 @@ extractUnboxed tt clos = go tt (nonPtrs clos)
            | (x, rest) <- splitAt ((sizeofType t + wORD_SIZE - 1) `div` wORD_SIZE) xx 
            = x : go tt rest
 
+sizeofTyCon :: TyCon -> Int
 sizeofTyCon = sizeofPrimRep . tyConPrimRep
 
 -----------------------------------
 -- * Traversals for Terms
 -----------------------------------
+type TermProcessor a b = Type -> Either String DataCon -> HValue -> [a] -> b
 
-data TermFold a = TermFold { fTerm :: Type -> Either String DataCon -> HValue -> [a] -> a
+data TermFold a = TermFold { fTerm :: TermProcessor a a
                            , fPrim :: Type -> [Word] -> a
                            , fSuspension :: ClosureType -> Maybe Type -> HValue
                                            -> Maybe Name -> a
+                           , fNewtypeWrap :: Type -> Either String DataCon
+                                            -> a -> 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)
 
 idTermFold :: TermFold Term
 idTermFold = TermFold {
               fTerm = Term,
               fPrim = Prim,
-              fSuspension = Suspension
+              fSuspension  = Suspension,
+              fNewtypeWrap = NewtypeWrap
                       }
 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
+              fSuspension = (((return.).).). Suspension,
+              fNewtypeWrap= \ty dc t -> NewtypeWrap ty dc `liftM` t
                        }
 
 mapTermType :: (Type -> 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 }
+                          Suspension ct (fmap f mb_ty) hval n,
+          fNewtypeWrap= \ty dc t -> NewtypeWrap (f ty) dc t}
 
 termTyVars :: Term -> TyVarSet
 termTyVars = foldTerm TermFold {
@@ -297,102 +315,148 @@ termTyVars = foldTerm TermFold {
                           tyVarsOfType ty `plusVarEnv` concatVarEnv tt,
             fSuspension = \_ mb_ty _ _ -> 
                           maybe emptyVarEnv tyVarsOfType mb_ty,
-            fPrim       = \ _ _ -> emptyVarEnv }
+            fPrim       = \ _ _ -> emptyVarEnv,
+            fNewtypeWrap= \ty _ t -> tyVarsOfType ty `plusVarEnv` t}
     where concatVarEnv = foldr plusVarEnv emptyVarEnv
+
 ----------------------------------
 -- Pretty printing of terms
 ----------------------------------
 
+type Precedence        = Int
+type TermPrinter       = Precedence -> Term ->   SDoc
+type TermPrinterM m    = Precedence -> Term -> m SDoc
+
 app_prec,cons_prec ::Int
 app_prec = 10
 cons_prec = 5 -- TODO Extract this info from GHC itself
 
-pprTerm y p t | Just doc <- pprTermM y p t = doc
+pprTerm :: TermPrinter -> TermPrinter
+pprTerm y p t | Just doc <- pprTermM (\p -> Just . y p) p t = doc
+pprTerm _ _ _ = panic "pprTerm"
 
-pprTermM :: Monad m => (Int -> Term -> m SDoc) -> Int -> Term -> m SDoc
-pprTermM y p t@Term{dc=Left dc_tag, subTerms=tt, ty=ty} = do
+pprTermM, ppr_termM, pprNewtypeWrap :: Monad m => TermPrinterM m -> TermPrinterM m
+pprTermM y p t = pprDeeper `liftM` ppr_termM y p t
+
+pprTermM1, ppr_termM1 :: Monad m => Term -> m SDoc
+pprTermM1 t    = pprDeeper `liftM` ppr_termM1 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 <+> sep tt_docs)
+  return$ cparen (not(null tt) && p >= app_prec) (text dc_tag <+> pprDeeperList fsep tt_docs)
   
-pprTermM y p t@Term{dc=Right dc, subTerms=tt, ty=ty} 
+ppr_termM y p Term{dc=Right dc, subTerms=tt} 
 {-  | dataConIsInfix dc, (t1:t2:tt') <- tt  --TODO fixity
-  = parens (pprTerm1 True t1 <+> ppr dc <+> pprTerm1 True ppr t2) 
-    <+> hsep (map (pprTerm1 True) 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
-  | Just (tc,_) <- splitNewTyConApp_maybe ty
-  , isNewTyCon tc
-  , Just new_dc <- maybeTyConSingleCon tc = do 
-         real_value <- y 10 t{ty=repType ty}
-         return$ cparen (p >= app_prec) (ppr new_dc <+> real_value)
   | otherwise = do
          tt_docs <- mapM (y app_prec) tt
-         return$ cparen (p >= app_prec) (ppr dc <+> sep tt_docs)
+         return$ cparen (p >= app_prec) (ppr dc <+> pprDeeperList fsep tt_docs)
+
+ppr_termM y p t@NewtypeWrap{} = pprNewtypeWrap y p t
+
+ppr_termM _ _ t = ppr_termM1 t
 
-pprTermM y _ t = pprTermM1 y t
-pprTermM1 _ Prim{value=words, ty=ty} = 
+
+ppr_termM1 Prim{value=words, ty=ty} = 
     return$ text$ repPrim (tyConAppTyCon ty) words
-pprTermM1 y t@Term{} = panic "pprTermM1 - unreachable"
-pprTermM1 _ Suspension{bound_to=Nothing} = return$ char '_'
-pprTermM1 _ Suspension{mb_ty=Just ty, bound_to=Just n}
+ppr_termM1 Term{} = panic "ppr_termM1 - unreachable"
+ppr_termM1 Suspension{bound_to=Nothing} = return$ char '_'
+ppr_termM1 Suspension{mb_ty=Just ty, bound_to=Just n}
   | Just _ <- splitFunTy_maybe ty = return$ ptext SLIT("<function>")
   | otherwise = return$ parens$ ppr n <> text "::" <> ppr ty 
+ppr_termM1 _ = panic "ppr_termM1"
 
--- Takes a list of custom printers with a explicit recursion knot and a term, 
+pprNewtypeWrap y p NewtypeWrap{ty=ty, wrapped_term=t} 
+  | Just (tc,_) <- splitNewTyConApp_maybe ty
+  , ASSERT(isNewTyCon tc) True
+  , Just new_dc <- maybeTyConSingleCon tc = do 
+         real_term <- y 10 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 :: 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{} = do
-    let default_ prec t = Just `liftM` pprTermM go prec t
-        mb_customDocs = [pp prec t | pp <- custom go ++ [default_]]
+cPprTerm :: Monad m => CustomTermPrinter m -> Term -> m SDoc
+cPprTerm printers_ = go 0 where
+  printers = printers_ go
+  go prec t | isTerm t || isNewtypeWrap 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
-  go _ t = pprTermM1 go t
+  go _ t = pprTermM1 t
+
   firstJustM (mb:mbs) = mb >>= maybe (firstJustM mbs) (return . Just)
   firstJustM [] = return Nothing
 
 -- Default set of custom printers. Note that the recursion knot is explicit
-cPprTermBase :: Monad m => (Int->Term-> m SDoc)->[Int->Term->m (Maybe SDoc)]
+cPprTermBase :: Monad m => CustomTermPrinter m
 cPprTermBase y =
-  [ 
-    ifTerm isTupleTy             (\_ -> liftM (parens . hcat . punctuate comma) 
-                                 . mapM (y (-1)) . subTerms)
-  , ifTerm (\t -> isTyCon listTyCon t && subTerms t `lengthIs` 2)
-                                 (\ p Term{subTerms=[h,t]} -> doList p h t)
-  , ifTerm (isTyCon intTyCon)    (coerceShow$ \(a::Int)->a)
-  , ifTerm (isTyCon charTyCon)   (coerceShow$ \(a::Char)->a)
---  , ifTerm (isTyCon wordTyCon) (coerceShow$ \(a::Word)->a)
-  , ifTerm (isTyCon floatTyCon)  (coerceShow$ \(a::Float)->a)
-  , ifTerm (isTyCon doubleTyCon) (coerceShow$ \(a::Double)->a)
-  , ifTerm isIntegerTy           (coerceShow$ \(a::Integer)->a)
-  ] 
-     where ifTerm pred f p t@Term{} | pred t = liftM Just (f p t) 
-           ifTerm _    _ _ _                 = return Nothing
-           isIntegerTy Term{ty=ty} = fromMaybe False $ do
+  [ 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)
+  ]
+     where ifTerm pred f prec t@Term{}
+               | pred t    = Just `liftM` f prec t
+           ifTerm _ _ _ _  = return Nothing
+
+           isIntegerTy ty  = fromMaybe False $ do
              (tc,_) <- splitTyConApp_maybe ty 
              return (tyConName tc == integerTyConName)
-           isTupleTy Term{ty=ty} = fromMaybe False $ do 
+
+           isTupleTy ty    = fromMaybe False $ do 
              (tc,_) <- splitTyConApp_maybe ty 
              return (tc `elem` (fst.unzip.elems) boxedTupleArr)
-           isTyCon a_tc Term{ty=ty} = fromMaybe False $ do 
+
+           isTyCon a_tc ty = fromMaybe False $ do 
              (tc,_) <- splitTyConApp_maybe ty
              return (a_tc == tc)
-           coerceShow f _ = return . text . show . f . unsafeCoerce# . val
-           --TODO pprinting of list terms is not lazy
+
+           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
+               let elems      = h : getListTerms t
                    isConsLast = termType(last elems) /= termType h
                print_elems <- mapM (y cons_prec) elems
                return$ if isConsLast
-                     then cparen (p >= cons_prec) . hsep . punctuate (space<>colon) 
-                           $ print_elems
-                     else brackets (hcat$ punctuate comma print_elems)
+                     then cparen (p >= cons_prec) 
+                        . pprDeeperList fsep 
+                        . punctuate (space<>colon)
+                        $ print_elems
+                     else brackets (pprDeeperList fcat$
+                                         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=[]}  = []
+                      getListTerms Term{subTerms=[]}    = []
                       getListTerms t@Suspension{}       = [t]
                       getListTerms t = pprPanic "getListTerms" (ppr t)
 
@@ -462,6 +526,9 @@ runTR hsc_env c = do
 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 . traceTc
+
 trIO :: IO a -> TR a 
 trIO = liftTcM . ioToTcRn
 
@@ -474,8 +541,8 @@ newVar = liftTcM . fmap mkTyVarTy . newFlexiTyVar
 -- | 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
+instScheme ty | (tvs, _rho) <- tcSplitForAllTys ty = liftTcM$ do
+   (tvs',_theta,ty') <- tcInstType (mapM tcInstTyVar) ty
    return (ty', zipTopTvSubst tvs' (mkTyVarTys tvs))
 
 -- Adds a constraint of the form t1 == t2
@@ -493,17 +560,21 @@ cvObtainTerm :: HscEnv -> Int -> Bool -> Maybe Type -> HValue -> IO Term
 cvObtainTerm hsc_env bound force mb_ty hval = runTR hsc_env $ do
    tv <- newVar argTypeKind
    case mb_ty of
-     Nothing -> go bound tv tv hval >>= zonkTerm
-     Just ty | isMonomorphic ty -> go bound ty ty hval >>= zonkTerm
+     Nothing ->      go bound tv tv hval 
+                >>= zonkTerm 
+                >>= return . expandNewtypes
+     Just ty | isMonomorphic ty ->     go bound ty ty hval 
+                                   >>= zonkTerm
+                                   >>= return . expandNewtypes
      Just ty -> do 
               (ty',rev_subst) <- instScheme (sigmaType ty)
               addConstraint tv ty'
               term <- go bound tv tv hval >>= zonkTerm
               --restore original Tyvars
-              return$ mapTermType (substTy rev_subst) term
+              return$ expandNewtypes $ mapTermType (substTy rev_subst) term
     where 
   go bound _ _ _ | seq bound False = undefined
-  go 0 tv ty a = do
+  go 0 tv _ty a = do
     clos <- trIO $ getClosureData a
     return (Suspension (tipe clos) (Just tv) a Nothing)
   go bound tv ty a = do 
@@ -518,7 +589,7 @@ cvObtainTerm hsc_env bound force mb_ty hval = runTR hsc_env $ do
 -- and showing the '_' is more useful.
       t | isThunk t && force -> seq a $ go (pred bound) tv ty a
 -- We always follow indirections 
-      Indirection _ -> go (pred bound) tv ty $! (ptrs clos ! 0)
+      Indirection _ -> go bound tv ty $! (ptrs clos ! 0)
  -- The interesting case
       Constr -> do
         Right dcname <- dataConInfoPtrToName (infoPtr clos)
@@ -566,7 +637,6 @@ cvObtainTerm hsc_env bound force mb_ty hval = runTR hsc_env $ do
       tipe_clos -> 
          return (Suspension tipe_clos (Just tv) a Nothing)
 
---  matchSubTypes dc ty | pprTrace "matchSubtypes" (ppr dc <+> ppr ty) False = undefined
   matchSubTypes dc ty
     | Just (_,ty_args) <- splitTyConApp_maybe (repType ty) 
 --     assumption:             ^^^ looks through newtypes 
@@ -581,18 +651,29 @@ cvObtainTerm hsc_env bound force mb_ty hval = runTR hsc_env $ do
    | isPointed ty = ASSERT2(not(null pointed)
                             , ptext SLIT("reOrderTerms") $$ 
                                         (ppr pointed $$ ppr unpointed))
-                    head pointed : reOrderTerms (tail pointed) unpointed tys
+                    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
+                    let (t:tt) = unpointed in t : reOrderTerms pointed tt tys
+  
+  expandNewtypes t@Term{ ty=ty, subTerms=tt }
+   | Just (tc, args) <- splitNewTyConApp_maybe ty
+   , isNewTyCon tc
+   , wrapped_type    <- newTyConInstRhs tc args
+   , Just dc         <- maybeTyConSingleCon tc
+   , t'              <- expandNewtypes t{ ty = wrapped_type
+                                        , subTerms = map expandNewtypes tt }
+   = NewtypeWrap ty (Right dc) t'
 
+   | otherwise = t{ subTerms = map expandNewtypes tt }
+
+  expandNewtypes t = t
 
 
 -- Fast, breadth-first Type reconstruction
-max_depth = 10 :: Int
-cvReconstructType :: HscEnv -> Bool -> Maybe Type -> HValue -> IO (Maybe Type)
-cvReconstructType hsc_env force mb_ty hval = runTR_maybe hsc_env $ do
+cvReconstructType :: HscEnv -> Int -> Maybe Type -> HValue -> IO (Maybe Type)
+cvReconstructType hsc_env max_depth mb_ty hval = runTR_maybe hsc_env $ do
    tv <- newVar argTypeKind
    case mb_ty of
      Nothing -> do search (isMonomorphic `fmap` zonkTcType tv)
@@ -611,12 +692,14 @@ cvReconstructType hsc_env force mb_ty hval = runTR_maybe hsc_env $ do
               substTy rev_subst `fmap` zonkTcType tv
     where 
 --  search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m ()
-  search stop expand l depth | Seq.null l = return ()
-  search stop expand x 0 = fail$ "Failed to reconstruct a type after " ++
-                                show max_depth ++ " steps"
-  search stop expand l d | x :< xx <- viewl l = unlessM stop $ do
-    new <- expand x
-    search stop expand (xx `mappend` Seq.fromList new) $! (pred d)
+  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)]
@@ -630,10 +713,6 @@ cvReconstructType hsc_env force mb_ty hval = runTR_maybe hsc_env $ do
         case mb_dc of
           Nothing-> do
                      --  TODO: Check this case
-            vars     <- replicateM (length$ elems$ ptrs clos)
-                                   (newVar (liftedTypeKind))
-            subTerms <- sequence [ appArr (go tv) (ptrs clos) i
-                                   | (i, tv) <- zip [0..] vars]    
             forM [0..length (elems $ ptrs clos)] $ \i -> do
                         tv <- newVar liftedTypeKind
                         return$ appArr (\e->(tv,e)) (ptrs clos) i
@@ -653,21 +732,26 @@ cvReconstructType hsc_env force mb_ty hval = runTR_maybe hsc_env $ do
             return $ [ appArr (\e->(t,e)) (ptrs clos) i
                        | (i,t) <- drop extra_args $ 
                                      zip [0..] (filter isPointed subTtypes)]
-      otherwise -> return []
+      _ -> return []
 
      -- This helper computes the difference between a base type t and the 
      -- improved rtti_t computed by RTTI
      -- The main difference between RTTI types and their normal counterparts
      --  is that the former are _not_ polymorphic, thus polymorphism must
-     --  be stripped. Syntactically, forall's must be stripped
+     --  be stripped. Syntactically, forall's must be stripped.
+     -- We also remove predicates.
+computeRTTIsubst :: Type -> Type -> TvSubst
 computeRTTIsubst ty rtti_ty = 
+    case mb_subst of
+      Just subst -> subst
+      Nothing    -> pprPanic "Failed to compute a RTTI substitution" 
+                             (ppr (ty, rtti_ty))
      -- In addition, we strip newtypes too, since the reconstructed type might
      --   not have recovered them all
-           tcUnifyTys (const BindMe) 
-                      [repType' $ dropForAlls$ ty]
-                      [repType' $ rtti_ty]  
--- TODO stripping newtypes shouldn't be necessary, test
-
+     -- TODO stripping newtypes shouldn't be necessary, test
+   where mb_subst = tcUnifyTys (const BindMe) 
+                               [rttiView ty]
+                               [rttiView rtti_ty]  
 
 -- Dealing with newtypes
 {-
@@ -696,16 +780,18 @@ computeRTTIsubst ty rtti_ty =
    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).
+ constraints are unified is vital for this.
+   This is a simple form of residuation, the technique of 
+ delaying unification steps until enough information
+ is available.
 -}
-congruenceNewtypes ::  TcType -> TcType -> TcM (TcType,TcType)
+congruenceNewtypes ::  TcType -> TcType -> TR (TcType,TcType)
 congruenceNewtypes lhs rhs 
  -- TyVar lhs inductive case
     | Just tv <- getTyVar_maybe lhs 
     = recoverTc (return (lhs,rhs)) $ do  
          Indirect ty_v <- readMetaTyVar tv
-         (lhs1, rhs1) <- congruenceNewtypes ty_v rhs
+         (_lhs1, rhs1) <- congruenceNewtypes ty_v rhs
          return (lhs, rhs1)
 -- FunTy inductive case
     | Just (l1,l2) <- splitFunTy_maybe lhs
@@ -714,43 +800,51 @@ congruenceNewtypes lhs rhs
          (l1',r1') <- congruenceNewtypes l1 r1
          return (mkFunTy l1' l2', 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 
+    | Just (tycon_l, _) <- splitNewTyConApp_maybe lhs
+    , Just (tycon_r, _) <- splitNewTyConApp_maybe rhs 
     , tycon_l /= tycon_r 
-    = return (lhs, upgrade tycon_l rhs)
+    = do rhs' <- upgrade tycon_l rhs
+         return (lhs, rhs')
 
     | otherwise = return (lhs,rhs)
 
-    where upgrade :: TyCon -> Type -> Type
+    where upgrade :: TyCon -> Type -> TR Type
           upgrade new_tycon ty
-            | not (isNewTyCon new_tycon) = ty 
-            | ty' <- mkTyConApp new_tycon (map mkTyVarTy $ tyConTyVars new_tycon)
-            , Just subst <- tcUnifyTys (const BindMe) [ty] [repType ty']
-            = substTy subst ty'
-        -- assumes that reptype doesn't touch tyconApp args ^^^
+            | not (isNewTyCon new_tycon) = return ty 
+            | otherwise = do 
+               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'
 
 
 --------------------------------------------------------------------------------
 -- Semantically different to recoverM in TcRnMonad 
 -- recoverM retains the errors in the first action,
 --  whereas recoverTc here does not
+recoverTc :: TcM a -> TcM a -> TcM a
 recoverTc recover thing = do 
   (_,mb_res) <- tryTcErrs thing
   case mb_res of 
     Nothing  -> recover
     Just res -> return res
 
+isMonomorphic :: Type -> Bool
 isMonomorphic ty | (tvs, ty') <- splitForAllTys ty
                  = null tvs && (isEmptyVarSet . tyVarsOfType) 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 :: Ix i => (e -> a) -> Array i e -> Int -> a
 appArr f a@(Array _ _ _ ptrs#) i@(I# i#)
  = ASSERT (i < length(elems a))
    case indexArray# ptrs# i# of
@@ -762,11 +856,14 @@ zonkTerm = foldTerm idTermFoldM {
                                      zonkTcType ty    >>= \ty' ->
                                      return (Term ty' dc v tt)
              ,fSuspension = \ct ty v b -> fmapMMaybe zonkTcType ty >>= \ty ->
-                                          return (Suspension ct ty v b)}  
+                                          return (Suspension ct ty v b)
+             ,fNewtypeWrap= \ty dc t -> 
+                   return NewtypeWrap `ap` zonkTcType ty `ap` return dc `ap` t}
 
 
 -- Is this defined elsewhere?
 -- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
+sigmaType :: Type -> Type
 sigmaType ty = mkForAllTys (varSetElems$ tyVarsOfType (dropForAlls ty)) ty