Generate Typeable info at definition sites
[ghc.git] / compiler / typecheck / TcTyDecls.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1999
4
5
6 Analysis functions over data types. Specficially, detecting recursive types.
7
8 This stuff is only used for source-code decls; it's recorded in interface
9 files for imported data types.
10 -}
11
12 {-# LANGUAGE CPP #-}
13
14 module TcTyDecls(
15 calcRecFlags, RecTyInfo(..),
16 calcSynCycles, calcClassCycles,
17
18 -- * Roles
19 RoleAnnots, extractRoleAnnots, emptyRoleAnnots, lookupRoleAnnots,
20
21 -- * Implicits
22 tcAddImplicits
23 ) where
24
25 #include "HsVersions.h"
26
27 import TcRnMonad
28 import TcEnv
29 import TcTypeable( mkTypeableBinds )
30 import TcBinds( tcValBinds, addTypecheckedBinds )
31 import TypeRep( Type(..) )
32 import TcType
33 import TysWiredIn( unitTy )
34 import MkCore( rEC_SEL_ERROR_ID )
35 import HsSyn
36 import Class
37 import Type
38 import HscTypes
39 import TyCon
40 import DataCon
41 import Name
42 import NameEnv
43 import RdrName ( mkVarUnqual )
44 import Id
45 import IdInfo
46 import VarEnv
47 import VarSet
48 import NameSet
49 import Coercion ( ltRole )
50 import Digraph
51 import BasicTypes
52 import SrcLoc
53 import Unique ( mkBuiltinUnique )
54 import Outputable
55 import UniqSet
56 import Util
57 import Maybes
58 import Data.List
59 import Bag
60 import FastString ( fastStringToByteString )
61
62 import Control.Monad
63
64 {-
65 ************************************************************************
66 * *
67 Cycles in class and type synonym declarations
68 * *
69 ************************************************************************
70
71 Checking for class-decl loops is easy, because we don't allow class decls
72 in interface files.
73
74 We allow type synonyms in hi-boot files, but we *trust* hi-boot files,
75 so we don't check for loops that involve them. So we only look for synonym
76 loops in the module being compiled.
77
78 We check for type synonym and class cycles on the *source* code.
79 Main reasons:
80
81 a) Otherwise we'd need a special function to extract type-synonym tycons
82 from a type, whereas we already have the free vars pinned on the decl
83
84 b) If we checked for type synonym loops after building the TyCon, we
85 can't do a hoistForAllTys on the type synonym rhs, (else we fall into
86 a black hole) which seems unclean. Apart from anything else, it'd mean
87 that a type-synonym rhs could have for-alls to the right of an arrow,
88 which means adding new cases to the validity checker
89
90 Indeed, in general, checking for cycles beforehand means we need to
91 be less careful about black holes through synonym cycles.
92
93 The main disadvantage is that a cycle that goes via a type synonym in an
94 .hi-boot file can lead the compiler into a loop, because it assumes that cycles
95 only occur entirely within the source code of the module being compiled.
96 But hi-boot files are trusted anyway, so this isn't much worse than (say)
97 a kind error.
98
99 [ NOTE ----------------------------------------------
100 If we reverse this decision, this comment came from tcTyDecl1, and should
101 go back there
102 -- dsHsType, not tcHsKindedType, to avoid a loop. tcHsKindedType does hoisting,
103 -- which requires looking through synonyms... and therefore goes into a loop
104 -- on (erroneously) recursive synonyms.
105 -- Solution: do not hoist synonyms, because they'll be hoisted soon enough
106 -- when they are substituted
107
108 We'd also need to add back in this definition
109
110 synonymTyConsOfType :: Type -> [TyCon]
111 -- Does not look through type synonyms at all
112 -- Return a list of synonym tycons
113 synonymTyConsOfType ty
114 = nameEnvElts (go ty)
115 where
116 go :: Type -> NameEnv TyCon -- The NameEnv does duplicate elim
117 go (TyVarTy v) = emptyNameEnv
118 go (TyConApp tc tys) = go_tc tc tys
119 go (AppTy a b) = go a `plusNameEnv` go b
120 go (FunTy a b) = go a `plusNameEnv` go b
121 go (ForAllTy _ ty) = go ty
122
123 go_tc tc tys | isTypeSynonymTyCon tc = extendNameEnv (go_s tys)
124 (tyConName tc) tc
125 | otherwise = go_s tys
126 go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
127 ---------------------------------------- END NOTE ]
128 -}
129
130 mkSynEdges :: [LTyClDecl Name] -> [(LTyClDecl Name, Name, [Name])]
131 mkSynEdges syn_decls = [ (ldecl, name, nameSetElems fvs)
132 | ldecl@(L _ (SynDecl { tcdLName = L _ name
133 , tcdFVs = fvs })) <- syn_decls ]
134
135 calcSynCycles :: [LTyClDecl Name] -> [SCC (LTyClDecl Name)]
136 calcSynCycles = stronglyConnCompFromEdgedVertices . mkSynEdges
137
138 {-
139 Note [Superclass cycle check]
140 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
141 We can't allow cycles via superclasses because it would result in the
142 type checker looping when it canonicalises a class constraint (superclasses
143 are added during canonicalisation). More precisely, given a constraint
144 C ty1 .. tyn
145 we want to instantiate all of C's superclasses, transitively, and
146 that set must be finite. So if
147 class (D b, E b a) => C a b
148 then when we encounter the constraint
149 C ty1 ty2
150 we'll instantiate the superclasses
151 (D ty2, E ty2 ty1)
152 and then *their* superclasses, and so on. This set must be finite!
153
154 It is OK for superclasses to be type synonyms for other classes, so
155 must "look through" type synonyms. Eg
156 type X a = C [a]
157 class X a => C a -- No! Recursive superclass!
158
159 We want definitions such as:
160
161 class C cls a where cls a => a -> a
162 class C D a => D a where
163
164 to be accepted, even though a naive acyclicity check would reject the
165 program as having a cycle between D and its superclass. Why? Because
166 when we instantiate
167 D ty1
168 we get the superclas
169 C D ty1
170 and C has no superclasses, so we have terminated with a finite set.
171
172 More precisely, the rule is this: the superclasses sup_C of a class C
173 are rejected iff:
174
175 C \elem expand(sup_C)
176
177 Where expand is defined as follows:
178
179 (1) expand(a ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
180
181 (2) expand(D ty1 ... tyN) = {D}
182 \union sup_D[ty1/x1, ..., tyP/xP]
183 \union expand(ty(P+1)) ... \union expand(tyN)
184 where (D x1 ... xM) is a class, P = min(M,N)
185
186 (3) expand(T ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
187 where T is not a class
188
189 Eqn (1) is conservative; when there's a type variable at the head,
190 look in all the argument types. Eqn (2) expands superclasses; the
191 third component of the union is like Eqn (1). Eqn (3) happens mainly
192 when the context is a (constraint) tuple, such as (Eq a, Show a).
193
194 Furthermore, expand always looks through type synonyms.
195 -}
196
197 calcClassCycles :: Class -> [[TyCon]]
198 calcClassCycles cls
199 = nubBy eqAsCycle $
200 expandTheta (unitUniqSet cls) [classTyCon cls] (classSCTheta cls) []
201 where
202 -- The last TyCon in the cycle is always the same as the first
203 eqAsCycle xs ys = any (xs ==) (cycles (tail ys))
204 cycles xs = take n . map (take n) . tails . cycle $ xs
205 where n = length xs
206
207 -- No more superclasses to expand ==> no problems with cycles
208 -- See Note [Superclass cycle check]
209 expandTheta :: UniqSet Class -- Path of Classes to here in set form
210 -> [TyCon] -- Path to here
211 -> ThetaType -- Superclass work list
212 -> [[TyCon]] -- Input error paths
213 -> [[TyCon]] -- Final error paths
214 expandTheta _ _ [] = id
215 expandTheta seen path (pred:theta) = expandType seen path pred . expandTheta seen path theta
216
217 expandType seen path (TyConApp tc tys)
218 -- Expand unsaturated classes to their superclass theta if they are yet unseen.
219 -- If they have already been seen then we have detected an error!
220 | Just cls <- tyConClass_maybe tc
221 , let (env, remainder) = papp (classTyVars cls) tys
222 rest_tys = either (const []) id remainder
223 = if cls `elementOfUniqSet` seen
224 then (reverse (classTyCon cls:path):)
225 . flip (foldr (expandType seen path)) tys
226 else expandTheta (addOneToUniqSet seen cls) (tc:path)
227 (substTys (mkTopTvSubst env) (classSCTheta cls))
228 . flip (foldr (expandType seen path)) rest_tys
229
230 -- For synonyms, try to expand them: some arguments might be
231 -- phantoms, after all. We can expand with impunity because at
232 -- this point the type synonym cycle check has already happened.
233 | Just (tvs, rhs) <- synTyConDefn_maybe tc
234 , let (env, remainder) = papp tvs tys
235 rest_tys = either (const []) id remainder
236 = expandType seen (tc:path) (substTy (mkTopTvSubst env) rhs)
237 . flip (foldr (expandType seen path)) rest_tys
238
239 -- For non-class, non-synonyms, just check the arguments
240 | otherwise
241 = flip (foldr (expandType seen path)) tys
242
243 expandType _ _ (TyVarTy {}) = id
244 expandType _ _ (LitTy {}) = id
245 expandType seen path (AppTy t1 t2) = expandType seen path t1 . expandType seen path t2
246 expandType seen path (FunTy t1 t2) = expandType seen path t1 . expandType seen path t2
247 expandType seen path (ForAllTy _tv t) = expandType seen path t
248
249 papp :: [TyVar] -> [Type] -> ([(TyVar, Type)], Either [TyVar] [Type])
250 papp [] tys = ([], Right tys)
251 papp tvs [] = ([], Left tvs)
252 papp (tv:tvs) (ty:tys) = ((tv, ty):env, remainder)
253 where (env, remainder) = papp tvs tys
254
255 {-
256 ************************************************************************
257 * *
258 Deciding which type constructors are recursive
259 * *
260 ************************************************************************
261
262 Identification of recursive TyCons
263 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
264 The knot-tying parameters: @rec_details_list@ is an alist mapping @Name@s to
265 @TyThing@s.
266
267 Identifying a TyCon as recursive serves two purposes
268
269 1. Avoid infinite types. Non-recursive newtypes are treated as
270 "transparent", like type synonyms, after the type checker. If we did
271 this for all newtypes, we'd get infinite types. So we figure out for
272 each newtype whether it is "recursive", and add a coercion if so. In
273 effect, we are trying to "cut the loops" by identifying a loop-breaker.
274
275 2. Avoid infinite unboxing. This has nothing to do with newtypes.
276 Suppose we have
277 data T = MkT Int T
278 f (MkT x t) = f t
279 Well, this function diverges, but we don't want the strictness analyser
280 to diverge. But the strictness analyser will diverge because it looks
281 deeper and deeper into the structure of T. (I believe there are
282 examples where the function does something sane, and the strictness
283 analyser still diverges, but I can't see one now.)
284
285 Now, concerning (1), the FC2 branch currently adds a coercion for ALL
286 newtypes. I did this as an experiment, to try to expose cases in which
287 the coercions got in the way of optimisations. If it turns out that we
288 can indeed always use a coercion, then we don't risk recursive types,
289 and don't need to figure out what the loop breakers are.
290
291 For newtype *families* though, we will always have a coercion, so they
292 are always loop breakers! So you can easily adjust the current
293 algorithm by simply treating all newtype families as loop breakers (and
294 indeed type families). I think.
295
296
297
298 For newtypes, we label some as "recursive" such that
299
300 INVARIANT: there is no cycle of non-recursive newtypes
301
302 In any loop, only one newtype need be marked as recursive; it is
303 a "loop breaker". Labelling more than necessary as recursive is OK,
304 provided the invariant is maintained.
305
306 A newtype M.T is defined to be "recursive" iff
307 (a) it is declared in an hi-boot file (see RdrHsSyn.hsIfaceDecl)
308 (b) it is declared in a source file, but that source file has a
309 companion hi-boot file which declares the type
310 or (c) one can get from T's rhs to T via type
311 synonyms, or non-recursive newtypes *in M*
312 e.g. newtype T = MkT (T -> Int)
313
314 (a) is conservative; declarations in hi-boot files are always
315 made loop breakers. That's why in (b) we can restrict attention
316 to tycons in M, because any loops through newtypes outside M
317 will be broken by those newtypes
318 (b) ensures that a newtype is not treated as a loop breaker in one place
319 and later as a non-loop-breaker. This matters in GHCi particularly, when
320 a newtype T might be embedded in many types in the environment, and then
321 T's source module is compiled. We don't want T's recursiveness to change.
322
323 The "recursive" flag for algebraic data types is irrelevant (never consulted)
324 for types with more than one constructor.
325
326
327 An algebraic data type M.T is "recursive" iff
328 it has just one constructor, and
329 (a) it is declared in an hi-boot file (see RdrHsSyn.hsIfaceDecl)
330 (b) it is declared in a source file, but that source file has a
331 companion hi-boot file which declares the type
332 or (c) one can get from its arg types to T via type synonyms,
333 or by non-recursive newtypes or non-recursive product types in M
334 e.g. data T = MkT (T -> Int) Bool
335 Just like newtype in fact
336
337 A type synonym is recursive if one can get from its
338 right hand side back to it via type synonyms. (This is
339 reported as an error.)
340
341 A class is recursive if one can get from its superclasses
342 back to it. (This is an error too.)
343
344 Hi-boot types
345 ~~~~~~~~~~~~~
346 A data type read from an hi-boot file will have an AbstractTyCon as its AlgTyConRhs
347 and will respond True to isAbstractTyCon. The idea is that we treat these as if one
348 could get from these types to anywhere. So when we see
349
350 module Baz where
351 import {-# SOURCE #-} Foo( T )
352 newtype S = MkS T
353
354 then we mark S as recursive, just in case. What that means is that if we see
355
356 import Baz( S )
357 newtype R = MkR S
358
359 then we don't need to look inside S to compute R's recursiveness. Since S is imported
360 (not from an hi-boot file), one cannot get from R back to S except via an hi-boot file,
361 and that means that some data type will be marked recursive along the way. So R is
362 unconditionly non-recursive (i.e. there'll be a loop breaker elsewhere if necessary)
363
364 This in turn means that we grovel through fewer interface files when computing
365 recursiveness, because we need only look at the type decls in the module being
366 compiled, plus the outer structure of directly-mentioned types.
367 -}
368
369 data RecTyInfo = RTI { rti_promotable :: Bool
370 , rti_roles :: Name -> [Role]
371 , rti_is_rec :: Name -> RecFlag }
372
373 calcRecFlags :: SelfBootInfo -> Bool -- hs-boot file?
374 -> RoleAnnots -> [TyThing] -> RecTyInfo
375 -- The 'boot_names' are the things declared in M.hi-boot, if M is the current module.
376 -- Any type constructors in boot_names are automatically considered loop breakers
377 calcRecFlags boot_details is_boot mrole_env tyclss
378 = RTI { rti_promotable = is_promotable
379 , rti_roles = roles
380 , rti_is_rec = is_rec }
381 where
382 rec_tycon_names = mkNameSet (map tyConName all_tycons)
383 all_tycons = mapMaybe getTyCon tyclss
384 -- Recursion of newtypes/data types can happen via
385 -- the class TyCon, so tyclss includes the class tycons
386
387 is_promotable = all (computeTyConPromotability rec_tycon_names) all_tycons
388
389 roles = inferRoles is_boot mrole_env all_tycons
390
391 ----------------- Recursion calculation ----------------
392 is_rec n | n `elemNameSet` rec_names = Recursive
393 | otherwise = NonRecursive
394
395 boot_name_set = case boot_details of
396 NoSelfBoot -> emptyNameSet
397 SelfBoot { sb_tcs = tcs } -> tcs
398 rec_names = boot_name_set `unionNameSet`
399 nt_loop_breakers `unionNameSet`
400 prod_loop_breakers
401
402
403 -------------------------------------------------
404 -- NOTE
405 -- These edge-construction loops rely on
406 -- every loop going via tyclss, the types and classes
407 -- in the module being compiled. Stuff in interface
408 -- files should be correctly marked. If not (e.g. a
409 -- type synonym in a hi-boot file) we can get an infinite
410 -- loop. We could program round this, but it'd make the code
411 -- rather less nice, so I'm not going to do that yet.
412
413 single_con_tycons = [ tc | tc <- all_tycons
414 , not (tyConName tc `elemNameSet` boot_name_set)
415 -- Remove the boot_name_set because they are
416 -- going to be loop breakers regardless.
417 , isSingleton (tyConDataCons tc) ]
418 -- Both newtypes and data types, with exactly one data constructor
419
420 (new_tycons, prod_tycons) = partition isNewTyCon single_con_tycons
421 -- NB: we do *not* call isProductTyCon because that checks
422 -- for vanilla-ness of data constructors; and that depends
423 -- on empty existential type variables; and that is figured
424 -- out by tcResultType; which uses tcMatchTy; which uses
425 -- coreView; which calls expandSynTyCon_maybe; which uses
426 -- the recursiveness of the TyCon. Result... a black hole.
427 -- YUK YUK YUK
428
429 --------------- Newtypes ----------------------
430 nt_loop_breakers = mkNameSet (findLoopBreakers nt_edges)
431 is_rec_nt tc = tyConName tc `elemNameSet` nt_loop_breakers
432 -- is_rec_nt is a locally-used helper function
433
434 nt_edges = [(t, mk_nt_edges t) | t <- new_tycons]
435
436 mk_nt_edges nt -- Invariant: nt is a newtype
437 = [ tc | tc <- nameEnvElts (tyConsOfType (new_tc_rhs nt))
438 -- tyConsOfType looks through synonyms
439 , tc `elem` new_tycons ]
440 -- If not (tc `elem` new_tycons) we know that either it's a local *data* type,
441 -- or it's imported. Either way, it can't form part of a newtype cycle
442
443 --------------- Product types ----------------------
444 prod_loop_breakers = mkNameSet (findLoopBreakers prod_edges)
445
446 prod_edges = [(tc, mk_prod_edges tc) | tc <- prod_tycons]
447
448 mk_prod_edges tc -- Invariant: tc is a product tycon
449 = concatMap (mk_prod_edges1 tc) (dataConOrigArgTys (head (tyConDataCons tc)))
450
451 mk_prod_edges1 ptc ty = concatMap (mk_prod_edges2 ptc) (nameEnvElts (tyConsOfType ty))
452
453 mk_prod_edges2 ptc tc
454 | tc `elem` prod_tycons = [tc] -- Local product
455 | tc `elem` new_tycons = if is_rec_nt tc -- Local newtype
456 then []
457 else mk_prod_edges1 ptc (new_tc_rhs tc)
458 -- At this point we know that either it's a local non-product data type,
459 -- or it's imported. Either way, it can't form part of a cycle
460 | otherwise = []
461
462 new_tc_rhs :: TyCon -> Type
463 new_tc_rhs tc = snd (newTyConRhs tc) -- Ignore the type variables
464
465 getTyCon :: TyThing -> Maybe TyCon
466 getTyCon (ATyCon tc) = Just tc
467 getTyCon _ = Nothing
468
469 findLoopBreakers :: [(TyCon, [TyCon])] -> [Name]
470 -- Finds a set of tycons that cut all loops
471 findLoopBreakers deps
472 = go [(tc,tc,ds) | (tc,ds) <- deps]
473 where
474 go edges = [ name
475 | CyclicSCC ((tc,_,_) : edges') <- stronglyConnCompFromEdgedVerticesR edges,
476 name <- tyConName tc : go edges']
477
478 {-
479 ************************************************************************
480 * *
481 Role annotations
482 * *
483 ************************************************************************
484 -}
485
486 type RoleAnnots = NameEnv (LRoleAnnotDecl Name)
487
488 extractRoleAnnots :: TyClGroup Name -> RoleAnnots
489 extractRoleAnnots (TyClGroup { group_roles = roles })
490 = mkNameEnv [ (tycon, role_annot)
491 | role_annot@(L _ (RoleAnnotDecl (L _ tycon) _)) <- roles ]
492
493 emptyRoleAnnots :: RoleAnnots
494 emptyRoleAnnots = emptyNameEnv
495
496 lookupRoleAnnots :: RoleAnnots -> Name -> Maybe (LRoleAnnotDecl Name)
497 lookupRoleAnnots = lookupNameEnv
498
499 {-
500 ************************************************************************
501 * *
502 Role inference
503 * *
504 ************************************************************************
505
506 Note [Role inference]
507 ~~~~~~~~~~~~~~~~~~~~~
508 The role inference algorithm datatype definitions to infer the roles on the
509 parameters. Although these roles are stored in the tycons, we can perform this
510 algorithm on the built tycons, as long as we don't peek at an as-yet-unknown
511 roles field! Ah, the magic of laziness.
512
513 First, we choose appropriate initial roles. For families and classes, roles
514 (including initial roles) are N. For datatypes, we start with the role in the
515 role annotation (if any), or otherwise use Phantom. This is done in
516 initialRoleEnv1.
517
518 The function irGroup then propagates role information until it reaches a
519 fixpoint, preferring N over (R or P) and R over P. To aid in this, we have a
520 monad RoleM, which is a combination reader and state monad. In its state are
521 the current RoleEnv, which gets updated by role propagation, and an update
522 bit, which we use to know whether or not we've reached the fixpoint. The
523 environment of RoleM contains the tycon whose parameters we are inferring, and
524 a VarEnv from parameters to their positions, so we can update the RoleEnv.
525 Between tycons, this reader information is missing; it is added by
526 addRoleInferenceInfo.
527
528 There are two kinds of tycons to consider: algebraic ones (excluding classes)
529 and type synonyms. (Remember, families don't participate -- all their parameters
530 are N.) An algebraic tycon processes each of its datacons, in turn. Note that
531 a datacon's universally quantified parameters might be different from the parent
532 tycon's parameters, so we use the datacon's univ parameters in the mapping from
533 vars to positions. Note also that we don't want to infer roles for existentials
534 (they're all at N, too), so we put them in the set of local variables. As an
535 optimisation, we skip any tycons whose roles are already all Nominal, as there
536 nowhere else for them to go. For synonyms, we just analyse their right-hand sides.
537
538 irType walks through a type, looking for uses of a variable of interest and
539 propagating role information. Because anything used under a phantom position
540 is at phantom and anything used under a nominal position is at nominal, the
541 irType function can assume that anything it sees is at representational. (The
542 other possibilities are pruned when they're encountered.)
543
544 The rest of the code is just plumbing.
545
546 How do we know that this algorithm is correct? It should meet the following
547 specification:
548
549 Let Z be a role context -- a mapping from variables to roles. The following
550 rules define the property (Z |- t : r), where t is a type and r is a role:
551
552 Z(a) = r' r' <= r
553 ------------------------- RCVar
554 Z |- a : r
555
556 ---------- RCConst
557 Z |- T : r -- T is a type constructor
558
559 Z |- t1 : r
560 Z |- t2 : N
561 -------------- RCApp
562 Z |- t1 t2 : r
563
564 forall i<=n. (r_i is R or N) implies Z |- t_i : r_i
565 roles(T) = r_1 .. r_n
566 ---------------------------------------------------- RCDApp
567 Z |- T t_1 .. t_n : R
568
569 Z, a:N |- t : r
570 ---------------------- RCAll
571 Z |- forall a:k.t : r
572
573
574 We also have the following rules:
575
576 For all datacon_i in type T, where a_1 .. a_n are universally quantified
577 and b_1 .. b_m are existentially quantified, and the arguments are t_1 .. t_p,
578 then if forall j<=p, a_1 : r_1 .. a_n : r_n, b_1 : N .. b_m : N |- t_j : R,
579 then roles(T) = r_1 .. r_n
580
581 roles(->) = R, R
582 roles(~#) = N, N
583
584 With -dcore-lint on, the output of this algorithm is checked in checkValidRoles,
585 called from checkValidTycon.
586
587 Note [Role-checking data constructor arguments]
588 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
589 Consider
590 data T a where
591 MkT :: Eq b => F a -> (a->a) -> T (G a)
592
593 Then we want to check the roles at which 'a' is used
594 in MkT's type. We want to work on the user-written type,
595 so we need to take into account
596 * the arguments: (F a) and (a->a)
597 * the context: C a b
598 * the result type: (G a) -- this is in the eq_spec
599 -}
600
601 type RoleEnv = NameEnv [Role] -- from tycon names to roles
602
603 -- This, and any of the functions it calls, must *not* look at the roles
604 -- field of a tycon we are inferring roles about!
605 -- See Note [Role inference]
606 inferRoles :: Bool -> RoleAnnots -> [TyCon] -> Name -> [Role]
607 inferRoles is_boot annots tycons
608 = let role_env = initialRoleEnv is_boot annots tycons
609 role_env' = irGroup role_env tycons in
610 \name -> case lookupNameEnv role_env' name of
611 Just roles -> roles
612 Nothing -> pprPanic "inferRoles" (ppr name)
613
614 initialRoleEnv :: Bool -> RoleAnnots -> [TyCon] -> RoleEnv
615 initialRoleEnv is_boot annots = extendNameEnvList emptyNameEnv .
616 map (initialRoleEnv1 is_boot annots)
617
618 initialRoleEnv1 :: Bool -> RoleAnnots -> TyCon -> (Name, [Role])
619 initialRoleEnv1 is_boot annots_env tc
620 | isFamilyTyCon tc = (name, map (const Nominal) tyvars)
621 | isAlgTyCon tc = (name, default_roles)
622 | isTypeSynonymTyCon tc = (name, default_roles)
623 | otherwise = pprPanic "initialRoleEnv1" (ppr tc)
624 where name = tyConName tc
625 tyvars = tyConTyVars tc
626 (kvs, tvs) = span isKindVar tyvars
627
628 -- if the number of annotations in the role annotation decl
629 -- is wrong, just ignore it. We check this in the validity check.
630 role_annots
631 = case lookupNameEnv annots_env name of
632 Just (L _ (RoleAnnotDecl _ annots))
633 | annots `equalLength` tvs -> map unLoc annots
634 _ -> map (const Nothing) tvs
635 default_roles = map (const Nominal) kvs ++
636 zipWith orElse role_annots (repeat default_role)
637
638 default_role
639 | isClassTyCon tc = Nominal
640 | is_boot && isAbstractTyCon tc = Representational
641 | otherwise = Phantom
642
643 irGroup :: RoleEnv -> [TyCon] -> RoleEnv
644 irGroup env tcs
645 = let (env', update) = runRoleM env $ mapM_ irTyCon tcs in
646 if update
647 then irGroup env' tcs
648 else env'
649
650 irTyCon :: TyCon -> RoleM ()
651 irTyCon tc
652 | isAlgTyCon tc
653 = do { old_roles <- lookupRoles tc
654 ; unless (all (== Nominal) old_roles) $ -- also catches data families,
655 -- which don't want or need role inference
656 do { whenIsJust (tyConClass_maybe tc) (irClass tc_name)
657 ; addRoleInferenceInfo tc_name (tyConTyVars tc) $
658 mapM_ (irType emptyVarSet) (tyConStupidTheta tc) -- See #8958
659 ; mapM_ (irDataCon tc_name) (visibleDataCons $ algTyConRhs tc) }}
660
661 | Just ty <- synTyConRhs_maybe tc
662 = addRoleInferenceInfo tc_name (tyConTyVars tc) $
663 irType emptyVarSet ty
664
665 | otherwise
666 = return ()
667
668 where
669 tc_name = tyConName tc
670
671 -- any type variable used in an associated type must be Nominal
672 irClass :: Name -> Class -> RoleM ()
673 irClass tc_name cls
674 = addRoleInferenceInfo tc_name cls_tvs $
675 mapM_ ir_at (classATs cls)
676 where
677 cls_tvs = classTyVars cls
678 cls_tv_set = mkVarSet cls_tvs
679
680 ir_at at_tc
681 = mapM_ (updateRole Nominal) (varSetElems nvars)
682 where nvars = (mkVarSet $ tyConTyVars at_tc) `intersectVarSet` cls_tv_set
683
684 -- See Note [Role inference]
685 irDataCon :: Name -> DataCon -> RoleM ()
686 irDataCon tc_name datacon
687 = addRoleInferenceInfo tc_name univ_tvs $
688 mapM_ (irType ex_var_set) (eqSpecPreds eq_spec ++ theta ++ arg_tys)
689 -- See Note [Role-checking data constructor arguments]
690 where
691 (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig datacon
692 ex_var_set = mkVarSet ex_tvs
693
694 irType :: VarSet -> Type -> RoleM ()
695 irType = go
696 where
697 go lcls (TyVarTy tv) = unless (tv `elemVarSet` lcls) $
698 updateRole Representational tv
699 go lcls (AppTy t1 t2) = go lcls t1 >> mark_nominal lcls t2
700 go lcls (TyConApp tc tys)
701 = do { roles <- lookupRolesX tc
702 ; zipWithM_ (go_app lcls) roles tys }
703 go lcls (FunTy t1 t2) = go lcls t1 >> go lcls t2
704 go lcls (ForAllTy tv ty) = go (extendVarSet lcls tv) ty
705 go _ (LitTy {}) = return ()
706
707 go_app _ Phantom _ = return () -- nothing to do here
708 go_app lcls Nominal ty = mark_nominal lcls ty -- all vars below here are N
709 go_app lcls Representational ty = go lcls ty
710
711 mark_nominal lcls ty = let nvars = tyVarsOfType ty `minusVarSet` lcls in
712 mapM_ (updateRole Nominal) (varSetElems nvars)
713
714 -- like lookupRoles, but with Nominal tags at the end for oversaturated TyConApps
715 lookupRolesX :: TyCon -> RoleM [Role]
716 lookupRolesX tc
717 = do { roles <- lookupRoles tc
718 ; return $ roles ++ repeat Nominal }
719
720 -- gets the roles either from the environment or the tycon
721 lookupRoles :: TyCon -> RoleM [Role]
722 lookupRoles tc
723 = do { env <- getRoleEnv
724 ; case lookupNameEnv env (tyConName tc) of
725 Just roles -> return roles
726 Nothing -> return $ tyConRoles tc }
727
728 -- tries to update a role; won't ever update a role "downwards"
729 updateRole :: Role -> TyVar -> RoleM ()
730 updateRole role tv
731 = do { var_ns <- getVarNs
732 ; case lookupVarEnv var_ns tv of
733 { Nothing -> pprPanic "updateRole" (ppr tv)
734 ; Just n -> do
735 { name <- getTyConName
736 ; updateRoleEnv name n role }}}
737
738 -- the state in the RoleM monad
739 data RoleInferenceState = RIS { role_env :: RoleEnv
740 , update :: Bool }
741
742 -- the environment in the RoleM monad
743 type VarPositions = VarEnv Int
744 data RoleInferenceInfo = RII { var_ns :: VarPositions
745 , name :: Name }
746
747 -- See [Role inference]
748 newtype RoleM a = RM { unRM :: Maybe RoleInferenceInfo
749 -> RoleInferenceState
750 -> (a, RoleInferenceState) }
751
752 instance Functor RoleM where
753 fmap = liftM
754
755 instance Applicative RoleM where
756 pure x = RM $ \_ state -> (x, state)
757 (<*>) = ap
758
759 instance Monad RoleM where
760 return = pure
761 a >>= f = RM $ \m_info state -> let (a', state') = unRM a m_info state in
762 unRM (f a') m_info state'
763
764 runRoleM :: RoleEnv -> RoleM () -> (RoleEnv, Bool)
765 runRoleM env thing = (env', update)
766 where RIS { role_env = env', update = update } = snd $ unRM thing Nothing state
767 state = RIS { role_env = env, update = False }
768
769 addRoleInferenceInfo :: Name -> [TyVar] -> RoleM a -> RoleM a
770 addRoleInferenceInfo name tvs thing
771 = RM $ \_nothing state -> ASSERT( isNothing _nothing )
772 unRM thing (Just info) state
773 where info = RII { var_ns = mkVarEnv (zip tvs [0..]), name = name }
774
775 getRoleEnv :: RoleM RoleEnv
776 getRoleEnv = RM $ \_ state@(RIS { role_env = env }) -> (env, state)
777
778 getVarNs :: RoleM VarPositions
779 getVarNs = RM $ \m_info state ->
780 case m_info of
781 Nothing -> panic "getVarNs"
782 Just (RII { var_ns = var_ns }) -> (var_ns, state)
783
784 getTyConName :: RoleM Name
785 getTyConName = RM $ \m_info state ->
786 case m_info of
787 Nothing -> panic "getTyConName"
788 Just (RII { name = name }) -> (name, state)
789
790
791 updateRoleEnv :: Name -> Int -> Role -> RoleM ()
792 updateRoleEnv name n role
793 = RM $ \_ state@(RIS { role_env = role_env }) -> ((),
794 case lookupNameEnv role_env name of
795 Nothing -> pprPanic "updateRoleEnv" (ppr name)
796 Just roles -> let (before, old_role : after) = splitAt n roles in
797 if role `ltRole` old_role
798 then let roles' = before ++ role : after
799 role_env' = extendNameEnv role_env name roles' in
800 RIS { role_env = role_env', update = True }
801 else state )
802
803
804 {- *********************************************************************
805 * *
806 Building implicits
807 * *
808 ********************************************************************* -}
809
810 tcAddImplicits :: [TyThing] -> TcM TcGblEnv
811 tcAddImplicits tyclss
812 = discardWarnings $
813 tcExtendGlobalEnvImplicit implicit_things $
814 tcExtendGlobalValEnv def_meth_ids $
815 do { (rec_sel_ids, rec_sel_binds) <- mkRecSelBinds tycons
816 ; (typeable_ids, typeable_binds) <- mkTypeableBinds tycons
817 ; gbl_env <- tcExtendGlobalValEnv (rec_sel_ids ++ typeable_ids) getGblEnv
818 ; return (gbl_env `addTypecheckedBinds` (rec_sel_binds ++ typeable_binds)) }
819 where
820 implicit_things = concatMap implicitTyThings tyclss
821 tycons = [tc | ATyCon tc <- tyclss]
822 def_meth_ids = mkDefaultMethodIds tyclss
823
824 {-
825 ************************************************************************
826 * *
827 Building record selectors
828 * *
829 ************************************************************************
830 -}
831
832 mkDefaultMethodIds :: [TyThing] -> [Id]
833 -- See Note [Default method Ids and Template Haskell]
834 mkDefaultMethodIds things
835 = [ mkExportedLocalId VanillaId dm_name (idType sel_id)
836 | ATyCon tc <- things
837 , Just cls <- [tyConClass_maybe tc]
838 , (sel_id, DefMeth dm_name) <- classOpItems cls ]
839
840 {-
841 Note [Default method Ids and Template Haskell]
842 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
843 Consider this (Trac #4169):
844 class Numeric a where
845 fromIntegerNum :: a
846 fromIntegerNum = ...
847
848 ast :: Q [Dec]
849 ast = [d| instance Numeric Int |]
850
851 When we typecheck 'ast' we have done the first pass over the class decl
852 (in tcTyClDecls), but we have not yet typechecked the default-method
853 declarations (because they can mention value declarations). So we
854 must bring the default method Ids into scope first (so they can be seen
855 when typechecking the [d| .. |] quote, and typecheck them later.
856 -}
857
858 mkRecSelBinds :: [TyCon] -> TcM ([Id], [LHsBinds Id])
859 mkRecSelBinds tycons
860 = do { -- We generate *un-typechecked* bindings in mkRecSelBind, and
861 -- then typecheck them, rather like 'deriving'. This makes life
862 -- easier, because the later type checking will add all necessary
863 -- type abstractions and applications
864
865 let sel_binds :: [(RecFlag, LHsBinds Name)]
866 sel_sigs :: [LSig Name]
867 (sel_sigs, sel_binds)
868 = mapAndUnzip mkRecSelBind [ (tc,fld)
869 | tc <- tycons
870 , fld <- tyConFieldLabels tc ]
871 sel_ids = [sel_id | L _ (IdSig sel_id) <- sel_sigs]
872 ; (sel_binds, _) <- tcValBinds TopLevel sel_binds sel_sigs (return ())
873 ; return (sel_ids, map snd sel_binds) }
874
875 mkRecSelBind :: (TyCon, FieldLabel) -> (LSig Name, (RecFlag, LHsBinds Name))
876 mkRecSelBind (tycon, fl)
877 = (L loc (IdSig sel_id), (NonRecursive, unitBag (L loc sel_bind)))
878 where
879 loc = getSrcSpan sel_name
880 sel_id = mkExportedLocalId rec_details sel_name sel_ty
881 lbl = flLabel fl
882 sel_name = flSelector fl
883 rec_details = RecSelId { sel_tycon = tycon, sel_naughty = is_naughty }
884
885 -- Find a representative constructor, con1
886 all_cons = tyConDataCons tycon
887 cons_w_field = tyConDataConsWithFields tycon [lbl]
888 con1 = ASSERT( not (null cons_w_field) ) head cons_w_field
889
890 -- Selector type; Note [Polymorphic selectors]
891 field_ty = dataConFieldType con1 lbl
892 data_ty = dataConOrigResTy con1
893 data_tvs = tyVarsOfType data_ty
894 is_naughty = not (tyVarsOfType field_ty `subVarSet` data_tvs)
895 (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty
896 sel_ty | is_naughty = unitTy -- See Note [Naughty record selectors]
897 | otherwise = mkForAllTys (varSetElemsKvsFirst $
898 data_tvs `extendVarSetList` field_tvs) $
899 mkPhiTy (dataConStupidTheta con1) $ -- Urgh!
900 mkPhiTy field_theta $ -- Urgh!
901 mkFunTy data_ty field_tau
902
903 -- Make the binding: sel (C2 { fld = x }) = x
904 -- sel (C7 { fld = x }) = x
905 -- where cons_w_field = [C2,C7]
906 sel_bind = mkTopFunBind Generated sel_lname alts
907 where
908 alts | is_naughty = [mkSimpleMatch [] unit_rhs]
909 | otherwise = map mk_match cons_w_field ++ deflt
910 mk_match con = mkSimpleMatch [L loc (mk_sel_pat con)]
911 (L loc (HsVar field_var))
912 mk_sel_pat con = ConPatIn (L loc (getName con)) (RecCon rec_fields)
913 rec_fields = HsRecFields { rec_flds = [rec_field], rec_dotdot = Nothing }
914 rec_field = noLoc (HsRecField { hsRecFieldLbl = L loc (FieldOcc (mkVarUnqual lbl) sel_name)
915 , hsRecFieldArg = L loc (VarPat field_var)
916 , hsRecPun = False })
917 sel_lname = L loc sel_name
918 field_var = mkInternalName (mkBuiltinUnique 1) (getOccName sel_name) loc
919
920 -- Add catch-all default case unless the case is exhaustive
921 -- We do this explicitly so that we get a nice error message that
922 -- mentions this particular record selector
923 deflt | all dealt_with all_cons = []
924 | otherwise = [mkSimpleMatch [L loc (WildPat placeHolderType)]
925 (mkHsApp (L loc (HsVar (getName rEC_SEL_ERROR_ID)))
926 (L loc (HsLit msg_lit)))]
927
928 -- Do not add a default case unless there are unmatched
929 -- constructors. We must take account of GADTs, else we
930 -- get overlap warning messages from the pattern-match checker
931 -- NB: we need to pass type args for the *representation* TyCon
932 -- to dataConCannotMatch, hence the calculation of inst_tys
933 -- This matters in data families
934 -- data instance T Int a where
935 -- A :: { fld :: Int } -> T Int Bool
936 -- B :: { fld :: Int } -> T Int Char
937 dealt_with con = con `elem` cons_w_field || dataConCannotMatch inst_tys con
938 inst_tys = substTyVars (mkTopTvSubst (dataConEqSpec con1)) (dataConUnivTyVars con1)
939
940 unit_rhs = mkLHsTupleExpr []
941 msg_lit = HsStringPrim "" (fastStringToByteString lbl)
942
943 {-
944 Note [Polymorphic selectors]
945 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
946 When a record has a polymorphic field, we pull the foralls out to the front.
947 data T = MkT { f :: forall a. [a] -> a }
948 Then f :: forall a. T -> [a] -> a
949 NOT f :: T -> forall a. [a] -> a
950
951 This is horrid. It's only needed in deeply obscure cases, which I hate.
952 The only case I know is test tc163, which is worth looking at. It's far
953 from clear that this test should succeed at all!
954
955 Note [Naughty record selectors]
956 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
957 A "naughty" field is one for which we can't define a record
958 selector, because an existential type variable would escape. For example:
959 data T = forall a. MkT { x,y::a }
960 We obviously can't define
961 x (MkT v _) = v
962 Nevertheless we *do* put a RecSelId into the type environment
963 so that if the user tries to use 'x' as a selector we can bleat
964 helpfully, rather than saying unhelpfully that 'x' is not in scope.
965 Hence the sel_naughty flag, to identify record selectors that don't really exist.
966
967 In general, a field is "naughty" if its type mentions a type variable that
968 isn't in the result type of the constructor. Note that this *allows*
969 GADT record selectors (Note [GADT record selectors]) whose types may look
970 like sel :: T [a] -> a
971
972 For naughty selectors we make a dummy binding
973 sel = ()
974 for naughty selectors, so that the later type-check will add them to the
975 environment, and they'll be exported. The function is never called, because
976 the tyepchecker spots the sel_naughty field.
977
978 Note [GADT record selectors]
979 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
980 For GADTs, we require that all constructors with a common field 'f' have the same
981 result type (modulo alpha conversion). [Checked in TcTyClsDecls.checkValidTyCon]
982 E.g.
983 data T where
984 T1 { f :: Maybe a } :: T [a]
985 T2 { f :: Maybe a, y :: b } :: T [a]
986 T3 :: T Int
987
988 and now the selector takes that result type as its argument:
989 f :: forall a. T [a] -> Maybe a
990
991 Details: the "real" types of T1,T2 are:
992 T1 :: forall r a. (r~[a]) => a -> T r
993 T2 :: forall r a b. (r~[a]) => a -> b -> T r
994
995 So the selector loooks like this:
996 f :: forall a. T [a] -> Maybe a
997 f (a:*) (t:T [a])
998 = case t of
999 T1 c (g:[a]~[c]) (v:Maybe c) -> v `cast` Maybe (right (sym g))
1000 T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g))
1001 T3 -> error "T3 does not have field f"
1002
1003 Note the forall'd tyvars of the selector are just the free tyvars
1004 of the result type; there may be other tyvars in the constructor's
1005 type (e.g. 'b' in T2).
1006
1007 Note the need for casts in the result!
1008
1009 Note [Selector running example]
1010 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1011 It's OK to combine GADTs and type families. Here's a running example:
1012
1013 data instance T [a] where
1014 T1 { fld :: b } :: T [Maybe b]
1015
1016 The representation type looks like this
1017 data :R7T a where
1018 T1 { fld :: b } :: :R7T (Maybe b)
1019
1020 and there's coercion from the family type to the representation type
1021 :CoR7T a :: T [a] ~ :R7T a
1022
1023 The selector we want for fld looks like this:
1024
1025 fld :: forall b. T [Maybe b] -> b
1026 fld = /\b. \(d::T [Maybe b]).
1027 case d `cast` :CoR7T (Maybe b) of
1028 T1 (x::b) -> x
1029
1030 The scrutinee of the case has type :R7T (Maybe b), which can be
1031 gotten by appying the eq_spec to the univ_tvs of the data con.
1032
1033 -}