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