RtClosureInspect.hs 25.1 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
-----------------------------------------------------------------------------
--
-- GHC Interactive support for inspecting arbitrary closures at runtime
--
-- Pepe Iborra (supported by Google SoC) 2006
--
-----------------------------------------------------------------------------

module RtClosureInspect(
  
     cvObtainTerm,       -- :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Term

Simon Marlow's avatar
Simon Marlow committed
13
     Term(..),
14
15
16
     pprTerm, 
     cPprTerm, 
     cPprTermBase,
17
18
19
20
21
22
23
24
     termType,
     foldTerm, 
     TermFold(..), 
     idTermFold, 
     idTermFoldM,
     isFullyEvaluated, 
     isPointed,
     isFullyEvaluatedTerm,
25
     mapTermType,
26
     termTyVars,
27
--     unsafeDeepSeq, 
mnislaih's avatar
wibble    
mnislaih committed
28
     cvReconstructType
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
 ) where 

#include "HsVersions.h"

import ByteCodeItbls    ( StgInfoTable )
import qualified ByteCodeItbls as BCI( StgInfoTable(..) )
import ByteCodeLink     ( HValue )
import HscTypes         ( HscEnv )

import DataCon          
import Type             
import TcRnMonad        ( TcM, initTcPrintErrors, ioToTcRn, recoverM, writeMutVar )
import TcType
import TcMType
import TcUnify
import TcGadt
import TyCon		
import Var
import Name 
import VarEnv
import OccName
import VarSet
import {-#SOURCE#-} TcRnDriver ( tcRnRecoverDataCon )

import TysPrim		
import PrelNames
import TysWiredIn

57
import Constants
58
59
60
61
62
63
64
import Outputable
import Maybes
import Panic
import FiniteMap

import GHC.Arr          ( Array(..) )
import GHC.Ptr          ( Ptr(..), castPtr )
65
import GHC.Exts
66
67
68
69

import Control.Monad
import Data.Maybe
import Data.Array.Base
70
import Data.List        ( partition, nub )
71
import Foreign
72

73
74
75
76
77
78
79
80
81
82
---------------------------------------------
-- * A representation of semi evaluated Terms
---------------------------------------------
{-
  A few examples in this representation:

  > Just 10 = Term Data.Maybe Data.Maybe.Just (Just 10) [Term Int I# (10) "10"]

  > (('a',_,_),_,('b',_,_)) = 
      Term ((Char,b,c),d,(Char,e,f)) (,,) (('a',_,_),_,('b',_,_))
83
84
85
          [ Term (Char, b, c) (,,) ('a',_,_) [Term Char C# "a", Suspension, Suspension]
          , Suspension
          , Term (Char, e, f) (,,) ('b',_,_) [Term Char C# "b", Suspension, Suspension]]
86
87
88
89
90
91
92
93
-}

data Term = Term { ty        :: Type 
                 , dc        :: DataCon 
                 , val       :: HValue 
                 , subTerms  :: [Term] }

          | Prim { ty        :: Type
94
                 , value     :: [Word] }
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111

          | Suspension { ctype    :: ClosureType
                       , mb_ty    :: Maybe Type
                       , val      :: HValue
                       , bound_to :: Maybe Name   -- Useful for printing
                       }

isTerm Term{} = True
isTerm   _    = False
isSuspension Suspension{} = True
isSuspension      _       = False
isPrim Prim{} = True
isPrim   _    = False

termType t@(Suspension {}) = mb_ty t
termType t = Just$ ty t

mnislaih's avatar
mnislaih committed
112
113
114
115
116
isFullyEvaluatedTerm :: Term -> Bool
isFullyEvaluatedTerm Term {subTerms=tt} = all isFullyEvaluatedTerm tt
isFullyEvaluatedTerm Suspension {}      = False
isFullyEvaluatedTerm Prim {}            = True

117
instance Outputable (Term) where
118
 ppr = head . cPprTerm cPprTermBase
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134

-------------------------------------------------------------------------
-- Runtime Closure Datatype and functions for retrieving closure related stuff
-------------------------------------------------------------------------
data ClosureType = Constr 
                 | Fun 
                 | Thunk Int 
                 | ThunkSelector
                 | Blackhole 
                 | AP 
                 | PAP 
                 | Indirection Int 
                 | Other Int
 deriving (Show, Eq)

data Closure = Closure { tipe         :: ClosureType 
135
                       , infoPtr      :: Ptr ()
136
137
                       , infoTable    :: StgInfoTable
                       , ptrs         :: Array Int HValue
138
                       , nonPtrs      :: [Word]
139
140
141
142
143
144
145
146
147
148
149
150
151
                       }

instance Outputable ClosureType where
  ppr = text . show 

#include "../includes/ClosureTypes.h"

aP_CODE = AP
pAP_CODE = PAP
#undef AP
#undef PAP

getClosureData :: a -> IO Closure
152
153
154
155
156
157
getClosureData a =
   case unpackClosure# a of 
     (# iptr, ptrs, nptrs #) -> do
           itbl <- peek (Ptr iptr)
           let tipe = readCType (BCI.tipe itbl)
               elems = BCI.ptrs itbl 
158
               ptrsList = Array 0 (fromIntegral$ elems) ptrs
159
160
161
               nptrs_data = [W# (indexWordArray# nptrs i)
                              | I# i <- [0.. fromIntegral (BCI.nptrs itbl)] ]
           ptrsList `seq` return (Closure tipe (Ptr iptr) itbl ptrsList nptrs_data)
162
163
164
165
166
167
168
169
170
171

readCType :: Integral a => a -> ClosureType
readCType i
 | i >= CONSTR && i <= CONSTR_NOCAF_STATIC = Constr
 | i >= FUN    && i <= FUN_STATIC          = Fun
 | i >= THUNK  && i < THUNK_SELECTOR       = Thunk (fromIntegral i)
 | i == THUNK_SELECTOR                     = ThunkSelector
 | i == BLACKHOLE                          = Blackhole
 | i >= IND    && i <= IND_STATIC          = Indirection (fromIntegral i)
 | fromIntegral i == aP_CODE               = AP
172
 | i == AP_STACK                           = AP
173
174
175
176
177
178
179
180
181
182
183
 | fromIntegral i == pAP_CODE              = PAP
 | otherwise                               = Other (fromIntegral i)

isConstr, isIndirection :: ClosureType -> Bool
isConstr Constr = True
isConstr    _   = False

isIndirection (Indirection _) = True
--isIndirection ThunkSelector = True
isIndirection _ = False

184
185
186
187
188
isThunk (Thunk _)     = True
isThunk ThunkSelector = True
isThunk AP            = True
isThunk _             = False

189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
isFullyEvaluated :: a -> IO Bool
isFullyEvaluated a = do 
  closure <- getClosureData a 
  case tipe closure of
    Constr -> do are_subs_evaluated <- amapM isFullyEvaluated (ptrs closure)
                 return$ and are_subs_evaluated
    otherwise -> return False
  where amapM f = sequence . amap' f

amap' f (Array i0 i arr#) = map (\(I# i#) -> case indexArray# arr# i# of
                                   (# e #) -> f e)
                                [0 .. i - i0]

-- TODO: Fix it. Probably the otherwise case is failing, trace/debug it
{-
unsafeDeepSeq :: a -> b -> b
unsafeDeepSeq = unsafeDeepSeq1 2
 where unsafeDeepSeq1 0 a b = seq a $! b
       unsafeDeepSeq1 i a b                -- 1st case avoids infinite loops for non reducible thunks
        | not (isConstr tipe) = seq a $! unsafeDeepSeq1 (i-1) a b     
     -- | unsafePerformIO (isFullyEvaluated a) = b
        | otherwise = case unsafePerformIO (getClosureData a) of
                        closure -> foldl' (flip unsafeDeepSeq) b (ptrs closure)
        where tipe = unsafePerformIO (getClosureType a)
-}
isPointed :: Type -> Bool
isPointed t | Just (t, _) <- splitTyConApp_maybe t = not$ isUnliftedTypeKind (tyConKind t)
isPointed _ = True

218
219
220
221
222
223
224
225
226
227
228
229
extractUnboxed  :: [Type] -> Closure -> [[Word]]
extractUnboxed tt clos = go tt (nonPtrs clos)
   where sizeofType t
           | Just (tycon,_) <- splitTyConApp_maybe t
           = ASSERT (isPrimTyCon tycon) sizeofTyCon tycon
           | otherwise = pprPanic "Expected a TcTyCon" (ppr t)
         go [] _ = []
         go (t:tt) xx 
           | (x, rest) <- splitAt (sizeofType t `div` wORD_SIZE) xx 
           = x : go tt rest

sizeofTyCon = sizeofPrimRep . tyConPrimRep
230
231

-----------------------------------
mnislaih's avatar
mnislaih committed
232
-- * Traversals for Terms
233
234
235
-----------------------------------

data TermFold a = TermFold { fTerm :: Type -> DataCon -> HValue -> [a] -> a
236
                           , fPrim :: Type -> [Word] -> a
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
                           , fSuspension :: ClosureType -> Maybe Type -> HValue -> Maybe Name -> a
                           }

foldTerm :: TermFold a -> Term -> a
foldTerm tf (Term ty dc v tt) = fTerm tf ty dc v (map (foldTerm tf) tt)
foldTerm tf (Prim ty    v   ) = fPrim tf ty v
foldTerm tf (Suspension ct ty v b) = fSuspension tf ct ty v b

idTermFold :: TermFold Term
idTermFold = TermFold {
              fTerm = Term,
              fPrim = Prim,
              fSuspension = Suspension
                      }
idTermFoldM :: Monad m => TermFold (m Term)
idTermFoldM = TermFold {
              fTerm       = \ty dc v tt -> sequence tt >>= return . Term ty dc v,
              fPrim       = (return.). Prim,
              fSuspension = (((return.).).). Suspension
                       }

258
259
260
261
262
263
264
265
266
267
268
269
mapTermType f = foldTerm idTermFold {
          fTerm       = \ty dc hval tt -> Term (f ty) dc hval tt,
          fSuspension = \ct mb_ty hval n ->
                          Suspension ct (fmap f mb_ty) hval n }

termTyVars = foldTerm TermFold {
            fTerm       = \ty _ _ tt   -> 
                          tyVarsOfType ty `plusVarEnv` concatVarEnv tt,
            fSuspension = \_ mb_ty _ _ -> 
                          maybe emptyVarEnv tyVarsOfType mb_ty,
            fPrim       = \ _ _ -> emptyVarEnv }
    where concatVarEnv = foldr plusVarEnv emptyVarEnv
270
271
272
273
274
275
276
----------------------------------
-- Pretty printing of terms
----------------------------------

app_prec::Int
app_prec = 10

277
278
pprTerm :: Int -> Term -> SDoc
pprTerm p Term{dc=dc, subTerms=tt} 
279
{-  | dataConIsInfix dc, (t1:t2:tt') <- tt 
280
281
  = parens (pprTerm1 True t1 <+> ppr dc <+> pprTerm1 True ppr t2) 
    <+> hsep (map (pprTerm1 True) tt) 
282
283
-}
  | null tt   = ppr dc
284
285
  | otherwise = cparen (p >= app_prec) 
                       (ppr dc <+> sep (map (pprTerm app_prec) tt))
286
287
288

  where fixity   = undefined 

289
290
pprTerm _ t = pprTerm1 t

291
pprTerm1 Prim{value=words, ty=ty} = text$ repPrim (tyConAppTyCon ty) words
292
293
294
295
296
297
pprTerm1 t@Term{} = pprTerm 0 t 
pprTerm1 Suspension{bound_to=Nothing} =  char '_' -- <> ppr ct <> char '_'
pprTerm1 Suspension{mb_ty=Just ty, bound_to=Just n}
  | Just _ <- splitFunTy_maybe ty = ptext SLIT("<function>")
  | otherwise = parens$ ppr n <> text "::" <> ppr ty 

298

299
300
cPprTerm :: forall m. Monad m => ((Int->Term->m SDoc)->[Int->Term->m (Maybe SDoc)]) -> Term -> m SDoc
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
304
    first_success <- firstJustM mb_customDocs
    case first_success of
305
      Just doc -> return$ cparen (prec>app_prec+1) doc
306
307
--    | dataConIsInfix dc, (t1:t2:tt') <- tt =
      Nothing  -> do pprSubterms <- mapM (go (app_prec+1)) tt
308
309
310
                     return$ cparen (prec >= app_prec) 
                                    (ppr dc <+> sep pprSubterms)
  go _ t = return$ pprTerm1 t
311
312
  firstJustM (mb:mbs) = mb >>= maybe (firstJustM mbs) (return . Just)
  firstJustM [] = return Nothing
313

314
315
cPprTermBase :: Monad m => (Int->Term-> m SDoc)->[Int->Term->m (Maybe SDoc)]
cPprTermBase pprP =
316
  [ 
317
318
319
320
321
322
323
324
325
    ifTerm isTupleDC            (\_ -> liftM (parens . hcat . punctuate comma) 
                                 . mapM (pprP (-1)) . subTerms)
  , ifTerm (isDC consDataCon)   (\ p Term{subTerms=[h,t]} -> doList p h t)
  , ifTerm (isDC intDataCon)    (coerceShow$ \(a::Int)->a)
  , ifTerm (isDC charDataCon)   (coerceShow$ \(a::Char)->a)
--  , ifTerm (isDC wordDataCon) (coerceShow$ \(a::Word)->a)
  , ifTerm (isDC floatDataCon)  (coerceShow$ \(a::Float)->a)
  , ifTerm (isDC doubleDataCon) (coerceShow$ \(a::Double)->a)
  , 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
329
330
           isIntegerDC Term{dc=dc} = 
              dataConName dc `elem` [ smallIntegerDataConName
                                    , largeIntegerDataConName] 
331
332
333
           isTupleDC Term{dc=dc} = dc `elem` snd (unzip (elems boxedTupleArr))
           isDC a_dc Term{dc=dc} = a_dc == dc
           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
338
339
340
341
342
                   isConsLast = termType(last elems) /= termType h
               print_elems <- mapM (pprP 5) elems
               return$ if isConsLast
                     then cparen (p >= 5) . hsep . punctuate (space<>colon) 
                           $ print_elems
                     else brackets (hcat$ punctuate comma print_elems)
343
344
345
346
347
348
349
350

                where Just a /= Just b = not (a `coreEqType` b)
                      _      /=   _    = True
                      getListTerms Term{subTerms=[h,t]} = h : getListTerms t
                      getListTerms t@Term{subTerms=[]}  = []
                      getListTerms t@Suspension{}       = [t]
                      getListTerms t = pprPanic "getListTerms" (ppr t)

351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
repPrim :: TyCon -> [Word] -> String
repPrim t = rep where 
   rep x
    | t == charPrimTyCon   = show (build x :: Char)
    | t == intPrimTyCon    = show (build x :: Int)
    | t == wordPrimTyCon   = show (build x :: Word)
    | t == floatPrimTyCon  = show (build x :: Float)
    | t == doublePrimTyCon = show (build x :: Double)
    | t == int32PrimTyCon  = show (build x :: Int32)
    | t == word32PrimTyCon = show (build x :: Word32)
    | t == int64PrimTyCon  = show (build x :: Int64)
    | t == word64PrimTyCon = show (build x :: Word64)
    | t == addrPrimTyCon   = show (nullPtr `plusPtr` build x)
    | t == stablePtrPrimTyCon  = "<stablePtr>"
    | t == stableNamePrimTyCon = "<stableName>"
    | t == statePrimTyCon      = "<statethread>"
    | t == realWorldTyCon      = "<realworld>"
    | t == threadIdPrimTyCon   = "<ThreadId>"
    | t == weakPrimTyCon       = "<Weak>"
    | t == arrayPrimTyCon      = "<array>"
    | t == byteArrayPrimTyCon  = "<bytearray>"
    | t == mutableArrayPrimTyCon = "<mutableArray>"
    | t == mutableByteArrayPrimTyCon = "<mutableByteArray>"
    | t == mutVarPrimTyCon= "<mutVar>"
    | t == mVarPrimTyCon  = "<mVar>"
    | t == tVarPrimTyCon  = "<tVar>"
    | otherwise = showSDoc (char '<' <> ppr t <> char '>')
    where build ww = unsafePerformIO $ withArray ww (peek . castPtr) 
mnislaih's avatar
mnislaih committed
379

380
381
382
-----------------------------------
-- Type Reconstruction
-----------------------------------
mnislaih's avatar
mnislaih committed
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
{-
Type Reconstruction is type inference done on heap closures.
The algorithm walks the heap generating a set of equations, which
are solved with syntactic unification.
A type reconstruction equation looks like:

  <datacon reptype>  =  <actual heap contents> 

The full equation set is generated by traversing all the subterms, starting
from a given term.

The only difficult part is that newtypes are only found in the lhs of equations.
Right hand sides are missing them. We can either (a) drop them from the lhs, or 
(b) reconstruct them in the rhs when possible. 

The function congruenceNewtypes takes a shot at (b)
-}
400
401
402
403

-- The Type Reconstruction monad
type TR a = TcM a

404
runTR :: HscEnv -> TR a -> IO a
405
runTR hsc_env c = do 
406
  mb_term <- initTcPrintErrors hsc_env iNTERACTIVE c
407
408
  case mb_term of 
    Nothing -> panic "Can't unify"
409
    Just x -> return x
410
411
412
413

trIO :: IO a -> TR a 
trIO = liftTcM . ioToTcRn

mnislaih's avatar
mnislaih committed
414
liftTcM = id
415
416
417
418

newVar :: Kind -> TR TcTyVar
newVar = liftTcM . newFlexiTyVar

419
420
421
422
423
424
-- | Returns the instantiated type scheme ty', and the substitution sigma 
--   such that sigma(ty') = ty 
instScheme :: Type -> TR (TcType, TvSubst)
instScheme ty | (tvs, rho) <- tcSplitForAllTys ty = liftTcM$ do
   (tvs',theta,ty') <- tcInstType (mapM tcInstTyVar) ty
   return (ty', zipTopTvSubst tvs' (mkTyVarTys tvs))
425

mnislaih's avatar
mnislaih committed
426
427
428
429
430
431
addConstraint :: TcType -> TcType -> TR ()
addConstraint t1 t2  = congruenceNewtypes t1 t2 >>= uncurry unifyType 



-- 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
435
   tv <- liftM mkTyVarTy (newVar argTypeKind)
   case mb_ty of
436
437
     Nothing -> go tv tv hval >>= zonkTerm
     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
446
447
  go tv ty a = do 
    let monomorphic = not(isTyVarTy tv)   -- This is a convention. The ancestor tests for
                                         -- monomorphism and passes a type instead of a tv
448
449
    clos <- trIO $ getClosureData a
    case tipe clos of
450
-- Thunks we may want to force
Simon Marlow's avatar
Simon Marlow committed
451
452
453
-- NB. this won't attempt to force a BLACKHOLE.  Even with :force, we never
-- force blackholes, because it would almost certainly result in deadlock,
-- 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
458
 -- The interesting case
      Constr -> do
459
        m_dc <- trIO$ tcRnRecoverDataCon hsc_env (infoPtr clos)
460
461
462
463
        case m_dc of
          Nothing -> panic "Can't find the DataCon for a term"
          Just dc -> do 
            let extra_args = length(dataConRepArgTys dc) - length(dataConOrigArgTys dc)
464
                subTtypes  = matchSubTypes dc ty
465
                (subTtypesP, subTtypesNP) = partition isPointed subTtypes
466
467
468
469
470
471
472
            subTermTvs <- sequence
                 [ if isMonomorphic t then return t else (mkTyVarTy `fmap` newVar k)
                   | (t,k) <- zip subTtypesP (map typeKind subTtypesP)]
            -- It is vital for newtype reconstruction that the unification step is done
            --     right here, _before_ the subterms are RTTI reconstructed.
            when (not monomorphic) $ do
                  let myType = mkFunTys (reOrderTerms subTermTvs subTtypesNP subTtypes) tv
473
                  instScheme(dataConRepType dc) >>= addConstraint myType . fst
474
475
476
            subTermsP <- sequence $ drop extra_args -- all extra arguments are pointed
                  [ appArr (go tv t) (ptrs clos) i
                   | (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.
mnislaih's avatar
wibbles    
mnislaih committed
482
      otherwise -> 
483
         return (Suspension (tipe clos) (Just tv) a Nothing)
484

485
486
487
488
489
490
  matchSubTypes dc ty
    | Just (_,ty_args) <- splitTyConApp_maybe (repType ty) 
    , null (dataConExTyVars dc)  --TODO Handle the case of extra existential tyvars
    = dataConInstArgTys dc ty_args

    | otherwise = dataConRepArgTys dc
491
492
493
494
495

-- This is used to put together pointed and nonpointed subterms in the 
--  correct order.
  reOrderTerms _ _ [] = []
  reOrderTerms pointed unpointed (ty:tys) 
mnislaih's avatar
mnislaih committed
496
497
498
499
500
501
   | isPointed ty = ASSERT2(not(null pointed)
                           , ptext SLIT("reOrderTerms") $$ (ppr pointed $$ ppr unpointed))
                    head pointed : reOrderTerms (tail pointed) unpointed tys
   | otherwise    = ASSERT2(not(null unpointed)
                           , ptext SLIT("reOrderTerms") $$ (ppr pointed $$ ppr unpointed))
                    head unpointed : reOrderTerms pointed (tail unpointed) tys
502

mnislaih's avatar
mnislaih committed
503

504
505

-- Fast, breadth-first version of obtainTerm that deals only with type reconstruction
mnislaih's avatar
mnislaih committed
506

507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
cvReconstructType :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Type
cvReconstructType hsc_env force mb_ty hval = runTR hsc_env $ do
   tv <- liftM mkTyVarTy (newVar argTypeKind)
   case mb_ty of
     Nothing -> search (isMonomorphic `fmap` zonkTcType tv) (++) [(tv, hval)] >> 
                zonkTcType tv  -- TODO untested!
     Just ty | isMonomorphic ty -> return ty
     Just ty -> do 
              (ty',rev_subst) <- instScheme (sigmaType ty)
              addConstraint tv ty'
              search (isMonomorphic `fmap` zonkTcType tv) (++) [(tv, hval)]
              substTy rev_subst `fmap` zonkTcType tv
    where 
--  search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m ()
  search stop combine []     = return ()
  search stop combine ((t,a):jj) =  (jj `combine`) `fmap` go t a >>= 
                                    unlessM stop . search stop combine

   -- returns unification tasks, since we are going to want a breadth-first search
  go :: Type -> HValue -> TR [(Type, HValue)]
  go tv a = do 
    clos <- trIO $ getClosureData a
    case tipe clos of
      Indirection _ -> go tv $! (ptrs clos ! 0)
      Constr -> do
        m_dc <- trIO$ tcRnRecoverDataCon hsc_env (infoPtr clos)
        case m_dc of
          Nothing -> panic "Can't find the DataCon for a term"
          Just dc -> do 
            let extra_args = length(dataConRepArgTys dc) - length(dataConOrigArgTys dc)
            subTtypes <- mapMif (not . isMonomorphic)
                                (\t -> mkTyVarTy `fmap` newVar (typeKind t))
                                (dataConRepArgTys dc)
            -- It is vital for newtype reconstruction that the unification step is done
            --     right here, _before_ the subterms are RTTI reconstructed.
            let myType = mkFunTys subTtypes tv
            fst `fmap` instScheme(dataConRepType dc) >>= addConstraint myType
            return $map (\(I# i#,t) -> case ptrs clos of 
                                       (Array _ _ ptrs#) -> case indexArray# ptrs# i# of 
                                                              (# e #) -> (t,e))
                        (drop extra_args $ zip [0..] subTtypes)
      otherwise -> return []


mnislaih's avatar
mnislaih committed
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
-- Dealing with newtypes
{-
   A parallel fold over two Type values, 
 compensating for missing newtypes on both sides. 
 This is necessary because newtypes are not present 
 in runtime, but since sometimes there is evidence 
 available we do our best to reconstruct them. 
   Evidence can come from DataCon signatures or 
 from compile-time type inference.
   I am using the words congruence and rewriting 
 because what we are doing here is an approximation 
 of unification modulo a set of equations, which would 
 come from newtype definitions. These should be the 
 equality coercions seen in System Fc. Rewriting 
 is performed, taking those equations as rules, 
 before launching unification.

   It doesn't make sense to rewrite everywhere, 
 or we would end up with all newtypes. So we rewrite 
 only in presence of evidence.
   The lhs comes from the heap structure of ptrs,nptrs. 
   The rhs comes from a DataCon type signature. 
 Rewriting in the rhs is restricted to the result type.

   Note that it is very tricky to make this 'rewriting'
 work with the unification implemented by TcM, where
 substitutions are 'inlined'. The order in which 
 constraints are unified is vital for this (or I am 
 using TcM wrongly).
-}
congruenceNewtypes ::  TcType -> TcType -> TcM (TcType,TcType)
congruenceNewtypes = go True
  where 
   go rewriteRHS lhs rhs  
 -- TyVar lhs inductive case
    | Just tv <- getTyVar_maybe lhs 
    = recoverM (return (lhs,rhs)) $ do  
         Indirect ty_v <- readMetaTyVar tv
         (lhs', rhs') <- go rewriteRHS ty_v rhs
         writeMutVar (metaTvRef tv) (Indirect lhs')
         return (lhs, rhs')
 -- TyVar rhs inductive case
    | Just tv <- getTyVar_maybe rhs 
    = recoverM (return (lhs,rhs)) $ do  
         Indirect ty_v <- readMetaTyVar tv
         (lhs', rhs') <- go rewriteRHS lhs ty_v
         writeMutVar (metaTvRef tv) (Indirect rhs')
         return (lhs', rhs)
-- FunTy inductive case
    | Just (l1,l2) <- splitFunTy_maybe lhs
    , Just (r1,r2) <- splitFunTy_maybe rhs
    = do (l2',r2') <- go True l2 r2
         (l1',r1') <- go False l1 r1
         return (mkFunTy l1' l2', mkFunTy r1' r2')
-- TyconApp Inductive case; this is the interesting bit.
    | Just (tycon_l, args_l) <- splitNewTyConApp_maybe lhs
    , Just (tycon_r, args_r) <- splitNewTyConApp_maybe rhs = do

      let (tycon_l',args_l') = if isNewTyCon tycon_r && not(isNewTyCon tycon_l)
                                then (tycon_r, rewrite tycon_r lhs)
                                else (tycon_l, args_l)
          (tycon_r',args_r') = if rewriteRHS && isNewTyCon tycon_l && not(isNewTyCon tycon_r)
                                then (tycon_l, rewrite tycon_l rhs)
                                else (tycon_r, args_r)
      (args_l'', args_r'') <- unzip `liftM` zipWithM (go rewriteRHS) args_l' args_r'
      return (mkTyConApp tycon_l' args_l'', mkTyConApp tycon_r' args_r'') 

    | otherwise = return (lhs,rhs)

    where rewrite newtyped_tc lame_tipe
           | (tvs, tipe) <- newTyConRep newtyped_tc 
           = case tcUnifyTys (const BindMe) [tipe] [lame_tipe] of
               Just subst -> substTys subst (map mkTyVarTy tvs)
               otherwise  -> panic "congruenceNewtypes: Can't unify a newtype"


------------------------------------------------------------------------------------

629
630
631
632
633
634
635
636
637
isMonomorphic ty | (tvs, ty') <- splitForAllTys ty
                 = null tvs && (isEmptyVarSet . tyVarsOfType) ty'

mapMif :: Monad m => (a -> Bool) -> (a -> m a) -> [a] -> m [a]
mapMif pred f xx = sequence $ mapMif_ pred f xx
mapMif_ pred f []     = []
mapMif_ pred f (x:xx) = (if pred x then f x else return x) : mapMif_ pred f xx

unlessM condM acc = condM >>= \c -> unless c acc
638

mnislaih's avatar
mnislaih committed
639
640
641
642
-- Strict application of f at index i
appArr f (Array _ _ ptrs#) (I# i#) = case indexArray# ptrs# i# of 
                                       (# e #) -> f e

643
644
645
646
647
648
649
650
zonkTerm :: Term -> TcM Term
zonkTerm = foldTerm idTermFoldM {
              fTerm = \ty dc v tt -> sequence tt      >>= \tt ->
                                     zonkTcType ty    >>= \ty' ->
                                     return (Term ty' dc v tt)
             ,fSuspension = \ct ty v b -> fmapMMaybe zonkTcType ty >>= \ty ->
                                          return (Suspension ct ty v b)}  

mnislaih's avatar
mnislaih committed
651
652

-- Is this defined elsewhere?
653
-- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
mnislaih's avatar
mnislaih committed
654
655
sigmaType ty = mkForAllTys (varSetElems$ tyVarsOfType (dropForAlls ty)) ty

656