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