Typos in comments only [ci skip]
[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 RolesInfo,
16 inferRoles,
17 checkSynCycles,
18 checkClassCycles,
19
20 -- * Implicits
21 tcAddImplicits, mkDefaultMethodType,
22
23 -- * Record selectors
24 mkRecSelBinds, mkOneRecordSelector
25 ) where
26
27 #include "HsVersions.h"
28
29 import TcRnMonad
30 import TcEnv
31 import TcBinds( tcRecSelBinds )
32 import RnEnv( RoleAnnotEnv, lookupRoleAnnot )
33 import TyCoRep( Type(..), Coercion(..), UnivCoProvenance(..) )
34 import TcType
35 import TysWiredIn( unitTy )
36 import MkCore( rEC_SEL_ERROR_ID )
37 import HsSyn
38 import Class
39 import Type
40 import HscTypes
41 import TyCon
42 import ConLike
43 import DataCon
44 import Name
45 import NameEnv
46 import RdrName ( mkVarUnqual )
47 import Id
48 import IdInfo
49 import VarEnv
50 import VarSet
51 import NameSet ( NameSet, unitNameSet, extendNameSet, elemNameSet )
52 import Coercion ( ltRole )
53 import BasicTypes
54 import SrcLoc
55 import Unique ( mkBuiltinUnique )
56 import Outputable
57 import Util
58 import Maybes
59 import Bag
60 import FastString
61 import FV
62 import Module
63
64 import Control.Monad
65
66 {-
67 ************************************************************************
68 * *
69 Cycles in type synonym declarations
70 * *
71 ************************************************************************
72 -}
73
74 synonymTyConsOfType :: Type -> [TyCon]
75 -- Does not look through type synonyms at all
76 -- Return a list of synonym tycons
77 -- Keep this synchronized with 'expandTypeSynonyms'
78 synonymTyConsOfType ty
79 = nameEnvElts (go ty)
80 where
81 go :: Type -> NameEnv TyCon -- The NameEnv does duplicate elim
82 go (TyConApp tc tys) = go_tc tc `plusNameEnv` go_s tys
83 go (LitTy _) = emptyNameEnv
84 go (TyVarTy _) = emptyNameEnv
85 go (AppTy a b) = go a `plusNameEnv` go b
86 go (FunTy a b) = go a `plusNameEnv` go b
87 go (ForAllTy _ ty) = go ty
88 go (CastTy ty co) = go ty `plusNameEnv` go_co co
89 go (CoercionTy co) = go_co co
90
91 -- Note [TyCon cycles through coercions?!]
92 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
93 -- Although, in principle, it's possible for a type synonym loop
94 -- could go through a coercion (since a coercion can refer to
95 -- a TyCon or Type), it doesn't seem possible to actually construct
96 -- a Haskell program which tickles this case. Here is an example
97 -- program which causes a coercion:
98 --
99 -- type family Star where
100 -- Star = Type
101 --
102 -- data T :: Star -> Type
103 -- data S :: forall (a :: Type). T a -> Type
104 --
105 -- Here, the application 'T a' must first coerce a :: Type to a :: Star,
106 -- witnessed by the type family. But if we now try to make Type refer
107 -- to a type synonym which in turn refers to Star, we'll run into
108 -- trouble: we're trying to define and use the type constructor
109 -- in the same recursive group. Possibly this restriction will be
110 -- lifted in the future but for now, this code is "just for completeness
111 -- sake".
112 go_co (Refl _ ty) = go ty
113 go_co (TyConAppCo _ tc cs) = go_tc tc `plusNameEnv` go_co_s cs
114 go_co (AppCo co co') = go_co co `plusNameEnv` go_co co'
115 go_co (ForAllCo _ co co') = go_co co `plusNameEnv` go_co co'
116 go_co (CoVarCo _) = emptyNameEnv
117 go_co (AxiomInstCo _ _ cs) = go_co_s cs
118 go_co (UnivCo p _ ty ty') = go_prov p `plusNameEnv` go ty `plusNameEnv` go ty'
119 go_co (SymCo co) = go_co co
120 go_co (TransCo co co') = go_co co `plusNameEnv` go_co co'
121 go_co (NthCo _ co) = go_co co
122 go_co (LRCo _ co) = go_co co
123 go_co (InstCo co co') = go_co co `plusNameEnv` go_co co'
124 go_co (CoherenceCo co co') = go_co co `plusNameEnv` go_co co'
125 go_co (KindCo co) = go_co co
126 go_co (SubCo co) = go_co co
127 go_co (AxiomRuleCo _ cs) = go_co_s cs
128
129 go_prov UnsafeCoerceProv = emptyNameEnv
130 go_prov (PhantomProv co) = go_co co
131 go_prov (ProofIrrelProv co) = go_co co
132 go_prov (PluginProv _) = emptyNameEnv
133 go_prov (HoleProv _) = emptyNameEnv
134
135 go_tc tc | isTypeSynonymTyCon tc = unitNameEnv (tyConName tc) tc
136 | otherwise = emptyNameEnv
137 go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
138 go_co_s cos = foldr (plusNameEnv . go_co) emptyNameEnv cos
139
140 -- | A monad for type synonym cycle checking, which keeps
141 -- track of the TyCons which are known to be acyclic, or
142 -- a failure message reporting that a cycle was found.
143 newtype SynCycleM a = SynCycleM {
144 runSynCycleM :: SynCycleState -> Either (SrcSpan, SDoc) (a, SynCycleState) }
145
146 type SynCycleState = NameSet
147
148 instance Functor SynCycleM where
149 fmap = liftM
150
151 instance Applicative SynCycleM where
152 pure x = SynCycleM $ \state -> Right (x, state)
153 (<*>) = ap
154
155 instance Monad SynCycleM where
156 m >>= f = SynCycleM $ \state ->
157 case runSynCycleM m state of
158 Right (x, state') ->
159 runSynCycleM (f x) state'
160 Left err -> Left err
161
162 failSynCycleM :: SrcSpan -> SDoc -> SynCycleM ()
163 failSynCycleM loc err = SynCycleM $ \_ -> Left (loc, err)
164
165 -- | Test if a 'Name' is acyclic, short-circuiting if we've
166 -- seen it already.
167 checkNameIsAcyclic :: Name -> SynCycleM () -> SynCycleM ()
168 checkNameIsAcyclic n m = SynCycleM $ \s ->
169 if n `elemNameSet` s
170 then Right ((), s) -- short circuit
171 else case runSynCycleM m s of
172 Right ((), s') -> Right ((), extendNameSet s' n)
173 Left err -> Left err
174
175 -- | Checks if any of the passed in 'TyCon's have cycles.
176 -- Takes the 'UnitId' of the home package (as we can avoid
177 -- checking those TyCons: cycles never go through foreign packages) and
178 -- the corresponding @LTyClDecl Name@ for each 'TyCon', so we
179 -- can give better error messages.
180 checkSynCycles :: UnitId -> [TyCon] -> [LTyClDecl Name] -> TcM ()
181 checkSynCycles this_uid tcs tyclds = do
182 case runSynCycleM (mapM_ (go emptyNameEnv []) tcs) emptyNameEnv of
183 Left (loc, err) -> setSrcSpan loc $ failWithTc err
184 Right _ -> return ()
185 where
186 -- Try our best to print the LTyClDecl for locally defined things
187 lcl_decls = mkNameEnv (zip (map tyConName tcs) tyclds)
188
189 -- Short circuit if we've already seen this Name and concluded
190 -- it was acyclic.
191 go :: NameSet -> [TyCon] -> TyCon -> SynCycleM ()
192 go so_far seen_tcs tc =
193 checkNameIsAcyclic (tyConName tc) $ go' so_far seen_tcs tc
194
195 -- Expand type synonyms, complaining if you find the same
196 -- type synonym a second time.
197 go' :: NameSet -> [TyCon] -> TyCon -> SynCycleM ()
198 go' so_far seen_tcs tc
199 | n `elemNameSet` so_far
200 = failSynCycleM (getSrcSpan (head seen_tcs)) $
201 sep [ text "Cycle in type synonym declarations:"
202 , nest 2 (vcat (map ppr_decl seen_tcs)) ]
203 -- Optimization: we don't allow cycles through external packages,
204 -- so once we find a non-local name we are guaranteed to not
205 -- have a cycle.
206 --
207 -- This won't hold once we get recursive packages with Backpack,
208 -- but for now it's fine.
209 | not (isHoleModule mod ||
210 moduleUnitId mod == this_uid ||
211 isInteractiveModule mod)
212 = return ()
213 | Just ty <- synTyConRhs_maybe tc =
214 go_ty (extendNameSet so_far (tyConName tc)) (tc:seen_tcs) ty
215 | otherwise = return ()
216 where
217 n = tyConName tc
218 mod = nameModule n
219 ppr_decl tc =
220 case lookupNameEnv lcl_decls n of
221 Just (L loc decl) -> ppr loc <> colon <+> ppr decl
222 Nothing -> ppr (getSrcSpan n) <> colon <+> ppr n <+> text "from external module"
223 where
224 n = tyConName tc
225
226 go_ty :: NameSet -> [TyCon] -> Type -> SynCycleM ()
227 go_ty so_far seen_tcs ty =
228 mapM_ (go so_far seen_tcs) (synonymTyConsOfType ty)
229
230 {- Note [Superclass cycle check]
231 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
232 The superclass cycle check for C decides if we can statically
233 guarantee that expanding C's superclass cycles transitively is
234 guaranteed to terminate. This is a Haskell98 requirement,
235 but one that we lift with -XUndecidableSuperClasses.
236
237 The worry is that a superclass cycle could make the type checker loop.
238 More precisely, with a constraint (Given or Wanted)
239 C ty1 .. tyn
240 one approach is to instantiate all of C's superclasses, transitively.
241 We can only do so if that set is finite.
242
243 This potential loop occurs only through superclasses. This, for
244 exmaple, is fine
245 class C a where
246 op :: C b => a -> b -> b
247 even though C's full definition uses C.
248
249 Making the check static also makes it conservative. Eg
250 type family F a
251 class F a => C a
252 Here an instance of (F a) might mention C:
253 type instance F [a] = C a
254 and now we'd have a loop.
255
256 The static check works like this, starting with C
257 * Look at C's superclass predicates
258 * If any is a type-function application,
259 or is headed by a type variable, fail
260 * If any has C at the head, fail
261 * If any has a type class D at the head,
262 make the same test with D
263
264 A tricky point is: what if there is a type variable at the head?
265 Consider this:
266 class f (C f) => C f
267 class c => Id c
268 and now expand superclasses for constraint (C Id):
269 C Id
270 --> Id (C Id)
271 --> C Id
272 --> ....
273 Each step expands superclasses one layer, and clearly does not terminate.
274 -}
275
276 checkClassCycles :: Class -> Maybe SDoc
277 -- Nothing <=> ok
278 -- Just err <=> possible cycle error
279 checkClassCycles cls
280 = do { (definite_cycle, err) <- go (unitNameSet (getName cls))
281 cls (mkTyVarTys (classTyVars cls))
282 ; let herald | definite_cycle = text "Superclass cycle for"
283 | otherwise = text "Potential superclass cycle for"
284 ; return (vcat [ herald <+> quotes (ppr cls)
285 , nest 2 err, hint]) }
286 where
287 hint = text "Use UndecidableSuperClasses to accept this"
288
289 -- Expand superclasses starting with (C a b), complaining
290 -- if you find the same class a second time, or a type function
291 -- or predicate headed by a type variable
292 --
293 -- NB: this code duplicates TcType.transSuperClasses, but
294 -- with more error message generation clobber
295 -- Make sure the two stay in sync.
296 go :: NameSet -> Class -> [Type] -> Maybe (Bool, SDoc)
297 go so_far cls tys = firstJusts $
298 map (go_pred so_far) $
299 immSuperClasses cls tys
300
301 go_pred :: NameSet -> PredType -> Maybe (Bool, SDoc)
302 -- Nothing <=> ok
303 -- Just (True, err) <=> definite cycle
304 -- Just (False, err) <=> possible cycle
305 go_pred so_far pred -- NB: tcSplitTyConApp looks through synonyms
306 | Just (tc, tys) <- tcSplitTyConApp_maybe pred
307 = go_tc so_far pred tc tys
308 | hasTyVarHead pred
309 = Just (False, hang (text "one of whose superclass constraints is headed by a type variable:")
310 2 (quotes (ppr pred)))
311 | otherwise
312 = Nothing
313
314 go_tc :: NameSet -> PredType -> TyCon -> [Type] -> Maybe (Bool, SDoc)
315 go_tc so_far pred tc tys
316 | isFamilyTyCon tc
317 = Just (False, hang (text "one of whose superclass constraints is headed by a type family:")
318 2 (quotes (ppr pred)))
319 | Just cls <- tyConClass_maybe tc
320 = go_cls so_far cls tys
321 | otherwise -- Equality predicate, for example
322 = Nothing
323
324 go_cls :: NameSet -> Class -> [Type] -> Maybe (Bool, SDoc)
325 go_cls so_far cls tys
326 | cls_nm `elemNameSet` so_far
327 = Just (True, text "one of whose superclasses is" <+> quotes (ppr cls))
328 | isCTupleClass cls
329 = go so_far cls tys
330 | otherwise
331 = do { (b,err) <- go (so_far `extendNameSet` cls_nm) cls tys
332 ; return (b, text "one of whose superclasses is" <+> quotes (ppr cls)
333 $$ err) }
334 where
335 cls_nm = getName cls
336
337 {-
338 ************************************************************************
339 * *
340 Role inference
341 * *
342 ************************************************************************
343
344 Note [Role inference]
345 ~~~~~~~~~~~~~~~~~~~~~
346 The role inference algorithm datatype definitions to infer the roles on the
347 parameters. Although these roles are stored in the tycons, we can perform this
348 algorithm on the built tycons, as long as we don't peek at an as-yet-unknown
349 roles field! Ah, the magic of laziness.
350
351 First, we choose appropriate initial roles. For families and classes, roles
352 (including initial roles) are N. For datatypes, we start with the role in the
353 role annotation (if any), or otherwise use Phantom. This is done in
354 initialRoleEnv1.
355
356 The function irGroup then propagates role information until it reaches a
357 fixpoint, preferring N over (R or P) and R over P. To aid in this, we have a
358 monad RoleM, which is a combination reader and state monad. In its state are
359 the current RoleEnv, which gets updated by role propagation, and an update
360 bit, which we use to know whether or not we've reached the fixpoint. The
361 environment of RoleM contains the tycon whose parameters we are inferring, and
362 a VarEnv from parameters to their positions, so we can update the RoleEnv.
363 Between tycons, this reader information is missing; it is added by
364 addRoleInferenceInfo.
365
366 There are two kinds of tycons to consider: algebraic ones (excluding classes)
367 and type synonyms. (Remember, families don't participate -- all their parameters
368 are N.) An algebraic tycon processes each of its datacons, in turn. Note that
369 a datacon's universally quantified parameters might be different from the parent
370 tycon's parameters, so we use the datacon's univ parameters in the mapping from
371 vars to positions. Note also that we don't want to infer roles for existentials
372 (they're all at N, too), so we put them in the set of local variables. As an
373 optimisation, we skip any tycons whose roles are already all Nominal, as there
374 nowhere else for them to go. For synonyms, we just analyse their right-hand sides.
375
376 irType walks through a type, looking for uses of a variable of interest and
377 propagating role information. Because anything used under a phantom position
378 is at phantom and anything used under a nominal position is at nominal, the
379 irType function can assume that anything it sees is at representational. (The
380 other possibilities are pruned when they're encountered.)
381
382 The rest of the code is just plumbing.
383
384 How do we know that this algorithm is correct? It should meet the following
385 specification:
386
387 Let Z be a role context -- a mapping from variables to roles. The following
388 rules define the property (Z |- t : r), where t is a type and r is a role:
389
390 Z(a) = r' r' <= r
391 ------------------------- RCVar
392 Z |- a : r
393
394 ---------- RCConst
395 Z |- T : r -- T is a type constructor
396
397 Z |- t1 : r
398 Z |- t2 : N
399 -------------- RCApp
400 Z |- t1 t2 : r
401
402 forall i<=n. (r_i is R or N) implies Z |- t_i : r_i
403 roles(T) = r_1 .. r_n
404 ---------------------------------------------------- RCDApp
405 Z |- T t_1 .. t_n : R
406
407 Z, a:N |- t : r
408 ---------------------- RCAll
409 Z |- forall a:k.t : r
410
411
412 We also have the following rules:
413
414 For all datacon_i in type T, where a_1 .. a_n are universally quantified
415 and b_1 .. b_m are existentially quantified, and the arguments are t_1 .. t_p,
416 then if forall j<=p, a_1 : r_1 .. a_n : r_n, b_1 : N .. b_m : N |- t_j : R,
417 then roles(T) = r_1 .. r_n
418
419 roles(->) = R, R
420 roles(~#) = N, N
421
422 With -dcore-lint on, the output of this algorithm is checked in checkValidRoles,
423 called from checkValidTycon.
424
425 Note [Role-checking data constructor arguments]
426 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
427 Consider
428 data T a where
429 MkT :: Eq b => F a -> (a->a) -> T (G a)
430
431 Then we want to check the roles at which 'a' is used
432 in MkT's type. We want to work on the user-written type,
433 so we need to take into account
434 * the arguments: (F a) and (a->a)
435 * the context: C a b
436 * the result type: (G a) -- this is in the eq_spec
437
438
439 Note [Coercions in role inference]
440 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
441 Is (t |> co1) representationally equal to (t |> co2)? Of course they are! Changing
442 the kind of a type is totally irrelevant to the representation of that type. So,
443 we want to totally ignore coercions when doing role inference. This includes omitting
444 any type variables that appear in nominal positions but only within coercions.
445 -}
446
447 type RolesInfo = Name -> [Role]
448
449 type RoleEnv = NameEnv [Role] -- from tycon names to roles
450
451 -- This, and any of the functions it calls, must *not* look at the roles
452 -- field of a tycon we are inferring roles about!
453 -- See Note [Role inference]
454 inferRoles :: Bool -> RoleAnnotEnv -> [TyCon] -> Name -> [Role]
455 inferRoles is_boot annots tycons
456 = let role_env = initialRoleEnv is_boot annots tycons
457 role_env' = irGroup role_env tycons in
458 \name -> case lookupNameEnv role_env' name of
459 Just roles -> roles
460 Nothing -> pprPanic "inferRoles" (ppr name)
461
462 initialRoleEnv :: Bool -> RoleAnnotEnv -> [TyCon] -> RoleEnv
463 initialRoleEnv is_boot annots = extendNameEnvList emptyNameEnv .
464 map (initialRoleEnv1 is_boot annots)
465
466 initialRoleEnv1 :: Bool -> RoleAnnotEnv -> TyCon -> (Name, [Role])
467 initialRoleEnv1 is_boot annots_env tc
468 | isFamilyTyCon tc = (name, map (const Nominal) bndrs)
469 | isAlgTyCon tc = (name, default_roles)
470 | isTypeSynonymTyCon tc = (name, default_roles)
471 | otherwise = pprPanic "initialRoleEnv1" (ppr tc)
472 where name = tyConName tc
473 bndrs = tyConBinders tc
474 argflags = map tyConBinderArgFlag bndrs
475 num_exps = count isVisibleArgFlag argflags
476
477 -- if the number of annotations in the role annotation decl
478 -- is wrong, just ignore it. We check this in the validity check.
479 role_annots
480 = case lookupRoleAnnot annots_env name of
481 Just (L _ (RoleAnnotDecl _ annots))
482 | annots `lengthIs` num_exps -> map unLoc annots
483 _ -> replicate num_exps Nothing
484 default_roles = build_default_roles argflags role_annots
485
486 build_default_roles (argf : argfs) (m_annot : ras)
487 | isVisibleArgFlag argf
488 = (m_annot `orElse` default_role) : build_default_roles argfs ras
489 build_default_roles (_argf : argfs) ras
490 = Nominal : build_default_roles argfs ras
491 build_default_roles [] [] = []
492 build_default_roles _ _ = pprPanic "initialRoleEnv1 (2)"
493 (vcat [ppr tc, ppr role_annots])
494
495 default_role
496 | isClassTyCon tc = Nominal
497 | is_boot && isAbstractTyCon tc = Representational
498 | otherwise = Phantom
499
500 irGroup :: RoleEnv -> [TyCon] -> RoleEnv
501 irGroup env tcs
502 = let (env', update) = runRoleM env $ mapM_ irTyCon tcs in
503 if update
504 then irGroup env' tcs
505 else env'
506
507 irTyCon :: TyCon -> RoleM ()
508 irTyCon tc
509 | isAlgTyCon tc
510 = do { old_roles <- lookupRoles tc
511 ; unless (all (== Nominal) old_roles) $ -- also catches data families,
512 -- which don't want or need role inference
513 irTcTyVars tc $
514 do { mapM_ (irType emptyVarSet) (tyConStupidTheta tc) -- See #8958
515 ; whenIsJust (tyConClass_maybe tc) irClass
516 ; mapM_ irDataCon (visibleDataCons $ algTyConRhs tc) }}
517
518 | Just ty <- synTyConRhs_maybe tc
519 = irTcTyVars tc $
520 irType emptyVarSet ty
521
522 | otherwise
523 = return ()
524
525 -- any type variable used in an associated type must be Nominal
526 irClass :: Class -> RoleM ()
527 irClass cls
528 = mapM_ ir_at (classATs cls)
529 where
530 cls_tvs = classTyVars cls
531 cls_tv_set = mkVarSet cls_tvs
532
533 ir_at at_tc
534 = mapM_ (updateRole Nominal) nvars
535 where nvars = filter (`elemVarSet` cls_tv_set) $ tyConTyVars at_tc
536
537 -- See Note [Role inference]
538 irDataCon :: DataCon -> RoleM ()
539 irDataCon datacon
540 = setRoleInferenceVars univ_tvs $
541 irExTyVars ex_tvs $ \ ex_var_set ->
542 mapM_ (irType ex_var_set)
543 (map tyVarKind ex_tvs ++ eqSpecPreds eq_spec ++ theta ++ arg_tys)
544 -- See Note [Role-checking data constructor arguments]
545 where
546 (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
547 = dataConFullSig datacon
548
549 irType :: VarSet -> Type -> RoleM ()
550 irType = go
551 where
552 go lcls (TyVarTy tv) = unless (tv `elemVarSet` lcls) $
553 updateRole Representational tv
554 go lcls (AppTy t1 t2) = go lcls t1 >> markNominal lcls t2
555 go lcls (TyConApp tc tys) = do { roles <- lookupRolesX tc
556 ; zipWithM_ (go_app lcls) roles tys }
557 go lcls (ForAllTy tvb ty) = do { let tv = binderVar tvb
558 lcls' = extendVarSet lcls tv
559 ; markNominal lcls (tyVarKind tv)
560 ; go lcls' ty }
561 go lcls (FunTy arg res) = go lcls arg >> go lcls res
562 go _ (LitTy {}) = return ()
563 -- See Note [Coercions in role inference]
564 go lcls (CastTy ty _) = go lcls ty
565 go _ (CoercionTy _) = return ()
566
567 go_app _ Phantom _ = return () -- nothing to do here
568 go_app lcls Nominal ty = markNominal lcls ty -- all vars below here are N
569 go_app lcls Representational ty = go lcls ty
570
571 irTcTyVars :: TyCon -> RoleM a -> RoleM a
572 irTcTyVars tc thing
573 = setRoleInferenceTc (tyConName tc) $ go (tyConTyVars tc)
574 where
575 go [] = thing
576 go (tv:tvs) = do { markNominal emptyVarSet (tyVarKind tv)
577 ; addRoleInferenceVar tv $ go tvs }
578
579 irExTyVars :: [TyVar] -> (TyVarSet -> RoleM a) -> RoleM a
580 irExTyVars orig_tvs thing = go emptyVarSet orig_tvs
581 where
582 go lcls [] = thing lcls
583 go lcls (tv:tvs) = do { markNominal lcls (tyVarKind tv)
584 ; go (extendVarSet lcls tv) tvs }
585
586 markNominal :: TyVarSet -- local variables
587 -> Type -> RoleM ()
588 markNominal lcls ty = let nvars = fvVarList (FV.delFVs lcls $ get_ty_vars ty) in
589 mapM_ (updateRole Nominal) nvars
590 where
591 -- get_ty_vars gets all the tyvars (no covars!) from a type *without*
592 -- recurring into coercions. Recall: coercions are totally ignored during
593 -- role inference. See [Coercions in role inference]
594 get_ty_vars :: Type -> FV
595 get_ty_vars (TyVarTy tv) = unitFV tv
596 get_ty_vars (AppTy t1 t2) = get_ty_vars t1 `unionFV` get_ty_vars t2
597 get_ty_vars (FunTy t1 t2) = get_ty_vars t1 `unionFV` get_ty_vars t2
598 get_ty_vars (TyConApp _ tys) = mapUnionFV get_ty_vars tys
599 get_ty_vars (ForAllTy tvb ty) = tyCoFVsBndr tvb (get_ty_vars ty)
600 get_ty_vars (LitTy {}) = emptyFV
601 get_ty_vars (CastTy ty _) = get_ty_vars ty
602 get_ty_vars (CoercionTy _) = emptyFV
603
604 -- like lookupRoles, but with Nominal tags at the end for oversaturated TyConApps
605 lookupRolesX :: TyCon -> RoleM [Role]
606 lookupRolesX tc
607 = do { roles <- lookupRoles tc
608 ; return $ roles ++ repeat Nominal }
609
610 -- gets the roles either from the environment or the tycon
611 lookupRoles :: TyCon -> RoleM [Role]
612 lookupRoles tc
613 = do { env <- getRoleEnv
614 ; case lookupNameEnv env (tyConName tc) of
615 Just roles -> return roles
616 Nothing -> return $ tyConRoles tc }
617
618 -- tries to update a role; won't ever update a role "downwards"
619 updateRole :: Role -> TyVar -> RoleM ()
620 updateRole role tv
621 = do { var_ns <- getVarNs
622 ; name <- getTyConName
623 ; case lookupVarEnv var_ns tv of
624 Nothing -> pprPanic "updateRole" (ppr name $$ ppr tv $$ ppr var_ns)
625 Just n -> updateRoleEnv name n role }
626
627 -- the state in the RoleM monad
628 data RoleInferenceState = RIS { role_env :: RoleEnv
629 , update :: Bool }
630
631 -- the environment in the RoleM monad
632 type VarPositions = VarEnv Int
633
634 -- See [Role inference]
635 newtype RoleM a = RM { unRM :: Maybe Name -- of the tycon
636 -> VarPositions
637 -> Int -- size of VarPositions
638 -> RoleInferenceState
639 -> (a, RoleInferenceState) }
640
641 instance Functor RoleM where
642 fmap = liftM
643
644 instance Applicative RoleM where
645 pure x = RM $ \_ _ _ state -> (x, state)
646 (<*>) = ap
647
648 instance Monad RoleM where
649 a >>= f = RM $ \m_info vps nvps state ->
650 let (a', state') = unRM a m_info vps nvps state in
651 unRM (f a') m_info vps nvps state'
652
653 runRoleM :: RoleEnv -> RoleM () -> (RoleEnv, Bool)
654 runRoleM env thing = (env', update)
655 where RIS { role_env = env', update = update }
656 = snd $ unRM thing Nothing emptyVarEnv 0 state
657 state = RIS { role_env = env
658 , update = False }
659
660 setRoleInferenceTc :: Name -> RoleM a -> RoleM a
661 setRoleInferenceTc name thing = RM $ \m_name vps nvps state ->
662 ASSERT( isNothing m_name )
663 ASSERT( isEmptyVarEnv vps )
664 ASSERT( nvps == 0 )
665 unRM thing (Just name) vps nvps state
666
667 addRoleInferenceVar :: TyVar -> RoleM a -> RoleM a
668 addRoleInferenceVar tv thing
669 = RM $ \m_name vps nvps state ->
670 ASSERT( isJust m_name )
671 unRM thing m_name (extendVarEnv vps tv nvps) (nvps+1) state
672
673 setRoleInferenceVars :: [TyVar] -> RoleM a -> RoleM a
674 setRoleInferenceVars tvs thing
675 = RM $ \m_name _vps _nvps state ->
676 ASSERT( isJust m_name )
677 unRM thing m_name (mkVarEnv (zip tvs [0..])) (panic "setRoleInferenceVars")
678 state
679
680 getRoleEnv :: RoleM RoleEnv
681 getRoleEnv = RM $ \_ _ _ state@(RIS { role_env = env }) -> (env, state)
682
683 getVarNs :: RoleM VarPositions
684 getVarNs = RM $ \_ vps _ state -> (vps, state)
685
686 getTyConName :: RoleM Name
687 getTyConName = RM $ \m_name _ _ state ->
688 case m_name of
689 Nothing -> panic "getTyConName"
690 Just name -> (name, state)
691
692 updateRoleEnv :: Name -> Int -> Role -> RoleM ()
693 updateRoleEnv name n role
694 = RM $ \_ _ _ state@(RIS { role_env = role_env }) -> ((),
695 case lookupNameEnv role_env name of
696 Nothing -> pprPanic "updateRoleEnv" (ppr name)
697 Just roles -> let (before, old_role : after) = splitAt n roles in
698 if role `ltRole` old_role
699 then let roles' = before ++ role : after
700 role_env' = extendNameEnv role_env name roles' in
701 RIS { role_env = role_env', update = True }
702 else state )
703
704
705 {- *********************************************************************
706 * *
707 Building implicits
708 * *
709 ********************************************************************* -}
710
711 tcAddImplicits :: [TyCon] -> TcM TcGblEnv
712 -- Given a [TyCon], add to the TcGblEnv
713 -- * extend the TypeEnv with their implicitTyThings
714 -- * extend the TypeEnv with any default method Ids
715 -- * add bindings for record selectors
716 -- * add bindings for type representations for the TyThings
717 tcAddImplicits tycons
718 = discardWarnings $
719 tcExtendGlobalEnvImplicit implicit_things $
720 tcExtendGlobalValEnv def_meth_ids $
721 do { traceTc "tcAddImplicits" $ vcat
722 [ text "tycons" <+> ppr tycons
723 , text "implicits" <+> ppr implicit_things ]
724 ; tcRecSelBinds (mkRecSelBinds tycons) }
725 where
726 implicit_things = concatMap implicitTyConThings tycons
727 def_meth_ids = mkDefaultMethodIds tycons
728
729 mkDefaultMethodIds :: [TyCon] -> [Id]
730 -- We want to put the default-method Ids (both vanilla and generic)
731 -- into the type environment so that they are found when we typecheck
732 -- the filled-in default methods of each instance declaration
733 -- See Note [Default method Ids and Template Haskell]
734 mkDefaultMethodIds tycons
735 = [ mkExportedVanillaId dm_name (mkDefaultMethodType cls sel_id dm_spec)
736 | tc <- tycons
737 , Just cls <- [tyConClass_maybe tc]
738 , (sel_id, Just (dm_name, dm_spec)) <- classOpItems cls ]
739
740 mkDefaultMethodType :: Class -> Id -> DefMethSpec Type -> Type
741 -- Returns the top-level type of the default method
742 mkDefaultMethodType _ sel_id VanillaDM = idType sel_id
743 mkDefaultMethodType cls _ (GenericDM dm_ty) = mkSpecSigmaTy cls_tvs [pred] dm_ty
744 where
745 cls_tvs = classTyVars cls
746 pred = mkClassPred cls (mkTyVarTys cls_tvs)
747
748 {-
749 ************************************************************************
750 * *
751 Building record selectors
752 * *
753 ************************************************************************
754 -}
755
756 {-
757 Note [Default method Ids and Template Haskell]
758 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
759 Consider this (Trac #4169):
760 class Numeric a where
761 fromIntegerNum :: a
762 fromIntegerNum = ...
763
764 ast :: Q [Dec]
765 ast = [d| instance Numeric Int |]
766
767 When we typecheck 'ast' we have done the first pass over the class decl
768 (in tcTyClDecls), but we have not yet typechecked the default-method
769 declarations (because they can mention value declarations). So we
770 must bring the default method Ids into scope first (so they can be seen
771 when typechecking the [d| .. |] quote, and typecheck them later.
772 -}
773
774 {-
775 ************************************************************************
776 * *
777 Building record selectors
778 * *
779 ************************************************************************
780 -}
781
782 mkRecSelBinds :: [TyCon] -> HsValBinds Name
783 -- NB We produce *un-typechecked* bindings, rather like 'deriving'
784 -- This makes life easier, because the later type checking will add
785 -- all necessary type abstractions and applications
786 mkRecSelBinds tycons
787 = ValBindsOut binds sigs
788 where
789 (sigs, binds) = unzip rec_sels
790 rec_sels = map mkRecSelBind [ (tc,fld)
791 | tc <- tycons
792 , fld <- tyConFieldLabels tc ]
793
794 mkRecSelBind :: (TyCon, FieldLabel) -> (LSig Name, (RecFlag, LHsBinds Name))
795 mkRecSelBind (tycon, fl)
796 = mkOneRecordSelector all_cons (RecSelData tycon) fl
797 where
798 all_cons = map RealDataCon (tyConDataCons tycon)
799
800 mkOneRecordSelector :: [ConLike] -> RecSelParent -> FieldLabel
801 -> (LSig Name, (RecFlag, LHsBinds Name))
802 mkOneRecordSelector all_cons idDetails fl
803 = (L loc (IdSig sel_id), (NonRecursive, unitBag (L loc sel_bind)))
804 where
805 loc = getSrcSpan sel_name
806 lbl = flLabel fl
807 sel_name = flSelector fl
808
809 sel_id = mkExportedLocalId rec_details sel_name sel_ty
810 rec_details = RecSelId { sel_tycon = idDetails, sel_naughty = is_naughty }
811
812 -- Find a representative constructor, con1
813 cons_w_field = conLikesWithFields all_cons [lbl]
814 con1 = ASSERT( not (null cons_w_field) ) head cons_w_field
815
816 -- Selector type; Note [Polymorphic selectors]
817 field_ty = conLikeFieldType con1 lbl
818 data_tvs = tyCoVarsOfTypeWellScoped data_ty
819 data_tv_set= mkVarSet data_tvs
820 is_naughty = not (tyCoVarsOfType field_ty `subVarSet` data_tv_set)
821 (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty
822 sel_ty | is_naughty = unitTy -- See Note [Naughty record selectors]
823 | otherwise = mkSpecForAllTys data_tvs $
824 mkPhiTy (conLikeStupidTheta con1) $ -- Urgh!
825 mkFunTy data_ty $
826 mkSpecForAllTys field_tvs $
827 mkPhiTy field_theta $
828 -- req_theta is empty for normal DataCon
829 mkPhiTy req_theta $
830 field_tau
831
832 -- Make the binding: sel (C2 { fld = x }) = x
833 -- sel (C7 { fld = x }) = x
834 -- where cons_w_field = [C2,C7]
835 sel_bind = mkTopFunBind Generated sel_lname alts
836 where
837 alts | is_naughty = [mkSimpleMatch (FunRhs sel_lname Prefix)
838 [] unit_rhs]
839 | otherwise = map mk_match cons_w_field ++ deflt
840 mk_match con = mkSimpleMatch (FunRhs sel_lname Prefix)
841 [L loc (mk_sel_pat con)]
842 (L loc (HsVar (L loc field_var)))
843 mk_sel_pat con = ConPatIn (L loc (getName con)) (RecCon rec_fields)
844 rec_fields = HsRecFields { rec_flds = [rec_field], rec_dotdot = Nothing }
845 rec_field = noLoc (HsRecField
846 { hsRecFieldLbl
847 = L loc (FieldOcc (L loc $ mkVarUnqual lbl) sel_name)
848 , hsRecFieldArg = L loc (VarPat (L loc field_var))
849 , hsRecPun = False })
850 sel_lname = L loc sel_name
851 field_var = mkInternalName (mkBuiltinUnique 1) (getOccName sel_name) loc
852
853 -- Add catch-all default case unless the case is exhaustive
854 -- We do this explicitly so that we get a nice error message that
855 -- mentions this particular record selector
856 deflt | all dealt_with all_cons = []
857 | otherwise = [mkSimpleMatch CaseAlt
858 [L loc (WildPat placeHolderType)]
859 (mkHsApp (L loc (HsVar
860 (L loc (getName rEC_SEL_ERROR_ID))))
861 (L loc (HsLit msg_lit)))]
862
863 -- Do not add a default case unless there are unmatched
864 -- constructors. We must take account of GADTs, else we
865 -- get overlap warning messages from the pattern-match checker
866 -- NB: we need to pass type args for the *representation* TyCon
867 -- to dataConCannotMatch, hence the calculation of inst_tys
868 -- This matters in data families
869 -- data instance T Int a where
870 -- A :: { fld :: Int } -> T Int Bool
871 -- B :: { fld :: Int } -> T Int Char
872 dealt_with :: ConLike -> Bool
873 dealt_with (PatSynCon _) = False -- We can't predict overlap
874 dealt_with con@(RealDataCon dc) =
875 con `elem` cons_w_field || dataConCannotMatch inst_tys dc
876
877 (univ_tvs, _, eq_spec, _, req_theta, _, data_ty) = conLikeFullSig con1
878
879 eq_subst = mkTvSubstPrs (map eqSpecPair eq_spec)
880 inst_tys = substTyVars eq_subst univ_tvs
881
882 unit_rhs = mkLHsTupleExpr []
883 msg_lit = HsStringPrim NoSourceText (fastStringToByteString lbl)
884
885 {-
886 Note [Polymorphic selectors]
887 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
888 We take care to build the type of a polymorphic selector in the right
889 order, so that visible type application works.
890
891 data Ord a => T a = MkT { field :: forall b. (Num a, Show b) => (a, b) }
892
893 We want
894
895 field :: forall a. Ord a => T a -> forall b. (Num a, Show b) => (a, b)
896
897 Note [Naughty record selectors]
898 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
899 A "naughty" field is one for which we can't define a record
900 selector, because an existential type variable would escape. For example:
901 data T = forall a. MkT { x,y::a }
902 We obviously can't define
903 x (MkT v _) = v
904 Nevertheless we *do* put a RecSelId into the type environment
905 so that if the user tries to use 'x' as a selector we can bleat
906 helpfully, rather than saying unhelpfully that 'x' is not in scope.
907 Hence the sel_naughty flag, to identify record selectors that don't really exist.
908
909 In general, a field is "naughty" if its type mentions a type variable that
910 isn't in the result type of the constructor. Note that this *allows*
911 GADT record selectors (Note [GADT record selectors]) whose types may look
912 like sel :: T [a] -> a
913
914 For naughty selectors we make a dummy binding
915 sel = ()
916 so that the later type-check will add them to the environment, and they'll be
917 exported. The function is never called, because the typechecker spots the
918 sel_naughty field.
919
920 Note [GADT record selectors]
921 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
922 For GADTs, we require that all constructors with a common field 'f' have the same
923 result type (modulo alpha conversion). [Checked in TcTyClsDecls.checkValidTyCon]
924 E.g.
925 data T where
926 T1 { f :: Maybe a } :: T [a]
927 T2 { f :: Maybe a, y :: b } :: T [a]
928 T3 :: T Int
929
930 and now the selector takes that result type as its argument:
931 f :: forall a. T [a] -> Maybe a
932
933 Details: the "real" types of T1,T2 are:
934 T1 :: forall r a. (r~[a]) => a -> T r
935 T2 :: forall r a b. (r~[a]) => a -> b -> T r
936
937 So the selector loooks like this:
938 f :: forall a. T [a] -> Maybe a
939 f (a:*) (t:T [a])
940 = case t of
941 T1 c (g:[a]~[c]) (v:Maybe c) -> v `cast` Maybe (right (sym g))
942 T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g))
943 T3 -> error "T3 does not have field f"
944
945 Note the forall'd tyvars of the selector are just the free tyvars
946 of the result type; there may be other tyvars in the constructor's
947 type (e.g. 'b' in T2).
948
949 Note the need for casts in the result!
950
951 Note [Selector running example]
952 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
953 It's OK to combine GADTs and type families. Here's a running example:
954
955 data instance T [a] where
956 T1 { fld :: b } :: T [Maybe b]
957
958 The representation type looks like this
959 data :R7T a where
960 T1 { fld :: b } :: :R7T (Maybe b)
961
962 and there's coercion from the family type to the representation type
963 :CoR7T a :: T [a] ~ :R7T a
964
965 The selector we want for fld looks like this:
966
967 fld :: forall b. T [Maybe b] -> b
968 fld = /\b. \(d::T [Maybe b]).
969 case d `cast` :CoR7T (Maybe b) of
970 T1 (x::b) -> x
971
972 The scrutinee of the case has type :R7T (Maybe b), which can be
973 gotten by appying the eq_spec to the univ_tvs of the data con.
974
975 -}