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