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