iface_sums

6 Type
6 TyCon
6 CallStack
8 Addr#
8 TrName
11 b1
15 'Lifted
29 Int
48 'Many
76 AgdaError
total (47, 281)
--
4 String
5 Addr#
5 Char
5 TrName
5 KindRep
6 b
6 CutOff -> CutOff -> Bool
8 Int
44 'Many
45 CutOff
total (37, 172)
--
4 TyCon
5 Semiring a
6 Addr#
6 TrName
7 Int
7 Integer
9 a
9 'Many
11 Type
15 KindRep
total (27, 104)
--
6 Addr#
6 TrName
9 AffineHole r b
10 AffineHole r a
11 KindRep
18 a
22 b
35 'Many
38 r
55 Type
total (63, 285)
--
6 f b
7 b
7 t
8 Alternative f
10 f a
16 Type -> Type
18 a
20 f
22 Type
36 'Many
total (57, 222)
--
14 Boolean b
19 KindRep
21 a -> b
23 IsBool a
31 Bool
31 Boolean a
37 b
76 Type
87 a
123 'Many
total (70, 577)
--
18 C
23 U1 @Type
24 Int
25 Bool
31 x
34 'Lifted
63 Type
69 IsFibrant
136 'Many
136 Univ
total (134, 868)
--
5 Char
5 Word
5 HasCallStack
6 "callStack"
7 String
7 [Char]
7 CallSite
13 Type
26 'Many
28 CallStack
total (42, 168)
--
1 Integer -> Integer
1 Bool
1 Module
1 GeneralCategory
2 Addr#
2 TrName
3 Int
8 'Many
11 Char
12 Integer
total (14, 46)
--
6 EnvVars
6 (String, String)
9 KindRep
12 [Char]
18 [Token]
20 LiftedRep
27 Char
32 Token
36 String
46 'Many
total (53, 292)
--
9 String
10 Either String
10 Fail a
12 [Char]
12 Either String a
15 KindRep
22 b
44 a
48 'Many
85 Type
total (72, 364)
--
12 Bool
13 (Bool, a)
14 LiftedRep
16 m
17 i
18 a -> a
31 b
48 Type
60 a
96 'Many
total (93, 495)
--
8 LiftedRep
8 TyCon
10 Addr#
10 Bool
10 Int
10 TrName
24 Type
27 a
30 'Many
34 KindRep
total (46, 250)
--
15 d
21 Decoration t
22 Functor m
25 b
28 m
30 t
37 a
52 Type -> Type
68 Type
100 'Many
total (153, 632)
--
6 Eq k
6 Hashable k
9 IO
9 Set k
10 HashTable k v
18 MVector
22 v
25 Type
28 'Many
33 k
total (57, 222)
--
33 ModuleName
46 LiftedRep
46 ()
74 Bool
87 TyCon
89 Addr#
89 TrName
99 'One
138 'Many
207 KindRep
total (147, 1491)
--
8 Stmt
8 Match
8 GuardedRhs
9 MakeStrict a
10 Pat
10 Binds
10 Decl
12 a
12 Type
39 'Many
total (70, 237)
--
5 WriterT w m a
6 w
7 IOException
8 s
9 CatchIO m
12 Type -> Type
13 a
17 m
19 Type
34 'Many
total (58, 204)
--
1 Module
1 ()
2 Addr#
2 TrName
2 FilePath
2 Handle
3 IO
3 ByteString
4 'Many
4 (ByteString, IO ())
total (13, 27)
--
9 WriterT (Endo [CopyDirAction]) IO
9 CopyDirAction
10 KindRep
11 [CopyDirAction]
12 LiftedRep
14 ()
16 IO
16 Endo [CopyDirAction]
19 FilePath
21 'Many
total (38, 202)
--
2 String
2 LiftedRep
2 TrName
3 IO FilePath
3 Handle
4 IO
4 ()
4 (FilePath, Handle)
5 'Many
10 FilePath
total (15, 45)
--
8 Char
8 ByteString
9 KindRep
11 String
11 Type
11 LiftedRep
11 FilePath
16 Text
26 ReadException
38 'Many
total (61, 251)
--
1 Module
2 a -> a
2 Addr#
2 Type
2 TrName
2 IORef a
2 ()
3 IO
6 'Many
12 a
total (16, 40)
--
15 String
16 CatchImpossible m
17 Type -> Type
17 KindRep
19 CallStack
20 m a
26 a
50 Type
75 Impossible
102 'Many
total (113, 594)
--
3 Int
3 Type
3 TrName
4 ShowS
5 IO
6 Empty -> Empty -> Bool
7 Maybe Impossible
8 Impossible
41 'Many
47 Empty
total (40, 165)
--
8 b1
8 BoolSet -> BoolSet -> Bool
8 CallStack
9 BoolSet -> BoolSet -> BoolSet
11 LiftedRep
22 Int
30 'Lifted
41 Bool
88 'Many
134 BoolSet
total (57, 465)
--
19 Bool
30 m
40 Ord a
50 Map a [a]
51 [a]
89 b
111 Bag a
134 Type
256 a
296 'Many
total (243, 1573)
--
10 [Integer]
11 KindRep
13 (Maybe Integer, Maybe Integer, Set Integer)
18 Set Integer
23 String
27 LiftedRep
43 b
92 IntSet
99 'Many
116 Integer
total (72, 596)
--
12 MonadState o m
13 a
20 r
24 Lens' o i
27 Type -> Type
58 m
58 o
66 i
94 Type
128 'Many
total (171, 798)
--
18 x -> Type
19 xs
20 p
24 [x]
30 x1
31 [KindRep]
44 Type
52 'Many
72 x
74 KindRep
total (131, 679)
--
4 Functor f
4 Addr#
4 TrName
6 f
9 a
9 b
9 KindRep
10 Record a b
20 'Many
23 Type
total (37, 134)
--
4 Bool
4 Maybe v
6 (,) a
7 Map k v
8 a
11 k
14 f
14 v
26 Type
30 'Many
total (57, 195)
--
13 m b
16 m (Maybe a)
16 Monad m
18 Type -> Type
23 b
26 Maybe a
28 m
55 a
58 Type
113 'Many
total (133, 559)
--
6 HashMap a b
9 s
10 Maybe a
12 IO
13 a -> b
18 Type
24 b
25 m
37 a
39 'Many
total (53, 280)
--
5 KindRep
6 Int -> Int -> Bool
6 Int -> Int -> Int
7 Bool
8 Int -> Int
11 String
39 MaxNat
43 b
45 Int
87 'Many
total (60, 338)
--
24 Null (m a)
28 b
31 m
32 Bool
36 Type -> Type
36 Monad m
53 Null a
119 a
200 Type
239 'Many
total (346, 1374)
--
12 Type -> Type
12 Monad m
12 Maybe b
13 m
13 m b
29 b
29 Maybe a
42 a
60 Type
101 'Many
total (122, 500)
--
19 PartialOrd a
20 Inclusion a
22 Ordering
24 String
32 Int
55 b
102 a
126 PartialOrdering
130 Type
259 'Many
total (230, 1296)
--
3 PartialOrd a
4 LeftClosedPOMonoid a
5 POMonoid a
6 TyCon
8 Addr#
8 TrName
12 Type
13 'Many
15 KindRep
20 a
total (21, 111)
--
12 KindRep
13 Char
15 LiftedRep
24 Integer
31 m
44 b
110 Ptr a
127 Type
177 a
223 'Many
total (219, 1184)
--
6 Addr#
6 TrName
8 StarSemiRing a
13 Maybe a
13 SemiRing a
14 ()
16 KindRep
21 Type
28 a
35 'Many
total (35, 196)
--
16 Applicative m
16 Semigroup doc
19 ReaderT s m doc
19 StateT s m doc
26 s
40 Type
45 m
73 doc
75 'Many
81 b
total (96, 585)
--
11 String
12 KindRep
15 LiftedRep
43 b
48 SmallSetElement a
63 Word64
72 SmallSet a
89 Type
128 a
149 'Many
total (119, 808)
--
12 (k, a)
16 [a] -> [a]
18 k
23 el
29 [a]
29 KindRep
33 coll
77 'Many
149 a
151 Type
total (176, 859)
--
10 Fail
10 (a, NonEmpty c)
11 EquivT s c c Fail
14 a
16 NonEmpty a
18 NonEmpty (NonEmpty a)
22 Type
27 LiftedRep
31 'Many
44 c
total (67, 321)
--
4 CallStack
5 KindRep
6 Addr#
6 TrName
8 String
23 Suffix
24 LiftedRep
25 'Many
26 Integer
39 Char
total (27, 200)
--
15 KindRep
27 Int
31 'Lifted
38 b
38 c
39 Either3 a b c
45 a
101 Three
120 Type
187 'Many
total (180, 1032)
--
25 Maybe v
30 Ord k
35 b
35 Trie k a
77 Trie k v
92 a
97 v
133 k
227 Type
285 'Many
total (292, 1607)
--
12 Pair b
14 Type -> Type
16 d
23 c
36 m
50 Pair a
68 b
109 a
180 Type
223 'Many
total (267, 1153)
[ 50 of 427] Compiling Agda.Utils.List1[boot] ( src/full/Agda/Utils/List1.hs-boot, interpreted )
1 Type -> Type
1 NonEmpty
1 Module
1 'Many
2 Type
total (5, 6)
--
20 Eq a
23 [b]
24 Bool
48 LiftedRep
49 b
89 Int
185 Type
233 [a]
274 a
383 'Many
total (382, 2152)
--
12 Bool
20 LiftedRep
26 m
26 NonEmpty a
46 [a]
47 List1 a
48 b
105 Type
114 a
171 'Many
total (222, 997)
--
8 String -> String
8 Monad m
8 IsString (m a)
10 Type -> Type
12 a
17 [Char]
25 String
26 Type
39 'Many
44 Char
total (63, 290)
--
10 Peano -> Peano
10 Sized a
12 k
14 SizedThing a
17 Int
19 KindRep
39 Peano
72 'Many
76 a
102 Type
total (131, 586)
--
34 m
35 KindRep
48 [Int]
52 LiftedRep
82 Drop a
86 Permutation
129 a
201 Type
207 Int
380 'Many
total (386, 2231)
--
31 'Lifted
34 [Char]
36 C
38 ProfileOptions
42 String
45 U1 @Type
67 x
114 Type
134 'Many
169 ProfileOption
total (169, 1301)
--
12 Int
16 Ord a
17 String
22 [a]
26 m
43 b
105 List2 a
138 Type
170 a
241 'Many
total (230, 1211)
--
6 Word64
6 CallStack
7 Maybe Word64
7 (Integer, Integer)
9 LiftedRep
18 Int
19 Double -> Double
47 'Many
53 Integer
117 Double
total (51, 369)
--
10 (Either (List1 a) (List1 b), [Either a b])
11 c1
11 [Either a b]
12 d
13 m
17 Either a b
48 b
60 a
84 Type
92 'Many
total (158, 614)
--
35 m Bool
36 e
38 [a]
41 b
54 Monad m
74 a
92 Type -> Type
103 Type
134 m
261 'Many
total (294, 1495)
--
53 Applicative m
65 LiftedRep
74 Monad m
78 b
100 ListT m a
117 Type -> Type
138 a
148 Type
211 m
378 'Many
total (370, 2198)
--
6 Text -> Text -> Bool
8 Int
8 LiftedRep
14 String
15 IO
22 Bool
31 Text
34 FilePath
41 AbsolutePath
72 'Many
total (58, 327)
--
2 AbsolutePath
3 Word8
4 String
4 Word64
4 LiftedRep
4 ByteString
4 Text
9 'Many
9 Hash
10 Hash
total (28, 74)
--
35 Map k v
41 HasTag v
47 Ord k
51 Maybe v
54 Tag v
107 BiMap k v
169 k
202 v
257 Type
392 'Many
total (404, 2259)
--
16 Int
17 x
18 KindRep
24 Word64
34 String
47 range
53 ModuleNameHash
63 TopLevelModuleName' range
101 Type
107 'Many
total (159, 763)
--
120 D
122 Addr#
122 TrName
144 'Many
331 WarningName
351 Zero
462 C
570 U1 @Type
1254 x
1755 Type
total (873, 9775)
--
9 Any @Type
11 U1 @Type
12 String
12 Zero
14 C
17 x
30 Help
40 HelpTopic
48 'Many
50 Type
total (105, 452)
--
16 CompareResult a
18 LiftedRep
19 []
20 PartialOrd a
32 [a]
61 b
69 Favorites a
142 a
153 Type
194 'Many
total (175, 1058)
--
8 f
8 LiftedRep
8 AssocList k v
9 m
9 [(k, v)]
21 (k, v)
26 v
29 k
47 Type
69 'Many
total (100, 377)
--
26 Proxy @{Type} b
35 [Type]
42 as
43 l
46 KindRep
49 a
65 k
68 b
139 'Many
225 Type
total (215, 1264)
[ 71 of 427] Compiling Agda.Syntax.Position[boot] ( src/full/Agda/Syntax/Position.hs-boot, interpreted )
1 Type
1 TyCon
1 Module
total (3, 3)
--
74 m
93 String
93 Range
101 Interval' a
135 Range' a
151 Position' a
199 b
534 a
939 Type
1200 'Many
total (1311, 7290)
--
53 NameKind
62 KindRep
81 b
110 OtherAspect
116 String
120 C
144 U1 @Type
251 'Many
358 x
612 Type
total (562, 3949)
--
21 String
22 KindRep
32 LiftedRep
75 Int
86 Pretty a
98 a
121 Aspects
134 Type
262 Doc
278 'Many
total (352, 1954)
--
6 Type
7 Bool
8 LiftedRep
9 Integer -> Integer -> Integer
9 Integer -> Integer
9 Int
13 m
39 CPUTime
64 Integer
97 'Many
total (76, 386)
--
53 Docs k
63 b
67 LiftedRep
90 KindRep
115 a
211 tok1
226 r
246 k
373 'Many
578 Type
total (543, 3493)
--
80 Map n e
102 Edge n e
109 Int
116 LiftedRep
122 Ord n
146 Graph n e
338 e
523 Type
525 n
863 'Many
total (814, 5246)
--
5 [a]
6 Map n (Maybe ())
8 LiftedRep
8 (n, Map n (Maybe ()))
9 a
9 [n]
15 [(n, Map n (Maybe ()))]
16 Maybe ()
28 n
30 'Many
total (44, 192)
--
3 Type
4 Int
4 [Char]
4 DotGraph
7 WithUniqueInt Text
7 ()
8 [Text]
10 LiftedRep
16 'Many
36 Text
total (37, 141)
--
3 SrcLoc -> Doc
3 CallSite -> Doc
5 CallSite
6 []
6 CallStack
8 Int
8 SrcLoc
10 Aspects
12 'Many
37 Doc
total (31, 126)
[ 81 of 427] Compiling Agda.Utils.CallStack ( src/full/Agda/Utils/CallStack.hs, interpreted )
1 Module
2 Addr#
2 TrName
total (3, 5)
--
37 x
49 CPUTime
56 a
56 r
86 LiftedRep
97 MonadBench m
104 Type -> Type
259 Type
273 m
313 'Many
total (524, 2871)
--
55 Size i
57 String
71 MIx i
73 Ord i
87 Matrix i b
135 a
136 b
300 i
423 Type
663 'Many
total (607, 3500)
--
15 String
18 Type
19 IP "cutoff" CutOff
22 KindRep
29 LiftedRep
29 Matrix Int Order
34 Bool
82 Int
121 Order
139 'Many
total (125, 797)
--
35 Matrix ArgumentIndex a
38 CMSet cinfo
42 String
44 KindRep
55 Int
79 CallMatrixAug cinfo
92 cinfo
134 a
283 Type
348 'Many
total (348, 1998)
--
26 KindRep
27 Graph Node (CMSet cinfo)
29 LiftedRep
32 Node
34 CMSet cinfo
56 b
84 CallGraph cinfo
96 cinfo
105 Type
165 'Many
total (213, 1105)
--
7 Node
8 IP "cutoff" CutOff
8 Either cinfo ()
9 [Call cinfo]
12 Type
14 [CallMatrixAug cinfo]
14 CallMatrixAug cinfo
20 LiftedRep
24 cinfo
31 'Many
total (47, 214)
--
12 Bool
13 SpecialCharacters
15 'Lifted
18 KindRep
22 Int
23 Aspects
32 Type
52 Doc
96 'Many
109 UnicodeOrAscii
total (108, 658)
--
7 Ord (Maybe RangeFile)
7 Ord (Range' (Maybe RangeFile))
8 Bool
11 String
12 KindRep
12 RangeFile
16 Maybe RangeFile
31 Range
40 KwRange
54 'Many
total (59, 289)
--
8 Pretty a
9 Char
9 Doc
12 KindRep
16 Lisp String
19 String
19 Type
21 Lisp a
22 a
37 'Many
total (56, 283)
--
349 'Lifted
406 LiftedRep
412 x
484 KindRep
493 Int
610 String
1139 a
1219 b
3557 Type
5922 'Many
total (5271, 36594)
--
24 [(LayerRole, String)]
26 Layer
27 [Char]
32 LayerRole
34 Regex
38 LiftedRep
44 (LayerRole, String)
45 Char
97 String
118 'Many
total (113, 836)
--
44 Zero
45 U1 @Type
45 Precedence
48 ThingWithFixity a
51 C
63 a
71 ParenPreference
110 x
234 'Many
269 Type
total (352, 2018)
--
15 U1 @Type
19 PrecedenceKey
20 MaybePlaceholder tok
21 tok
21 C
32 Zero
35 'Many
45 x
48 MemoKey
113 Type
total (155, 772)
--
48 NameParts
54 LiftedRep
54 KindRep
78 Type
82 NameInScope
84 String
105 NamePart
107 QName
156 Name
346 'Many
total (305, 2045)
--
39 TrName
40 GlobalId
42 Int
53 Comment
54 Exp
64 MemberId
106 KindRep
120 Type
221 String
329 'Many
total (308, 2108)
--
3 LocalId
3 ([MemberId], Exp)
5 Nat -> LocalId -> Exp
6 Exp -> Exp
9 [Exp]
9 (Comment, Exp)
14 MemberId
34 Nat
64 'Many
64 Exp
total (34, 247)
--
36 String
41 Int
41 KindRep
43 a
49 b
51 LiftedRep
55 Char
81 Type
221 'Many
256 Doc
total (247, 1594)
--
325 TyCon
327 Addr#
327 TrName
327 D
380 BuiltinId
965 Zero
1282 C
1590 U1 @Type
3652 x
4966 Type
total (2118, 25088)
--
72 Name
75 KindRep
90 a
91 LiftedRep
113 ModuleName
128 String
153 Type
162 QName
207 Name
546 'Many
total (531, 3383)
--
43 Int
46 String
51 Zero
59 C
60 OccursWhere
76 Where
124 x
169 Occurrence
188 'Many
236 Type
total (308, 2309)
--
  'MetaSel
    ('Nothing @Symbol)
    'NoSourceUnpackedness
    'NoSourceStrictness
    'DecidedLazy
15 RecordFieldWarning
20 String
26 x
28 KindRep
55 Type
total (85, 366)
--
11 Int
15 LiftedRep
16 Char
16 'One
16 Doc
17 QName
36 KindRep
45 String
56 'Many
64 Literal
total (85, 500)
--
96 R
123 S
175 U1 @Type
207 String
209 Zero
215 TTerm
231 C
451 'Many
507 x
914 Type
total (837, 6836)
--
2 Addr#
2 TrName
2 ([TAlt], [TAlt])
3 TTerm -> TTerm
3 []
4 CallStack
5 [TAlt]
9 TTerm
10 'Many
14 TAlt
total (17, 62)
--
10 TAlt
13 KindRep
17 String
20 LiftedRep
26 AsPat
27 [AsPat]
33 Int
38 ReaderT [AsPat] Identity
64 'Many
70 TTerm
total (75, 457)
--
22 Token
23 Interval
23 Symbol
37 Keyword
38 KindRep
47 'Many
50 String
113 TyCon
115 Addr#
115 TrName
total (74, 790)
--
412 KillRange
448 Bool
608 [Type]
623 KindRep
628 a
705 Expr
762 '[] @Type
1013 LiftedRep
1853 Type
2123 'Many
total (2752, 23277)
--
12 LiftedRep
18 KindRep
18 Range
23 TopLevelModuleName
26 Text
29 String
30 TopLevelModuleNameParts
34 Type
94 'Many
97 RawTopLevelModuleName
total (159, 707)
--
136 []
156 Doc Aspects
171 a
250 LiftedRep
265 Type
272 Int
370 Aspects
788 'Many
885 Doc
1813 String
total (1001, 8348)
--
34 Zero
47 KindRep
53 String
56 a
59 x
60 SplitTree' a
67 LazySplit
84 SplitTag
180 'Many
234 Type
total (344, 1972)
--
46 NotationKind
47 Zero
52 KindRep
57 Int
64 LiftedRep
80 NewNotation
83 x
99 String
188 Type
207 'Many
total (385, 2417)
--
13 Int
25 Arg a
27 m
29 String
31 KindRep
49 b
71 Elim' a
130 a
132 Type
206 'Many
total (247, 1207)
--
64 LiftedRep
68 String
94 Blocked' t a
103 x
127 b
135 a
164 t
193 Blocker
428 'Many
553 Type
total (643, 3937)
--
279 b
279 '[] @Type
381 KindRep
385 x
390 Term
553 LiftedRep
726 String
858 a
2487 'Many
2671 Type
total (3360, 23910)
--
6 PlusLevel
9 Maybe Int
10 Term
17 String
17 DeBruijn a
18 Type
19 Int
21 a
22 KindRep
54 'Many
total (61, 286)
--
22 Sort
23 Sort' Term
37 Identity
38 PrecomputeFreeVars a
54 IntSet
59 Type
62 WriterT IntSet Identity
65 Term
74 a
136 'Many
total (186, 974)
--
68 KindRep
70 IgnoreSorts
87 VarOcc' a
116 FlexRig' a
146 LiftedRep
199 b
226 c
493 a
653 Type
816 'Many
total (896, 5650)
--
24 Term
31 Type
38 'One
39 TyCon
41 Addr#
41 TrName
45 Int
87 'Many
105 KindRep
191 String
total (122, 950)
--
43 Pattern' a
45 KindRep
47 DeBruijnPattern
80 b
93 Int
104 LiftedRep
105 m
119 a
326 Type
411 'Many
total (557, 3104)
--
52 Monad m
58 Type -> Type
82 TermLike a
84 Term -> m
85 Term -> m Term
103 a
116 Term
182 Type
392 m
473 'Many
total (505, 2800)
--
73 KindRep
76 CompiledClauses' a
85 x
92 c
109 String
116 m
187 b
301 a
664 Type
718 'Many
total (935, 5486)
--
14 Term
16 AllMetas b
20 MetaId
29 MetaId -> m
34 a
34 AllMetas a
35 Monoid m
78 m
132 Type
191 'Many
total (225, 943)
--
31 KindRep
34 GetDefs a
36 Monad m
38 b
39 MonadGetDefs m
44 Type -> Type
70 ()
73 Type
128 m
144 'Many
total (214, 1117)
--
52 KindRep
61 Type -> Type
63 Pattern -> m Pattern
74 LiftedRep
83 CPatternLike p
144 p
184 Type
200 Pattern
263 m
518 'Many
total (499, 3026)
--
26 MemoKey
26 Expr
30 Int
36 Pattern
52 MaybePlaceholder e
56 LiftedRep
81 Type
105 KindRep
129 e
251 'Many
total (368, 1963)
--
97 Type -> Type
146 Declaration
158 ExprLike a
159 Expr -> Expr
164 LiftedRep
191 Expr
249 a
384 m
420 Type
918 'Many
total (970, 5568)
--
29 Fixity'
40 KindRep
41 Type -> Type
43 MonadicFixPol m
58 DeclaredNames
68 LiftedRep
89 b
94 Name
111 m
182 'Many
total (184, 1381)
--
425 S
464
  'MetaSel
    ('Nothing @Symbol)
    'NoSourceUnpackedness
    'NoSourceStrictness
    'DecidedLazy
901 String
921 x
1443 Type
total (905, 9698)
--
    'NoSourceStrictness
    'DecidedLazy
116 Zero
118 S
130 LiftedRep
150 Doc
221 C
277 String
473 x
841 Type
total (536, 5729)
--
39 ()
42 LoneSig
43 Nice
45 NiceEnv
48 Name
75 KindRep
105 a
116 NiceState
143 Type
252 'Many
total (274, 1877)
--
15 Cohesion
19 Type
19 Relevance
21 KindRep
22 Quantity
48 LiftedRep
57 a
61 String
68 Attribute
104 'Many
total (113, 761)
--
37 Aspects
42 LiftedRep
64 'One
66 ParseError
80 a
109 ParseState
115 KindRep
143 Type
297 'Many
332 String
total (294, 2358)
--
17 CurrentInput
17 PreviousInput
18 LexAction a
22 b
22 ParseState
25 AlexInput
32 a
35 KindRep
59 Type
154 'Many
total (139, 711)
--
21 KindRep
21 LookAhead b
27 Char
28 StateT AlexInput Parser
30 ErrorFunction
31 b
47 AlexInput
56 a
99 Type
100 'Many
total (124, 784)
--
8 Literal
11 Token
12 ()
13 Int
25 LookAhead
27 String
28 LiftedRep
47 (String, Char)
60 Char
65 'Many
total (66, 420)
[137 of 427] Compiling Agda.Syntax.Parser.Layout[boot] ( src/full/Agda/Syntax/Parser/Layout.hs-boot, interpreted )
1 Module
1 Token
1 Parser ()
1 ()
3 LexAction Token
total (5, 7)
--
2 LexAction r
3 LexState
3 LexPredicate
3 LexAction tok
4 tok
4 String
5 a
7 LexAction Token
10 Type
23 'Many
total (60, 123)
--
6 PreviousInput -> CurrentInput -> TokenLength -> Parser Token
9 Type
9 LookAhead ()
9 ()
10 a
10 String
11 Parser
16 Token
22 LiftedRep
36 'Many
total (55, 232)
--
32 AlexInput
38 Int
38 KindRep
58 Type
72 Keyword -> LexAction Token
120 'Many
152 LexAction Token
575 (Int, LexAction Token)
628 AlexAcc ([LexState], ParseFlags)
653 ([LexState], ParseFlags)
total (155, 2817)
--
16 String
18 Parser
22 a
24 Type
25 Interval
28 Integer
39 Token
40 Char
48 LiftedRep
142 'Many
total (130, 766)
--
6 LexAction Token
9 PreviousInput -> CurrentInput -> TokenLength -> Parser Token
10 LayoutStatus
10 Parser ()
13 ()
14 Column
20 LiftedRep
20 Token
27 Parser
39 'Many
total (47, 256)
--
40 Char
41 KindRep
46 CallStack
46 Name
49 String
52 Attr
105 Parser
121 Expr
204 LiftedRep
331 'Many
total (454, 2727)
--
  -> Happy_IntList
  -> HappyStk HappyAbsSyn
  -> Parser HappyAbsSyn
586 Token
606 b
631 LiftedRep
934 KindRep
2202 'Many
2241 Type
3390 HappyAbsSyn
total (1067, 22495)
--
22 b
23 ExceptT ParseError (StateT [ParseWarning] IO)
28 IO
28 StateT [ParseWarning] IO
34 ParseError
46 [ParseWarning]
72 KindRep
73 a
135 Type
152 'Many
total (227, 1263)
--
43 TrName
43
  'MetaData "Phase" "Agda.Benchmarking" "Agda-2.6.5-inplace" 'False
62 Phase
67 'Many
123 Zero
162 C
190 U1 @Type
380 x
572 Type
total (369, 3106)
--
34 KindRep
37 a
42 SingleFlexRig
42 SingleVarOcc
42 VarCounts
47 LiftedRep
61 c
90 Type
120 b
280 'Many
total (242, 1547)
--
31 SubstArg a
32 Nat
39 Subst a
43 KindRep
45 LiftedRep
63 Int
72 Substitution' a
97 Type
181 a
207 'Many
total (176, 1246)
--
188 Scope
199 C
220 S
253 KindRep
253 Zero
323 LiftedRep
397 String
482 x
1201 Type
1476 'Many
total (1937, 14236)
--
108 ConPatLazy
116 Zero
121 R
126 Range
128 KindRep
159 S
183 x
321 String
495 'Many
569 Type
total (853, 5330)
--
    'NoSourceUnpackedness
    'NoSourceStrictness
    'DecidedLazy
767 R
892 S
973 LiftedRep
1542 String
1829 x
2103 'Many
4693 Type
total (4589, 40252)
--
76 Expr -> Expr
78 Declaration
118 Expr -> m Expr -> m Expr
149 Type -> Type
170 ExprLike a
278 a
528 Type
682 Expr
1024 m
1257 'Many
total (1146, 7922)
--
17 KindRep
24 e
32 a
36 BoundAndUsed a
37 Set Name
42 Expr
56 b
118 Type
155 BoundAndUsedNames
212 'Many
total (323, 1407)
--
16 Pattern' e1
16 Expr
20 f
24 Maybe
25 e
28 ()
29 Pattern' e
31 Type
31 Name
68 'Many
total (153, 635)
--
38 NamedArg (Pattern' e)
40 Pattern' e
61 Pattern' a
68 e
71 KindRep
122 LiftedRep
144 a
199 m
242 Type
530 'Many
total (597, 3385)
--
67 Aspects
70 FilePath
74 LiftedRep
90 S
103 x
104 KindRep
131 Doc
194 String
307 Type
307 'Many
total (552, 3740)
--
26 [String]
28 AgdaLibFile
30 [Char]
33 LibParseError
34 LiftedRep
39 ExceptT LibParseError (Writer [LibWarning'])
40 Char
60 KindRep
88 String
143 'Many
total (183, 1079)
--
8 Int32
9 ()
10 LiftedRep
13 KindRep
19 [Range]
25 String
25 Ranges
37 Int
78 Range
85 'Many
total (72, 422)
--
43 b
53 KindRep
61 PairInt a
63 LiftedRep
78 Map Int (PairInt a)
98 RangeMap a
108 Type
126 Int
198 'Many
221 a
total (197, 1544)
--
42 hl
42 Key
54 C
75 U1 @Type
93 PositionMap
98 Zero
98 Aspects
168 b
178 Type
313 'Many
total (502, 2589)
--
4 [KindRep]
5 TyCon
6 b
6 'False
6 'True
7 Addr#
7 TrName
8 'Many
10 Bool
23 KindRep
total (27, 106)
--
1 a -> Bool
1 forall a. a -> a -> Bool
1 Bool
1 Module
2 Addr#
2 Type
2 TrName
2 'Lifted
4 'Many
6 a
total (11, 23)
--
44 (a, Bool)
61 Any
62 b
74 LiftedRep
76 Identity
115 Type -> Type
147 m
179 a
212 Type
299 'Many
total (347, 2181)
--
101 ChangeT Nice
110 ([NiceDeclaration], [Declaration])
115 Declaration
136 CallStack
148 Name
185 [NiceDeclaration]
293 NiceDeclaration
323 LiftedRep
370 Nice
678 'Many
total (494, 5347)
--
1 VarSet -> VarSet
1 Type
1 Module
1 Key
1 IntSet
2 Addr#
2 Int
2 TrName
2 VarSet
3 'Many
total (11, 17)
--
34 Graph
42 NodeId
44 Rigid
62 Node
71 KindRep
71 Weight
74 Doc
76 Type
127 Int
289 'Many
total (259, 1774)
--
7 Eq a
8 Show a
10 Boolean a
12 KindRep
27 b
39 WithDefault' a b
41 Bool
41 Type
49 a
70 'Many
total (95, 429)
--
17 [a]
18 KindRep
22 g
26 m
32 f
40 b
87 ListZipper a
154 a
166 Type
274 'Many
total (289, 1461)
--
2 (# #)
3 IO a
4 Int
5 String
7 IO FilePath
8 IO
8 IOException
10 Char
20 'Many
27 FilePath
total (28, 117)
--
5 LiftedRep
5 'MetaData
    "AnArbitrarySymbolInThisPackage"
    "Agda.Version"
    "Agda-2.6.5-inplace"
    'False
6 'Many
8 String
8 AnArbitrarySymbolInThisPackage
12 Type
total (37, 109)
--
2 Addr#
2 [a]
2 Maybe String
2 Type
2 LiftedRep
2 TrName
4 'Many
6 String
7 Char
9 [Char]
total (16, 45)
--
38 StateT LibState IO
39 AgdaLibFile
40 [FilePath]
48 String
49 IO
53 [AgdaLibFile]
97 WriterT LibErrWarns (StateT LibState IO)
128 FilePath
135 LiftedRep
177 'Many
total (319, 2059)
--
261 LiftedRep
261 Zero
323 WithDefault 'False
487 S
546 x
582 Bool
683 PragmaOptions
1155 'Many
1299 Type
1305 String
total (1599, 15147)
--
15 n
15 w
17 Monad m
21 PragmaOptions
21 CommandLineOptions
54 Type
107 HasOptions m
121 Type -> Type
139 'Many
178 m
total (236, 1062)
--
3 Doc
4 Bool
4 Type
5 Aspects
5 Aspect
7 ()
9 IO ()
10 m
17 'Many
33 SGR
total (36, 135)
[176 of 427] Compiling Agda.Interaction.Options ( src/full/Agda/Interaction/Options.hs, interpreted )
1 Module
2 Addr#
2 TrName
total (3, 5)
[177 of 427] Compiling Agda.Compiler.Treeless.Pretty[boot] ( src/full/Agda/Compiler/Treeless/Pretty.hs-boot, interpreted )
1 Module
1 Pretty Compiled
1 Compiled
total (3, 3)
--
2 a
2 IORef TCState -> TCEnv -> m a
2 HighlightingLevel
2 HighlightingMethod
4 TCMT m
7 m
8 Type -> Type
8 'Many
14 TyCon
21 Type
total (47, 107)
--
23 opts
28 [KindRep]
36 R
36 S
37 Backend'_boot tcm opts env menv mod def
46 Type -> Type
62 x
67 'Many
127 KindRep
360 Type
total (336, 1513)
--
179 'One
183 ReadPrec
185 range
220 KindRep
253 Interaction' range
272 b
344 a
455 Type
760 String
824 'Many
total (747, 6826)
--
10 ResponseContextEntry
11 Expr
13 'Many
54 [KindRep]
63 Addr#
63 TrName
64 TyCon
72 'One
124 Type
253 KindRep
total (74, 846)
--
    'DecidedLazy
2244 KindRep
2543 C
2963 R
3203 Zero
3749 S
4320 String
8413 x
9445 'Many
17317 Type
total (16544, 137494)
--
150 Args
157 CallStack
168 Subst a
172 t
223 Sort
564 a
666 Type
770 LiftedRep
883 Term
2463 'Many
total (1735, 13455)
--
32 All
32 Any
33 a
38 KindRep
52 b
56 Type
62 TTerm
72 Int
102 Occurs
237 'Many
total (196, 1206)
--
42 TTerm
50 Aspects
54 Doc Aspects
67 ReaderT PEnv Identity
68 P Doc
74 PEnv
85 Int
105 LiftedRep
123 Doc
144 'Many
total (151, 1305)
--
4 Int
4 [a]
5 (# #) -> Bool
5 TAlt
6 Bool
6 (# #)
7 a
15 TTerm
30 'Many
37 Integer
total (35, 153)
--
2 (# #)
3 m
3 TTerm -> TTerm
4 Int
4 CallStack
8 LiftedRep
9 TPrim
13 TAlt
36 'Many
51 TTerm
total (39, 173)
--
66 Dict
69 'One
96 IO
111 LiftedRep
123 t
141 a
190 KindRep
233 Int32
293 Type
415 'Many
total (407, 3611)
--
10 TCState
11 TCMT IO ()
13 Map TopLevelModuleName ModuleInfo
14 ModuleInfo
20 m
21 Doc
23 TCMT IO
36 TopLevelModuleName
40 LiftedRep
48 'Many
total (88, 418)
--
14 TCEnv -> TCEnv
18 m a -> m a
18 TCEnv
22 a
26 Type -> Type
26 MonadTCEnv m
30 Type
32 m
36 LiftedRep
70 'Many
total (91, 480)
--
2 SomeBuiltin -> m (Maybe (Builtin PrimFun))
2 forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type).
  (MonadTrans t, HasBuiltins n, (~) @(Type -> Type) (t n) m) =>
  SomeBuiltin -> m (Maybe (Builtin PrimFun))
2 TyCon
4 HasBuiltins m
5 Type
10 Type -> Type
11 m
11 'Many
total (51, 92)
--
  forall (m :: Type -> Type).
  (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
  m Term
223 MonadError TCErr m
223 ReadTCState m
225 MonadTCEnv m
360 HasBuiltins m
383 Type -> Type
624 m
1365 'Many
total (585, 6252)
--
2 TCMT IO Defn
3 []
3 (# #)
5 IO
7 LiftedRep
8 TCMT IO
10 Bool
11 Int
11 Defn
29 'Many
total (55, 144)
--
7 SplitTree' SplitTag
7 Clause
8 a
8 CallStack
8 CompiledClauses
11 KindRep
12 Term
18 LiftedRep
38 Int
45 'Many
total (78, 298)
--
56 Term
59 Semigroup m
81 QName
97 a
118 NamesIn a
128 Monoid m
216 Either QName MetaId -> m
399 Type
639 m
733 'Many
total (830, 4215)
[196 of 427] Compiling Agda.Interaction.Output ( src/full/Agda/Interaction/Output.hs, interpreted )
1 Module
1 OutputConstraint_boot TCErr a b
1 OutputForm_boot TCErr a b
2 a
2 b
2 Addr#
2 TrName
2 TCErr
6 Type
total (9, 19)
--
1 Args
1 ReduceM (Reduced (Blocked [Elim]) Term)
1 ReduceM (Reduced (Blocked Args) Term)
1 MaybeReducedElims
1 MaybeReducedArgs
1 Reduced (Blocked [Elim]) Term
1 Reduced (Blocked Args) Term
2 Term
2 CompiledClauses
4 'Many
total (19, 24)
[198 of 427] Compiling Agda.TypeChecking.Reduce.Fast[boot] ( src/full/Agda/TypeChecking/Reduce/Fast.hs-boot, interpreted )
1 Term -> ReduceM (Blocked Term)
1 Term -> ReduceM Term
1 Module
1 Blocked Term
1 ReduceM (Blocked Term)
1 ReduceM Term
2 'Many
4 Term
total (8, 12)
--
1 TopLevelModuleName
  -> ModuleName -> TCM (ModuleName, Map ModuleName Scope)
1 Module
1 Map ModuleName Scope
1 TopLevelModuleName
1 Scope
1 TCM (ModuleName, Map ModuleName Scope)
1 (ModuleName, Map ModuleName Scope)
2 'Many
3 ModuleName
total (10, 13)
--
1 Type
1 Module
1 QName
1 BackendName
1 TCM
1 TCM Bool
1 TCM (Maybe Backend)
1 Backend_boot TCM
1 Backend
2 'Many
total (14, 15)
[201 of 427] Compiling Agda.Compiler.Builtin[boot] ( src/full/Agda/Compiler/Builtin.hs-boot, interpreted )
1 [Backend]
1 Module
1 Backend
total (3, 3)
[202 of 427] Compiling Agda.Compiler.Treeless.Erase[boot] ( src/full/Agda/Compiler/Treeless/Erase.hs-boot, interpreted )
1 QName -> TCM Bool
1 Bool
1 Module
1 'Many
1 QName
1 TCM Bool
total (6, 6)
--
1 Type -> Arg Term -> Type -> TCM ()
1 Type -> TCM ()
1 Term -> Type -> Arg Term -> Type -> TCM ()
1 Module
1 Arg Term
1 TCM ()
1 ()
2 Type
2 Term
4 'Many
total (11, 16)
--
2 Range
2 Telescope
3 Term
3 Args
3 ExpandHidden
4 Comparison
4 TCM Term
6 Type
6 Expr
34 'Many
total (64, 122)
--
1 Module
1 QName
1 SplitTree
1 Clause
1 Type
1 CompiledClauses
1 TCM (Maybe SplitTree, Bool, CompiledClauses)
1 (Maybe SplitTree, Bool, CompiledClauses)
1 (QName, Type)
2 'Many
total (16, 17)
[206 of 427] Compiling Agda.TypeChecking.Rules.Data[boot] ( src/full/Agda/TypeChecking/Rules/Data.hs-boot, interpreted )
1 QName -> Sort -> TCM ()
1 Sort -> TCM ()
1 Module
1 QName
1 Sort
1 TCM ()
1 ()
2 'Many
total (8, 9)
--
1 ModuleApplication
1 ImportDirective
1 DefInfo
1 ScopeCopyInfo
1 Expr
1 ()
2 Erased
2 Declaration
4 TCM ()
14 'Many
total (31, 49)
[208 of 427] Compiling Agda.Interaction.Highlighting.Generate[boot] ( src/full/Agda/Interaction/Highlighting/Generate.hs-boot, interpreted )
1 TCWarning -> TCM ()
1 Module
1 'Many
1 TCM ()
1 TCWarning
1 ()
total (6, 6)
--
1 ()
1 (List1 (WithHiding Name), Maybe Type)
1 (Term, Type)
2 Type -> TCM Term
3 Expr -> Type -> TCM Term
3 Expr
3 Comparison
5 Type
5 Term
12 'Many
total (30, 56)
[210 of 427] Compiling Agda.TypeChecking.Primitive[boot] ( src/full/Agda/TypeChecking/Primitive.hs-boot, interpreted )
1 Module
1 Map PrimitiveId (TCM PrimitiveImpl)
1 PrimitiveId
1 TCM PrimitiveImpl
1 PrimitiveImpl
total (5, 5)
--
1 [AbsolutePath]
1 Module
1 AbsolutePath
1 LibM a
1 HasOptions m
1 TCM a
2 a
2 m
3 Type
3 'Many
total (16, 22)
--
1 Level -> m Term
1 HasBuiltins m => Level -> m Term
1 forall (m :: Type -> Type). HasBuiltins m => Level -> m Term
1 Module
1 Level
1 Term
1 HasBuiltins m
2 m
2 Type
3 'Many
total (12, 16)
--
2 MonadTrans t
2 InteractionId
2 InteractionPoints
2 ReadTCState m
2 MonadInteractionPoints n
5 Type
5 MonadInteractionPoints m
10 m
12 Type -> Type
17 'Many
total (61, 119)
--
4 m a
4 (Type -> Type) -> Type -> Type
4 (~) @(Type -> Type) (t n) m
4 MonadTransControl t
4 MonadAddContext n
7 m
7 MonadAddContext m
13 Type
16 Type -> Type
36 'Many
total (99, 206)
[215 of 427] Compiling Agda.TypeChecking.Monad.Debug[boot] ( src/full/Agda/TypeChecking/Monad/Debug.hs-boot, interpreted )
1 Type -> Type
1 TyCon
1 Module
1 'Many
2 Type
total (5, 6)
--
1 MonadTCM tcm
1 MonadTCEnv m
1 ReadTCState m
1 MonadDebug m
2 tcm
2 Type -> Type
2 Type
2 QName
4 m
7 'Many
total (23, 36)
--
87 a
104 VerboseKey
108 LiftedRep
122 VerboseLevel
124 String
187 Type
264 MonadDebug m
312 Type -> Type
491 m
732 'Many
total (764, 4397)
--
17 Integer -> Integer
19 ()
20 KindRep
23 Integer
28 Type
35 String
40 MonadStatistics m
53 Type -> Type
70 m
120 'Many
total (176, 781)
--
4 MonadTCM tcm
5 tcm
6 ()
7 'Many
8 IO
9 Phase
9 TCMT IO (BenchmarkOn Phase)
16 BenchmarkOn Phase
20 LiftedRep
23 TCMT IO
total (32, 144)
--
17 m1
18 Maybe LoadedFileCache
18 LoadedFileCache
19 MonadTCState m
22 m ()
25 ()
26 Type -> Type
40 LiftedRep
70 m
97 'Many
total (113, 618)
--
2 TCM a
2 Definition
2 HasConstInfo n
4 QName
5 HasConstInfo m
6 Type
6 TyCon
12 Type -> Type
15 m
21 'Many
total (76, 153)
--
1 forall (m :: Type -> Type). HasConstInfo m => QName -> m Bool
1 Bool
1 Module
1 TCM ()
1 HasConstInfo m
1 ()
2 m
2 Type
2 QName
4 'Many
total (15, 21)
--
1 TCState
1 TCEnv
1 Definition
1 MonadTCEnv m
1 ReadTCState m
1 HasConstInfo m
2 Bool
2 Type
4 m
8 'Many
total (22, 34)
--
1 PureTCM (StateT s m)
1 PureTCM (WriterT w m)
1 PureTCM TCM
2 w
2 TyCon
4 PureTCM m
5 Type -> Type
6 Type
6 'Many
12 m
total (40, 70)
--
4 forall (m :: Type -> Type) (t :: Type -> Type).
  (Applicative m, Foldable t) =>
  t (m Doc) -> m Doc
5 a
7 Applicative m
7 Type
9 m
12 m Doc
12 Type -> Type
23 'Many
total (95, 179)
--
1 Module
1 Range
1 Doc
1 Call
1 Closure Call
1 MonadPretty m
2 m
2 m Doc
2 Type
5 'Many
total (17, 24)
--
1 Module
1 WarningName
1 Doc
1 Warning
2 m
2 m Doc
2 Type -> Type
2 Type
2 MonadPretty m
5 'Many
total (16, 25)
--
28 HasOptions m
28 Warning
28 MonadInteractionPoints m
30 MonadFresh NameId m
32 TCWarning
36 MonadWarning m
37 WhichWarnings
53 Type -> Type
117 m
149 'Many
total (247, 1336)
--
1 Goals_boot TCErr
1 GoalDisplayInfo_boot TCErr
1 DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
1 Response_boot TCErr TCWarning WarningsAndNonFatalErrors
2 Addr#
2 TrName
2 WarningsAndNonFatalErrors
3 TCWarning
5 Type
5 TCErr
total (12, 25)
--
37 Signature
40 Type -> Type
52 ScopeInfo
55 ()
60 a
60 QName
77 m
138 LiftedRep
139 TCMT IO
428 'Many
total (345, 2391)
--
32 Closure Call
36 TCEnv
69 Call
83 a
103 MonadTrace m
106 LiftedRep
116 Type -> Type
155 Type
208 m
370 'Many
total (426, 2453)
--
11 Substitution
12 Type -> Type
12 LiftedRep
14 MaybeT m
14 Open a
20 CheckpointId
21 Type
29 a
36 m
61 'Many
total (108, 434)
--
76 MonadTCEnv m
146 Term
180 Name
180 MonadAddContext m
219 a
240 LiftedRep
264 Type -> Type
309 Type
473 m
950 'Many
total (1054, 6306)
--
1 HasBuiltins m
1 MonadAddContext m
1 MonadDebug m
1 HasConstInfo m
1 MonadPretty m
1 ()
2 Type
3 Polarity
11 m
14 'Many
total (34, 60)
--
20 MonadTCEnv tcm
23 tcm a
27 TCEnv
28 Type -> Type
30 LiftedRep
35 m
43 a
45 tcm
46 Type
87 'Many
total (135, 743)
--
6 ReadTCState m
8 m b
8 Closure a
9 a
9 b
11 m (Closure b)
14 LiftedRep
16 Type
21 m
30 'Many
total (48, 210)
--
36 Bool
36 ()
39 ProblemConstraint
41 Type
44 LiftedRep
44 KindRep
63 MonadConstraint m
81 Type -> Type
188 m
210 'Many
total (225, 1532)
--
2 m a
2 a -> TCM b
2 TCM b
3 a
3 ProblemId
4 TCM a
4 TCM ()
5 m
6 Type
17 'Many
total (42, 80)
--
86 m
91 ()
93 QName
99 AbstractName
110 Type
137 ModuleName
185 Name
205 TCMT IO
376 LiftedRep
595 'Many
total (730, 5004)
--
13 List1 AbstractName
14 Name
14 AbstractName
15 KindRep
19 Scope
21 Map QName (List1 AbstractName)
24 NewNotation
36 LiftedRep
39 QName
58 'Many
total (118, 535)
--
34 HasBuiltins m
38 QName
44 Type
48 KindRep
54 String
57 DeepSizeView
63 LiftedRep
111 m
119 Term
275 'Many
total (286, 1842)
--
38 PersistentVerbosity
40 SafeMode
44 LiftedRep
50 PragmaOptions
58 CommandLineOptions
72 a
74 Type
75 FilePath
86 KindRep
270 'Many
total (223, 1620)
--
8 Set QName
9 IO
10 tcm
11 Maybe MutualBlock
11 QName
22 LiftedRep
27 TCMT IO
33 MutualId
34 MutualBlock
41 'Many
total (61, 309)
--
54 MemoKey
56 TCMT IO
60 []
63 QName
87 MaybePlaceholder e
94 KindRep
148 Pattern
183 LiftedRep
189 e
319 'Many
total (398, 3118)
--
19 Bool
19 FilePath
23 TopLevelModuleName
30 IO
43 String
56 LiftedRep
60 SourceFile
63 TCMT IO
82 AbsolutePath
138 'Many
total (164, 991)
--
29 PragmaOptions
30 [AbsolutePath]
31 Type -> Type
40 AbsolutePath
41 TopLevelModuleName
60 ()
66 m
108 LiftedRep
111 TCMT IO
145 'Many
total (205, 1367)
--
530 ReaderT Dict IO
608 ReaderT Dict IO Int32
635 EmbPrj
716 a
1470 Int32
1673 'Many
2533 LiftedRep
2615 [Type]
3004 '[] @Type
5357 Type
total (2403, 41079)
--
141 EmbPrj
169 'Many
186 ()
224 Aspect
234 NameKind
245 Int32
282 LiftedRep
477 [Type]
507 '[] @Type
783 Type
total (292, 6059)
--
292 EmbPrj
298 WhyInScope
342 Precedence
460 'Many
470 Pattern' e
489 Int32
1148 LiftedRep
1316 [Type]
1457 '[] @Type
2381 Type
total (811, 17346)
--
1 Blocked Term
1 Type
1 TCM ()
1 ReduceM (Reduced (Blocked Term) Term)
1 Reduced (Blocked Term) Term
1 RewriteRules
1 ()
2 Elims
4 Term
7 'Many
total (19, 29)
--
1 QName -> Elims -> TCM (Reduced () Term)
1 Elims -> TCM (Reduced () Term)
1 Module
1 QName
1 Elims
1 Term
1 TCM (Reduced () Term)
1 Reduced () Term
1 ()
2 'Many
total (10, 11)
--
143 Bool
143 Defn
197 Definition
250 HasConstInfo m
323 Type -> Type
370 QName
400 TCMT IO
537 LiftedRep
645 m
1969 'Many
total (1186, 10469)
--
1 Either SigError ConHead
1 Module
1 ConHead
1 SigError
2 Type -> Type
2 Type
2 HasConstInfo m
3 m
3 QName
5 'Many
total (18, 29)
--
15 e
15 r
15 s
16 w
16 Monoid w
67 Type
151 PureTCM m
152 Type -> Type
168 'Many
206 m
total (295, 1203)
--
  Type -> m (Maybe (Term, Term, Term, Term))
1 Maybe (Term, Term, Term, Term)
1 Module
1 Type
1 PureTCM m
1 (Term, Term, Term, Term)
2 m
2 Type
3 'Many
4 Term
total (14, 21)
--
1 Bool
1 Module
1 LensSort a
1 MonadBlock m
1 PureTCM m
1 PrettyTCM a
3 a
3 m
3 Type
6 'Many
total (19, 30)
--
  Type -> a -> m Type
2 HasBuiltins m
3 Type -> Type
3 Type
3 MonadReduce m
3 PiApplyM a
4 a
6 m
6 Type
14 'Many
total (42, 79)
--
75 MetaKind
84 CallStack
84 MonadMetaSolver m
95 ReadTCState m
123 Type
129 LiftedRep
155 MetaId
248 Type -> Type
518 m
791 'Many
total (823, 5056)
--
3 String
3 Args
4 Type
4 Type
4 Term
5 m
5 MetaId
8 Type -> Type
8 MonadMetaSolver m
31 'Many
total (80, 154)
[260 of 427] Compiling Agda.TypeChecking.Monad ( src/full/Agda/TypeChecking/Monad.hs, interpreted )
1 Module
2 Addr#
2 TrName
total (3, 5)
--
1 ReadTCState m
1 (QName, Defn)
2 HasConstInfo m => QName -> m Bool
2 Type
2 Defn
5 HasConstInfo m
6 Type -> Type
6 QName
8 m
16 'Many
total (48, 87)
--
2 Args
3 Type -> Term -> Term -> m ()
5 Type
5 Term
6 m ()
6 Comparison
11 m
13 MonadConversion m
14 Type -> Type
43 'Many
total (90, 203)
--
1 DefInfo
1 TCM Definition
1 TCM ()
1 ExtLamInfo
1 ()
2 DefInfo -> QName -> [Clause] -> TCM ()
2 QName
2 TCM a
2 Definition
12 'Many
total (34, 49)
--
3 TypeOf a
3 Type
3 CheckInternal a
3 Action m
6 MonadCheckInternal m
7 a
8 Type
9 Type -> Type
14 m
25 'Many
total (77, 160)
--
2 Args
2 MonadMatch m
2 Match Term
3 a
3 Type -> Type
3 'One
4 m
4 TyCon
8 Type
11 'Many
total (44, 79)
--
1 Module
1 TCM (Either ErrorNonEmpty Int)
1 TCM ()
1 ErrorNonEmpty
1 ()
2 Range
2 Telescope
2 Type
2 TCM Bool
6 'Many
total (21, 30)
[267 of 427] Compiling Agda.TypeChecking.Rules.Builtin.Coinduction[boot] ( src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs-boot, interpreted )
1 Module
1 'Many
1 Type
1 ResolvedName
1 TCM ()
1 ()
3 ResolvedName -> TCM ()
3 TCM Type
total (8, 12)
--
11 String
15 a
15 TCState
17 m
17 ReduceM a
21 Term
28 Type
30 LiftedRep
37 ReduceM
80 'Many
total (146, 549)
--
3 String
3 ReduceM a
4 LiftedRep
4 HasCallStack
5 [String]
6 a
6 Type
8 "callStack"
11 'Many
12 CallStack
total (27, 88)
--
8 HasOptions m
8 MonadTCEnv m
11 Type -> Type
11 KindRep
11 HasConstInfo m
12 m Term
15 LiftedRep
29 m
31 Term
76 'Many
total (90, 379)
--
135 m
172 Constraint
193 Sort
287 t
327 a
336 LiftedRep
742 Type
1078 Term
1079 ReduceM
2220 'Many
total (1963, 14045)
--
82 Type -> Type
82 Telescope
102 a
131 Int
145 Type
167 LiftedRep
174 m
217 Type
221 Term
573 'Many
total (644, 4076)
--
35 FUN 'Many @{LiftedRep} @{LiftedRep}
38 SynEq a
39 Sort
53 ReduceM
69 Type
97 Term
103 Bool
132 a
152 StateT Bool ReduceM
275 'Many
total (338, 2136)
--
39 LevelKit
41 b
53 Level
58 LiftedRep
69 Integer
104 a
107 Type
159 m
163 Term
345 'Many
total (333, 2136)
--
11 t
12 SingleLevel
13 Constraint
18 Int
19 [Leq]
20 LiftedRep
24 SingleLevel' Term
26 Term
28 Leq
52 'Many
total (90, 399)
--
29 a
33 Elim' Term
35 MatchResult
36 Type
42 MaybeT m
49 DisplayTerm
92 m
95 Term
99 LiftedRep
258 'Many
total (273, 1760)
--
32 MonadReader MetaSet m
37 IsFree
38 Reduce a
49 MonadReduce m
49 ForceNotFree a
70 Type
105 Term
116 a
171 m
214 'Many
total (264, 1571)
--
46 Range
47 KindRep
48 QName
52 Expr
68 a
71 Hilite a
130 LiftedRep
192 Type
281 Hiliter
449 'Many
total (609, 3023)
--
14 (Modality, Nat)
15 a
16 [IsForced]
16 ForcedVariables a
18 DList (Modality, Nat)
18 TCMT IO
19 KindRep
20 Modality
28 Type
59 'Many
total (117, 461)
--
11 a
16 KindRep
16 MentionsMeta a
24 t
26 MentionsMeta t
34 Term
38 Bool
46 HashSet MetaId
67 Type
149 'Many
total (192, 757)
--
7 Type
7 ProblemConstraint
8 ()
10 f
13 [MetaId]
16 LiftedRep
18 MetaId
25 Bool
47 'Many
88 m
total (91, 401)
--
13 NamesPerClause
14 CallStack
14 Defn
16 [Clause]
18 Bool
34 TCMT IO
44 LiftedRep
49 Set QName
50 QName
189 'Many
total (133, 812)
--
13 QName
18 b
18 Elim' NLPat
19 m
20 ToNLPat a b
21 a
21 NLPat
28 LiftedRep
68 Type
87 'Many
total (157, 608)
--
51 MonadReflectedToAbstract m
52 ReadTCState m
55 MonadReader Vars m
63 HasOptions m
65 Type -> Type
73 Type
107 Expr
126 LiftedRep
284 m
310 'Many
total (430, 2655)
--
9 []
18 a
20 LiftedRep
23 TTerm
24 ArgUsage
27 Int
30 [ArgUsage]
37 TCMT IO
41 Set Int
49 'Many
total (71, 404)
--
33 String -> ForeignCode
39 'Many
50 [Type]
54 [Char]
57 CompilerPragma
59 '[] @Type
60 ForeignCode
61 SerialisedRange
80 LiftedRep
106 Type
total (105, 1030)
--
1061 FUN 'Many @{LiftedRep} @{LiftedRep}
1139 Term
1280 EmbPrj
1303 ReaderT Dict IO Int32
1913 Int32
2265 'Many
6345 LiftedRep
6566 [Type]
6917 '[] @Type
11644 Type
total (3570, 84833)
--
856 EmbPrj
1027 WithDefault' Bool 'False
1271 'Many
1517 DeclarationWarning'
1558 Int32
2378 Warning
4226 LiftedRep
4633 [Type]
5163 '[] @Type
7837 Type
total (1549, 55102)
--
48 'False
53 EmbPrj
61 [OptionsPragma]
75 ReaderT Dict IO Int32
102 Interface
132 'Many
200 [Type]
205 '[] @Type
333 Type
438 LiftedRep
total (318, 3861)
--
28 String
31 Int32
31 Type
34 a
39 ByteString
44 ()
47 IO
77 TCMT IO
88 LiftedRep
106 'Many
total (238, 1269)
--
17 Bool
20 IO ()
22 Definition
28 LiftedRep
29 IO
30 TCMT IO
36 MetaId
48 ()
63 QName
78 'Many
total (159, 770)
--
9 List1 Expr
10 Type
13 a
15 m
15 QName
15 ()
20 LiftedRep
31 TCMT IO
55 'Many
56 Expr
total (102, 444)
--
11 Name
11 LamClause
13 ScopeM Expr
14 DoStmt
16 Pattern
21 TCMT IO
29 QName
44 LiftedRep
74 'Many
74 Expr
total (91, 477)
--
13 [Char]
16 []
17 List1 String
19 Int
22 Name
26 [String]
28 LiftedRep
29 Char
47 'Many
54 String
total (77, 430)
--
7 (# #)
8 TCMT IO
9 LiftedRep
9 KindRep
9 QName
29 IdentityIn
31 TTerm
41 Int
43 b
71 'Many
total (82, 395)
--
15 Type
18 KindRep
19 BuiltinKit
21 QName
34 LiftedRep
44 QName -> Bool
50 TCMT IO
62 TAlt
102 TTerm
119 'Many
total (110, 776)
--
84 KindRep
85 RWST Env [Output] State m
95 Int
96 State
96 ()
126 String
156 LiftedRep
160 m
185 Text
336 'Many
total (306, 2898)
--
30 ()
35 Attribute
36 Bool
41 HtmlHighlight
48 String
55 Type
55 KindRep
86 LiftedRep
92 Html
159 'Many
total (221, 1462)
--
9 []
9 Args
10 Type -> Type
12 TAlt
14 LiftedRep
14 Nat
18 m
51 'Many
59 m1
107 TTerm
total (57, 389)
--
6 CallStack
6 ExitCode
6 TCMT IO ()
12 Maybe String
15 IO
19 String
22 ()
24 LiftedRep
24 'Many
29 TCMT IO
total (51, 242)
--
19 MaybeReduced Elim
20 [Elim]
21 Reduced (Blocked Elims) Term
25 Elims
26 ReduceM
29 ReduceM (Reduced (Blocked Elims) Term)
39 Elim
74 Term
82 LiftedRep
101 'Many
total (132, 833)
--
4 Defn
6 [QName]
7 QName
8 IO
9 LiftedRep
11 [TAlt]
23 TAlt
42 TCMT IO
43 'Many
57 TTerm
total (44, 264)
--
183 Name
193 m
212 Expr
216 b
266 AbsToCon
327 AbsToCon b
373 a
591 Type
749 LiftedRep
2041 'Many
total (2034, 13705)
--
7 Doc
7 MonadAbsToCon m
8 Type -> Type
8 ToConcrete a
10 HasOptions m
12 ConOfAbs a
14 a
14 Type
25 m
33 'Many
total (51, 233)
--
190 Type -> Type
222 m1
263 Bool
349 Term
350 Type
357 TCMT IO
709 Expr
938 LiftedRep
1068 m
1800 'Many
total (1638, 15498)
--
176 Semigroup (m Doc)
181 IsString (m Doc)
195 PureTCM m
196 MonadFresh NameId m
197 MonadInteractionPoints m
218 HasOptions m
220 Type -> Type
381 m Doc
585 m
611 'Many
total (819, 6559)
--
1 [Doc]
1 [ProblemConstraint]
1 Module
1 Doc
1 PrettyTCM ProblemConstraint
1 MonadPretty m
2 m
2 Type
3 ProblemConstraint
4 'Many
total (17, 24)
--
14 IsString (m Doc)
16 QName
16 HasOptions m
19 m1
35 'Many
36 [m Doc]
42 []
100 LiftedRep
227 m
270 m Doc
total (148, 1191)
--
31 Nat
40 Bool
41 Type
41 TCMT IO
43 ConHead
51 Term
64 QName
100 LiftedRep
152 m
408 'Many
total (223, 1936)
--
56 NamesT m
64 b
66 ReaderT Names m
70 [String]
81 AbsN a
256 a
262 Type -> Type
311 Type
508 m
699 'Many
total (739, 4156)
--
29 Applicative m
29 QName
30 m Term
45 Type
48 String
49 Type -> Type
49 LiftedRep
106 Term
111 m
250 'Many
total (231, 1383)
--
63 FamilyOrNot a
64 TCMT IO
68 NamesT m
81 ReduceM
91 a
101 Type
103 LiftedRep
127 m
241 Term
411 'Many
total (383, 2789)
--
28 CallStack
29 Int
31 Type
76 LiftedRep
82 QuotingKit
114 ReduceM Term
128 TCMT IO
139 ReduceM
356 'Many
412 Term
total (280, 2199)
--
41 NamesT ReduceM Term
48 NamesT (TCMT IO) Term
73 ReduceM
88 NamesT ReduceM
99 Arg Term
101 TCMT IO
105 NamesT (TCMT IO)
148 'Many
193 LiftedRep
212 Term
total (132, 1668)
--
43 Maybe Term
74 NamesT (TCMT IO)
96 NamesT m Term
106 TCMT IO
109 m
133 Arg Term
168 LiftedRep
197 'Many
222 NamesT m
261 Term
total (133, 2077)
--
47 Maybe Term
74 NamesT m Term
76 NamesT (TCMT IO)
85 TCMT IO
94 Arg Term
106 m
108 LiftedRep
169 'Many
182 NamesT m
258 Term
total (137, 1791)
--
140 NamesT (ExceptT (Closure (Abs Type)) m)
145 Type
174 NamesT ReduceM
210 ReduceM
220 TCMT IO
257 Arg Term
288 m
649 LiftedRep
1137 Term
1206 'Many
total (916, 9881)
--
146 Integer
146 TCM PrimitiveImpl
155 Arg Term
185 Type
204 Nat
215 Double
438 TCMT IO
453 Term
467 LiftedRep
993 'Many
total (851, 7565)
--
54 Integer
54 Type
58 (# #)
59 TAlt
69 TPrim
89 Atom
95 ReaderT SEnv Identity
131 LiftedRep
406 TTerm
443 'Many
total (281, 2543)
--
6 CallStack
7 IO
8 Maybe QName
8 TAlt
8 CaseType
9 BuiltinKit
10 KindRep
11 TCMT IO
16 TTerm
20 'Many
total (38, 148)
--
53 LiftedRep
54 Modality
55 m Bool
55 Type -> Type
69 Bool
89 Term
89 TCMT IO
111 Type
212 m
515 'Many
total (475, 2679)
--
89 Int
90 Bool
100 TCMT IO Doc
136 QName
144 Type
170 TCMT IO
268 Term
324 LiftedRep
424 m
779 'Many
total (744, 5733)
--
9 Dom (ArgName, Type)
10 TCMT IO Doc
12 ArgName
13 Clause
14 Type
15 IO
18 'Many
23 Term
24 LiftedRep
35 TCMT IO
total (91, 331)
--
79 m1
82 Nat
88 QName
101 Node
110 a
143 Type
185 OccurrencesBuilder
239 LiftedRep
239 TCMT IO
721 'Many
total (696, 5183)
--
41 Type -> Type
43 Name
49 String
58 [TCWarning]
116 []
131 [m Doc]
231 LiftedRep
257 'Many
394 m Doc
426 m
total (394, 3228)
--
34 ()
36 TCMT IO Doc
47 TCMT IO ()
59 Bool
69 Type
102 m
115 TCMT IO
127 Term
167 LiftedRep
313 'Many
total (280, 2062)
--
13 Level
14 CallStack
17 IO
24 Type
26 Int
35 Type
39 LiftedRep
57 TCMT IO
65 Term
94 'Many
total (164, 757)
--
76 LiftedRep
77 LeftoverPatterns
86 FlexibleVar a
87 String
106 b
130 a
138 m
189 KindRep
233 Type
550 'Many
total (646, 3976)
--
22 WithOrigin (Ranged ArgName)
25 m1
31 Type
43 Type
49 TCMT IO
50 TCMT IO Doc
65 Term
78 LiftedRep
95 m
165 'Many
total (307, 1503)
--
16 Type
20 Type
22 NamedArg Pattern
28 Term
30 TCMT IO
35 [NamedArg Pattern]
39 TCMT IO Doc
47 LiftedRep
63 m
67 'Many
total (179, 761)
--
18 Pattern
22 m
22 IO
24 ExpandPatternSynonyms a
26 Pattern' e
32 a
32 TCMT IO
38 LiftedRep
55 Type
70 'Many
total (179, 730)
--
94 b
111 Cmp
117 r
123 Int
135 f
136 String
163 rigid1
171 a
657 Type
873 'Many
total (868, 5262)
--
135 Node r f
135 Weight
146 SizeExpr' r f
189 Label
203 Offset
224 r
273 LiftedRep
307 f
531 Type
948 'Many
total (883, 6769)
--
66 UnifyState
68 UnifyStep
106 Int
108 KindRep
126 LiftedRep
144 m Doc
147 Term
224 m
271 'Many
454 String
total (328, 3127)
--
80 NamesT (ExceptT NoLeftInv tcm)
93 ()
105 TCMT IO
119 [Arg Term]
122 ExceptT NoLeftInv tcm
142 Telescope
225 tcm
229 'Many
287 Term
380 LiftedRep
total (369, 3742)
--
46 a
51 b
52 Type
54 m1
68 TCMT IO Doc
73 TCMT IO
93 LiftedRep
95 Term
102 m
231 'Many
total (324, 1987)
--
79 PureConversionT m
85 StateT FreshThings m
95 Monad m
107 FreshThings
121 TCErr
128 a
177 Type
293 Type -> Type
600 m
706 'Many
total (710, 4268)
--
25 Type
27 Telescope
28 NamedArg Pattern
29 Type
37 Term
48 LiftedRep
52 m
60 TCMT IO
62 TCMT IO Doc
64 'Many
total (223, 987)
--
63 a
63 SplitPatVar
70 Term
74 Type
80 String
91 DList (Nat, SplitPattern)
92 TCMT IO
120 LiftedRep
157 m
294 'Many
total (341, 2684)
--
55 Either (RecPatM (Pattern, [Term], Changes)) RecordTree
62 KindRep
94 TCMT IO Doc
99 Int
104 Term
125 TCMT IO
136 m
142 Type
209 LiftedRep
329 'Many
total (541, 3664)
--
20 m
23 TCM a
24 Int
24 Nat
28 a
28 Type
49 TCMT IO
59 LiftedRep
68 Term
143 'Many
total (205, 979)
--
91 VarSet
93 KindRep
111 b
121 m
137 LiftedRep
145 TCMT IO
156 TerEnv
238 a
362 Type
676 'Many
total (731, 4635)
--
57 IO
77 LiftedRep
94 Type
100 a
107 NLPat
131 m
156 TCMT IO
181 Term
204 Type
430 'Many
total (568, 3394)
--
102 TCMT IO
103 NLMState
105 TCMT IO Doc
116 a
119 NLM
158 ()
167 LiftedRep
217 Type
231 Term
470 'Many
total (554, 4064)
--
19 TCMT IO
20 HashSet QName
21 m1
24 OpaqueId
25 OpaqueBlock
25 ()
42 LiftedRep
56 QName
59 m
86 'Many
total (147, 727)
--
33 TAlt
35 [TAlt]
41 QName
47 TCMT IO
53 ESt
81 LiftedRep
104 TypeInfo
108 StateT ESt TCM
141 TTerm
302 'Many
total (272, 1905)
--
108 Char
113 QName
127 Term
130 m1
239 [m Doc]
296 []
423 'Many
722 LiftedRep
1195 m
1466 m Doc
total (647, 8158)
--
20 PureTCM m
21 MonadInteractionPoints m
22 MonadFresh NameId m
22 Doc
24 LiftedRep
24 ProblemConstraint
34 m1
90 m Doc
95 'Many
150 m
total (186, 1076)
--
70 TCMT IO Doc
71 SizeMaxView
84 DeepSizeView
98 ()
105 Int
170 Term
186 TCMT IO
244 LiftedRep
275 m
367 'Many
total (409, 3572)
--
55 Nat
69 [Polarity]
71 Type -> Type
89 Type
89 LeastPolarity m
91 Term
105 LiftedRep
114 Polarity
290 m
452 'Many
total (451, 2842)
--
55 ()
56 Bool
59 Maybe TermHead
89 Term
94 TermHead
104 TCMT IO Doc
156 TCMT IO
163 LiftedRep
212 m
386 'Many
total (421, 3019)
--
64 CallStack
70 Candidate
82 ()
94 [Candidate]
96 Type
140 Term
191 TCMT IO Doc
285 LiftedRep
326 'Many
484 TCMT IO
total (423, 3607)
--
129 Order
137 QName
145 Calls
148 Type
157 TCMT IO Doc
187 Term
313 TCMT IO
354 TerM
494 LiftedRep
622 'Many
total (700, 6028)
--
24 ()
29 TCMT IO Doc
44 CallStack
48 LiftedRep
65 Type
105 TCMT IO
114 Sort
127 Term
138 m
147 'Many
total (184, 1433)
--
33 ProblemId
33 Constraint
44 ProblemConstraint
51 TCMT IO Doc
55 TCMT IO ()
78 m
85 ()
102 LiftedRep
171 TCMT IO
238 'Many
total (314, 1744)
--
123 Type
134 m
141 Bool
155 TCMT IO Doc
212 ()
217 ReaderT OccursCtx TCM
253 TCMT IO
272 Term
323 LiftedRep
728 'Many
total (715, 5729)
--
107 UnifyStep
125 Int
129 a
143 m1
147 UnificationResult' UnifyState
152 Type
213 Term
515 LiftedRep
540 m
650 'Many
total (759, 6277)
--
15 Key
17 Int
17 TCMT IO ()
19 Type
20 IO
22 ()
46 LiftedRep
51 'Many
51 Term
74 TCMT IO
total (131, 652)
--
123 Type
160 Type
174 TCMT IO ()
299 TCMT IO Doc
340 m
368 ()
498 Term
575 LiftedRep
916 'Many
944 TCMT IO
total (896, 8423)
--
198 Type
262 Bool
365 m ()
671 ()
761 TCMT IO Doc
858 TCMT IO
927 LiftedRep
1031 Term
1300 m
1320 'Many
total (916, 14409)
--
14 TCMT IO
14 TCMT IO Doc
14 MonadWarning m
17 MonadError TCErr m
18 PureTCM m
21 m Doc
26 Maybe TypeError
32 LiftedRep
37 'Many
99 m
total (96, 631)
--
18 Arg Term
18 TCM Doc
26 Type
27 a
51 TCMT IO ()
58 ()
118 'Many
119 LiftedRep
122 Term
168 TCMT IO
total (235, 1398)
--
58 Int
63 ()
71 MetaId
88 NamedRigid
93 SizeMeta
96 Term
99 TCMT IO Doc
266 LiftedRep
272 TCMT IO
331 'Many
total (455, 3607)
--
11 Telescope
13 Addr#
13 TrName
16 SplitClause
21 'One
21 UnifyEquiv
36 [KindRep]
57 'Many
79 String
142 KindRep
total (91, 597)
--
106 Clause
111 Dom Type
185 Telescope
223 [Term]
376 NamesT (TCMT IO) Term
724 NamesT (TCMT IO)
997 LiftedRep
1090 TCMT IO
1132 'Many
1246 Term
total (842, 11817)
--
38 TCWarning
41 NameKindBuilder
47 b
57 RangePair
69 Aspects
83 Range
102 TCMT IO
147 LiftedRep
147 HighlightingInfoBuilder
265 'Many
total (310, 2150)
--
74 CallStack
81 QName
110 ()
113 Type
147 MetaId
190 Term
248 TCMT IO Doc
356 LiftedRep
420 'Many
580 TCMT IO
total (582, 4892)
--
158 Arg Term
159 ()
160 Telescope
284 NamesT (TCMT IO) Term
291 Type
336 NamesT (TCMT IO)
1002 LiftedRep
1044 TCMT IO
1082 Term
1255 'Many
total (1043, 11922)
--
57 PureTCM m
72 MonadCheckInternal m
86 Type -> Type
87 TCMT IO
108 TCMT IO Doc
121 Type
152 LiftedRep
304 Term
360 m
483 'Many
total (407, 3647)
--
34 KindRep
63 Bool
68 a
94 Type
104 TCMT IO Doc
105 Type
151 TCMT IO
162 LiftedRep
258 Term
280 'Many
total (364, 2362)
--
49 []
58 Int
59 Type
105 [NamedArg Pattern]
110 WriterT [ProblemEq] TCM
137 Term
208 TCMT IO Doc
292 LiftedRep
312 TCMT IO
322 'Many
total (460, 3569)
--
169 a
169 ExceptT TCErr tcm
179 m
252 ()
276 CallStack
281 Term
463 TCMT IO Doc
848 TCMT IO
877 LiftedRep
910 'Many
total (1118, 10541)
--
20 Elim
25 Args
31 Elims
32 Arg Term
50 TCMT IO Doc
58 Type
98 LiftedRep
146 'Many
161 Term
169 TCMT IO
total (168, 1233)
--
142 CallStack
155 QName
389
  ReaderT
    Context
    (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
417 LiftedRep
557 TCMT IO
633 Term
942 'Many
total (920, 7957)
--
102 CallStack
114 TCMT IO ()
123 Expr
135 ()
264 TCMT IO Doc
287 Type
503 Term
634 LiftedRep
702 'Many
902 TCMT IO
total (800, 7220)
--
105 Bool
105 SplitClause
115 ()
120 Type
122 Telescope
224 Term
358 TCMT IO Doc
626 'Many
643 TCMT IO
718 LiftedRep
total (823, 7692)
--
13 Type
14 Telescope
16 ()
24 Either ErrorNonEmpty ()
31 LiftedRep
31 Term
36 TCMT IO
43 b
49 ErrorNonEmpty
55 'Many
total (124, 588)
--
31 CompiledClauses
32 Term
36 Int
43 Pattern' PatVarName
48 Bool
50 Arg Pattern
69 TCMT IO
91 Cl
123 LiftedRep
187 'Many
total (316, 1843)
--
54 Term
78 CCEnv
80 QName
83 TCMT IO Doc
103 ReaderT CCEnv TCM
180 TTerm
180 TCMT IO
197 LiftedRep
212 Int
376 'Many
total (315, 2938)
--
66 QName
71 TCMT IO ()
72 Type
80 Telescope
127 Term
135 ()
138 TCMT IO Doc
276 'Many
281 LiftedRep
346 TCMT IO
total (354, 2977)
--
149 TCMT IO Type
153 NamesT (TCMT IO)
160 Type
178 BuiltinId
211 BuiltinInfo
254 ()
497 Term
573 LiftedRep
657 'Many
1014 TCMT IO
total (439, 6254)
--
13 QName
13 Tele (Dom Type)
13 CompiledClauses' Term
14 IO
18 TCMT IO Type
29 Type
58 'Many
81 TCMT IO
91 Term
114 LiftedRep
total (103, 725)
--
121 TCMT IO ()
137 Type
143 ()
208 TCMT IO Doc
236 Type
430 LiftedRep
474 TCMT IO
546 Term
583 m
919 'Many
total (982, 7797)
--
40 QName
59 TCMT IO ()
59 RewriteRule
62 CallStack
74 TCMT IO Doc
81 ()
122 Term
201 'Many
205 LiftedRep
261 TCMT IO
total (276, 2256)
--
140 [Literal] -> Term
141 ReduceM CompactDefn
163 CompactDefn
200 Term
227 KindRep
272 a
397 Type
488 LiftedRep
509 s
1058 'Many
total (786, 7776)
--
83 Telescope
100 KindRep
116 Type
125 TCMT IO ()
191 ()
249 Term
329 TCMT IO Doc
538 'Many
601 LiftedRep
777 TCMT IO
total (724, 6486)
--
106 ()
134 QName
141 Expr
175 Arg Term
274 Type
351 TCMT IO Doc
478 Term
805 LiftedRep
924 TCMT IO
962 'Many
total (790, 8622)
--
64 Telescope
66 QName
72 CallStack
74 Term
171 TCMT IO Doc
238 TCMT IO ()
331 ()
556 LiftedRep
569 'Many
596 TCMT IO
total (520, 5037)
[389 of 427] Compiling Agda.TheTypeChecker ( src/full/Agda/TheTypeChecker.hs, interpreted )
1 Module
2 Addr#
2 TrName
total (3, 5)
--
254 KindRep
256 Name
282 Type
318 Expr
360 CallStack
387 ()
500 IO
1231 LiftedRep
1549 TCMT IO
1561 'Many
total (1812, 16140)
--
133 TCMT IO Doc
173 Type
187 a
223 Type
296 m
320 Term
400 Expr
513 LiftedRep
710 TCMT IO
1121 'Many
total (1222, 9569)
--
67 ExceptT String TCM
106 TCMT IO ()
111 Interface
113 String
159 [Char]
177 ModuleInfo
291 ()
420 LiftedRep
481 'Many
593 TCMT IO
total (629, 5155)
--
15 StateT (Set ModuleName) TCM
20 ()
23 TopLevelModuleName
25 Set ModuleName
27 Interface
36 r
40 m
48 LiftedRep
52 TCMT IO
73 'Many
total (168, 858)
--
27 menv
28 ()
30 def
30 env
30 opts
37 mod
40 LiftedRep
81 Type
87 TCMT IO
112 'Many
total (223, 1144)
--
53 ()
64 Bool
65 JSOptions
72 PrimitiveId
77 Type
83 String
183 Exp
206 TCMT IO
221 LiftedRep
509 'Many
total (427, 3447)
--
15 S
16 LiftedRep
16 FilePath
16 LaTeXCompileEnv
17 x
28 KindRep
43 m
43 LaTeXFlags
55 Type
101 'Many
total (195, 859)
[397 of 427] Compiling Agda.Interaction.Highlighting.LaTeX ( src/full/Agda/Interaction/Highlighting/LaTeX.hs, interpreted )
1 Module
2 Addr#
2 TrName
total (3, 5)
--
20 String
25 S
26 HtmlCompileEnv
27 x
28 LiftedRep
44 KindRep
47 m
55 HtmlFlags
77 Type
109 'Many
total (211, 1088)
[399 of 427] Compiling Agda.Interaction.Highlighting.HTML ( src/full/Agda/Interaction/Highlighting/HTML.hs, interpreted )
1 Module
2 Addr#
2 TrName
total (3, 5)
--
22 DotModule
24 String
24 DotCompileEnv
30 TopLevelModuleName
35 m
36 LiftedRep
41 DotFlags
48 KindRep
50 Type
105 'Many
total (218, 1057)
[401 of 427] Compiling Agda.Interaction.Highlighting.Dot ( src/full/Agda/Interaction/Highlighting/Dot.hs, interpreted )
1 Module
2 Addr#
2 TrName
total (3, 5)
--
45 String
45 'One
47 Type
51 GHCEnv
59 ReadGHCModuleEnv m
61 GHCModuleEnv
85 Type -> Type
108 KindRep
141 m
294 'Many
total (344, 2083)
--
30 TCMT IO
32 SomeBuiltin
73 LiftedRep
111 m String
113 Either String Exp
113 (PrimitiveId, m (Either String Exp))
120 Exp
246 m
279 'Many
525 String
total (240, 2355)
--
2 []
2 TrName
2 (# #)
4 [Char] -> [Char]
4 String
4 LiftedRep
4 ModuleName
25 'Many
27 Char
30 [Char]
total (24, 121)
--
14 Exp
20 Type
28 [Doc]
56 []
58 Int
75 Doc Aspects
120 LiftedRep
142 'Many
142 Aspects
303 Doc
total (197, 1409)
--
29 ReaderT GHCModuleEnv (StateT HsCompileState TCM)
32 Maybe HaskellCode
35 Char
36 HaskellCode
38 m
39 ()
55 HaskellPragma
84 LiftedRep
95 String
226 'Many
total (233, 1522)
--
48 ExceptT WhyNot HsCompileM
49 WhyNot
59 TCMT IO
66 m Doc
74 m
86 Term
88 ReaderT GHCModuleEnv (StateT HsCompileState TCM)
99 LiftedRep
157 Type
287 'Many
total (341, 2250)
--
112 (UsesFloat, [Decl])
115 m
115 String
115 Decl
116 [Decl]
169 TCMT IO
197 Exp
240 ReaderT GHCModuleEnv (StateT HsCompileState TCM)
429 LiftedRep
865 'Many
total (861, 7095)
[409 of 427] Compiling Agda.Compiler.Builtin ( src/full/Agda/Compiler/Builtin.hs, interpreted )
1 [Backend]
1 Module
2 Addr#
2 TrName
7 Backend
total (5, 13)
--
14 IO
14 Term
15 b
16 TermToPattern a b
17 KindRep
21 TCMT IO
24 a
28 Pattern' a
49 'Many
66 Type
total (109, 461)
--
18 Telescope
19 ()
22 Doc Aspects
22 TCMT IO
29 Tele (Dom Type)
29 TCMT IO ()
31 'Many
45 Doc
47 Aspects
48 LiftedRep
total (67, 486)
--
16 IM a
17 TCMT (InputT IO) a
20 IM
25 b
28 IO
31 TCMT (InputT IO)
44 InputT IO
64 a
87 'Many
112 Type
total (137, 699)
--
15 EncodeTCM a
16 IO
16 KindRep
19 Doc
20 TCM Value
24 a
24 TCMT IO
44 Type
94 Value
106 'Many
total (117, 668)
--
3 Aspect
3 HighlightingInfo
4 a
5 HighlightingMethod
6 NameKind
7 Char
7 OtherAspect
8 Aspects
16 String
17 'Many
total (34, 113)
--
5 IO
5 IO Value
5 FilePath
6 Int
9 Type
19 Text
20 TokenBased
20 Pair
43 'Many
43 Value
total (74, 291)
--
3 (Range, Aspects)
4 Char
4 ModuleToSource
5 IO (Lisp String)
7 Int
8 [Lisp String]
20 LiftedRep
29 'Many
41 String
49 Lisp String
total (48, 226)
--
2 TrName
2 QName
2 Definition
3 [TAlt]
3 Args
6 IO
10 TAlt
22 'Many
27 TCMT IO
47 TTerm
total (26, 142)
--
34 IO
36 m
37 Term
46 CallStack
51 String
63 Bool
130 TCMT IO Doc
212 LiftedRep
253 'Many
280 TCMT IO
total (422, 2649)
--
17 Addr#
17 TrName
18 LiftedRep
21 Options
27 Token
29 KindRep
30 Int
32 HintMode
76 String
90 'Many
total (101, 603)
--
211 Doc Aspects
235 x
244 Component
342 Doc
377 Aspects
380 TCMT IO
548 LiftedRep
589 ReaderT SearchOptions TCM
623 Type
1389 'Many
total (1481, 13565)
--
56 StateT ReplState IM
60 ReplState
65 ReplEnv
85 String
112 TCMT IO
128 a
178 Type
185 ()
195 LiftedRep
366 'Many
total (417, 3129)
--
10 Char
10 (Name, AbstractName)
11 Type
12 [(Name, Type)]
13 AbstractName
14 []
18 TCMT IO
22 LiftedRep
23 String
30 'Many
total (75, 320)
--
78 TCErr
84 a
84 CommandM ()
90 TCM
192 CommandState
203 TCMT IO
235 ()
296 StateT CommandState TCM
468 'Many
473 LiftedRep
total (664, 5114)
--
7 TCM
9 Command
13 LiftedRep
16 CommandState
17 'Many
18 Bool
19 IO
23 TCMT IO
24 StateT CommandState TCM
40 ()
total (53, 259)
--
35 [Char]
49 Doc Aspects
57 Aspects
73 [Lisp String]
88 Doc
112 'Many
134 TCMT IO
152 LiftedRep
174 Lisp String
182 String
total (159, 1643)
--
49 TCM Value
60 BuildStep r
60 BufferRange
60 BuildSignal r
62 TCMT IO
160 Type
202 TCM Pair
231 Text
447 Value
468 'Many
total (385, 3311)
--
30 Char
31 KindRep
38 IO ()
52 IO
58 String
66 [Char]
75 ()
78 TCMT IO
126 'Many
139 LiftedRep
total (196, 1393)