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