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