1 -----------------------------------------------------------------------------
3 -- GHC Interactive support for inspecting arbitrary closures at runtime
5 -- Pepe Iborra (supported by Google SoC) 2006
7 -----------------------------------------------------------------------------
9 module RtClosureInspect(
11 cvObtainTerm, -- :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Term
32 #include "HsVersions.h"
34 import ByteCodeItbls ( StgInfoTable )
35 import qualified ByteCodeItbls as BCI( StgInfoTable(..) )
36 import HscTypes ( HscEnv )
41 import TcRnMonad ( TcM, initTc, initTcPrintErrors, ioToTcRn,
64 import GHC.Arr ( Array(..) )
69 import Data.Array.Base
70 import Data.List ( partition )
71 import qualified Data.Sequence as Seq
73 import System.IO.Unsafe
75 ---------------------------------------------
76 -- * A representation of semi evaluated Terms
77 ---------------------------------------------
79 A few examples in this representation:
81 > Just 10 = Term Data.Maybe Data.Maybe.Just (Just 10) [Term Int I# (10) "10"]
83 > (('a',_,_),_,('b',_,_)) =
84 Term ((Char,b,c),d,(Char,e,f)) (,,) (('a',_,_),_,('b',_,_))
85 [ Term (Char, b, c) (,,) ('a',_,_) [Term Char C# "a", Suspension, Suspension]
87 , Term (Char, e, f) (,,) ('b',_,_) [Term Char C# "b", Suspension, Suspension]]
90 data Term = Term { ty :: Type
91 , dc :: Either String DataCon
92 -- The heap datacon. If ty is a newtype,
93 -- this is NOT the newtype datacon.
94 -- Empty if the datacon aint exported by the .hi
95 -- (private constructors in -O0 libraries)
97 , subTerms :: [Term] }
102 | Suspension { ctype :: ClosureType
103 , mb_ty :: Maybe Type
105 , bound_to :: Maybe Name -- Useful for printing
108 isTerm, isSuspension, isPrim :: Term -> Bool
111 isSuspension Suspension{} = True
112 isSuspension _ = False
116 termType :: Term -> Maybe Type
117 termType t@(Suspension {}) = mb_ty t
118 termType t = Just$ ty t
120 isFullyEvaluatedTerm :: Term -> Bool
121 isFullyEvaluatedTerm Term {subTerms=tt} = all isFullyEvaluatedTerm tt
122 isFullyEvaluatedTerm Suspension {} = False
123 isFullyEvaluatedTerm Prim {} = True
125 instance Outputable (Term) where
126 ppr = head . cPprTerm cPprTermBase
128 -------------------------------------------------------------------------
129 -- Runtime Closure Datatype and functions for retrieving closure related stuff
130 -------------------------------------------------------------------------
131 data ClosureType = Constr
142 data Closure = Closure { tipe :: ClosureType
144 , infoTable :: StgInfoTable
145 , ptrs :: Array Int HValue
149 instance Outputable ClosureType where
152 #include "../includes/ClosureTypes.h"
159 getClosureData :: a -> IO Closure
161 case unpackClosure# a of
162 (# iptr, ptrs, nptrs #) -> do
163 itbl <- peek (Ptr iptr)
164 let tipe = readCType (BCI.tipe itbl)
165 elems = BCI.ptrs itbl
166 ptrsList = Array 0 ((fromIntegral elems) - 1) ptrs
167 nptrs_data = [W# (indexWordArray# nptrs i)
168 | I# i <- [0.. fromIntegral (BCI.nptrs itbl)] ]
169 ASSERT(fromIntegral elems >= 0) return ()
171 return (Closure tipe (Ptr iptr) itbl ptrsList nptrs_data)
173 readCType :: Integral a => a -> ClosureType
175 | i >= CONSTR && i <= CONSTR_NOCAF_STATIC = Constr
176 | i >= FUN && i <= FUN_STATIC = Fun
177 | i >= THUNK && i < THUNK_SELECTOR = Thunk (fromIntegral i)
178 | i == THUNK_SELECTOR = ThunkSelector
179 | i == BLACKHOLE = Blackhole
180 | i >= IND && i <= IND_STATIC = Indirection (fromIntegral i)
181 | fromIntegral i == aP_CODE = AP
183 | fromIntegral i == pAP_CODE = PAP
184 | otherwise = Other (fromIntegral i)
186 isConstr, isIndirection, isThunk :: ClosureType -> Bool
187 isConstr Constr = True
190 isIndirection (Indirection _) = True
191 --isIndirection ThunkSelector = True
192 isIndirection _ = False
194 isThunk (Thunk _) = True
195 isThunk ThunkSelector = True
199 isFullyEvaluated :: a -> IO Bool
200 isFullyEvaluated a = do
201 closure <- getClosureData a
203 Constr -> do are_subs_evaluated <- amapM isFullyEvaluated (ptrs closure)
204 return$ and are_subs_evaluated
205 otherwise -> return False
206 where amapM f = sequence . amap' f
208 amap' f (Array i0 i arr#) = map (\(I# i#) -> case indexArray# arr# i# of
212 -- TODO: Fix it. Probably the otherwise case is failing, trace/debug it
214 unsafeDeepSeq :: a -> b -> b
215 unsafeDeepSeq = unsafeDeepSeq1 2
216 where unsafeDeepSeq1 0 a b = seq a $! b
217 unsafeDeepSeq1 i a b -- 1st case avoids infinite loops for non reducible thunks
218 | not (isConstr tipe) = seq a $! unsafeDeepSeq1 (i-1) a b
219 -- | unsafePerformIO (isFullyEvaluated a) = b
220 | otherwise = case unsafePerformIO (getClosureData a) of
221 closure -> foldl' (flip unsafeDeepSeq) b (ptrs closure)
222 where tipe = unsafePerformIO (getClosureType a)
224 isPointed :: Type -> Bool
225 isPointed t | Just (t, _) <- splitTyConApp_maybe t
226 = not$ isUnliftedTypeKind (tyConKind t)
229 extractUnboxed :: [Type] -> Closure -> [[Word]]
230 extractUnboxed tt clos = go tt (nonPtrs clos)
232 | Just (tycon,_) <- splitTyConApp_maybe t
233 = ASSERT (isPrimTyCon tycon) sizeofTyCon tycon
234 | otherwise = pprPanic "Expected a TcTyCon" (ppr t)
237 | (x, rest) <- splitAt (sizeofType t `div` wORD_SIZE) xx
240 sizeofTyCon = sizeofPrimRep . tyConPrimRep
242 -----------------------------------
243 -- * Traversals for Terms
244 -----------------------------------
246 data TermFold a = TermFold { fTerm :: Type -> Either String DataCon -> HValue -> [a] -> a
247 , fPrim :: Type -> [Word] -> a
248 , fSuspension :: ClosureType -> Maybe Type -> HValue
252 foldTerm :: TermFold a -> Term -> a
253 foldTerm tf (Term ty dc v tt) = fTerm tf ty dc v (map (foldTerm tf) tt)
254 foldTerm tf (Prim ty v ) = fPrim tf ty v
255 foldTerm tf (Suspension ct ty v b) = fSuspension tf ct ty v b
257 idTermFold :: TermFold Term
258 idTermFold = TermFold {
261 fSuspension = Suspension
263 idTermFoldM :: Monad m => TermFold (m Term)
264 idTermFoldM = TermFold {
265 fTerm = \ty dc v tt -> sequence tt >>= return . Term ty dc v,
266 fPrim = (return.). Prim,
267 fSuspension = (((return.).).). Suspension
270 mapTermType :: (Type -> Type) -> Term -> Term
271 mapTermType f = foldTerm idTermFold {
272 fTerm = \ty dc hval tt -> Term (f ty) dc hval tt,
273 fSuspension = \ct mb_ty hval n ->
274 Suspension ct (fmap f mb_ty) hval n }
276 termTyVars :: Term -> TyVarSet
277 termTyVars = foldTerm TermFold {
278 fTerm = \ty _ _ tt ->
279 tyVarsOfType ty `plusVarEnv` concatVarEnv tt,
280 fSuspension = \_ mb_ty _ _ ->
281 maybe emptyVarEnv tyVarsOfType mb_ty,
282 fPrim = \ _ _ -> emptyVarEnv }
283 where concatVarEnv = foldr plusVarEnv emptyVarEnv
284 ----------------------------------
285 -- Pretty printing of terms
286 ----------------------------------
288 app_prec,cons_prec ::Int
290 cons_prec = 5 -- TODO Extract this info from GHC itself
292 pprTerm y p t | Just doc <- pprTermM y p t = doc
294 pprTermM :: Monad m => (Int -> Term -> m SDoc) -> Int -> Term -> m SDoc
295 pprTermM y p t@Term{dc=Left dc_tag, subTerms=tt, ty=ty} = do
296 tt_docs <- mapM (y app_prec) tt
297 return$ cparen (not(null tt) && p >= app_prec) (text dc_tag <+> sep tt_docs)
299 pprTermM y p t@Term{dc=Right dc, subTerms=tt, ty=ty}
300 {- | dataConIsInfix dc, (t1:t2:tt') <- tt --TODO fixity
301 = parens (pprTerm1 True t1 <+> ppr dc <+> pprTerm1 True ppr t2)
302 <+> hsep (map (pprTerm1 True) tt)
303 -} -- TODO Printing infix constructors properly
304 | null tt = return$ ppr dc
305 | Just (tc,_) <- splitNewTyConApp_maybe ty
307 , Just new_dc <- maybeTyConSingleCon tc = do
308 real_value <- y 10 t{ty=repType ty}
309 return$ cparen (p >= app_prec) (ppr new_dc <+> real_value)
311 tt_docs <- mapM (y app_prec) tt
312 return$ cparen (p >= app_prec) (ppr dc <+> sep tt_docs)
314 pprTermM y _ t = pprTermM1 y t
315 pprTermM1 _ Prim{value=words, ty=ty} =
316 return$ text$ repPrim (tyConAppTyCon ty) words
317 pprTermM1 y t@Term{} = panic "pprTermM1 - unreachable"
318 pprTermM1 _ Suspension{bound_to=Nothing} = return$ char '_'
319 pprTermM1 _ Suspension{mb_ty=Just ty, bound_to=Just n}
320 | Just _ <- splitFunTy_maybe ty = return$ ptext SLIT("<function>")
321 | otherwise = return$ parens$ ppr n <> text "::" <> ppr ty
323 -- Takes a list of custom printers with a explicit recursion knot and a term,
324 -- and returns the output of the first succesful printer, or the default printer
325 cPprTerm :: forall m. Monad m =>
326 ((Int->Term->m SDoc)->[Int->Term->m (Maybe SDoc)]) -> Term -> m SDoc
327 cPprTerm custom = go 0 where
328 go prec t@Term{} = do
329 let default_ prec t = Just `liftM` pprTermM go prec t
330 mb_customDocs = [pp prec t | pp <- custom go ++ [default_]]
331 Just doc <- firstJustM mb_customDocs
332 return$ cparen (prec>app_prec+1) doc
333 go _ t = pprTermM1 go t
334 firstJustM (mb:mbs) = mb >>= maybe (firstJustM mbs) (return . Just)
335 firstJustM [] = return Nothing
337 -- Default set of custom printers. Note that the recursion knot is explicit
338 cPprTermBase :: Monad m => (Int->Term-> m SDoc)->[Int->Term->m (Maybe SDoc)]
341 ifTerm isTupleTy (\_ -> liftM (parens . hcat . punctuate comma)
342 . mapM (y (-1)) . subTerms)
343 , ifTerm (\t -> isTyCon listTyCon t && subTerms t `lengthIs` 2)
344 (\ p Term{subTerms=[h,t]} -> doList p h t)
345 , ifTerm (isTyCon intTyCon) (coerceShow$ \(a::Int)->a)
346 , ifTerm (isTyCon charTyCon) (coerceShow$ \(a::Char)->a)
347 -- , ifTerm (isTyCon wordTyCon) (coerceShow$ \(a::Word)->a)
348 , ifTerm (isTyCon floatTyCon) (coerceShow$ \(a::Float)->a)
349 , ifTerm (isTyCon doubleTyCon) (coerceShow$ \(a::Double)->a)
350 , ifTerm isIntegerTy (coerceShow$ \(a::Integer)->a)
352 where ifTerm pred f p t@Term{} | pred t = liftM Just (f p t)
353 ifTerm _ _ _ _ = return Nothing
354 isIntegerTy Term{ty=ty} = fromMaybe False $ do
355 (tc,_) <- splitTyConApp_maybe ty
356 return (tyConName tc == integerTyConName)
357 isTupleTy Term{ty=ty} = fromMaybe False $ do
358 (tc,_) <- splitTyConApp_maybe ty
359 return (tc `elem` (fst.unzip.elems) boxedTupleArr)
360 isTyCon a_tc Term{ty=ty} = fromMaybe False $ do
361 (tc,_) <- splitTyConApp_maybe ty
363 coerceShow f _ = return . text . show . f . unsafeCoerce# . val
364 --TODO pprinting of list terms is not lazy
366 let elems = h : getListTerms t
367 isConsLast = termType(last elems) /= termType h
368 print_elems <- mapM (y cons_prec) elems
369 return$ if isConsLast
370 then cparen (p >= cons_prec) . hsep . punctuate (space<>colon)
372 else brackets (hcat$ punctuate comma print_elems)
374 where Just a /= Just b = not (a `coreEqType` b)
376 getListTerms Term{subTerms=[h,t]} = h : getListTerms t
377 getListTerms t@Term{subTerms=[]} = []
378 getListTerms t@Suspension{} = [t]
379 getListTerms t = pprPanic "getListTerms" (ppr t)
382 repPrim :: TyCon -> [Word] -> String
383 repPrim t = rep where
385 | t == charPrimTyCon = show (build x :: Char)
386 | t == intPrimTyCon = show (build x :: Int)
387 | t == wordPrimTyCon = show (build x :: Word)
388 | t == floatPrimTyCon = show (build x :: Float)
389 | t == doublePrimTyCon = show (build x :: Double)
390 | t == int32PrimTyCon = show (build x :: Int32)
391 | t == word32PrimTyCon = show (build x :: Word32)
392 | t == int64PrimTyCon = show (build x :: Int64)
393 | t == word64PrimTyCon = show (build x :: Word64)
394 | t == addrPrimTyCon = show (nullPtr `plusPtr` build x)
395 | t == stablePtrPrimTyCon = "<stablePtr>"
396 | t == stableNamePrimTyCon = "<stableName>"
397 | t == statePrimTyCon = "<statethread>"
398 | t == realWorldTyCon = "<realworld>"
399 | t == threadIdPrimTyCon = "<ThreadId>"
400 | t == weakPrimTyCon = "<Weak>"
401 | t == arrayPrimTyCon = "<array>"
402 | t == byteArrayPrimTyCon = "<bytearray>"
403 | t == mutableArrayPrimTyCon = "<mutableArray>"
404 | t == mutableByteArrayPrimTyCon = "<mutableByteArray>"
405 | t == mutVarPrimTyCon= "<mutVar>"
406 | t == mVarPrimTyCon = "<mVar>"
407 | t == tVarPrimTyCon = "<tVar>"
408 | otherwise = showSDoc (char '<' <> ppr t <> char '>')
409 where build ww = unsafePerformIO $ withArray ww (peek . castPtr)
410 -- This ^^^ relies on the representation of Haskell heap values being
411 -- the same as in a C array.
413 -----------------------------------
414 -- Type Reconstruction
415 -----------------------------------
417 Type Reconstruction is type inference done on heap closures.
418 The algorithm walks the heap generating a set of equations, which
419 are solved with syntactic unification.
420 A type reconstruction equation looks like:
422 <datacon reptype> = <actual heap contents>
424 The full equation set is generated by traversing all the subterms, starting
427 The only difficult part is that newtypes are only found in the lhs of equations.
428 Right hand sides are missing them. We can either (a) drop them from the lhs, or
429 (b) reconstruct them in the rhs when possible.
431 The function congruenceNewtypes takes a shot at (b)
434 -- The Type Reconstruction monad
437 runTR :: HscEnv -> TR a -> IO a
439 mb_term <- runTR_maybe hsc_env c
441 Nothing -> panic "Can't unify"
444 runTR_maybe :: HscEnv -> TR a -> IO (Maybe a)
445 runTR_maybe hsc_env = fmap snd . initTc hsc_env HsSrcFile False iNTERACTIVE
448 trIO = liftTcM . ioToTcRn
450 liftTcM :: TcM a -> TR a
453 newVar :: Kind -> TR TcType
454 newVar = liftTcM . fmap mkTyVarTy . newFlexiTyVar
456 -- | Returns the instantiated type scheme ty', and the substitution sigma
457 -- such that sigma(ty') = ty
458 instScheme :: Type -> TR (TcType, TvSubst)
459 instScheme ty | (tvs, rho) <- tcSplitForAllTys ty = liftTcM$ do
460 (tvs',theta,ty') <- tcInstType (mapM tcInstTyVar) ty
461 return (ty', zipTopTvSubst tvs' (mkTyVarTys tvs))
463 -- Adds a constraint of the form t1 == t2
464 -- t1 is expected to come from walking the heap
465 -- t2 is expected to come from a datacon signature
466 -- Before unification, congruenceNewtypes needs to
468 addConstraint :: TcType -> TcType -> TR ()
469 addConstraint t1 t2 = congruenceNewtypes t1 t2 >>= uncurry unifyType
473 -- Type & Term reconstruction
474 cvObtainTerm :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Term
475 cvObtainTerm hsc_env force mb_ty hval = runTR hsc_env $ do
476 tv <- newVar argTypeKind
478 Nothing -> go tv tv hval >>= zonkTerm
479 Just ty | isMonomorphic ty -> go ty ty hval >>= zonkTerm
481 (ty',rev_subst) <- instScheme (sigmaType ty)
483 term <- go tv tv hval >>= zonkTerm
484 --restore original Tyvars
485 return$ mapTermType (substTy rev_subst) term
488 let monomorphic = not(isTyVarTy tv)
489 -- This ^^^ is a convention. The ancestor tests for
490 -- monomorphism and passes a type instead of a tv
491 clos <- trIO $ getClosureData a
493 -- Thunks we may want to force
494 -- NB. this won't attempt to force a BLACKHOLE. Even with :force, we never
495 -- force blackholes, because it would almost certainly result in deadlock,
496 -- and showing the '_' is more useful.
497 t | isThunk t && force -> seq a $ go tv ty a
498 -- We always follow indirections
499 Indirection _ -> go tv ty $! (ptrs clos ! 0)
500 -- The interesting case
502 Right dcname <- dataConInfoPtrToName (infoPtr clos)
503 (_,mb_dc) <- tryTcErrs (tcLookupDataCon dcname)
505 Nothing -> do -- This can happen for private constructors compiled -O0
506 -- where the .hi descriptor does not export them
507 -- In such case, we return a best approximation:
508 -- ignore the unpointed args, and recover the pointeds
509 -- This preserves laziness, and should be safe.
510 let tag = showSDoc (ppr dcname)
511 vars <- replicateM (length$ elems$ ptrs clos)
512 (newVar (liftedTypeKind))
513 subTerms <- sequence [appArr (go tv tv) (ptrs clos) i
514 | (i, tv) <- zip [0..] vars]
515 return (Term tv (Left ('<' : tag ++ ">")) a subTerms)
517 let extra_args = length(dataConRepArgTys dc) -
518 length(dataConOrigArgTys dc)
519 subTtypes = matchSubTypes dc ty
520 (subTtypesP, subTtypesNP) = partition isPointed subTtypes
521 subTermTvs <- sequence
522 [ if isMonomorphic t then return t
524 | (t,k) <- zip subTtypesP (map typeKind subTtypesP)]
525 -- It is vital for newtype reconstruction that the unification step
526 -- is done right here, _before_ the subterms are RTTI reconstructed
527 when (not monomorphic) $ do
528 let myType = mkFunTys (reOrderTerms subTermTvs
532 (signatureType,_) <- instScheme(dataConRepType dc)
533 addConstraint myType signatureType
534 subTermsP <- sequence $ drop extra_args
535 -- ^^^ all extra arguments are pointed
536 [ appArr (go tv t) (ptrs clos) i
537 | (i,tv,t) <- zip3 [0..] subTermTvs subTtypesP]
538 let unboxeds = extractUnboxed subTtypesNP clos
539 subTermsNP = map (uncurry Prim) (zip subTtypesNP unboxeds)
540 subTerms = reOrderTerms subTermsP subTermsNP
541 (drop extra_args subTtypes)
542 return (Term tv (Right dc) a subTerms)
543 -- The otherwise case: can be a Thunk,AP,PAP,etc.
545 return (Suspension (tipe clos) (Just tv) a Nothing)
548 | Just (_,ty_args) <- splitTyConApp_maybe (repType ty)
549 -- assumption: ^^^ looks through newtypes
550 , isVanillaDataCon dc --TODO non-vanilla case
551 = dataConInstArgTys dc ty_args
552 | otherwise = dataConRepArgTys dc
554 -- This is used to put together pointed and nonpointed subterms in the
556 reOrderTerms _ _ [] = []
557 reOrderTerms pointed unpointed (ty:tys)
558 | isPointed ty = ASSERT2(not(null pointed)
559 , ptext SLIT("reOrderTerms") $$
560 (ppr pointed $$ ppr unpointed))
561 head pointed : reOrderTerms (tail pointed) unpointed tys
562 | otherwise = ASSERT2(not(null unpointed)
563 , ptext SLIT("reOrderTerms") $$
564 (ppr pointed $$ ppr unpointed))
565 head unpointed : reOrderTerms pointed (tail unpointed) tys
569 -- Fast, breadth-first Type reconstruction
570 max_depth = 10 :: Int
571 cvReconstructType :: HscEnv -> Bool -> Maybe Type -> HValue -> IO (Maybe Type)
572 cvReconstructType hsc_env force mb_ty hval = runTR_maybe hsc_env $ do
573 tv <- newVar argTypeKind
575 Nothing -> do search (isMonomorphic `fmap` zonkTcType tv)
579 zonkTcType tv -- TODO untested!
580 Just ty | isMonomorphic ty -> return ty
582 (ty',rev_subst) <- instScheme (sigmaType ty)
584 search (isMonomorphic `fmap` zonkTcType tv)
588 substTy rev_subst `fmap` zonkTcType tv
590 -- search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m ()
591 search stop expand [] depth = return ()
592 search stop expand x 0 = fail$ "Failed to reconstruct a type after " ++
593 show max_depth ++ " steps"
594 search stop expand (x:xx) d = do
596 unlessM stop $ search stop expand (xx ++ new) $! (pred d)
598 -- returns unification tasks,since we are going to want a breadth-first search
599 go :: Type -> HValue -> TR [(Type, HValue)]
601 clos <- trIO $ getClosureData a
603 Indirection _ -> go tv $! (ptrs clos ! 0)
605 mb_dcname <- dataConInfoPtrToName (infoPtr clos)
608 vars <- replicateM (length$ elems$ ptrs clos)
609 (newVar (liftedTypeKind))
610 subTerms <- sequence [ appArr (go tv) (ptrs clos) i
611 | (i, tv) <- zip [0..] vars]
612 forM [0..length (elems $ ptrs clos)] $ \i -> do
613 tv <- newVar openTypeKind
614 return$ appArr (\e->(tv,e)) (ptrs clos) i
617 dc <- tcLookupDataCon name
618 let extra_args = length(dataConRepArgTys dc) -
619 length(dataConOrigArgTys dc)
620 subTtypes <- mapMif (not . isMonomorphic)
621 (\t -> newVar (typeKind t))
622 (dataConRepArgTys dc)
623 -- It is vital for newtype reconstruction that the unification step
624 -- is done right here, _before_ the subterms are RTTI reconstructed
625 let myType = mkFunTys subTtypes tv
626 (signatureType,_) <- instScheme(dataConRepType dc)
627 addConstraint myType signatureType
628 return $ [ appArr (\e->(t,e)) (ptrs clos) i
629 | (i,t) <- drop extra_args $ zip [0..] subTtypes]
630 otherwise -> return []
633 -- Dealing with newtypes
635 A parallel fold over two Type values,
636 compensating for missing newtypes on both sides.
637 This is necessary because newtypes are not present
638 in runtime, but since sometimes there is evidence
639 available we do our best to reconstruct them.
640 Evidence can come from DataCon signatures or
641 from compile-time type inference.
642 I am using the words congruence and rewriting
643 because what we are doing here is an approximation
644 of unification modulo a set of equations, which would
645 come from newtype definitions. These should be the
646 equality coercions seen in System Fc. Rewriting
647 is performed, taking those equations as rules,
648 before launching unification.
650 It doesn't make sense to rewrite everywhere,
651 or we would end up with all newtypes. So we rewrite
652 only in presence of evidence.
653 The lhs comes from the heap structure of ptrs,nptrs.
654 The rhs comes from a DataCon type signature.
655 Rewriting in the rhs is restricted to the result type.
657 Note that it is very tricky to make this 'rewriting'
658 work with the unification implemented by TcM, where
659 substitutions are 'inlined'. The order in which
660 constraints are unified is vital for this (or I am
663 congruenceNewtypes :: TcType -> TcType -> TcM (TcType,TcType)
664 congruenceNewtypes lhs rhs
665 -- TyVar lhs inductive case
666 | Just tv <- getTyVar_maybe lhs
667 = recoverTc (return (lhs,rhs)) $ do
668 Indirect ty_v <- readMetaTyVar tv
669 (lhs1, rhs1) <- congruenceNewtypes ty_v rhs
671 -- FunTy inductive case
672 | Just (l1,l2) <- splitFunTy_maybe lhs
673 , Just (r1,r2) <- splitFunTy_maybe rhs
674 = do (l2',r2') <- congruenceNewtypes l2 r2
675 (l1',r1') <- congruenceNewtypes l1 r1
676 return (mkFunTy l1' l2', mkFunTy r1' r2')
677 -- TyconApp Inductive case; this is the interesting bit.
678 | Just (tycon_l, args_l) <- splitNewTyConApp_maybe lhs
679 , Just (tycon_r, args_r) <- splitNewTyConApp_maybe rhs
681 = return (lhs, upgrade tycon_l rhs)
683 | otherwise = return (lhs,rhs)
685 where upgrade :: TyCon -> Type -> Type
687 | not (isNewTyCon new_tycon) = ty
688 | ty' <- mkTyConApp new_tycon (map mkTyVarTy $ tyConTyVars new_tycon)
689 , Just subst <- tcUnifyTys (const BindMe) [ty] [repType ty']
691 -- assumes that reptype doesn't touch tyconApp args ^^^
694 --------------------------------------------------------------------------------
695 -- Semantically different to recoverM in TcRnMonad
696 -- recoverM retains the errors in the first action,
697 -- whereas recoverTc here does not
698 recoverTc recover thing = do
699 (_,mb_res) <- tryTcErrs thing
702 Just res -> return res
704 isMonomorphic ty | (tvs, ty') <- splitForAllTys ty
705 = null tvs && (isEmptyVarSet . tyVarsOfType) ty'
707 mapMif :: Monad m => (a -> Bool) -> (a -> m a) -> [a] -> m [a]
708 mapMif pred f xx = sequence $ mapMif_ pred f xx
709 mapMif_ pred f [] = []
710 mapMif_ pred f (x:xx) = (if pred x then f x else return x) : mapMif_ pred f xx
712 unlessM condM acc = condM >>= \c -> unless c acc
714 -- Strict application of f at index i
715 appArr f a@(Array _ _ ptrs#) i@(I# i#) = ASSERT (i < length(elems a))
716 case indexArray# ptrs# i# of
719 zonkTerm :: Term -> TcM Term
720 zonkTerm = foldTerm idTermFoldM {
721 fTerm = \ty dc v tt -> sequence tt >>= \tt ->
722 zonkTcType ty >>= \ty' ->
723 return (Term ty' dc v tt)
724 ,fSuspension = \ct ty v b -> fmapMMaybe zonkTcType ty >>= \ty ->
725 return (Suspension ct ty v b)}
728 -- Is this defined elsewhere?
729 -- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
730 sigmaType ty = mkForAllTys (varSetElems$ tyVarsOfType (dropForAlls ty)) ty