RtClosureInspect.hs 47.8 KB
Newer Older
1
2
3
4
5
6
7
8
9
-----------------------------------------------------------------------------
--
-- GHC Interactive support for inspecting arbitrary closures at runtime
--
-- Pepe Iborra (supported by Google SoC) 2006
--
-----------------------------------------------------------------------------

module RtClosureInspect(
10
     cvObtainTerm,      -- :: HscEnv -> Int -> Bool -> Maybe Type -> HValue -> IO Term
11
     cvReconstructType,
12
     improveRTTIType,
pepe's avatar
pepe committed
13
14
15
16
17
18
19
20
21
22
23
24
25
26

     Term(..),
     isTerm, isSuspension, isPrim, isFun, isFunLike, isNewtypeWrap,
     isFullyEvaluated, isFullyEvaluatedTerm,
     termType, mapTermType, termTyVars,
     foldTerm, TermFold(..), foldTermM, TermFoldM(..), idTermFold,
     pprTerm, cPprTerm, cPprTermBase, CustomTermPrinter,

--     unsafeDeepSeq,

     Closure(..), getClosureData, ClosureType(..), isConstr, isIndirection,

     sigmaType
 ) where
27
28
29
30
31

#include "HsVersions.h"

import ByteCodeItbls    ( StgInfoTable )
import qualified ByteCodeItbls as BCI( StgInfoTable(..) )
pepe's avatar
pepe committed
32
import HscTypes
33
import Linker
34

35
36
import DataCon
import Type
pepe's avatar
pepe committed
37
import TypeRep         -- I know I know, this is cheating
38
import Var
twanvl's avatar
twanvl committed
39
import TcRnMonad
40
41
42
import TcType
import TcMType
import TcUnify
43
import TcEnv
pepe's avatar
pepe committed
44

45
46
import TyCon
import Name
47
import VarEnv
48
import Util
mnislaih's avatar
mnislaih committed
49
import ListSetOps
50
import VarSet
51
import TysPrim
52
53
import PrelNames
import TysWiredIn
pepe's avatar
pepe committed
54
import DynFlags
55
import Outputable
56
import FastString
57
58
import Panic

59
60
import Constants        ( wORD_SIZE )

61
import GHC.Arr          ( Array(..) )
62
import GHC.Exts
63
64
65
66
67
68

#if __GLASGOW_HASKELL__ >= 611
import GHC.IO ( IO(..) )
#else
import GHC.IOBase ( IO(..) )
#endif
69
70
71
72

import Control.Monad
import Data.Maybe
import Data.Array.Base
mnislaih's avatar
mnislaih committed
73
import Data.Ix
pepe's avatar
pepe committed
74
import Data.List
75
76
77
import qualified Data.Sequence as Seq
import Data.Monoid
import Data.Sequence hiding (null, length, index, take, drop, splitAt, reverse)
78
import Foreign
79
import System.IO.Unsafe
80

81
import System.IO
82
83
84
85
---------------------------------------------
-- * A representation of semi evaluated Terms
---------------------------------------------

pepe's avatar
pepe committed
86
data Term = Term { ty        :: RttiType
87
                 , dc        :: Either String DataCon
mnislaih's avatar
mnislaih committed
88
89
90
                               -- Carries a text representation if the datacon is
                               -- not exported by the .hi file, which is the case 
                               -- for private constructors in -O0 compiled libraries
91
92
93
                 , val       :: HValue 
                 , subTerms  :: [Term] }

pepe's avatar
pepe committed
94
          | Prim { ty        :: RttiType
95
                 , value     :: [Word] }
96
97

          | Suspension { ctype    :: ClosureType
pepe's avatar
pepe committed
98
                       , ty       :: RttiType
99
100
101
                       , val      :: HValue
                       , bound_to :: Maybe Name   -- Useful for printing
                       }
pepe's avatar
pepe committed
102
103
104
105
106
          | NewtypeWrap{       -- At runtime there are no newtypes, and hence no
                               -- newtype constructors. A NewtypeWrap is just a
                               -- made-up tag saying "heads up, there used to be
                               -- a newtype constructor here".
                         ty           :: RttiType
107
108
                       , dc           :: Either String DataCon
                       , wrapped_term :: Term }
pepe's avatar
pepe committed
109
110
          | RefWrap    {       -- The contents of a reference
                         ty           :: RttiType
111
                       , wrapped_term :: Term }
112

pepe's avatar
pepe committed
113
isTerm, isSuspension, isPrim, isFun, isFunLike, isNewtypeWrap :: Term -> Bool
114
115
116
117
118
119
isTerm Term{} = True
isTerm   _    = False
isSuspension Suspension{} = True
isSuspension      _       = False
isPrim Prim{} = True
isPrim   _    = False
120
121
isNewtypeWrap NewtypeWrap{} = True
isNewtypeWrap _             = False
122

pepe's avatar
pepe committed
123
124
125
126
127
128
129
isFun Suspension{ctype=Fun} = True
isFun _ = False

isFunLike s@Suspension{ty=ty} = isFun s || isFunTy ty
isFunLike _ = False

termType :: Term -> RttiType
mnislaih's avatar
mnislaih committed
130
termType t = ty t
131

mnislaih's avatar
mnislaih committed
132
133
134
isFullyEvaluatedTerm :: Term -> Bool
isFullyEvaluatedTerm Term {subTerms=tt} = all isFullyEvaluatedTerm tt
isFullyEvaluatedTerm Prim {}            = True
135
isFullyEvaluatedTerm NewtypeWrap{wrapped_term=t} = isFullyEvaluatedTerm t
136
isFullyEvaluatedTerm RefWrap{wrapped_term=t}     = isFullyEvaluatedTerm t
137
isFullyEvaluatedTerm _                  = False
mnislaih's avatar
mnislaih committed
138

139
instance Outputable (Term) where
mnislaih's avatar
mnislaih committed
140
141
 ppr t | Just doc <- cPprTerm cPprTermBase t = doc
       | otherwise = panic "Outputable Term instance"
142
143
144
145
146
147
148
149
150
151
152
153

-------------------------------------------------------------------------
-- Runtime Closure Datatype and functions for retrieving closure related stuff
-------------------------------------------------------------------------
data ClosureType = Constr 
                 | Fun 
                 | Thunk Int 
                 | ThunkSelector
                 | Blackhole 
                 | AP 
                 | PAP 
                 | Indirection Int 
154
                 | MutVar Int
pepe's avatar
pepe committed
155
                 | MVar   Int
156
                 | Other  Int
157
158
159
 deriving (Show, Eq)

data Closure = Closure { tipe         :: ClosureType 
160
                       , infoPtr      :: Ptr ()
161
162
                       , infoTable    :: StgInfoTable
                       , ptrs         :: Array Int HValue
163
                       , nonPtrs      :: [Word]
164
165
166
167
168
169
170
                       }

instance Outputable ClosureType where
  ppr = text . show 

#include "../includes/ClosureTypes.h"

mnislaih's avatar
mnislaih committed
171
aP_CODE, pAP_CODE :: Int
172
173
174
175
176
177
aP_CODE = AP
pAP_CODE = PAP
#undef AP
#undef PAP

getClosureData :: a -> IO Closure
178
179
180
getClosureData a =
   case unpackClosure# a of 
     (# iptr, ptrs, nptrs #) -> do
Ian Lynagh's avatar
Ian Lynagh committed
181
182
183
184
185
186
187
188
189
190
191
           let iptr'
                | ghciTablesNextToCode =
                   Ptr iptr
                | otherwise =
                   -- the info pointer we get back from unpackClosure#
                   -- is to the beginning of the standard info table,
                   -- but the Storable instance for info tables takes
                   -- into account the extra entry pointer when
                   -- !ghciTablesNextToCode, so we must adjust here:
                   Ptr iptr `plusPtr` negate wORD_SIZE
           itbl <- peek iptr'
192
           let tipe = readCType (BCI.tipe itbl)
193
194
               elems = fromIntegral (BCI.ptrs itbl)
               ptrsList = Array 0 (elems - 1) elems ptrs
195
196
               nptrs_data = [W# (indexWordArray# nptrs i)
                              | I# i <- [0.. fromIntegral (BCI.nptrs itbl)] ]
197
           ASSERT(elems >= 0) return ()
198
199
           ptrsList `seq` 
            return (Closure tipe (Ptr iptr) itbl ptrsList nptrs_data)
200
201

readCType :: Integral a => a -> ClosureType
202
readCType i 
203
204
 | i >= CONSTR && i <= CONSTR_NOCAF_STATIC = Constr
 | i >= FUN    && i <= FUN_STATIC          = Fun
205
 | i >= THUNK  && i < THUNK_SELECTOR       = Thunk i'
206
207
 | i == THUNK_SELECTOR                     = ThunkSelector
 | i == BLACKHOLE                          = Blackhole
208
209
 | i >= IND    && i <= IND_STATIC          = Indirection i'
 | i' == aP_CODE                           = AP
210
 | i == AP_STACK                           = AP
211
 | i' == pAP_CODE                          = PAP
pepe's avatar
pepe committed
212
213
 | i == MUT_VAR_CLEAN || i == MUT_VAR_DIRTY= MutVar i'
 | i == MVAR_CLEAN    || i == MVAR_DIRTY   = MVar i'
214
215
216
 | otherwise                               = Other  i'
  where i' = fromIntegral i
 
217
isConstr, isIndirection, isThunk :: ClosureType -> Bool
218
219
220
221
222
223
isConstr Constr = True
isConstr    _   = False

isIndirection (Indirection _) = True
isIndirection _ = False

224
225
226
227
228
isThunk (Thunk _)     = True
isThunk ThunkSelector = True
isThunk AP            = True
isThunk _             = False

229
230
231
232
233
234
isFullyEvaluated :: a -> IO Bool
isFullyEvaluated a = do 
  closure <- getClosureData a 
  case tipe closure of
    Constr -> do are_subs_evaluated <- amapM isFullyEvaluated (ptrs closure)
                 return$ and are_subs_evaluated
mnislaih's avatar
mnislaih committed
235
    _      -> return False
236
237
238
239
240
241
242
  where amapM f = sequence . amap' f

-- TODO: Fix it. Probably the otherwise case is failing, trace/debug it
{-
unsafeDeepSeq :: a -> b -> b
unsafeDeepSeq = unsafeDeepSeq1 2
 where unsafeDeepSeq1 0 a b = seq a $! b
243
       unsafeDeepSeq1 i a b   -- 1st case avoids infinite loops for non reducible thunks
244
245
246
247
248
249
250
251
        | not (isConstr tipe) = seq a $! unsafeDeepSeq1 (i-1) a b     
     -- | unsafePerformIO (isFullyEvaluated a) = b
        | otherwise = case unsafePerformIO (getClosureData a) of
                        closure -> foldl' (flip unsafeDeepSeq) b (ptrs closure)
        where tipe = unsafePerformIO (getClosureType a)
-}

-----------------------------------
mnislaih's avatar
mnislaih committed
252
-- * Traversals for Terms
253
-----------------------------------
pepe's avatar
pepe committed
254
type TermProcessor a b = RttiType -> Either String DataCon -> HValue -> [a] -> b
255

256
data TermFold a = TermFold { fTerm        :: TermProcessor a a
pepe's avatar
pepe committed
257
258
                           , fPrim        :: RttiType -> [Word] -> a
                           , fSuspension  :: ClosureType -> RttiType -> HValue
mnislaih's avatar
mnislaih committed
259
                                            -> Maybe Name -> a
pepe's avatar
pepe committed
260
                           , fNewtypeWrap :: RttiType -> Either String DataCon
261
                                            -> a -> a
pepe's avatar
pepe committed
262
263
264
265
266
267
268
269
270
271
272
273
                           , fRefWrap     :: RttiType -> a -> a
                           }


data TermFoldM m a =
                   TermFoldM {fTermM        :: TermProcessor a (m a)
                            , fPrimM        :: RttiType -> [Word] -> m a
                            , fSuspensionM  :: ClosureType -> RttiType -> HValue
                                             -> Maybe Name -> m a
                            , fNewtypeWrapM :: RttiType -> Either String DataCon
                                            -> a -> m a
                            , fRefWrapM     :: RttiType -> a -> m a
274
275
276
277
278
279
                           }

foldTerm :: TermFold a -> Term -> a
foldTerm tf (Term ty dc v tt) = fTerm tf ty dc v (map (foldTerm tf) tt)
foldTerm tf (Prim ty    v   ) = fPrim tf ty v
foldTerm tf (Suspension ct ty v b) = fSuspension tf ct ty v b
280
foldTerm tf (NewtypeWrap ty dc t)  = fNewtypeWrap tf ty dc (foldTerm tf t)
281
foldTerm tf (RefWrap ty t)         = fRefWrap tf ty (foldTerm tf t)
282

pepe's avatar
pepe committed
283
284
285
286
287
288
289
290

foldTermM :: Monad m => TermFoldM m a -> Term -> m a
foldTermM tf (Term ty dc v tt) = mapM (foldTermM tf) tt >>= fTermM tf ty dc v
foldTermM tf (Prim ty    v   ) = fPrimM tf ty v
foldTermM tf (Suspension ct ty v b) = fSuspensionM tf ct ty v b
foldTermM tf (NewtypeWrap ty dc t)  = foldTermM tf t >>=  fNewtypeWrapM tf ty dc
foldTermM tf (RefWrap ty t)         = foldTermM tf t >>= fRefWrapM tf ty

291
292
293
294
idTermFold :: TermFold Term
idTermFold = TermFold {
              fTerm = Term,
              fPrim = Prim,
295
              fSuspension  = Suspension,
296
297
              fNewtypeWrap = NewtypeWrap,
              fRefWrap = RefWrap
298
299
                      }

pepe's avatar
pepe committed
300
mapTermType :: (RttiType -> Type) -> Term -> Term
301
302
mapTermType f = foldTerm idTermFold {
          fTerm       = \ty dc hval tt -> Term (f ty) dc hval tt,
mnislaih's avatar
mnislaih committed
303
304
          fSuspension = \ct ty hval n ->
                          Suspension ct (f ty) hval n,
305
306
          fNewtypeWrap= \ty dc t -> NewtypeWrap (f ty) dc t,
          fRefWrap    = \ty t -> RefWrap (f ty) t}
307

pepe's avatar
pepe committed
308
309
310
311
312
313
314
315
316
mapTermTypeM :: Monad m =>  (RttiType -> m Type) -> Term -> m Term
mapTermTypeM f = foldTermM TermFoldM {
          fTermM       = \ty dc hval tt -> f ty >>= \ty' -> return $ Term ty'  dc hval tt,
          fPrimM       = (return.) . Prim,
          fSuspensionM = \ct ty hval n ->
                          f ty >>= \ty' -> return $ Suspension ct ty' hval n,
          fNewtypeWrapM= \ty dc t -> f ty >>= \ty' -> return $ NewtypeWrap ty' dc t,
          fRefWrapM    = \ty t -> f ty >>= \ty' -> return $ RefWrap ty' t}

317
termTyVars :: Term -> TyVarSet
318
319
320
termTyVars = foldTerm TermFold {
            fTerm       = \ty _ _ tt   -> 
                          tyVarsOfType ty `plusVarEnv` concatVarEnv tt,
mnislaih's avatar
mnislaih committed
321
            fSuspension = \_ ty _ _ -> tyVarsOfType ty,
322
            fPrim       = \ _ _ -> emptyVarEnv,
323
324
            fNewtypeWrap= \ty _ t -> tyVarsOfType ty `plusVarEnv` t,
            fRefWrap    = \ty t -> tyVarsOfType ty `plusVarEnv` t}
325
    where concatVarEnv = foldr plusVarEnv emptyVarEnv
326

327
328
329
330
----------------------------------
-- Pretty printing of terms
----------------------------------

mnislaih's avatar
mnislaih committed
331
332
333
334
type Precedence        = Int
type TermPrinter       = Precedence -> Term ->   SDoc
type TermPrinterM m    = Precedence -> Term -> m SDoc

mnislaih's avatar
mnislaih committed
335
336
337
app_prec,cons_prec, max_prec ::Int
max_prec  = 10
app_prec  = max_prec
338
cons_prec = 5 -- TODO Extract this info from GHC itself
339

mnislaih's avatar
mnislaih committed
340
341
pprTerm :: TermPrinter -> TermPrinter
pprTerm y p t | Just doc <- pprTermM (\p -> Just . y p) p t = doc
mnislaih's avatar
mnislaih committed
342
pprTerm _ _ _ = panic "pprTerm"
343

mnislaih's avatar
mnislaih committed
344
345
346
347
pprTermM, ppr_termM, pprNewtypeWrap :: Monad m => TermPrinterM m -> TermPrinterM m
pprTermM y p t = pprDeeper `liftM` ppr_termM y p t

ppr_termM y p Term{dc=Left dc_tag, subTerms=tt} = do
348
  tt_docs <- mapM (y app_prec) tt
mnislaih's avatar
mnislaih committed
349
  return$ cparen (not(null tt) && p >= app_prec) (text dc_tag <+> pprDeeperList fsep tt_docs)
350
  
mnislaih's avatar
mnislaih committed
351
ppr_termM y p Term{dc=Right dc, subTerms=tt} 
352
{-  | dataConIsInfix dc, (t1:t2:tt') <- tt  --TODO fixity
mnislaih's avatar
mnislaih committed
353
354
  = parens (ppr_term1 True t1 <+> ppr dc <+> ppr_term1 True ppr t2) 
    <+> hsep (map (ppr_term1 True) tt) 
355
-} -- TODO Printing infix constructors properly
356
357
358
  | null tt   = return$ ppr dc
  | otherwise = do
         tt_docs <- mapM (y app_prec) tt
mnislaih's avatar
mnislaih committed
359
         return$ cparen (p >= app_prec) (ppr dc <+> pprDeeperList fsep tt_docs)
360

mnislaih's avatar
mnislaih committed
361
ppr_termM y p t@NewtypeWrap{} = pprNewtypeWrap y p t
mnislaih's avatar
mnislaih committed
362
ppr_termM y p RefWrap{wrapped_term=t}  = do
363
364
365
366
367
368
369
  contents <- y app_prec t
  return$ cparen (p >= app_prec) (text "GHC.Prim.MutVar#" <+> contents)
  -- The constructor name is wired in here ^^^ for the sake of simplicity.
  -- I don't think mutvars are going to change in a near future.
  -- In any case this is solely a presentation matter: MutVar# is
  -- a datatype with no constructors, implemented by the RTS
  -- (hence there is no way to obtain a datacon and print it).
mnislaih's avatar
mnislaih committed
370
ppr_termM _ _ t = ppr_termM1 t
mnislaih's avatar
mnislaih committed
371

mnislaih's avatar
mnislaih committed
372

373
ppr_termM1 :: Monad m => Term -> m SDoc
mnislaih's avatar
mnislaih committed
374
ppr_termM1 Prim{value=words, ty=ty} = 
375
    return$ text$ repPrim (tyConAppTyCon ty) words
pepe's avatar
pepe committed
376
377
ppr_termM1 Suspension{ty=ty, bound_to=Nothing} = 
    return (char '_' <+> ifPprDebug (text "::" <> ppr ty))
mnislaih's avatar
mnislaih committed
378
ppr_termM1 Suspension{ty=ty, bound_to=Just n}
pepe's avatar
pepe committed
379
--  | Just _ <- splitFunTy_maybe ty = return$ ptext (sLit("<function>")
380
381
382
383
  | otherwise = return$ parens$ ppr n <> text "::" <> ppr ty
ppr_termM1 Term{}        = panic "ppr_termM1 - Term"
ppr_termM1 RefWrap{}     = panic "ppr_termM1 - RefWrap"
ppr_termM1 NewtypeWrap{} = panic "ppr_termM1 - NewtypeWrap"
mnislaih's avatar
mnislaih committed
384

385
pprNewtypeWrap y p NewtypeWrap{ty=ty, wrapped_term=t}
386
  | Just (tc,_) <- tcSplitTyConApp_maybe ty
387
  , ASSERT(isNewTyCon tc) True
388
  , Just new_dc <- tyConSingleDataCon_maybe tc = do 
389
390
391
392
         if integerDataConName == dataConName new_dc
             then return $ text $ show $ (unsafeCoerce# $ val t :: Integer)
             else do real_term <- y max_prec t
                     return$ cparen (p >= app_prec) (ppr new_dc <+> real_term)
393
394
pprNewtypeWrap _ _ _ = panic "pprNewtypeWrap"

395
396
397
398
399
400
401
402
403
404
405
406
407
-------------------------------------------------------
-- Custom Term Pretty Printers
-------------------------------------------------------

-- We can want to customize the representation of a 
--  term depending on its type. 
-- However, note that custom printers have to work with
--  type representations, instead of directly with types.
-- We cannot use type classes here, unless we employ some 
--  typerep trickery (e.g. Weirich's RepLib tricks),
--  which I didn't. Therefore, this code replicates a lot
--  of what type classes provide for free.

mnislaih's avatar
mnislaih committed
408
type CustomTermPrinter m = TermPrinterM m
409
                         -> [Precedence -> Term -> (m (Maybe SDoc))]
410

mnislaih's avatar
mnislaih committed
411
-- | Takes a list of custom printers with a explicit recursion knot and a term, 
412
-- and returns the output of the first succesful printer, or the default printer
413
cPprTerm :: Monad m => CustomTermPrinter m -> Term -> m SDoc
mnislaih's avatar
mnislaih committed
414
415
cPprTerm printers_ = go 0 where
  printers = printers_ go
416
  go prec t = do
mnislaih's avatar
mnislaih committed
417
    let default_ = Just `liftM` pprTermM go prec t
418
        mb_customDocs = [pp prec t | pp <- printers] ++ [default_]
419
420
    Just doc <- firstJustM mb_customDocs
    return$ cparen (prec>app_prec+1) doc
421

422
423
  firstJustM (mb:mbs) = mb >>= maybe (firstJustM mbs) (return . Just)
  firstJustM [] = return Nothing
424

425
-- Default set of custom printers. Note that the recursion knot is explicit
426
cPprTermBase :: Monad m => CustomTermPrinter m
427
cPprTermBase y =
428
429
430
431
432
433
434
435
436
  [ ifTerm (isTupleTy.ty) (\_p -> liftM (parens . hcat . punctuate comma) 
                                      . mapM (y (-1))
                                      . subTerms)
  , ifTerm (\t -> isTyCon listTyCon (ty t) && subTerms t `lengthIs` 2)
           (\ p Term{subTerms=[h,t]} -> doList p h t)
  , ifTerm (isTyCon intTyCon    . ty) (coerceShow$ \(a::Int)->a)
  , ifTerm (isTyCon charTyCon   . ty) (coerceShow$ \(a::Char)->a)
  , ifTerm (isTyCon floatTyCon  . ty) (coerceShow$ \(a::Float)->a)
  , ifTerm (isTyCon doubleTyCon . ty) (coerceShow$ \(a::Double)->a)
mnislaih's avatar
mnislaih committed
437
  ]
438
439
440
441
442
     where ifTerm pred f prec t@Term{}
               | pred t    = Just `liftM` f prec t
           ifTerm _ _ _ _  = return Nothing

           isTupleTy ty    = fromMaybe False $ do 
pepe's avatar
pepe committed
443
             (tc,_) <- tcSplitTyConApp_maybe ty 
444
             return (isBoxedTupleTyCon tc)
445
446

           isTyCon a_tc ty = fromMaybe False $ do 
pepe's avatar
pepe committed
447
             (tc,_) <- tcSplitTyConApp_maybe ty
448
             return (a_tc == tc)
449
450
451

           coerceShow f _p = return . text . show . f . unsafeCoerce# . val

mnislaih's avatar
mnislaih committed
452
           --Note pprinting of list terms is not lazy
453
           doList p h t = do
454
               let elems      = h : getListTerms t
mnislaih's avatar
mnislaih committed
455
                   isConsLast = not(termType(last elems) `coreEqType` termType h)
456
               print_elems <- mapM (y cons_prec) elems
457
               return$ if isConsLast
mnislaih's avatar
mnislaih committed
458
                     then cparen (p >= cons_prec) 
mnislaih's avatar
mnislaih committed
459
                        . pprDeeperList fsep 
mnislaih's avatar
mnislaih committed
460
461
                        . punctuate (space<>colon)
                        $ print_elems
mnislaih's avatar
wibble    
mnislaih committed
462
                     else brackets (pprDeeperList fcat$
mnislaih's avatar
mnislaih committed
463
                                         punctuate comma print_elems)
464

mnislaih's avatar
mnislaih committed
465
                where getListTerms Term{subTerms=[h,t]} = h : getListTerms t
mnislaih's avatar
wibble    
mnislaih committed
466
                      getListTerms Term{subTerms=[]}    = []
467
468
469
                      getListTerms t@Suspension{}       = [t]
                      getListTerms t = pprPanic "getListTerms" (ppr t)

470

471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
repPrim :: TyCon -> [Word] -> String
repPrim t = rep where 
   rep x
    | t == charPrimTyCon   = show (build x :: Char)
    | t == intPrimTyCon    = show (build x :: Int)
    | t == wordPrimTyCon   = show (build x :: Word)
    | t == floatPrimTyCon  = show (build x :: Float)
    | t == doublePrimTyCon = show (build x :: Double)
    | t == int32PrimTyCon  = show (build x :: Int32)
    | t == word32PrimTyCon = show (build x :: Word32)
    | t == int64PrimTyCon  = show (build x :: Int64)
    | t == word64PrimTyCon = show (build x :: Word64)
    | t == addrPrimTyCon   = show (nullPtr `plusPtr` build x)
    | t == stablePtrPrimTyCon  = "<stablePtr>"
    | t == stableNamePrimTyCon = "<stableName>"
    | t == statePrimTyCon      = "<statethread>"
    | t == realWorldTyCon      = "<realworld>"
    | t == threadIdPrimTyCon   = "<ThreadId>"
    | t == weakPrimTyCon       = "<Weak>"
    | t == arrayPrimTyCon      = "<array>"
    | t == byteArrayPrimTyCon  = "<bytearray>"
    | t == mutableArrayPrimTyCon = "<mutableArray>"
    | t == mutableByteArrayPrimTyCon = "<mutableByteArray>"
    | t == mutVarPrimTyCon= "<mutVar>"
    | t == mVarPrimTyCon  = "<mVar>"
    | t == tVarPrimTyCon  = "<tVar>"
    | otherwise = showSDoc (char '<' <> ppr t <> char '>')
    where build ww = unsafePerformIO $ withArray ww (peek . castPtr) 
499
500
--   This ^^^ relies on the representation of Haskell heap values being 
--   the same as in a C array. 
mnislaih's avatar
mnislaih committed
501

502
503
504
-----------------------------------
-- Type Reconstruction
-----------------------------------
mnislaih's avatar
mnislaih committed
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
{-
Type Reconstruction is type inference done on heap closures.
The algorithm walks the heap generating a set of equations, which
are solved with syntactic unification.
A type reconstruction equation looks like:

  <datacon reptype>  =  <actual heap contents> 

The full equation set is generated by traversing all the subterms, starting
from a given term.

The only difficult part is that newtypes are only found in the lhs of equations.
Right hand sides are missing them. We can either (a) drop them from the lhs, or 
(b) reconstruct them in the rhs when possible. 

The function congruenceNewtypes takes a shot at (b)
-}
522
523


pepe's avatar
pepe committed
524
525
526
527
528
529
530
531
532
-- A (non-mutable) tau type containing
-- existentially quantified tyvars.
--    (since GHC type language currently does not support
--     existentials, we leave these variables unquantified)
type RttiType = Type

-- An incomplete type as stored in GHCi:
--  no polymorphism: no quantifiers & all tyvars are skolem.
type GhciType = Type
533
534
535
536
537


-- The Type Reconstruction monad
--------------------------------
type TR a = TcM a
pepe's avatar
pepe committed
538
539
540
541
542

runTR :: HscEnv -> TR a -> IO a
runTR hsc_env thing = do
  mb_val <- runTR_maybe hsc_env thing
  case mb_val of
543
    Nothing -> error "unable to :print the term"
544
545
546
    Just x  -> return x

runTR_maybe :: HscEnv -> TR a -> IO (Maybe a)
547
runTR_maybe hsc_env = fmap snd . initTc hsc_env HsSrcFile False  iNTERACTIVE
548

549
traceTR :: SDoc -> TR ()
pepe's avatar
pepe committed
550
551
552
553
554
555
556
557
558
559
560
561
traceTR = liftTcM . traceOptTcRn Opt_D_dump_rtti


-- Semantically different to recoverM in TcRnMonad 
-- recoverM retains the errors in the first action,
--  whereas recoverTc here does not
recoverTR :: TR a -> TR a -> TR a
recoverTR recover thing = do 
  (_,mb_res) <- tryTcErrs thing
  case mb_res of 
    Nothing  -> recover
    Just res -> return res
562

563
trIO :: IO a -> TR a 
twanvl's avatar
twanvl committed
564
trIO = liftTcM . liftIO
565

566
liftTcM :: TcM a -> TR a
mnislaih's avatar
mnislaih committed
567
liftTcM = id
568

569
newVar :: Kind -> TR TcType
pepe's avatar
pepe committed
570
newVar = liftTcM . liftM mkTyVarTy . newBoxyTyVar
571

572
573
574
-- | Returns the instantiated type scheme ty', and the substitution sigma 
--   such that sigma(ty') = ty 
instScheme :: Type -> TR (TcType, TvSubst)
pepe's avatar
pepe committed
575
576
577
instScheme ty = liftTcM$ do
   (tvs, _, _)      <- tcInstType return ty
   (tvs',_,ty') <- tcInstType (mapM tcInstTyVar) ty
578
   return (ty', zipTopTvSubst tvs' (mkTyVarTys tvs))
579

580
581
582
583
584
-- Adds a constraint of the form t1 == t2
-- t1 is expected to come from walking the heap
-- t2 is expected to come from a datacon signature
-- Before unification, congruenceNewtypes needs to
-- do its magic.
mnislaih's avatar
mnislaih committed
585
addConstraint :: TcType -> TcType -> TR ()
pepe's avatar
pepe committed
586
addConstraint actual expected = do
mnislaih's avatar
mnislaih committed
587
    traceTR (text "add constraint:" <+> fsep [ppr actual, equals, ppr expected])
pepe's avatar
pepe committed
588
589
590
    recoverTR (traceTR $ fsep [text "Failed to unify", ppr actual,
                                    text "with", ppr expected])
              (congruenceNewtypes actual expected >>=
591
                           (getLIE . uncurry boxyUnify) >> return ())
pepe's avatar
pepe committed
592
593
     -- TOMDO: what about the coercion?
     -- we should consider family instances
mnislaih's avatar
mnislaih committed
594

595
596
597

-- Type & Term reconstruction
------------------------------
pepe's avatar
pepe committed
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
cvObtainTerm :: HscEnv -> Int -> Bool -> RttiType -> HValue -> IO Term
cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
  -- we quantify existential tyvars as universal,
  -- as this is needed to be able to manipulate
  -- them properly
   let sigma_old_ty = sigmaType old_ty
   traceTR (text "Term reconstruction started with initial type " <> ppr old_ty)
   term <-
     if isMonomorphic sigma_old_ty
      then do
        new_ty <- go max_depth sigma_old_ty sigma_old_ty hval >>= zonkTerm
        return $ fixFunDictionaries $ expandNewtypes new_ty
      else do
              (old_ty', rev_subst) <- instScheme sigma_old_ty
              my_ty <- newVar argTypeKind
              when (check1 sigma_old_ty) (traceTR (text "check1 passed") >>
                                          addConstraint my_ty old_ty')
              term  <- go max_depth my_ty sigma_old_ty hval
              zterm <- zonkTerm term
              let new_ty = termType zterm
              if isMonomorphic new_ty || check2 (sigmaType new_ty) sigma_old_ty
                 then do
                      traceTR (text "check2 passed")
                      addConstraint (termType term) old_ty'
                      zterm' <- zonkTerm term
                      return ((fixFunDictionaries . expandNewtypes . mapTermType (substTy rev_subst)) zterm')
                 else do
                      traceTR (text "check2 failed" <+> parens
                                       (ppr zterm <+> text "::" <+> ppr new_ty))
                      -- we have unsound types. Replace constructor types in
                      -- subterms with tyvars
                      zterm' <- mapTermTypeM
                                 (\ty -> case tcSplitTyConApp_maybe ty of
                                           Just (tc, _:_) | tc /= funTyCon
                                               -> newVar argTypeKind
                                           _   -> return ty)
                                 zterm
                      zonkTerm zterm'
mnislaih's avatar
mnislaih committed
636
637
638
   traceTR (text "Term reconstruction completed." $$
            text "Term obtained: " <> ppr term $$
            text "Type obtained: " <> ppr (termType term))
pepe's avatar
pepe committed
639
   return term
640
    where 
pepe's avatar
pepe committed
641
642
643
  go :: Int -> Type -> Type -> HValue -> TcM Term
  go max_depth _ _ _ | seq max_depth False = undefined
  go 0 my_ty _old_ty a = do
mnislaih's avatar
mnislaih committed
644
645
    traceTR (text "Gave up reconstructing a term after" <>
                  int max_depth <> text " steps")
646
    clos <- trIO $ getClosureData a
pepe's avatar
pepe committed
647
    return (Suspension (tipe clos) my_ty a Nothing)
mnislaih's avatar
mnislaih committed
648
  go max_depth my_ty old_ty a = do
pepe's avatar
pepe committed
649
    let monomorphic = not(isTyVarTy my_ty)   
650
651
    -- This ^^^ is a convention. The ancestor tests for
    -- monomorphism and passes a type instead of a tv
652
653
    clos <- trIO $ getClosureData a
    case tipe clos of
654
-- Thunks we may want to force
Simon Marlow's avatar
Simon Marlow committed
655
656
657
-- NB. this won't attempt to force a BLACKHOLE.  Even with :force, we never
-- force blackholes, because it would almost certainly result in deadlock,
-- and showing the '_' is more useful.
pepe's avatar
pepe committed
658
659
660
661
662
      t | isThunk t && force -> traceTR (text "Forcing a " <> text (show t)) >>
                                seq a (go (pred max_depth) my_ty old_ty a)
-- We always follow indirections
      Indirection i -> do traceTR (text "Following an indirection" <> parens (int i) )
                          go max_depth my_ty old_ty $! (ptrs clos ! 0)
663
-- We also follow references
pepe's avatar
pepe committed
664
      MutVar _ | Just (tycon,[world,contents_ty]) <- tcSplitTyConApp_maybe old_ty
665
             -> do
pepe's avatar
pepe committed
666
667
668
669
670
671
                  -- Deal with the MutVar# primitive
                  -- It does not have a constructor at all, 
                  -- so we simulate the following one
                  -- MutVar# :: contents_ty -> MutVar# s contents_ty
         traceTR (text "Following a MutVar")
         contents_tv <- newVar liftedTypeKind
672
         contents <- trIO$ IO$ \w -> readMutVar# (unsafeCoerce# a) w
pepe's avatar
pepe committed
673
674
675
676
677
678
         ASSERT(isUnliftedTypeKind $ typeKind my_ty) return ()
         (mutvar_ty,_) <- instScheme $ sigmaType $ mkFunTy 
                            contents_ty (mkTyConApp tycon [world,contents_ty])
         addConstraint (mkFunTy contents_tv my_ty) mutvar_ty
         x <- go (pred max_depth) contents_tv contents_ty contents
         return (RefWrap my_ty x)
679

680
681
 -- The interesting case
      Constr -> do
mnislaih's avatar
mnislaih committed
682
683
684
685
        traceTR (text "entering a constructor " <>
                      if monomorphic
                        then parens (text "already monomorphic: " <> ppr my_ty)
                        else Outputable.empty)
686
687
688
689
690
691
692
693
694
695
696
        Right dcname <- dataConInfoPtrToName (infoPtr clos)
        (_,mb_dc)    <- tryTcErrs (tcLookupDataCon dcname)
        case mb_dc of
          Nothing -> do -- This can happen for private constructors compiled -O0
                        -- where the .hi descriptor does not export them
                        -- In such case, we return a best approximation:
                        --  ignore the unpointed args, and recover the pointeds
                        -- This preserves laziness, and should be safe.
                       let tag = showSDoc (ppr dcname)
                       vars     <- replicateM (length$ elems$ ptrs clos) 
                                              (newVar (liftedTypeKind))
pepe's avatar
pepe committed
697
                       subTerms <- sequence [appArr (go (pred max_depth) tv tv) (ptrs clos) i 
698
                                              | (i, tv) <- zip [0..] vars]
pepe's avatar
pepe committed
699
700
701
702
703
704
                       return (Term my_ty (Left ('<' : tag ++ ">")) a subTerms)
          Just dc -> do
            let subTtypes  = matchSubTypes dc old_ty
            subTermTvs    <- mapMif (not . isMonomorphic)
                                    (\t -> newVar (typeKind t))
                                    subTtypes
mnislaih's avatar
mnislaih committed
705
706
707
708
709
710
711
712
713
            let (subTermsP, subTermsNP) = partition (\(ty,_) -> isLifted ty
                                                             || isRefType ty)
                                                    (zip subTtypes subTermTvs)
                (subTtypesP,   subTermTvsP ) = unzip subTermsP
                (subTtypesNP, _subTermTvsNP) = unzip subTermsNP

            -- When we already have all the information, avoid solving
            -- unnecessary constraints. Propagation of type information
            -- to subterms is already being done via matching.
714
            when (not monomorphic) $ do
pepe's avatar
pepe committed
715
               let myType = mkFunTys subTermTvs my_ty
mnislaih's avatar
mnislaih committed
716
               (signatureType,_) <- instScheme (mydataConType dc)
mnislaih's avatar
mnislaih committed
717
718
            -- It is vital for newtype reconstruction that the unification step
            -- is done right here, _before_ the subterms are RTTI reconstructed
pepe's avatar
pepe committed
719
720
721
               addConstraint myType signatureType
            subTermsP <- sequence
                  [ appArr (go (pred max_depth) tv t) (ptrs clos) i
mnislaih's avatar
mnislaih committed
722
                   | (i,tv,t) <- zip3 [0..] subTermTvsP subTtypesP]
723
            let unboxeds   = extractUnboxed subTtypesNP clos
mnislaih's avatar
mnislaih committed
724
                subTermsNP = map (uncurry Prim) (zip subTtypesNP unboxeds)
pepe's avatar
pepe committed
725
726
                subTerms   = reOrderTerms subTermsP subTermsNP subTtypes
            return (Term my_ty (Right dc) a subTerms)
727
-- The otherwise case: can be a Thunk,AP,PAP,etc.
728
      tipe_clos ->
pepe's avatar
pepe committed
729
         return (Suspension tipe_clos my_ty a Nothing)
730

731
  matchSubTypes dc ty
pepe's avatar
pepe committed
732
733
734
735
736
737
738
    | ty' <- repType ty     -- look through newtypes
    , Just (tc,ty_args) <- tcSplitTyConApp_maybe ty'
    , dc `elem` tyConDataCons tc
      -- It is necessary to check that dc is actually a constructor for tycon tc,
      -- because it may be the case that tc is a recursive newtype and tcSplitTyConApp
      -- has not removed it. In that case, we happily give up and don't match
    = myDataConInstArgTys dc ty_args
739
    | otherwise = dataConRepArgTys dc
740

pepe's avatar
pepe committed
741
742
  -- put together pointed and nonpointed subterms in the
  --  correct order.
743
744
  reOrderTerms _ _ [] = []
  reOrderTerms pointed unpointed (ty:tys) 
pepe's avatar
pepe committed
745
746
   | isLifted ty || isRefType ty
                  = ASSERT2(not(null pointed)
747
                            , ptext (sLit "reOrderTerms") $$ 
748
                                        (ppr pointed $$ ppr unpointed))
749
                    let (t:tt) = pointed in t : reOrderTerms tt unpointed tys
mnislaih's avatar
mnislaih committed
750
   | otherwise    = ASSERT2(not(null unpointed)
mnislaih's avatar
mnislaih committed
751
                           , ptext (sLit "reOrderTerms") $$ 
752
                                       (ppr pointed $$ ppr unpointed))
753
                    let (t:tt) = unpointed in t : reOrderTerms pointed tt tys
754

pepe's avatar
pepe committed
755
756
757
758
759
760
761
762
763
764
765
  -- insert NewtypeWraps around newtypes
  expandNewtypes = foldTerm idTermFold { fTerm = worker } where
   worker ty dc hval tt
     | Just (tc, args) <- tcSplitTyConApp_maybe ty
     , isNewTyCon tc
     , wrapped_type    <- newTyConInstRhs tc args
     , Just dc'        <- tyConSingleDataCon_maybe tc
     , t'              <- worker wrapped_type dc hval tt
     = NewtypeWrap ty (Right dc') t'
     | otherwise = Term ty dc hval tt

766

pepe's avatar
pepe committed
767
768
769
770
   -- Avoid returning types where predicates have been expanded to dictionaries.
  fixFunDictionaries = foldTerm idTermFold {fSuspension = worker} where
      worker ct ty hval n | isFunTy ty = Suspension ct (dictsView ty) hval n
                          | otherwise  = Suspension ct ty hval n
mnislaih's avatar
mnislaih committed
771

772

773
-- Fast, breadth-first Type reconstruction
774
------------------------------------------
pepe's avatar
pepe committed
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
cvReconstructType :: HscEnv -> Int -> GhciType -> HValue -> IO (Maybe Type)
cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
   traceTR (text "RTTI started with initial type " <> ppr old_ty)
   let sigma_old_ty = sigmaType old_ty
   new_ty <-
       if isMonomorphic sigma_old_ty
        then return old_ty
        else do
          (old_ty', rev_subst) <- instScheme sigma_old_ty
          my_ty <- newVar argTypeKind
          when (check1 sigma_old_ty) (traceTR (text "check1 passed") >>
                                      addConstraint my_ty old_ty')
          search (isMonomorphic `fmap` zonkTcType my_ty)
                 (\(ty,a) -> go ty a)
                 (Seq.singleton (my_ty, hval))
                 max_depth
          new_ty <- zonkTcType my_ty
          if isMonomorphic new_ty || check2 (sigmaType new_ty) sigma_old_ty
            then do
                 traceTR (text "check2 passed")
                 addConstraint my_ty old_ty'
                 new_ty' <- zonkTcType my_ty
                 return (substTy rev_subst new_ty')
            else traceTR (text "check2 failed" <+> parens (ppr new_ty)) >>
                 return old_ty
   traceTR (text "RTTI completed. Type obtained:" <+> ppr new_ty)
   return new_ty
    where
803
--  search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m ()
804
805
  search _ _ _ 0 = traceTR (text "Failed to reconstruct a type after " <>
                                int max_depth <> text " steps")
mnislaih's avatar
mnislaih committed
806
807
808
809
810
811
  search stop expand l d =
    case viewl l of 
      EmptyL  -> return ()
      x :< xx -> unlessM stop $ do
                  new <- expand x
                  search stop expand (xx `mappend` Seq.fromList new) $! (pred d)
812

813
   -- returns unification tasks,since we are going to want a breadth-first search
814
  go :: Type -> HValue -> TR [(Type, HValue)]
pepe's avatar
pepe committed
815
  go my_ty a = do
816
817
    clos <- trIO $ getClosureData a
    case tipe clos of
pepe's avatar
pepe committed
818
      Indirection _ -> go my_ty $! (ptrs clos ! 0)
819
820
821
822
      MutVar _ -> do
         contents <- trIO$ IO$ \w -> readMutVar# (unsafeCoerce# a) w
         tv'   <- newVar liftedTypeKind
         world <- newVar liftedTypeKind
pepe's avatar
pepe committed
823
         addConstraint my_ty (mkTyConApp mutVarPrimTyCon [world,tv'])
824
         return [(tv', contents)]
825
      Constr -> do
mnislaih's avatar
mnislaih committed
826
827
828
        Right dcname <- dataConInfoPtrToName (infoPtr clos)
        (_,mb_dc)    <- tryTcErrs (tcLookupDataCon dcname)
        case mb_dc of
829
          Nothing-> do
mnislaih's avatar
mnislaih committed
830
                     --  TODO: Check this case
831
            forM [0..length (elems $ ptrs clos)] $ \i -> do
832
                        tv <- newVar liftedTypeKind
833
834
                        return$ appArr (\e->(tv,e)) (ptrs clos) i

835
          Just dc -> do
836
            subTtypes <- mapMif (not . isMonomorphic)
837
                                (\t -> newVar (typeKind t))
838
                                (dataConRepArgTys dc)
839

840
841
            -- It is vital for newtype reconstruction that the unification step
            -- is done right here, _before_ the subterms are RTTI reconstructed
pepe's avatar
pepe committed
842
            let myType         = mkFunTys subTtypes my_ty
mnislaih's avatar
mnislaih committed
843
            (signatureType,_) <- instScheme(mydataConType dc)
844
            addConstraint myType signatureType
845
            return $ [ appArr (\e->(t,e)) (ptrs clos) i
pepe's avatar
pepe committed
846
                       | (i,t) <- zip [0..] (filter (isLifted |.| isRefType) subTtypes)]
mnislaih's avatar
mnislaih committed
847
      _ -> return []
848

849
850
851
852
-- Compute the difference between a base type and the type found by RTTI
-- improveType <base_type> <rtti_type>
-- The types can contain skolem type variables, which need to be treated as normal vars.
-- In particular, we want them to unify with things.
pepe's avatar
pepe committed
853
854
improveRTTIType :: HscEnv -> RttiType -> RttiType -> IO (Maybe TvSubst)
improveRTTIType hsc_env _ty rtti_ty = runTR_maybe hsc_env $ do
mnislaih's avatar
mnislaih committed
855
    traceTR (text "improveRttiType" <+> fsep [ppr _ty, ppr rtti_ty])
pepe's avatar
pepe committed
856
857
858
    (ty_tvs,  _, _)   <- tcInstType return ty
    (ty_tvs', _, ty') <- tcInstType (mapM tcInstTyVar) ty
    (_, _, rtti_ty')  <- tcInstType (mapM tcInstTyVar) (sigmaType rtti_ty)
859
    getLIE(boxyUnify rtti_ty' ty')
pepe's avatar
pepe committed
860
861
862
863
864
865
    tvs1_contents     <- zonkTcTyVars ty_tvs'
    let subst = (uncurry zipTopTvSubst . unzip)
                 [(tv,ty) | (tv,ty) <- zip ty_tvs tvs1_contents
                          , getTyVar_maybe ty /= Just tv
                          --, not(isTyVarTy ty)
                          ]
866
    return subst
pepe's avatar
pepe committed
867
868
869
870
871
872
873
 where ty = sigmaType _ty

myDataConInstArgTys :: DataCon -> [Type] -> [Type]
myDataConInstArgTys dc args
    | null (dataConExTyVars dc) && null (dataConEqTheta dc) = dataConInstArgTys dc args
    | otherwise = dataConRepArgTys dc

mnislaih's avatar
mnislaih committed
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
mydataConType :: DataCon -> Type
-- ^ Custom version of DataCon.dataConUserType where we
--    - remove the equality constraints
--    - use the representation types for arguments, including dictionaries
--    - keep the original result type
mydataConType  dc
  = mkForAllTys ((univ_tvs `minusList` map fst eq_spec) ++ ex_tvs) $
    mkFunTys arg_tys $
    res_ty
  where univ_tvs   = dataConUnivTyVars dc
        ex_tvs     = dataConExTyVars dc
        eq_spec    = dataConEqSpec dc
        arg_tys    = [case a of
                        PredTy p -> predTypeRep p
                        _        -> a
                     | a <- dataConRepArgTys dc]
        res_ty     = dataConOrigResTy dc

pepe's avatar
pepe committed
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
isRefType :: Type -> Bool
isRefType ty
   | Just (tc, _) <- tcSplitTyConApp_maybe ty' = isRefTyCon tc
   | otherwise = False
  where ty'= repType ty

isRefTyCon :: TyCon -> Bool
isRefTyCon tc = tc `elem` [mutVarPrimTyCon, mVarPrimTyCon, tVarPrimTyCon]

-- Soundness checks
--------------------
{-
This is not formalized anywhere, so hold to your seats!
RTTI in the presence of newtypes can be a tricky and unsound business.

Example:
~~~~~~~~~
Suppose we are doing RTTI for a partially evaluated
closure t, the real type of which is t :: MkT Int, for

   newtype MkT a = MkT [Maybe a]

The table below shows the results of RTTI and the improvement
calculated for different combinations of evaluatedness and :type t.
Regard the two first columns as input and the next two as output.

  # |     t     |  :type t  | rtti(t)  | improv.    | result
    ------------------------------------------------------------
  1 |     _     |    t b    |    a     | none       | OK
  2 |     _     |   MkT b   |    a     | none       | OK
  3 |     _     |   t Int   |    a     | none       | OK

  If t is not evaluated at *all*, we are safe.

  4 |  (_ : _)  |    t b    |   [a]    | t = []     | UNSOUND
  5 |  (_ : _)  |   MkT b   |  MkT a   | none       | OK (compensating for the missing newtype)
  6 |  (_ : _)  |   t Int   |  [Int]   | t = []     | UNSOUND

  If a is a minimal whnf, we run into trouble. Note that
  row 5 above does newtype enrichment on the ty_rtty parameter.

  7 | (Just _:_)|    t b    |[Maybe a] | t = [],    | UNSOUND
    |                       |          | b = Maybe a|

  8 | (Just _:_)|   MkT b   |  MkT a   |  none      | OK
  9 | (Just _:_)|   t Int   |   FAIL   |  none      | OK

  And if t is any more evaluated than whnf, we are still in trouble.
  Because constraints are solved in top-down order, when we reach the
  Maybe subterm what we got is already unsound. This explains why the
  row 9 fails to complete.

  10 | (Just _:_)|  t Int  | [Maybe a]   |  FAIL    | OK
  11 | (Just 1:_)|  t Int  | [Maybe Int] |  FAIL    | OK

  We can undo the failure in row 9 by leaving out the constraint
  coming from the type signature of t (i.e., the 2nd column).
  Note that this type information is still used
  to calculate the improvement. But we fail
  when trying to calculate the improvement, as there is no unifier for
  t Int = [Maybe a] or t Int = [Maybe Int].


  Another set of examples with t :: [MkT (Maybe Int)]  \equiv  [[Maybe (Maybe Int)]]

  # |     t     |    :type t    |  rtti(t)    | improvement | result
    ---------------------------------------------------------------------
  1 |(Just _:_) | [t (Maybe a)] | [[Maybe b]] | t = []      |
    |           |               |             | b = Maybe a |

The checks:
~~~~~~~~~~~
Consider a function obtainType that takes a value and a type and produces
the Term representation and a substitution (the improvement).
Assume an auxiliar rtti' function which does the actual job if recovering
the type, but which may produce a false type.

In pseudocode:

  rtti' :: a -> IO Type  -- Does not use the static type information

  obtainType :: a -> Type -> IO (Maybe (Term, Improvement))
  obtainType v old_ty = do
       rtti_ty <- rtti' v
       if monomorphic rtti_ty || (check rtti_ty old_ty)
        then ...
         else return Nothing
  where check rtti_ty old_ty = check1 rtti_ty &&
                              check2 rtti_ty old_ty

  check1 :: Type -> Bool
  check2 :: Type -> Type -> Bool

Now, if rtti' returns a monomorphic type, we are safe.
If that is not the case, then we consider two conditions.


1. To prevent the class of unsoundness displayed by
   rows 4 and 7 in the example: no higher kind tyvars
   accepted.

  check1 (t a)   = NO
  check1 (t Int) = NO
  check1 ([] a)  = YES

2. To prevent the class of unsoundness shown by row 6,
   the rtti type should be structurally more
   defined than the old type we are comparing it to.
mnislaih's avatar
mnislaih committed
1000
  check2 :: NewType -> OldType -> Bool