Export `Monoid(..)`/`Foldable(..)`/`Traversable(..)` from Prelude
[ghc.git] / compiler / ghci / RtClosureInspect.hs
1 {-# LANGUAGE CPP, ScopedTypeVariables, MagicHash, UnboxedTuples #-}
2
3 -----------------------------------------------------------------------------
4 --
5 -- GHC Interactive support for inspecting arbitrary closures at runtime
6 --
7 -- Pepe Iborra (supported by Google SoC) 2006
8 --
9 -----------------------------------------------------------------------------
10 module RtClosureInspect(
11 cvObtainTerm, -- :: HscEnv -> Int -> Bool -> Maybe Type -> HValue -> IO Term
12 cvReconstructType,
13 improveRTTIType,
14
15 Term(..),
16 isTerm, isSuspension, isPrim, isFun, isFunLike, isNewtypeWrap,
17 isFullyEvaluated, isFullyEvaluatedTerm,
18 termType, mapTermType, termTyVars,
19 foldTerm, TermFold(..), foldTermM, TermFoldM(..), idTermFold,
20 pprTerm, cPprTerm, cPprTermBase, CustomTermPrinter,
21
22 -- unsafeDeepSeq,
23
24 Closure(..), getClosureData, ClosureType(..), isConstr, isIndirection
25 ) where
26
27 #include "HsVersions.h"
28
29 import DebuggerUtils
30 import ByteCodeItbls ( StgInfoTable, peekItbl )
31 import qualified ByteCodeItbls as BCI( StgInfoTable(..) )
32 import BasicTypes ( HValue )
33 import HscTypes
34
35 import DataCon
36 import Type
37 import qualified Unify as U
38 import Var
39 import TcRnMonad
40 import TcType
41 import TcMType
42 import TcHsSyn ( zonkTcTypeToType, mkEmptyZonkEnv )
43 import TcUnify
44 import TcEnv
45
46 import TyCon
47 import Name
48 import VarEnv
49 import Util
50 import VarSet
51 import BasicTypes ( TupleSort(UnboxedTuple) )
52 import TysPrim
53 import PrelNames
54 import TysWiredIn
55 import DynFlags
56 import Outputable as Ppr
57 import GHC.Arr ( Array(..) )
58 import GHC.Exts
59 import GHC.IO ( IO(..) )
60
61 import StaticFlags( opt_PprStyle_Debug )
62 import Control.Monad
63 import Data.Maybe
64 import Data.Array.Base
65 import Data.Ix
66 import Data.List
67 import qualified Data.Sequence as Seq
68 #if __GLASGOW_HASKELL__ < 709
69 import Data.Monoid (mappend)
70 #endif
71 import Data.Sequence (viewl, ViewL(..))
72 import Foreign.Safe
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 :: DynFlags -> a -> IO Closure
171 getClosureData dflags 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 dflags)
184 itbl <- peekItbl dflags 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)-1] ]
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 :: DynFlags -> a -> IO Bool
223 isFullyEvaluated dflags a = do
224 closure <- getClosureData dflags a
225 case tipe closure of
226 Constr -> do are_subs_evaluated <- amapM (isFullyEvaluated dflags) (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)
343 (text dc_tag <+> pprDeeperList fsep tt_docs)
344
345 ppr_termM y p Term{dc=Right dc, subTerms=tt}
346 {- | dataConIsInfix dc, (t1:t2:tt') <- tt --TODO fixity
347 = parens (ppr_term1 True t1 <+> ppr dc <+> ppr_term1 True ppr t2)
348 <+> hsep (map (ppr_term1 True) tt)
349 -} -- TODO Printing infix constructors properly
350 | null sub_terms_to_show
351 = return (ppr dc)
352 | otherwise
353 = do { tt_docs <- mapM (y app_prec) sub_terms_to_show
354 ; return $ cparen (p >= app_prec) $
355 sep [ppr dc, nest 2 (pprDeeperList fsep tt_docs)] }
356 where
357 sub_terms_to_show -- Don't show the dictionary arguments to
358 -- constructors unless -dppr-debug is on
359 | opt_PprStyle_Debug = tt
360 | otherwise = dropList (dataConTheta dc) tt
361
362 ppr_termM y p t@NewtypeWrap{} = pprNewtypeWrap y p t
363 ppr_termM y p RefWrap{wrapped_term=t} = do
364 contents <- y app_prec t
365 return$ cparen (p >= app_prec) (text "GHC.Prim.MutVar#" <+> contents)
366 -- The constructor name is wired in here ^^^ for the sake of simplicity.
367 -- I don't think mutvars are going to change in a near future.
368 -- In any case this is solely a presentation matter: MutVar# is
369 -- a datatype with no constructors, implemented by the RTS
370 -- (hence there is no way to obtain a datacon and print it).
371 ppr_termM _ _ t = ppr_termM1 t
372
373
374 ppr_termM1 :: Monad m => Term -> m SDoc
375 ppr_termM1 Prim{value=words, ty=ty} =
376 return $ repPrim (tyConAppTyCon ty) words
377 ppr_termM1 Suspension{ty=ty, bound_to=Nothing} =
378 return (char '_' <+> ifPprDebug (text "::" <> ppr ty))
379 ppr_termM1 Suspension{ty=ty, bound_to=Just n}
380 -- | Just _ <- splitFunTy_maybe ty = return$ ptext (sLit("<function>")
381 | otherwise = return$ parens$ ppr n <> text "::" <> ppr ty
382 ppr_termM1 Term{} = panic "ppr_termM1 - Term"
383 ppr_termM1 RefWrap{} = panic "ppr_termM1 - RefWrap"
384 ppr_termM1 NewtypeWrap{} = panic "ppr_termM1 - NewtypeWrap"
385
386 pprNewtypeWrap y p NewtypeWrap{ty=ty, wrapped_term=t}
387 | Just (tc,_) <- tcSplitTyConApp_maybe ty
388 , ASSERT(isNewTyCon tc) True
389 , Just new_dc <- tyConSingleDataCon_maybe tc = do
390 real_term <- y max_prec t
391 return $ cparen (p >= app_prec) (ppr new_dc <+> real_term)
392 pprNewtypeWrap _ _ _ = panic "pprNewtypeWrap"
393
394 -------------------------------------------------------
395 -- Custom Term Pretty Printers
396 -------------------------------------------------------
397
398 -- We can want to customize the representation of a
399 -- term depending on its type.
400 -- However, note that custom printers have to work with
401 -- type representations, instead of directly with types.
402 -- We cannot use type classes here, unless we employ some
403 -- typerep trickery (e.g. Weirich's RepLib tricks),
404 -- which I didn't. Therefore, this code replicates a lot
405 -- of what type classes provide for free.
406
407 type CustomTermPrinter m = TermPrinterM m
408 -> [Precedence -> Term -> (m (Maybe SDoc))]
409
410 -- | Takes a list of custom printers with a explicit recursion knot and a term,
411 -- and returns the output of the first successful printer, or the default printer
412 cPprTerm :: Monad m => CustomTermPrinter m -> Term -> m SDoc
413 cPprTerm printers_ = go 0 where
414 printers = printers_ go
415 go prec t = do
416 let default_ = Just `liftM` pprTermM go prec t
417 mb_customDocs = [pp prec t | pp <- printers] ++ [default_]
418 Just doc <- firstJustM mb_customDocs
419 return$ cparen (prec>app_prec+1) doc
420
421 firstJustM (mb:mbs) = mb >>= maybe (firstJustM mbs) (return . Just)
422 firstJustM [] = return Nothing
423
424 -- Default set of custom printers. Note that the recursion knot is explicit
425 cPprTermBase :: forall m. Monad m => CustomTermPrinter m
426 cPprTermBase y =
427 [ ifTerm (isTupleTy.ty) (\_p -> liftM (parens . hcat . punctuate comma)
428 . mapM (y (-1))
429 . subTerms)
430 , ifTerm (\t -> isTyCon listTyCon (ty t) && subTerms t `lengthIs` 2)
431 ppr_list
432 , ifTerm (isTyCon intTyCon . ty) ppr_int
433 , ifTerm (isTyCon charTyCon . ty) ppr_char
434 , ifTerm (isTyCon floatTyCon . ty) ppr_float
435 , ifTerm (isTyCon doubleTyCon . ty) ppr_double
436 , ifTerm (isIntegerTy . ty) ppr_integer
437 ]
438 where
439 ifTerm :: (Term -> Bool)
440 -> (Precedence -> Term -> m SDoc)
441 -> Precedence -> Term -> m (Maybe SDoc)
442 ifTerm pred f prec t@Term{}
443 | pred t = Just `liftM` f prec t
444 ifTerm _ _ _ _ = return Nothing
445
446 isTupleTy ty = fromMaybe False $ do
447 (tc,_) <- tcSplitTyConApp_maybe ty
448 return (isBoxedTupleTyCon tc)
449
450 isTyCon a_tc ty = fromMaybe False $ do
451 (tc,_) <- tcSplitTyConApp_maybe ty
452 return (a_tc == tc)
453
454 isIntegerTy ty = fromMaybe False $ do
455 (tc,_) <- tcSplitTyConApp_maybe ty
456 return (tyConName tc == integerTyConName)
457
458 ppr_int, ppr_char, ppr_float, ppr_double, ppr_integer
459 :: Precedence -> Term -> m SDoc
460 ppr_int _ v = return (Ppr.int (unsafeCoerce# (val v)))
461 ppr_char _ v = return (Ppr.char '\'' <> Ppr.char (unsafeCoerce# (val v)) <> Ppr.char '\'')
462 ppr_float _ v = return (Ppr.float (unsafeCoerce# (val v)))
463 ppr_double _ v = return (Ppr.double (unsafeCoerce# (val v)))
464 ppr_integer _ v = return (Ppr.integer (unsafeCoerce# (val v)))
465
466 --Note pprinting of list terms is not lazy
467 ppr_list :: Precedence -> Term -> m SDoc
468 ppr_list p (Term{subTerms=[h,t]}) = do
469 let elems = h : getListTerms t
470 isConsLast = not(termType(last elems) `eqType` termType h)
471 is_string = all (isCharTy . ty) elems
472
473 print_elems <- mapM (y cons_prec) elems
474 if is_string
475 then return (Ppr.doubleQuotes (Ppr.text (unsafeCoerce# (map val elems))))
476 else if isConsLast
477 then return $ cparen (p >= cons_prec)
478 $ pprDeeperList fsep
479 $ punctuate (space<>colon) print_elems
480 else return $ brackets
481 $ pprDeeperList fcat
482 $ punctuate comma print_elems
483
484 where getListTerms Term{subTerms=[h,t]} = h : getListTerms t
485 getListTerms Term{subTerms=[]} = []
486 getListTerms t@Suspension{} = [t]
487 getListTerms t = pprPanic "getListTerms" (ppr t)
488 ppr_list _ _ = panic "doList"
489
490
491 repPrim :: TyCon -> [Word] -> SDoc
492 repPrim t = rep where
493 rep x
494 | t == charPrimTyCon = text $ show (build x :: Char)
495 | t == intPrimTyCon = text $ show (build x :: Int)
496 | t == wordPrimTyCon = text $ show (build x :: Word)
497 | t == floatPrimTyCon = text $ show (build x :: Float)
498 | t == doublePrimTyCon = text $ show (build x :: Double)
499 | t == int32PrimTyCon = text $ show (build x :: Int32)
500 | t == word32PrimTyCon = text $ show (build x :: Word32)
501 | t == int64PrimTyCon = text $ show (build x :: Int64)
502 | t == word64PrimTyCon = text $ show (build x :: Word64)
503 | t == addrPrimTyCon = text $ show (nullPtr `plusPtr` build x)
504 | t == stablePtrPrimTyCon = text "<stablePtr>"
505 | t == stableNamePrimTyCon = text "<stableName>"
506 | t == statePrimTyCon = text "<statethread>"
507 | t == proxyPrimTyCon = text "<proxy>"
508 | t == realWorldTyCon = text "<realworld>"
509 | t == threadIdPrimTyCon = text "<ThreadId>"
510 | t == weakPrimTyCon = text "<Weak>"
511 | t == arrayPrimTyCon = text "<array>"
512 | t == smallArrayPrimTyCon = text "<smallArray>"
513 | t == byteArrayPrimTyCon = text "<bytearray>"
514 | t == mutableArrayPrimTyCon = text "<mutableArray>"
515 | t == smallMutableArrayPrimTyCon = text "<smallMutableArray>"
516 | t == mutableByteArrayPrimTyCon = text "<mutableByteArray>"
517 | t == mutVarPrimTyCon = text "<mutVar>"
518 | t == mVarPrimTyCon = text "<mVar>"
519 | t == tVarPrimTyCon = text "<tVar>"
520 | otherwise = char '<' <> ppr t <> char '>'
521 where build ww = unsafePerformIO $ withArray ww (peek . castPtr)
522 -- This ^^^ relies on the representation of Haskell heap values being
523 -- the same as in a C array.
524
525 -----------------------------------
526 -- Type Reconstruction
527 -----------------------------------
528 {-
529 Type Reconstruction is type inference done on heap closures.
530 The algorithm walks the heap generating a set of equations, which
531 are solved with syntactic unification.
532 A type reconstruction equation looks like:
533
534 <datacon reptype> = <actual heap contents>
535
536 The full equation set is generated by traversing all the subterms, starting
537 from a given term.
538
539 The only difficult part is that newtypes are only found in the lhs of equations.
540 Right hand sides are missing them. We can either (a) drop them from the lhs, or
541 (b) reconstruct them in the rhs when possible.
542
543 The function congruenceNewtypes takes a shot at (b)
544 -}
545
546
547 -- A (non-mutable) tau type containing
548 -- existentially quantified tyvars.
549 -- (since GHC type language currently does not support
550 -- existentials, we leave these variables unquantified)
551 type RttiType = Type
552
553 -- An incomplete type as stored in GHCi:
554 -- no polymorphism: no quantifiers & all tyvars are skolem.
555 type GhciType = Type
556
557
558 -- The Type Reconstruction monad
559 --------------------------------
560 type TR a = TcM a
561
562 runTR :: HscEnv -> TR a -> IO a
563 runTR hsc_env thing = do
564 mb_val <- runTR_maybe hsc_env thing
565 case mb_val of
566 Nothing -> error "unable to :print the term"
567 Just x -> return x
568
569 runTR_maybe :: HscEnv -> TR a -> IO (Maybe a)
570 runTR_maybe hsc_env thing_inside
571 = do { (_errs, res) <- initTc hsc_env HsSrcFile False
572 (icInteractiveModule (hsc_IC hsc_env))
573 thing_inside
574 ; return res }
575
576 traceTR :: SDoc -> TR ()
577 traceTR = liftTcM . traceOptTcRn Opt_D_dump_rtti
578
579
580 -- Semantically different to recoverM in TcRnMonad
581 -- recoverM retains the errors in the first action,
582 -- whereas recoverTc here does not
583 recoverTR :: TR a -> TR a -> TR a
584 recoverTR recover thing = do
585 (_,mb_res) <- tryTcErrs thing
586 case mb_res of
587 Nothing -> recover
588 Just res -> return res
589
590 trIO :: IO a -> TR a
591 trIO = liftTcM . liftIO
592
593 liftTcM :: TcM a -> TR a
594 liftTcM = id
595
596 newVar :: Kind -> TR TcType
597 newVar = liftTcM . newFlexiTyVarTy
598
599 instTyVars :: [TyVar] -> TR ([TcTyVar], [TcType], TvSubst)
600 -- Instantiate fresh mutable type variables from some TyVars
601 -- This function preserves the print-name, which helps error messages
602 instTyVars = liftTcM . tcInstTyVars
603
604 type RttiInstantiation = [(TcTyVar, TyVar)]
605 -- Associates the typechecker-world meta type variables
606 -- (which are mutable and may be refined), to their
607 -- debugger-world RuntimeUnk counterparts.
608 -- If the TcTyVar has not been refined by the runtime type
609 -- elaboration, then we want to turn it back into the
610 -- original RuntimeUnk
611
612 -- | Returns the instantiated type scheme ty', and the
613 -- mapping from new (instantiated) -to- old (skolem) type variables
614 instScheme :: QuantifiedType -> TR (TcType, RttiInstantiation)
615 instScheme (tvs, ty)
616 = liftTcM $ do { (tvs', _, subst) <- tcInstTyVars tvs
617 ; let rtti_inst = [(tv',tv) | (tv',tv) <- tvs' `zip` tvs]
618 ; return (substTy subst ty, rtti_inst) }
619
620 applyRevSubst :: RttiInstantiation -> TR ()
621 -- Apply the *reverse* substitution in-place to any un-filled-in
622 -- meta tyvars. This recovers the original debugger-world variable
623 -- unless it has been refined by new information from the heap
624 applyRevSubst pairs = liftTcM (mapM_ do_pair pairs)
625 where
626 do_pair (tc_tv, rtti_tv)
627 = do { tc_ty <- zonkTcTyVar tc_tv
628 ; case tcGetTyVar_maybe tc_ty of
629 Just tv | isMetaTyVar tv -> writeMetaTyVar tv (mkTyVarTy rtti_tv)
630 _ -> return () }
631
632 -- Adds a constraint of the form t1 == t2
633 -- t1 is expected to come from walking the heap
634 -- t2 is expected to come from a datacon signature
635 -- Before unification, congruenceNewtypes needs to
636 -- do its magic.
637 addConstraint :: TcType -> TcType -> TR ()
638 addConstraint actual expected = do
639 traceTR (text "add constraint:" <+> fsep [ppr actual, equals, ppr expected])
640 recoverTR (traceTR $ fsep [text "Failed to unify", ppr actual,
641 text "with", ppr expected]) $
642 do { (ty1, ty2) <- congruenceNewtypes actual expected
643 ; _ <- captureConstraints $ unifyType ty1 ty2
644 ; return () }
645 -- TOMDO: what about the coercion?
646 -- we should consider family instances
647
648
649 -- Type & Term reconstruction
650 ------------------------------
651 cvObtainTerm :: HscEnv -> Int -> Bool -> RttiType -> HValue -> IO Term
652 cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
653 -- we quantify existential tyvars as universal,
654 -- as this is needed to be able to manipulate
655 -- them properly
656 let quant_old_ty@(old_tvs, old_tau) = quantifyType old_ty
657 sigma_old_ty = mkForAllTys old_tvs old_tau
658 traceTR (text "Term reconstruction started with initial type " <> ppr old_ty)
659 term <-
660 if null old_tvs
661 then do
662 term <- go max_depth sigma_old_ty sigma_old_ty hval
663 term' <- zonkTerm term
664 return $ fixFunDictionaries $ expandNewtypes term'
665 else do
666 (old_ty', rev_subst) <- instScheme quant_old_ty
667 my_ty <- newVar openTypeKind
668 when (check1 quant_old_ty) (traceTR (text "check1 passed") >>
669 addConstraint my_ty old_ty')
670 term <- go max_depth my_ty sigma_old_ty hval
671 new_ty <- zonkTcType (termType term)
672 if isMonomorphic new_ty || check2 (quantifyType new_ty) quant_old_ty
673 then do
674 traceTR (text "check2 passed")
675 addConstraint new_ty old_ty'
676 applyRevSubst rev_subst
677 zterm' <- zonkTerm term
678 return ((fixFunDictionaries . expandNewtypes) zterm')
679 else do
680 traceTR (text "check2 failed" <+> parens
681 (ppr term <+> text "::" <+> ppr new_ty))
682 -- we have unsound types. Replace constructor types in
683 -- subterms with tyvars
684 zterm' <- mapTermTypeM
685 (\ty -> case tcSplitTyConApp_maybe ty of
686 Just (tc, _:_) | tc /= funTyCon
687 -> newVar openTypeKind
688 _ -> return ty)
689 term
690 zonkTerm zterm'
691 traceTR (text "Term reconstruction completed." $$
692 text "Term obtained: " <> ppr term $$
693 text "Type obtained: " <> ppr (termType term))
694 return term
695 where
696 dflags = hsc_dflags hsc_env
697
698 go :: Int -> Type -> Type -> HValue -> TcM Term
699 -- I believe that my_ty should not have any enclosing
700 -- foralls, nor any free RuntimeUnk skolems;
701 -- that is partly what the quantifyType stuff achieved
702 --
703 -- [SPJ May 11] I don't understand the difference between my_ty and old_ty
704
705 go max_depth _ _ _ | seq max_depth False = undefined
706 go 0 my_ty _old_ty a = do
707 traceTR (text "Gave up reconstructing a term after" <>
708 int max_depth <> text " steps")
709 clos <- trIO $ getClosureData dflags a
710 return (Suspension (tipe clos) my_ty a Nothing)
711 go max_depth my_ty old_ty a = do
712 let monomorphic = not(isTyVarTy my_ty)
713 -- This ^^^ is a convention. The ancestor tests for
714 -- monomorphism and passes a type instead of a tv
715 clos <- trIO $ getClosureData dflags a
716 case tipe clos of
717 -- Thunks we may want to force
718 t | isThunk t && force -> traceTR (text "Forcing a " <> text (show t)) >>
719 seq a (go (pred max_depth) my_ty old_ty a)
720 -- Blackholes are indirections iff the payload is not TSO or BLOCKING_QUEUE. So we
721 -- treat them like indirections; if the payload is TSO or BLOCKING_QUEUE, we'll end up
722 -- showing '_' which is what we want.
723 Blackhole -> do traceTR (text "Following a BLACKHOLE")
724 appArr (go max_depth my_ty old_ty) (ptrs clos) 0
725 -- We always follow indirections
726 Indirection i -> do traceTR (text "Following an indirection" <> parens (int i) )
727 go max_depth my_ty old_ty $! (ptrs clos ! 0)
728 -- We also follow references
729 MutVar _ | Just (tycon,[world,contents_ty]) <- tcSplitTyConApp_maybe old_ty
730 -> do
731 -- Deal with the MutVar# primitive
732 -- It does not have a constructor at all,
733 -- so we simulate the following one
734 -- MutVar# :: contents_ty -> MutVar# s contents_ty
735 traceTR (text "Following a MutVar")
736 contents_tv <- newVar liftedTypeKind
737 contents <- trIO$ IO$ \w -> readMutVar# (unsafeCoerce# a) w
738 ASSERT(isUnliftedTypeKind $ typeKind my_ty) return ()
739 (mutvar_ty,_) <- instScheme $ quantifyType $ mkFunTy
740 contents_ty (mkTyConApp tycon [world,contents_ty])
741 addConstraint (mkFunTy contents_tv my_ty) mutvar_ty
742 x <- go (pred max_depth) contents_tv contents_ty contents
743 return (RefWrap my_ty x)
744
745 -- The interesting case
746 Constr -> do
747 traceTR (text "entering a constructor " <>
748 if monomorphic
749 then parens (text "already monomorphic: " <> ppr my_ty)
750 else Ppr.empty)
751 Right dcname <- dataConInfoPtrToName (infoPtr clos)
752 (_,mb_dc) <- tryTcErrs (tcLookupDataCon dcname)
753 case mb_dc of
754 Nothing -> do -- This can happen for private constructors compiled -O0
755 -- where the .hi descriptor does not export them
756 -- In such case, we return a best approximation:
757 -- ignore the unpointed args, and recover the pointeds
758 -- This preserves laziness, and should be safe.
759 traceTR (text "Not constructor" <+> ppr dcname)
760 let dflags = hsc_dflags hsc_env
761 tag = showPpr dflags dcname
762 vars <- replicateM (length$ elems$ ptrs clos)
763 (newVar liftedTypeKind)
764 subTerms <- sequence [appArr (go (pred max_depth) tv tv) (ptrs clos) i
765 | (i, tv) <- zip [0..] vars]
766 return (Term my_ty (Left ('<' : tag ++ ">")) a subTerms)
767 Just dc -> do
768 traceTR (text "Is constructor" <+> (ppr dc $$ ppr my_ty))
769 subTtypes <- getDataConArgTys dc my_ty
770 subTerms <- extractSubTerms (\ty -> go (pred max_depth) ty ty) clos subTtypes
771 return (Term my_ty (Right dc) a subTerms)
772
773 -- The otherwise case: can be a Thunk,AP,PAP,etc.
774 tipe_clos ->
775 return (Suspension tipe_clos my_ty a Nothing)
776
777 -- insert NewtypeWraps around newtypes
778 expandNewtypes = foldTerm idTermFold { fTerm = worker } where
779 worker ty dc hval tt
780 | Just (tc, args) <- tcSplitTyConApp_maybe ty
781 , isNewTyCon tc
782 , wrapped_type <- newTyConInstRhs tc args
783 , Just dc' <- tyConSingleDataCon_maybe tc
784 , t' <- worker wrapped_type dc hval tt
785 = NewtypeWrap ty (Right dc') t'
786 | otherwise = Term ty dc hval tt
787
788
789 -- Avoid returning types where predicates have been expanded to dictionaries.
790 fixFunDictionaries = foldTerm idTermFold {fSuspension = worker} where
791 worker ct ty hval n | isFunTy ty = Suspension ct (dictsView ty) hval n
792 | otherwise = Suspension ct ty hval n
793
794 extractSubTerms :: (Type -> HValue -> TcM Term)
795 -> Closure -> [Type] -> TcM [Term]
796 extractSubTerms recurse clos = liftM thirdOf3 . go 0 (nonPtrs clos)
797 where
798 go ptr_i ws [] = return (ptr_i, ws, [])
799 go ptr_i ws (ty:tys)
800 | Just (tc, elem_tys) <- tcSplitTyConApp_maybe ty
801 , isUnboxedTupleTyCon tc
802 = do (ptr_i, ws, terms0) <- go ptr_i ws elem_tys
803 (ptr_i, ws, terms1) <- go ptr_i ws tys
804 return (ptr_i, ws, unboxedTupleTerm ty terms0 : terms1)
805 | otherwise
806 = case repType ty of
807 UnaryRep rep_ty -> do
808 (ptr_i, ws, term0) <- go_rep ptr_i ws ty (typePrimRep rep_ty)
809 (ptr_i, ws, terms1) <- go ptr_i ws tys
810 return (ptr_i, ws, term0 : terms1)
811 UbxTupleRep rep_tys -> do
812 (ptr_i, ws, terms0) <- go_unary_types ptr_i ws rep_tys
813 (ptr_i, ws, terms1) <- go ptr_i ws tys
814 return (ptr_i, ws, unboxedTupleTerm ty terms0 : terms1)
815
816 go_unary_types ptr_i ws [] = return (ptr_i, ws, [])
817 go_unary_types ptr_i ws (rep_ty:rep_tys) = do
818 tv <- newVar liftedTypeKind
819 (ptr_i, ws, term0) <- go_rep ptr_i ws tv (typePrimRep rep_ty)
820 (ptr_i, ws, terms1) <- go_unary_types ptr_i ws rep_tys
821 return (ptr_i, ws, term0 : terms1)
822
823 go_rep ptr_i ws ty rep = case rep of
824 PtrRep -> do
825 t <- appArr (recurse ty) (ptrs clos) ptr_i
826 return (ptr_i + 1, ws, t)
827 _ -> do
828 dflags <- getDynFlags
829 let (ws0, ws1) = splitAt (primRepSizeW dflags rep) ws
830 return (ptr_i, ws1, Prim ty ws0)
831
832 unboxedTupleTerm ty terms = Term ty (Right (tupleCon UnboxedTuple (length terms)))
833 (error "unboxedTupleTerm: no HValue for unboxed tuple") terms
834
835
836 -- Fast, breadth-first Type reconstruction
837 ------------------------------------------
838 cvReconstructType :: HscEnv -> Int -> GhciType -> HValue -> IO (Maybe Type)
839 cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
840 traceTR (text "RTTI started with initial type " <> ppr old_ty)
841 let sigma_old_ty@(old_tvs, _) = quantifyType old_ty
842 new_ty <-
843 if null old_tvs
844 then return old_ty
845 else do
846 (old_ty', rev_subst) <- instScheme sigma_old_ty
847 my_ty <- newVar openTypeKind
848 when (check1 sigma_old_ty) (traceTR (text "check1 passed") >>
849 addConstraint my_ty old_ty')
850 search (isMonomorphic `fmap` zonkTcType my_ty)
851 (\(ty,a) -> go ty a)
852 (Seq.singleton (my_ty, hval))
853 max_depth
854 new_ty <- zonkTcType my_ty
855 if isMonomorphic new_ty || check2 (quantifyType new_ty) sigma_old_ty
856 then do
857 traceTR (text "check2 passed" <+> ppr old_ty $$ ppr new_ty)
858 addConstraint my_ty old_ty'
859 applyRevSubst rev_subst
860 zonkRttiType new_ty
861 else traceTR (text "check2 failed" <+> parens (ppr new_ty)) >>
862 return old_ty
863 traceTR (text "RTTI completed. Type obtained:" <+> ppr new_ty)
864 return new_ty
865 where
866 dflags = hsc_dflags hsc_env
867
868 -- search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m ()
869 search _ _ _ 0 = traceTR (text "Failed to reconstruct a type after " <>
870 int max_depth <> text " steps")
871 search stop expand l d =
872 case viewl l of
873 EmptyL -> return ()
874 x :< xx -> unlessM stop $ do
875 new <- expand x
876 search stop expand (xx `mappend` Seq.fromList new) $! (pred d)
877
878 -- returns unification tasks,since we are going to want a breadth-first search
879 go :: Type -> HValue -> TR [(Type, HValue)]
880 go my_ty a = do
881 traceTR (text "go" <+> ppr my_ty)
882 clos <- trIO $ getClosureData dflags a
883 case tipe clos of
884 Blackhole -> appArr (go my_ty) (ptrs clos) 0 -- carefully, don't eval the TSO
885 Indirection _ -> go my_ty $! (ptrs clos ! 0)
886 MutVar _ -> do
887 contents <- trIO$ IO$ \w -> readMutVar# (unsafeCoerce# a) w
888 tv' <- newVar liftedTypeKind
889 world <- newVar liftedTypeKind
890 addConstraint my_ty (mkTyConApp mutVarPrimTyCon [world,tv'])
891 return [(tv', contents)]
892 Constr -> do
893 Right dcname <- dataConInfoPtrToName (infoPtr clos)
894 traceTR (text "Constr1" <+> ppr dcname)
895 (_,mb_dc) <- tryTcErrs (tcLookupDataCon dcname)
896 case mb_dc of
897 Nothing-> do
898 -- TODO: Check this case
899 forM [0..length (elems $ ptrs clos)] $ \i -> do
900 tv <- newVar liftedTypeKind
901 return$ appArr (\e->(tv,e)) (ptrs clos) i
902
903 Just dc -> do
904 arg_tys <- getDataConArgTys dc my_ty
905 (_, itys) <- findPtrTyss 0 arg_tys
906 traceTR (text "Constr2" <+> ppr dcname <+> ppr arg_tys)
907 return $ [ appArr (\e-> (ty,e)) (ptrs clos) i
908 | (i,ty) <- itys]
909 _ -> return []
910
911 findPtrTys :: Int -- Current pointer index
912 -> Type -- Type
913 -> TR (Int, [(Int, Type)])
914 findPtrTys i ty
915 | Just (tc, elem_tys) <- tcSplitTyConApp_maybe ty
916 , isUnboxedTupleTyCon tc
917 = findPtrTyss i elem_tys
918
919 | otherwise
920 = case repType ty of
921 UnaryRep rep_ty | typePrimRep rep_ty == PtrRep -> return (i + 1, [(i, ty)])
922 | otherwise -> return (i, [])
923 UbxTupleRep rep_tys -> foldM (\(i, extras) rep_ty -> if typePrimRep rep_ty == PtrRep
924 then newVar liftedTypeKind >>= \tv -> return (i + 1, extras ++ [(i, tv)])
925 else return (i, extras))
926 (i, []) rep_tys
927
928 findPtrTyss :: Int
929 -> [Type]
930 -> TR (Int, [(Int, Type)])
931 findPtrTyss i tys = foldM step (i, []) tys
932 where step (i, discovered) elem_ty = findPtrTys i elem_ty >>= \(i, extras) -> return (i, discovered ++ extras)
933
934
935 -- Compute the difference between a base type and the type found by RTTI
936 -- improveType <base_type> <rtti_type>
937 -- The types can contain skolem type variables, which need to be treated as normal vars.
938 -- In particular, we want them to unify with things.
939 improveRTTIType :: HscEnv -> RttiType -> RttiType -> Maybe TvSubst
940 improveRTTIType _ base_ty new_ty = U.tcUnifyTy base_ty new_ty
941
942 getDataConArgTys :: DataCon -> Type -> TR [Type]
943 -- Given the result type ty of a constructor application (D a b c :: ty)
944 -- return the types of the arguments. This is RTTI-land, so 'ty' might
945 -- not be fully known. Moreover, the arg types might involve existentials;
946 -- if so, make up fresh RTTI type variables for them
947 --
948 -- I believe that con_app_ty should not have any enclosing foralls
949 getDataConArgTys dc con_app_ty
950 = do { let UnaryRep rep_con_app_ty = repType con_app_ty
951 ; traceTR (text "getDataConArgTys 1" <+> (ppr con_app_ty $$ ppr rep_con_app_ty
952 $$ ppr (tcSplitTyConApp_maybe rep_con_app_ty)))
953 ; (_, _, subst) <- instTyVars (univ_tvs ++ ex_tvs)
954 ; addConstraint rep_con_app_ty (substTy subst (dataConOrigResTy dc))
955 -- See Note [Constructor arg types]
956 ; let con_arg_tys = substTys subst (dataConRepArgTys dc)
957 ; traceTR (text "getDataConArgTys 2" <+> (ppr rep_con_app_ty $$ ppr con_arg_tys $$ ppr subst))
958 ; return con_arg_tys }
959 where
960 univ_tvs = dataConUnivTyVars dc
961 ex_tvs = dataConExTyVars dc
962
963 {- Note [Constructor arg types]
964 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
965 Consider a GADT (cf Trac #7386)
966 data family D a b
967 data instance D [a] a where
968 MkT :: a -> D [a] (Maybe a)
969 ...
970
971 In getDataConArgTys
972 * con_app_ty is the known type (from outside) of the constructor application,
973 say D [Int] Int
974
975 * The data constructor MkT has a (representation) dataConTyCon = DList,
976 say where
977 data DList a where
978 MkT :: a -> DList a (Maybe a)
979 ...
980
981 So the dataConTyCon of the data constructor, DList, differs from
982 the "outside" type, D. So we can't straightforwardly decompose the
983 "outside" type, and we end up in the "_" branch of the case.
984
985 Then we match the dataConOrigResTy of the data constructor against the
986 outside type, hoping to get a substitution that tells how to instantiate
987 the *representation* type constructor. This looks a bit delicate to
988 me, but it seems to work.
989 -}
990
991 -- Soundness checks
992 --------------------
993 {-
994 This is not formalized anywhere, so hold to your seats!
995 RTTI in the presence of newtypes can be a tricky and unsound business.
996
997 Example:
998 ~~~~~~~~~
999 Suppose we are doing RTTI for a partially evaluated
1000 closure t, the real type of which is t :: MkT Int, for
1001
1002 newtype MkT a = MkT [Maybe a]
1003
1004 The table below shows the results of RTTI and the improvement
1005 calculated for different combinations of evaluatedness and :type t.
1006 Regard the two first columns as input and the next two as output.
1007
1008 # | t | :type t | rtti(t) | improv. | result
1009 ------------------------------------------------------------
1010 1 | _ | t b | a | none | OK
1011 2 | _ | MkT b | a | none | OK
1012 3 | _ | t Int | a | none | OK
1013
1014 If t is not evaluated at *all*, we are safe.
1015
1016 4 | (_ : _) | t b | [a] | t = [] | UNSOUND
1017 5 | (_ : _) | MkT b | MkT a | none | OK (compensating for the missing newtype)
1018 6 | (_ : _) | t Int | [Int] | t = [] | UNSOUND
1019
1020 If a is a minimal whnf, we run into trouble. Note that
1021 row 5 above does newtype enrichment on the ty_rtty parameter.
1022
1023 7 | (Just _:_)| t b |[Maybe a] | t = [], | UNSOUND
1024 | | | b = Maybe a|
1025
1026 8 | (Just _:_)| MkT b | MkT a | none | OK
1027 9 | (Just _:_)| t Int | FAIL | none | OK
1028
1029 And if t is any more evaluated than whnf, we are still in trouble.
1030 Because constraints are solved in top-down order, when we reach the
1031 Maybe subterm what we got is already unsound. This explains why the
1032 row 9 fails to complete.
1033
1034 10 | (Just _:_)| t Int | [Maybe a] | FAIL | OK
1035 11 | (Just 1:_)| t Int | [Maybe Int] | FAIL | OK
1036
1037 We can undo the failure in row 9 by leaving out the constraint
1038 coming from the type signature of t (i.e., the 2nd column).
1039 Note that this type information is still used
1040 to calculate the improvement. But we fail
1041 when trying to calculate the improvement, as there is no unifier for
1042 t Int = [Maybe a] or t Int = [Maybe Int].
1043
1044
1045 Another set of examples with t :: [MkT (Maybe Int)] \equiv [[Maybe (Maybe Int)]]
1046
1047 # | t | :type t | rtti(t) | improvement | result
1048 ---------------------------------------------------------------------
1049 1 |(Just _:_) | [t (Maybe a)] | [[Maybe b]] | t = [] |
1050 | | | | b = Maybe a |
1051
1052 The checks:
1053 ~~~~~~~~~~~
1054 Consider a function obtainType that takes a value and a type and produces
1055 the Term representation and a substitution (the improvement).
1056 Assume an auxiliar rtti' function which does the actual job if recovering
1057 the type, but which may produce a false type.
1058
1059 In pseudocode:
1060
1061 rtti' :: a -> IO Type -- Does not use the static type information
1062
1063 obtainType :: a -> Type -> IO (Maybe (Term, Improvement))
1064 obtainType v old_ty = do
1065 rtti_ty <- rtti' v
1066 if monomorphic rtti_ty || (check rtti_ty old_ty)
1067 then ...
1068 else return Nothing
1069 where check rtti_ty old_ty = check1 rtti_ty &&
1070 check2 rtti_ty old_ty
1071
1072 check1 :: Type -> Bool
1073 check2 :: Type -> Type -> Bool
1074
1075 Now, if rtti' returns a monomorphic type, we are safe.
1076 If that is not the case, then we consider two conditions.
1077
1078
1079 1. To prevent the class of unsoundness displayed by
1080 rows 4 and 7 in the example: no higher kind tyvars
1081 accepted.
1082
1083 check1 (t a) = NO
1084 check1 (t Int) = NO
1085 check1 ([] a) = YES
1086
1087 2. To prevent the class of unsoundness shown by row 6,
1088 the rtti type should be structurally more
1089 defined than the old type we are comparing it to.
1090 check2 :: NewType -> OldType -> Bool
1091 check2 a _ = True
1092 check2 [a] a = True
1093 check2 [a] (t Int) = False
1094 check2 [a] (t a) = False -- By check1 we never reach this equation
1095 check2 [Int] a = True
1096 check2 [Int] (t Int) = True
1097 check2 [Maybe a] (t Int) = False
1098 check2 [Maybe Int] (t Int) = True
1099 check2 (Maybe [a]) (m [Int]) = False
1100 check2 (Maybe [Int]) (m [Int]) = True
1101
1102 -}
1103
1104 check1 :: QuantifiedType -> Bool
1105 check1 (tvs, _) = not $ any isHigherKind (map tyVarKind tvs)
1106 where
1107 isHigherKind = not . null . fst . splitKindFunTys
1108
1109 check2 :: QuantifiedType -> QuantifiedType -> Bool
1110 check2 (_, rtti_ty) (_, old_ty)
1111 | Just (_, rttis) <- tcSplitTyConApp_maybe rtti_ty
1112 = case () of
1113 _ | Just (_,olds) <- tcSplitTyConApp_maybe old_ty
1114 -> and$ zipWith check2 (map quantifyType rttis) (map quantifyType olds)
1115 _ | Just _ <- splitAppTy_maybe old_ty
1116 -> isMonomorphicOnNonPhantomArgs rtti_ty
1117 _ -> True
1118 | otherwise = True
1119
1120 -- Dealing with newtypes
1121 --------------------------
1122 {-
1123 congruenceNewtypes does a parallel fold over two Type values,
1124 compensating for missing newtypes on both sides.
1125 This is necessary because newtypes are not present
1126 in runtime, but sometimes there is evidence available.
1127 Evidence can come from DataCon signatures or
1128 from compile-time type inference.
1129 What we are doing here is an approximation
1130 of unification modulo a set of equations derived
1131 from newtype definitions. These equations should be the
1132 same as the equality coercions generated for newtypes
1133 in System Fc. The idea is to perform a sort of rewriting,
1134 taking those equations as rules, before launching unification.
1135
1136 The caller must ensure the following.
1137 The 1st type (lhs) comes from the heap structure of ptrs,nptrs.
1138 The 2nd type (rhs) comes from a DataCon type signature.
1139 Rewriting (i.e. adding/removing a newtype wrapper) can happen
1140 in both types, but in the rhs it is restricted to the result type.
1141
1142 Note that it is very tricky to make this 'rewriting'
1143 work with the unification implemented by TcM, where
1144 substitutions are operationally inlined. The order in which
1145 constraints are unified is vital as we cannot modify
1146 anything that has been touched by a previous unification step.
1147 Therefore, congruenceNewtypes is sound only if the types
1148 recovered by the RTTI mechanism are unified Top-Down.
1149 -}
1150 congruenceNewtypes :: TcType -> TcType -> TR (TcType,TcType)
1151 congruenceNewtypes lhs rhs = go lhs rhs >>= \rhs' -> return (lhs,rhs')
1152 where
1153 go l r
1154 -- TyVar lhs inductive case
1155 | Just tv <- getTyVar_maybe l
1156 , isTcTyVar tv
1157 , isMetaTyVar tv
1158 = recoverTR (return r) $ do
1159 Indirect ty_v <- readMetaTyVar tv
1160 traceTR $ fsep [text "(congruence) Following indirect tyvar:",
1161 ppr tv, equals, ppr ty_v]
1162 go ty_v r
1163 -- FunTy inductive case
1164 | Just (l1,l2) <- splitFunTy_maybe l
1165 , Just (r1,r2) <- splitFunTy_maybe r
1166 = do r2' <- go l2 r2
1167 r1' <- go l1 r1
1168 return (mkFunTy r1' r2')
1169 -- TyconApp Inductive case; this is the interesting bit.
1170 | Just (tycon_l, _) <- tcSplitTyConApp_maybe lhs
1171 , Just (tycon_r, _) <- tcSplitTyConApp_maybe rhs
1172 , tycon_l /= tycon_r
1173 = upgrade tycon_l r
1174
1175 | otherwise = return r
1176
1177 where upgrade :: TyCon -> Type -> TR Type
1178 upgrade new_tycon ty
1179 | not (isNewTyCon new_tycon) = do
1180 traceTR (text "(Upgrade) Not matching newtype evidence: " <>
1181 ppr new_tycon <> text " for " <> ppr ty)
1182 return ty
1183 | otherwise = do
1184 traceTR (text "(Upgrade) upgraded " <> ppr ty <>
1185 text " in presence of newtype evidence " <> ppr new_tycon)
1186 (_, vars, _) <- instTyVars (tyConTyVars new_tycon)
1187 let ty' = mkTyConApp new_tycon vars
1188 UnaryRep rep_ty = repType ty'
1189 _ <- liftTcM (unifyType ty rep_ty)
1190 -- assumes that reptype doesn't ^^^^ touch tyconApp args
1191 return ty'
1192
1193
1194 zonkTerm :: Term -> TcM Term
1195 zonkTerm = foldTermM (TermFoldM
1196 { fTermM = \ty dc v tt -> zonkRttiType ty >>= \ty' ->
1197 return (Term ty' dc v tt)
1198 , fSuspensionM = \ct ty v b -> zonkRttiType ty >>= \ty ->
1199 return (Suspension ct ty v b)
1200 , fNewtypeWrapM = \ty dc t -> zonkRttiType ty >>= \ty' ->
1201 return$ NewtypeWrap ty' dc t
1202 , fRefWrapM = \ty t -> return RefWrap `ap`
1203 zonkRttiType ty `ap` return t
1204 , fPrimM = (return.) . Prim })
1205
1206 zonkRttiType :: TcType -> TcM Type
1207 -- Zonk the type, replacing any unbound Meta tyvars
1208 -- by skolems, safely out of Meta-tyvar-land
1209 zonkRttiType = zonkTcTypeToType (mkEmptyZonkEnv zonk_unbound_meta)
1210 where
1211 zonk_unbound_meta tv
1212 = ASSERT( isTcTyVar tv )
1213 do { tv' <- skolemiseUnboundMetaTyVar tv RuntimeUnk
1214 -- This is where RuntimeUnks are born:
1215 -- otherwise-unconstrained unification variables are
1216 -- turned into RuntimeUnks as they leave the
1217 -- typechecker's monad
1218 ; return (mkTyVarTy tv') }
1219
1220 --------------------------------------------------------------------------------
1221 -- Restore Class predicates out of a representation type
1222 dictsView :: Type -> Type
1223 dictsView ty = ty
1224
1225
1226 -- Use only for RTTI types
1227 isMonomorphic :: RttiType -> Bool
1228 isMonomorphic ty = noExistentials && noUniversals
1229 where (tvs, _, ty') = tcSplitSigmaTy ty
1230 noExistentials = isEmptyVarSet (tyVarsOfType ty')
1231 noUniversals = null tvs
1232
1233 -- Use only for RTTI types
1234 isMonomorphicOnNonPhantomArgs :: RttiType -> Bool
1235 isMonomorphicOnNonPhantomArgs ty
1236 | UnaryRep rep_ty <- repType ty
1237 , Just (tc, all_args) <- tcSplitTyConApp_maybe rep_ty
1238 , phantom_vars <- tyConPhantomTyVars tc
1239 , concrete_args <- [ arg | (tyv,arg) <- tyConTyVars tc `zip` all_args
1240 , tyv `notElem` phantom_vars]
1241 = all isMonomorphicOnNonPhantomArgs concrete_args
1242 | Just (ty1, ty2) <- splitFunTy_maybe ty
1243 = all isMonomorphicOnNonPhantomArgs [ty1,ty2]
1244 | otherwise = isMonomorphic ty
1245
1246 tyConPhantomTyVars :: TyCon -> [TyVar]
1247 tyConPhantomTyVars tc
1248 | isAlgTyCon tc
1249 , Just dcs <- tyConDataCons_maybe tc
1250 , dc_vars <- concatMap dataConUnivTyVars dcs
1251 = tyConTyVars tc \\ dc_vars
1252 tyConPhantomTyVars _ = []
1253
1254 type QuantifiedType = ([TyVar], Type)
1255 -- Make the free type variables explicit
1256 -- The returned Type should have no top-level foralls (I believe)
1257
1258 quantifyType :: Type -> QuantifiedType
1259 -- Generalize the type: find all free and forall'd tyvars
1260 -- and return them, together with the type inside, which
1261 -- should not be a forall type.
1262 --
1263 -- Thus (quantifyType (forall a. a->[b]))
1264 -- returns ([a,b], a -> [b])
1265
1266 quantifyType ty = (varSetElems (tyVarsOfType rho), rho)
1267 where
1268 (_tvs, rho) = tcSplitForAllTys ty
1269
1270 unlessM :: Monad m => m Bool -> m () -> m ()
1271 unlessM condM acc = condM >>= \c -> unless c acc
1272
1273
1274 -- Strict application of f at index i
1275 appArr :: Ix i => (e -> a) -> Array i e -> Int -> a
1276 appArr f a@(Array _ _ _ ptrs#) i@(I# i#)
1277 = ASSERT2(i < length(elems a), ppr(length$ elems a, i))
1278 case indexArray# ptrs# i# of
1279 (# e #) -> f e
1280
1281 amap' :: (t -> b) -> Array Int t -> [b]
1282 amap' f (Array i0 i _ arr#) = map g [0 .. i - i0]
1283 where g (I# i#) = case indexArray# arr# i# of
1284 (# e #) -> f e