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