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