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