Merge remote-tracking branch 'origin/unboxed-tuple-arguments2'
[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$ text$ 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] -> String
497 repPrim t = rep where
498 rep x
499 | t == charPrimTyCon = show (build x :: Char)
500 | t == intPrimTyCon = show (build x :: Int)
501 | t == wordPrimTyCon = show (build x :: Word)
502 | t == floatPrimTyCon = show (build x :: Float)
503 | t == doublePrimTyCon = show (build x :: Double)
504 | t == int32PrimTyCon = show (build x :: Int32)
505 | t == word32PrimTyCon = show (build x :: Word32)
506 | t == int64PrimTyCon = show (build x :: Int64)
507 | t == word64PrimTyCon = show (build x :: Word64)
508 | t == addrPrimTyCon = show (nullPtr `plusPtr` build x)
509 | t == stablePtrPrimTyCon = "<stablePtr>"
510 | t == stableNamePrimTyCon = "<stableName>"
511 | t == statePrimTyCon = "<statethread>"
512 | t == realWorldTyCon = "<realworld>"
513 | t == threadIdPrimTyCon = "<ThreadId>"
514 | t == weakPrimTyCon = "<Weak>"
515 | t == arrayPrimTyCon = "<array>"
516 | t == byteArrayPrimTyCon = "<bytearray>"
517 | t == mutableArrayPrimTyCon = "<mutableArray>"
518 | t == mutableByteArrayPrimTyCon = "<mutableByteArray>"
519 | t == mutVarPrimTyCon= "<mutVar>"
520 | t == mVarPrimTyCon = "<mVar>"
521 | t == tVarPrimTyCon = "<tVar>"
522 | otherwise = showSDoc (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 tag = showSDoc (ppr dcname)
754 vars <- replicateM (length$ elems$ ptrs clos)
755 (newVar liftedTypeKind)
756 subTerms <- sequence [appArr (go (pred max_depth) tv tv) (ptrs clos) i
757 | (i, tv) <- zip [0..] vars]
758 return (Term my_ty (Left ('<' : tag ++ ">")) a subTerms)
759 Just dc -> do
760 traceTR (text "Just" <+> ppr dc)
761 subTtypes <- getDataConArgTys dc my_ty
762 subTerms <- extractSubTerms (\ty -> go (pred max_depth) ty ty) clos subTtypes
763 return (Term my_ty (Right dc) a subTerms)
764
765 -- The otherwise case: can be a Thunk,AP,PAP,etc.
766 tipe_clos ->
767 return (Suspension tipe_clos my_ty a Nothing)
768
769 -- insert NewtypeWraps around newtypes
770 expandNewtypes = foldTerm idTermFold { fTerm = worker } where
771 worker ty dc hval tt
772 | Just (tc, args) <- tcSplitTyConApp_maybe ty
773 , isNewTyCon tc
774 , wrapped_type <- newTyConInstRhs tc args
775 , Just dc' <- tyConSingleDataCon_maybe tc
776 , t' <- worker wrapped_type dc hval tt
777 = NewtypeWrap ty (Right dc') t'
778 | otherwise = Term ty dc hval tt
779
780
781 -- Avoid returning types where predicates have been expanded to dictionaries.
782 fixFunDictionaries = foldTerm idTermFold {fSuspension = worker} where
783 worker ct ty hval n | isFunTy ty = Suspension ct (dictsView ty) hval n
784 | otherwise = Suspension ct ty hval n
785
786 extractSubTerms :: (Type -> HValue -> TcM Term)
787 -> Closure -> [Type] -> TcM [Term]
788 extractSubTerms recurse clos = liftM thirdOf3 . go 0 (nonPtrs clos)
789 where
790 go ptr_i ws [] = return (ptr_i, ws, [])
791 go ptr_i ws (ty:tys)
792 | Just (tc, elem_tys) <- tcSplitTyConApp_maybe ty
793 , isUnboxedTupleTyCon tc
794 = do (ptr_i, ws, terms0) <- go ptr_i ws elem_tys
795 (ptr_i, ws, terms1) <- go ptr_i ws tys
796 return (ptr_i, ws, unboxedTupleTerm ty terms0 : terms1)
797 | otherwise
798 = case repType ty of
799 UnaryRep rep_ty -> do
800 (ptr_i, ws, term0) <- go_rep ptr_i ws ty (typePrimRep rep_ty)
801 (ptr_i, ws, terms1) <- go ptr_i ws tys
802 return (ptr_i, ws, term0 : terms1)
803 UbxTupleRep rep_tys -> do
804 (ptr_i, ws, terms0) <- go_unary_types ptr_i ws rep_tys
805 (ptr_i, ws, terms1) <- go ptr_i ws tys
806 return (ptr_i, ws, unboxedTupleTerm ty terms0 : terms1)
807
808 go_unary_types ptr_i ws [] = return (ptr_i, ws, [])
809 go_unary_types ptr_i ws (rep_ty:rep_tys) = do
810 tv <- newVar liftedTypeKind
811 (ptr_i, ws, term0) <- go_rep ptr_i ws tv (typePrimRep rep_ty)
812 (ptr_i, ws, terms1) <- go_unary_types ptr_i ws rep_tys
813 return (ptr_i, ws, term0 : terms1)
814
815 go_rep ptr_i ws ty rep = case rep of
816 PtrRep -> do
817 t <- appArr (recurse ty) (ptrs clos) ptr_i
818 return (ptr_i + 1, ws, t)
819 _ -> do
820 let (ws0, ws1) = splitAt (primRepSizeW rep) ws
821 return (ptr_i, ws1, Prim ty ws0)
822
823 unboxedTupleTerm ty terms = Term ty (Right (tupleCon UnboxedTuple (length terms)))
824 (error "unboxedTupleTerm: no HValue for unboxed tuple") terms
825
826
827 -- Fast, breadth-first Type reconstruction
828 ------------------------------------------
829 cvReconstructType :: HscEnv -> Int -> GhciType -> HValue -> IO (Maybe Type)
830 cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
831 traceTR (text "RTTI started with initial type " <> ppr old_ty)
832 let sigma_old_ty@(old_tvs, _) = quantifyType old_ty
833 new_ty <-
834 if null old_tvs
835 then return old_ty
836 else do
837 (old_ty', rev_subst) <- instScheme sigma_old_ty
838 my_ty <- newVar openTypeKind
839 when (check1 sigma_old_ty) (traceTR (text "check1 passed") >>
840 addConstraint my_ty old_ty')
841 search (isMonomorphic `fmap` zonkTcType my_ty)
842 (\(ty,a) -> go ty a)
843 (Seq.singleton (my_ty, hval))
844 max_depth
845 new_ty <- zonkTcType my_ty
846 if isMonomorphic new_ty || check2 (quantifyType new_ty) sigma_old_ty
847 then do
848 traceTR (text "check2 passed" <+> ppr old_ty $$ ppr new_ty)
849 addConstraint my_ty old_ty'
850 applyRevSubst rev_subst
851 zonkRttiType new_ty
852 else traceTR (text "check2 failed" <+> parens (ppr new_ty)) >>
853 return old_ty
854 traceTR (text "RTTI completed. Type obtained:" <+> ppr new_ty)
855 return new_ty
856 where
857 -- search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m ()
858 search _ _ _ 0 = traceTR (text "Failed to reconstruct a type after " <>
859 int max_depth <> text " steps")
860 search stop expand l d =
861 case viewl l of
862 EmptyL -> return ()
863 x :< xx -> unlessM stop $ do
864 new <- expand x
865 search stop expand (xx `mappend` Seq.fromList new) $! (pred d)
866
867 -- returns unification tasks,since we are going to want a breadth-first search
868 go :: Type -> HValue -> TR [(Type, HValue)]
869 go my_ty a = do
870 traceTR (text "go" <+> ppr my_ty)
871 clos <- trIO $ getClosureData a
872 case tipe clos of
873 Blackhole -> appArr (go my_ty) (ptrs clos) 0 -- carefully, don't eval the TSO
874 Indirection _ -> go my_ty $! (ptrs clos ! 0)
875 MutVar _ -> do
876 contents <- trIO$ IO$ \w -> readMutVar# (unsafeCoerce# a) w
877 tv' <- newVar liftedTypeKind
878 world <- newVar liftedTypeKind
879 addConstraint my_ty (mkTyConApp mutVarPrimTyCon [world,tv'])
880 return [(tv', contents)]
881 Constr -> do
882 Right dcname <- dataConInfoPtrToName (infoPtr clos)
883 traceTR (text "Constr1" <+> ppr dcname)
884 (_,mb_dc) <- tryTcErrs (tcLookupDataCon dcname)
885 case mb_dc of
886 Nothing-> do
887 -- TODO: Check this case
888 forM [0..length (elems $ ptrs clos)] $ \i -> do
889 tv <- newVar liftedTypeKind
890 return$ appArr (\e->(tv,e)) (ptrs clos) i
891
892 Just dc -> do
893 arg_tys <- getDataConArgTys dc my_ty
894 (_, itys) <- findPtrTyss 0 arg_tys
895 traceTR (text "Constr2" <+> ppr dcname <+> ppr arg_tys)
896 return $ [ appArr (\e-> (ty,e)) (ptrs clos) i
897 | (i,ty) <- itys]
898 _ -> return []
899
900 findPtrTys :: Int -- Current pointer index
901 -> Type -- Type
902 -> TR (Int, [(Int, Type)])
903 findPtrTys i ty
904 | Just (tc, elem_tys) <- tcSplitTyConApp_maybe ty
905 , isUnboxedTupleTyCon tc
906 = findPtrTyss i elem_tys
907
908 | otherwise
909 = case repType ty of
910 UnaryRep rep_ty | typePrimRep rep_ty == PtrRep -> return (i + 1, [(i, ty)])
911 | otherwise -> return (i, [])
912 UbxTupleRep rep_tys -> foldM (\(i, extras) rep_ty -> if typePrimRep rep_ty == PtrRep
913 then newVar liftedTypeKind >>= \tv -> return (i + 1, extras ++ [(i, tv)])
914 else return (i, extras))
915 (i, []) rep_tys
916
917 findPtrTyss :: Int
918 -> [Type]
919 -> TR (Int, [(Int, Type)])
920 findPtrTyss i tys = foldM step (i, []) tys
921 where step (i, discovered) elem_ty = findPtrTys i elem_ty >>= \(i, extras) -> return (i, discovered ++ extras)
922
923
924 -- Compute the difference between a base type and the type found by RTTI
925 -- improveType <base_type> <rtti_type>
926 -- The types can contain skolem type variables, which need to be treated as normal vars.
927 -- In particular, we want them to unify with things.
928 improveRTTIType :: HscEnv -> RttiType -> RttiType -> Maybe TvSubst
929 improveRTTIType _ base_ty new_ty
930 = U.tcUnifyTys (const U.BindMe) [base_ty] [new_ty]
931
932 getDataConArgTys :: DataCon -> Type -> TR [Type]
933 -- Given the result type ty of a constructor application (D a b c :: ty)
934 -- return the types of the arguments. This is RTTI-land, so 'ty' might
935 -- not be fully known. Moreover, the arg types might involve existentials;
936 -- if so, make up fresh RTTI type variables for them
937 getDataConArgTys dc con_app_ty
938 = do { (_, ex_tys, _) <- instTyVars ex_tvs
939 ; let UnaryRep rep_con_app_ty = repType con_app_ty
940 ; ty_args <- case tcSplitTyConApp_maybe rep_con_app_ty of
941 Just (tc, ty_args) | dataConTyCon dc == tc
942 -> ASSERT( univ_tvs `equalLength` ty_args)
943 return ty_args
944 _ -> do { (_, ty_args, subst) <- instTyVars univ_tvs
945 ; let res_ty = substTy subst (dataConOrigResTy dc)
946 ; addConstraint rep_con_app_ty res_ty
947 ; return ty_args }
948 -- It is necessary to check dataConTyCon dc == tc
949 -- because it may be the case that tc is a recursive
950 -- newtype and tcSplitTyConApp has not removed it. In
951 -- that case, we happily give up and don't match
952 ; let subst = zipTopTvSubst (univ_tvs ++ ex_tvs) (ty_args ++ ex_tys)
953 ; return (substTys subst (dataConRepArgTys dc)) }
954 where
955 univ_tvs = dataConUnivTyVars dc
956 ex_tvs = dataConExTyVars dc
957
958 -- Soundness checks
959 --------------------
960 {-
961 This is not formalized anywhere, so hold to your seats!
962 RTTI in the presence of newtypes can be a tricky and unsound business.
963
964 Example:
965 ~~~~~~~~~
966 Suppose we are doing RTTI for a partially evaluated
967 closure t, the real type of which is t :: MkT Int, for
968
969 newtype MkT a = MkT [Maybe a]
970
971 The table below shows the results of RTTI and the improvement
972 calculated for different combinations of evaluatedness and :type t.
973 Regard the two first columns as input and the next two as output.
974
975 # | t | :type t | rtti(t) | improv. | result
976 ------------------------------------------------------------
977 1 | _ | t b | a | none | OK
978 2 | _ | MkT b | a | none | OK
979 3 | _ | t Int | a | none | OK
980
981 If t is not evaluated at *all*, we are safe.
982
983 4 | (_ : _) | t b | [a] | t = [] | UNSOUND
984 5 | (_ : _) | MkT b | MkT a | none | OK (compensating for the missing newtype)
985 6 | (_ : _) | t Int | [Int] | t = [] | UNSOUND
986
987 If a is a minimal whnf, we run into trouble. Note that
988 row 5 above does newtype enrichment on the ty_rtty parameter.
989
990 7 | (Just _:_)| t b |[Maybe a] | t = [], | UNSOUND
991 | | | b = Maybe a|
992
993 8 | (Just _:_)| MkT b | MkT a | none | OK
994 9 | (Just _:_)| t Int | FAIL | none | OK
995
996 And if t is any more evaluated than whnf, we are still in trouble.
997 Because constraints are solved in top-down order, when we reach the
998 Maybe subterm what we got is already unsound. This explains why the
999 row 9 fails to complete.
1000
1001 10 | (Just _:_)| t Int | [Maybe a] | FAIL | OK
1002 11 | (Just 1:_)| t Int | [Maybe Int] | FAIL | OK
1003
1004 We can undo the failure in row 9 by leaving out the constraint
1005 coming from the type signature of t (i.e., the 2nd column).
1006 Note that this type information is still used
1007 to calculate the improvement. But we fail
1008 when trying to calculate the improvement, as there is no unifier for
1009 t Int = [Maybe a] or t Int = [Maybe Int].
1010
1011
1012 Another set of examples with t :: [MkT (Maybe Int)] \equiv [[Maybe (Maybe Int)]]
1013
1014 # | t | :type t | rtti(t) | improvement | result
1015 ---------------------------------------------------------------------
1016 1 |(Just _:_) | [t (Maybe a)] | [[Maybe b]] | t = [] |
1017 | | | | b = Maybe a |
1018
1019 The checks:
1020 ~~~~~~~~~~~
1021 Consider a function obtainType that takes a value and a type and produces
1022 the Term representation and a substitution (the improvement).
1023 Assume an auxiliar rtti' function which does the actual job if recovering
1024 the type, but which may produce a false type.
1025
1026 In pseudocode:
1027
1028 rtti' :: a -> IO Type -- Does not use the static type information
1029
1030 obtainType :: a -> Type -> IO (Maybe (Term, Improvement))
1031 obtainType v old_ty = do
1032 rtti_ty <- rtti' v
1033 if monomorphic rtti_ty || (check rtti_ty old_ty)
1034 then ...
1035 else return Nothing
1036 where check rtti_ty old_ty = check1 rtti_ty &&
1037 check2 rtti_ty old_ty
1038
1039 check1 :: Type -> Bool
1040 check2 :: Type -> Type -> Bool
1041
1042 Now, if rtti' returns a monomorphic type, we are safe.
1043 If that is not the case, then we consider two conditions.
1044
1045
1046 1. To prevent the class of unsoundness displayed by
1047 rows 4 and 7 in the example: no higher kind tyvars
1048 accepted.
1049
1050 check1 (t a) = NO
1051 check1 (t Int) = NO
1052 check1 ([] a) = YES
1053
1054 2. To prevent the class of unsoundness shown by row 6,
1055 the rtti type should be structurally more
1056 defined than the old type we are comparing it to.
1057 check2 :: NewType -> OldType -> Bool
1058 check2 a _ = True
1059 check2 [a] a = True
1060 check2 [a] (t Int) = False
1061 check2 [a] (t a) = False -- By check1 we never reach this equation
1062 check2 [Int] a = True
1063 check2 [Int] (t Int) = True
1064 check2 [Maybe a] (t Int) = False
1065 check2 [Maybe Int] (t Int) = True
1066 check2 (Maybe [a]) (m [Int]) = False
1067 check2 (Maybe [Int]) (m [Int]) = True
1068
1069 -}
1070
1071 check1 :: QuantifiedType -> Bool
1072 check1 (tvs, _) = not $ any isHigherKind (map tyVarKind tvs)
1073 where
1074 isHigherKind = not . null . fst . splitKindFunTys
1075
1076 check2 :: QuantifiedType -> QuantifiedType -> Bool
1077 check2 (_, rtti_ty) (_, old_ty)
1078 | Just (_, rttis) <- tcSplitTyConApp_maybe rtti_ty
1079 = case () of
1080 _ | Just (_,olds) <- tcSplitTyConApp_maybe old_ty
1081 -> and$ zipWith check2 (map quantifyType rttis) (map quantifyType olds)
1082 _ | Just _ <- splitAppTy_maybe old_ty
1083 -> isMonomorphicOnNonPhantomArgs rtti_ty
1084 _ -> True
1085 | otherwise = True
1086
1087 -- Dealing with newtypes
1088 --------------------------
1089 {-
1090 congruenceNewtypes does a parallel fold over two Type values,
1091 compensating for missing newtypes on both sides.
1092 This is necessary because newtypes are not present
1093 in runtime, but sometimes there is evidence available.
1094 Evidence can come from DataCon signatures or
1095 from compile-time type inference.
1096 What we are doing here is an approximation
1097 of unification modulo a set of equations derived
1098 from newtype definitions. These equations should be the
1099 same as the equality coercions generated for newtypes
1100 in System Fc. The idea is to perform a sort of rewriting,
1101 taking those equations as rules, before launching unification.
1102
1103 The caller must ensure the following.
1104 The 1st type (lhs) comes from the heap structure of ptrs,nptrs.
1105 The 2nd type (rhs) comes from a DataCon type signature.
1106 Rewriting (i.e. adding/removing a newtype wrapper) can happen
1107 in both types, but in the rhs it is restricted to the result type.
1108
1109 Note that it is very tricky to make this 'rewriting'
1110 work with the unification implemented by TcM, where
1111 substitutions are operationally inlined. The order in which
1112 constraints are unified is vital as we cannot modify
1113 anything that has been touched by a previous unification step.
1114 Therefore, congruenceNewtypes is sound only if the types
1115 recovered by the RTTI mechanism are unified Top-Down.
1116 -}
1117 congruenceNewtypes :: TcType -> TcType -> TR (TcType,TcType)
1118 congruenceNewtypes lhs rhs = go lhs rhs >>= \rhs' -> return (lhs,rhs')
1119 where
1120 go l r
1121 -- TyVar lhs inductive case
1122 | Just tv <- getTyVar_maybe l
1123 , isTcTyVar tv
1124 , isMetaTyVar tv
1125 = recoverTR (return r) $ do
1126 Indirect ty_v <- readMetaTyVar tv
1127 traceTR $ fsep [text "(congruence) Following indirect tyvar:",
1128 ppr tv, equals, ppr ty_v]
1129 go ty_v r
1130 -- FunTy inductive case
1131 | Just (l1,l2) <- splitFunTy_maybe l
1132 , Just (r1,r2) <- splitFunTy_maybe r
1133 = do r2' <- go l2 r2
1134 r1' <- go l1 r1
1135 return (mkFunTy r1' r2')
1136 -- TyconApp Inductive case; this is the interesting bit.
1137 | Just (tycon_l, _) <- tcSplitTyConApp_maybe lhs
1138 , Just (tycon_r, _) <- tcSplitTyConApp_maybe rhs
1139 , tycon_l /= tycon_r
1140 = upgrade tycon_l r
1141
1142 | otherwise = return r
1143
1144 where upgrade :: TyCon -> Type -> TR Type
1145 upgrade new_tycon ty
1146 | not (isNewTyCon new_tycon) = do
1147 traceTR (text "(Upgrade) Not matching newtype evidence: " <>
1148 ppr new_tycon <> text " for " <> ppr ty)
1149 return ty
1150 | otherwise = do
1151 traceTR (text "(Upgrade) upgraded " <> ppr ty <>
1152 text " in presence of newtype evidence " <> ppr new_tycon)
1153 (_, vars, _) <- instTyVars (tyConTyVars new_tycon)
1154 let ty' = mkTyConApp new_tycon vars
1155 UnaryRep rep_ty = repType ty'
1156 _ <- liftTcM (unifyType ty rep_ty)
1157 -- assumes that reptype doesn't ^^^^ touch tyconApp args
1158 return ty'
1159
1160
1161 zonkTerm :: Term -> TcM Term
1162 zonkTerm = foldTermM (TermFoldM
1163 { fTermM = \ty dc v tt -> zonkRttiType ty >>= \ty' ->
1164 return (Term ty' dc v tt)
1165 , fSuspensionM = \ct ty v b -> zonkRttiType ty >>= \ty ->
1166 return (Suspension ct ty v b)
1167 , fNewtypeWrapM = \ty dc t -> zonkRttiType ty >>= \ty' ->
1168 return$ NewtypeWrap ty' dc t
1169 , fRefWrapM = \ty t -> return RefWrap `ap`
1170 zonkRttiType ty `ap` return t
1171 , fPrimM = (return.) . Prim })
1172
1173 zonkRttiType :: TcType -> TcM Type
1174 -- Zonk the type, replacing any unbound Meta tyvars
1175 -- by skolems, safely out of Meta-tyvar-land
1176 zonkRttiType = zonkTcTypeToType (mkEmptyZonkEnv zonk_unbound_meta)
1177 where
1178 zonk_unbound_meta tv
1179 = ASSERT( isTcTyVar tv )
1180 do { tv' <- skolemiseUnboundMetaTyVar tv RuntimeUnk
1181 -- This is where RuntimeUnks are born:
1182 -- otherwise-unconstrained unification variables are
1183 -- turned into RuntimeUnks as they leave the
1184 -- typechecker's monad
1185 ; return (mkTyVarTy tv') }
1186
1187 --------------------------------------------------------------------------------
1188 -- Restore Class predicates out of a representation type
1189 dictsView :: Type -> Type
1190 dictsView ty = ty
1191
1192
1193 -- Use only for RTTI types
1194 isMonomorphic :: RttiType -> Bool
1195 isMonomorphic ty = noExistentials && noUniversals
1196 where (tvs, _, ty') = tcSplitSigmaTy ty
1197 noExistentials = isEmptyVarSet (tyVarsOfType ty')
1198 noUniversals = null tvs
1199
1200 -- Use only for RTTI types
1201 isMonomorphicOnNonPhantomArgs :: RttiType -> Bool
1202 isMonomorphicOnNonPhantomArgs ty
1203 | UnaryRep rep_ty <- repType ty
1204 , Just (tc, all_args) <- tcSplitTyConApp_maybe rep_ty
1205 , phantom_vars <- tyConPhantomTyVars tc
1206 , concrete_args <- [ arg | (tyv,arg) <- tyConTyVars tc `zip` all_args
1207 , tyv `notElem` phantom_vars]
1208 = all isMonomorphicOnNonPhantomArgs concrete_args
1209 | Just (ty1, ty2) <- splitFunTy_maybe ty
1210 = all isMonomorphicOnNonPhantomArgs [ty1,ty2]
1211 | otherwise = isMonomorphic ty
1212
1213 tyConPhantomTyVars :: TyCon -> [TyVar]
1214 tyConPhantomTyVars tc
1215 | isAlgTyCon tc
1216 , Just dcs <- tyConDataCons_maybe tc
1217 , dc_vars <- concatMap dataConUnivTyVars dcs
1218 = tyConTyVars tc \\ dc_vars
1219 tyConPhantomTyVars _ = []
1220
1221 type QuantifiedType = ([TyVar], Type) -- Make the free type variables explicit
1222
1223 quantifyType :: Type -> QuantifiedType
1224 -- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
1225 quantifyType ty = (varSetElems (tyVarsOfType ty), ty)
1226
1227 unlessM :: Monad m => m Bool -> m () -> m ()
1228 unlessM condM acc = condM >>= \c -> unless c acc
1229
1230
1231 -- Strict application of f at index i
1232 appArr :: Ix i => (e -> a) -> Array i e -> Int -> a
1233 appArr f a@(Array _ _ _ ptrs#) i@(I# i#)
1234 = ASSERT2 (i < length(elems a), ppr(length$ elems a, i))
1235 case indexArray# ptrs# i# of
1236 (# e #) -> f e
1237
1238 amap' :: (t -> b) -> Array Int t -> [b]
1239 amap' f (Array i0 i _ arr#) = map g [0 .. i - i0]
1240 where g (I# i#) = case indexArray# arr# i# of
1241 (# e #) -> f e