Type checking for type synonym families
[ghc-hetmet.git] / compiler / ghci / RtClosureInspect.hs
1 -----------------------------------------------------------------------------
2 --
3 -- GHC Interactive support for inspecting arbitrary closures at runtime
4 --
5 -- Pepe Iborra (supported by Google SoC) 2006
6 --
7 -----------------------------------------------------------------------------
8
9 module RtClosureInspect(
10   
11      cvObtainTerm,       -- :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Term
12
13      Term(..),
14      pprTerm, 
15      cPprTerm, 
16      cPprTermBase,
17      termType,
18      foldTerm, 
19      TermFold(..), 
20      idTermFold, 
21      idTermFoldM,
22      isFullyEvaluated, 
23      isPointed,
24      isFullyEvaluatedTerm,
25      mapTermType,
26      termTyVars,
27 --     unsafeDeepSeq, 
28      cvReconstructType,
29      computeRTTIsubst, 
30      sigmaType
31  ) where 
32
33 #include "HsVersions.h"
34
35 import ByteCodeItbls    ( StgInfoTable )
36 import qualified ByteCodeItbls as BCI( StgInfoTable(..) )
37 import HscTypes         ( HscEnv )
38 import Linker
39
40 import DataCon          
41 import Type             
42 import TcRnMonad        ( TcM, initTc, initTcPrintErrors, ioToTcRn, 
43                           tryTcErrs)
44 import TcType
45 import TcMType
46 import TcUnify
47 import TcGadt
48 import TcEnv
49 import DriverPhases
50 import TyCon            
51 import Name 
52 import VarEnv
53 import Util
54 import VarSet
55
56 import TysPrim          
57 import PrelNames
58 import TysWiredIn
59
60 import Constants
61 import Outputable
62 import Maybes
63 import Panic
64
65 import GHC.Arr          ( Array(..) )
66 import GHC.Exts
67
68 import Control.Monad
69 import Data.Maybe
70 import Data.Array.Base
71 import Data.List        ( partition )
72 import qualified Data.Sequence as Seq
73 import Foreign
74 import System.IO.Unsafe
75
76 ---------------------------------------------
77 -- * A representation of semi evaluated Terms
78 ---------------------------------------------
79 {-
80   A few examples in this representation:
81
82   > Just 10 = Term Data.Maybe Data.Maybe.Just (Just 10) [Term Int I# (10) "10"]
83
84   > (('a',_,_),_,('b',_,_)) = 
85       Term ((Char,b,c),d,(Char,e,f)) (,,) (('a',_,_),_,('b',_,_))
86           [ Term (Char, b, c) (,,) ('a',_,_) [Term Char C# "a", Suspension, Suspension]
87           , Suspension
88           , Term (Char, e, f) (,,) ('b',_,_) [Term Char C# "b", Suspension, Suspension]]
89 -}
90
91 data Term = Term { ty        :: Type 
92                  , dc        :: Either String DataCon
93                                -- The heap datacon. If ty is a newtype,
94                                -- this is NOT the newtype datacon.
95                                -- Empty if the datacon aint exported by the .hi
96                                -- (private constructors in -O0 libraries)
97                  , val       :: HValue 
98                  , subTerms  :: [Term] }
99
100           | Prim { ty        :: Type
101                  , value     :: [Word] }
102
103           | Suspension { ctype    :: ClosureType
104                        , mb_ty    :: Maybe Type
105                        , val      :: HValue
106                        , bound_to :: Maybe Name   -- Useful for printing
107                        }
108
109 isTerm, isSuspension, isPrim :: Term -> Bool
110 isTerm Term{} = True
111 isTerm   _    = False
112 isSuspension Suspension{} = True
113 isSuspension      _       = False
114 isPrim Prim{} = True
115 isPrim   _    = False
116
117 termType :: Term -> Maybe Type
118 termType t@(Suspension {}) = mb_ty t
119 termType t = Just$ ty t
120
121 isFullyEvaluatedTerm :: Term -> Bool
122 isFullyEvaluatedTerm Term {subTerms=tt} = all isFullyEvaluatedTerm tt
123 isFullyEvaluatedTerm Suspension {}      = False
124 isFullyEvaluatedTerm Prim {}            = True
125
126 instance Outputable (Term) where
127  ppr = head . cPprTerm cPprTermBase
128
129 -------------------------------------------------------------------------
130 -- Runtime Closure Datatype and functions for retrieving closure related stuff
131 -------------------------------------------------------------------------
132 data ClosureType = Constr 
133                  | Fun 
134                  | Thunk Int 
135                  | ThunkSelector
136                  | Blackhole 
137                  | AP 
138                  | PAP 
139                  | Indirection Int 
140                  | Other Int
141  deriving (Show, Eq)
142
143 data Closure = Closure { tipe         :: ClosureType 
144                        , infoPtr      :: Ptr ()
145                        , infoTable    :: StgInfoTable
146                        , ptrs         :: Array Int HValue
147                        , nonPtrs      :: [Word]
148                        }
149
150 instance Outputable ClosureType where
151   ppr = text . show 
152
153 #include "../includes/ClosureTypes.h"
154
155 aP_CODE = AP
156 pAP_CODE = PAP
157 #undef AP
158 #undef PAP
159
160 getClosureData :: a -> IO Closure
161 getClosureData a =
162    case unpackClosure# a of 
163      (# iptr, ptrs, nptrs #) -> do
164            itbl <- peek (Ptr iptr)
165            let tipe = readCType (BCI.tipe itbl)
166                elems = fromIntegral (BCI.ptrs itbl)
167                ptrsList = Array 0 (elems - 1) elems ptrs
168                nptrs_data = [W# (indexWordArray# nptrs i)
169                               | I# i <- [0.. fromIntegral (BCI.nptrs itbl)] ]
170            ASSERT(fromIntegral elems >= 0) return ()
171            ptrsList `seq` 
172             return (Closure tipe (Ptr iptr) itbl ptrsList nptrs_data)
173
174 readCType :: Integral a => a -> ClosureType
175 readCType i
176  | i >= CONSTR && i <= CONSTR_NOCAF_STATIC = Constr
177  | i >= FUN    && i <= FUN_STATIC          = Fun
178  | i >= THUNK  && i < THUNK_SELECTOR       = Thunk (fromIntegral i)
179  | i == THUNK_SELECTOR                     = ThunkSelector
180  | i == BLACKHOLE                          = Blackhole
181  | i >= IND    && i <= IND_STATIC          = Indirection (fromIntegral i)
182  | fromIntegral i == aP_CODE               = AP
183  | i == AP_STACK                           = AP
184  | fromIntegral i == pAP_CODE              = PAP
185  | otherwise                               = Other (fromIntegral i)
186
187 isConstr, isIndirection, isThunk :: ClosureType -> Bool
188 isConstr Constr = True
189 isConstr    _   = False
190
191 isIndirection (Indirection _) = True
192 --isIndirection ThunkSelector = True
193 isIndirection _ = False
194
195 isThunk (Thunk _)     = True
196 isThunk ThunkSelector = True
197 isThunk AP            = True
198 isThunk _             = False
199
200 isFullyEvaluated :: a -> IO Bool
201 isFullyEvaluated a = do 
202   closure <- getClosureData a 
203   case tipe closure of
204     Constr -> do are_subs_evaluated <- amapM isFullyEvaluated (ptrs closure)
205                  return$ and are_subs_evaluated
206     otherwise -> return False
207   where amapM f = sequence . amap' f
208
209 amap' f (Array i0 i _ arr#) = map g [0 .. i - i0]
210     where g (I# i#) = case indexArray# arr# i# of
211                           (# e #) -> f e
212
213 -- TODO: Fix it. Probably the otherwise case is failing, trace/debug it
214 {-
215 unsafeDeepSeq :: a -> b -> b
216 unsafeDeepSeq = unsafeDeepSeq1 2
217  where unsafeDeepSeq1 0 a b = seq a $! b
218        unsafeDeepSeq1 i a b   -- 1st case avoids infinite loops for non reducible thunks
219         | not (isConstr tipe) = seq a $! unsafeDeepSeq1 (i-1) a b     
220      -- | unsafePerformIO (isFullyEvaluated a) = b
221         | otherwise = case unsafePerformIO (getClosureData a) of
222                         closure -> foldl' (flip unsafeDeepSeq) b (ptrs closure)
223         where tipe = unsafePerformIO (getClosureType a)
224 -}
225 isPointed :: Type -> Bool
226 isPointed t | Just (t, _) <- splitTyConApp_maybe t 
227             = not$ isUnliftedTypeKind (tyConKind t)
228 isPointed _ = True
229
230 extractUnboxed  :: [Type] -> Closure -> [[Word]]
231 extractUnboxed tt clos = go tt (nonPtrs clos)
232    where sizeofType t
233            | Just (tycon,_) <- splitTyConApp_maybe t
234            = ASSERT (isPrimTyCon tycon) sizeofTyCon tycon
235            | otherwise = pprPanic "Expected a TcTyCon" (ppr t)
236          go [] _ = []
237          go (t:tt) xx 
238            | (x, rest) <- splitAt ((sizeofType t + wORD_SIZE - 1) `div` wORD_SIZE) xx 
239            = x : go tt rest
240
241 sizeofTyCon = sizeofPrimRep . tyConPrimRep
242
243 -----------------------------------
244 -- * Traversals for Terms
245 -----------------------------------
246
247 data TermFold a = TermFold { fTerm :: Type -> Either String DataCon -> HValue -> [a] -> a
248                            , fPrim :: Type -> [Word] -> a
249                            , fSuspension :: ClosureType -> Maybe Type -> HValue
250                                            -> Maybe Name -> a
251                            }
252
253 foldTerm :: TermFold a -> Term -> a
254 foldTerm tf (Term ty dc v tt) = fTerm tf ty dc v (map (foldTerm tf) tt)
255 foldTerm tf (Prim ty    v   ) = fPrim tf ty v
256 foldTerm tf (Suspension ct ty v b) = fSuspension tf ct ty v b
257
258 idTermFold :: TermFold Term
259 idTermFold = TermFold {
260               fTerm = Term,
261               fPrim = Prim,
262               fSuspension = Suspension
263                       }
264 idTermFoldM :: Monad m => TermFold (m Term)
265 idTermFoldM = TermFold {
266               fTerm       = \ty dc v tt -> sequence tt >>= return . Term ty dc v,
267               fPrim       = (return.). Prim,
268               fSuspension = (((return.).).). Suspension
269                        }
270
271 mapTermType :: (Type -> Type) -> Term -> Term
272 mapTermType f = foldTerm idTermFold {
273           fTerm       = \ty dc hval tt -> Term (f ty) dc hval tt,
274           fSuspension = \ct mb_ty hval n ->
275                           Suspension ct (fmap f mb_ty) hval n }
276
277 termTyVars :: Term -> TyVarSet
278 termTyVars = foldTerm TermFold {
279             fTerm       = \ty _ _ tt   -> 
280                           tyVarsOfType ty `plusVarEnv` concatVarEnv tt,
281             fSuspension = \_ mb_ty _ _ -> 
282                           maybe emptyVarEnv tyVarsOfType mb_ty,
283             fPrim       = \ _ _ -> emptyVarEnv }
284     where concatVarEnv = foldr plusVarEnv emptyVarEnv
285 ----------------------------------
286 -- Pretty printing of terms
287 ----------------------------------
288
289 app_prec,cons_prec ::Int
290 app_prec = 10
291 cons_prec = 5 -- TODO Extract this info from GHC itself
292
293 pprTerm y p t | Just doc <- pprTermM y p t = doc
294
295 pprTermM :: Monad m => (Int -> Term -> m SDoc) -> Int -> Term -> m SDoc
296 pprTermM y p t@Term{dc=Left dc_tag, subTerms=tt, ty=ty} = do
297   tt_docs <- mapM (y app_prec) tt
298   return$ cparen (not(null tt) && p >= app_prec) (text dc_tag <+> sep tt_docs)
299   
300 pprTermM y p t@Term{dc=Right dc, subTerms=tt, ty=ty} 
301 {-  | dataConIsInfix dc, (t1:t2:tt') <- tt  --TODO fixity
302   = parens (pprTerm1 True t1 <+> ppr dc <+> pprTerm1 True ppr t2) 
303     <+> hsep (map (pprTerm1 True) tt) 
304 -} -- TODO Printing infix constructors properly
305   | null tt   = return$ ppr dc
306   | Just (tc,_) <- splitNewTyConApp_maybe ty
307   , isNewTyCon tc
308   , Just new_dc <- maybeTyConSingleCon tc = do 
309          real_value <- y 10 t{ty=repType ty}
310          return$ cparen (p >= app_prec) (ppr new_dc <+> real_value)
311   | otherwise = do
312          tt_docs <- mapM (y app_prec) tt
313          return$ cparen (p >= app_prec) (ppr dc <+> sep tt_docs)
314
315 pprTermM y _ t = pprTermM1 y t
316 pprTermM1 _ Prim{value=words, ty=ty} = 
317     return$ text$ repPrim (tyConAppTyCon ty) words
318 pprTermM1 y t@Term{} = panic "pprTermM1 - unreachable"
319 pprTermM1 _ Suspension{bound_to=Nothing} = return$ char '_'
320 pprTermM1 _ Suspension{mb_ty=Just ty, bound_to=Just n}
321   | Just _ <- splitFunTy_maybe ty = return$ ptext SLIT("<function>")
322   | otherwise = return$ parens$ ppr n <> text "::" <> ppr ty 
323
324 -- Takes a list of custom printers with a explicit recursion knot and a term, 
325 -- and returns the output of the first succesful printer, or the default printer
326 cPprTerm :: forall m. Monad m => 
327            ((Int->Term->m SDoc)->[Int->Term->m (Maybe SDoc)]) -> Term -> m SDoc
328 cPprTerm custom = go 0 where
329   go prec t@Term{} = do
330     let default_ prec t = Just `liftM` pprTermM go prec t
331         mb_customDocs = [pp prec t | pp <- custom go ++ [default_]]
332     Just doc <- firstJustM mb_customDocs
333     return$ cparen (prec>app_prec+1) doc
334   go _ t = pprTermM1 go t
335   firstJustM (mb:mbs) = mb >>= maybe (firstJustM mbs) (return . Just)
336   firstJustM [] = return Nothing
337
338 -- Default set of custom printers. Note that the recursion knot is explicit
339 cPprTermBase :: Monad m => (Int->Term-> m SDoc)->[Int->Term->m (Maybe SDoc)]
340 cPprTermBase y =
341   [ 
342     ifTerm isTupleTy             (\_ -> liftM (parens . hcat . punctuate comma) 
343                                  . mapM (y (-1)) . subTerms)
344   , ifTerm (\t -> isTyCon listTyCon t && subTerms t `lengthIs` 2)
345                                  (\ p Term{subTerms=[h,t]} -> doList p h t)
346   , ifTerm (isTyCon intTyCon)    (coerceShow$ \(a::Int)->a)
347   , ifTerm (isTyCon charTyCon)   (coerceShow$ \(a::Char)->a)
348 --  , ifTerm (isTyCon wordTyCon) (coerceShow$ \(a::Word)->a)
349   , ifTerm (isTyCon floatTyCon)  (coerceShow$ \(a::Float)->a)
350   , ifTerm (isTyCon doubleTyCon) (coerceShow$ \(a::Double)->a)
351   , ifTerm isIntegerTy           (coerceShow$ \(a::Integer)->a)
352   ] 
353      where ifTerm pred f p t@Term{} | pred t = liftM Just (f p t) 
354            ifTerm _    _ _ _                 = return Nothing
355            isIntegerTy Term{ty=ty} = fromMaybe False $ do
356              (tc,_) <- splitTyConApp_maybe ty 
357              return (tyConName tc == integerTyConName)
358            isTupleTy Term{ty=ty} = fromMaybe False $ do 
359              (tc,_) <- splitTyConApp_maybe ty 
360              return (tc `elem` (fst.unzip.elems) boxedTupleArr)
361            isTyCon a_tc Term{ty=ty} = fromMaybe False $ do 
362              (tc,_) <- splitTyConApp_maybe ty
363              return (a_tc == tc)
364            coerceShow f _ = return . text . show . f . unsafeCoerce# . val
365            --TODO pprinting of list terms is not lazy
366            doList p h t = do
367                let elems = h : getListTerms t
368                    isConsLast = termType(last elems) /= termType h
369                print_elems <- mapM (y cons_prec) elems
370                return$ if isConsLast
371                      then cparen (p >= cons_prec) . hsep . punctuate (space<>colon) 
372                            $ print_elems
373                      else brackets (hcat$ punctuate comma print_elems)
374
375                 where Just a /= Just b = not (a `coreEqType` b)
376                       _      /=   _    = True
377                       getListTerms Term{subTerms=[h,t]} = h : getListTerms t
378                       getListTerms t@Term{subTerms=[]}  = []
379                       getListTerms t@Suspension{}       = [t]
380                       getListTerms t = pprPanic "getListTerms" (ppr t)
381
382
383 repPrim :: TyCon -> [Word] -> String
384 repPrim t = rep where 
385    rep x
386     | t == charPrimTyCon   = show (build x :: Char)
387     | t == intPrimTyCon    = show (build x :: Int)
388     | t == wordPrimTyCon   = show (build x :: Word)
389     | t == floatPrimTyCon  = show (build x :: Float)
390     | t == doublePrimTyCon = show (build x :: Double)
391     | t == int32PrimTyCon  = show (build x :: Int32)
392     | t == word32PrimTyCon = show (build x :: Word32)
393     | t == int64PrimTyCon  = show (build x :: Int64)
394     | t == word64PrimTyCon = show (build x :: Word64)
395     | t == addrPrimTyCon   = show (nullPtr `plusPtr` build x)
396     | t == stablePtrPrimTyCon  = "<stablePtr>"
397     | t == stableNamePrimTyCon = "<stableName>"
398     | t == statePrimTyCon      = "<statethread>"
399     | t == realWorldTyCon      = "<realworld>"
400     | t == threadIdPrimTyCon   = "<ThreadId>"
401     | t == weakPrimTyCon       = "<Weak>"
402     | t == arrayPrimTyCon      = "<array>"
403     | t == byteArrayPrimTyCon  = "<bytearray>"
404     | t == mutableArrayPrimTyCon = "<mutableArray>"
405     | t == mutableByteArrayPrimTyCon = "<mutableByteArray>"
406     | t == mutVarPrimTyCon= "<mutVar>"
407     | t == mVarPrimTyCon  = "<mVar>"
408     | t == tVarPrimTyCon  = "<tVar>"
409     | otherwise = showSDoc (char '<' <> ppr t <> char '>')
410     where build ww = unsafePerformIO $ withArray ww (peek . castPtr) 
411 --   This ^^^ relies on the representation of Haskell heap values being 
412 --   the same as in a C array. 
413
414 -----------------------------------
415 -- Type Reconstruction
416 -----------------------------------
417 {-
418 Type Reconstruction is type inference done on heap closures.
419 The algorithm walks the heap generating a set of equations, which
420 are solved with syntactic unification.
421 A type reconstruction equation looks like:
422
423   <datacon reptype>  =  <actual heap contents> 
424
425 The full equation set is generated by traversing all the subterms, starting
426 from a given term.
427
428 The only difficult part is that newtypes are only found in the lhs of equations.
429 Right hand sides are missing them. We can either (a) drop them from the lhs, or 
430 (b) reconstruct them in the rhs when possible. 
431
432 The function congruenceNewtypes takes a shot at (b)
433 -}
434
435 -- The Type Reconstruction monad
436 type TR a = TcM a
437
438 runTR :: HscEnv -> TR a -> IO a
439 runTR hsc_env c = do 
440   mb_term <- runTR_maybe hsc_env c
441   case mb_term of 
442     Nothing -> panic "Can't unify"
443     Just x  -> return x
444
445 runTR_maybe :: HscEnv -> TR a -> IO (Maybe a)
446 runTR_maybe hsc_env = fmap snd . initTc hsc_env HsSrcFile False iNTERACTIVE
447
448 trIO :: IO a -> TR a 
449 trIO = liftTcM . ioToTcRn
450
451 liftTcM :: TcM a -> TR a
452 liftTcM = id
453
454 newVar :: Kind -> TR TcType
455 newVar = liftTcM . fmap mkTyVarTy . newFlexiTyVar
456
457 -- | Returns the instantiated type scheme ty', and the substitution sigma 
458 --   such that sigma(ty') = ty 
459 instScheme :: Type -> TR (TcType, TvSubst)
460 instScheme ty | (tvs, rho) <- tcSplitForAllTys ty = liftTcM$ do
461    (tvs',theta,ty') <- tcInstType (mapM tcInstTyVar) ty
462    return (ty', zipTopTvSubst tvs' (mkTyVarTys tvs))
463
464 -- Adds a constraint of the form t1 == t2
465 -- t1 is expected to come from walking the heap
466 -- t2 is expected to come from a datacon signature
467 -- Before unification, congruenceNewtypes needs to
468 -- do its magic.
469 addConstraint :: TcType -> TcType -> TR ()
470 addConstraint t1 t2  = congruenceNewtypes t1 t2 >>= uncurry unifyType 
471                        >> return () -- TOMDO: what about the coercion?
472                                     -- we should consider family instances 
473
474
475
476 -- Type & Term reconstruction 
477 cvObtainTerm :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Term
478 cvObtainTerm hsc_env force mb_ty hval = runTR hsc_env $ do
479    tv <- newVar argTypeKind
480    case mb_ty of
481      Nothing -> go tv tv hval >>= zonkTerm
482      Just ty | isMonomorphic ty -> go ty ty hval >>= zonkTerm
483      Just ty -> do 
484               (ty',rev_subst) <- instScheme (sigmaType ty)
485               addConstraint tv ty'
486               term <- go tv tv hval >>= zonkTerm
487               --restore original Tyvars
488               return$ mapTermType (substTy rev_subst) term
489     where 
490   go tv ty a = do 
491     let monomorphic = not(isTyVarTy tv)   
492     -- This ^^^ is a convention. The ancestor tests for
493     -- monomorphism and passes a type instead of a tv
494     clos <- trIO $ getClosureData a
495     case tipe clos of
496 -- Thunks we may want to force
497 -- NB. this won't attempt to force a BLACKHOLE.  Even with :force, we never
498 -- force blackholes, because it would almost certainly result in deadlock,
499 -- and showing the '_' is more useful.
500       t | isThunk t && force -> seq a $ go tv ty a
501 -- We always follow indirections 
502       Indirection _ -> go tv ty $! (ptrs clos ! 0)
503  -- The interesting case
504       Constr -> do
505         Right dcname <- dataConInfoPtrToName (infoPtr clos)
506         (_,mb_dc)    <- tryTcErrs (tcLookupDataCon dcname)
507         case mb_dc of
508           Nothing -> do -- This can happen for private constructors compiled -O0
509                         -- where the .hi descriptor does not export them
510                         -- In such case, we return a best approximation:
511                         --  ignore the unpointed args, and recover the pointeds
512                         -- This preserves laziness, and should be safe.
513                        let tag = showSDoc (ppr dcname)
514                        vars     <- replicateM (length$ elems$ ptrs clos) 
515                                               (newVar (liftedTypeKind))
516                        subTerms <- sequence [appArr (go tv tv) (ptrs clos) i 
517                                               | (i, tv) <- zip [0..] vars]
518                        return (Term tv (Left ('<' : tag ++ ">")) a subTerms)
519           Just dc -> do 
520             let extra_args = length(dataConRepArgTys dc) - 
521                              length(dataConOrigArgTys dc)
522                 subTtypes  = matchSubTypes dc ty
523                 (subTtypesP, subTtypesNP) = partition isPointed subTtypes
524             subTermTvs <- sequence
525                  [ if isMonomorphic t then return t 
526                                       else (newVar k)
527                    | (t,k) <- zip subTtypesP (map typeKind subTtypesP)]
528             -- It is vital for newtype reconstruction that the unification step
529             --  is done right here, _before_ the subterms are RTTI reconstructed
530             when (not monomorphic) $ do
531                   let myType = mkFunTys (reOrderTerms subTermTvs 
532                                                       subTtypesNP 
533                                                       subTtypes) 
534                                         tv
535                   (signatureType,_) <- instScheme(dataConRepType dc) 
536                   addConstraint myType signatureType
537             subTermsP <- sequence $ drop extra_args 
538                                  -- ^^^  all extra arguments are pointed
539                   [ appArr (go tv t) (ptrs clos) i
540                    | (i,tv,t) <- zip3 [0..] subTermTvs subTtypesP]
541             let unboxeds   = extractUnboxed subTtypesNP clos
542                 subTermsNP = map (uncurry Prim) (zip subTtypesNP unboxeds)      
543                 subTerms   = reOrderTerms subTermsP subTermsNP 
544                                 (drop extra_args subTtypes)
545             return (Term tv (Right dc) a subTerms)
546 -- The otherwise case: can be a Thunk,AP,PAP,etc.
547       otherwise -> 
548          return (Suspension (tipe clos) (Just tv) a Nothing)
549
550   matchSubTypes dc ty
551     | Just (_,ty_args) <- splitTyConApp_maybe (repType ty) 
552 --     assumption:             ^^^ looks through newtypes 
553     , isVanillaDataCon dc  --TODO non-vanilla case
554     = dataConInstArgTys dc ty_args
555     | otherwise = dataConRepArgTys dc
556
557 -- This is used to put together pointed and nonpointed subterms in the 
558 --  correct order.
559   reOrderTerms _ _ [] = []
560   reOrderTerms pointed unpointed (ty:tys) 
561    | isPointed ty = ASSERT2(not(null pointed)
562                             , ptext SLIT("reOrderTerms") $$ 
563                                         (ppr pointed $$ ppr unpointed))
564                     head pointed : reOrderTerms (tail pointed) unpointed tys
565    | otherwise    = ASSERT2(not(null unpointed)
566                            , ptext SLIT("reOrderTerms") $$ 
567                                        (ppr pointed $$ ppr unpointed))
568                     head unpointed : reOrderTerms pointed (tail unpointed) tys
569
570
571
572 -- Fast, breadth-first Type reconstruction
573 max_depth = 10 :: Int
574 cvReconstructType :: HscEnv -> Bool -> Maybe Type -> HValue -> IO (Maybe Type)
575 cvReconstructType hsc_env force mb_ty hval = runTR_maybe hsc_env $ do
576    tv <- newVar argTypeKind
577    case mb_ty of
578      Nothing -> do search (isMonomorphic `fmap` zonkTcType tv)
579                           (uncurry go)  
580                           [(tv, hval)]  
581                           max_depth
582                    zonkTcType tv  -- TODO untested!
583      Just ty | isMonomorphic ty -> return ty
584      Just ty -> do 
585               (ty',rev_subst) <- instScheme (sigmaType ty) 
586               addConstraint tv ty'
587               search (isMonomorphic `fmap` zonkTcType tv) 
588                      (\(ty,a) -> go ty a) 
589                      [(tv, hval)]
590                      max_depth
591               substTy rev_subst `fmap` zonkTcType tv
592     where 
593 --  search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m ()
594   search stop expand [] depth  = return ()
595   search stop expand x 0 = fail$ "Failed to reconstruct a type after " ++
596                                 show max_depth ++ " steps"
597   search stop expand (x:xx) d  = unlessM stop $ do 
598     new <- expand x 
599     search stop expand (xx ++ new) $! (pred d)
600
601    -- returns unification tasks,since we are going to want a breadth-first search
602   go :: Type -> HValue -> TR [(Type, HValue)]
603   go tv a = do 
604     clos <- trIO $ getClosureData a
605     case tipe clos of
606       Indirection _ -> go tv $! (ptrs clos ! 0)
607       Constr -> do
608         Right dcname <- dataConInfoPtrToName (infoPtr clos)
609         (_,mb_dc)    <- tryTcErrs (tcLookupDataCon dcname)
610         case mb_dc of
611           Nothing-> do 
612                      --  TODO: Check this case
613             vars     <- replicateM (length$ elems$ ptrs clos) 
614                                    (newVar (liftedTypeKind))
615             subTerms <- sequence [ appArr (go tv) (ptrs clos) i 
616                                    | (i, tv) <- zip [0..] vars]    
617             forM [0..length (elems $ ptrs clos)] $ \i -> do
618                         tv <- newVar liftedTypeKind 
619                         return$ appArr (\e->(tv,e)) (ptrs clos) i
620
621           Just dc -> do 
622             let extra_args = length(dataConRepArgTys dc) - 
623                              length(dataConOrigArgTys dc)
624             subTtypes <- mapMif (not . isMonomorphic)
625                                 (\t -> newVar (typeKind t))
626                                 (dataConRepArgTys dc)
627             -- It is vital for newtype reconstruction that the unification step
628             -- is done right here, _before_ the subterms are RTTI reconstructed
629             let myType         = mkFunTys subTtypes tv
630             (signatureType,_) <- instScheme(dataConRepType dc) 
631             addConstraint myType signatureType
632             return $ [ appArr (\e->(t,e)) (ptrs clos) i
633                        | (i,t) <- drop extra_args $ zip [0..] subTtypes]
634       otherwise -> return []
635
636      -- This helper computes the difference between a base type t and the 
637      -- improved rtti_t computed by RTTI
638      -- The main difference between RTTI types and their normal counterparts
639      --  is that the former are _not_ polymorphic, thus polymorphism must
640      --  be stripped. Syntactically, forall's must be stripped
641 computeRTTIsubst ty rtti_ty = 
642      -- In addition, we strip newtypes too, since the reconstructed type might
643      --   not have recovered them all
644            tcUnifyTys (const BindMe) 
645                       [repType' $ dropForAlls$ ty]
646                       [repType' $ rtti_ty]  
647 -- TODO stripping newtypes shouldn't be necessary, test
648
649
650 -- Dealing with newtypes
651 {-
652    A parallel fold over two Type values, 
653  compensating for missing newtypes on both sides. 
654  This is necessary because newtypes are not present 
655  in runtime, but since sometimes there is evidence 
656  available we do our best to reconstruct them. 
657    Evidence can come from DataCon signatures or 
658  from compile-time type inference.
659    I am using the words congruence and rewriting 
660  because what we are doing here is an approximation 
661  of unification modulo a set of equations, which would 
662  come from newtype definitions. These should be the 
663  equality coercions seen in System Fc. Rewriting 
664  is performed, taking those equations as rules, 
665  before launching unification.
666
667    It doesn't make sense to rewrite everywhere, 
668  or we would end up with all newtypes. So we rewrite 
669  only in presence of evidence.
670    The lhs comes from the heap structure of ptrs,nptrs. 
671    The rhs comes from a DataCon type signature. 
672  Rewriting in the rhs is restricted to the result type.
673
674    Note that it is very tricky to make this 'rewriting'
675  work with the unification implemented by TcM, where
676  substitutions are 'inlined'. The order in which 
677  constraints are unified is vital for this (or I am 
678  using TcM wrongly).
679 -}
680 congruenceNewtypes ::  TcType -> TcType -> TcM (TcType,TcType)
681 congruenceNewtypes lhs rhs 
682  -- TyVar lhs inductive case
683     | Just tv <- getTyVar_maybe lhs 
684     = recoverTc (return (lhs,rhs)) $ do  
685          Indirect ty_v <- readMetaTyVar tv
686          (lhs1, rhs1) <- congruenceNewtypes ty_v rhs
687          return (lhs, rhs1)
688 -- FunTy inductive case
689     | Just (l1,l2) <- splitFunTy_maybe lhs
690     , Just (r1,r2) <- splitFunTy_maybe rhs
691     = do (l2',r2') <- congruenceNewtypes l2 r2
692          (l1',r1') <- congruenceNewtypes l1 r1
693          return (mkFunTy l1' l2', mkFunTy r1' r2')
694 -- TyconApp Inductive case; this is the interesting bit.
695     | Just (tycon_l, args_l) <- splitNewTyConApp_maybe lhs
696     , Just (tycon_r, args_r) <- splitNewTyConApp_maybe rhs 
697     , tycon_l /= tycon_r 
698     = return (lhs, upgrade tycon_l rhs)
699
700     | otherwise = return (lhs,rhs)
701
702     where upgrade :: TyCon -> Type -> Type
703           upgrade new_tycon ty
704             | not (isNewTyCon new_tycon) = ty 
705             | ty' <- mkTyConApp new_tycon (map mkTyVarTy $ tyConTyVars new_tycon)
706             , Just subst <- tcUnifyTys (const BindMe) [ty] [repType ty']
707             = substTy subst ty'
708         -- assumes that reptype doesn't touch tyconApp args ^^^
709
710
711 --------------------------------------------------------------------------------
712 -- Semantically different to recoverM in TcRnMonad 
713 -- recoverM retains the errors in the first action,
714 --  whereas recoverTc here does not
715 recoverTc recover thing = do 
716   (_,mb_res) <- tryTcErrs thing
717   case mb_res of 
718     Nothing  -> recover
719     Just res -> return res
720
721 isMonomorphic ty | (tvs, ty') <- splitForAllTys ty
722                  = null tvs && (isEmptyVarSet . tyVarsOfType) ty'
723
724 mapMif :: Monad m => (a -> Bool) -> (a -> m a) -> [a] -> m [a]
725 mapMif pred f xx = sequence $ mapMif_ pred f xx
726 mapMif_ pred f []     = []
727 mapMif_ pred f (x:xx) = (if pred x then f x else return x) : mapMif_ pred f xx
728
729 unlessM condM acc = condM >>= \c -> unless c acc
730
731 -- Strict application of f at index i
732 appArr f a@(Array _ _ _ ptrs#) i@(I# i#)
733  = ASSERT (i < length(elems a))
734    case indexArray# ptrs# i# of
735        (# e #) -> f e
736
737 zonkTerm :: Term -> TcM Term
738 zonkTerm = foldTerm idTermFoldM {
739               fTerm = \ty dc v tt -> sequence tt      >>= \tt ->
740                                      zonkTcType ty    >>= \ty' ->
741                                      return (Term ty' dc v tt)
742              ,fSuspension = \ct ty v b -> fmapMMaybe zonkTcType ty >>= \ty ->
743                                           return (Suspension ct ty v b)}  
744
745
746 -- Is this defined elsewhere?
747 -- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
748 sigmaType ty = mkForAllTys (varSetElems$ tyVarsOfType (dropForAlls ty)) ty
749
750