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