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