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