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