Rename maybeTyConSingleCon to tyConSingleDataCon_maybe
[ghc-hetmet.git] / compiler / ghci / RtClosureInspect.hs
index 945e752..509eb99 100644 (file)
@@ -14,6 +14,7 @@ module RtClosureInspect(
      isTerm,
      isSuspension,
      isPrim,
+     isNewtypeWrap,
      pprTerm, 
      cPprTerm, 
      cPprTermBase,
@@ -30,7 +31,7 @@ module RtClosureInspect(
      termTyVars,
 --     unsafeDeepSeq, 
      cvReconstructType,
-     computeRTTIsubst, 
+     improveRTTIType,
      sigmaType,
      Closure(..),
      getClosureData,
@@ -46,33 +47,34 @@ 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
 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
 
-import Constants
 import Outputable
-import Maybes
+import FastString
 import Panic
 
+import Constants        ( wORD_SIZE )
+
 import GHC.Arr          ( Array(..) )
 import GHC.Exts
+import GHC.IOBase ( IO(IO) )
 
 import Control.Monad
 import Data.Maybe
@@ -85,27 +87,19 @@ 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", Suspension, Suspension]
-          , Suspension
-          , Term (Char, e, f) (,,) ('b',_,_) [Term Char C# "b", Suspension, Suspension]]
 -}
 
 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)
+                               -- 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] }
 
@@ -113,30 +107,39 @@ data Term = Term { ty        :: Type
                  , 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 :: 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
-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 . 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
@@ -149,7 +152,8 @@ data ClosureType = Constr
                  | AP 
                  | PAP 
                  | Indirection Int 
-                 | Other Int
+                 | MutVar Int
+                 | Other  Int
  deriving (Show, Eq)
 
 data Closure = Closure { tipe         :: ClosureType 
@@ -174,7 +178,17 @@ 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 = fromIntegral (BCI.ptrs itbl)
                ptrsList = Array 0 (elems - 1) elems ptrs
@@ -185,24 +199,25 @@ getClosureData a =
             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)
-
+ | 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
@@ -249,99 +264,132 @@ extractUnboxed tt clos = go tt (nonPtrs clos)
            | otherwise = pprPanic "Expected a TcTyCon" (ppr t)
          go [] _ = []
          go (t:tt) xx 
-           | (x, rest) <- splitAt ((sizeofType t + wORD_SIZE - 1) `div` wORD_SIZE) xx 
+           | (x, rest) <- splitAt (sizeofType t) xx
            = x : go tt rest
 
-sizeofTyCon :: TyCon -> Int
-sizeofTyCon = sizeofPrimRep . tyConPrimRep
+sizeofTyCon :: TyCon -> Int -- in *words*
+sizeofTyCon = primRepSizeW . tyConPrimRep
 
 -----------------------------------
 -- * Traversals for Terms
 -----------------------------------
 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 -> Maybe Type -> HValue
-                                           -> Maybe Name -> a
+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 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}
 
 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,cons_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 :: (Int -> Term -> Maybe SDoc) -> Int -> Term -> SDoc
-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 Term{dc=Left dc_tag, subTerms=tt} = do
+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 <+> 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)
-
-pprTermM _ _ t = pprTermM1 t
-
-pprTermM1 :: Monad m => Term -> m SDoc
-pprTermM1 Prim{value=words, ty=ty} = 
+         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
-pprTermM1 Term{} = panic "pprTermM1 - unreachable"
-pprTermM1 Suspension{bound_to=Nothing} = return$ char '_'
-pprTermM1 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 
-pprTermM1 _ = panic "pprTermM1"
+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
@@ -356,76 +404,70 @@ pprTermM1 _ = panic "pprTermM1"
 --  which I didn't. Therefore, this code replicates a lot
 --  of what type classes provide for free.
 
--- Concretely a custom term printer takes an explicit
---  recursion knot, and produces a list of Term Processors,
---  which additionally need a precedence value to
---  either produce a SDoc or fail (and they do this in some monad m).
+type CustomTermPrinter m = TermPrinterM m
+                         -> [Precedence -> Term -> (m (Maybe SDoc))]
 
-type Precedence          = Int
-type RecursionKnot m     = Int-> Term -> m SDoc
-type CustomTermPrinter m = RecursionKnot m
-                         -> [Precedence -> TermProcessor Term (m (Maybe SDoc))]
-
--- Takes a list of custom printers with a explicit recursion knot and a term, 
+-- | 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@(Term ty dc val tt) = do
+  go prec t = do
     let default_ = Just `liftM` pprTermM go prec t
-        mb_customDocs = [pp prec ty dc val tt | pp <- printers] ++ [default_]
+        mb_customDocs = [pp prec t | pp <- printers] ++ [default_]
     Just doc <- firstJustM mb_customDocs
     return$ cparen (prec>app_prec+1) doc
-  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 => CustomTermPrinter m
 cPprTermBase y =
-  [ 
-    ifTerm isTupleTy             (\ _ _ tt -> 
-                                      liftM (parens . hcat . punctuate comma) 
-                                    . mapM (y (-1))
-                                    $ tt)
-  , ifTerm (\ty tt -> isTyCon listTyCon ty tt && tt `lengthIs` 2)
-                                 (\ p _ [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)
+  [ 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 ty _ val tt 
-               | pred ty tt = liftM Just (f prec val tt)
-               | otherwise     = return Nothing
-           isIntegerTy ty _ = fromMaybe False $ do
+     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 
+
+           isTupleTy ty    = fromMaybe False $ do 
              (tc,_) <- splitTyConApp_maybe ty 
              return (tc `elem` (fst.unzip.elems) boxedTupleArr)
-           isTyCon a_tc ty _ = fromMaybe False $ do 
+
+           isTyCon a_tc ty = fromMaybe False $ do 
              (tc,_) <- splitTyConApp_maybe ty
              return (a_tc == tc)
-           coerceShow f _ val _ = (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
-                   isConsLast = termType(last elems) /= termType h
+               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) 
-                        . hsep 
+                        . pprDeeperList fsep 
                         . punctuate (space<>colon)
                         $ print_elems
-                     else brackets (hcat$ punctuate comma 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 Term{subTerms=[]}  = []
+                where getListTerms Term{subTerms=[h,t]} = h : getListTerms t
+                      getListTerms Term{subTerms=[]}    = []
                       getListTerms t@Suspension{}       = [t]
                       getListTerms t = pprPanic "getListTerms" (ppr t)
 
@@ -493,16 +535,19 @@ runTR hsc_env c = do
     Just x  -> return x
 
 runTR_maybe :: HscEnv -> TR a -> IO (Maybe a)
-runTR_maybe hsc_env = fmap snd . initTc hsc_env HsSrcFile False iNTERACTIVE
+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 . newFlexiTyVar
+newVar = liftTcM . fmap mkTyVarTy . newBoxyTyVar
 
 -- | Returns the instantiated type scheme ty', and the substitution sigma 
 --   such that sigma(ty') = ty 
@@ -517,7 +562,7 @@ instScheme ty | (tvs, _rho) <- tcSplitForAllTys ty = liftTcM$ do
 -- 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 
 
@@ -526,19 +571,23 @@ 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
     clos <- trIO $ getClosureData a
-    return (Suspension (tipe clos) (Just tv) a Nothing)
+    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
@@ -551,7 +600,17 @@ 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)
+-- 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)
@@ -587,7 +646,7 @@ cvObtainTerm hsc_env bound force mb_ty hval = runTR hsc_env $ do
                   (signatureType,_) <- instScheme(dataConRepType dc) 
                   addConstraint myType signatureType
             subTermsP <- sequence $ drop extra_args 
-                                 -- ^^^  all extra arguments are pointed
+                                -- \^^^  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
@@ -596,10 +655,9 @@ cvObtainTerm hsc_env bound force mb_ty hval = runTR hsc_env $ do
                                 (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 (Just tv) a Nothing)
+      tipe_clos ->
+         return (Suspension tipe_clos 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 
@@ -612,14 +670,26 @@ cvObtainTerm hsc_env bound force mb_ty hval = runTR hsc_env $ do
   reOrderTerms _ _ [] = []
   reOrderTerms pointed unpointed (ty:tys) 
    | isPointed ty = ASSERT2(not(null pointed)
-                            , ptext SLIT("reOrderTerms") $$ 
+                            , 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") $$ 
+                           , 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         <- 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
@@ -643,8 +713,8 @@ cvReconstructType hsc_env max_depth mb_ty hval = runTR_maybe hsc_env $ do
               substTy rev_subst `fmap` zonkTcType tv
     where 
 --  search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m ()
-  search _ _ _ 0 = fail$ "Failed to reconstruct a type after " ++
-                                show max_depth ++ " steps"
+  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 ()
@@ -658,6 +728,13 @@ cvReconstructType hsc_env max_depth mb_ty hval = runTR_maybe hsc_env $ 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)
@@ -685,52 +762,57 @@ cvReconstructType hsc_env max_depth mb_ty hval = runTR_maybe hsc_env $ do
                                      zip [0..] (filter isPointed subTtypes)]
       _ -> 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
-computeRTTIsubst :: Type -> Type -> Maybe TvSubst
-computeRTTIsubst 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
-
+-- 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 ::  TcType -> TcType -> TR (TcType,TcType)
 congruenceNewtypes lhs rhs 
  -- TyVar lhs inductive case
     | Just tv <- getTyVar_maybe lhs 
@@ -748,18 +830,20 @@ congruenceNewtypes lhs 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'
-          upgrade _ _ = panic "congruenceNewtypes.upgrade"
-        -- 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'
 
 
 --------------------------------------------------------------------------------
@@ -798,8 +882,10 @@ 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?