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