Fix FFI declaration checks
[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      cvObtainTerm,      -- :: HscEnv -> Int -> Bool -> Maybe Type -> HValue -> IO Term
11      cvReconstructType,
12      improveRTTIType,
13
14      Term(..),
15      isTerm, isSuspension, isPrim, isFun, isFunLike, isNewtypeWrap,
16      isFullyEvaluated, isFullyEvaluatedTerm,
17      termType, mapTermType, termTyVars,
18      foldTerm, TermFold(..), foldTermM, TermFoldM(..), idTermFold,
19      pprTerm, cPprTerm, cPprTermBase, CustomTermPrinter,
20
21 --     unsafeDeepSeq,
22
23      Closure(..), getClosureData, ClosureType(..), isConstr, isIndirection,
24
25      sigmaType
26  ) where
27
28 #include "HsVersions.h"
29
30 import ByteCodeItbls    ( StgInfoTable )
31 import qualified ByteCodeItbls as BCI( StgInfoTable(..) )
32 import HscTypes
33 import Linker
34
35 import DataCon
36 import Type
37 import TypeRep         -- I know I know, this is cheating
38 import Var
39 import TcRnMonad
40 import TcType
41 import TcMType
42 import TcUnify
43 import TcEnv
44
45 import TyCon
46 import Name
47 import VarEnv
48 import Util
49 import ListSetOps
50 import VarSet
51 import TysPrim
52 import PrelNames
53 import TysWiredIn
54 import DynFlags
55 import Outputable
56 import FastString
57 -- import Panic
58
59 import Constants        ( wORD_SIZE )
60
61 import GHC.Arr          ( Array(..) )
62 import GHC.Exts
63
64 #if __GLASGOW_HASKELL__ >= 611
65 import GHC.IO ( IO(..) )
66 #else
67 import GHC.IOBase ( IO(..) )
68 #endif
69
70 import Control.Monad
71 import Data.Maybe
72 import Data.Array.Base
73 import Data.Ix
74 import Data.List
75 import qualified Data.Sequence as Seq
76 import Data.Monoid
77 import Data.Sequence (viewl, ViewL(..))
78 import Foreign
79 -- import System.IO.Unsafe
80
81 ---------------------------------------------
82 -- * A representation of semi evaluated Terms
83 ---------------------------------------------
84
85 data Term = Term { ty        :: RttiType
86                  , dc        :: Either String DataCon
87                                -- Carries a text representation if the datacon is
88                                -- not exported by the .hi file, which is the case 
89                                -- for private constructors in -O0 compiled libraries
90                  , val       :: HValue 
91                  , subTerms  :: [Term] }
92
93           | Prim { ty        :: RttiType
94                  , value     :: [Word] }
95
96           | Suspension { ctype    :: ClosureType
97                        , ty       :: RttiType
98                        , val      :: HValue
99                        , bound_to :: Maybe Name   -- Useful for printing
100                        }
101           | NewtypeWrap{       -- At runtime there are no newtypes, and hence no
102                                -- newtype constructors. A NewtypeWrap is just a
103                                -- made-up tag saying "heads up, there used to be
104                                -- a newtype constructor here".
105                          ty           :: RttiType
106                        , dc           :: Either String DataCon
107                        , wrapped_term :: Term }
108           | RefWrap    {       -- The contents of a reference
109                          ty           :: RttiType
110                        , wrapped_term :: Term }
111
112 isTerm, isSuspension, isPrim, isFun, isFunLike, isNewtypeWrap :: Term -> Bool
113 isTerm Term{} = True
114 isTerm   _    = False
115 isSuspension Suspension{} = True
116 isSuspension      _       = False
117 isPrim Prim{} = True
118 isPrim   _    = False
119 isNewtypeWrap NewtypeWrap{} = True
120 isNewtypeWrap _             = False
121
122 isFun Suspension{ctype=Fun} = True
123 isFun _ = False
124
125 isFunLike s@Suspension{ty=ty} = isFun s || isFunTy ty
126 isFunLike _ = False
127
128 termType :: Term -> RttiType
129 termType t = ty t
130
131 isFullyEvaluatedTerm :: Term -> Bool
132 isFullyEvaluatedTerm Term {subTerms=tt} = all isFullyEvaluatedTerm tt
133 isFullyEvaluatedTerm Prim {}            = True
134 isFullyEvaluatedTerm NewtypeWrap{wrapped_term=t} = isFullyEvaluatedTerm t
135 isFullyEvaluatedTerm RefWrap{wrapped_term=t}     = isFullyEvaluatedTerm t
136 isFullyEvaluatedTerm _                  = False
137
138 instance Outputable (Term) where
139  ppr t | Just doc <- cPprTerm cPprTermBase t = doc
140        | otherwise = panic "Outputable Term instance"
141
142 -------------------------------------------------------------------------
143 -- Runtime Closure Datatype and functions for retrieving closure related stuff
144 -------------------------------------------------------------------------
145 data ClosureType = Constr 
146                  | Fun 
147                  | Thunk Int 
148                  | ThunkSelector
149                  | Blackhole 
150                  | AP 
151                  | PAP 
152                  | Indirection Int 
153                  | MutVar Int
154                  | MVar   Int
155                  | Other  Int
156  deriving (Show, Eq)
157
158 data Closure = Closure { tipe         :: ClosureType 
159                        , infoPtr      :: Ptr ()
160                        , infoTable    :: StgInfoTable
161                        , ptrs         :: Array Int HValue
162                        , nonPtrs      :: [Word]
163                        }
164
165 instance Outputable ClosureType where
166   ppr = text . show 
167
168 #include "../includes/rts/storage/ClosureTypes.h"
169
170 aP_CODE, pAP_CODE :: Int
171 aP_CODE = AP
172 pAP_CODE = PAP
173 #undef AP
174 #undef PAP
175
176 getClosureData :: a -> IO Closure
177 getClosureData a =
178    case unpackClosure# a of 
179      (# iptr, ptrs, nptrs #) -> do
180            let iptr'
181                 | ghciTablesNextToCode =
182                    Ptr iptr
183                 | otherwise =
184                    -- the info pointer we get back from unpackClosure#
185                    -- is to the beginning of the standard info table,
186                    -- but the Storable instance for info tables takes
187                    -- into account the extra entry pointer when
188                    -- !ghciTablesNextToCode, so we must adjust here:
189                    Ptr iptr `plusPtr` negate wORD_SIZE
190            itbl <- peek iptr'
191            let tipe = readCType (BCI.tipe itbl)
192                elems = fromIntegral (BCI.ptrs itbl)
193                ptrsList = Array 0 (elems - 1) elems ptrs
194                nptrs_data = [W# (indexWordArray# nptrs i)
195                               | I# i <- [0.. fromIntegral (BCI.nptrs itbl)] ]
196            ASSERT(elems >= 0) return ()
197            ptrsList `seq` 
198             return (Closure tipe (Ptr iptr) itbl ptrsList nptrs_data)
199
200 readCType :: Integral a => a -> ClosureType
201 readCType i 
202  | i >= CONSTR && i <= CONSTR_NOCAF_STATIC = Constr
203  | i >= FUN    && i <= FUN_STATIC          = Fun
204  | i >= THUNK  && i < THUNK_SELECTOR       = Thunk i'
205  | i == THUNK_SELECTOR                     = ThunkSelector
206  | i == BLACKHOLE                          = Blackhole
207  | i >= IND    && i <= IND_STATIC          = Indirection i'
208  | i' == aP_CODE                           = AP
209  | i == AP_STACK                           = AP
210  | i' == pAP_CODE                          = PAP
211  | i == MUT_VAR_CLEAN || i == MUT_VAR_DIRTY= MutVar i'
212  | i == MVAR_CLEAN    || i == MVAR_DIRTY   = MVar i'
213  | otherwise                               = Other  i'
214   where i' = fromIntegral i
215  
216 isConstr, isIndirection, isThunk :: ClosureType -> Bool
217 isConstr Constr = True
218 isConstr    _   = False
219
220 isIndirection (Indirection _) = True
221 isIndirection _ = False
222
223 isThunk (Thunk _)     = True
224 isThunk ThunkSelector = True
225 isThunk AP            = True
226 isThunk _             = False
227
228 isFullyEvaluated :: a -> IO Bool
229 isFullyEvaluated a = do 
230   closure <- getClosureData a 
231   case tipe closure of
232     Constr -> do are_subs_evaluated <- amapM isFullyEvaluated (ptrs closure)
233                  return$ and are_subs_evaluated
234     _      -> return False
235   where amapM f = sequence . amap' f
236
237 -- TODO: Fix it. Probably the otherwise case is failing, trace/debug it
238 {-
239 unsafeDeepSeq :: a -> b -> b
240 unsafeDeepSeq = unsafeDeepSeq1 2
241  where unsafeDeepSeq1 0 a b = seq a $! b
242        unsafeDeepSeq1 i a b   -- 1st case avoids infinite loops for non reducible thunks
243         | not (isConstr tipe) = seq a $! unsafeDeepSeq1 (i-1) a b     
244      -- | unsafePerformIO (isFullyEvaluated a) = b
245         | otherwise = case unsafePerformIO (getClosureData a) of
246                         closure -> foldl' (flip unsafeDeepSeq) b (ptrs closure)
247         where tipe = unsafePerformIO (getClosureType a)
248 -}
249
250 -----------------------------------
251 -- * Traversals for Terms
252 -----------------------------------
253 type TermProcessor a b = RttiType -> Either String DataCon -> HValue -> [a] -> b
254
255 data TermFold a = TermFold { fTerm        :: TermProcessor a a
256                            , fPrim        :: RttiType -> [Word] -> a
257                            , fSuspension  :: ClosureType -> RttiType -> HValue
258                                             -> Maybe Name -> a
259                            , fNewtypeWrap :: RttiType -> Either String DataCon
260                                             -> a -> a
261                            , fRefWrap     :: RttiType -> a -> a
262                            }
263
264
265 data TermFoldM m a =
266                    TermFoldM {fTermM        :: TermProcessor a (m a)
267                             , fPrimM        :: RttiType -> [Word] -> m a
268                             , fSuspensionM  :: ClosureType -> RttiType -> HValue
269                                              -> Maybe Name -> m a
270                             , fNewtypeWrapM :: RttiType -> Either String DataCon
271                                             -> a -> m a
272                             , fRefWrapM     :: RttiType -> a -> m a
273                            }
274
275 foldTerm :: TermFold a -> Term -> a
276 foldTerm tf (Term ty dc v tt) = fTerm tf ty dc v (map (foldTerm tf) tt)
277 foldTerm tf (Prim ty    v   ) = fPrim tf ty v
278 foldTerm tf (Suspension ct ty v b) = fSuspension tf ct ty v b
279 foldTerm tf (NewtypeWrap ty dc t)  = fNewtypeWrap tf ty dc (foldTerm tf t)
280 foldTerm tf (RefWrap ty t)         = fRefWrap tf ty (foldTerm tf t)
281
282
283 foldTermM :: Monad m => TermFoldM m a -> Term -> m a
284 foldTermM tf (Term ty dc v tt) = mapM (foldTermM tf) tt >>= fTermM tf ty dc v
285 foldTermM tf (Prim ty    v   ) = fPrimM tf ty v
286 foldTermM tf (Suspension ct ty v b) = fSuspensionM tf ct ty v b
287 foldTermM tf (NewtypeWrap ty dc t)  = foldTermM tf t >>=  fNewtypeWrapM tf ty dc
288 foldTermM tf (RefWrap ty t)         = foldTermM tf t >>= fRefWrapM tf ty
289
290 idTermFold :: TermFold Term
291 idTermFold = TermFold {
292               fTerm = Term,
293               fPrim = Prim,
294               fSuspension  = Suspension,
295               fNewtypeWrap = NewtypeWrap,
296               fRefWrap = RefWrap
297                       }
298
299 mapTermType :: (RttiType -> Type) -> Term -> Term
300 mapTermType f = foldTerm idTermFold {
301           fTerm       = \ty dc hval tt -> Term (f ty) dc hval tt,
302           fSuspension = \ct ty hval n ->
303                           Suspension ct (f ty) hval n,
304           fNewtypeWrap= \ty dc t -> NewtypeWrap (f ty) dc t,
305           fRefWrap    = \ty t -> RefWrap (f ty) t}
306
307 mapTermTypeM :: Monad m =>  (RttiType -> m Type) -> Term -> m Term
308 mapTermTypeM f = foldTermM TermFoldM {
309           fTermM       = \ty dc hval tt -> f ty >>= \ty' -> return $ Term ty'  dc hval tt,
310           fPrimM       = (return.) . Prim,
311           fSuspensionM = \ct ty hval n ->
312                           f ty >>= \ty' -> return $ Suspension ct ty' hval n,
313           fNewtypeWrapM= \ty dc t -> f ty >>= \ty' -> return $ NewtypeWrap ty' dc t,
314           fRefWrapM    = \ty t -> f ty >>= \ty' -> return $ RefWrap ty' t}
315
316 termTyVars :: Term -> TyVarSet
317 termTyVars = foldTerm TermFold {
318             fTerm       = \ty _ _ tt   -> 
319                           tyVarsOfType ty `plusVarEnv` concatVarEnv tt,
320             fSuspension = \_ ty _ _ -> tyVarsOfType ty,
321             fPrim       = \ _ _ -> emptyVarEnv,
322             fNewtypeWrap= \ty _ t -> tyVarsOfType ty `plusVarEnv` t,
323             fRefWrap    = \ty t -> tyVarsOfType ty `plusVarEnv` t}
324     where concatVarEnv = foldr plusVarEnv emptyVarEnv
325
326 ----------------------------------
327 -- Pretty printing of terms
328 ----------------------------------
329
330 type Precedence        = Int
331 type TermPrinter       = Precedence -> Term ->   SDoc
332 type TermPrinterM m    = Precedence -> Term -> m SDoc
333
334 app_prec,cons_prec, max_prec ::Int
335 max_prec  = 10
336 app_prec  = max_prec
337 cons_prec = 5 -- TODO Extract this info from GHC itself
338
339 pprTerm :: TermPrinter -> TermPrinter
340 pprTerm y p t | Just doc <- pprTermM (\p -> Just . y p) p t = doc
341 pprTerm _ _ _ = panic "pprTerm"
342
343 pprTermM, ppr_termM, pprNewtypeWrap :: Monad m => TermPrinterM m -> TermPrinterM m
344 pprTermM y p t = pprDeeper `liftM` ppr_termM y p t
345
346 ppr_termM y p Term{dc=Left dc_tag, subTerms=tt} = do
347   tt_docs <- mapM (y app_prec) tt
348   return$ cparen (not(null tt) && p >= app_prec) (text dc_tag <+> pprDeeperList fsep tt_docs)
349   
350 ppr_termM y p Term{dc=Right dc, subTerms=tt} 
351 {-  | dataConIsInfix dc, (t1:t2:tt') <- tt  --TODO fixity
352   = parens (ppr_term1 True t1 <+> ppr dc <+> ppr_term1 True ppr t2) 
353     <+> hsep (map (ppr_term1 True) tt) 
354 -} -- TODO Printing infix constructors properly
355   | null tt   = return$ ppr dc
356   | otherwise = do
357          tt_docs <- mapM (y app_prec) tt
358          return$ cparen (p >= app_prec) (ppr dc <+> pprDeeperList fsep tt_docs)
359
360 ppr_termM y p t@NewtypeWrap{} = pprNewtypeWrap y p t
361 ppr_termM y p RefWrap{wrapped_term=t}  = do
362   contents <- y app_prec t
363   return$ cparen (p >= app_prec) (text "GHC.Prim.MutVar#" <+> contents)
364   -- The constructor name is wired in here ^^^ for the sake of simplicity.
365   -- I don't think mutvars are going to change in a near future.
366   -- In any case this is solely a presentation matter: MutVar# is
367   -- a datatype with no constructors, implemented by the RTS
368   -- (hence there is no way to obtain a datacon and print it).
369 ppr_termM _ _ t = ppr_termM1 t
370
371
372 ppr_termM1 :: Monad m => Term -> m SDoc
373 ppr_termM1 Prim{value=words, ty=ty} = 
374     return$ text$ repPrim (tyConAppTyCon ty) words
375 ppr_termM1 Suspension{ty=ty, bound_to=Nothing} = 
376     return (char '_' <+> ifPprDebug (text "::" <> ppr ty))
377 ppr_termM1 Suspension{ty=ty, bound_to=Just n}
378 --  | Just _ <- splitFunTy_maybe ty = return$ ptext (sLit("<function>")
379   | otherwise = return$ parens$ ppr n <> text "::" <> ppr ty
380 ppr_termM1 Term{}        = panic "ppr_termM1 - Term"
381 ppr_termM1 RefWrap{}     = panic "ppr_termM1 - RefWrap"
382 ppr_termM1 NewtypeWrap{} = panic "ppr_termM1 - NewtypeWrap"
383
384 pprNewtypeWrap y p NewtypeWrap{ty=ty, wrapped_term=t}
385   | Just (tc,_) <- tcSplitTyConApp_maybe ty
386   , ASSERT(isNewTyCon tc) True
387   , Just new_dc <- tyConSingleDataCon_maybe tc = do 
388              real_term <- y max_prec t
389              return $ cparen (p >= app_prec) (ppr new_dc <+> real_term)
390 pprNewtypeWrap _ _ _ = panic "pprNewtypeWrap"
391
392 -------------------------------------------------------
393 -- Custom Term Pretty Printers
394 -------------------------------------------------------
395
396 -- We can want to customize the representation of a 
397 --  term depending on its type. 
398 -- However, note that custom printers have to work with
399 --  type representations, instead of directly with types.
400 -- We cannot use type classes here, unless we employ some 
401 --  typerep trickery (e.g. Weirich's RepLib tricks),
402 --  which I didn't. Therefore, this code replicates a lot
403 --  of what type classes provide for free.
404
405 type CustomTermPrinter m = TermPrinterM m
406                          -> [Precedence -> Term -> (m (Maybe SDoc))]
407
408 -- | Takes a list of custom printers with a explicit recursion knot and a term, 
409 -- and returns the output of the first succesful printer, or the default printer
410 cPprTerm :: Monad m => CustomTermPrinter m -> Term -> m SDoc
411 cPprTerm printers_ = go 0 where
412   printers = printers_ go
413   go prec t = do
414     let default_ = Just `liftM` pprTermM go prec t
415         mb_customDocs = [pp prec t | pp <- printers] ++ [default_]
416     Just doc <- firstJustM mb_customDocs
417     return$ cparen (prec>app_prec+1) doc
418
419   firstJustM (mb:mbs) = mb >>= maybe (firstJustM mbs) (return . Just)
420   firstJustM [] = return Nothing
421
422 -- Default set of custom printers. Note that the recursion knot is explicit
423 cPprTermBase :: Monad m => CustomTermPrinter m
424 cPprTermBase y =
425   [ ifTerm (isTupleTy.ty) (\_p -> liftM (parens . hcat . punctuate comma) 
426                                       . mapM (y (-1))
427                                       . subTerms)
428   , ifTerm (\t -> isTyCon listTyCon (ty t) && subTerms t `lengthIs` 2)
429            (\ p Term{subTerms=[h,t]} -> doList p h t)
430   , ifTerm (isTyCon intTyCon    . ty) (coerceShow$ \(a::Int)->a)
431   , ifTerm (isTyCon charTyCon   . ty) (coerceShow$ \(a::Char)->a)
432   , ifTerm (isTyCon floatTyCon  . ty) (coerceShow$ \(a::Float)->a)
433   , ifTerm (isTyCon doubleTyCon . ty) (coerceShow$ \(a::Double)->a)
434   , ifTerm (isIntegerTy         . ty) (coerceShow$ \(a::Integer)->a)
435   ]
436      where ifTerm pred f prec t@Term{}
437                | pred t    = Just `liftM` f prec t
438            ifTerm _ _ _ _  = return Nothing
439
440            isTupleTy ty    = fromMaybe False $ do 
441              (tc,_) <- tcSplitTyConApp_maybe ty 
442              return (isBoxedTupleTyCon tc)
443
444            isTyCon a_tc ty = fromMaybe False $ do 
445              (tc,_) <- tcSplitTyConApp_maybe ty
446              return (a_tc == tc)
447
448            isIntegerTy ty = fromMaybe False $ do
449              (tc,_) <- tcSplitTyConApp_maybe ty
450              return (tyConName tc == integerTyConName)
451
452            coerceShow f _p = return . text . show . f . unsafeCoerce# . val
453
454            --Note pprinting of list terms is not lazy
455            doList p h t = do
456                let elems      = h : getListTerms t
457                    isConsLast = not(termType(last elems) `coreEqType` termType h)
458                print_elems <- mapM (y cons_prec) elems
459                return$ if isConsLast
460                      then cparen (p >= cons_prec) 
461                         . pprDeeperList fsep 
462                         . punctuate (space<>colon)
463                         $ print_elems
464                      else brackets (pprDeeperList fcat$
465                                          punctuate comma print_elems)
466
467                 where getListTerms Term{subTerms=[h,t]} = h : getListTerms t
468                       getListTerms Term{subTerms=[]}    = []
469                       getListTerms t@Suspension{}       = [t]
470                       getListTerms t = pprPanic "getListTerms" (ppr t)
471
472
473 repPrim :: TyCon -> [Word] -> String
474 repPrim t = rep where 
475    rep x
476     | t == charPrimTyCon   = show (build x :: Char)
477     | t == intPrimTyCon    = show (build x :: Int)
478     | t == wordPrimTyCon   = show (build x :: Word)
479     | t == floatPrimTyCon  = show (build x :: Float)
480     | t == doublePrimTyCon = show (build x :: Double)
481     | t == int32PrimTyCon  = show (build x :: Int32)
482     | t == word32PrimTyCon = show (build x :: Word32)
483     | t == int64PrimTyCon  = show (build x :: Int64)
484     | t == word64PrimTyCon = show (build x :: Word64)
485     | t == addrPrimTyCon   = show (nullPtr `plusPtr` build x)
486     | t == stablePtrPrimTyCon  = "<stablePtr>"
487     | t == stableNamePrimTyCon = "<stableName>"
488     | t == statePrimTyCon      = "<statethread>"
489     | t == realWorldTyCon      = "<realworld>"
490     | t == threadIdPrimTyCon   = "<ThreadId>"
491     | t == weakPrimTyCon       = "<Weak>"
492     | t == arrayPrimTyCon      = "<array>"
493     | t == byteArrayPrimTyCon  = "<bytearray>"
494     | t == mutableArrayPrimTyCon = "<mutableArray>"
495     | t == mutableByteArrayPrimTyCon = "<mutableByteArray>"
496     | t == mutVarPrimTyCon= "<mutVar>"
497     | t == mVarPrimTyCon  = "<mVar>"
498     | t == tVarPrimTyCon  = "<tVar>"
499     | otherwise = showSDoc (char '<' <> ppr t <> char '>')
500     where build ww = unsafePerformIO $ withArray ww (peek . castPtr) 
501 --   This ^^^ relies on the representation of Haskell heap values being 
502 --   the same as in a C array. 
503
504 -----------------------------------
505 -- Type Reconstruction
506 -----------------------------------
507 {-
508 Type Reconstruction is type inference done on heap closures.
509 The algorithm walks the heap generating a set of equations, which
510 are solved with syntactic unification.
511 A type reconstruction equation looks like:
512
513   <datacon reptype>  =  <actual heap contents> 
514
515 The full equation set is generated by traversing all the subterms, starting
516 from a given term.
517
518 The only difficult part is that newtypes are only found in the lhs of equations.
519 Right hand sides are missing them. We can either (a) drop them from the lhs, or 
520 (b) reconstruct them in the rhs when possible. 
521
522 The function congruenceNewtypes takes a shot at (b)
523 -}
524
525
526 -- A (non-mutable) tau type containing
527 -- existentially quantified tyvars.
528 --    (since GHC type language currently does not support
529 --     existentials, we leave these variables unquantified)
530 type RttiType = Type
531
532 -- An incomplete type as stored in GHCi:
533 --  no polymorphism: no quantifiers & all tyvars are skolem.
534 type GhciType = Type
535
536
537 -- The Type Reconstruction monad
538 --------------------------------
539 type TR a = TcM a
540
541 runTR :: HscEnv -> TR a -> IO a
542 runTR hsc_env thing = do
543   mb_val <- runTR_maybe hsc_env thing
544   case mb_val of
545     Nothing -> error "unable to :print the term"
546     Just x  -> return x
547
548 runTR_maybe :: HscEnv -> TR a -> IO (Maybe a)
549 runTR_maybe hsc_env = fmap snd . initTc hsc_env HsSrcFile False  iNTERACTIVE
550
551 traceTR :: SDoc -> TR ()
552 traceTR = liftTcM . traceOptTcRn Opt_D_dump_rtti
553
554
555 -- Semantically different to recoverM in TcRnMonad 
556 -- recoverM retains the errors in the first action,
557 --  whereas recoverTc here does not
558 recoverTR :: TR a -> TR a -> TR a
559 recoverTR recover thing = do 
560   (_,mb_res) <- tryTcErrs thing
561   case mb_res of 
562     Nothing  -> recover
563     Just res -> return res
564
565 trIO :: IO a -> TR a 
566 trIO = liftTcM . liftIO
567
568 liftTcM :: TcM a -> TR a
569 liftTcM = id
570
571 newVar :: Kind -> TR TcType
572 newVar = liftTcM . liftM mkTyVarTy . newBoxyTyVar
573
574 -- | Returns the instantiated type scheme ty', and the substitution sigma 
575 --   such that sigma(ty') = ty 
576 instScheme :: Type -> TR (TcType, TvSubst)
577 instScheme ty = liftTcM$ do
578    (tvs, _, _)      <- tcInstType return ty
579    (tvs',_,ty') <- tcInstType (mapM tcInstTyVar) ty
580    return (ty', zipTopTvSubst tvs' (mkTyVarTys tvs))
581
582 -- Adds a constraint of the form t1 == t2
583 -- t1 is expected to come from walking the heap
584 -- t2 is expected to come from a datacon signature
585 -- Before unification, congruenceNewtypes needs to
586 -- do its magic.
587 addConstraint :: TcType -> TcType -> TR ()
588 addConstraint actual expected = do
589     traceTR (text "add constraint:" <+> fsep [ppr actual, equals, ppr expected])
590     recoverTR (traceTR $ fsep [text "Failed to unify", ppr actual,
591                                     text "with", ppr expected])
592               (congruenceNewtypes actual expected >>=
593                            (getLIE . uncurry boxyUnify) >> return ())
594      -- TOMDO: what about the coercion?
595      -- we should consider family instances
596
597
598 -- Type & Term reconstruction
599 ------------------------------
600 cvObtainTerm :: HscEnv -> Int -> Bool -> RttiType -> HValue -> IO Term
601 cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
602   -- we quantify existential tyvars as universal,
603   -- as this is needed to be able to manipulate
604   -- them properly
605    let sigma_old_ty = sigmaType old_ty
606    traceTR (text "Term reconstruction started with initial type " <> ppr old_ty)
607    term <-
608      if isMonomorphic sigma_old_ty
609       then do
610         new_ty <- go max_depth sigma_old_ty sigma_old_ty hval >>= zonkTerm
611         return $ fixFunDictionaries $ expandNewtypes new_ty
612       else do
613               (old_ty', rev_subst) <- instScheme sigma_old_ty
614               my_ty <- newVar argTypeKind
615               when (check1 sigma_old_ty) (traceTR (text "check1 passed") >>
616                                           addConstraint my_ty old_ty')
617               term  <- go max_depth my_ty sigma_old_ty hval
618               zterm <- zonkTerm term
619               let new_ty = termType zterm
620               if isMonomorphic new_ty || check2 (sigmaType new_ty) sigma_old_ty
621                  then do
622                       traceTR (text "check2 passed")
623                       addConstraint (termType term) old_ty'
624                       zterm' <- zonkTerm term
625                       return ((fixFunDictionaries . expandNewtypes . mapTermType (substTy rev_subst)) zterm')
626                  else do
627                       traceTR (text "check2 failed" <+> parens
628                                        (ppr zterm <+> text "::" <+> ppr new_ty))
629                       -- we have unsound types. Replace constructor types in
630                       -- subterms with tyvars
631                       zterm' <- mapTermTypeM
632                                  (\ty -> case tcSplitTyConApp_maybe ty of
633                                            Just (tc, _:_) | tc /= funTyCon
634                                                -> newVar argTypeKind
635                                            _   -> return ty)
636                                  zterm
637                       zonkTerm zterm'
638    traceTR (text "Term reconstruction completed." $$
639             text "Term obtained: " <> ppr term $$
640             text "Type obtained: " <> ppr (termType term))
641    return term
642     where 
643   go :: Int -> Type -> Type -> HValue -> TcM Term
644   go max_depth _ _ _ | seq max_depth False = undefined
645   go 0 my_ty _old_ty a = do
646     traceTR (text "Gave up reconstructing a term after" <>
647                   int max_depth <> text " steps")
648     clos <- trIO $ getClosureData a
649     return (Suspension (tipe clos) my_ty a Nothing)
650   go max_depth my_ty old_ty a = do
651     let monomorphic = not(isTyVarTy my_ty)   
652     -- This ^^^ is a convention. The ancestor tests for
653     -- monomorphism and passes a type instead of a tv
654     clos <- trIO $ getClosureData a
655     case tipe clos of
656 -- Thunks we may want to force
657 -- NB. this won't attempt to force a BLACKHOLE.  Even with :force, we never
658 -- force blackholes, because it would almost certainly result in deadlock,
659 -- and showing the '_' is more useful.
660       t | isThunk t && force -> traceTR (text "Forcing a " <> text (show t)) >>
661                                 seq a (go (pred max_depth) my_ty old_ty a)
662 -- We always follow indirections
663       Indirection i -> do traceTR (text "Following an indirection" <> parens (int i) )
664                           go max_depth my_ty old_ty $! (ptrs clos ! 0)
665 -- We also follow references
666       MutVar _ | Just (tycon,[world,contents_ty]) <- tcSplitTyConApp_maybe old_ty
667              -> do
668                   -- Deal with the MutVar# primitive
669                   -- It does not have a constructor at all, 
670                   -- so we simulate the following one
671                   -- MutVar# :: contents_ty -> MutVar# s contents_ty
672          traceTR (text "Following a MutVar")
673          contents_tv <- newVar liftedTypeKind
674          contents <- trIO$ IO$ \w -> readMutVar# (unsafeCoerce# a) w
675          ASSERT(isUnliftedTypeKind $ typeKind my_ty) return ()
676          (mutvar_ty,_) <- instScheme $ sigmaType $ mkFunTy 
677                             contents_ty (mkTyConApp tycon [world,contents_ty])
678          addConstraint (mkFunTy contents_tv my_ty) mutvar_ty
679          x <- go (pred max_depth) contents_tv contents_ty contents
680          return (RefWrap my_ty x)
681
682  -- The interesting case
683       Constr -> do
684         traceTR (text "entering a constructor " <>
685                       if monomorphic
686                         then parens (text "already monomorphic: " <> ppr my_ty)
687                         else Outputable.empty)
688         Right dcname <- dataConInfoPtrToName (infoPtr clos)
689         (_,mb_dc)    <- tryTcErrs (tcLookupDataCon dcname)
690         case mb_dc of
691           Nothing -> do -- This can happen for private constructors compiled -O0
692                         -- where the .hi descriptor does not export them
693                         -- In such case, we return a best approximation:
694                         --  ignore the unpointed args, and recover the pointeds
695                         -- This preserves laziness, and should be safe.
696                        let tag = showSDoc (ppr dcname)
697                        vars     <- replicateM (length$ elems$ ptrs clos) 
698                                               (newVar (liftedTypeKind))
699                        subTerms <- sequence [appArr (go (pred max_depth) tv tv) (ptrs clos) i 
700                                               | (i, tv) <- zip [0..] vars]
701                        return (Term my_ty (Left ('<' : tag ++ ">")) a subTerms)
702           Just dc -> do
703             let subTtypes  = matchSubTypes dc old_ty
704             subTermTvs    <- mapMif (not . isMonomorphic)
705                                     (\t -> newVar (typeKind t))
706                                     subTtypes
707             let (subTermsP, subTermsNP) = partition (\(ty,_) -> isLifted ty
708                                                              || isRefType ty)
709                                                     (zip subTtypes subTermTvs)
710                 (subTtypesP,   subTermTvsP ) = unzip subTermsP
711                 (subTtypesNP, _subTermTvsNP) = unzip subTermsNP
712
713             -- When we already have all the information, avoid solving
714             -- unnecessary constraints. Propagation of type information
715             -- to subterms is already being done via matching.
716             when (not monomorphic) $ do
717                let myType = mkFunTys subTermTvs my_ty
718                (signatureType,_) <- instScheme (mydataConType dc)
719             -- It is vital for newtype reconstruction that the unification step
720             -- is done right here, _before_ the subterms are RTTI reconstructed
721                addConstraint myType signatureType
722             subTermsP <- sequence
723                   [ appArr (go (pred max_depth) tv t) (ptrs clos) i
724                    | (i,tv,t) <- zip3 [0..] subTermTvsP subTtypesP]
725             let unboxeds   = extractUnboxed subTtypesNP clos
726                 subTermsNP = map (uncurry Prim) (zip subTtypesNP unboxeds)
727                 subTerms   = reOrderTerms subTermsP subTermsNP subTtypes
728             return (Term my_ty (Right dc) a subTerms)
729 -- The otherwise case: can be a Thunk,AP,PAP,etc.
730       tipe_clos ->
731          return (Suspension tipe_clos my_ty a Nothing)
732
733   matchSubTypes dc ty
734     | ty' <- repType ty     -- look through newtypes
735     , Just (tc,ty_args) <- tcSplitTyConApp_maybe ty'
736     , dc `elem` tyConDataCons tc
737       -- It is necessary to check that dc is actually a constructor for tycon tc,
738       -- because it may be the case that tc is a recursive newtype and tcSplitTyConApp
739       -- has not removed it. In that case, we happily give up and don't match
740     = myDataConInstArgTys dc ty_args
741     | otherwise = dataConRepArgTys dc
742
743   -- put together pointed and nonpointed subterms in the
744   --  correct order.
745   reOrderTerms _ _ [] = []
746   reOrderTerms pointed unpointed (ty:tys) 
747    | isLifted ty || isRefType ty
748                   = ASSERT2(not(null pointed)
749                             , ptext (sLit "reOrderTerms") $$ 
750                                         (ppr pointed $$ ppr unpointed))
751                     let (t:tt) = pointed in t : reOrderTerms tt unpointed tys
752    | otherwise    = ASSERT2(not(null unpointed)
753                            , ptext (sLit "reOrderTerms") $$ 
754                                        (ppr pointed $$ ppr unpointed))
755                     let (t:tt) = unpointed in t : reOrderTerms pointed tt tys
756
757   -- insert NewtypeWraps around newtypes
758   expandNewtypes = foldTerm idTermFold { fTerm = worker } where
759    worker ty dc hval tt
760      | Just (tc, args) <- tcSplitTyConApp_maybe ty
761      , isNewTyCon tc
762      , wrapped_type    <- newTyConInstRhs tc args
763      , Just dc'        <- tyConSingleDataCon_maybe tc
764      , t'              <- worker wrapped_type dc hval tt
765      = NewtypeWrap ty (Right dc') t'
766      | otherwise = Term ty dc hval tt
767
768
769    -- Avoid returning types where predicates have been expanded to dictionaries.
770   fixFunDictionaries = foldTerm idTermFold {fSuspension = worker} where
771       worker ct ty hval n | isFunTy ty = Suspension ct (dictsView ty) hval n
772                           | otherwise  = Suspension ct ty hval n
773
774
775 -- Fast, breadth-first Type reconstruction
776 ------------------------------------------
777 cvReconstructType :: HscEnv -> Int -> GhciType -> HValue -> IO (Maybe Type)
778 cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
779    traceTR (text "RTTI started with initial type " <> ppr old_ty)
780    let sigma_old_ty = sigmaType old_ty
781    new_ty <-
782        if isMonomorphic sigma_old_ty
783         then return old_ty
784         else do
785           (old_ty', rev_subst) <- instScheme sigma_old_ty
786           my_ty <- newVar argTypeKind
787           when (check1 sigma_old_ty) (traceTR (text "check1 passed") >>
788                                       addConstraint my_ty old_ty')
789           search (isMonomorphic `fmap` zonkTcType my_ty)
790                  (\(ty,a) -> go ty a)
791                  (Seq.singleton (my_ty, hval))
792                  max_depth
793           new_ty <- zonkTcType my_ty
794           if isMonomorphic new_ty || check2 (sigmaType new_ty) sigma_old_ty
795             then do
796                  traceTR (text "check2 passed")
797                  addConstraint my_ty old_ty'
798                  new_ty' <- zonkTcType my_ty
799                  return (substTy rev_subst new_ty')
800             else traceTR (text "check2 failed" <+> parens (ppr new_ty)) >>
801                  return old_ty
802    traceTR (text "RTTI completed. Type obtained:" <+> ppr new_ty)
803    return new_ty
804     where
805 --  search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m ()
806   search _ _ _ 0 = traceTR (text "Failed to reconstruct a type after " <>
807                                 int max_depth <> text " steps")
808   search stop expand l d =
809     case viewl l of 
810       EmptyL  -> return ()
811       x :< xx -> unlessM stop $ do
812                   new <- expand x
813                   search stop expand (xx `mappend` Seq.fromList new) $! (pred d)
814
815    -- returns unification tasks,since we are going to want a breadth-first search
816   go :: Type -> HValue -> TR [(Type, HValue)]
817   go my_ty a = do
818     clos <- trIO $ getClosureData a
819     case tipe clos of
820       Indirection _ -> go my_ty $! (ptrs clos ! 0)
821       MutVar _ -> do
822          contents <- trIO$ IO$ \w -> readMutVar# (unsafeCoerce# a) w
823          tv'   <- newVar liftedTypeKind
824          world <- newVar liftedTypeKind
825          addConstraint my_ty (mkTyConApp mutVarPrimTyCon [world,tv'])
826          return [(tv', contents)]
827       Constr -> do
828         Right dcname <- dataConInfoPtrToName (infoPtr clos)
829         (_,mb_dc)    <- tryTcErrs (tcLookupDataCon dcname)
830         case mb_dc of
831           Nothing-> do
832                      --  TODO: Check this case
833             forM [0..length (elems $ ptrs clos)] $ \i -> do
834                         tv <- newVar liftedTypeKind
835                         return$ appArr (\e->(tv,e)) (ptrs clos) i
836
837           Just dc -> do
838             subTtypes <- mapMif (not . isMonomorphic)
839                                 (\t -> newVar (typeKind t))
840                                 (dataConRepArgTys dc)
841
842             -- It is vital for newtype reconstruction that the unification step
843             -- is done right here, _before_ the subterms are RTTI reconstructed
844             let myType         = mkFunTys subTtypes my_ty
845             (signatureType,_) <- instScheme(mydataConType dc)
846             addConstraint myType signatureType
847             return $ [ appArr (\e->(t,e)) (ptrs clos) i
848                        | (i,t) <- zip [0..] (filter (isLifted |.| isRefType) subTtypes)]
849       _ -> return []
850
851 -- Compute the difference between a base type and the type found by RTTI
852 -- improveType <base_type> <rtti_type>
853 -- The types can contain skolem type variables, which need to be treated as normal vars.
854 -- In particular, we want them to unify with things.
855 improveRTTIType :: HscEnv -> RttiType -> RttiType -> IO (Maybe TvSubst)
856 improveRTTIType hsc_env _ty rtti_ty = runTR_maybe hsc_env $ do
857     traceTR (text "improveRttiType" <+> fsep [ppr _ty, ppr rtti_ty])
858     (ty_tvs,  _, _)   <- tcInstType return ty
859     (ty_tvs', _, ty') <- tcInstType (mapM tcInstTyVar) ty
860     (_, _, rtti_ty')  <- tcInstType (mapM tcInstTyVar) (sigmaType rtti_ty)
861     _ <- getLIE(boxyUnify rtti_ty' ty')
862     tvs1_contents     <- zonkTcTyVars ty_tvs'
863     let subst = (uncurry zipTopTvSubst . unzip)
864                  [(tv,ty) | (tv,ty) <- zip ty_tvs tvs1_contents
865                           , getTyVar_maybe ty /= Just tv
866                           --, not(isTyVarTy ty)
867                           ]
868     return subst
869  where ty = sigmaType _ty
870
871 myDataConInstArgTys :: DataCon -> [Type] -> [Type]
872 myDataConInstArgTys dc args
873     | null (dataConExTyVars dc) && null (dataConEqTheta dc) = dataConInstArgTys dc args
874     | otherwise = dataConRepArgTys dc
875
876 mydataConType :: DataCon -> Type
877 -- ^ Custom version of DataCon.dataConUserType where we
878 --    - remove the equality constraints
879 --    - use the representation types for arguments, including dictionaries
880 --    - keep the original result type
881 mydataConType  dc
882   = mkForAllTys ((univ_tvs `minusList` map fst eq_spec) ++ ex_tvs) $
883     mkFunTys arg_tys $
884     res_ty
885   where univ_tvs   = dataConUnivTyVars dc
886         ex_tvs     = dataConExTyVars dc
887         eq_spec    = dataConEqSpec dc
888         arg_tys    = [case a of
889                         PredTy p -> predTypeRep p
890                         _        -> a
891                      | a <- dataConRepArgTys dc]
892         res_ty     = dataConOrigResTy dc
893
894 isRefType :: Type -> Bool
895 isRefType ty
896    | Just (tc, _) <- tcSplitTyConApp_maybe ty' = isRefTyCon tc
897    | otherwise = False
898   where ty'= repType ty
899
900 isRefTyCon :: TyCon -> Bool
901 isRefTyCon tc = tc `elem` [mutVarPrimTyCon, mVarPrimTyCon, tVarPrimTyCon]
902
903 -- Soundness checks
904 --------------------
905 {-
906 This is not formalized anywhere, so hold to your seats!
907 RTTI in the presence of newtypes can be a tricky and unsound business.
908
909 Example:
910 ~~~~~~~~~
911 Suppose we are doing RTTI for a partially evaluated
912 closure t, the real type of which is t :: MkT Int, for
913
914    newtype MkT a = MkT [Maybe a]
915
916 The table below shows the results of RTTI and the improvement
917 calculated for different combinations of evaluatedness and :type t.
918 Regard the two first columns as input and the next two as output.
919
920   # |     t     |  :type t  | rtti(t)  | improv.    | result
921     ------------------------------------------------------------
922   1 |     _     |    t b    |    a     | none       | OK
923   2 |     _     |   MkT b   |    a     | none       | OK
924   3 |     _     |   t Int   |    a     | none       | OK
925
926   If t is not evaluated at *all*, we are safe.
927
928   4 |  (_ : _)  |    t b    |   [a]    | t = []     | UNSOUND
929   5 |  (_ : _)  |   MkT b   |  MkT a   | none       | OK (compensating for the missing newtype)
930   6 |  (_ : _)  |   t Int   |  [Int]   | t = []     | UNSOUND
931
932   If a is a minimal whnf, we run into trouble. Note that
933   row 5 above does newtype enrichment on the ty_rtty parameter.
934
935   7 | (Just _:_)|    t b    |[Maybe a] | t = [],    | UNSOUND
936     |                       |          | b = Maybe a|
937
938   8 | (Just _:_)|   MkT b   |  MkT a   |  none      | OK
939   9 | (Just _:_)|   t Int   |   FAIL   |  none      | OK
940
941   And if t is any more evaluated than whnf, we are still in trouble.
942   Because constraints are solved in top-down order, when we reach the
943   Maybe subterm what we got is already unsound. This explains why the
944   row 9 fails to complete.
945
946   10 | (Just _:_)|  t Int  | [Maybe a]   |  FAIL    | OK
947   11 | (Just 1:_)|  t Int  | [Maybe Int] |  FAIL    | OK
948
949   We can undo the failure in row 9 by leaving out the constraint
950   coming from the type signature of t (i.e., the 2nd column).
951   Note that this type information is still used
952   to calculate the improvement. But we fail
953   when trying to calculate the improvement, as there is no unifier for
954   t Int = [Maybe a] or t Int = [Maybe Int].
955
956
957   Another set of examples with t :: [MkT (Maybe Int)]  \equiv  [[Maybe (Maybe Int)]]
958
959   # |     t     |    :type t    |  rtti(t)    | improvement | result
960     ---------------------------------------------------------------------
961   1 |(Just _:_) | [t (Maybe a)] | [[Maybe b]] | t = []      |
962     |           |               |             | b = Maybe a |
963
964 The checks:
965 ~~~~~~~~~~~
966 Consider a function obtainType that takes a value and a type and produces
967 the Term representation and a substitution (the improvement).
968 Assume an auxiliar rtti' function which does the actual job if recovering
969 the type, but which may produce a false type.
970
971 In pseudocode:
972
973   rtti' :: a -> IO Type  -- Does not use the static type information
974
975   obtainType :: a -> Type -> IO (Maybe (Term, Improvement))
976   obtainType v old_ty = do
977        rtti_ty <- rtti' v
978        if monomorphic rtti_ty || (check rtti_ty old_ty)
979         then ...
980          else return Nothing
981   where check rtti_ty old_ty = check1 rtti_ty &&
982                               check2 rtti_ty old_ty
983
984   check1 :: Type -> Bool
985   check2 :: Type -> Type -> Bool
986
987 Now, if rtti' returns a monomorphic type, we are safe.
988 If that is not the case, then we consider two conditions.
989
990
991 1. To prevent the class of unsoundness displayed by
992    rows 4 and 7 in the example: no higher kind tyvars
993    accepted.
994
995   check1 (t a)   = NO
996   check1 (t Int) = NO
997   check1 ([] a)  = YES
998
999 2. To prevent the class of unsoundness shown by row 6,
1000    the rtti type should be structurally more
1001    defined than the old type we are comparing it to.
1002   check2 :: NewType -> OldType -> Bool
1003   check2 a  _        = True
1004   check2 [a] a       = True
1005   check2 [a] (t Int) = False
1006   check2 [a] (t a)   = False  -- By check1 we never reach this equation
1007   check2 [Int] a     = True
1008   check2 [Int] (t Int) = True
1009   check2 [Maybe a]   (t Int) = False
1010   check2 [Maybe Int] (t Int) = True
1011   check2 (Maybe [a])   (m [Int]) = False
1012   check2 (Maybe [Int]) (m [Int]) = True
1013
1014 -}
1015
1016 check1 :: Type -> Bool
1017 check1 ty | (tvs, _, _) <- tcSplitSigmaTy ty = not $ any isHigherKind (map tyVarKind tvs)
1018  where
1019    isHigherKind = not . null . fst . splitKindFunTys
1020
1021 check2 :: Type -> Type -> Bool
1022 check2 sigma_rtti_ty sigma_old_ty
1023   | Just (_, rttis) <- tcSplitTyConApp_maybe rtti_ty
1024   = case () of
1025       _ | Just (_,olds) <- tcSplitTyConApp_maybe old_ty
1026         -> and$ zipWith check2 rttis olds
1027       _ | Just _ <- splitAppTy_maybe old_ty
1028         -> isMonomorphicOnNonPhantomArgs rtti_ty
1029       _ -> True
1030   | otherwise = True
1031   where (_, _ , rtti_ty) = tcSplitSigmaTy sigma_rtti_ty
1032         (_, _ , old_ty)  = tcSplitSigmaTy sigma_old_ty
1033
1034
1035 -- Dealing with newtypes
1036 --------------------------
1037 {-
1038  congruenceNewtypes does a parallel fold over two Type values, 
1039  compensating for missing newtypes on both sides. 
1040  This is necessary because newtypes are not present 
1041  in runtime, but sometimes there is evidence available.
1042    Evidence can come from DataCon signatures or
1043  from compile-time type inference.
1044  What we are doing here is an approximation
1045  of unification modulo a set of equations derived
1046  from newtype definitions. These equations should be the
1047  same as the equality coercions generated for newtypes
1048  in System Fc. The idea is to perform a sort of rewriting,
1049  taking those equations as rules, before launching unification.
1050
1051  The caller must ensure the following.
1052  The 1st type (lhs) comes from the heap structure of ptrs,nptrs.
1053  The 2nd type (rhs) comes from a DataCon type signature.
1054  Rewriting (i.e. adding/removing a newtype wrapper) can happen
1055  in both types, but in the rhs it is restricted to the result type.
1056
1057    Note that it is very tricky to make this 'rewriting'
1058  work with the unification implemented by TcM, where
1059  substitutions are operationally inlined. The order in which
1060  constraints are unified is vital as we cannot modify
1061  anything that has been touched by a previous unification step.
1062 Therefore, congruenceNewtypes is sound only if the types
1063 recovered by the RTTI mechanism are unified Top-Down.
1064 -}
1065 congruenceNewtypes ::  TcType -> TcType -> TR (TcType,TcType)
1066 congruenceNewtypes lhs rhs = go lhs rhs >>= \rhs' -> return (lhs,rhs')
1067  where
1068    go l r
1069  -- TyVar lhs inductive case
1070     | Just tv <- getTyVar_maybe l
1071     = recoverTR (return r) $ do
1072          Indirect ty_v <- readMetaTyVar tv
1073          traceTR $ fsep [text "(congruence) Following indirect tyvar:",
1074                           ppr tv, equals, ppr ty_v]
1075          go ty_v r
1076 -- FunTy inductive case
1077     | Just (l1,l2) <- splitFunTy_maybe l
1078     , Just (r1,r2) <- splitFunTy_maybe r
1079     = do r2' <- go l2 r2
1080          r1' <- go l1 r1
1081          return (mkFunTy r1' r2')
1082 -- TyconApp Inductive case; this is the interesting bit.
1083     | Just (tycon_l, _) <- tcSplitTyConApp_maybe lhs
1084     , Just (tycon_r, _) <- tcSplitTyConApp_maybe rhs 
1085     , tycon_l /= tycon_r 
1086     = upgrade tycon_l r
1087
1088     | otherwise = return r
1089
1090     where upgrade :: TyCon -> Type -> TR Type
1091           upgrade new_tycon ty
1092             | not (isNewTyCon new_tycon) = do
1093               traceTR (text "(Upgrade) Not matching newtype evidence: " <>
1094                        ppr new_tycon <> text " for " <> ppr ty)
1095               return ty 
1096             | otherwise = do
1097                traceTR (text "(Upgrade) upgraded " <> ppr ty <>
1098                         text " in presence of newtype evidence " <> ppr new_tycon)
1099                vars <- mapM (newVar . tyVarKind) (tyConTyVars new_tycon)
1100                let ty' = mkTyConApp new_tycon vars
1101                _ <- liftTcM (boxyUnify ty (repType ty'))
1102         -- assumes that reptype doesn't ^^^^ touch tyconApp args 
1103                return ty'
1104
1105
1106 zonkTerm :: Term -> TcM Term
1107 zonkTerm = foldTermM TermFoldM{
1108               fTermM = \ty dc v tt -> zonkTcType ty    >>= \ty' ->
1109                                       return (Term ty' dc v tt)
1110              ,fSuspensionM = \ct ty v b -> zonkTcType ty >>= \ty ->
1111                                            return (Suspension ct ty v b)
1112              ,fNewtypeWrapM= \ty dc t -> zonkTcType ty >>= \ty' ->
1113                                          return$ NewtypeWrap ty' dc t
1114              ,fRefWrapM    = \ty t ->
1115                                return RefWrap `ap` zonkTcType ty `ap` return t
1116              ,fPrimM       = (return.) . Prim
1117              }
1118
1119 --------------------------------------------------------------------------------
1120 -- Restore Class predicates out of a representation type
1121 dictsView :: Type -> Type
1122 -- dictsView ty = ty
1123 dictsView (FunTy (TyConApp tc_dict args) ty)
1124   | Just c <- tyConClass_maybe tc_dict
1125   = FunTy (PredTy (ClassP c args)) (dictsView ty)
1126 dictsView ty
1127   | Just (tc_fun, [TyConApp tc_dict args, ty2]) <- tcSplitTyConApp_maybe ty
1128   , Just c <- tyConClass_maybe tc_dict
1129   = mkTyConApp tc_fun [PredTy (ClassP c args), dictsView ty2]
1130 dictsView ty = ty
1131
1132
1133 -- Use only for RTTI types
1134 isMonomorphic :: RttiType -> Bool
1135 isMonomorphic ty = noExistentials && noUniversals
1136  where (tvs, _, ty')     = tcSplitSigmaTy ty
1137        noExistentials = isEmptyVarSet (tyVarsOfType ty')
1138        noUniversals   = null tvs
1139
1140 -- Use only for RTTI types
1141 isMonomorphicOnNonPhantomArgs :: RttiType -> Bool
1142 isMonomorphicOnNonPhantomArgs ty
1143   | Just (tc, all_args) <- tcSplitTyConApp_maybe (repType ty)
1144   , phantom_vars  <- tyConPhantomTyVars tc
1145   , concrete_args <- [ arg | (tyv,arg) <- tyConTyVars tc `zip` all_args
1146                            , tyv `notElem` phantom_vars]
1147   = all isMonomorphicOnNonPhantomArgs concrete_args
1148   | Just (ty1, ty2) <- splitFunTy_maybe ty
1149   = all isMonomorphicOnNonPhantomArgs [ty1,ty2]
1150   | otherwise = isMonomorphic ty
1151
1152 tyConPhantomTyVars :: TyCon -> [TyVar]
1153 tyConPhantomTyVars tc
1154   | isAlgTyCon tc
1155   , Just dcs <- tyConDataCons_maybe tc
1156   , dc_vars  <- concatMap dataConUnivTyVars dcs
1157   = tyConTyVars tc \\ dc_vars
1158 tyConPhantomTyVars _ = []
1159
1160 -- Is this defined elsewhere?
1161 -- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
1162 sigmaType :: Type -> Type
1163 sigmaType ty = mkSigmaTy (varSetElems$ tyVarsOfType ty) [] ty
1164
1165
1166 mapMif :: Monad m => (a -> Bool) -> (a -> m a) -> [a] -> m [a]
1167 mapMif pred f xx = sequence $ mapMif_ pred f xx
1168   where
1169    mapMif_ _ _ []     = []
1170    mapMif_ pred f (x:xx) = (if pred x then f x else return x) : mapMif_ pred f xx
1171
1172 unlessM :: Monad m => m Bool -> m () -> m ()
1173 unlessM condM acc = condM >>= \c -> unless c acc
1174
1175
1176 -- Strict application of f at index i
1177 appArr :: Ix i => (e -> a) -> Array i e -> Int -> a
1178 appArr f a@(Array _ _ _ ptrs#) i@(I# i#)
1179  = ASSERT2 (i < length(elems a), ppr(length$ elems a, i))
1180    case indexArray# ptrs# i# of
1181        (# e #) -> f e
1182
1183 amap' :: (t -> b) -> Array Int t -> [b]
1184 amap' f (Array i0 i _ arr#) = map g [0 .. i - i0]
1185     where g (I# i#) = case indexArray# arr# i# of
1186                           (# e #) -> f e
1187
1188
1189 isLifted :: Type -> Bool
1190 isLifted =  not . isUnLiftedType
1191
1192 extractUnboxed  :: [Type] -> Closure -> [[Word]]
1193 extractUnboxed tt clos = go tt (nonPtrs clos)
1194    where sizeofType t
1195            | Just (tycon,_) <- tcSplitTyConApp_maybe t
1196            = ASSERT (isPrimTyCon tycon) sizeofTyCon tycon
1197            | otherwise = pprPanic "Expected a TcTyCon" (ppr t)
1198          go [] _ = []
1199          go (t:tt) xx 
1200            | (x, rest) <- splitAt (sizeofType t) xx
1201            = x : go tt rest
1202
1203 sizeofTyCon :: TyCon -> Int -- in *words*
1204 sizeofTyCon = primRepSizeW . tyConPrimRep
1205
1206
1207 (|.|) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
1208 (f |.| g) x = f x || g x