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