wibble
[ghc.git] / compiler / ghci / RtClosureInspect.hs
1 -----------------------------------------------------------------------------
2 --
3 -- GHC Interactive support for inspecting arbitrary closures at runtime
4 --
5 -- Pepe Iborra (supported by Google SoC) 2006
6 --
7 -----------------------------------------------------------------------------
8
9 module RtClosureInspect(
10
11 cvObtainTerm, -- :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Term
12
13 Term(..),
14 pprTerm,
15 cPprTerm,
16 cPprTermBase,
17 termType,
18 foldTerm,
19 TermFold(..),
20 idTermFold,
21 idTermFoldM,
22 isFullyEvaluated,
23 isPointed,
24 isFullyEvaluatedTerm,
25 mapTermType,
26 termTyVars,
27 -- unsafeDeepSeq,
28 cvReconstructType
29 ) where
30
31 #include "HsVersions.h"
32
33 import ByteCodeItbls ( StgInfoTable )
34 import qualified ByteCodeItbls as BCI( StgInfoTable(..) )
35 import ByteCodeLink ( HValue )
36 import HscTypes ( HscEnv )
37
38 import DataCon
39 import Type
40 import TcRnMonad ( TcM, initTcPrintErrors, ioToTcRn, recoverM, writeMutVar )
41 import TcType
42 import TcMType
43 import TcUnify
44 import TcGadt
45 import TyCon
46 import Var
47 import Name
48 import VarEnv
49 import OccName
50 import VarSet
51 import {-#SOURCE#-} TcRnDriver ( tcRnRecoverDataCon )
52
53 import TysPrim
54 import PrelNames
55 import TysWiredIn
56
57 import Constants
58 import Outputable
59 import Maybes
60 import Panic
61 import FiniteMap
62
63 import GHC.Arr ( Array(..) )
64 import GHC.Ptr ( Ptr(..), castPtr )
65 import GHC.Exts
66
67 import Control.Monad
68 import Data.Maybe
69 import Data.Array.Base
70 import Data.List ( partition, nub )
71 import Foreign
72
73 ---------------------------------------------
74 -- * A representation of semi evaluated Terms
75 ---------------------------------------------
76 {-
77 A few examples in this representation:
78
79 > Just 10 = Term Data.Maybe Data.Maybe.Just (Just 10) [Term Int I# (10) "10"]
80
81 > (('a',_,_),_,('b',_,_)) =
82 Term ((Char,b,c),d,(Char,e,f)) (,,) (('a',_,_),_,('b',_,_))
83 [ Term (Char, b, c) (,,) ('a',_,_) [Term Char C# "a", Suspension, Suspension]
84 , Suspension
85 , Term (Char, e, f) (,,) ('b',_,_) [Term Char C# "b", Suspension, Suspension]]
86 -}
87
88 data Term = Term { ty :: Type
89 , dc :: DataCon
90 , val :: HValue
91 , subTerms :: [Term] }
92
93 | Prim { ty :: Type
94 , value :: [Word] }
95
96 | Suspension { ctype :: ClosureType
97 , mb_ty :: Maybe Type
98 , val :: HValue
99 , bound_to :: Maybe Name -- Useful for printing
100 }
101
102 isTerm Term{} = True
103 isTerm _ = False
104 isSuspension Suspension{} = True
105 isSuspension _ = False
106 isPrim Prim{} = True
107 isPrim _ = False
108
109 termType t@(Suspension {}) = mb_ty t
110 termType t = Just$ ty t
111
112 isFullyEvaluatedTerm :: Term -> Bool
113 isFullyEvaluatedTerm Term {subTerms=tt} = all isFullyEvaluatedTerm tt
114 isFullyEvaluatedTerm Suspension {} = False
115 isFullyEvaluatedTerm Prim {} = True
116
117 instance Outputable (Term) where
118 ppr = head . cPprTerm cPprTermBase
119
120 -------------------------------------------------------------------------
121 -- Runtime Closure Datatype and functions for retrieving closure related stuff
122 -------------------------------------------------------------------------
123 data ClosureType = Constr
124 | Fun
125 | Thunk Int
126 | ThunkSelector
127 | Blackhole
128 | AP
129 | PAP
130 | Indirection Int
131 | Other Int
132 deriving (Show, Eq)
133
134 data Closure = Closure { tipe :: ClosureType
135 , infoPtr :: Ptr ()
136 , infoTable :: StgInfoTable
137 , ptrs :: Array Int HValue
138 , nonPtrs :: [Word]
139 }
140
141 instance Outputable ClosureType where
142 ppr = text . show
143
144 #include "../includes/ClosureTypes.h"
145
146 aP_CODE = AP
147 pAP_CODE = PAP
148 #undef AP
149 #undef PAP
150
151 getClosureData :: a -> IO Closure
152 getClosureData a =
153 case unpackClosure# a of
154 (# iptr, ptrs, nptrs #) -> do
155 itbl <- peek (Ptr iptr)
156 let tipe = readCType (BCI.tipe itbl)
157 elems = BCI.ptrs itbl
158 ptrsList = Array 0 (fromIntegral$ elems) ptrs
159 nptrs_data = [W# (indexWordArray# nptrs i)
160 | I# i <- [0.. fromIntegral (BCI.nptrs itbl)] ]
161 ptrsList `seq` return (Closure tipe (Ptr iptr) itbl ptrsList nptrs_data)
162
163 readCType :: Integral a => a -> ClosureType
164 readCType i
165 | i >= CONSTR && i <= CONSTR_NOCAF_STATIC = Constr
166 | i >= FUN && i <= FUN_STATIC = Fun
167 | i >= THUNK && i < THUNK_SELECTOR = Thunk (fromIntegral i)
168 | i == THUNK_SELECTOR = ThunkSelector
169 | i == BLACKHOLE = Blackhole
170 | i >= IND && i <= IND_STATIC = Indirection (fromIntegral i)
171 | fromIntegral i == aP_CODE = AP
172 | i == AP_STACK = AP
173 | fromIntegral i == pAP_CODE = PAP
174 | otherwise = Other (fromIntegral i)
175
176 isConstr, isIndirection :: ClosureType -> Bool
177 isConstr Constr = True
178 isConstr _ = False
179
180 isIndirection (Indirection _) = True
181 --isIndirection ThunkSelector = True
182 isIndirection _ = False
183
184 isThunk (Thunk _) = True
185 isThunk ThunkSelector = True
186 isThunk AP = True
187 isThunk _ = False
188
189 isFullyEvaluated :: a -> IO Bool
190 isFullyEvaluated a = do
191 closure <- getClosureData a
192 case tipe closure of
193 Constr -> do are_subs_evaluated <- amapM isFullyEvaluated (ptrs closure)
194 return$ and are_subs_evaluated
195 otherwise -> return False
196 where amapM f = sequence . amap' f
197
198 amap' f (Array i0 i arr#) = map (\(I# i#) -> case indexArray# arr# i# of
199 (# e #) -> f e)
200 [0 .. i - i0]
201
202 -- TODO: Fix it. Probably the otherwise case is failing, trace/debug it
203 {-
204 unsafeDeepSeq :: a -> b -> b
205 unsafeDeepSeq = unsafeDeepSeq1 2
206 where unsafeDeepSeq1 0 a b = seq a $! b
207 unsafeDeepSeq1 i a b -- 1st case avoids infinite loops for non reducible thunks
208 | not (isConstr tipe) = seq a $! unsafeDeepSeq1 (i-1) a b
209 -- | unsafePerformIO (isFullyEvaluated a) = b
210 | otherwise = case unsafePerformIO (getClosureData a) of
211 closure -> foldl' (flip unsafeDeepSeq) b (ptrs closure)
212 where tipe = unsafePerformIO (getClosureType a)
213 -}
214 isPointed :: Type -> Bool
215 isPointed t | Just (t, _) <- splitTyConApp_maybe t = not$ isUnliftedTypeKind (tyConKind t)
216 isPointed _ = True
217
218 extractUnboxed :: [Type] -> Closure -> [[Word]]
219 extractUnboxed tt clos = go tt (nonPtrs clos)
220 where sizeofType t
221 | Just (tycon,_) <- splitTyConApp_maybe t
222 = ASSERT (isPrimTyCon tycon) sizeofTyCon tycon
223 | otherwise = pprPanic "Expected a TcTyCon" (ppr t)
224 go [] _ = []
225 go (t:tt) xx
226 | (x, rest) <- splitAt (sizeofType t `div` wORD_SIZE) xx
227 = x : go tt rest
228
229 sizeofTyCon = sizeofPrimRep . tyConPrimRep
230
231 -----------------------------------
232 -- * Traversals for Terms
233 -----------------------------------
234
235 data TermFold a = TermFold { fTerm :: Type -> DataCon -> HValue -> [a] -> a
236 , fPrim :: Type -> [Word] -> a
237 , fSuspension :: ClosureType -> Maybe Type -> HValue -> Maybe Name -> a
238 }
239
240 foldTerm :: TermFold a -> Term -> a
241 foldTerm tf (Term ty dc v tt) = fTerm tf ty dc v (map (foldTerm tf) tt)
242 foldTerm tf (Prim ty v ) = fPrim tf ty v
243 foldTerm tf (Suspension ct ty v b) = fSuspension tf ct ty v b
244
245 idTermFold :: TermFold Term
246 idTermFold = TermFold {
247 fTerm = Term,
248 fPrim = Prim,
249 fSuspension = Suspension
250 }
251 idTermFoldM :: Monad m => TermFold (m Term)
252 idTermFoldM = TermFold {
253 fTerm = \ty dc v tt -> sequence tt >>= return . Term ty dc v,
254 fPrim = (return.). Prim,
255 fSuspension = (((return.).).). Suspension
256 }
257
258 mapTermType f = foldTerm idTermFold {
259 fTerm = \ty dc hval tt -> Term (f ty) dc hval tt,
260 fSuspension = \ct mb_ty hval n ->
261 Suspension ct (fmap f mb_ty) hval n }
262
263 termTyVars = foldTerm TermFold {
264 fTerm = \ty _ _ tt ->
265 tyVarsOfType ty `plusVarEnv` concatVarEnv tt,
266 fSuspension = \_ mb_ty _ _ ->
267 maybe emptyVarEnv tyVarsOfType mb_ty,
268 fPrim = \ _ _ -> emptyVarEnv }
269 where concatVarEnv = foldr plusVarEnv emptyVarEnv
270 ----------------------------------
271 -- Pretty printing of terms
272 ----------------------------------
273
274 app_prec::Int
275 app_prec = 10
276
277 pprTerm :: Int -> Term -> SDoc
278 pprTerm p Term{dc=dc, subTerms=tt}
279 {- | dataConIsInfix dc, (t1:t2:tt') <- tt
280 = parens (pprTerm1 True t1 <+> ppr dc <+> pprTerm1 True ppr t2)
281 <+> hsep (map (pprTerm1 True) tt)
282 -}
283 | null tt = ppr dc
284 | otherwise = cparen (p >= app_prec)
285 (ppr dc <+> sep (map (pprTerm app_prec) tt))
286
287 where fixity = undefined
288
289 pprTerm _ t = pprTerm1 t
290
291 pprTerm1 Prim{value=words, ty=ty} = text$ repPrim (tyConAppTyCon ty) words
292 pprTerm1 t@Term{} = pprTerm 0 t
293 pprTerm1 Suspension{bound_to=Nothing} = char '_' -- <> ppr ct <> char '_'
294 pprTerm1 Suspension{mb_ty=Just ty, bound_to=Just n}
295 | Just _ <- splitFunTy_maybe ty = ptext SLIT("<function>")
296 | otherwise = parens$ ppr n <> text "::" <> ppr ty
297
298
299 cPprTerm :: forall m. Monad m => ((Int->Term->m SDoc)->[Int->Term->m (Maybe SDoc)]) -> Term -> m SDoc
300 cPprTerm custom = go 0 where
301 go prec t@Term{subTerms=tt, dc=dc} = do
302 let mb_customDocs = map (($t) . ($prec)) (custom go) :: [m (Maybe SDoc)]
303 first_success <- firstJustM mb_customDocs
304 case first_success of
305 Just doc -> return$ cparen (prec>app_prec+1) doc
306 -- | dataConIsInfix dc, (t1:t2:tt') <- tt =
307 Nothing -> do pprSubterms <- mapM (go (app_prec+1)) tt
308 return$ cparen (prec >= app_prec)
309 (ppr dc <+> sep pprSubterms)
310 go _ t = return$ pprTerm1 t
311 firstJustM (mb:mbs) = mb >>= maybe (firstJustM mbs) (return . Just)
312 firstJustM [] = return Nothing
313
314 cPprTermBase :: Monad m => (Int->Term-> m SDoc)->[Int->Term->m (Maybe SDoc)]
315 cPprTermBase pprP =
316 [
317 ifTerm isTupleDC (\_ -> liftM (parens . hcat . punctuate comma)
318 . mapM (pprP (-1)) . subTerms)
319 , ifTerm (isDC consDataCon) (\ p Term{subTerms=[h,t]} -> doList p h t)
320 , ifTerm (isDC intDataCon) (coerceShow$ \(a::Int)->a)
321 , ifTerm (isDC charDataCon) (coerceShow$ \(a::Char)->a)
322 -- , ifTerm (isDC wordDataCon) (coerceShow$ \(a::Word)->a)
323 , ifTerm (isDC floatDataCon) (coerceShow$ \(a::Float)->a)
324 , ifTerm (isDC doubleDataCon) (coerceShow$ \(a::Double)->a)
325 , ifTerm isIntegerDC (coerceShow$ \(a::Integer)->a)
326 ]
327 where ifTerm pred f p t = if pred t then liftM Just (f p t) else return Nothing
328 isIntegerDC Term{dc=dc} =
329 dataConName dc `elem` [ smallIntegerDataConName
330 , largeIntegerDataConName]
331 isTupleDC Term{dc=dc} = dc `elem` snd (unzip (elems boxedTupleArr))
332 isDC a_dc Term{dc=dc} = a_dc == dc
333 coerceShow f _ = return . text . show . f . unsafeCoerce# . val
334 --TODO pprinting of list terms is not lazy
335 doList p h t = do
336 let elems = h : getListTerms t
337 isConsLast = termType(last elems) /= termType h
338 print_elems <- mapM (pprP 5) elems
339 return$ if isConsLast
340 then cparen (p >= 5) . hsep . punctuate (space<>colon)
341 $ print_elems
342 else brackets (hcat$ punctuate comma print_elems)
343
344 where Just a /= Just b = not (a `coreEqType` b)
345 _ /= _ = True
346 getListTerms Term{subTerms=[h,t]} = h : getListTerms t
347 getListTerms t@Term{subTerms=[]} = []
348 getListTerms t@Suspension{} = [t]
349 getListTerms t = pprPanic "getListTerms" (ppr t)
350
351 repPrim :: TyCon -> [Word] -> String
352 repPrim t = rep where
353 rep x
354 | t == charPrimTyCon = show (build x :: Char)
355 | t == intPrimTyCon = show (build x :: Int)
356 | t == wordPrimTyCon = show (build x :: Word)
357 | t == floatPrimTyCon = show (build x :: Float)
358 | t == doublePrimTyCon = show (build x :: Double)
359 | t == int32PrimTyCon = show (build x :: Int32)
360 | t == word32PrimTyCon = show (build x :: Word32)
361 | t == int64PrimTyCon = show (build x :: Int64)
362 | t == word64PrimTyCon = show (build x :: Word64)
363 | t == addrPrimTyCon = show (nullPtr `plusPtr` build x)
364 | t == stablePtrPrimTyCon = "<stablePtr>"
365 | t == stableNamePrimTyCon = "<stableName>"
366 | t == statePrimTyCon = "<statethread>"
367 | t == realWorldTyCon = "<realworld>"
368 | t == threadIdPrimTyCon = "<ThreadId>"
369 | t == weakPrimTyCon = "<Weak>"
370 | t == arrayPrimTyCon = "<array>"
371 | t == byteArrayPrimTyCon = "<bytearray>"
372 | t == mutableArrayPrimTyCon = "<mutableArray>"
373 | t == mutableByteArrayPrimTyCon = "<mutableByteArray>"
374 | t == mutVarPrimTyCon= "<mutVar>"
375 | t == mVarPrimTyCon = "<mVar>"
376 | t == tVarPrimTyCon = "<tVar>"
377 | otherwise = showSDoc (char '<' <> ppr t <> char '>')
378 where build ww = unsafePerformIO $ withArray ww (peek . castPtr)
379
380 -----------------------------------
381 -- Type Reconstruction
382 -----------------------------------
383 {-
384 Type Reconstruction is type inference done on heap closures.
385 The algorithm walks the heap generating a set of equations, which
386 are solved with syntactic unification.
387 A type reconstruction equation looks like:
388
389 <datacon reptype> = <actual heap contents>
390
391 The full equation set is generated by traversing all the subterms, starting
392 from a given term.
393
394 The only difficult part is that newtypes are only found in the lhs of equations.
395 Right hand sides are missing them. We can either (a) drop them from the lhs, or
396 (b) reconstruct them in the rhs when possible.
397
398 The function congruenceNewtypes takes a shot at (b)
399 -}
400
401 -- The Type Reconstruction monad
402 type TR a = TcM a
403
404 runTR :: HscEnv -> TR a -> IO a
405 runTR hsc_env c = do
406 mb_term <- initTcPrintErrors hsc_env iNTERACTIVE c
407 case mb_term of
408 Nothing -> panic "Can't unify"
409 Just x -> return x
410
411 trIO :: IO a -> TR a
412 trIO = liftTcM . ioToTcRn
413
414 liftTcM = id
415
416 newVar :: Kind -> TR TcTyVar
417 newVar = liftTcM . newFlexiTyVar
418
419 -- | Returns the instantiated type scheme ty', and the substitution sigma
420 -- such that sigma(ty') = ty
421 instScheme :: Type -> TR (TcType, TvSubst)
422 instScheme ty | (tvs, rho) <- tcSplitForAllTys ty = liftTcM$ do
423 (tvs',theta,ty') <- tcInstType (mapM tcInstTyVar) ty
424 return (ty', zipTopTvSubst tvs' (mkTyVarTys tvs))
425
426 addConstraint :: TcType -> TcType -> TR ()
427 addConstraint t1 t2 = congruenceNewtypes t1 t2 >>= uncurry unifyType
428
429
430
431 -- Type & Term reconstruction
432 cvObtainTerm :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Term
433 cvObtainTerm hsc_env force mb_ty hval = runTR hsc_env $ do
434 tv <- liftM mkTyVarTy (newVar argTypeKind)
435 case mb_ty of
436 Nothing -> go tv tv hval >>= zonkTerm
437 Just ty | isMonomorphic ty -> go ty ty hval >>= zonkTerm
438 Just ty -> do
439 (ty',rev_subst) <- instScheme (sigmaType ty)
440 addConstraint tv ty'
441 term <- go tv tv hval >>= zonkTerm
442 --restore original Tyvars
443 return$ mapTermType (substTy rev_subst) term
444 where
445 go tv ty a = do
446 let monomorphic = not(isTyVarTy tv) -- This is a convention. The ancestor tests for
447 -- monomorphism and passes a type instead of a tv
448 clos <- trIO $ getClosureData a
449 case tipe clos of
450 -- Thunks we may want to force
451 -- NB. this won't attempt to force a BLACKHOLE. Even with :force, we never
452 -- force blackholes, because it would almost certainly result in deadlock,
453 -- and showing the '_' is more useful.
454 t | isThunk t && force -> seq a $ go tv ty a
455 -- We always follow indirections
456 Indirection _ -> go tv ty $! (ptrs clos ! 0)
457 -- The interesting case
458 Constr -> do
459 m_dc <- trIO$ tcRnRecoverDataCon hsc_env (infoPtr clos)
460 case m_dc of
461 Nothing -> panic "Can't find the DataCon for a term"
462 Just dc -> do
463 let extra_args = length(dataConRepArgTys dc) - length(dataConOrigArgTys dc)
464 subTtypes = matchSubTypes dc ty
465 (subTtypesP, subTtypesNP) = partition isPointed subTtypes
466 subTermTvs <- sequence
467 [ if isMonomorphic t then return t else (mkTyVarTy `fmap` newVar k)
468 | (t,k) <- zip subTtypesP (map typeKind subTtypesP)]
469 -- It is vital for newtype reconstruction that the unification step is done
470 -- right here, _before_ the subterms are RTTI reconstructed.
471 when (not monomorphic) $ do
472 let myType = mkFunTys (reOrderTerms subTermTvs subTtypesNP subTtypes) tv
473 instScheme(dataConRepType dc) >>= addConstraint myType . fst
474 subTermsP <- sequence $ drop extra_args -- all extra arguments are pointed
475 [ appArr (go tv t) (ptrs clos) i
476 | (i,tv,t) <- zip3 [0..] subTermTvs subTtypesP]
477 let unboxeds = extractUnboxed subTtypesNP clos
478 subTermsNP = map (uncurry Prim) (zip subTtypesNP unboxeds)
479 subTerms = reOrderTerms subTermsP subTermsNP (drop extra_args subTtypes)
480 return (Term tv dc a subTerms)
481 -- The otherwise case: can be a Thunk,AP,PAP,etc.
482 otherwise ->
483 return (Suspension (tipe clos) (Just tv) a Nothing)
484
485 matchSubTypes dc ty
486 | Just (_,ty_args) <- splitTyConApp_maybe (repType ty)
487 , null (dataConExTyVars dc) --TODO Handle the case of extra existential tyvars
488 = dataConInstArgTys dc ty_args
489
490 | otherwise = dataConRepArgTys dc
491
492 -- This is used to put together pointed and nonpointed subterms in the
493 -- correct order.
494 reOrderTerms _ _ [] = []
495 reOrderTerms pointed unpointed (ty:tys)
496 | isPointed ty = ASSERT2(not(null pointed)
497 , ptext SLIT("reOrderTerms") $$ (ppr pointed $$ ppr unpointed))
498 head pointed : reOrderTerms (tail pointed) unpointed tys
499 | otherwise = ASSERT2(not(null unpointed)
500 , ptext SLIT("reOrderTerms") $$ (ppr pointed $$ ppr unpointed))
501 head unpointed : reOrderTerms pointed (tail unpointed) tys
502
503
504
505 -- Fast, breadth-first version of obtainTerm that deals only with type reconstruction
506
507 cvReconstructType :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Type
508 cvReconstructType hsc_env force mb_ty hval = runTR hsc_env $ do
509 tv <- liftM mkTyVarTy (newVar argTypeKind)
510 case mb_ty of
511 Nothing -> search (isMonomorphic `fmap` zonkTcType tv) (++) [(tv, hval)] >>
512 zonkTcType tv -- TODO untested!
513 Just ty | isMonomorphic ty -> return ty
514 Just ty -> do
515 (ty',rev_subst) <- instScheme (sigmaType ty)
516 addConstraint tv ty'
517 search (isMonomorphic `fmap` zonkTcType tv) (++) [(tv, hval)]
518 substTy rev_subst `fmap` zonkTcType tv
519 where
520 -- search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m ()
521 search stop combine [] = return ()
522 search stop combine ((t,a):jj) = (jj `combine`) `fmap` go t a >>=
523 unlessM stop . search stop combine
524
525 -- returns unification tasks, since we are going to want a breadth-first search
526 go :: Type -> HValue -> TR [(Type, HValue)]
527 go tv a = do
528 clos <- trIO $ getClosureData a
529 case tipe clos of
530 Indirection _ -> go tv $! (ptrs clos ! 0)
531 Constr -> do
532 m_dc <- trIO$ tcRnRecoverDataCon hsc_env (infoPtr clos)
533 case m_dc of
534 Nothing -> panic "Can't find the DataCon for a term"
535 Just dc -> do
536 let extra_args = length(dataConRepArgTys dc) - length(dataConOrigArgTys dc)
537 subTtypes <- mapMif (not . isMonomorphic)
538 (\t -> mkTyVarTy `fmap` newVar (typeKind t))
539 (dataConRepArgTys dc)
540 -- It is vital for newtype reconstruction that the unification step is done
541 -- right here, _before_ the subterms are RTTI reconstructed.
542 let myType = mkFunTys subTtypes tv
543 fst `fmap` instScheme(dataConRepType dc) >>= addConstraint myType
544 return $map (\(I# i#,t) -> case ptrs clos of
545 (Array _ _ ptrs#) -> case indexArray# ptrs# i# of
546 (# e #) -> (t,e))
547 (drop extra_args $ zip [0..] subTtypes)
548 otherwise -> return []
549
550
551 -- Dealing with newtypes
552 {-
553 A parallel fold over two Type values,
554 compensating for missing newtypes on both sides.
555 This is necessary because newtypes are not present
556 in runtime, but since sometimes there is evidence
557 available we do our best to reconstruct them.
558 Evidence can come from DataCon signatures or
559 from compile-time type inference.
560 I am using the words congruence and rewriting
561 because what we are doing here is an approximation
562 of unification modulo a set of equations, which would
563 come from newtype definitions. These should be the
564 equality coercions seen in System Fc. Rewriting
565 is performed, taking those equations as rules,
566 before launching unification.
567
568 It doesn't make sense to rewrite everywhere,
569 or we would end up with all newtypes. So we rewrite
570 only in presence of evidence.
571 The lhs comes from the heap structure of ptrs,nptrs.
572 The rhs comes from a DataCon type signature.
573 Rewriting in the rhs is restricted to the result type.
574
575 Note that it is very tricky to make this 'rewriting'
576 work with the unification implemented by TcM, where
577 substitutions are 'inlined'. The order in which
578 constraints are unified is vital for this (or I am
579 using TcM wrongly).
580 -}
581 congruenceNewtypes :: TcType -> TcType -> TcM (TcType,TcType)
582 congruenceNewtypes = go True
583 where
584 go rewriteRHS lhs rhs
585 -- TyVar lhs inductive case
586 | Just tv <- getTyVar_maybe lhs
587 = recoverM (return (lhs,rhs)) $ do
588 Indirect ty_v <- readMetaTyVar tv
589 (lhs', rhs') <- go rewriteRHS ty_v rhs
590 writeMutVar (metaTvRef tv) (Indirect lhs')
591 return (lhs, rhs')
592 -- TyVar rhs inductive case
593 | Just tv <- getTyVar_maybe rhs
594 = recoverM (return (lhs,rhs)) $ do
595 Indirect ty_v <- readMetaTyVar tv
596 (lhs', rhs') <- go rewriteRHS lhs ty_v
597 writeMutVar (metaTvRef tv) (Indirect rhs')
598 return (lhs', rhs)
599 -- FunTy inductive case
600 | Just (l1,l2) <- splitFunTy_maybe lhs
601 , Just (r1,r2) <- splitFunTy_maybe rhs
602 = do (l2',r2') <- go True l2 r2
603 (l1',r1') <- go False l1 r1
604 return (mkFunTy l1' l2', mkFunTy r1' r2')
605 -- TyconApp Inductive case; this is the interesting bit.
606 | Just (tycon_l, args_l) <- splitNewTyConApp_maybe lhs
607 , Just (tycon_r, args_r) <- splitNewTyConApp_maybe rhs = do
608
609 let (tycon_l',args_l') = if isNewTyCon tycon_r && not(isNewTyCon tycon_l)
610 then (tycon_r, rewrite tycon_r lhs)
611 else (tycon_l, args_l)
612 (tycon_r',args_r') = if rewriteRHS && isNewTyCon tycon_l && not(isNewTyCon tycon_r)
613 then (tycon_l, rewrite tycon_l rhs)
614 else (tycon_r, args_r)
615 (args_l'', args_r'') <- unzip `liftM` zipWithM (go rewriteRHS) args_l' args_r'
616 return (mkTyConApp tycon_l' args_l'', mkTyConApp tycon_r' args_r'')
617
618 | otherwise = return (lhs,rhs)
619
620 where rewrite newtyped_tc lame_tipe
621 | (tvs, tipe) <- newTyConRep newtyped_tc
622 = case tcUnifyTys (const BindMe) [tipe] [lame_tipe] of
623 Just subst -> substTys subst (map mkTyVarTy tvs)
624 otherwise -> panic "congruenceNewtypes: Can't unify a newtype"
625
626
627 ------------------------------------------------------------------------------------
628
629 isMonomorphic ty | (tvs, ty') <- splitForAllTys ty
630 = null tvs && (isEmptyVarSet . tyVarsOfType) ty'
631
632 mapMif :: Monad m => (a -> Bool) -> (a -> m a) -> [a] -> m [a]
633 mapMif pred f xx = sequence $ mapMif_ pred f xx
634 mapMif_ pred f [] = []
635 mapMif_ pred f (x:xx) = (if pred x then f x else return x) : mapMif_ pred f xx
636
637 unlessM condM acc = condM >>= \c -> unless c acc
638
639 -- Strict application of f at index i
640 appArr f (Array _ _ ptrs#) (I# i#) = case indexArray# ptrs# i# of
641 (# e #) -> f e
642
643 zonkTerm :: Term -> TcM Term
644 zonkTerm = foldTerm idTermFoldM {
645 fTerm = \ty dc v tt -> sequence tt >>= \tt ->
646 zonkTcType ty >>= \ty' ->
647 return (Term ty' dc v tt)
648 ,fSuspension = \ct ty v b -> fmapMMaybe zonkTcType ty >>= \ty ->
649 return (Suspension ct ty v b)}
650
651
652 -- Is this defined elsewhere?
653 -- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
654 sigmaType ty = mkForAllTys (varSetElems$ tyVarsOfType (dropForAlls ty)) ty
655
656