summaryrefslogtreecommitdiff
path: root/compiler/ghci/RtClosureInspect.hs
blob: be052945aa76aca13e9131e3fb76083d4ad1825c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
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
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
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
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
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
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
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
-----------------------------------------------------------------------------
--
-- GHC Interactive support for inspecting arbitrary closures at runtime
--
-- Pepe Iborra (supported by Google SoC) 2006
--
-----------------------------------------------------------------------------

{-# OPTIONS -fno-warn-tabs #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
--     http://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details

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

     Term(..),
     isTerm, isSuspension, isPrim, isFun, isFunLike, isNewtypeWrap,
     isFullyEvaluated, isFullyEvaluatedTerm,
     termType, mapTermType, termTyVars,
     foldTerm, TermFold(..), foldTermM, TermFoldM(..), idTermFold,
     pprTerm, cPprTerm, cPprTermBase, CustomTermPrinter,

--     unsafeDeepSeq,

     Closure(..), getClosureData, ClosureType(..), isConstr, isIndirection
 ) where

#include "HsVersions.h"

import DebuggerUtils
import ByteCodeItbls    ( StgInfoTable, peekItbl )
import qualified ByteCodeItbls as BCI( StgInfoTable(..) )
import BasicTypes       ( HValue )
import HscTypes

import DataCon
import Type
import qualified Unify as U
import Var
import TcRnMonad
import TcType
import TcMType
import TcHsSyn ( zonkTcTypeToType, mkEmptyZonkEnv )
import TcUnify
import TcEnv

import TyCon
import Name
import VarEnv
import Util
import VarSet
import BasicTypes       ( TupleSort(UnboxedTuple) )
import TysPrim
import PrelNames
import TysWiredIn
import DynFlags
import Outputable as Ppr
import GHC.Arr          ( Array(..) )
import GHC.Exts
import GHC.IO ( IO(..) )

import StaticFlags( opt_PprStyle_Debug )
import Control.Monad
import Data.Maybe
import Data.Array.Base
import Data.Ix
import Data.List
import qualified Data.Sequence as Seq
import Data.Monoid (mappend)
import Data.Sequence (viewl, ViewL(..))
import Foreign.Safe
import System.IO.Unsafe

---------------------------------------------
-- * A representation of semi evaluated Terms
---------------------------------------------

data Term = Term { ty        :: RttiType
                 , dc        :: Either String DataCon
                               -- Carries a text representation if the datacon is
                               -- not exported by the .hi file, which is the case 
                               -- for private constructors in -O0 compiled libraries
                 , val       :: HValue 
                 , subTerms  :: [Term] }

          | Prim { ty        :: RttiType
                 , value     :: [Word] }

          | Suspension { ctype    :: ClosureType
                       , ty       :: RttiType
                       , val      :: HValue
                       , bound_to :: Maybe Name   -- Useful for printing
                       }
          | NewtypeWrap{       -- At runtime there are no newtypes, and hence no
                               -- newtype constructors. A NewtypeWrap is just a
                               -- made-up tag saying "heads up, there used to be
                               -- a newtype constructor here".
                         ty           :: RttiType
                       , dc           :: Either String DataCon
                       , wrapped_term :: Term }
          | RefWrap    {       -- The contents of a reference
                         ty           :: RttiType
                       , wrapped_term :: Term }

isTerm, isSuspension, isPrim, isFun, isFunLike, isNewtypeWrap :: Term -> Bool
isTerm Term{} = True
isTerm   _    = False
isSuspension Suspension{} = True
isSuspension      _       = False
isPrim Prim{} = True
isPrim   _    = False
isNewtypeWrap NewtypeWrap{} = True
isNewtypeWrap _             = False

isFun Suspension{ctype=Fun} = True
isFun _ = False

isFunLike s@Suspension{ty=ty} = isFun s || isFunTy ty
isFunLike _ = False

termType :: Term -> RttiType
termType t = ty t

isFullyEvaluatedTerm :: Term -> Bool
isFullyEvaluatedTerm Term {subTerms=tt} = all isFullyEvaluatedTerm tt
isFullyEvaluatedTerm Prim {}            = True
isFullyEvaluatedTerm NewtypeWrap{wrapped_term=t} = isFullyEvaluatedTerm t
isFullyEvaluatedTerm RefWrap{wrapped_term=t}     = isFullyEvaluatedTerm t
isFullyEvaluatedTerm _                  = False

instance Outputable (Term) where
 ppr t | Just doc <- cPprTerm cPprTermBase t = doc
       | otherwise = panic "Outputable Term instance"

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

data Closure = Closure { tipe         :: ClosureType 
                       , infoPtr      :: Ptr ()
                       , infoTable    :: StgInfoTable
                       , ptrs         :: Array Int HValue
                       , nonPtrs      :: [Word]
                       }

instance Outputable ClosureType where
  ppr = text . show 

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

aP_CODE, pAP_CODE :: Int
aP_CODE = AP
pAP_CODE = PAP
#undef AP
#undef PAP

getClosureData :: DynFlags -> a -> IO Closure
getClosureData dflags a =
   case unpackClosure# a of 
     (# iptr, ptrs, nptrs #) -> do
           let iptr'
                | ghciTablesNextToCode =
                   Ptr iptr
                | otherwise =
                   -- the info pointer we get back from unpackClosure#
                   -- is to the beginning of the standard info table,
                   -- but the Storable instance for info tables takes
                   -- into account the extra entry pointer when
                   -- !ghciTablesNextToCode, so we must adjust here:
                   Ptr iptr `plusPtr` negate (wORD_SIZE dflags)
           itbl <- peekItbl dflags iptr'
           let tipe = readCType (BCI.tipe itbl)
               elems = fromIntegral (BCI.ptrs itbl)
               ptrsList = Array 0 (elems - 1) elems ptrs
               nptrs_data = [W# (indexWordArray# nptrs i)
                              | I# i <- [0.. fromIntegral (BCI.nptrs itbl)-1] ]
           ASSERT(elems >= 0) return ()
           ptrsList `seq` 
            return (Closure tipe (Ptr iptr) itbl ptrsList nptrs_data)

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 i'
 | i == THUNK_SELECTOR                     = ThunkSelector
 | i == BLACKHOLE                          = Blackhole
 | i >= IND    && i <= IND_STATIC          = Indirection i'
 | i' == aP_CODE                           = AP
 | i == AP_STACK                           = AP
 | i' == pAP_CODE                          = PAP
 | i == MUT_VAR_CLEAN || i == MUT_VAR_DIRTY= MutVar i'
 | i == MVAR_CLEAN    || i == MVAR_DIRTY   = MVar i'
 | otherwise                               = Other  i'
  where i' = fromIntegral i
 
isConstr, isIndirection, isThunk :: ClosureType -> Bool
isConstr Constr = True
isConstr    _   = False

isIndirection (Indirection _) = True
isIndirection _ = False

isThunk (Thunk _)     = True
isThunk ThunkSelector = True
isThunk AP            = True
isThunk _             = False

isFullyEvaluated :: DynFlags -> a -> IO Bool
isFullyEvaluated dflags a = do
  closure <- getClosureData dflags a
  case tipe closure of
    Constr -> do are_subs_evaluated <- amapM (isFullyEvaluated dflags) (ptrs closure)
                 return$ and are_subs_evaluated
    _      -> return False
  where amapM f = sequence . amap' f

-- 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)
-}

-----------------------------------
-- * Traversals for Terms
-----------------------------------
type TermProcessor a b = RttiType -> Either String DataCon -> HValue -> [a] -> b

data TermFold a = TermFold { fTerm        :: TermProcessor a a
                           , fPrim        :: RttiType -> [Word] -> a
                           , fSuspension  :: ClosureType -> RttiType -> HValue
                                            -> Maybe Name -> a
                           , fNewtypeWrap :: RttiType -> Either String DataCon
                                            -> a -> a
                           , fRefWrap     :: RttiType -> a -> a
                           }


data TermFoldM m a =
                   TermFoldM {fTermM        :: TermProcessor a (m a)
                            , fPrimM        :: RttiType -> [Word] -> m a
                            , fSuspensionM  :: ClosureType -> RttiType -> HValue
                                             -> Maybe Name -> m a
                            , fNewtypeWrapM :: RttiType -> Either String DataCon
                                            -> a -> m a
                            , fRefWrapM     :: RttiType -> a -> m 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
foldTerm tf (NewtypeWrap ty dc t)  = fNewtypeWrap tf ty dc (foldTerm tf t)
foldTerm tf (RefWrap ty t)         = fRefWrap tf ty (foldTerm tf t)


foldTermM :: Monad m => TermFoldM m a -> Term -> m a
foldTermM tf (Term ty dc v tt) = mapM (foldTermM tf) tt >>= fTermM tf ty dc v
foldTermM tf (Prim ty    v   ) = fPrimM tf ty v
foldTermM tf (Suspension ct ty v b) = fSuspensionM tf ct ty v b
foldTermM tf (NewtypeWrap ty dc t)  = foldTermM tf t >>=  fNewtypeWrapM tf ty dc
foldTermM tf (RefWrap ty t)         = foldTermM tf t >>= fRefWrapM tf ty

idTermFold :: TermFold Term
idTermFold = TermFold {
              fTerm = Term,
              fPrim = Prim,
              fSuspension  = Suspension,
              fNewtypeWrap = NewtypeWrap,
              fRefWrap = RefWrap
                      }

mapTermType :: (RttiType -> Type) -> Term -> Term
mapTermType f = foldTerm idTermFold {
          fTerm       = \ty dc hval tt -> Term (f ty) dc hval tt,
          fSuspension = \ct ty hval n ->
                          Suspension ct (f ty) hval n,
          fNewtypeWrap= \ty dc t -> NewtypeWrap (f ty) dc t,
          fRefWrap    = \ty t -> RefWrap (f ty) t}

mapTermTypeM :: Monad m =>  (RttiType -> m Type) -> Term -> m Term
mapTermTypeM f = foldTermM TermFoldM {
          fTermM       = \ty dc hval tt -> f ty >>= \ty' -> return $ Term ty'  dc hval tt,
          fPrimM       = (return.) . Prim,
          fSuspensionM = \ct ty hval n ->
                          f ty >>= \ty' -> return $ Suspension ct ty' hval n,
          fNewtypeWrapM= \ty dc t -> f ty >>= \ty' -> return $ NewtypeWrap ty' dc t,
          fRefWrapM    = \ty t -> f ty >>= \ty' -> return $ RefWrap ty' t}

termTyVars :: Term -> TyVarSet
termTyVars = foldTerm TermFold {
            fTerm       = \ty _ _ tt   -> 
                          tyVarsOfType ty `plusVarEnv` concatVarEnv tt,
            fSuspension = \_ ty _ _ -> tyVarsOfType ty,
            fPrim       = \ _ _ -> emptyVarEnv,
            fNewtypeWrap= \ty _ t -> tyVarsOfType ty `plusVarEnv` t,
            fRefWrap    = \ty t -> tyVarsOfType ty `plusVarEnv` t}
    where concatVarEnv = foldr plusVarEnv emptyVarEnv

----------------------------------
-- Pretty printing of terms
----------------------------------

type Precedence        = Int
type TermPrinter       = Precedence -> Term ->   SDoc
type TermPrinterM m    = Precedence -> Term -> m SDoc

app_prec,cons_prec, max_prec ::Int
max_prec  = 10
app_prec  = max_prec
cons_prec = 5 -- TODO Extract this info from GHC itself

pprTerm :: TermPrinter -> TermPrinter
pprTerm y p t | Just doc <- pprTermM (\p -> Just . y p) p t = doc
pprTerm _ _ _ = panic "pprTerm"

pprTermM, ppr_termM, pprNewtypeWrap :: Monad m => TermPrinterM m -> TermPrinterM m
pprTermM y p t = pprDeeper `liftM` ppr_termM y p t

ppr_termM y p Term{dc=Left dc_tag, subTerms=tt} = do
  tt_docs <- mapM (y app_prec) tt
  return $ cparen (not (null tt) && p >= app_prec)
                  (text dc_tag <+> pprDeeperList fsep tt_docs)
  
ppr_termM y p Term{dc=Right dc, subTerms=tt} 
{-  | dataConIsInfix dc, (t1:t2:tt') <- tt  --TODO fixity
  = parens (ppr_term1 True t1 <+> ppr dc <+> ppr_term1 True ppr t2) 
    <+> hsep (map (ppr_term1 True) tt) 
-} -- TODO Printing infix constructors properly
  | null sub_terms_to_show
  = return (ppr dc)
  | otherwise 
  = do { tt_docs <- mapM (y app_prec) sub_terms_to_show
       ; return $ cparen (p >= app_prec) $
         sep [ppr dc, nest 2 (pprDeeperList fsep tt_docs)] }
  where
    sub_terms_to_show	-- Don't show the dictionary arguments to 
    			-- constructors unless -dppr-debug is on
      | opt_PprStyle_Debug = tt
      | otherwise = dropList (dataConTheta dc) tt

ppr_termM y p t@NewtypeWrap{} = pprNewtypeWrap y p t
ppr_termM y p RefWrap{wrapped_term=t}  = do
  contents <- y app_prec t
  return$ cparen (p >= app_prec) (text "GHC.Prim.MutVar#" <+> contents)
  -- The constructor name is wired in here ^^^ for the sake of simplicity.
  -- I don't think mutvars are going to change in a near future.
  -- In any case this is solely a presentation matter: MutVar# is
  -- a datatype with no constructors, implemented by the RTS
  -- (hence there is no way to obtain a datacon and print it).
ppr_termM _ _ t = ppr_termM1 t


ppr_termM1 :: Monad m => Term -> m SDoc
ppr_termM1 Prim{value=words, ty=ty} = 
    return $ repPrim (tyConAppTyCon ty) words
ppr_termM1 Suspension{ty=ty, bound_to=Nothing} = 
    return (char '_' <+> ifPprDebug (text "::" <> ppr ty))
ppr_termM1 Suspension{ty=ty, bound_to=Just n}
--  | Just _ <- splitFunTy_maybe ty = return$ ptext (sLit("<function>")
  | otherwise = return$ parens$ ppr n <> text "::" <> ppr ty
ppr_termM1 Term{}        = panic "ppr_termM1 - Term"
ppr_termM1 RefWrap{}     = panic "ppr_termM1 - RefWrap"
ppr_termM1 NewtypeWrap{} = panic "ppr_termM1 - NewtypeWrap"

pprNewtypeWrap y p NewtypeWrap{ty=ty, wrapped_term=t}
  | Just (tc,_) <- tcSplitTyConApp_maybe ty
  , ASSERT(isNewTyCon tc) True
  , Just new_dc <- tyConSingleDataCon_maybe tc = do 
             real_term <- y max_prec t
             return $ cparen (p >= app_prec) (ppr new_dc <+> real_term)
pprNewtypeWrap _ _ _ = panic "pprNewtypeWrap"

-------------------------------------------------------
-- Custom Term Pretty Printers
-------------------------------------------------------

-- We can want to customize the representation of a 
--  term depending on its type. 
-- However, note that custom printers have to work with
--  type representations, instead of directly with types.
-- We cannot use type classes here, unless we employ some 
--  typerep trickery (e.g. Weirich's RepLib tricks),
--  which I didn't. Therefore, this code replicates a lot
--  of what type classes provide for free.

type CustomTermPrinter m = TermPrinterM m
                         -> [Precedence -> Term -> (m (Maybe SDoc))]

-- | Takes a list of custom printers with a explicit recursion knot and a term, 
-- and returns the output of the first successful printer, or the default printer
cPprTerm :: Monad m => CustomTermPrinter m -> Term -> m SDoc
cPprTerm printers_ = go 0 where
  printers = printers_ go
  go prec t = do
    let default_ = Just `liftM` pprTermM go prec t
        mb_customDocs = [pp prec t | pp <- printers] ++ [default_]
    Just doc <- firstJustM mb_customDocs
    return$ cparen (prec>app_prec+1) doc

  firstJustM (mb:mbs) = mb >>= maybe (firstJustM mbs) (return . Just)
  firstJustM [] = return Nothing

-- Default set of custom printers. Note that the recursion knot is explicit
cPprTermBase :: forall m. Monad m => CustomTermPrinter m
cPprTermBase y =
  [ ifTerm (isTupleTy.ty) (\_p -> liftM (parens . hcat . punctuate comma) 
                                      . mapM (y (-1))
                                      . subTerms)
  , ifTerm (\t -> isTyCon listTyCon (ty t) && subTerms t `lengthIs` 2)
           ppr_list
  , ifTerm (isTyCon intTyCon    . ty) ppr_int
  , ifTerm (isTyCon charTyCon   . ty) ppr_char
  , ifTerm (isTyCon floatTyCon  . ty) ppr_float
  , ifTerm (isTyCon doubleTyCon . ty) ppr_double
  , ifTerm (isIntegerTy         . ty) ppr_integer
  ]
 where 
   ifTerm :: (Term -> Bool)
          -> (Precedence -> Term -> m SDoc)
          -> Precedence -> Term -> m (Maybe SDoc)
   ifTerm pred f prec t@Term{}
       | pred t    = Just `liftM` f prec t
   ifTerm _ _ _ _  = return Nothing

   isTupleTy ty    = fromMaybe False $ do 
     (tc,_) <- tcSplitTyConApp_maybe ty 
     return (isBoxedTupleTyCon tc)

   isTyCon a_tc ty = fromMaybe False $ do 
     (tc,_) <- tcSplitTyConApp_maybe ty
     return (a_tc == tc)

   isIntegerTy ty = fromMaybe False $ do
     (tc,_) <- tcSplitTyConApp_maybe ty
     return (tyConName tc == integerTyConName)

   ppr_int, ppr_char, ppr_float, ppr_double, ppr_integer 
      :: Precedence -> Term -> m SDoc
   ppr_int     _ v = return (Ppr.int     (unsafeCoerce# (val v)))
   ppr_char    _ v = return (Ppr.char '\'' <> Ppr.char (unsafeCoerce# (val v)) <> Ppr.char '\'')
   ppr_float   _ v = return (Ppr.float   (unsafeCoerce# (val v)))
   ppr_double  _ v = return (Ppr.double  (unsafeCoerce# (val v)))
   ppr_integer _ v = return (Ppr.integer (unsafeCoerce# (val v)))

   --Note pprinting of list terms is not lazy
   ppr_list :: Precedence -> Term -> m SDoc
   ppr_list p (Term{subTerms=[h,t]}) = do
       let elems      = h : getListTerms t
           isConsLast = not(termType(last elems) `eqType` termType h)
   	   is_string  = all (isCharTy . ty) elems

       print_elems <- mapM (y cons_prec) elems
       if is_string
        then return (Ppr.doubleQuotes (Ppr.text (unsafeCoerce# (map val elems))))
        else if isConsLast
        then return $ cparen (p >= cons_prec) 
                    $ pprDeeperList fsep 
                    $ punctuate (space<>colon) print_elems
        else return $ brackets 
                    $ pprDeeperList fcat
                    $ punctuate comma print_elems

        where getListTerms Term{subTerms=[h,t]} = h : getListTerms t
              getListTerms Term{subTerms=[]}    = []
              getListTerms t@Suspension{}       = [t]
              getListTerms t = pprPanic "getListTerms" (ppr t)
   ppr_list _ _ = panic "doList"


repPrim :: TyCon -> [Word] -> SDoc
repPrim t = rep where
   rep x
    | t == charPrimTyCon             = text $ show (build x :: Char)
    | t == intPrimTyCon              = text $ show (build x :: Int)
    | t == wordPrimTyCon             = text $ show (build x :: Word)
    | t == floatPrimTyCon            = text $ show (build x :: Float)
    | t == doublePrimTyCon           = text $ show (build x :: Double)
    | t == int32PrimTyCon            = text $ show (build x :: Int32)
    | t == word32PrimTyCon           = text $ show (build x :: Word32)
    | t == int64PrimTyCon            = text $ show (build x :: Int64)
    | t == word64PrimTyCon           = text $ show (build x :: Word64)
    | t == addrPrimTyCon             = text $ show (nullPtr `plusPtr` build x)
    | t == stablePtrPrimTyCon        = text "<stablePtr>"
    | t == stableNamePrimTyCon       = text "<stableName>"
    | t == statePrimTyCon            = text "<statethread>"
    | t == proxyPrimTyCon            = text "<proxy>"
    | t == realWorldTyCon            = text "<realworld>"
    | t == threadIdPrimTyCon         = text "<ThreadId>"
    | t == weakPrimTyCon             = text "<Weak>"
    | t == arrayPrimTyCon            = text "<array>"
    | t == byteArrayPrimTyCon        = text "<bytearray>"
    | t == mutableArrayPrimTyCon     = text "<mutableArray>"
    | t == mutableByteArrayPrimTyCon = text "<mutableByteArray>"
    | t == mutVarPrimTyCon           = text "<mutVar>"
    | t == mVarPrimTyCon             = text "<mVar>"
    | t == tVarPrimTyCon             = text "<tVar>"
    | otherwise                      = char '<' <> ppr t <> char '>'
    where build ww = unsafePerformIO $ withArray ww (peek . castPtr) 
--   This ^^^ relies on the representation of Haskell heap values being 
--   the same as in a C array. 

-----------------------------------
-- Type Reconstruction
-----------------------------------
{-
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)
-}


-- A (non-mutable) tau type containing
-- existentially quantified tyvars.
--    (since GHC type language currently does not support
--     existentials, we leave these variables unquantified)
type RttiType = Type

-- An incomplete type as stored in GHCi:
--  no polymorphism: no quantifiers & all tyvars are skolem.
type GhciType = Type


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

runTR :: HscEnv -> TR a -> IO a
runTR hsc_env thing = do
  mb_val <- runTR_maybe hsc_env thing
  case mb_val of
    Nothing -> error "unable to :print the term"
    Just x  -> return x

runTR_maybe :: HscEnv -> TR a -> IO (Maybe a)
runTR_maybe hsc_env = fmap snd . initTc hsc_env HsSrcFile False  iNTERACTIVE

traceTR :: SDoc -> TR ()
traceTR = liftTcM . traceOptTcRn Opt_D_dump_rtti


-- Semantically different to recoverM in TcRnMonad 
-- recoverM retains the errors in the first action,
--  whereas recoverTc here does not
recoverTR :: TR a -> TR a -> TR a
recoverTR recover thing = do 
  (_,mb_res) <- tryTcErrs thing
  case mb_res of 
    Nothing  -> recover
    Just res -> return res

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

liftTcM :: TcM a -> TR a
liftTcM = id

newVar :: Kind -> TR TcType
newVar = liftTcM . newFlexiTyVarTy

instTyVars :: [TyVar] -> TR ([TcTyVar], [TcType], TvSubst)
-- Instantiate fresh mutable type variables from some TyVars
-- This function preserves the print-name, which helps error messages
instTyVars = liftTcM . tcInstTyVars

type RttiInstantiation = [(TcTyVar, TyVar)]
   -- Associates the typechecker-world meta type variables 
   -- (which are mutable and may be refined), to their 
   -- debugger-world RuntimeUnk counterparts.
   -- If the TcTyVar has not been refined by the runtime type
   -- elaboration, then we want to turn it back into the
   -- original RuntimeUnk

-- | Returns the instantiated type scheme ty', and the 
--   mapping from new (instantiated) -to- old (skolem) type variables
instScheme :: QuantifiedType -> TR (TcType, RttiInstantiation)
instScheme (tvs, ty) 
  = liftTcM $ do { (tvs', _, subst) <- tcInstTyVars tvs
                 ; let rtti_inst = [(tv',tv) | (tv',tv) <- tvs' `zip` tvs]
                 ; return (substTy subst ty, rtti_inst) }

applyRevSubst :: RttiInstantiation -> TR ()
-- Apply the *reverse* substitution in-place to any un-filled-in
-- meta tyvars.  This recovers the original debugger-world variable
-- unless it has been refined by new information from the heap
applyRevSubst pairs = liftTcM (mapM_ do_pair pairs)
  where
    do_pair (tc_tv, rtti_tv)
      = do { tc_ty <- zonkTcTyVar tc_tv
           ; case tcGetTyVar_maybe tc_ty of
               Just tv | isMetaTyVar tv -> writeMetaTyVar tv (mkTyVarTy rtti_tv)
               _                        -> return () }

-- Adds a constraint of the form t1 == t2
-- t1 is expected to come from walking the heap
-- t2 is expected to come from a datacon signature
-- Before unification, congruenceNewtypes needs to
-- do its magic.
addConstraint :: TcType -> TcType -> TR ()
addConstraint actual expected = do
    traceTR (text "add constraint:" <+> fsep [ppr actual, equals, ppr expected])
    recoverTR (traceTR $ fsep [text "Failed to unify", ppr actual,
                                    text "with", ppr expected]) $
      do { (ty1, ty2) <- congruenceNewtypes actual expected
         ; _  <- captureConstraints $ unifyType ty1 ty2
         ; return () }
     -- TOMDO: what about the coercion?
     -- we should consider family instances


-- Type & Term reconstruction
------------------------------
cvObtainTerm :: HscEnv -> Int -> Bool -> RttiType -> HValue -> IO Term
cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
  -- we quantify existential tyvars as universal,
  -- as this is needed to be able to manipulate
  -- them properly
   let quant_old_ty@(old_tvs, old_tau) = quantifyType old_ty
       sigma_old_ty = mkForAllTys old_tvs old_tau
   traceTR (text "Term reconstruction started with initial type " <> ppr old_ty)
   term <-
     if null old_tvs
      then do
        term  <- go max_depth sigma_old_ty sigma_old_ty hval
        term' <- zonkTerm term
        return $ fixFunDictionaries $ expandNewtypes term'
      else do
              (old_ty', rev_subst) <- instScheme quant_old_ty
              my_ty <- newVar openTypeKind
              when (check1 quant_old_ty) (traceTR (text "check1 passed") >>
                                          addConstraint my_ty old_ty')
              term  <- go max_depth my_ty sigma_old_ty hval
              new_ty <- zonkTcType (termType term)
              if isMonomorphic new_ty || check2 (quantifyType new_ty) quant_old_ty
                 then do
                      traceTR (text "check2 passed")
                      addConstraint new_ty old_ty'
                      applyRevSubst rev_subst
                      zterm' <- zonkTerm term
                      return ((fixFunDictionaries . expandNewtypes) zterm')
                 else do
                      traceTR (text "check2 failed" <+> parens
                                       (ppr term <+> text "::" <+> ppr new_ty))
                      -- we have unsound types. Replace constructor types in
                      -- subterms with tyvars
                      zterm' <- mapTermTypeM
                                 (\ty -> case tcSplitTyConApp_maybe ty of
                                           Just (tc, _:_) | tc /= funTyCon
                                               -> newVar openTypeKind
                                           _   -> return ty)
                                 term
                      zonkTerm zterm'
   traceTR (text "Term reconstruction completed." $$
            text "Term obtained: " <> ppr term $$
            text "Type obtained: " <> ppr (termType term))
   return term
    where 
  dflags = hsc_dflags hsc_env

  go :: Int -> Type -> Type -> HValue -> TcM Term
   -- [SPJ May 11] I don't understand the difference between my_ty and old_ty

  go max_depth _ _ _ | seq max_depth False = undefined
  go 0 my_ty _old_ty a = do
    traceTR (text "Gave up reconstructing a term after" <>
                  int max_depth <> text " steps")
    clos <- trIO $ getClosureData dflags a
    return (Suspension (tipe clos) my_ty a Nothing)
  go max_depth my_ty old_ty a = do
    let monomorphic = not(isTyVarTy my_ty)   
    -- This ^^^ is a convention. The ancestor tests for
    -- monomorphism and passes a type instead of a tv
    clos <- trIO $ getClosureData dflags a
    case tipe clos of
-- Thunks we may want to force
      t | isThunk t && force -> traceTR (text "Forcing a " <> text (show t)) >>
                                seq a (go (pred max_depth) my_ty old_ty a)
-- Blackholes are indirections iff the payload is not TSO or BLOCKING_QUEUE.  So we
-- treat them like indirections; if the payload is TSO or BLOCKING_QUEUE, we'll end up
-- showing '_' which is what we want.
      Blackhole -> do traceTR (text "Following a BLACKHOLE")
                      appArr (go max_depth my_ty old_ty) (ptrs clos) 0
-- We always follow indirections
      Indirection i -> do traceTR (text "Following an indirection" <> parens (int i) )
                          go max_depth my_ty old_ty $! (ptrs clos ! 0)
-- We also follow references
      MutVar _ | Just (tycon,[world,contents_ty]) <- tcSplitTyConApp_maybe old_ty
             -> do
                  -- Deal with the MutVar# primitive
                  -- It does not have a constructor at all, 
                  -- so we simulate the following one
                  -- MutVar# :: contents_ty -> MutVar# s contents_ty
         traceTR (text "Following a MutVar")
         contents_tv <- newVar liftedTypeKind
         contents <- trIO$ IO$ \w -> readMutVar# (unsafeCoerce# a) w
         ASSERT(isUnliftedTypeKind $ typeKind my_ty) return ()
         (mutvar_ty,_) <- instScheme $ quantifyType $ mkFunTy 
                            contents_ty (mkTyConApp tycon [world,contents_ty])
         addConstraint (mkFunTy contents_tv my_ty) mutvar_ty
         x <- go (pred max_depth) contents_tv contents_ty contents
         return (RefWrap my_ty x)

 -- The interesting case
      Constr -> do
        traceTR (text "entering a constructor " <>
                      if monomorphic
                        then parens (text "already monomorphic: " <> ppr my_ty)
                        else Ppr.empty)
        Right dcname <- dataConInfoPtrToName (infoPtr clos)
        (_,mb_dc)    <- tryTcErrs (tcLookupDataCon dcname)
        case mb_dc of
          Nothing -> do -- This can happen for private constructors compiled -O0
                        -- where the .hi descriptor does not export them
                        -- In such case, we return a best approximation:
                        --  ignore the unpointed args, and recover the pointeds
                        -- This preserves laziness, and should be safe.
		       traceTR (text "Not constructor" <+> ppr dcname)
                       let dflags = hsc_dflags hsc_env
                           tag = showPpr dflags dcname
                       vars     <- replicateM (length$ elems$ ptrs clos) 
                                              (newVar liftedTypeKind)
                       subTerms <- sequence [appArr (go (pred max_depth) tv tv) (ptrs clos) i 
                                              | (i, tv) <- zip [0..] vars]
                       return (Term my_ty (Left ('<' : tag ++ ">")) a subTerms)
          Just dc -> do
            traceTR (text "Is constructor" <+> (ppr dc $$ ppr my_ty))
            subTtypes <- getDataConArgTys dc my_ty
            subTerms <- extractSubTerms (\ty -> go (pred max_depth) ty ty) clos subTtypes
            return (Term my_ty (Right dc) a subTerms)

-- The otherwise case: can be a Thunk,AP,PAP,etc.
      tipe_clos ->
         return (Suspension tipe_clos my_ty a Nothing)

  -- insert NewtypeWraps around newtypes
  expandNewtypes = foldTerm idTermFold { fTerm = worker } where
   worker ty dc hval tt
     | Just (tc, args) <- tcSplitTyConApp_maybe ty
     , isNewTyCon tc
     , wrapped_type    <- newTyConInstRhs tc args
     , Just dc'        <- tyConSingleDataCon_maybe tc
     , t'              <- worker wrapped_type dc hval tt
     = NewtypeWrap ty (Right dc') t'
     | otherwise = Term ty dc hval tt


   -- Avoid returning types where predicates have been expanded to dictionaries.
  fixFunDictionaries = foldTerm idTermFold {fSuspension = worker} where
      worker ct ty hval n | isFunTy ty = Suspension ct (dictsView ty) hval n
                          | otherwise  = Suspension ct ty hval n

extractSubTerms :: (Type -> HValue -> TcM Term)
                -> Closure -> [Type] -> TcM [Term]
extractSubTerms recurse clos = liftM thirdOf3 . go 0 (nonPtrs clos)
  where
    go ptr_i ws [] = return (ptr_i, ws, [])
    go ptr_i ws (ty:tys)
      | Just (tc, elem_tys) <- tcSplitTyConApp_maybe ty
      , isUnboxedTupleTyCon tc
      = do (ptr_i, ws, terms0) <- go ptr_i ws elem_tys
           (ptr_i, ws, terms1) <- go ptr_i ws tys
           return (ptr_i, ws, unboxedTupleTerm ty terms0 : terms1)
      | otherwise
      = case repType ty of
          UnaryRep rep_ty -> do
            (ptr_i, ws, term0)  <- go_rep ptr_i ws ty (typePrimRep rep_ty)
            (ptr_i, ws, terms1) <- go ptr_i ws tys
            return (ptr_i, ws, term0 : terms1)
          UbxTupleRep rep_tys -> do
            (ptr_i, ws, terms0) <- go_unary_types ptr_i ws rep_tys
            (ptr_i, ws, terms1) <- go ptr_i ws tys
            return (ptr_i, ws, unboxedTupleTerm ty terms0 : terms1)

    go_unary_types ptr_i ws [] = return (ptr_i, ws, [])
    go_unary_types ptr_i ws (rep_ty:rep_tys) = do
      tv <- newVar liftedTypeKind
      (ptr_i, ws, term0)  <- go_rep ptr_i ws tv (typePrimRep rep_ty)
      (ptr_i, ws, terms1) <- go_unary_types ptr_i ws rep_tys
      return (ptr_i, ws, term0 : terms1)

    go_rep ptr_i ws ty rep = case rep of
      PtrRep -> do
        t <- appArr (recurse ty) (ptrs clos) ptr_i
        return (ptr_i + 1, ws, t)
      _ -> do
        dflags <- getDynFlags
        let (ws0, ws1) = splitAt (primRepSizeW dflags rep) ws
        return (ptr_i, ws1, Prim ty ws0)

    unboxedTupleTerm ty terms = Term ty (Right (tupleCon UnboxedTuple (length terms)))
                                        (error "unboxedTupleTerm: no HValue for unboxed tuple") terms


-- Fast, breadth-first Type reconstruction
------------------------------------------
cvReconstructType :: HscEnv -> Int -> GhciType -> HValue -> IO (Maybe Type)
cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
   traceTR (text "RTTI started with initial type " <> ppr old_ty)
   let sigma_old_ty@(old_tvs, _) = quantifyType old_ty
   new_ty <-
       if null old_tvs
        then return old_ty
        else do
          (old_ty', rev_subst) <- instScheme sigma_old_ty
          my_ty <- newVar openTypeKind
          when (check1 sigma_old_ty) (traceTR (text "check1 passed") >>
                                      addConstraint my_ty old_ty')
          search (isMonomorphic `fmap` zonkTcType my_ty)
                 (\(ty,a) -> go ty a)
                 (Seq.singleton (my_ty, hval))
                 max_depth
          new_ty <- zonkTcType my_ty
          if isMonomorphic new_ty || check2 (quantifyType new_ty) sigma_old_ty
            then do
                 traceTR (text "check2 passed" <+> ppr old_ty $$ ppr new_ty)
                 addConstraint my_ty old_ty'
                 applyRevSubst rev_subst
                 zonkRttiType new_ty
            else traceTR (text "check2 failed" <+> parens (ppr new_ty)) >>
                 return old_ty
   traceTR (text "RTTI completed. Type obtained:" <+> ppr new_ty)
   return new_ty
    where
  dflags = hsc_dflags hsc_env

--  search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m ()
  search _ _ _ 0 = traceTR (text "Failed to reconstruct a type after " <>
                                int max_depth <> text " steps")
  search stop expand l d =
    case viewl l of 
      EmptyL  -> return ()
      x :< xx -> unlessM stop $ do
                  new <- expand x
                  search stop expand (xx `mappend` Seq.fromList new) $! (pred d)

   -- returns unification tasks,since we are going to want a breadth-first search
  go :: Type -> HValue -> TR [(Type, HValue)]
  go my_ty a = do
    traceTR (text "go" <+> ppr my_ty)
    clos <- trIO $ getClosureData dflags a
    case tipe clos of
      Blackhole -> appArr (go my_ty) (ptrs clos) 0 -- carefully, don't eval the TSO
      Indirection _ -> go my_ty $! (ptrs clos ! 0)
      MutVar _ -> do
         contents <- trIO$ IO$ \w -> readMutVar# (unsafeCoerce# a) w
         tv'   <- newVar liftedTypeKind
         world <- newVar liftedTypeKind
         addConstraint my_ty (mkTyConApp mutVarPrimTyCon [world,tv'])
         return [(tv', contents)]
      Constr -> do
        Right dcname <- dataConInfoPtrToName (infoPtr clos)
        traceTR (text "Constr1" <+> ppr dcname)
        (_,mb_dc)    <- tryTcErrs (tcLookupDataCon dcname)
        case mb_dc of
          Nothing-> do
                     --  TODO: Check this case
            forM [0..length (elems $ ptrs clos)] $ \i -> do
                        tv <- newVar liftedTypeKind
                        return$ appArr (\e->(tv,e)) (ptrs clos) i

          Just dc -> do
            arg_tys <- getDataConArgTys dc my_ty
            (_, itys) <- findPtrTyss 0 arg_tys
            traceTR (text "Constr2" <+> ppr dcname <+> ppr arg_tys)
            return $ [ appArr (\e-> (ty,e)) (ptrs clos) i
                     | (i,ty) <- itys]
      _ -> return []

findPtrTys :: Int  -- Current pointer index
           -> Type -- Type
           -> TR (Int, [(Int, Type)])
findPtrTys i ty
  | Just (tc, elem_tys) <- tcSplitTyConApp_maybe ty
  , isUnboxedTupleTyCon tc
  = findPtrTyss i elem_tys
  
  | otherwise
  = case repType ty of
      UnaryRep rep_ty | typePrimRep rep_ty == PtrRep -> return (i + 1, [(i, ty)])
                      | otherwise                    -> return (i,     [])
      UbxTupleRep rep_tys  -> foldM (\(i, extras) rep_ty -> if typePrimRep rep_ty == PtrRep
                                                             then newVar liftedTypeKind >>= \tv -> return (i + 1, extras ++ [(i, tv)])
                                                             else return (i, extras))
                                    (i, []) rep_tys

findPtrTyss :: Int
            -> [Type]
            -> TR (Int, [(Int, Type)])
findPtrTyss i tys = foldM step (i, []) tys
  where step (i, discovered) elem_ty = findPtrTys i elem_ty >>= \(i, extras) -> return (i, discovered ++ extras)


-- Compute the difference between a base type and the type found by RTTI
-- improveType <base_type> <rtti_type>
-- The types can contain skolem type variables, which need to be treated as normal vars.
-- In particular, we want them to unify with things.
improveRTTIType :: HscEnv -> RttiType -> RttiType -> Maybe TvSubst
improveRTTIType _ base_ty new_ty
  = U.tcUnifyTys (const U.BindMe) [base_ty] [new_ty]

getDataConArgTys :: DataCon -> Type -> TR [Type]
-- Given the result type ty of a constructor application (D a b c :: ty) 
-- return the types of the arguments.  This is RTTI-land, so 'ty' might
-- not be fully known.  Moreover, the arg types might involve existentials;
-- if so, make up fresh RTTI type variables for them
getDataConArgTys dc con_app_ty
  = do { (_, ex_tys, ex_subst) <- instTyVars ex_tvs
       ; let UnaryRep rep_con_app_ty = repType con_app_ty
       ; traceTR (text "getDataConArgTys 1" <+> (ppr con_app_ty $$ ppr rep_con_app_ty))
       ; ty_args <- case tcSplitTyConApp_maybe rep_con_app_ty of
                       Just (tc, ty_args) | dataConTyCon dc == tc
		       	   -> ASSERT( univ_tvs `equalLength` ty_args) 
                              return ty_args
 		       _   -> do { (_, ty_args, univ_subst) <- instTyVars univ_tvs
		       	         ; let res_ty = substTy ex_subst (substTy univ_subst (dataConOrigResTy dc))
                                   -- See Note [Constructor arg types]
                                 ; addConstraint rep_con_app_ty res_ty
                                 ; return ty_args }
		-- It is necessary to check dataConTyCon dc == tc
      		-- because it may be the case that tc is a recursive
      		-- newtype and tcSplitTyConApp has not removed it. In
      		-- that case, we happily give up and don't match
       ; let subst = zipTopTvSubst (univ_tvs ++ ex_tvs) (ty_args ++ ex_tys)
       ; traceTR (text "getDataConArgTys 2" <+> (ppr rep_con_app_ty $$ ppr ty_args $$ ppr subst))
       ; return (substTys subst (dataConRepArgTys dc)) }
  where
    univ_tvs = dataConUnivTyVars dc
    ex_tvs   = dataConExTyVars dc

{- Note [Constructor arg types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider a GADT (cf Trac #7386)
   data family D a b
   data instance D [a] b where
     MkT :: b -> D [a] (Maybe b)

In getDataConArgTys
* con_app_ty is the known type (from outside) of the constructor application, 
  say D [Int] Bool

* The data constructor MkT has a (representation) dataConTyCon = DList,
  say where
    data DList a b where
      MkT :: b -> DList a (Maybe b)

So the dataConTyCon of the data constructor, DList, differs from 
the "outside" type, D. So we can't straightforwardly decompose the
"outside" type, and we end up in the "_" branch of the case.

Then we match the dataConOrigResTy of the data constructor against the
outside type, hoping to get a substitution that tells how to instantiate
the *representation* type constructor.   This looks a bit delicate to
me, but it seems to work.
-}

-- Soundness checks
--------------------
{-
This is not formalized anywhere, so hold to your seats!
RTTI in the presence of newtypes can be a tricky and unsound business.

Example:
~~~~~~~~~
Suppose we are doing RTTI for a partially evaluated
closure t, the real type of which is t :: MkT Int, for

   newtype MkT a = MkT [Maybe a]

The table below shows the results of RTTI and the improvement
calculated for different combinations of evaluatedness and :type t.
Regard the two first columns as input and the next two as output.

  # |     t     |  :type t  | rtti(t)  | improv.    | result
    ------------------------------------------------------------
  1 |     _     |    t b    |    a     | none       | OK
  2 |     _     |   MkT b   |    a     | none       | OK
  3 |     _     |   t Int   |    a     | none       | OK

  If t is not evaluated at *all*, we are safe.

  4 |  (_ : _)  |    t b    |   [a]    | t = []     | UNSOUND
  5 |  (_ : _)  |   MkT b   |  MkT a   | none       | OK (compensating for the missing newtype)
  6 |  (_ : _)  |   t Int   |  [Int]   | t = []     | UNSOUND

  If a is a minimal whnf, we run into trouble. Note that
  row 5 above does newtype enrichment on the ty_rtty parameter.

  7 | (Just _:_)|    t b    |[Maybe a] | t = [],    | UNSOUND
    |                       |          | b = Maybe a|

  8 | (Just _:_)|   MkT b   |  MkT a   |  none      | OK
  9 | (Just _:_)|   t Int   |   FAIL   |  none      | OK

  And if t is any more evaluated than whnf, we are still in trouble.
  Because constraints are solved in top-down order, when we reach the
  Maybe subterm what we got is already unsound. This explains why the
  row 9 fails to complete.

  10 | (Just _:_)|  t Int  | [Maybe a]   |  FAIL    | OK
  11 | (Just 1:_)|  t Int  | [Maybe Int] |  FAIL    | OK

  We can undo the failure in row 9 by leaving out the constraint
  coming from the type signature of t (i.e., the 2nd column).
  Note that this type information is still used
  to calculate the improvement. But we fail
  when trying to calculate the improvement, as there is no unifier for
  t Int = [Maybe a] or t Int = [Maybe Int].


  Another set of examples with t :: [MkT (Maybe Int)]  \equiv  [[Maybe (Maybe Int)]]

  # |     t     |    :type t    |  rtti(t)    | improvement | result
    ---------------------------------------------------------------------
  1 |(Just _:_) | [t (Maybe a)] | [[Maybe b]] | t = []      |
    |           |               |             | b = Maybe a |

The checks:
~~~~~~~~~~~
Consider a function obtainType that takes a value and a type and produces
the Term representation and a substitution (the improvement).
Assume an auxiliar rtti' function which does the actual job if recovering
the type, but which may produce a false type.

In pseudocode:

  rtti' :: a -> IO Type  -- Does not use the static type information

  obtainType :: a -> Type -> IO (Maybe (Term, Improvement))
  obtainType v old_ty = do
       rtti_ty <- rtti' v
       if monomorphic rtti_ty || (check rtti_ty old_ty)
        then ...
         else return Nothing
  where check rtti_ty old_ty = check1 rtti_ty &&
                              check2 rtti_ty old_ty

  check1 :: Type -> Bool
  check2 :: Type -> Type -> Bool

Now, if rtti' returns a monomorphic type, we are safe.
If that is not the case, then we consider two conditions.


1. To prevent the class of unsoundness displayed by
   rows 4 and 7 in the example: no higher kind tyvars
   accepted.

  check1 (t a)   = NO
  check1 (t Int) = NO
  check1 ([] a)  = YES

2. To prevent the class of unsoundness shown by row 6,
   the rtti type should be structurally more
   defined than the old type we are comparing it to.
  check2 :: NewType -> OldType -> Bool
  check2 a  _        = True
  check2 [a] a       = True
  check2 [a] (t Int) = False
  check2 [a] (t a)   = False  -- By check1 we never reach this equation
  check2 [Int] a     = True
  check2 [Int] (t Int) = True
  check2 [Maybe a]   (t Int) = False
  check2 [Maybe Int] (t Int) = True
  check2 (Maybe [a])   (m [Int]) = False
  check2 (Maybe [Int]) (m [Int]) = True

-}

check1 :: QuantifiedType -> Bool
check1 (tvs, _) = not $ any isHigherKind (map tyVarKind tvs)
 where
   isHigherKind = not . null . fst . splitKindFunTys

check2 :: QuantifiedType -> QuantifiedType -> Bool
check2 (_, rtti_ty) (_, old_ty)
  | Just (_, rttis) <- tcSplitTyConApp_maybe rtti_ty
  = case () of
      _ | Just (_,olds) <- tcSplitTyConApp_maybe old_ty
        -> and$ zipWith check2 (map quantifyType rttis) (map quantifyType olds)
      _ | Just _ <- splitAppTy_maybe old_ty
        -> isMonomorphicOnNonPhantomArgs rtti_ty
      _ -> True
  | otherwise = True

-- Dealing with newtypes
--------------------------
{-
 congruenceNewtypes does 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 sometimes there is evidence available.
   Evidence can come from DataCon signatures or
 from compile-time type inference.
 What we are doing here is an approximation
 of unification modulo a set of equations derived
 from newtype definitions. These equations should be the
 same as the equality coercions generated for newtypes
 in System Fc. The idea is to perform a sort of rewriting,
 taking those equations as rules, before launching unification.

 The caller must ensure the following.
 The 1st type (lhs) comes from the heap structure of ptrs,nptrs.
 The 2nd type (rhs) comes from a DataCon type signature.
 Rewriting (i.e. adding/removing a newtype wrapper) can happen
 in both types, but in the rhs it 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 operationally inlined. The order in which
 constraints are unified is vital as we cannot modify
 anything that has been touched by a previous unification step.
Therefore, congruenceNewtypes is sound only if the types
recovered by the RTTI mechanism are unified Top-Down.
-}
congruenceNewtypes ::  TcType -> TcType -> TR (TcType,TcType)
congruenceNewtypes lhs rhs = go lhs rhs >>= \rhs' -> return (lhs,rhs')
 where
   go l r
 -- TyVar lhs inductive case
    | Just tv <- getTyVar_maybe l
    , isTcTyVar tv
    , isMetaTyVar tv
    = recoverTR (return r) $ do
         Indirect ty_v <- readMetaTyVar tv
         traceTR $ fsep [text "(congruence) Following indirect tyvar:",
                          ppr tv, equals, ppr ty_v]
         go ty_v r
-- FunTy inductive case
    | Just (l1,l2) <- splitFunTy_maybe l
    , Just (r1,r2) <- splitFunTy_maybe r
    = do r2' <- go l2 r2
         r1' <- go l1 r1
         return (mkFunTy r1' r2')
-- TyconApp Inductive case; this is the interesting bit.
    | Just (tycon_l, _) <- tcSplitTyConApp_maybe lhs
    , Just (tycon_r, _) <- tcSplitTyConApp_maybe rhs 
    , tycon_l /= tycon_r 
    = upgrade tycon_l r

    | otherwise = return r

    where upgrade :: TyCon -> Type -> TR Type
          upgrade new_tycon ty
            | not (isNewTyCon new_tycon) = do
              traceTR (text "(Upgrade) Not matching newtype evidence: " <>
                       ppr new_tycon <> text " for " <> ppr ty)
              return ty 
            | otherwise = do
               traceTR (text "(Upgrade) upgraded " <> ppr ty <>
                        text " in presence of newtype evidence " <> ppr new_tycon)
               (_, vars, _) <- instTyVars (tyConTyVars new_tycon)
               let ty' = mkTyConApp new_tycon vars
                   UnaryRep rep_ty = repType ty'
               _ <- liftTcM (unifyType ty rep_ty)
        -- assumes that reptype doesn't ^^^^ touch tyconApp args 
               return ty'


zonkTerm :: Term -> TcM Term
zonkTerm = foldTermM (TermFoldM
             { fTermM = \ty dc v tt -> zonkRttiType ty    >>= \ty' ->
                                       return (Term ty' dc v tt)
             , fSuspensionM  = \ct ty v b -> zonkRttiType ty >>= \ty ->
                                             return (Suspension ct ty v b)
             , fNewtypeWrapM = \ty dc t -> zonkRttiType ty >>= \ty' ->
                                           return$ NewtypeWrap ty' dc t
             , fRefWrapM     = \ty t -> return RefWrap  `ap` 
                                        zonkRttiType ty `ap` return t
             , fPrimM        = (return.) . Prim })

zonkRttiType :: TcType -> TcM Type
-- Zonk the type, replacing any unbound Meta tyvars
-- by skolems, safely out of Meta-tyvar-land
zonkRttiType = zonkTcTypeToType (mkEmptyZonkEnv zonk_unbound_meta)
  where
    zonk_unbound_meta tv 
      = ASSERT( isTcTyVar tv )
        do { tv' <- skolemiseUnboundMetaTyVar tv RuntimeUnk
	     -- This is where RuntimeUnks are born: 
	     -- otherwise-unconstrained unification variables are
	     -- turned into RuntimeUnks as they leave the
	     -- typechecker's monad
           ; return (mkTyVarTy tv') }

--------------------------------------------------------------------------------
-- Restore Class predicates out of a representation type
dictsView :: Type -> Type
dictsView ty = ty


-- Use only for RTTI types
isMonomorphic :: RttiType -> Bool
isMonomorphic ty = noExistentials && noUniversals
 where (tvs, _, ty')  = tcSplitSigmaTy ty
       noExistentials = isEmptyVarSet (tyVarsOfType ty')
       noUniversals   = null tvs

-- Use only for RTTI types
isMonomorphicOnNonPhantomArgs :: RttiType -> Bool
isMonomorphicOnNonPhantomArgs ty
  | UnaryRep rep_ty <- repType ty
  , Just (tc, all_args) <- tcSplitTyConApp_maybe rep_ty
  , phantom_vars  <- tyConPhantomTyVars tc
  , concrete_args <- [ arg | (tyv,arg) <- tyConTyVars tc `zip` all_args
                           , tyv `notElem` phantom_vars]
  = all isMonomorphicOnNonPhantomArgs concrete_args
  | Just (ty1, ty2) <- splitFunTy_maybe ty
  = all isMonomorphicOnNonPhantomArgs [ty1,ty2]
  | otherwise = isMonomorphic ty

tyConPhantomTyVars :: TyCon -> [TyVar]
tyConPhantomTyVars tc
  | isAlgTyCon tc
  , Just dcs <- tyConDataCons_maybe tc
  , dc_vars  <- concatMap dataConUnivTyVars dcs
  = tyConTyVars tc \\ dc_vars
tyConPhantomTyVars _ = []

type QuantifiedType = ([TyVar], Type)   -- Make the free type variables explicit

quantifyType :: Type -> QuantifiedType
-- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
quantifyType ty = (varSetElems (tyVarsOfType ty), ty)

unlessM :: Monad m => m Bool -> m () -> m ()
unlessM condM acc = condM >>= \c -> unless c acc


-- Strict application of f at index i
appArr :: Ix i => (e -> a) -> Array i e -> Int -> a
appArr f a@(Array _ _ _ ptrs#) i@(I# i#)
 = ASSERT2(i < length(elems a), ppr(length$ elems a, i))
   case indexArray# ptrs# i# of
       (# e #) -> f e

amap' :: (t -> b) -> Array Int t -> [b]
amap' f (Array i0 i _ arr#) = map g [0 .. i - i0]
    where g (I# i#) = case indexArray# arr# i# of
                          (# e #) -> f e