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