Rename maybeTyConSingleCon to tyConSingleDataCon_maybe
[ghc-hetmet.git] / compiler / ghci / RtClosureInspect.hs
index f653de6..509eb99 100644 (file)
@@ -8,28 +8,17 @@
 
 module RtClosureInspect(
   
-     cvObtainTerm,       -- :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Term
-
-     AddressEnv(..), 
-     DataConEnv,
-     extendAddressEnvList, 
-     elemAddressEnv, 
-     delFromAddressEnv, 
-     emptyAddressEnv, 
-     lookupAddressEnv, 
-
-     ClosureType(..), 
-     getClosureData,     -- :: a -> IO Closure
-     Closure ( tipe, infoTable, ptrs, nonPtrs ), 
-     getClosureType,     -- :: a -> IO ClosureType
-     isConstr,           -- :: ClosureType -> Bool
-     isIndirection,      -- :: ClosureType -> Bool
-     getInfoTablePtr,    -- :: a -> Ptr StgInfoTable
-
-     Term(..), 
-     printTerm, 
-     customPrintTerm, 
-     customPrintTermBase,
+     cvObtainTerm,      -- :: HscEnv -> Int -> Bool -> Maybe Type -> HValue -> IO Term
+
+     Term(..),
+     isTerm,
+     isSuspension,
+     isPrim,
+     isNewtypeWrap,
+     pprTerm, 
+     cPprTerm, 
+     cPprTermBase,
+     CustomTermPrinter,
      termType,
      foldTerm, 
      TermFold(..), 
@@ -38,101 +27,119 @@ module RtClosureInspect(
      isFullyEvaluated, 
      isPointed,
      isFullyEvaluatedTerm,
+     mapTermType,
+     termTyVars,
 --     unsafeDeepSeq, 
-     
-     sigmaType
+     cvReconstructType,
+     improveRTTIType,
+     sigmaType,
+     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 Linker
 
-import DataCon          
-import Type             
-import TcRnMonad        ( TcM, initTcPrintErrors, ioToTcRn, recoverM, writeMutVar )
+import DataCon
+import Type
+import Var
+import TcRnMonad
 import TcType
 import TcMType
 import TcUnify
-import TcGadt
-import TyCon           
-import Var
-import Name 
+import TcEnv
+import DriverPhases
+import TyCon
+import Name
 import VarEnv
-import OccName
+import Util
 import VarSet
-import {-#SOURCE#-} TcRnDriver ( tcRnRecoverDataCon )
 
-import TysPrim         
+import TysPrim
 import PrelNames
 import TysWiredIn
 
-import Constants        ( wORD_SIZE )
 import Outputable
-import Maybes
+import FastString
 import Panic
-import FiniteMap
+
+import Constants        ( wORD_SIZE )
 
 import GHC.Arr          ( Array(..) )
-import GHC.Ptr          ( Ptr(..), castPtr )
-import GHC.Exts         
-import GHC.Int          ( Int32(..),  Int64(..) )
-import GHC.Word         ( Word32(..), Word64(..) )
+import GHC.Exts
+import GHC.IOBase ( IO(IO) )
 
 import Control.Monad
 import Data.Maybe
 import Data.Array.Base
+import Data.Ix
 import Data.List        ( partition )
-import Foreign.Storable
+import qualified Data.Sequence as Seq
+import Data.Monoid
+import Data.Sequence hiding (null, length, index, take, drop, splitAt, reverse)
+import Foreign
+import System.IO.Unsafe
 
+import System.IO
 ---------------------------------------------
 -- * 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", Thunk, Thunk]
-          , Thunk
-          , Term (Char, e, f) (,,) ('b',_,_) [Term Char C# "b", Thunk, Thunk]]
 -}
 
 data Term = Term { ty        :: Type 
-                 , dc        :: DataCon 
+                 , 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
-                 , value     :: String }
+                 , value     :: [Word] }
 
           | Suspension { ctype    :: ClosureType
-                       , mb_ty    :: Maybe Type
+                       , ty       :: Type
                        , val      :: HValue
                        , bound_to :: Maybe Name   -- Useful for printing
                        }
+          | NewtypeWrap{ ty           :: Type
+                       , dc           :: Either String DataCon
+                       , wrapped_term :: Term }
+          | RefWrap    { ty           :: Type
+                       , wrapped_term :: Term }
 
+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 t@(Suspension {}) = mb_ty t
-termType t = Just$ ty t
+termType :: Term -> Type
+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 . customPrintTerm customPrintTermBase
+ ppr t | Just doc <- cPprTerm cPprTermBase t = doc
+       | otherwise = panic "Outputable Term instance"
 
 -------------------------------------------------------------------------
 -- Runtime Closure Datatype and functions for retrieving closure related stuff
@@ -145,83 +152,99 @@ data ClosureType = Constr
                  | AP 
                  | PAP 
                  | Indirection Int 
-                 | Other Int
+                 | MutVar Int
+                 | Other  Int
  deriving (Show, Eq)
 
 data Closure = Closure { tipe         :: ClosureType 
+                       , infoPtr      :: Ptr ()
                        , infoTable    :: StgInfoTable
                        , ptrs         :: Array Int HValue
-                        -- What would be the type here? HValue is ok? Should I build a Ptr?
-                       , nonPtrs      :: ByteArray# 
+                       , nonPtrs      :: [Word]
                        }
 
 instance Outputable ClosureType where
   ppr = text . show 
 
-getInfoTablePtr :: a -> Ptr StgInfoTable
-getInfoTablePtr x = 
-    case infoPtr# x of
-      itbl_ptr -> castPtr ( Ptr itbl_ptr )
-
-getClosureType :: a -> IO ClosureType
-getClosureType = liftM (readCType . BCI.tipe ) . peek . getInfoTablePtr
-
 #include "../includes/ClosureTypes.h"
 
+aP_CODE, pAP_CODE :: Int
 aP_CODE = AP
 pAP_CODE = PAP
 #undef AP
 #undef PAP
 
 getClosureData :: a -> IO Closure
-getClosureData a = do
-   itbl <- peek (getInfoTablePtr a)
-   let tipe = readCType (BCI.tipe itbl)
-   case closurePayload# a of 
-     (# ptrs, nptrs #) -> 
-           let elems = BCI.ptrs itbl 
-               ptrsList = Array 0 (fromIntegral$ elems) ptrs
-           in ptrsList `seq` return (Closure tipe itbl ptrsList nptrs)
+getClosureData a =
+   case unpackClosure# a of 
+     (# iptr, ptrs, nptrs #) -> do
+           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 = 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(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
- | fromIntegral i == pAP_CODE              = PAP
- | otherwise                               = Other (fromIntegral i)
-
-isConstr, isIndirection :: ClosureType -> Bool
+ | i >= IND    && i <= IND_STATIC          = Indirection i'
+ | i' == aP_CODE                           = AP
+ | i == AP_STACK                           = AP
+ | i' == pAP_CODE                          = PAP
+ | i == MUT_VAR_CLEAN || i == MUT_VAR_DIRTY     = MutVar 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
+isThunk ThunkSelector = True
+isThunk AP            = True
+isThunk _             = False
+
 isFullyEvaluated :: a -> IO Bool
 isFullyEvaluated a = do 
   closure <- getClosureData a 
   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]
+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
 
 -- 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
@@ -229,429 +252,645 @@ unsafeDeepSeq = unsafeDeepSeq1 2
         where tipe = unsafePerformIO (getClosureType a)
 -}
 isPointed :: Type -> Bool
-isPointed t | Just (t, _) <- splitTyConApp_maybe t = not$ isUnliftedTypeKind (tyConKind t)
+isPointed t | Just (t, _) <- splitTyConApp_maybe t 
+            = not$ isUnliftedTypeKind (tyConKind t)
 isPointed _ = True
 
-#define MKDECODER(offset,cons,builder) (offset, show$ cons (builder addr 0#))
-
-extractUnboxed  :: [Type] -> ByteArray# -> [String]
-extractUnboxed tt ba = helper tt (byteArrayContents# ba)
-   where helper :: [Type] -> Addr# -> [String]
-         helper (t:tt) addr 
-          | Just ( tycon,_) <- splitTyConApp_maybe t 
-          =  let (offset, txt) = decode tycon addr
-                 (I# word_offset)   = offset*wORD_SIZE
-             in txt : helper tt (plusAddr# addr word_offset)
-          | otherwise 
-          = -- ["extractUnboxed.helper: Urk. I got a " ++ showSDoc (ppr t)]
-            panic$ "extractUnboxed.helper: Urk. I got a " ++ showSDoc (ppr t)
-         helper [] addr = []
-         decode :: TyCon -> Addr# -> (Int, String)
-         decode t addr                             
-           | t == charPrimTyCon   = MKDECODER(1,C#,indexCharOffAddr#)
-           | t == intPrimTyCon    = MKDECODER(1,I#,indexIntOffAddr#)
-           | t == wordPrimTyCon   = MKDECODER(1,W#,indexWordOffAddr#)
-           | t == floatPrimTyCon  = MKDECODER(1,F#,indexFloatOffAddr#)
-           | t == doublePrimTyCon = MKDECODER(2,D#,indexDoubleOffAddr#)
-           | t == int32PrimTyCon  = MKDECODER(1,I32#,indexInt32OffAddr#)
-           | t == word32PrimTyCon = MKDECODER(1,W32#,indexWord32OffAddr#)
-           | t == int64PrimTyCon  = MKDECODER(2,I64#,indexInt64OffAddr#)
-           | t == word64PrimTyCon = MKDECODER(2,W64#,indexWord64OffAddr#)
-           | t == addrPrimTyCon   = MKDECODER(1,I#,(\x off-> addr2Int# (indexAddrOffAddr# x off)))  --OPT Improve the presentation of addresses
-           | t == stablePtrPrimTyCon  = (1, "<stablePtr>")
-           | t == stableNamePrimTyCon = (1, "<stableName>")
-           | t == statePrimTyCon      = (1, "<statethread>")
-           | t == realWorldTyCon      = (1, "<realworld>")
-           | t == threadIdPrimTyCon   = (1, "<ThreadId>")
-           | t == weakPrimTyCon       = (1, "<Weak>")
-           | t == arrayPrimTyCon      = (1,"<array>")
-           | t == byteArrayPrimTyCon  = (1,"<bytearray>")
-           | t == mutableArrayPrimTyCon = (1, "<mutableArray>")
-           | t == mutableByteArrayPrimTyCon = (1, "<mutableByteArray>")
-           | t == mutVarPrimTyCon= (1, "<mutVar>")
-           | t == mVarPrimTyCon  = (1, "<mVar>")
-           | t == tVarPrimTyCon  = (1, "<tVar>")
-           | otherwise = (1, showSDoc (char '<' <> ppr t <> char '>')) 
-                 -- We cannot know the right offset in the otherwise case, so 1 is just a wild dangerous guess!
-           -- TODO: Improve the offset handling in decode (make it machine dependant)
+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) xx
+           = x : go tt rest
+
+sizeofTyCon :: TyCon -> Int -- in *words*
+sizeofTyCon = primRepSizeW . tyConPrimRep
 
 -----------------------------------
 -- * Traversals for Terms
 -----------------------------------
-
-data TermFold a = TermFold { fTerm :: Type -> DataCon -> HValue -> [a] -> a
-                           , fPrim :: Type -> String -> a
-                           , fSuspension :: ClosureType -> Maybe Type -> HValue -> Maybe Name -> a
+type TermProcessor a b = Type -> Either String DataCon -> HValue -> [a] -> b
+
+data TermFold a = TermFold { fTerm        :: TermProcessor a a
+                           , fPrim        :: Type -> [Word] -> a
+                           , fSuspension  :: ClosureType -> Type -> HValue
+                                            -> Maybe Name -> a
+                           , fNewtypeWrap :: Type -> Either String DataCon
+                                            -> a -> a
+                           , fRefWrap     :: Type -> 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)
+foldTerm tf (RefWrap ty t)         = fRefWrap tf ty (foldTerm tf t)
 
 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
+              fSuspension = (((return.).).). Suspension,
+              fNewtypeWrap= \ty dc t -> NewtypeWrap ty dc `liftM` t,
+              fRefWrap    = \ty t -> RefWrap ty `liftM` t
                        }
 
+mapTermType :: (Type -> Type) -> Term -> Term
+mapTermType f = foldTerm idTermFold {
+          fTerm       = \ty dc hval tt -> Term (f ty) dc hval tt,
+          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}
+
+termTyVars :: Term -> TyVarSet
+termTyVars = foldTerm TermFold {
+            fTerm       = \ty _ _ tt   -> 
+                          tyVarsOfType ty `plusVarEnv` concatVarEnv tt,
+            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
 ----------------------------------
 
-parensCond True  = parens
-parensCond False = id
-app_prec::Int
-app_prec = 10
-
-printTerm :: Term -> SDoc
-printTerm Prim{value=value} = text value 
-printTerm t@Term{} = printTerm1 0 t 
-printTerm Suspension{bound_to=Nothing} =  char '_' -- <> ppr ct <> char '_'
-printTerm Suspension{mb_ty=Just ty, bound_to=Just n} =
-  parens$ ppr n <> text "::" <> ppr ty 
-
-printTerm1 p Term{dc=dc, subTerms=tt} 
-{-  | dataConIsInfix dc, (t1:t2:tt') <- tt 
-  = parens (printTerm1 True t1 <+> ppr dc <+> printTerm1 True ppr t2) 
-    <+> hsep (map (printTerm1 True) tt) 
--}
-  | null tt   = ppr dc
-  | otherwise = parensCond (p > app_prec) 
-                     (ppr dc <+> sep (map (printTerm1 (app_prec+1)) tt))
-
-  where fixity   = undefined 
-
-printTerm1 _ t = printTerm t
-
-customPrintTerm :: Monad m => ((Int->Term->m SDoc)->[Term->m (Maybe SDoc)]) -> Term -> m SDoc
-customPrintTerm custom = let 
---  go :: Monad m => Int -> Term -> m SDoc
-  go prec t@Term{subTerms=tt, dc=dc} = do
-    mb_customDocs <- sequence$ sequence (custom go) t  -- Inner sequence is List monad
-    case msum mb_customDocs of        -- msum is in Maybe monad
-      Just doc -> return$ parensCond (prec>app_prec+1) doc
---    | dataConIsInfix dc, (t1:t2:tt') <- tt =
-      Nothing  -> do pprSubterms <- mapM (go (app_prec+1)) tt
-                     return$ parensCond (prec>app_prec+1) 
-                                        (ppr dc <+> sep pprSubterms)
-  go _ t = return$ printTerm t
-  in go 0 
-   where fixity = undefined 
-
-customPrintTermBase :: Monad m => (Int->Term-> m SDoc)->[Term->m (Maybe SDoc)]
-customPrintTermBase showP =
-  [ 
-    test isTupleDC (liftM (parens . hcat . punctuate comma) . mapM (showP 0) . subTerms)
-  , test (isDC consDataCon) (\Term{subTerms=[h,t]} -> doList h t)
-  , test (isDC intDataCon)  (coerceShow$ \(a::Int)->a)
-  , test (isDC charDataCon) (coerceShow$ \(a::Char)->a)
---  , test (isDC wordDataCon) (coerceShow$ \(a::Word)->a)
-  , test (isDC floatDataCon) (coerceShow$ \(a::Float)->a)
-  , test (isDC doubleDataCon) (coerceShow$ \(a::Double)->a)
-  , test isIntegerDC (coerceShow$ \(a::Integer)->a)
-  ] 
-     where test pred f t = if pred t then liftM Just (f 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 h t = do
-               let elems = h : getListTerms t
-                   isConsLast = isSuspension (last elems) && 
-                                (mb_ty$ last elems) /= (termType h)
-               init <- mapM (showP 0) (init elems) 
-               last0 <- showP 0 (last elems)
-               let last = case length elems of 
-                            1 -> last0 
-                            _ | isConsLast -> text " | " <> last0
-                            _ -> comma <> last0
-               return$ brackets (hcat (punctuate comma init ++ [last]))
-
-                where Just a /= Just b = not (a `coreEqType` b)
-                      _      /=   _    = True
-                      getListTerms Term{subTerms=[h,t]} = h : getListTerms t
-                      getListTerms t@Term{subTerms=[]}  = []
+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{bound_to=Nothing} = return$ char '_'
+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,_) <- splitNewTyConApp_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
+
+  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 => CustomTermPrinter m
+cPprTermBase y =
+  [ ifTerm (isTupleTy.ty) (\_p -> liftM (parens . hcat . punctuate comma) 
+                                      . mapM (y (-1))
+                                      . subTerms)
+  , ifTerm (\t -> isTyCon listTyCon (ty t) && subTerms t `lengthIs` 2)
+           (\ p Term{subTerms=[h,t]} -> doList p h t)
+  , ifTerm (isTyCon intTyCon    . ty) (coerceShow$ \(a::Int)->a)
+  , ifTerm (isTyCon charTyCon   . ty) (coerceShow$ \(a::Char)->a)
+  , ifTerm (isTyCon floatTyCon  . ty) (coerceShow$ \(a::Float)->a)
+  , ifTerm (isTyCon doubleTyCon . ty) (coerceShow$ \(a::Double)->a)
+  , ifTerm (isIntegerTy         . ty) (coerceShow$ \(a::Integer)->a)
+  ]
+     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 ty    = fromMaybe False $ do 
+             (tc,_) <- splitTyConApp_maybe ty 
+             return (tc `elem` (fst.unzip.elems) boxedTupleArr)
+
+           isTyCon a_tc ty = fromMaybe False $ do 
+             (tc,_) <- splitTyConApp_maybe ty
+             return (a_tc == tc)
+
+           coerceShow f _p = return . text . show . f . unsafeCoerce# . val
+
+           --Note pprinting of list terms is not lazy
+           doList p h t = do
+               let elems      = h : getListTerms t
+                   isConsLast = not(termType(last elems) `coreEqType` termType h)
+               print_elems <- mapM (y cons_prec) elems
+               return$ if isConsLast
+                     then cparen (p >= cons_prec) 
+                        . pprDeeperList fsep 
+                        . punctuate (space<>colon)
+                        $ print_elems
+                     else brackets (pprDeeperList fcat$
+                                         punctuate comma print_elems)
+
+                where getListTerms Term{subTerms=[h,t]} = h : getListTerms t
+                      getListTerms Term{subTerms=[]}    = []
                       getListTerms t@Suspension{}       = [t]
                       getListTerms t = pprPanic "getListTerms" (ppr t)
 
+
+repPrim :: TyCon -> [Word] -> String
+repPrim t = rep where 
+   rep x
+    | t == charPrimTyCon   = show (build x :: Char)
+    | t == intPrimTyCon    = show (build x :: Int)
+    | t == wordPrimTyCon   = show (build x :: Word)
+    | t == floatPrimTyCon  = show (build x :: Float)
+    | t == doublePrimTyCon = show (build x :: Double)
+    | t == int32PrimTyCon  = show (build x :: Int32)
+    | t == word32PrimTyCon = show (build x :: Word32)
+    | t == int64PrimTyCon  = show (build x :: Int64)
+    | t == word64PrimTyCon = show (build x :: Word64)
+    | t == addrPrimTyCon   = show (nullPtr `plusPtr` build x)
+    | t == stablePtrPrimTyCon  = "<stablePtr>"
+    | t == stableNamePrimTyCon = "<stableName>"
+    | t == statePrimTyCon      = "<statethread>"
+    | t == realWorldTyCon      = "<realworld>"
+    | t == threadIdPrimTyCon   = "<ThreadId>"
+    | t == weakPrimTyCon       = "<Weak>"
+    | t == arrayPrimTyCon      = "<array>"
+    | t == byteArrayPrimTyCon  = "<bytearray>"
+    | t == mutableArrayPrimTyCon = "<mutableArray>"
+    | t == mutableByteArrayPrimTyCon = "<mutableByteArray>"
+    | t == mutVarPrimTyCon= "<mutVar>"
+    | t == mVarPrimTyCon  = "<mVar>"
+    | 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
 -----------------------------------
+{-
+Type Reconstruction is type inference done on heap closures.
+The algorithm walks the heap generating a set of equations, which
+are solved with syntactic unification.
+A type reconstruction equation looks like:
+
+  <datacon reptype>  =  <actual heap contents> 
+
+The full equation set is generated by traversing all the subterms, starting
+from a given term.
+
+The only difficult part is that newtypes are only found in the lhs of equations.
+Right hand sides are missing them. We can either (a) drop them from the lhs, or 
+(b) reconstruct them in the rhs when possible. 
+
+The function congruenceNewtypes takes a shot at (b)
+-}
 
 -- The Type Reconstruction monad
 type TR a = TcM a
 
-runTR :: HscEnv -> TR Term -> IO Term
+runTR :: HscEnv -> TR a -> IO a
 runTR hsc_env c = do 
-  mb_term <- initTcPrintErrors hsc_env iNTERACTIVE (c >>= zonkTerm)
+  mb_term <- runTR_maybe hsc_env c
   case mb_term of 
     Nothing -> panic "Can't unify"
-    Just term -> return term
+    Just x  -> return x
+
+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
+trIO = liftTcM . liftIO
 
+liftTcM :: TcM a -> TR a
+liftTcM = id
+
+newVar :: Kind -> TR TcType
+newVar = liftTcM . fmap mkTyVarTy . newBoxyTyVar
+
+-- | 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))
+
+-- 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 
+addConstraint t1 t2  = congruenceNewtypes t1 t2 >>= uncurry boxyUnify 
+                      >> return () -- TOMDO: what about the coercion?
+                                   -- we should consider family instances 
+
+-- Type & Term reconstruction 
+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 
+                >>= 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$ expandNewtypes $ mapTermType (substTy rev_subst) term
+    where 
+  go bound _ _ _ | seq bound False = undefined
+  go 0 tv _ty a = do
+    clos <- trIO $ getClosureData a
+    return (Suspension (tipe clos) tv a Nothing)
+  go bound 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
+    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 (pred bound) tv ty a
+-- We always follow indirections 
+      Indirection _ -> go bound tv ty $! (ptrs clos ! 0)
+-- We also follow references
+      MutVar _ | Just (tycon,[world,ty_contents]) <- splitTyConApp_maybe ty
+                -- , tycon == mutVarPrimTyCon 
+             -> do
+         contents <- trIO$ IO$ \w -> readMutVar# (unsafeCoerce# a) w
+         tv' <- newVar liftedTypeKind
+         addConstraint tv (mkTyConApp tycon [world,tv'])
+         x <- go bound tv' ty_contents contents
+         return (RefWrap ty x)
 
+ -- The interesting case
+      Constr -> do
+        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 bound) tv tv) (ptrs clos) i 
+                                              | (i, tv) <- zip [0..] vars]
+                       return (Term tv (Left ('<' : tag ++ ">")) a subTerms)
+          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 (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
+            when (not monomorphic) $ do
+                  let myType = mkFunTys (reOrderTerms subTermTvs 
+                                                      subTtypesNP 
+                                                      subTtypes) 
+                                        tv
+                  (signatureType,_) <- instScheme(dataConRepType dc) 
+                  addConstraint myType signatureType
+            subTermsP <- sequence $ drop extra_args 
+                                -- \^^^  all extra arguments are pointed
+                  [ appArr (go (pred bound) tv t) (ptrs clos) i
+                   | (i,tv,t) <- zip3 [0..] subTermTvs subTtypesP]
+            let unboxeds   = extractUnboxed subTtypesNP clos
+                subTermsNP = map (uncurry Prim) (zip subTtypesNP unboxeds)      
+                subTerms   = reOrderTerms subTermsP subTermsNP 
+                                (drop extra_args subTtypes)
+            return (Term tv (Right dc) a subTerms)
+-- The otherwise case: can be a Thunk,AP,PAP,etc.
+      tipe_clos ->
+         return (Suspension tipe_clos tv a Nothing)
+
+  matchSubTypes dc ty
+    | Just (_,ty_args) <- splitTyConApp_maybe (repType ty) 
+--     assumption:             ^^^ looks through newtypes 
+    , isVanillaDataCon dc  --TODO non-vanilla case
+    = dataConInstArgTys dc ty_args
+    | otherwise = dataConRepArgTys dc
+
+-- This is used to 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))
+                    let (t:tt) = pointed in t : reOrderTerms tt unpointed tys
+   | otherwise    = ASSERT2(not(null unpointed)
+                           , ptext (sLit "reOrderTerms") $$ 
+                                       (ppr pointed $$ ppr unpointed))
+                    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         <- tyConSingleDataCon_maybe 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
+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)
+                          (uncurry go)
+                          (Seq.singleton (tv, hval))
+                          max_depth
+                   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)
+                     (\(ty,a) -> go ty a)
+                     (Seq.singleton (tv, hval))
+                     max_depth
+              substTy rev_subst `fmap` zonkTcType tv
+    where 
+--  search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m ()
+  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
+    clos <- trIO $ getClosureData a
+    case tipe clos of
+      Indirection _ -> go tv $! (ptrs clos ! 0)
+      MutVar _ -> do
+         contents <- trIO$ IO$ \w -> readMutVar# (unsafeCoerce# a) w
+         tv'   <- newVar liftedTypeKind
+         world <- newVar liftedTypeKind
+         addConstraint tv (mkTyConApp mutVarPrimTyCon [world,tv'])
+--         x <- go tv' ty_contents contents
+         return [(tv', contents)]
+      Constr -> do
+        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
+            let extra_args = length(dataConRepArgTys dc) -
+                             length(dataConOrigArgTys dc)
+            subTtypes <- mapMif (not . isMonomorphic)
+                                (\t -> newVar (typeKind t))
+                                (dataConRepArgTys dc)
+
+            -- It is vital for newtype reconstruction that the unification step
+            -- is done right here, _before_ the subterms are RTTI reconstructed
+            let myType         = mkFunTys subTtypes tv
+            (signatureType,_) <- instScheme(dataConRepType dc) 
+            addConstraint myType signatureType
+            return $ [ appArr (\e->(t,e)) (ptrs clos) i
+                       | (i,t) <- drop extra_args $ 
+                                     zip [0..] (filter isPointed 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 -> Type -> Type -> IO (Maybe TvSubst)
+improveRTTIType hsc_env ty rtti_ty = runTR_maybe hsc_env $ do
+    let (_,ty0)     = splitForAllTys ty
+        ty_tvs      = varSetElems $ tyVarsOfType ty0
+    let (_,rtti_ty0)= splitForAllTys rtti_ty
+        rtti_tvs    = varSetElems $ tyVarsOfType rtti_ty0
+    (ty_tvs',_,ty')<- tcInstType (mapM tcInstTyVar) (mkSigmaTy ty_tvs   [] ty0)
+    (_,_,rtti_ty') <- tcInstType (mapM tcInstTyVar) (mkSigmaTy rtti_tvs [] rtti_ty0)
+    boxyUnify rtti_ty' ty'
+    tvs1_contents  <- zonkTcTyVars ty_tvs'
+    let subst = uncurry zipTopTvSubst
+                  (unzip [(tv,ty) | tv <- ty_tvs, ty <- tvs1_contents
+                                  , getTyVar_maybe ty /= Just tv
+                                  , not(isTyVarTy ty)])
+--    liftIO $ hPutStrLn stderr $ showSDocDebug $ text "unify " <+> sep [ppr ty, ppr rtti_ty, equals, ppr subst ]
+    return subst
+
+-- 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 
  -- 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  
+    = recoverTc (return (lhs,rhs)) $ do  
          Indirect ty_v <- readMetaTyVar tv
-         (lhs', rhs') <- go rewriteRHS lhs ty_v
-         writeMutVar (metaTvRef tv) (Indirect rhs')
-         return (lhs', rhs)
+         (_lhs1, rhs1) <- congruenceNewtypes ty_v rhs
+         return (lhs, rhs1)
 -- 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
+    = do (l2',r2') <- congruenceNewtypes l2 r2
+         (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 = 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'') 
+    | Just (tycon_l, _) <- splitNewTyConApp_maybe lhs
+    , Just (tycon_r, _) <- splitNewTyConApp_maybe rhs 
+    , tycon_l /= tycon_r 
+    = do rhs' <- upgrade tycon_l rhs
+         return (lhs, rhs')
 
     | 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"
-
-newVar :: Kind -> TR TcTyVar
-newVar = liftTcM . newFlexiTyVar
-
-liftTcM = id
-
-instScheme :: Type -> TR TcType
-instScheme ty = liftTcM$ liftM trd (tcInstType (liftM fst3 . tcInstTyVars) ty)
-    where fst3 (x,y,z) = x
-          trd  (x,y,z) = z
-
-cvObtainTerm :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Term
-cvObtainTerm hsc_env force mb_ty a = 
- -- Obtain the term and tidy the type before returning it
-     cvObtainTerm1 hsc_env force mb_ty a >>= return . tidyTypes 
-   where 
-         tidyTypes = foldTerm idTermFold {
-            fTerm = \ty dc hval tt -> Term (tidy ty) dc hval tt,
-            fSuspension = \ct mb_ty hval n -> 
-                          Suspension ct (fmap tidy mb_ty) hval n
-            }
-         tidy ty = tidyType (emptyTidyOccEnv, tidyVarEnv ty) ty  
-         tidyVarEnv ty = 
-
-             mkVarEnv$ [ (v, setTyVarName v (tyVarName tv))
-                         | (tv,v) <- zip alphaTyVars vars]
-             where vars = varSetElems$ tyVarsOfType ty
-
-cvObtainTerm1 :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Term
-cvObtainTerm1 hsc_env force mb_ty hval = runTR hsc_env $ do
-   tv   <- liftM mkTyVarTy (newVar argTypeKind)
-   when (isJust mb_ty) $ 
-        instScheme (sigmaType$ fromJust mb_ty) >>= addConstraint tv
-   go tv hval
-    where 
-  go tv a = do 
-    ctype <- trIO$ getClosureType a
-    case ctype of
--- Thunks we may want to force
-      Thunk _ | force -> seq a $ go tv a
--- We always follow indirections 
-      _       | isIndirection ctype -> do
-        clos   <- trIO$ getClosureData a
-        (go tv $! (ptrs clos ! 0))
- -- The interesting case
-      Constr -> do
-        m_dc <- trIO$ tcRnRecoverDataCon hsc_env a
-        case m_dc of
-          Nothing -> panic "Can't find the DataCon for a term"
-          Just dc -> do 
-            clos          <- trIO$ getClosureData a
-            let extra_args = length(dataConRepArgTys dc) - length(dataConOrigArgTys dc)
-                subTtypes  = drop extra_args (dataConRepArgTys dc)
-                (subTtypesP, subTtypesNP) = partition isPointed subTtypes
-                n_subtermsP= length subTtypesP
-            subTermTvs    <- mapM (liftM mkTyVarTy . newVar ) (map typeKind subTtypesP)
-            baseType      <- instScheme (dataConRepType dc)
-            let myType     = mkFunTys (reOrderTerms subTermTvs subTtypesNP subTtypes) tv
-            addConstraint myType baseType
-            subTermsP <- sequence [ extractSubterm i tv (ptrs clos) 
-                                   | (i,tv) <- zip [extra_args..extra_args + n_subtermsP - 1]
-                                                   subTermTvs ]
-            let unboxeds   = extractUnboxed subTtypesNP (nonPtrs clos)
-                subTermsNP = map (uncurry Prim) (zip subTtypesNP unboxeds)      
-                subTerms   = reOrderTerms subTermsP subTermsNP subTtypes
-            return (Term tv dc a subTerms)
--- The otherwise case: can be a Thunk,AP,PAP,etc.
-      otherwise -> do
-         return (Suspension ctype (Just tv) a Nothing)
-
--- Access the array of pointers and recurse down. Needs to be done with
--- care of no introducing a thunk! or go will fail to do its job 
-  extractSubterm (I# i#) tv ptrs = case ptrs of 
-                 (Array _ _ ptrs#) -> case indexArray# ptrs# i# of 
-                       (# e #) -> go tv e
-
--- This is used to put together pointed and nonpointed subterms in the 
---  correct order.
-  reOrderTerms _ _ [] = []
-  reOrderTerms pointed unpointed (ty:tys) 
-   | isPointed ty = head pointed : reOrderTerms (tail pointed) unpointed tys
-   | otherwise    = head unpointed : reOrderTerms pointed (tail unpointed) tys
+    where upgrade :: TyCon -> Type -> TR Type
+          upgrade new_tycon ty
+            | 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
+  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
+       (# 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)}  
+             ,fSuspension = \ct ty v b -> zonkTcType ty >>= \ty ->
+                                          return (Suspension ct ty v b)
+             ,fNewtypeWrap= \ty dc t -> 
+                   return NewtypeWrap `ap` zonkTcType ty `ap` return dc `ap` t}
 
 
 -- Is this defined elsewhere?
--- Find all free tyvars and insert the appropiate ForAll.
+-- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
+sigmaType :: Type -> Type
 sigmaType ty = mkForAllTys (varSetElems$ tyVarsOfType (dropForAlls ty)) ty
 
-{-
-Example of Type Reconstruction
---------------------------------
-Suppose we have an existential type such as
-
-data Opaque = forall a. Opaque a
-
-And we have a term built as:
-
-t = Opaque (map Just [[1,1],[2,2]])
-
-The type of t as far as the typechecker goes is t :: Opaque
-If we seq the head of t, we obtain:
-
-t - O (_1::a) 
-
-seq _1 ()
-
-t - O ( (_3::b) : (_4::[b]) ) 
-
-seq _3 ()
-
-t - O ( (Just (_5::c)) : (_4::[b]) ) 
-
-At this point, we know that b = (Maybe c)
-
-seq _5 ()
-
-t - O ( (Just ((_6::d) : (_7::[d]) )) : (_4::[b]) )
-
-At this point, we know that c = [d]
-
-seq _6 ()
-
-t - O ( (Just (1 : (_7::[d]) )) : (_4::[b]) )
-
-At this point, we know that d = Integer
-
-The fully reconstructed expressions, with propagation, would be:
-
-t - O ( (Just (_5::c)) : (_4::[Maybe c]) ) 
-t - O ( (Just ((_6::d) : (_7::[d]) )) : (_4::[Maybe [d]]) )
-t - O ( (Just (1 : (_7::[Integer]) )) : (_4::[Maybe [Integer]]) )
-
-
-For reference, the type of the thing inside the opaque is 
-map Just [[1,1],[2,2]] :: [Maybe [Integer]]
-
-NOTE: (Num t) contexts have been manually replaced by Integer for clarity
--}
-
---------------------------------------------------------------------
--- The DataConEnv is used to store the addresses of datacons loaded
--- via the dynamic linker
---------------------------------------------------------------------
-
-type DataConEnv   = AddressEnv StgInfoTable
-
--- Note that this AddressEnv and DataConEnv I wrote trying to follow 
--- conventions in ghc, but probably they make not much sense.
-
-newtype AddressEnv a = AE {aenv:: FiniteMap (Ptr a) Name}
-  deriving (Outputable)
-
-emptyAddressEnv = AE emptyFM
-
-extendAddressEnvList  :: AddressEnv a -> [(Ptr a, Name)] -> AddressEnv a
-elemAddressEnv        :: Ptr a -> AddressEnv a -> Bool
-delFromAddressEnv     :: AddressEnv a -> Ptr a -> AddressEnv a
-nullAddressEnv        :: AddressEnv a -> Bool
-lookupAddressEnv       :: AddressEnv a -> Ptr a -> Maybe Name
-
-extendAddressEnvList  (AE env) = AE . addListToFM env 
-elemAddressEnv   ptr  (AE env) = ptr `elemFM` env
-delFromAddressEnv     (AE env) = AE . delFromFM env
-nullAddressEnv                 = isEmptyFM . aenv
-lookupAddressEnv      (AE env) = lookupFM env
-
 
-instance Outputable (Ptr a) where
-  ppr = text . show