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