Update the panic msg from #1257 to be an ordinary error, not a panic
[ghc-hetmet.git] / compiler / ghci / RtClosureInspect.hs
index 170dec0..f289b14 100644 (file)
@@ -10,26 +10,10 @@ 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,
+     Term(..),
+     pprTerm, 
+     cPprTerm, 
+     cPprTermBase,
      termType,
      foldTerm, 
      TermFold(..), 
@@ -38,6 +22,8 @@ module RtClosureInspect(
      isFullyEvaluated, 
      isPointed,
      isFullyEvaluatedTerm,
+     mapTermType,
+     termTyVars
 --     unsafeDeepSeq, 
  ) where 
 
@@ -82,9 +68,11 @@ import GHC.Word         ( Word32(..), Word64(..) )
 import Control.Monad
 import Data.Maybe
 import Data.Array.Base
-import Data.List        ( partition )
+import Data.List        ( partition, nub )
 import Foreign.Storable
 
+import IO
+
 ---------------------------------------------
 -- * A representation of semi evaluated Terms
 ---------------------------------------------
@@ -95,9 +83,9 @@ import Foreign.Storable
 
   > (('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]]
+          [ 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 
@@ -130,7 +118,7 @@ isFullyEvaluatedTerm Suspension {}      = False
 isFullyEvaluatedTerm Prim {}            = True
 
 instance Outputable (Term) where
- ppr = head . customPrintTerm customPrintTermBase
+ ppr = head . cPprTerm cPprTermBase
 
 -------------------------------------------------------------------------
 -- Runtime Closure Datatype and functions for retrieving closure related stuff
@@ -147,23 +135,15 @@ data ClosureType = Constr
  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# 
                        }
 
 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 = AP
@@ -172,14 +152,14 @@ pAP_CODE = PAP
 #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 
+getClosureData a =
+   case unpackClosure# a of 
+     (# iptr, ptrs, nptrs #) -> do
+           itbl <- peek (Ptr iptr)
+           let tipe = readCType (BCI.tipe itbl)
+               elems = BCI.ptrs itbl 
                ptrsList = Array 0 (fromIntegral$ elems) ptrs
-           in ptrsList `seq` return (Closure tipe itbl ptrsList nptrs)
+           ptrsList `seq` return (Closure tipe (Ptr iptr) itbl ptrsList nptrs)
 
 readCType :: Integral a => a -> ClosureType
 readCType i
@@ -190,6 +170,7 @@ readCType i
  | i == BLACKHOLE                          = Blackhole
  | i >= IND    && i <= IND_STATIC          = Indirection (fromIntegral i)
  | fromIntegral i == aP_CODE               = AP
+ | i == AP_STACK                           = AP
  | fromIntegral i == pAP_CODE              = PAP
  | otherwise                               = Other (fromIntegral i)
 
@@ -201,6 +182,11 @@ 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 
@@ -274,7 +260,7 @@ extractUnboxed tt ba = helper tt (byteArrayContents# ba)
            -- TODO: Improve the offset handling in decode (make it machine dependant)
 
 -----------------------------------
--- Boilerplate Fold code for Term
+-- * Traversals for Terms
 -----------------------------------
 
 data TermFold a = TermFold { fTerm :: Type -> DataCon -> HValue -> [a] -> a
@@ -300,81 +286,91 @@ idTermFoldM = TermFold {
               fSuspension = (((return.).).). Suspension
                        }
 
+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 }
+
+termTyVars = foldTerm TermFold {
+            fTerm       = \ty _ _ tt   -> 
+                          tyVarsOfType ty `plusVarEnv` concatVarEnv tt,
+            fSuspension = \_ mb_ty _ _ -> 
+                          maybe emptyVarEnv tyVarsOfType mb_ty,
+            fPrim       = \ _ _ -> emptyVarEnv }
+    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} 
+pprTerm :: Int -> Term -> SDoc
+pprTerm 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) 
+  = parens (pprTerm1 True t1 <+> ppr dc <+> pprTerm1 True ppr t2) 
+    <+> hsep (map (pprTerm1 True) tt) 
 -}
   | null tt   = ppr dc
-  | otherwise = parensCond (p > app_prec) 
-                     (ppr dc <+> sep (map (printTerm1 (app_prec+1)) tt))
+  | otherwise = cparen (p >= app_prec) 
+                       (ppr dc <+> sep (map (pprTerm app_prec) tt))
 
   where fixity   = undefined 
 
-printTerm1 _ t = printTerm t
+pprTerm _ t = pprTerm1 t
+
+pprTerm1 Prim{value=value} = text value 
+pprTerm1 t@Term{} = pprTerm 0 t 
+pprTerm1 Suspension{bound_to=Nothing} =  char '_' -- <> ppr ct <> char '_'
+pprTerm1 Suspension{mb_ty=Just ty, bound_to=Just n}
+  | Just _ <- splitFunTy_maybe ty = ptext SLIT("<function>")
+  | otherwise = parens$ ppr n <> text "::" <> ppr ty 
+
 
-customPrintTerm :: Monad m => ((Int->Term->m SDoc)->[Term->m (Maybe SDoc)]) -> Term -> m SDoc
-customPrintTerm custom = let 
---  go :: Monad m => Int -> Term -> m SDoc
+cPprTerm :: forall m. Monad m => ((Int->Term->m SDoc)->[Int->Term->m (Maybe SDoc)]) -> Term -> m SDoc
+cPprTerm custom = go 0 where
   go prec t@Term{subTerms=tt, dc=dc} = do
-    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
+    let mb_customDocs = map (($t) . ($prec)) (custom go) :: [m (Maybe SDoc)]    
+    first_success <- firstJustM mb_customDocs
+    case first_success of
+      Just doc -> return$ cparen (prec>app_prec+1) doc
 --    | dataConIsInfix dc, (t1:t2:tt') <- tt =
       Nothing  -> do pprSubterms <- mapM (go (app_prec+1)) tt
-                     return$ 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 =
+                     return$ cparen (prec >= app_prec) 
+                                    (ppr dc <+> sep pprSubterms)
+  go _ t = return$ pprTerm1 t
+  firstJustM (mb:mbs) = mb >>= maybe (firstJustM mbs) (return . Just)
+  firstJustM [] = return Nothing
+
+cPprTermBase :: Monad m => (Int->Term-> m SDoc)->[Int->Term->m (Maybe SDoc)]
+cPprTermBase pprP =
   [ 
-    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)
+    ifTerm isTupleDC            (\_ -> liftM (parens . hcat . punctuate comma) 
+                                 . mapM (pprP (-1)) . subTerms)
+  , ifTerm (isDC consDataCon)   (\ p Term{subTerms=[h,t]} -> doList p h t)
+  , ifTerm (isDC intDataCon)    (coerceShow$ \(a::Int)->a)
+  , ifTerm (isDC charDataCon)   (coerceShow$ \(a::Char)->a)
+--  , ifTerm (isDC wordDataCon) (coerceShow$ \(a::Word)->a)
+  , ifTerm (isDC floatDataCon)  (coerceShow$ \(a::Float)->a)
+  , ifTerm (isDC doubleDataCon) (coerceShow$ \(a::Double)->a)
+  , ifTerm isIntegerDC          (coerceShow$ \(a::Integer)->a)
   ] 
-     where test pred f t = if pred t then liftM Just (f t) else return Nothing
+     where ifTerm pred f p t = if pred t then liftM Just (f p t) else return Nothing
            isIntegerDC Term{dc=dc} = 
               dataConName dc `elem` [ smallIntegerDataConName
                                     , largeIntegerDataConName] 
-           isTupleDC Term{dc=dc}   = dc `elem` snd (unzip (elems boxedTupleArr))
-           isDC a_dc Term{dc=dc}   = a_dc == dc
-           coerceShow f = return . text . show . f . unsafeCoerce# . val
+           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
+           doList p 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]))
+                   isConsLast = termType(last elems) /= termType h
+               print_elems <- mapM (pprP 5) elems
+               return$ if isConsLast
+                     then cparen (p >= 5) . hsep . punctuate (space<>colon) 
+                           $ print_elems
+                     else brackets (hcat$ punctuate comma print_elems)
 
                 where Just a /= Just b = not (a `coreEqType` b)
                       _      /=   _    = True
@@ -392,7 +388,7 @@ type TR a = TcM a
 
 runTR :: HscEnv -> TR Term -> IO Term
 runTR hsc_env c = do 
-  mb_term <- initTcPrintErrors hsc_env iNTERACTIVE (c >>= zonkTerm)
+  mb_term <- initTcPrintErrors hsc_env iNTERACTIVE c
   case mb_term of 
     Nothing -> panic "Can't unify"
     Just term -> return term
@@ -401,135 +397,173 @@ trIO :: IO a -> TR a
 trIO = liftTcM . ioToTcRn
 
 addConstraint :: TcType -> TcType -> TR ()
-addConstraint t1 t2  = congruenceNewtypes t1 t2 >> unifyType t1 t2
-
--- A parallel fold over a Type value, replacing
--- in the right side reptypes for newtypes as found in the lhs
--- Sadly it doesn't cover all the possibilities. It does not always manage
--- to recover the highest level type. See test print016 for an example
-congruenceNewtypes ::  TcType -> TcType -> TcM TcType
-congruenceNewtypes lhs rhs
---    | pprTrace "Congruence" (ppr lhs $$ ppr rhs) False = undefined
- -- We have a tctyvar at the other side
+addConstraint t1 t2  = congruenceNewtypes t1 t2 >>= uncurry unifyType 
+
+{-
+   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 
+ 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.
+
+   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).
+-}
+congruenceNewtypes ::  TcType -> TcType -> TcM (TcType,TcType)
+congruenceNewtypes = go True
+  where 
+   go rewriteRHS 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 
---    , trace "congruence, entering tyvar" True
-    = recoverM (return rhs) $ do  
+    = recoverM (return (lhs,rhs)) $ do  
          Indirect ty_v <- readMetaTyVar tv
-         newtyped_tytv <- congruenceNewtypes lhs ty_v
-         writeMutVar (metaTvRef tv) (Indirect newtyped_tytv)
-         return newtyped_tytv
--- We have a function type: go on inductively
-    | Just (r1,r2) <- splitFunTy_maybe rhs
-    , Just (l1,l2) <- splitFunTy_maybe lhs
-    = liftM2 mkFunTy ( congruenceNewtypes l1 r1)
-                      (congruenceNewtypes l2 r2)
--- There is a newtype at the top level tycon and we can manage it
-    | Just (tycon, args)    <- splitNewTyConApp_maybe lhs
-    , isNewTyCon tycon
-    , (tvs, realtipe)       <- newTyConRep tycon
-    =   case tcUnifyTys (const BindMe) [realtipe] [rhs] of
-          Just subst -> 
-                let tvs' = substTys subst (map mkTyVarTy tvs) in
-                liftM (mkTyConApp tycon) (zipWithM congruenceNewtypes args tvs')
-          otherwise -> panic "congruenceNewtypes: Can't unify a newtype"
-                                             
--- We have a TyconApp: go on inductively
-    | Just (tycon, args)     <- splitNewTyConApp_maybe lhs
-    , Just (tycon_v, args_v) <- splitNewTyConApp_maybe rhs
-    = liftM (mkTyConApp tycon_v) (zipWithM congruenceNewtypes args args_v)
-
-    | otherwise = return rhs
-
+         (lhs', rhs') <- go rewriteRHS lhs ty_v
+         writeMutVar (metaTvRef tv) (Indirect rhs')
+         return (lhs', rhs)
+-- FunTy inductive case
+    | Just (l1,l2) <- splitFunTy_maybe lhs
+    , Just (r1,r2) <- splitFunTy_maybe rhs
+    = do (l2',r2') <- go True l2 r2
+         (l1',r1') <- go False l1 r1
+         return (mkFunTy l1' l2', mkFunTy r1' r2')
+-- TyconApp Inductive case; this is the interesting bit.
+    | Just (tycon_l, args_l) <- splitNewTyConApp_maybe lhs
+    , Just (tycon_r, args_r) <- splitNewTyConApp_maybe rhs = do
+
+      let (tycon_l',args_l') = if isNewTyCon tycon_r && not(isNewTyCon tycon_l)
+                                then (tycon_r, rewrite tycon_r lhs)
+                                else (tycon_l, args_l)
+          (tycon_r',args_r') = if rewriteRHS && isNewTyCon tycon_l && not(isNewTyCon tycon_r)
+                                then (tycon_l, rewrite tycon_l rhs)
+                                else (tycon_r, args_r)
+      (args_l'', args_r'') <- unzip `liftM` zipWithM (go rewriteRHS) args_l' args_r'
+      return (mkTyConApp tycon_l' args_l'', mkTyConApp tycon_r' args_r'') 
+
+    | otherwise = return (lhs,rhs)
+
+    where rewrite newtyped_tc lame_tipe
+           | (tvs, tipe) <- newTyConRep newtyped_tc 
+           = case tcUnifyTys (const BindMe) [tipe] [lame_tipe] of
+               Just subst -> substTys subst (map mkTyVarTy tvs)
+               otherwise  -> panic "congruenceNewtypes: Can't unify a newtype"
 
 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
+-- | 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))
 
 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
-  | Nothing <- mb_ty = runTR hsc_env . go argTypeKind $ hval
-  | Just ty <- mb_ty = runTR hsc_env $ do
-                 term <- go argTypeKind hval
-                 ty'  <- instScheme ty
-                 addConstraint ty' (fromMaybe (error "by definition") 
-                                              (termType term)) 
-                 return term
+cvObtainTerm hsc_env force mb_ty hval = runTR hsc_env $ do
+   tv <- liftM mkTyVarTy (newVar argTypeKind)
+   case mb_ty of
+     Nothing -> go tv tv hval >>= zonkTerm
+     Just ty | isMonomorphic ty -> go ty ty hval >>= zonkTerm
+     Just ty -> do 
+              (ty',rev_subst) <- instScheme (sigmaType ty)
+              addConstraint tv ty'
+              term <- go tv tv hval >>= zonkTerm
+              --restore original Tyvars
+              return$ mapTermType (substTy rev_subst) term
     where 
-  go k a = do 
-    ctype <- trIO$ getClosureType a
-    case ctype of
+  go tv ty a = do 
+    let monomorphic = not(isTyVarTy tv)   -- This is a convention. The ancestor tests for
+                                         -- monomorphism and passes a type instead of a tv
+    clos <- trIO $ getClosureData a
+    case tipe clos of
 -- Thunks we may want to force
-      Thunk _ | force -> seq a $ go k a
+-- NB. this won't attempt to force a BLACKHOLE.  Even with :force, we never
+-- force blackholes, because it would almost certainly result in deadlock,
+-- and showing the '_' is more useful.
+      t | isThunk t && force -> seq a $ go tv ty a
 -- We always follow indirections 
-      _       | isIndirection ctype 
-                      -> do
-        clos   <- trIO$ getClosureData a
---      dflags <- getSessionDynFlags session
---      debugTraceMsg dflags 2 (text "Following an indirection")
-        go k $! (ptrs clos ! 0)
+      Indirection _ -> go tv ty $! (ptrs clos ! 0)
  -- The interesting case
       Constr -> do
-        m_dc <- trIO$ tcRnRecoverDataCon hsc_env a
+        m_dc <- trIO$ tcRnRecoverDataCon hsc_env (infoPtr clos)
         case m_dc of
           Nothing -> panic "Can't find the DataCon for a term"
           Just dc -> do 
-            clos          <- trIO$ getClosureData a
             let extra_args = length(dataConRepArgTys dc) - length(dataConOrigArgTys dc)
-                subTtypes  = drop extra_args (dataConRepArgTys dc)
+                subTtypes  = matchSubTypes dc ty
                 (subTtypesP, subTtypesNP) = partition isPointed subTtypes
-                
-            subTermsP <- mapM (\i->extractSubterm i (ptrs clos)
-                                                    (subTtypesP!!(i-extra_args)))
-                              [extra_args..extra_args + length subTtypesP - 1]
+            subTermTvs <- sequence
+                 [ if isMonomorphic t then return t else (mkTyVarTy `fmap` newVar k)
+                   | (t,k) <- zip subTtypesP (map typeKind subTtypesP)]
+            -- It is vital for newtype reconstruction that the unification step is done
+            --     right here, _before_ the subterms are RTTI reconstructed.
+            when (not monomorphic) $ do
+                  let myType = mkFunTys (reOrderTerms subTermTvs subTtypesNP subTtypes) tv
+                  instScheme(dataConRepType dc) >>= addConstraint myType . fst
+            subTermsP <- sequence $ drop extra_args -- all extra arguments are pointed
+                  [ appArr (go tv t) (ptrs clos) i
+                   | (i,tv,t) <- zip3 [0..] subTermTvs subTtypesP]
             let unboxeds   = extractUnboxed subTtypesNP (nonPtrs clos)
                 subTermsNP = map (uncurry Prim) (zip subTtypesNP unboxeds)      
-                subTerms   = reOrderTerms subTermsP subTermsNP subTtypes
-            resType       <- liftM mkTyVarTy (newVar k)
-            baseType      <- instScheme (dataConRepType dc)
-            let myType     = mkFunTys (map (fromMaybe undefined . termType) 
-                                       subTerms) 
-                                  resType
-            addConstraint baseType myType
-            return (Term resType dc a subTerms)
+                subTerms   = reOrderTerms subTermsP subTermsNP (drop extra_args subTtypes)
+            return (Term tv dc a subTerms)
 -- The otherwise case: can be a Thunk,AP,PAP,etc.
-      otherwise -> do
-         x <- liftM mkTyVarTy (newVar k)
-         return (Suspension ctype (Just x) a Nothing)
+      otherwise -> 
+         return (Suspension (tipe clos) (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#) ptrs ty = case ptrs of 
+  appArr f arr (I# i#) = case arr of 
                  (Array _ _ ptrs#) -> case indexArray# ptrs# i# of 
-                       (# e #) -> go (typeKind ty) e
+                       (# e #) -> f e
+
+  matchSubTypes dc ty
+    | Just (_,ty_args) <- splitTyConApp_maybe (repType ty) 
+    , null (dataConExTyVars dc)  --TODO Handle the case of extra existential tyvars
+    = dataConInstArgTys dc ty_args
+
+    | 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 = head pointed : reOrderTerms (tail pointed) unpointed tys
-   | otherwise    = head unpointed : reOrderTerms pointed (tail unpointed) tys
+   | isPointed ty = ASSERT2(not(null pointed)
+                           , ptext SLIT("reOrderTerms") $$ (ppr pointed $$ ppr unpointed))
+                    head pointed : reOrderTerms (tail pointed) unpointed tys
+   | otherwise    = ASSERT2(not(null unpointed)
+                           , ptext SLIT("reOrderTerms") $$ (ppr pointed $$ ppr unpointed))
+                    head unpointed : reOrderTerms pointed (tail unpointed) tys
+
+isMonomorphic ty | isForAllTy ty = False
+isMonomorphic ty = (isEmptyVarSet . tyVarsOfType) ty
 
 zonkTerm :: Term -> TcM Term
 zonkTerm = foldTerm idTermFoldM {
@@ -539,6 +573,11 @@ zonkTerm = foldTerm idTermFoldM {
              ,fSuspension = \ct ty v b -> fmapMMaybe zonkTcType ty >>= \ty ->
                                           return (Suspension ct ty v b)}  
 
+
+-- Is this defined elsewhere?
+-- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
+sigmaType ty = mkForAllTys (varSetElems$ tyVarsOfType (dropForAlls ty)) ty
+
 {-
 Example of Type Reconstruction
 --------------------------------
@@ -589,34 +628,3 @@ 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