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