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