a1c3d43f2a7652584b94a64536476cd813de1264
[ghc.git] / compiler / typecheck / TcTyClsDecls.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The AQUA Project, Glasgow University, 1996-1998
4
5
6 TcTyClsDecls: Typecheck type and class declarations
7 -}
8
9 {-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
10 {-# LANGUAGE TypeFamilies #-}
11
12 module TcTyClsDecls (
13 tcTyAndClassDecls,
14
15 -- Functions used by TcInstDcls to check
16 -- data/type family instance declarations
17 kcDataDefn, tcConDecls, dataDeclChecks, checkValidTyCon,
18 tcFamTyPats, tcTyFamInstEqn,
19 tcAddTyFamInstCtxt, tcMkDataFamInstCtxt, tcAddDataFamInstCtxt,
20 wrongKindOfFamily, dataConCtxt
21 ) where
22
23 #include "HsVersions.h"
24
25 import GhcPrelude
26
27 import HsSyn
28 import HscTypes
29 import BuildTyCl
30 import TcRnMonad
31 import TcEnv
32 import TcValidity
33 import TcHsSyn
34 import TcTyDecls
35 import TcClassDcl
36 import {-# SOURCE #-} TcInstDcls( tcInstDecls1 )
37 import TcDeriv (DerivInfo)
38 import TcEvidence ( tcCoercionKind, isEmptyTcEvBinds )
39 import TcUnify ( checkConstraints )
40 import TcHsType
41 import TcMType
42 import TysWiredIn ( unitTy )
43 import TcType
44 import RnEnv( lookupConstructorFields )
45 import FamInst
46 import FamInstEnv
47 import Coercion
48 import Type
49 import TyCoRep -- for checkValidRoles
50 import Kind
51 import Class
52 import CoAxiom
53 import TyCon
54 import DataCon
55 import Id
56 import Var
57 import VarEnv
58 import VarSet
59 import Module
60 import Name
61 import NameSet
62 import NameEnv
63 import Outputable
64 import Maybes
65 import Unify
66 import Util
67 import Pair
68 import SrcLoc
69 import ListSetOps
70 import DynFlags
71 import Unique
72 import ConLike( ConLike(..) )
73 import BasicTypes
74 import qualified GHC.LanguageExtensions as LangExt
75
76 import Control.Monad
77 import Data.List
78 import Data.List.NonEmpty ( NonEmpty(..) )
79
80 {-
81 ************************************************************************
82 * *
83 \subsection{Type checking for type and class declarations}
84 * *
85 ************************************************************************
86
87 Note [Grouping of type and class declarations]
88 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
89 tcTyAndClassDecls is called on a list of `TyClGroup`s. Each group is a strongly
90 connected component of mutually dependent types and classes. We kind check and
91 type check each group separately to enhance kind polymorphism. Take the
92 following example:
93
94 type Id a = a
95 data X = X (Id Int)
96
97 If we were to kind check the two declarations together, we would give Id the
98 kind * -> *, since we apply it to an Int in the definition of X. But we can do
99 better than that, since Id really is kind polymorphic, and should get kind
100 forall (k::*). k -> k. Since it does not depend on anything else, it can be
101 kind-checked by itself, hence getting the most general kind. We then kind check
102 X, which works fine because we then know the polymorphic kind of Id, and simply
103 instantiate k to *.
104
105 Note [Check role annotations in a second pass]
106 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
107 Role inference potentially depends on the types of all of the datacons declared
108 in a mutually recursive group. The validity of a role annotation, in turn,
109 depends on the result of role inference. Because the types of datacons might
110 be ill-formed (see #7175 and Note [Checking GADT return types]) we must check
111 *all* the tycons in a group for validity before checking *any* of the roles.
112 Thus, we take two passes over the resulting tycons, first checking for general
113 validity and then checking for valid role annotations.
114 -}
115
116 tcTyAndClassDecls :: [TyClGroup GhcRn] -- Mutually-recursive groups in
117 -- dependency order
118 -> TcM ( TcGblEnv -- Input env extended by types and
119 -- classes
120 -- and their implicit Ids,DataCons
121 , [InstInfo GhcRn] -- Source-code instance decls info
122 , [DerivInfo] -- data family deriving info
123 )
124 -- Fails if there are any errors
125 tcTyAndClassDecls tyclds_s
126 -- The code recovers internally, but if anything gave rise to
127 -- an error we'd better stop now, to avoid a cascade
128 -- Type check each group in dependency order folding the global env
129 = checkNoErrs $ fold_env [] [] tyclds_s
130 where
131 fold_env :: [InstInfo GhcRn]
132 -> [DerivInfo]
133 -> [TyClGroup GhcRn]
134 -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
135 fold_env inst_info deriv_info []
136 = do { gbl_env <- getGblEnv
137 ; return (gbl_env, inst_info, deriv_info) }
138 fold_env inst_info deriv_info (tyclds:tyclds_s)
139 = do { (tcg_env, inst_info', deriv_info') <- tcTyClGroup tyclds
140 ; setGblEnv tcg_env $
141 -- remaining groups are typechecked in the extended global env.
142 fold_env (inst_info' ++ inst_info)
143 (deriv_info' ++ deriv_info)
144 tyclds_s }
145
146 tcTyClGroup :: TyClGroup GhcRn
147 -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
148 -- Typecheck one strongly-connected component of type, class, and instance decls
149 -- See Note [TyClGroups and dependency analysis] in HsDecls
150 tcTyClGroup (TyClGroup { group_tyclds = tyclds
151 , group_roles = roles
152 , group_instds = instds })
153 = do { let role_annots = mkRoleAnnotEnv roles
154
155 -- Step 1: Typecheck the type/class declarations
156 ; traceTc "---- tcTyClGroup ---- {" empty
157 ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds))
158 ; tyclss <- tcTyClDecls tyclds role_annots
159
160 -- Step 1.5: Make sure we don't have any type synonym cycles
161 ; traceTc "Starting synonym cycle check" (ppr tyclss)
162 ; this_uid <- fmap thisPackage getDynFlags
163 ; checkSynCycles this_uid tyclss tyclds
164 ; traceTc "Done synonym cycle check" (ppr tyclss)
165
166 -- Step 2: Perform the validity check on those types/classes
167 -- We can do this now because we are done with the recursive knot
168 -- Do it before Step 3 (adding implicit things) because the latter
169 -- expects well-formed TyCons
170 ; traceTc "Starting validity check" (ppr tyclss)
171 ; tyclss <- concatMapM checkValidTyCl tyclss
172 ; traceTc "Done validity check" (ppr tyclss)
173 ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
174 -- See Note [Check role annotations in a second pass]
175
176 ; traceTc "---- end tcTyClGroup ---- }" empty
177
178 -- Step 3: Add the implicit things;
179 -- we want them in the environment because
180 -- they may be mentioned in interface files
181 ; gbl_env <- addTyConsToGblEnv tyclss
182
183 -- Step 4: check instance declarations
184 ; setGblEnv gbl_env $
185 tcInstDecls1 instds }
186
187 tcTyClGroup (XTyClGroup _) = panic "tcTyClGroup"
188
189 tcTyClDecls :: [LTyClDecl GhcRn] -> RoleAnnotEnv -> TcM [TyCon]
190 tcTyClDecls tyclds role_annots
191 = tcExtendKindEnv promotion_err_env $ --- See Note [Type environment evolution]
192 do { -- Step 1: kind-check this group and returns the final
193 -- (possibly-polymorphic) kind of each TyCon and Class
194 -- See Note [Kind checking for type and class decls]
195 tc_tycons <- kcTyClGroup tyclds
196 ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons))
197
198 -- Step 2: type-check all groups together, returning
199 -- the final TyCons and Classes
200 --
201 -- NB: We have to be careful here to NOT eagerly unfold
202 -- type synonyms, as we have not tested for type synonym
203 -- loops yet and could fall into a black hole.
204 ; fixM $ \ ~rec_tyclss -> do
205 { tcg_env <- getGblEnv
206 ; let roles = inferRoles (tcg_src tcg_env) role_annots rec_tyclss
207
208 -- Populate environment with knot-tied ATyCon for TyCons
209 -- NB: if the decls mention any ill-staged data cons
210 -- (see Note [Recursion and promoting data constructors])
211 -- we will have failed already in kcTyClGroup, so no worries here
212 ; tcExtendRecEnv (zipRecTyClss tc_tycons rec_tyclss) $
213
214 -- Also extend the local type envt with bindings giving
215 -- the (polymorphic) kind of each knot-tied TyCon or Class
216 -- See Note [Type checking recursive type and class declarations]
217 -- and Note [Type environment evolution]
218 tcExtendKindEnvWithTyCons tc_tycons $
219
220 -- Kind and type check declarations for this group
221 mapM (tcTyClDecl roles) tyclds
222 } }
223 where
224 promotion_err_env = mkPromotionErrorEnv tyclds
225 ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma
226 , ppr (tyConBinders tc) <> comma
227 , ppr (tyConResKind tc) ])
228
229 zipRecTyClss :: [TcTyCon]
230 -> [TyCon] -- Knot-tied
231 -> [(Name,TyThing)]
232 -- Build a name-TyThing mapping for the TyCons bound by decls
233 -- being careful not to look at the knot-tied [TyThing]
234 -- The TyThings in the result list must have a visible ATyCon,
235 -- because typechecking types (in, say, tcTyClDecl) looks at
236 -- this outer constructor
237 zipRecTyClss tc_tycons rec_tycons
238 = [ (name, ATyCon (get name)) | tc_tycon <- tc_tycons, let name = getName tc_tycon ]
239 where
240 rec_tc_env :: NameEnv TyCon
241 rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
242
243 add_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
244 add_tc tc env = foldr add_one_tc env (tc : tyConATs tc)
245
246 add_one_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
247 add_one_tc tc env = extendNameEnv env (tyConName tc) tc
248
249 get name = case lookupNameEnv rec_tc_env name of
250 Just tc -> tc
251 other -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
252
253 {-
254 ************************************************************************
255 * *
256 Kind checking
257 * *
258 ************************************************************************
259
260 Note [Kind checking for type and class decls]
261 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
262 Kind checking is done thus:
263
264 1. Make up a kind variable for each parameter of the declarations,
265 and extend the kind environment (which is in the TcLclEnv)
266
267 2. Kind check the declarations
268
269 We need to kind check all types in the mutually recursive group
270 before we know the kind of the type variables. For example:
271
272 class C a where
273 op :: D b => a -> b -> b
274
275 class D c where
276 bop :: (Monad c) => ...
277
278 Here, the kind of the locally-polymorphic type variable "b"
279 depends on *all the uses of class D*. For example, the use of
280 Monad c in bop's type signature means that D must have kind Type->Type.
281
282 Note: we don't treat type synonyms specially (we used to, in the past);
283 in particular, even if we have a type synonym cycle, we still kind check
284 it normally, and test for cycles later (checkSynCycles). The reason
285 we can get away with this is because we have more systematic TYPE r
286 inference, which means that we can do unification between kinds that
287 aren't lifted (this historically was not true.)
288
289 The downside of not directly reading off the kinds off the RHS of
290 type synonyms in topological order is that we don't transparently
291 support making synonyms of types with higher-rank kinds. But
292 you can always specify a CUSK directly to make this work out.
293 See tc269 for an example.
294
295 Note [Skip decls with CUSKs in kcLTyClDecl]
296 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
297 Consider
298
299 data T (a :: *) = MkT (S a) -- Has CUSK
300 data S a = MkS (T Int) (S a) -- No CUSK
301
302 Via getInitialKinds we get
303 T :: * -> *
304 S :: kappa -> *
305
306 Then we call kcTyClDecl on each decl in the group, to constrain the
307 kind unification variables. BUT we /skip/ the RHS of any decl with
308 a CUSK. Here we skip the RHS of T, so we eventually get
309 S :: forall k. k -> *
310
311 This gets us more polymorphism than we would otherwise get, similar
312 (but implemented strangely differently from) the treatment of type
313 signatures in value declarations.
314
315 Open type families
316 ~~~~~~~~~~~~~~~~~~
317 This treatment of type synonyms only applies to Haskell 98-style synonyms.
318 General type functions can be recursive, and hence, appear in `alg_decls'.
319
320 The kind of an open type family is solely determinded by its kind signature;
321 hence, only kind signatures participate in the construction of the initial
322 kind environment (as constructed by `getInitialKind'). In fact, we ignore
323 instances of families altogether in the following. However, we need to include
324 the kinds of *associated* families into the construction of the initial kind
325 environment. (This is handled by `allDecls').
326
327 See also Note [Kind checking recursive type and class declarations]
328
329 Note [How TcTyCons work]
330 ~~~~~~~~~~~~~~~~~~~~~~~~
331 TcTyCons are used for two distinct purposes
332
333 1. When recovering from a type error in a type declaration,
334 we want to put the erroneous TyCon in the environment in a
335 way that won't lead to more errors. We use a TcTyCon for this;
336 see makeRecoveryTyCon.
337
338 2. When checking a type/class declaration (in module TcTyClsDecls), we come
339 upon knowledge of the eventual tycon in bits and pieces.
340
341 S1) First, we use getInitialKinds to look over the user-provided
342 kind signature of a tycon (including, for example, the number
343 of parameters written to the tycon) to get an initial shape of
344 the tycon's kind. We record that shape in a TcTyCon.
345
346 S2) Then, using these initial kinds, we kind-check the body of the
347 tycon (class methods, data constructors, etc.), filling in the
348 metavariables in the tycon's initial kind.
349
350 S3) We then generalize to get the tycon's final, fixed
351 kind. Finally, once this has happened for all tycons in a
352 mutually recursive group, we can desugar the lot.
353
354 For convenience, we store partially-known tycons in TcTyCons, which
355 might store meta-variables. These TcTyCons are stored in the local
356 environment in TcTyClsDecls, until the real full TyCons can be created
357 during desugaring. A desugared program should never have a TcTyCon.
358
359 A challenging piece in all of this is that we end up taking three separate
360 passes over every declaration:
361 - one in getInitialKind (this pass look only at the head, not the body)
362 - one in kcTyClDecls (to kind-check the body)
363 - a final one in tcTyClDecls (to desugar)
364 In the latter two passes, we need to connect the user-written type
365 variables in an LHsQTyVars with the variables in the tycon's
366 inferred kind. Because the tycon might not have a CUSK, this
367 matching up is, in general, quite hard to do. (Look through the
368 git history between Dec 2015 and Apr 2016 for
369 TcHsType.splitTelescopeTvs!) Instead of trying, we just store the
370 list of type variables to bring into scope, in the
371 tyConScopedTyVars field of the TcTyCon. These tyvars are brought
372 into scope in kcTyClTyVars and tcTyClTyVars, both in TcHsType.
373
374 In a TcTyCon, everything is zonked after the kind-checking pass (S2).
375
376 Note [Check telescope again during generalisation]
377 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
378 The telescope check before kind generalisation is useful to catch something
379 like this:
380
381 data T a k = MkT (Proxy (a :: k))
382
383 Clearly, the k has to come first. Checking for this problem must come before
384 kind generalisation, as described in Note [Bad telescopes] in
385 TcValidity.
386
387 However, we have to check again *after* kind generalisation, to catch something
388 like this:
389
390 data SameKind :: k -> k -> Type -- to force unification
391 data S a (b :: a) (d :: SameKind c b)
392
393 Note that c has no explicit binding site. As such, it's quantified by kind
394 generalisation. (Note that kcHsTyVarBndrs does not return such variables
395 as binders in its returned TcTyCon.) The user-written part of this telescope
396 is well-ordered; no earlier variables depend on later ones. However, after
397 kind generalisation, we put c up front, like so:
398
399 data S {c :: a} a (b :: a) (d :: SameKind c b)
400
401 We now have a problem. We could detect this problem just by looking at the
402 free vars of the kinds of the generalised variables (the kvs), but we get
403 such a nice error message out of checkValidTelescope that it seems like the
404 right thing to do.
405
406 Note [Type environment evolution]
407 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
408 As we typecheck a group of declarations the type environment evolves.
409 Consider for example:
410 data B (a :: Type) = MkB (Proxy 'MkB)
411
412 We do the following steps:
413
414 1. Start of tcTyClDecls: use mkPromotionErrorEnv to initialise the
415 type env with promotion errors
416 B :-> TyConPE
417 MkB :-> DataConPE
418
419 2. kcTyCLGruup
420 - Do getInitialKinds, which will signal a promotion
421 error if B is used in any of the kinds needed to initialse
422 B's kind (e.g. (a :: Type)) here
423
424 - Extend the type env with these initial kinds (monomorphic for
425 decls that lack a CUSK)
426 B :-> TcTyCon <initial kind>
427 (thereby overriding the B :-> TyConPE binding)
428 and do kcLTyClDecl on each decl to get equality constraints on
429 all those inital kinds
430
431 - Generalise the inital kind, making a poly-kinded TcTyCon
432
433 3. Back in tcTyDecls, extend the envt with bindings of the poly-kinded
434 TcTyCons, again overriding the promotion-error bindings.
435
436 But note that the data constructor promotion errors are still in place
437 so that (in our example) a use of MkB will sitll be signalled as
438 an error.
439
440 4. Typecheck the decls.
441
442 5. In tcTyClGroup, extend the envt with bindings for TyCon and DataCons
443
444
445 Note [Missed opportunity to retain higher-rank kinds]
446 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
447 In 'kcTyClGroup', there is a missed opportunity to make kind
448 inference work in a few more cases. The idea is analogous
449 to Note [Single function non-recursive binding special-case]:
450
451 * If we have an SCC with a single decl, which is non-recursive,
452 instead of creating a unification variable representing the
453 kind of the decl and unifying it with the rhs, we can just
454 read the type directly of the rhs.
455
456 * Furthermore, we can update our SCC analysis to ignore
457 dependencies on declarations which have CUSKs: we don't
458 have to kind-check these all at once, since we can use
459 the CUSK to initialize the kind environment.
460
461 Unfortunately this requires reworking a bit of the code in
462 'kcLTyClDecl' so I've decided to punt unless someone shouts about it.
463 -}
464
465 kcTyClGroup :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
466
467 -- Kind check this group, kind generalize, and return the resulting local env
468 -- This binds the TyCons and Classes of the group, but not the DataCons
469 -- See Note [Kind checking for type and class decls]
470 -- Third return value is Nothing if the tycon be unsaturated; otherwise,
471 -- the arity
472 kcTyClGroup decls
473 = do { mod <- getModule
474 ; traceTc "---- kcTyClGroup ---- {" (text "module" <+> ppr mod $$ vcat (map ppr decls))
475
476 -- Kind checking;
477 -- 1. Bind kind variables for decls
478 -- 2. Kind-check decls
479 -- 3. Generalise the inferred kinds
480 -- See Note [Kind checking for type and class decls]
481
482 -- Step 1: Bind kind variables for all decls
483 ; initial_tcs <- getInitialKinds decls
484 ; traceTc "kcTyClGroup: initial kinds" $
485 ppr_tc_kinds initial_tcs
486
487 -- Step 2: Set extended envt, kind-check the decls
488 -- NB: the environment extension overrides the tycon
489 -- promotion-errors bindings
490 -- See Note [Type environment evolution]
491
492 ; solveEqualities $
493 tcExtendKindEnvWithTyCons initial_tcs $
494 mapM_ kcLTyClDecl decls
495
496 -- Step 3: generalisation
497 -- Kind checking done for this group
498 -- Now we have to kind generalize the flexis
499 ; poly_tcs <- mapAndReportM generalise initial_tcs
500
501 ; traceTc "---- kcTyClGroup end ---- }" (ppr_tc_kinds poly_tcs)
502 ; return poly_tcs }
503
504 where
505 ppr_tc_kinds tcs = vcat (map pp_tc tcs)
506 pp_tc tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc)
507
508 generalise :: TcTyCon -> TcM TcTyCon
509 -- For polymorphic things this is a no-op
510 generalise tc
511 = setSrcSpan (getSrcSpan tc) $
512 addTyConCtxt tc $
513 do { let name = tyConName tc
514 ; tc_binders <- mapM zonkTcTyVarBinder (tyConBinders tc)
515 ; tc_res_kind <- zonkTcType (tyConResKind tc)
516 ; let scoped_tvs = tcTyConScopedTyVars tc
517 user_tyvars = tcTyConUserTyVars tc
518
519 -- See Note [checkValidDependency]
520 ; checkValidDependency tc_binders tc_res_kind
521
522 -- See Note [Bad telescopes] in TcValidity
523 ; checkValidTelescope tc_binders user_tyvars empty
524 ; kvs <- kindGeneralize (mkTyConKind tc_binders tc_res_kind)
525
526 ; let all_binders = mkNamedTyConBinders Inferred kvs ++ tc_binders
527
528 ; (env, all_binders') <- zonkTyVarBindersX emptyZonkEnv all_binders
529 ; tc_res_kind' <- zonkTcTypeToType env tc_res_kind
530 ; scoped_tvs' <- zonkSigTyVarPairs scoped_tvs
531
532 -- See Note [Check telescope again during generalisation]
533 ; let extra = text "NB: Implicitly declared variables come before others."
534 ; checkValidTelescope all_binders user_tyvars extra
535
536 -- Make sure tc_kind' has the final, zonked kind variables
537 ; traceTc "Generalise kind" $
538 vcat [ ppr name, ppr tc_binders, ppr (mkTyConKind tc_binders tc_res_kind)
539 , ppr kvs, ppr all_binders, ppr tc_res_kind
540 , ppr all_binders', ppr tc_res_kind'
541 , ppr scoped_tvs ]
542
543 ; return (mkTcTyCon name user_tyvars all_binders' tc_res_kind'
544 scoped_tvs'
545 (tyConFlavour tc)) }
546
547
548 --------------
549 tcExtendKindEnvWithTyCons :: [TcTyCon] -> TcM a -> TcM a
550 tcExtendKindEnvWithTyCons tcs
551 = tcExtendKindEnvList [ (tyConName tc, ATcTyCon tc) | tc <- tcs ]
552
553 --------------
554 mkPromotionErrorEnv :: [LTyClDecl GhcRn] -> TcTypeEnv
555 -- Maps each tycon/datacon to a suitable promotion error
556 -- tc :-> APromotionErr TyConPE
557 -- dc :-> APromotionErr RecDataConPE
558 -- See Note [Recursion and promoting data constructors]
559
560 mkPromotionErrorEnv decls
561 = foldr (plusNameEnv . mk_prom_err_env . unLoc)
562 emptyNameEnv decls
563
564 mk_prom_err_env :: TyClDecl GhcRn -> TcTypeEnv
565 mk_prom_err_env (ClassDecl { tcdLName = L _ nm, tcdATs = ats })
566 = unitNameEnv nm (APromotionErr ClassPE)
567 `plusNameEnv`
568 mkNameEnv [ (name, APromotionErr TyConPE)
569 | L _ (FamilyDecl { fdLName = L _ name }) <- ats ]
570
571 mk_prom_err_env (DataDecl { tcdLName = L _ name
572 , tcdDataDefn = HsDataDefn { dd_cons = cons } })
573 = unitNameEnv name (APromotionErr TyConPE)
574 `plusNameEnv`
575 mkNameEnv [ (con, APromotionErr RecDataConPE)
576 | L _ con' <- cons, L _ con <- getConNames con' ]
577
578 mk_prom_err_env decl
579 = unitNameEnv (tcdName decl) (APromotionErr TyConPE)
580 -- Works for family declarations too
581
582 --------------
583 getInitialKinds :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
584 -- Returns a TcTyCon for each TyCon bound by the decls,
585 -- each with its initial kind
586
587 getInitialKinds decls = concatMapM (addLocM getInitialKind) decls
588
589 getInitialKind :: TyClDecl GhcRn -> TcM [TcTyCon]
590 -- Allocate a fresh kind variable for each TyCon and Class
591 -- For each tycon, return a TcTyCon with kind k
592 -- where k is the kind of tc, derived from the LHS
593 -- of the definition (and probably including
594 -- kind unification variables)
595 -- Example: data T a b = ...
596 -- return (T, kv1 -> kv2 -> kv3)
597 --
598 -- This pass deals with (ie incorporates into the kind it produces)
599 -- * The kind signatures on type-variable binders
600 -- * The result kinds signature on a TyClDecl
601 --
602 -- No family instances are passed to getInitialKinds
603
604 getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
605 = do { let cusk = hsDeclHasCusk decl
606 ; (tycon, inner_tcs) <-
607 kcLHsQTyVars name ClassFlavour cusk ktvs $
608 do { inner_tcs <- getFamDeclInitialKinds (Just cusk) ats
609 ; return (constraintKind, inner_tcs) }
610 ; return (tycon : inner_tcs) }
611
612 getInitialKind decl@(DataDecl { tcdLName = L _ name
613 , tcdTyVars = ktvs
614 , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
615 , dd_ND = new_or_data } })
616 = do { (tycon, _) <-
617 kcLHsQTyVars name (newOrDataToFlavour new_or_data) (hsDeclHasCusk decl) ktvs $
618 do { res_k <- case m_sig of
619 Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig
620 Nothing -> return liftedTypeKind
621 ; return (res_k, ()) }
622 ; return [tycon] }
623
624 getInitialKind (FamDecl { tcdFam = decl })
625 = do { tc <- getFamDeclInitialKind Nothing decl
626 ; return [tc] }
627
628 getInitialKind decl@(SynDecl { tcdLName = L _ name
629 , tcdTyVars = ktvs
630 , tcdRhs = rhs })
631 = do { (tycon, _) <- kcLHsQTyVars name TypeSynonymFlavour
632 (hsDeclHasCusk decl) ktvs $
633 do { res_k <- case kind_annotation rhs of
634 Nothing -> newMetaKindVar
635 Just ksig -> tcLHsKindSig (TySynKindCtxt name) ksig
636 ; return (res_k, ()) }
637 ; return [tycon] }
638 where
639 -- Keep this synchronized with 'hsDeclHasCusk'.
640 kind_annotation (L _ ty) = case ty of
641 HsParTy _ lty -> kind_annotation lty
642 HsKindSig _ _ k -> Just k
643 _ -> Nothing
644
645 getInitialKind (DataDecl _ (L _ _) _ _ (XHsDataDefn _)) = panic "getInitialKind"
646 getInitialKind (XTyClDecl _) = panic "getInitialKind"
647
648 ---------------------------------
649 getFamDeclInitialKinds :: Maybe Bool -- if assoc., CUSKness of assoc. class
650 -> [LFamilyDecl GhcRn]
651 -> TcM [TcTyCon]
652 getFamDeclInitialKinds mb_cusk decls
653 = mapM (addLocM (getFamDeclInitialKind mb_cusk)) decls
654
655 getFamDeclInitialKind :: Maybe Bool -- if assoc., CUSKness of assoc. class
656 -> FamilyDecl GhcRn
657 -> TcM TcTyCon
658 getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName = L _ name
659 , fdTyVars = ktvs
660 , fdResultSig = L _ resultSig
661 , fdInfo = info })
662 = do { (tycon, _) <-
663 kcLHsQTyVars name flav cusk ktvs $
664 do { res_k <- case resultSig of
665 KindSig _ ki -> tcLHsKindSig ctxt ki
666 TyVarSig _ (L _ (KindedTyVar _ _ ki)) -> tcLHsKindSig ctxt ki
667 _ -- open type families have * return kind by default
668 | tcFlavourIsOpen flav -> return liftedTypeKind
669 -- closed type families have their return kind inferred
670 -- by default
671 | otherwise -> newMetaKindVar
672 ; return (res_k, ()) }
673 ; return tycon }
674 where
675 cusk = famDeclHasCusk mb_cusk decl
676 flav = case info of
677 DataFamily -> DataFamilyFlavour (isJust mb_cusk)
678 OpenTypeFamily -> OpenTypeFamilyFlavour (isJust mb_cusk)
679 ClosedTypeFamily _ -> ClosedTypeFamilyFlavour
680 ctxt = TyFamResKindCtxt name
681 getFamDeclInitialKind _ (XFamilyDecl _) = panic "getFamDeclInitialKind"
682
683 ------------------------------------------------------------------------
684 kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
685 -- See Note [Kind checking for type and class decls]
686 kcLTyClDecl (L loc decl)
687 | hsDeclHasCusk decl -- See Note [Skip decls with CUSKs in kcLTyClDecl]
688 = traceTc "kcTyClDecl skipped due to cusk" (ppr tc_name)
689
690 | otherwise
691 = setSrcSpan loc $
692 tcAddDeclCtxt decl $
693 do { traceTc "kcTyClDecl {" (ppr tc_name)
694 ; kcTyClDecl decl
695 ; traceTc "kcTyClDecl done }" (ppr tc_name) }
696 where
697 tc_name = tyClDeclLName decl
698
699 kcTyClDecl :: TyClDecl GhcRn -> TcM ()
700 -- This function is used solely for its side effect on kind variables
701 -- NB kind signatures on the type variables and
702 -- result kind signature have already been dealt with
703 -- by getInitialKind, so we can ignore them here.
704
705 kcTyClDecl (DataDecl { tcdLName = L _ name, tcdDataDefn = defn })
706 | HsDataDefn { dd_cons = cons@(L _ (ConDeclGADT {}) : _), dd_ctxt = L _ [] } <- defn
707 = mapM_ (wrapLocM kcConDecl) cons
708 -- hs_tvs and dd_kindSig already dealt with in getInitialKind
709 -- This must be a GADT-style decl,
710 -- (see invariants of DataDefn declaration)
711 -- so (a) we don't need to bring the hs_tvs into scope, because the
712 -- ConDecls bind all their own variables
713 -- (b) dd_ctxt is not allowed for GADT-style decls, so we can ignore it
714
715 | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
716 = kcTyClTyVars name $
717 do { _ <- tcHsContext ctxt
718 ; mapM_ (wrapLocM kcConDecl) cons }
719
720 kcTyClDecl (SynDecl { tcdLName = L _ name, tcdRhs = lrhs })
721 = kcTyClTyVars name $
722 do { syn_tc <- kcLookupTcTyCon name
723 -- NB: check against the result kind that we allocated
724 -- in getInitialKinds.
725 ; discardResult $ tcCheckLHsType lrhs (tyConResKind syn_tc) }
726
727 kcTyClDecl (ClassDecl { tcdLName = L _ name
728 , tcdCtxt = ctxt, tcdSigs = sigs })
729 = kcTyClTyVars name $
730 do { _ <- tcHsContext ctxt
731 ; mapM_ (wrapLocM kc_sig) sigs }
732 where
733 kc_sig (ClassOpSig _ _ nms op_ty)
734 = kcHsSigType (TyConSkol ClassFlavour name) nms op_ty
735 kc_sig _ = return ()
736
737 kcTyClDecl (FamDecl _ (FamilyDecl { fdLName = L _ fam_tc_name
738 , fdInfo = fd_info }))
739 -- closed type families look at their equations, but other families don't
740 -- do anything here
741 = case fd_info of
742 ClosedTypeFamily (Just eqns) ->
743 do { fam_tc <- kcLookupTcTyCon fam_tc_name
744 ; mapM_ (kcTyFamInstEqn fam_tc) eqns }
745 _ -> return ()
746 kcTyClDecl (FamDecl _ (XFamilyDecl _)) = panic "kcTyClDecl"
747 kcTyClDecl (DataDecl _ (L _ _) _ _ (XHsDataDefn _)) = panic "kcTyClDecl"
748 kcTyClDecl (XTyClDecl _) = panic "kcTyClDecl"
749
750 -------------------
751 kcConDecl :: ConDecl GhcRn -> TcM ()
752 kcConDecl (ConDeclH98 { con_name = name, con_ex_tvs = ex_tvs
753 , con_mb_cxt = ex_ctxt, con_args = args })
754 = addErrCtxt (dataConCtxtName [name]) $
755 -- See Note [Use SigTvs in kind-checking pass]
756 kcExplicitTKBndrs ex_tvs $
757 do { _ <- tcHsMbContext ex_ctxt
758 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args) }
759 -- We don't need to check the telescope here, because that's
760 -- done in tcConDecl
761
762 kcConDecl (ConDeclGADT { con_names = names
763 , con_qvars = qtvs, con_mb_cxt = cxt
764 , con_args = args, con_res_ty = res_ty })
765 | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = implicit_tkv_nms }
766 , hsq_explicit = explicit_tkv_nms } <- qtvs
767 = -- Even though the data constructor's type is closed, we
768 -- must still kind-check the type, because that may influence
769 -- the inferred kind of the /type/ constructor. Example:
770 -- data T f a where
771 -- MkT :: f a -> T f a
772 -- If we don't look at MkT we won't get the correct kind
773 -- for the type constructor T
774 addErrCtxt (dataConCtxtName names) $
775 discardResult $
776 kcImplicitTKBndrs implicit_tkv_nms $
777 kcExplicitTKBndrs explicit_tkv_nms $
778 do { _ <- tcHsMbContext cxt
779 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args)
780 ; _ <- tcHsOpenType res_ty
781 ; return () }
782 kcConDecl (XConDecl _) = panic "kcConDecl"
783 kcConDecl (ConDeclGADT _ _ _ (XLHsQTyVars _) _ _ _ _) = panic "kcConDecl"
784
785 {-
786 Note [Recursion and promoting data constructors]
787 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
788 We don't want to allow promotion in a strongly connected component
789 when kind checking.
790
791 Consider:
792 data T f = K (f (K Any))
793
794 When kind checking the `data T' declaration the local env contains the
795 mappings:
796 T -> ATcTyCon <some initial kind>
797 K -> APromotionErr
798
799 APromotionErr is only used for DataCons, and only used during type checking
800 in tcTyClGroup.
801
802 Note [Use SigTvs in kind-checking pass]
803 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
804 Consider
805
806 data Proxy a where
807 MkProxy1 :: forall k (b :: k). Proxy b
808 MkProxy2 :: forall j (c :: j). Proxy c
809
810 It seems reasonable that this should be accepted. But something very strange
811 is going on here: when we're kind-checking this declaration, we need to unify
812 the kind of `a` with k and j -- even though k and j's scopes are local to the type of
813 MkProxy{1,2}. The best approach we've come up with is to use SigTvs during
814 the kind-checking pass. First off, note that it's OK if the kind-checking pass
815 is too permissive: we'll snag the problems in the type-checking pass later.
816 (This extra permissiveness might happen with something like
817
818 data SameKind :: k -> k -> Type
819 data Bad a where
820 MkBad :: forall k1 k2 (a :: k1) (b :: k2). Bad (SameKind a b)
821
822 which would be accepted if k1 and k2 were SigTvs. This is correctly rejected
823 in the second pass, though. Test case: polykinds/SigTvKinds3)
824 Recall that the kind-checking pass exists solely to collect constraints
825 on the kinds and to power unification.
826
827 To achieve the use of SigTvs, we must be careful to use specialized functions
828 that produce SigTvs, not ordinary skolems. This is why we need
829 kcExplicitTKBndrs and kcImplicitTKBndrs in TcHsType, separate from their
830 tc... variants.
831
832 The drawback of this approach is sometimes it will accept a definition that
833 a (hypothetical) declarative specification would likely reject. As a general
834 rule, we don't want to allow polymorphic recursion without a CUSK. Indeed,
835 the whole point of CUSKs is to allow polymorphic recursion. Yet, the SigTvs
836 approach allows a limited form of polymorphic recursion *without* a CUSK.
837
838 To wit:
839 data T a = forall k (b :: k). MkT (T b) Int
840 (test case: dependent/should_compile/T14066a)
841
842 Note that this is polymorphically recursive, with the recursive occurrence
843 of T used at a kind other than a's kind. The approach outlined here accepts
844 this definition, because this kind is still a kind variable (and so the
845 SigTvs unify). Stepping back, I (Richard) have a hard time envisioning a
846 way to describe exactly what declarations will be accepted and which will
847 be rejected (without a CUSK). However, the accepted definitions are indeed
848 well-kinded and any rejected definitions would be accepted with a CUSK,
849 and so this wrinkle need not cause anyone to lose sleep.
850
851 ************************************************************************
852 * *
853 \subsection{Type checking}
854 * *
855 ************************************************************************
856
857 Note [Type checking recursive type and class declarations]
858 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
859 At this point we have completed *kind-checking* of a mutually
860 recursive group of type/class decls (done in kcTyClGroup). However,
861 we discarded the kind-checked types (eg RHSs of data type decls);
862 note that kcTyClDecl returns (). There are two reasons:
863
864 * It's convenient, because we don't have to rebuild a
865 kinded HsDecl (a fairly elaborate type)
866
867 * It's necessary, because after kind-generalisation, the
868 TyCons/Classes may now be kind-polymorphic, and hence need
869 to be given kind arguments.
870
871 Example:
872 data T f a = MkT (f a) (T f a)
873 During kind-checking, we give T the kind T :: k1 -> k2 -> *
874 and figure out constraints on k1, k2 etc. Then we generalise
875 to get T :: forall k. (k->*) -> k -> *
876 So now the (T f a) in the RHS must be elaborated to (T k f a).
877
878 However, during tcTyClDecl of T (above) we will be in a recursive
879 "knot". So we aren't allowed to look at the TyCon T itself; we are only
880 allowed to put it (lazily) in the returned structures. But when
881 kind-checking the RHS of T's decl, we *do* need to know T's kind (so
882 that we can correctly elaboarate (T k f a). How can we get T's kind
883 without looking at T? Delicate answer: during tcTyClDecl, we extend
884
885 *Global* env with T -> ATyCon (the (not yet built) final TyCon for T)
886 *Local* env with T -> ATcTyCon (TcTyCon with the polymorphic kind of T)
887
888 Then:
889
890 * During TcHsType.kcTyVar we look in the *local* env, to get the
891 known kind for T.
892
893 * But in TcHsType.ds_type (and ds_var_app in particular) we look in
894 the *global* env to get the TyCon. But we must be careful not to
895 force the TyCon or we'll get a loop.
896
897 This fancy footwork (with two bindings for T) is only necessary for the
898 TyCons or Classes of this recursive group. Earlier, finished groups,
899 live in the global env only.
900
901 See also Note [Kind checking recursive type and class declarations]
902
903 Note [Kind checking recursive type and class declarations]
904 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
905 Before we can type-check the decls, we must kind check them. This
906 is done by establishing an "initial kind", which is a rather uninformed
907 guess at a tycon's kind (by counting arguments, mainly) and then
908 using this initial kind for recursive occurrences.
909
910 The initial kind is stored in exactly the same way during kind-checking
911 as it is during type-checking (Note [Type checking recursive type and class
912 declarations]): in the *local* environment, with ATcTyCon. But we still
913 must store *something* in the *global* environment. Even though we
914 discard the result of kind-checking, we sometimes need to produce error
915 messages. These error messages will want to refer to the tycons being
916 checked, except that they don't exist yet, and it would be Terribly
917 Annoying to get the error messages to refer back to HsSyn. So we
918 create a TcTyCon and put it in the global env. This tycon can
919 print out its name and knows its kind,
920 but any other action taken on it will panic. Note
921 that TcTyCons are *not* knot-tied, unlike the rather valid but
922 knot-tied ones that occur during type-checking.
923
924 Note [Declarations for wired-in things]
925 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
926 For wired-in things we simply ignore the declaration
927 and take the wired-in information. That avoids complications.
928 e.g. the need to make the data constructor worker name for
929 a constraint tuple match the wired-in one
930 -}
931
932 tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM TyCon
933 tcTyClDecl roles_info (L loc decl)
934 | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
935 = case thing of -- See Note [Declarations for wired-in things]
936 ATyCon tc -> return tc
937 _ -> pprPanic "tcTyClDecl" (ppr thing)
938
939 | otherwise
940 = setSrcSpan loc $ tcAddDeclCtxt decl $
941 do { traceTc "---- tcTyClDecl ---- {" (ppr decl)
942 ; tc <- tcTyClDecl1 Nothing roles_info decl
943 ; traceTc "---- tcTyClDecl end ---- }" (ppr tc)
944 ; return tc }
945
946 -- "type family" declarations
947 tcTyClDecl1 :: Maybe Class -> RolesInfo -> TyClDecl GhcRn -> TcM TyCon
948 tcTyClDecl1 parent _roles_info (FamDecl { tcdFam = fd })
949 = tcFamDecl1 parent fd
950
951 -- "type" synonym declaration
952 tcTyClDecl1 _parent roles_info
953 (SynDecl { tcdLName = L _ tc_name, tcdRhs = rhs })
954 = ASSERT( isNothing _parent )
955 tcTyClTyVars tc_name $ \ binders res_kind ->
956 tcTySynRhs roles_info tc_name binders res_kind rhs
957
958 -- "data/newtype" declaration
959 tcTyClDecl1 _parent roles_info
960 (DataDecl { tcdLName = L _ tc_name
961 , tcdDataDefn = defn })
962 = ASSERT( isNothing _parent )
963 tcTyClTyVars tc_name $ \ tycon_binders res_kind ->
964 tcDataDefn roles_info tc_name tycon_binders res_kind defn
965
966 tcTyClDecl1 _parent roles_info
967 (ClassDecl { tcdLName = L _ class_name
968 , tcdCtxt = ctxt, tcdMeths = meths
969 , tcdFDs = fundeps, tcdSigs = sigs
970 , tcdATs = ats, tcdATDefs = at_defs })
971 = ASSERT( isNothing _parent )
972 do { clas <- fixM $ \ clas ->
973 -- We need the knot because 'clas' is passed into tcClassATs
974 tcTyClTyVars class_name $ \ binders res_kind ->
975 do { MASSERT( isConstraintKind res_kind )
976 ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders)
977 ; let tycon_name = class_name -- We use the same name
978 roles = roles_info tycon_name -- for TyCon and Class
979
980 ; ctxt' <- solveEqualities $ tcHsContext ctxt
981 ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
982 -- Squeeze out any kind unification variables
983 ; fds' <- mapM (addLocM tc_fundep) fundeps
984 ; sig_stuff <- tcClassSigs class_name sigs meths
985 ; at_stuff <- tcClassATs class_name clas ats at_defs
986 ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
987 -- TODO: Allow us to distinguish between abstract class,
988 -- and concrete class with no methods (maybe by
989 -- specifying a trailing where or not
990 ; is_boot <- tcIsHsBootOrSig
991 ; let body | is_boot, null ctxt', null at_stuff, null sig_stuff
992 = Nothing
993 | otherwise
994 = Just (ctxt', at_stuff, sig_stuff, mindef)
995 ; clas <- buildClass class_name binders roles fds' body
996 ; traceTc "tcClassDecl" (ppr fundeps $$ ppr binders $$
997 ppr fds')
998 ; return clas }
999
1000 ; return (classTyCon clas) }
1001 where
1002 tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ;
1003 ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
1004 ; return (tvs1', tvs2') }
1005
1006 tcTyClDecl1 _ _ (XTyClDecl _) = panic "tcTyClDecl1"
1007
1008 tcFamDecl1 :: Maybe Class -> FamilyDecl GhcRn -> TcM TyCon
1009 tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_name)
1010 , fdResultSig = L _ sig, fdTyVars = user_tyvars
1011 , fdInjectivityAnn = inj })
1012 | DataFamily <- fam_info
1013 = tcTyClTyVars tc_name $ \ binders res_kind -> do
1014 { traceTc "data family:" (ppr tc_name)
1015 ; checkFamFlag tc_name
1016
1017 -- Check the kind signature, if any.
1018 -- Data families might have a variable return kind.
1019 -- See See Note [Arity of data families] in FamInstEnv.
1020 ; (extra_binders, final_res_kind) <- tcDataKindSig binders res_kind
1021 ; checkTc (tcIsLiftedTypeKind final_res_kind
1022 || isJust (tcGetCastedTyVar_maybe final_res_kind))
1023 (badKindSig False res_kind)
1024
1025 ; tc_rep_name <- newTyConRepName tc_name
1026 ; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
1027 final_res_kind
1028 (resultVariableName sig)
1029 (DataFamilyTyCon tc_rep_name)
1030 parent NotInjective
1031 ; return tycon }
1032
1033 | OpenTypeFamily <- fam_info
1034 = tcTyClTyVars tc_name $ \ binders res_kind -> do
1035 { traceTc "open type family:" (ppr tc_name)
1036 ; checkFamFlag tc_name
1037 ; inj' <- tcInjectivity binders inj
1038 ; let tycon = mkFamilyTyCon tc_name binders res_kind
1039 (resultVariableName sig) OpenSynFamilyTyCon
1040 parent inj'
1041 ; return tycon }
1042
1043 | ClosedTypeFamily mb_eqns <- fam_info
1044 = -- Closed type families are a little tricky, because they contain the definition
1045 -- of both the type family and the equations for a CoAxiom.
1046 do { traceTc "Closed type family:" (ppr tc_name)
1047 -- the variables in the header scope only over the injectivity
1048 -- declaration but this is not involved here
1049 ; (inj', binders, res_kind)
1050 <- tcTyClTyVars tc_name
1051 $ \ binders res_kind ->
1052 do { inj' <- tcInjectivity binders inj
1053 ; return (inj', binders, res_kind) }
1054
1055 ; checkFamFlag tc_name -- make sure we have -XTypeFamilies
1056
1057 -- If Nothing, this is an abstract family in a hs-boot file;
1058 -- but eqns might be empty in the Just case as well
1059 ; case mb_eqns of
1060 Nothing ->
1061 return $ mkFamilyTyCon tc_name binders res_kind
1062 (resultVariableName sig)
1063 AbstractClosedSynFamilyTyCon parent
1064 inj'
1065 Just eqns -> do {
1066
1067 -- Process the equations, creating CoAxBranches
1068 ; let tc_fam_tc = mkTcTyCon tc_name (ppr user_tyvars) binders res_kind
1069 [] ClosedTypeFamilyFlavour
1070
1071 ; branches <- mapAndReportM (tcTyFamInstEqn tc_fam_tc Nothing) eqns
1072 -- Do not attempt to drop equations dominated by earlier
1073 -- ones here; in the case of mutual recursion with a data
1074 -- type, we get a knot-tying failure. Instead we check
1075 -- for this afterwards, in TcValidity.checkValidCoAxiom
1076 -- Example: tc265
1077
1078 -- Create a CoAxiom, with the correct src location. It is Vitally
1079 -- Important that we do not pass the branches into
1080 -- newFamInstAxiomName. They have types that have been zonked inside
1081 -- the knot and we will die if we look at them. This is OK here
1082 -- because there will only be one axiom, so we don't need to
1083 -- differentiate names.
1084 -- See [Zonking inside the knot] in TcHsType
1085 ; co_ax_name <- newFamInstAxiomName tc_lname []
1086
1087 ; let mb_co_ax
1088 | null eqns = Nothing -- mkBranchedCoAxiom fails on empty list
1089 | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches)
1090
1091 fam_tc = mkFamilyTyCon tc_name binders res_kind (resultVariableName sig)
1092 (ClosedSynFamilyTyCon mb_co_ax) parent inj'
1093
1094 -- We check for instance validity later, when doing validity
1095 -- checking for the tycon. Exception: checking equations
1096 -- overlap done by dropDominatedAxioms
1097 ; return fam_tc } }
1098
1099 | otherwise = panic "tcFamInst1" -- Silence pattern-exhaustiveness checker
1100 tcFamDecl1 _ (XFamilyDecl _) = panic "tcFamDecl1"
1101
1102 -- | Maybe return a list of Bools that say whether a type family was declared
1103 -- injective in the corresponding type arguments. Length of the list is equal to
1104 -- the number of arguments (including implicit kind/coercion arguments).
1105 -- True on position
1106 -- N means that a function is injective in its Nth argument. False means it is
1107 -- not.
1108 tcInjectivity :: [TyConBinder] -> Maybe (LInjectivityAnn GhcRn)
1109 -> TcM Injectivity
1110 tcInjectivity _ Nothing
1111 = return NotInjective
1112
1113 -- User provided an injectivity annotation, so for each tyvar argument we
1114 -- check whether a type family was declared injective in that argument. We
1115 -- return a list of Bools, where True means that corresponding type variable
1116 -- was mentioned in lInjNames (type family is injective in that argument) and
1117 -- False means that it was not mentioned in lInjNames (type family is not
1118 -- injective in that type variable). We also extend injectivity information to
1119 -- kind variables, so if a user declares:
1120 --
1121 -- type family F (a :: k1) (b :: k2) = (r :: k3) | r -> a
1122 --
1123 -- then we mark both `a` and `k1` as injective.
1124 -- NB: the return kind is considered to be *input* argument to a type family.
1125 -- Since injectivity allows to infer input arguments from the result in theory
1126 -- we should always mark the result kind variable (`k3` in this example) as
1127 -- injective. The reason is that result type has always an assigned kind and
1128 -- therefore we can always infer the result kind if we know the result type.
1129 -- But this does not seem to be useful in any way so we don't do it. (Another
1130 -- reason is that the implementation would not be straightforward.)
1131 tcInjectivity tcbs (Just (L loc (InjectivityAnn _ lInjNames)))
1132 = setSrcSpan loc $
1133 do { let tvs = binderVars tcbs
1134 ; dflags <- getDynFlags
1135 ; checkTc (xopt LangExt.TypeFamilyDependencies dflags)
1136 (text "Illegal injectivity annotation" $$
1137 text "Use TypeFamilyDependencies to allow this")
1138 ; inj_tvs <- mapM (tcLookupTyVar . unLoc) lInjNames
1139 ; inj_tvs <- mapM zonkTcTyVarToTyVar inj_tvs -- zonk the kinds
1140 ; let inj_ktvs = filterVarSet isTyVar $ -- no injective coercion vars
1141 closeOverKinds (mkVarSet inj_tvs)
1142 ; let inj_bools = map (`elemVarSet` inj_ktvs) tvs
1143 ; traceTc "tcInjectivity" (vcat [ ppr tvs, ppr lInjNames, ppr inj_tvs
1144 , ppr inj_ktvs, ppr inj_bools ])
1145 ; return $ Injective inj_bools }
1146
1147 tcTySynRhs :: RolesInfo
1148 -> Name
1149 -> [TyConBinder] -> Kind
1150 -> LHsType GhcRn -> TcM TyCon
1151 tcTySynRhs roles_info tc_name binders res_kind hs_ty
1152 = do { env <- getLclEnv
1153 ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
1154 ; rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
1155 ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
1156 ; let roles = roles_info tc_name
1157 tycon = buildSynTyCon tc_name binders res_kind roles rhs_ty
1158 ; return tycon }
1159
1160 tcDataDefn :: RolesInfo -> Name
1161 -> [TyConBinder] -> Kind
1162 -> HsDataDefn GhcRn -> TcM TyCon
1163 -- NB: not used for newtype/data instances (whether associated or not)
1164 tcDataDefn roles_info
1165 tc_name tycon_binders res_kind
1166 (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
1167 , dd_ctxt = ctxt, dd_kindSig = mb_ksig
1168 , dd_cons = cons })
1169 = do { tcg_env <- getGblEnv
1170 ; let hsc_src = tcg_src tcg_env
1171 ; (extra_bndrs, final_res_kind) <- tcDataKindSig tycon_binders res_kind
1172 ; unless (mk_permissive_kind hsc_src cons) $
1173 checkTc (tcIsLiftedTypeKind final_res_kind) (badKindSig True res_kind)
1174
1175 ; let final_bndrs = tycon_binders `chkAppend` extra_bndrs
1176 roles = roles_info tc_name
1177
1178 ; stupid_tc_theta <- solveEqualities $ tcHsContext ctxt
1179 ; stupid_theta <- zonkTcTypeToTypes emptyZonkEnv
1180 stupid_tc_theta
1181 ; kind_signatures <- xoptM LangExt.KindSignatures
1182
1183 -- Check that we don't use kind signatures without Glasgow extensions
1184 ; when (isJust mb_ksig) $
1185 checkTc (kind_signatures) (badSigTyDecl tc_name)
1186
1187 ; gadt_syntax <- dataDeclChecks tc_name new_or_data stupid_theta cons
1188
1189 ; tycon <- fixM $ \ tycon -> do
1190 { let res_ty = mkTyConApp tycon (mkTyVarTys (binderVars final_bndrs))
1191 ; data_cons <- tcConDecls tycon (final_bndrs, res_ty) cons
1192 ; tc_rhs <- mk_tc_rhs hsc_src tycon data_cons
1193 ; tc_rep_nm <- newTyConRepName tc_name
1194 ; return (mkAlgTyCon tc_name
1195 final_bndrs
1196 final_res_kind
1197 roles
1198 (fmap unLoc cType)
1199 stupid_theta tc_rhs
1200 (VanillaAlgTyCon tc_rep_nm)
1201 gadt_syntax) }
1202 ; traceTc "tcDataDefn" (ppr tc_name $$ ppr tycon_binders $$ ppr extra_bndrs)
1203 ; return tycon }
1204 where
1205 -- Abstract data types in hsig files can have arbitrary kinds,
1206 -- because they may be implemented by type synonyms
1207 -- (which themselves can have arbitrary kinds, not just *)
1208 mk_permissive_kind HsigFile [] = True
1209 mk_permissive_kind _ _ = False
1210
1211 -- In hs-boot, a 'data' declaration with no constructors
1212 -- indicates a nominally distinct abstract data type.
1213 mk_tc_rhs HsBootFile _ []
1214 = return AbstractTyCon
1215
1216 mk_tc_rhs HsigFile _ [] -- ditto
1217 = return AbstractTyCon
1218
1219 mk_tc_rhs _ tycon data_cons
1220 = case new_or_data of
1221 DataType -> return (mkDataTyConRhs data_cons)
1222 NewType -> ASSERT( not (null data_cons) )
1223 mkNewTyConRhs tc_name tycon (head data_cons)
1224 tcDataDefn _ _ _ _ (XHsDataDefn _) = panic "tcDataDefn"
1225
1226 {-
1227 ************************************************************************
1228 * *
1229 Typechecking associated types (in class decls)
1230 (including the associated-type defaults)
1231 * *
1232 ************************************************************************
1233
1234 Note [Associated type defaults]
1235 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1236
1237 The following is an example of associated type defaults:
1238 class C a where
1239 data D a
1240
1241 type F a b :: *
1242 type F a b = [a] -- Default
1243
1244 Note that we can get default definitions only for type families, not data
1245 families.
1246 -}
1247
1248 tcClassATs :: Name -- The class name (not knot-tied)
1249 -> Class -- The class parent of this associated type
1250 -> [LFamilyDecl GhcRn] -- Associated types.
1251 -> [LTyFamDefltEqn GhcRn] -- Associated type defaults.
1252 -> TcM [ClassATItem]
1253 tcClassATs class_name cls ats at_defs
1254 = do { -- Complain about associated type defaults for non associated-types
1255 sequence_ [ failWithTc (badATErr class_name n)
1256 | n <- map at_def_tycon at_defs
1257 , not (n `elemNameSet` at_names) ]
1258 ; mapM tc_at ats }
1259 where
1260 at_def_tycon :: LTyFamDefltEqn GhcRn -> Name
1261 at_def_tycon (L _ eqn) = unLoc (feqn_tycon eqn)
1262
1263 at_fam_name :: LFamilyDecl GhcRn -> Name
1264 at_fam_name (L _ decl) = unLoc (fdLName decl)
1265
1266 at_names = mkNameSet (map at_fam_name ats)
1267
1268 at_defs_map :: NameEnv [LTyFamDefltEqn GhcRn]
1269 -- Maps an AT in 'ats' to a list of all its default defs in 'at_defs'
1270 at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv
1271 (at_def_tycon at_def) [at_def])
1272 emptyNameEnv at_defs
1273
1274 tc_at at = do { fam_tc <- addLocM (tcFamDecl1 (Just cls)) at
1275 ; let at_defs = lookupNameEnv at_defs_map (at_fam_name at)
1276 `orElse` []
1277 ; atd <- tcDefaultAssocDecl fam_tc at_defs
1278 ; return (ATI fam_tc atd) }
1279
1280 -------------------------
1281 tcDefaultAssocDecl :: TyCon -- ^ Family TyCon (not knot-tied)
1282 -> [LTyFamDefltEqn GhcRn] -- ^ Defaults
1283 -> TcM (Maybe (Type, SrcSpan)) -- ^ Type checked RHS
1284 tcDefaultAssocDecl _ []
1285 = return Nothing -- No default declaration
1286
1287 tcDefaultAssocDecl _ (d1:_:_)
1288 = failWithTc (text "More than one default declaration for"
1289 <+> ppr (feqn_tycon (unLoc d1)))
1290
1291 tcDefaultAssocDecl fam_tc [L loc (FamEqn { feqn_tycon = L _ tc_name
1292 , feqn_pats = hs_tvs
1293 , feqn_rhs = rhs })]
1294 | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = imp_vars}
1295 , hsq_explicit = exp_vars } <- hs_tvs
1296 = -- See Note [Type-checking default assoc decls]
1297 setSrcSpan loc $
1298 tcAddFamInstCtxt (text "default type instance") tc_name $
1299 do { traceTc "tcDefaultAssocDecl" (ppr tc_name)
1300 ; let fam_tc_name = tyConName fam_tc
1301 fam_arity = length (tyConVisibleTyVars fam_tc)
1302
1303 -- Kind of family check
1304 ; ASSERT( fam_tc_name == tc_name )
1305 checkTc (isTypeFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
1306
1307 -- Arity check
1308 ; checkTc (exp_vars `lengthIs` fam_arity)
1309 (wrongNumberOfParmsErr fam_arity)
1310
1311 -- Typecheck RHS
1312 ; let all_vars = imp_vars ++ map hsLTyVarName exp_vars
1313 pats = map hsLTyVarBndrToType exp_vars
1314
1315 -- NB: Use tcFamTyPats, not tcTyClTyVars. The latter expects to get
1316 -- the LHsQTyVars used for declaring a tycon, but the names here
1317 -- are different.
1318
1319 -- You might think we should pass in some ClsInstInfo, as we're looking
1320 -- at an associated type. But this would be wrong, because an associated
1321 -- type default LHS can mention *different* type variables than the
1322 -- enclosing class. So it's treated more as a freestanding beast.
1323 ; (pats', rhs_ty)
1324 <- tcFamTyPats fam_tc Nothing all_vars pats
1325 (kcTyFamEqnRhs Nothing rhs) $
1326 \tvs pats rhs_kind ->
1327 do { rhs_ty <- solveEqualities $
1328 tcCheckLHsType rhs rhs_kind
1329
1330 -- Zonk the patterns etc into the Type world
1331 ; (ze, _) <- zonkTyBndrsX emptyZonkEnv tvs
1332 ; pats' <- zonkTcTypeToTypes ze pats
1333 ; rhs_ty' <- zonkTcTypeToType ze rhs_ty
1334 ; return (pats', rhs_ty') }
1335
1336 -- See Note [Type-checking default assoc decls]
1337 ; case tcMatchTys pats' (mkTyVarTys (tyConTyVars fam_tc)) of
1338 Just subst -> return (Just (substTyUnchecked subst rhs_ty, loc) )
1339 Nothing -> failWithTc (defaultAssocKindErr fam_tc)
1340 -- We check for well-formedness and validity later,
1341 -- in checkValidClass
1342 }
1343 tcDefaultAssocDecl _ [L _ (XFamEqn _)] = panic "tcDefaultAssocDecl"
1344 tcDefaultAssocDecl _ [L _ (FamEqn _ (L _ _) (XLHsQTyVars _) _ _)]
1345 = panic "tcDefaultAssocDecl"
1346
1347 {- Note [Type-checking default assoc decls]
1348 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1349 Consider this default declaration for an associated type
1350
1351 class C a where
1352 type F (a :: k) b :: *
1353 type F x y = Proxy x -> y
1354
1355 Note that the class variable 'a' doesn't scope over the default assoc
1356 decl (rather oddly I think), and (less oddly) neither does the second
1357 argument 'b' of the associated type 'F', or the kind variable 'k'.
1358 Instead, the default decl is treated more like a top-level type
1359 instance.
1360
1361 However we store the default rhs (Proxy x -> y) in F's TyCon, using
1362 F's own type variables, so we need to convert it to (Proxy a -> b).
1363 We do this by calling tcMatchTys to match them up. This also ensures
1364 that x's kind matches a's and similarly for y and b. The error
1365 message isn't great, mind you. (Trac #11361 was caused by not doing a
1366 proper tcMatchTys here.) -}
1367
1368 -------------------------
1369 kcTyFamInstEqn :: TcTyCon -> LTyFamInstEqn GhcRn -> TcM ()
1370 kcTyFamInstEqn tc_fam_tc
1371 (L loc (HsIB { hsib_ext = HsIBRn { hsib_vars = tv_names }
1372 , hsib_body = FamEqn { feqn_tycon = L _ eqn_tc_name
1373 , feqn_pats = pats
1374 , feqn_rhs = hs_ty }}))
1375 = setSrcSpan loc $
1376 do { traceTc "kcTyFamInstEqn" (vcat
1377 [ text "tc_name =" <+> ppr eqn_tc_name
1378 , text "fam_tc =" <+> ppr tc_fam_tc <+> dcolon <+> ppr (tyConKind tc_fam_tc)
1379 , text "hsib_vars =" <+> ppr tv_names
1380 , text "feqn_pats =" <+> ppr pats ])
1381 ; checkTc (fam_name == eqn_tc_name)
1382 (wrongTyFamName fam_name eqn_tc_name)
1383 -- this check reports an arity error instead of a kind error; easier for user
1384 ; checkTc (pats `lengthIs` vis_arity) $
1385 wrongNumberOfParmsErr vis_arity
1386 ; kcFamTyPats tc_fam_tc tv_names pats $ \ rhs_kind ->
1387 discardResult $ kcTyFamEqnRhs Nothing hs_ty rhs_kind }
1388 where
1389 fam_name = tyConName tc_fam_tc
1390 vis_arity = length (tyConVisibleTyVars tc_fam_tc)
1391 kcTyFamInstEqn _ (L _ (XHsImplicitBndrs _)) = panic "kcTyFamInstEqn"
1392 kcTyFamInstEqn _ (L _ (HsIB _ (XFamEqn _))) = panic "kcTyFamInstEqn"
1393
1394 -- Infer the kind of the type on the RHS of a type family eqn. Then use
1395 -- this kind to check the kind of the LHS of the equation. This is useful
1396 -- as the callback to tcFamTyPats.
1397 kcTyFamEqnRhs :: Maybe ClsInstInfo
1398 -> LHsType GhcRn -- ^ Eqn RHS
1399 -> TcKind -- ^ Inferred kind of left-hand side
1400 -> TcM ([TcType], TcKind) -- ^ New pats, inst'ed kind of left-hand side
1401 kcTyFamEqnRhs mb_clsinfo rhs_hs_ty lhs_ki
1402 = do { -- It's still possible the lhs_ki has some foralls. Instantiate these away.
1403 (new_pats, insted_lhs_ki)
1404 <- instantiateTyUntilN mb_kind_env 0 lhs_ki
1405
1406 ; traceTc "kcTyFamEqnRhs" (vcat
1407 [ text "rhs_hs_ty =" <+> ppr rhs_hs_ty
1408 , text "lhs_ki =" <+> ppr lhs_ki
1409 , text "insted_lhs_ki =" <+> ppr insted_lhs_ki
1410 , text "new_pats =" <+> ppr new_pats
1411 ])
1412
1413 ; _ <- tcCheckLHsType rhs_hs_ty insted_lhs_ki
1414
1415 ; return (new_pats, insted_lhs_ki) }
1416 where
1417 mb_kind_env = thdOf3 <$> mb_clsinfo
1418
1419 tcTyFamInstEqn :: TcTyCon -> Maybe ClsInstInfo -> LTyFamInstEqn GhcRn
1420 -> TcM CoAxBranch
1421 -- Needs to be here, not in TcInstDcls, because closed families
1422 -- (typechecked here) have TyFamInstEqns
1423 tcTyFamInstEqn fam_tc mb_clsinfo
1424 (L loc (HsIB { hsib_ext = HsIBRn { hsib_vars = tv_names }
1425 , hsib_body = FamEqn { feqn_tycon = L _ eqn_tc_name
1426 , feqn_pats = pats
1427 , feqn_rhs = hs_ty }}))
1428 = ASSERT( getName fam_tc == eqn_tc_name )
1429 setSrcSpan loc $
1430 tcFamTyPats fam_tc mb_clsinfo tv_names pats
1431 (kcTyFamEqnRhs mb_clsinfo hs_ty) $
1432 \tvs pats res_kind ->
1433 do { rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
1434
1435 ; (ze, tvs') <- zonkTyBndrsX emptyZonkEnv tvs
1436 ; pats' <- zonkTcTypeToTypes ze pats
1437 ; rhs_ty' <- zonkTcTypeToType ze rhs_ty
1438 ; traceTc "tcTyFamInstEqn" (ppr fam_tc <+> pprTyVars tvs')
1439 -- don't print out the pats here, as they might be zonked inside the knot
1440 ; return (mkCoAxBranch tvs' [] pats' rhs_ty'
1441 (map (const Nominal) tvs')
1442 loc) }
1443 tcTyFamInstEqn _ _ (L _ (XHsImplicitBndrs _)) = panic "tcTyFamInstEqn"
1444 tcTyFamInstEqn _ _ (L _ (HsIB _ (XFamEqn _))) = panic "tcTyFamInstEqn"
1445
1446 kcDataDefn :: Maybe (VarEnv Kind) -- ^ Possibly, instantiations for vars
1447 -- (associated types only)
1448 -> DataFamInstDecl GhcRn
1449 -> TcKind -- ^ the kind of the tycon applied to pats
1450 -> TcM ([TcType], TcKind)
1451 -- ^ the kind signature might force instantiation
1452 -- of the tycon; this returns any extra args and the inst'ed kind
1453 -- See Note [Instantiating a family tycon]
1454 -- Used for 'data instance' only
1455 -- Ordinary 'data' is handled by kcTyClDec
1456 kcDataDefn mb_kind_env
1457 (DataFamInstDecl { dfid_eqn = HsIB { hsib_body =
1458 FamEqn { feqn_tycon = fam_name
1459 , feqn_pats = pats
1460 , feqn_fixity = fixity
1461 , feqn_rhs = HsDataDefn { dd_ctxt = ctxt
1462 , dd_cons = cons
1463 , dd_kindSig = mb_kind } }}})
1464 res_k
1465 = do { _ <- tcHsContext ctxt
1466 ; checkNoErrs $ mapM_ (wrapLocM kcConDecl) cons
1467 -- See Note [Failing early in kcDataDefn]
1468 ; exp_res_kind <- case mb_kind of
1469 Nothing -> return liftedTypeKind
1470 Just k -> tcLHsKindSig (DataKindCtxt (unLoc fam_name)) k
1471
1472 -- The expected type might have a forall at the type. Normally, we
1473 -- can't skolemise in kinds because we don't have type-level lambda.
1474 -- But here, we're at the top-level of an instance declaration, so
1475 -- we actually have a place to put the regeneralised variables.
1476 -- Thus: skolemise away. cf. Inst.deeplySkolemise and TcUnify.tcSkolemise
1477 -- Examples in indexed-types/should_compile/T12369
1478 ; let (tvs_to_skolemise, inner_res_kind) = tcSplitForAllTys exp_res_kind
1479
1480 ; (skol_subst, tvs') <- tcInstSkolTyVars tvs_to_skolemise
1481 -- we don't need to do anything substantive with the tvs' because the
1482 -- quantifyTyVars in tcFamTyPats will catch them.
1483
1484 ; let inner_res_kind' = substTyAddInScope skol_subst inner_res_kind
1485 tv_prs = zip (map tyVarName tvs_to_skolemise) tvs'
1486 skol_info = SigSkol (InstDeclCtxt False) exp_res_kind tv_prs
1487
1488 ; (ev_binds, (_, new_args, co))
1489 <- solveEqualities $
1490 checkConstraints skol_info tvs' [] $
1491 checkExpectedKindX mb_kind_env pp_fam_app
1492 bogus_ty res_k inner_res_kind'
1493
1494 ; let Pair lhs_ki rhs_ki = tcCoercionKind co
1495
1496 ; when debugIsOn $
1497 do { (_, ev_binds) <- zonkTcEvBinds emptyZonkEnv ev_binds
1498 ; MASSERT( isEmptyTcEvBinds ev_binds )
1499 ; lhs_ki <- zonkTcType lhs_ki
1500 ; rhs_ki <- zonkTcType rhs_ki
1501 ; MASSERT( lhs_ki `tcEqType` rhs_ki ) }
1502
1503 ; return (new_args, lhs_ki) }
1504 where
1505 bogus_ty = pprPanic "kcDataDefn" (ppr fam_name <+> ppr pats)
1506 pp_fam_app = pprFamInstLHS fam_name pats fixity (unLoc ctxt) mb_kind
1507 kcDataDefn _ (DataFamInstDecl (XHsImplicitBndrs _)) _
1508 = panic "kcDataDefn"
1509 kcDataDefn _ (DataFamInstDecl (HsIB _ (FamEqn _ _ _ _ (XHsDataDefn _)))) _
1510 = panic "kcDataDefn"
1511 kcDataDefn _ (DataFamInstDecl (HsIB _ (XFamEqn _))) _
1512 = panic "kcDataDefn"
1513
1514 {-
1515 Kind check type patterns and kind annotate the embedded type variables.
1516 type instance F [a] = rhs
1517
1518 * Here we check that a type instance matches its kind signature, but we do
1519 not check whether there is a pattern for each type index; the latter
1520 check is only required for type synonym instances.
1521
1522 Note [Instantiating a family tycon]
1523 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1524 It's possible that kind-checking the result of a family tycon applied to
1525 its patterns will instantiate the tycon further. For example, we might
1526 have
1527
1528 type family F :: k where
1529 F = Int
1530 F = Maybe
1531
1532 After checking (F :: forall k. k) (with no visible patterns), we still need
1533 to instantiate the k. With data family instances, this problem can be even
1534 more intricate, due to Note [Arity of data families] in FamInstEnv. See
1535 indexed-types/should_compile/T12369 for an example.
1536
1537 So, the kind-checker must return both the new args (that is, Type
1538 (Type -> Type) for the equations above) and the instantiated kind.
1539
1540 Because we don't need this information in the kind-checking phase of
1541 checking closed type families, we don't require these extra pieces of
1542 information in tc_fam_ty_pats.
1543
1544 Note [Failing early in kcDataDefn]
1545 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1546 We need to use checkNoErrs when calling kcConDecl. This is because kcConDecl
1547 calls tcConDecl, which checks that the return type of a GADT-like constructor
1548 is actually an instance of the type head. Without the checkNoErrs, potentially
1549 two bad things could happen:
1550
1551 1) Duplicate error messages, because tcConDecl will be called again during
1552 *type* checking (as opposed to kind checking)
1553 2) If we just keep blindly forging forward after both kind checking and type
1554 checking, we can get a panic in rejigConRes. See Trac #8368.
1555 -}
1556
1557 -----------------
1558 kcFamTyPats :: TcTyCon
1559 -> [Name]
1560 -> HsTyPats GhcRn
1561 -> (TcKind -> TcM ())
1562 -> TcM ()
1563 kcFamTyPats tc_fam_tc tv_names arg_pats kind_checker
1564 = discardResult $
1565 kcImplicitTKBndrs tv_names $
1566 do { let loc = nameSrcSpan name
1567 lhs_fun = L loc (HsTyVar noExt NotPromoted (L loc name))
1568 -- lhs_fun is for error messages only
1569 no_fun = pprPanic "kcFamTyPats" (ppr name)
1570 fun_kind = tyConKind tc_fam_tc
1571
1572 ; (_, _, res_kind_out) <- tcInferApps typeLevelMode Nothing lhs_fun no_fun
1573 fun_kind arg_pats
1574 ; kind_checker res_kind_out }
1575 where
1576 name = tyConName tc_fam_tc
1577
1578 tcFamTyPats :: TyCon
1579 -> Maybe ClsInstInfo
1580 -> [Name] -- Implicitly bound kind/type variable names
1581 -> HsTyPats GhcRn -- Type patterns
1582 -> (TcKind -> TcM ([TcType], TcKind))
1583 -- kind-checker for RHS
1584 -- See Note [Instantiating a family tycon]
1585 -> ( [TcTyVar] -- Kind and type variables
1586 -> [TcType] -- Kind and type arguments
1587 -> TcKind
1588 -> TcM a) -- NB: You can use solveEqualities here.
1589 -> TcM a
1590 -- Check the type patterns of a type or data family instance
1591 -- type instance F <pat1> <pat2> = <type>
1592 -- The 'tyvars' are the free type variables of pats
1593 --
1594 -- NB: The family instance declaration may be an associated one,
1595 -- nested inside an instance decl, thus
1596 -- instance C [a] where
1597 -- type F [a] = ...
1598 -- In that case, the type variable 'a' will *already be in scope*
1599 -- (and, if C is poly-kinded, so will its kind parameter).
1600 tcFamTyPats fam_tc mb_clsinfo
1601 tv_names arg_pats kind_checker thing_inside
1602 = do { -- First, check the arity.
1603 -- If we wait until validity checking, we'll get kind
1604 -- errors below when an arity error will be much easier to
1605 -- understand.
1606 let should_check_arity
1607 | DataFamilyFlavour _ <- flav = False
1608 -- why not check data families? See [Arity of data families] in FamInstEnv
1609 | otherwise = True
1610
1611 ; when should_check_arity $
1612 checkTc (arg_pats `lengthIs` vis_arity) $
1613 wrongNumberOfParmsErr vis_arity
1614 -- report only explicit arguments
1615
1616 ; (fam_used_tvs, (typats, (more_typats, res_kind)))
1617 <- solveEqualities $ -- See Note [Constraints in patterns]
1618 tcImplicitQTKBndrs FamInstSkol tv_names $
1619 -- See Note [Kind-checking tyvar binders for associated types]
1620 do { let loc = nameSrcSpan fam_name
1621 lhs_fun = L loc (HsTyVar noExt NotPromoted
1622 (L loc fam_name))
1623 fun_ty = mkTyConApp fam_tc []
1624 fun_kind = tyConKind fam_tc
1625 mb_kind_env = thdOf3 <$> mb_clsinfo
1626
1627 ; (_, args, res_kind_out)
1628 <- tcInferApps typeLevelMode mb_kind_env
1629 lhs_fun fun_ty fun_kind arg_pats
1630
1631 ; stuff <- kind_checker res_kind_out
1632 ; return (args, stuff) }
1633
1634 {- TODO (RAE): This should be cleverer. Consider this:
1635
1636 type family F a
1637
1638 data G a where
1639 MkG :: F a ~ Bool => G a
1640
1641 type family Foo (x :: G a) :: F a
1642 type instance Foo MkG = False
1643
1644 This should probably be accepted. Yet the solveEqualities
1645 will fail, unable to solve (F a ~ Bool)
1646 We want to quantify over that proof.
1647 But see Note [Constraints in patterns]
1648 below, which is missing this piece. -}
1649
1650
1651 -- Find free variables (after zonking) and turn
1652 -- them into skolems, so that we don't subsequently
1653 -- replace a meta kind var with (Any *)
1654 -- Very like kindGeneralize
1655 ; let all_pats = typats `chkAppend` more_typats
1656 ; vars <- zonkTcTypesAndSplitDepVars all_pats
1657 ; qtkvs <- quantifyTyVars emptyVarSet vars
1658
1659 ; when debugIsOn $
1660 do { all_pats <- mapM zonkTcTypeInKnot all_pats
1661 ; MASSERT2( isEmptyVarSet $ coVarsOfTypes all_pats, ppr all_pats ) }
1662 -- This should be the case, because otherwise the solveEqualities
1663 -- above would fail. TODO (RAE): Update once the solveEqualities
1664 -- bit is cleverer.
1665
1666 ; traceTc "tcFamTyPats" (ppr (getName fam_tc)
1667 $$ ppr all_pats $$ ppr qtkvs)
1668 -- Don't print out too much, as we might be in the knot
1669
1670 -- See Note [Free-floating kind vars] in TcHsType
1671 ; let all_mentioned_tvs = mkVarSet qtkvs
1672 -- qtkvs has all the tyvars bound by LHS
1673 -- type patterns
1674 unmentioned_tvs = filterOut (`elemVarSet` all_mentioned_tvs)
1675 fam_used_tvs
1676 -- If there are tyvars left over, we can
1677 -- assume they're free-floating, since they
1678 -- aren't bound by a type pattern
1679 ; checkNoErrs $ reportFloatingKvs fam_name flav
1680 qtkvs unmentioned_tvs
1681
1682 ; scopeTyVars FamInstSkol qtkvs $
1683 -- Extend envt with TcTyVars not TyVars, because the
1684 -- kind checking etc done by thing_inside does not expect
1685 -- to encounter TyVars; it expects TcTyVars
1686 thing_inside qtkvs all_pats res_kind }
1687 where
1688 fam_name = tyConName fam_tc
1689 flav = tyConFlavour fam_tc
1690 vis_arity = length (tyConVisibleTyVars fam_tc)
1691
1692
1693 {-
1694 Note [Constraints in patterns]
1695 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1696 NB: This isn't the whole story. See comment in tcFamTyPats.
1697
1698 At first glance, it seems there is a complicated story to tell in tcFamTyPats
1699 around constraint solving. After all, type family patterns can now do
1700 GADT pattern-matching, which is jolly complicated. But, there's a key fact
1701 which makes this all simple: everything is at top level! There cannot
1702 be untouchable type variables. There can't be weird interaction between
1703 case branches. There can't be global skolems.
1704
1705 This means that the semantics of type-level GADT matching is a little
1706 different than term level. If we have
1707
1708 data G a where
1709 MkGBool :: G Bool
1710
1711 And then
1712
1713 type family F (a :: G k) :: k
1714 type instance F MkGBool = True
1715
1716 we get
1717
1718 axF : F Bool (MkGBool <Bool>) ~ True
1719
1720 Simple! No casting on the RHS, because we can affect the kind parameter
1721 to F.
1722
1723 If we ever introduce local type families, this all gets a lot more
1724 complicated, and will end up looking awfully like term-level GADT
1725 pattern-matching.
1726
1727
1728 ** The new story **
1729
1730 Here is really what we want:
1731
1732 The matcher really can't deal with covars in arbitrary spots in coercions.
1733 But it can deal with covars that are arguments to GADT data constructors.
1734 So we somehow want to allow covars only in precisely those spots, then use
1735 them as givens when checking the RHS. TODO (RAE): Implement plan.
1736
1737
1738 Note [Quantifying over family patterns]
1739 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1740 We need to quantify over two different lots of kind variables:
1741
1742 First, the ones that come from the kinds of the tyvar args of
1743 tcTyVarBndrsKindGen, as usual
1744 data family Dist a
1745
1746 -- Proxy :: forall k. k -> *
1747 data instance Dist (Proxy a) = DP
1748 -- Generates data DistProxy = DP
1749 -- ax8 k (a::k) :: Dist * (Proxy k a) ~ DistProxy k a
1750 -- The 'k' comes from the tcTyVarBndrsKindGen (a::k)
1751
1752 Second, the ones that come from the kind argument of the type family
1753 which we pick up using the (tyCoVarsOfTypes typats) in the result of
1754 the thing_inside of tcHsTyvarBndrsGen.
1755 -- Any :: forall k. k
1756 data instance Dist Any = DA
1757 -- Generates data DistAny k = DA
1758 -- ax7 k :: Dist k (Any k) ~ DistAny k
1759 -- The 'k' comes from kindGeneralizeKinds (Any k)
1760
1761 Note [Quantified kind variables of a family pattern]
1762 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1763 Consider type family KindFam (p :: k1) (q :: k1)
1764 data T :: Maybe k1 -> k2 -> *
1765 type instance KindFam (a :: Maybe k) b = T a b -> Int
1766 The HsBSig for the family patterns will be ([k], [a])
1767
1768 Then in the family instance we want to
1769 * Bring into scope [ "k" -> k:*, "a" -> a:k ]
1770 * Kind-check the RHS
1771 * Quantify the type instance over k and k', as well as a,b, thus
1772 type instance [k, k', a:Maybe k, b:k']
1773 KindFam (Maybe k) k' a b = T k k' a b -> Int
1774
1775 Notice that in the third step we quantify over all the visibly-mentioned
1776 type variables (a,b), but also over the implicitly mentioned kind variables
1777 (k, k'). In this case one is bound explicitly but often there will be
1778 none. The role of the kind signature (a :: Maybe k) is to add a constraint
1779 that 'a' must have that kind, and to bring 'k' into scope.
1780
1781
1782
1783 ************************************************************************
1784 * *
1785 Data types
1786 * *
1787 ************************************************************************
1788 -}
1789
1790 dataDeclChecks :: Name -> NewOrData -> ThetaType -> [LConDecl GhcRn] -> TcM Bool
1791 dataDeclChecks tc_name new_or_data stupid_theta cons
1792 = do { -- Check that we don't use GADT syntax in H98 world
1793 gadtSyntax_ok <- xoptM LangExt.GADTSyntax
1794 ; let gadt_syntax = consUseGadtSyntax cons
1795 ; checkTc (gadtSyntax_ok || not gadt_syntax) (badGadtDecl tc_name)
1796
1797 -- Check that the stupid theta is empty for a GADT-style declaration
1798 ; checkTc (null stupid_theta || not gadt_syntax) (badStupidTheta tc_name)
1799
1800 -- Check that a newtype has exactly one constructor
1801 -- Do this before checking for empty data decls, so that
1802 -- we don't suggest -XEmptyDataDecls for newtypes
1803 ; checkTc (new_or_data == DataType || isSingleton cons)
1804 (newtypeConError tc_name (length cons))
1805
1806 -- Check that there's at least one condecl,
1807 -- or else we're reading an hs-boot file, or -XEmptyDataDecls
1808 ; empty_data_decls <- xoptM LangExt.EmptyDataDecls
1809 ; is_boot <- tcIsHsBootOrSig -- Are we compiling an hs-boot file?
1810 ; checkTc (not (null cons) || empty_data_decls || is_boot)
1811 (emptyConDeclsErr tc_name)
1812 ; return gadt_syntax }
1813
1814
1815 -----------------------------------
1816 consUseGadtSyntax :: [LConDecl a] -> Bool
1817 consUseGadtSyntax (L _ (ConDeclGADT { }) : _) = True
1818 consUseGadtSyntax _ = False
1819 -- All constructors have same shape
1820
1821 -----------------------------------
1822 tcConDecls :: TyCon -> ([TyConBinder], Type)
1823 -> [LConDecl GhcRn] -> TcM [DataCon]
1824 -- Why both the tycon tyvars and binders? Because the tyvars
1825 -- have all the names and the binders have the visibilities.
1826 tcConDecls rep_tycon (tmpl_bndrs, res_tmpl)
1827 = concatMapM $ addLocM $
1828 tcConDecl rep_tycon (mkTyConTagMap rep_tycon) tmpl_bndrs res_tmpl
1829 -- It's important that we pay for tag allocation here, once per TyCon,
1830 -- See Note [Constructor tag allocation], fixes #14657
1831
1832 tcConDecl :: TyCon -- Representation tycon. Knot-tied!
1833 -> NameEnv ConTag
1834 -> [TyConBinder] -> Type
1835 -- Return type template (with its template tyvars)
1836 -- (tvs, T tys), where T is the family TyCon
1837 -> ConDecl GhcRn
1838 -> TcM [DataCon]
1839
1840 tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
1841 (ConDeclH98 { con_name = name
1842 , con_ex_tvs = explicit_tkv_nms
1843 , con_mb_cxt = hs_ctxt
1844 , con_args = hs_args })
1845 = addErrCtxt (dataConCtxtName [name]) $
1846 do { -- Get hold of the existential type variables
1847 -- e.g. data T a = forall k (b::k) f. MkT a (f b)
1848 -- Here tmpl_bndrs = {a}
1849 -- hs_qvars = HsQTvs { hsq_implicit = {k}
1850 -- , hsq_explicit = {f,b} }
1851
1852 ; traceTc "tcConDecl 1" (vcat [ ppr name, ppr explicit_tkv_nms ])
1853
1854 ; (exp_tvs, (ctxt, arg_tys, field_lbls, stricts))
1855 <- solveEqualities $
1856 tcExplicitTKBndrs skol_info explicit_tkv_nms $
1857 do { ctxt <- tcHsMbContext hs_ctxt
1858 ; btys <- tcConArgs hs_args
1859 ; field_lbls <- lookupConstructorFields (unLoc name)
1860 ; let (arg_tys, stricts) = unzip btys
1861 ; return (ctxt, arg_tys, field_lbls, stricts)
1862 }
1863
1864 -- exp_tvs have explicit, user-written binding sites
1865 -- the kvs below are those kind variables entirely unmentioned by the user
1866 -- and discovered only by generalization
1867
1868 ; kvs <- quantifyConDecl (mkVarSet (binderVars tmpl_bndrs))
1869 (mkSpecForAllTys exp_tvs $
1870 mkFunTys ctxt $
1871 mkFunTys arg_tys $
1872 unitTy)
1873 -- That type is a lie, of course. (It shouldn't end in ()!)
1874 -- And we could construct a proper result type from the info
1875 -- at hand. But the result would mention only the tmpl_tvs,
1876 -- and so it just creates more work to do it right. Really,
1877 -- we're doing this to get the right behavior around removing
1878 -- any vars bound in exp_binders.
1879
1880 -- Zonk to Types
1881 ; (ze, qkvs) <- zonkTyBndrsX emptyZonkEnv kvs
1882 ; (ze, user_qtvs) <- zonkTyBndrsX ze exp_tvs
1883 ; arg_tys <- zonkTcTypeToTypes ze arg_tys
1884 ; ctxt <- zonkTcTypeToTypes ze ctxt
1885
1886 ; fam_envs <- tcGetFamInstEnvs
1887
1888 -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
1889 ; traceTc "tcConDecl 2" (ppr name $$ ppr field_lbls)
1890 ; let
1891 univ_tvbs = tyConTyVarBinders tmpl_bndrs
1892 univ_tvs = binderVars univ_tvbs
1893 ex_tvbs = mkTyVarBinders Inferred qkvs ++
1894 mkTyVarBinders Specified user_qtvs
1895 ex_tvs = qkvs ++ user_qtvs
1896 -- For H98 datatypes, the user-written tyvar binders are precisely
1897 -- the universals followed by the existentials.
1898 -- See Note [DataCon user type variable binders] in DataCon.
1899 user_tvbs = univ_tvbs ++ ex_tvbs
1900 buildOneDataCon (L _ name) = do
1901 { is_infix <- tcConIsInfixH98 name hs_args
1902 ; rep_nm <- newTyConRepName name
1903
1904 ; buildDataCon fam_envs name is_infix rep_nm
1905 stricts Nothing field_lbls
1906 univ_tvs ex_tvs user_tvbs
1907 [{- no eq_preds -}] ctxt arg_tys
1908 res_tmpl rep_tycon tag_map
1909 -- NB: we put data_tc, the type constructor gotten from the
1910 -- constructor type signature into the data constructor;
1911 -- that way checkValidDataCon can complain if it's wrong.
1912 }
1913 ; traceTc "tcConDecl 2" (ppr name)
1914 ; mapM buildOneDataCon [name]
1915 }
1916 where
1917 skol_info = SigTypeSkol (ConArgCtxt (unLoc name))
1918
1919 tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
1920 (ConDeclGADT { con_names = names
1921 , con_qvars = qtvs
1922 , con_mb_cxt = cxt, con_args = hs_args
1923 , con_res_ty = res_ty })
1924 | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = implicit_tkv_nms }
1925 , hsq_explicit = explicit_tkv_nms } <- qtvs
1926 = addErrCtxt (dataConCtxtName names) $
1927 do { traceTc "tcConDecl 1" (ppr names)
1928 ; let (L _ name : _) = names
1929 skol_info = DataConSkol name
1930
1931 ; (imp_tvs, (exp_tvs, (ctxt, arg_tys, res_ty, field_lbls, stricts)))
1932 <- solveEqualities $
1933 tcImplicitTKBndrs skol_info implicit_tkv_nms $
1934 tcExplicitTKBndrs skol_info explicit_tkv_nms $
1935 do { ctxt <- tcHsMbContext cxt
1936 ; btys <- tcConArgs hs_args
1937 ; res_ty' <- tcHsLiftedType res_ty
1938 ; field_lbls <- lookupConstructorFields name
1939 ; let (arg_tys, stricts) = unzip btys
1940 ; return (ctxt, arg_tys, res_ty', field_lbls, stricts)
1941 }
1942 ; let user_tvs = imp_tvs ++ exp_tvs
1943
1944 ; tkvs <- quantifyConDecl emptyVarSet (mkSpecForAllTys user_tvs $
1945 mkFunTys ctxt $
1946 mkFunTys arg_tys $
1947 res_ty)
1948
1949 -- Zonk to Types
1950 ; (ze, tkvs) <- zonkTyBndrsX emptyZonkEnv tkvs
1951 ; (ze, user_tvs) <- zonkTyBndrsX ze user_tvs
1952 ; arg_tys <- zonkTcTypeToTypes ze arg_tys
1953 ; ctxt <- zonkTcTypeToTypes ze ctxt
1954 ; res_ty <- zonkTcTypeToType ze res_ty
1955
1956 ; let (univ_tvs, ex_tvs, tkvs', user_tvs', eq_preds, arg_subst)
1957 = rejigConRes tmpl_bndrs res_tmpl tkvs user_tvs res_ty
1958 -- NB: this is a /lazy/ binding, so we pass six thunks to
1959 -- buildDataCon without yet forcing the guards in rejigConRes
1960 -- See Note [Checking GADT return types]
1961
1962 -- Compute the user-written tyvar binders. These have the same
1963 -- tyvars as univ_tvs/ex_tvs, but perhaps in a different order.
1964 -- See Note [DataCon user type variable binders] in DataCon.
1965 tkv_bndrs = mkTyVarBinders Inferred tkvs'
1966 user_tv_bndrs = mkTyVarBinders Specified user_tvs'
1967 all_user_bndrs = tkv_bndrs ++ user_tv_bndrs
1968
1969 ctxt' = substTys arg_subst ctxt
1970 arg_tys' = substTys arg_subst arg_tys
1971 res_ty' = substTy arg_subst res_ty
1972
1973
1974 ; fam_envs <- tcGetFamInstEnvs
1975
1976 -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
1977 ; traceTc "tcConDecl 2" (ppr names $$ ppr field_lbls)
1978 ; let
1979 buildOneDataCon (L _ name) = do
1980 { is_infix <- tcConIsInfixGADT name hs_args
1981 ; rep_nm <- newTyConRepName name
1982
1983 ; buildDataCon fam_envs name is_infix
1984 rep_nm
1985 stricts Nothing field_lbls
1986 univ_tvs ex_tvs all_user_bndrs eq_preds
1987 ctxt' arg_tys' res_ty' rep_tycon tag_map
1988 -- NB: we put data_tc, the type constructor gotten from the
1989 -- constructor type signature into the data constructor;
1990 -- that way checkValidDataCon can complain if it's wrong.
1991 }
1992 ; traceTc "tcConDecl 2" (ppr names)
1993 ; mapM buildOneDataCon names
1994 }
1995 tcConDecl _ _ _ _ (ConDeclGADT _ _ _ (XLHsQTyVars _) _ _ _ _)
1996 = panic "tcConDecl"
1997 tcConDecl _ _ _ _ (XConDecl _) = panic "tcConDecl"
1998
1999 -- | Produce the telescope of kind variables that this datacon is
2000 -- implicitly quantified over. Incoming type need not be zonked.
2001 quantifyConDecl :: TcTyCoVarSet -- outer tvs, not to be quantified over; zonked
2002 -> TcType -> TcM [TcTyVar]
2003 quantifyConDecl gbl_tvs ty
2004 = do { ty <- zonkTcTypeInKnot ty
2005 ; let fvs = candidateQTyVarsOfType ty
2006 ; quantifyTyVars gbl_tvs fvs }
2007
2008 tcConIsInfixH98 :: Name
2009 -> HsConDetails (LHsType GhcRn) (Located [LConDeclField GhcRn])
2010 -> TcM Bool
2011 tcConIsInfixH98 _ details
2012 = case details of
2013 InfixCon {} -> return True
2014 _ -> return False
2015
2016 tcConIsInfixGADT :: Name
2017 -> HsConDetails (LHsType GhcRn) (Located [LConDeclField GhcRn])
2018 -> TcM Bool
2019 tcConIsInfixGADT con details
2020 = case details of
2021 InfixCon {} -> return True
2022 RecCon {} -> return False
2023 PrefixCon arg_tys -- See Note [Infix GADT constructors]
2024 | isSymOcc (getOccName con)
2025 , [_ty1,_ty2] <- arg_tys
2026 -> do { fix_env <- getFixityEnv
2027 ; return (con `elemNameEnv` fix_env) }
2028 | otherwise -> return False
2029
2030 tcConArgs :: HsConDeclDetails GhcRn
2031 -> TcM [(TcType, HsSrcBang)]
2032 tcConArgs (PrefixCon btys)
2033 = mapM tcConArg btys
2034 tcConArgs (InfixCon bty1 bty2)
2035 = do { bty1' <- tcConArg bty1
2036 ; bty2' <- tcConArg bty2
2037 ; return [bty1', bty2'] }
2038 tcConArgs (RecCon fields)
2039 = mapM tcConArg btys
2040 where
2041 -- We need a one-to-one mapping from field_names to btys
2042 combined = map (\(L _ f) -> (cd_fld_names f,cd_fld_type f)) (unLoc fields)
2043 explode (ns,ty) = zip ns (repeat ty)
2044 exploded = concatMap explode combined
2045 (_,btys) = unzip exploded
2046
2047
2048 tcConArg :: LHsType GhcRn -> TcM (TcType, HsSrcBang)
2049 tcConArg bty
2050 = do { traceTc "tcConArg 1" (ppr bty)
2051 ; arg_ty <- tcHsOpenType (getBangType bty)
2052 -- Newtypes can't have unboxed types, but we check
2053 -- that in checkValidDataCon; this tcConArg stuff
2054 -- doesn't happen for GADT-style declarations
2055 ; traceTc "tcConArg 2" (ppr bty)
2056 ; return (arg_ty, getBangStrictness bty) }
2057
2058 {-
2059 Note [Infix GADT constructors]
2060 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2061 We do not currently have syntax to declare an infix constructor in GADT syntax,
2062 but it makes a (small) difference to the Show instance. So as a slightly
2063 ad-hoc solution, we regard a GADT data constructor as infix if
2064 a) it is an operator symbol
2065 b) it has two arguments
2066 c) there is a fixity declaration for it
2067 For example:
2068 infix 6 (:--:)
2069 data T a where
2070 (:--:) :: t1 -> t2 -> T Int
2071
2072
2073 Note [Checking GADT return types]
2074 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2075 There is a delicacy around checking the return types of a datacon. The
2076 central problem is dealing with a declaration like
2077
2078 data T a where
2079 MkT :: T a -> Q a
2080
2081 Note that the return type of MkT is totally bogus. When creating the T
2082 tycon, we also need to create the MkT datacon, which must have a "rejigged"
2083 return type. That is, the MkT datacon's type must be transformed to have
2084 a uniform return type with explicit coercions for GADT-like type parameters.
2085 This rejigging is what rejigConRes does. The problem is, though, that checking
2086 that the return type is appropriate is much easier when done over *Type*,
2087 not *HsType*, and doing a call to tcMatchTy will loop because T isn't fully
2088 defined yet.
2089
2090 So, we want to make rejigConRes lazy and then check the validity of
2091 the return type in checkValidDataCon. To do this we /always/ return a
2092 6-tuple from rejigConRes (so that we can compute the return type from it, which
2093 checkValidDataCon needs), but the first three fields may be bogus if
2094 the return type isn't valid (the last equation for rejigConRes).
2095
2096 This is better than an earlier solution which reduced the number of
2097 errors reported in one pass. See Trac #7175, and #10836.
2098 -}
2099
2100 -- Example
2101 -- data instance T (b,c) where
2102 -- TI :: forall e. e -> T (e,e)
2103 --
2104 -- The representation tycon looks like this:
2105 -- data :R7T b c where
2106 -- TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1
2107 -- In this case orig_res_ty = T (e,e)
2108
2109 rejigConRes :: [TyConBinder] -> Type -- Template for result type; e.g.
2110 -- data instance T [a] b c ...
2111 -- gives template ([a,b,c], T [a] b c)
2112 -- Type must be of kind *!
2113 -> [TyVar] -- The constructor's user-written, inferred
2114 -- type variables
2115 -> [TyVar] -- The constructor's user-written, specified
2116 -- type variables
2117 -> Type -- res_ty type must be of kind *
2118 -> ([TyVar], -- Universal
2119 [TyVar], -- Existential (distinct OccNames from univs)
2120 [TyVar], -- The constructor's rejigged, user-written,
2121 -- inferred type variables
2122 [TyVar], -- The constructor's rejigged, user-written,
2123 -- specified type variables
2124 [EqSpec], -- Equality predicates
2125 TCvSubst) -- Substitution to apply to argument types
2126 -- We don't check that the TyCon given in the ResTy is
2127 -- the same as the parent tycon, because checkValidDataCon will do it
2128
2129 rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty
2130 -- E.g. data T [a] b c where
2131 -- MkT :: forall x y z. T [(x,y)] z z
2132 -- The {a,b,c} are the tmpl_tvs, and the {x,y,z} are the dc_tvs
2133 -- (NB: unlike the H98 case, the dc_tvs are not all existential)
2134 -- Then we generate
2135 -- Univ tyvars Eq-spec
2136 -- a a~(x,y)
2137 -- b b~z
2138 -- z
2139 -- Existentials are the leftover type vars: [x,y]
2140 -- The user-written type variables are what is listed in the forall:
2141 -- [x, y, z] (all specified). We must rejig these as well.
2142 -- See Note [DataCon user type variable binders] in DataCon.
2143 -- So we return ( [a,b,z], [x,y]
2144 -- , [], [x,y,z]
2145 -- , [a~(x,y),b~z], <arg-subst> )
2146 | Just subst <- ASSERT( isLiftedTypeKind (typeKind res_ty) )
2147 ASSERT( isLiftedTypeKind (typeKind res_tmpl) )
2148 tcMatchTy res_tmpl res_ty
2149 = let (univ_tvs, raw_eqs, kind_subst) = mkGADTVars tmpl_tvs dc_tvs subst
2150 raw_ex_tvs = dc_tvs `minusList` univ_tvs
2151 (arg_subst, substed_ex_tvs) = substTyVarBndrs kind_subst raw_ex_tvs
2152
2153 -- After rejigging the existential tyvars, the resulting substitution
2154 -- gives us exactly what we need to rejig the user-written tyvars,
2155 -- since the dcUserTyVarBinders invariant guarantees that the
2156 -- substitution has *all* the tyvars in its domain.
2157 -- See Note [DataCon user type variable binders] in DataCon.
2158 subst_user_tvs = map (getTyVar "rejigConRes" . substTyVar arg_subst)
2159 substed_inferred_tvs = subst_user_tvs dc_inferred_tvs
2160 substed_specified_tvs = subst_user_tvs dc_specified_tvs
2161
2162 substed_eqs = map (substEqSpec arg_subst) raw_eqs
2163 in
2164 (univ_tvs, substed_ex_tvs, substed_inferred_tvs, substed_specified_tvs,
2165 substed_eqs, arg_subst)
2166
2167 | otherwise
2168 -- If the return type of the data constructor doesn't match the parent
2169 -- type constructor, or the arity is wrong, the tcMatchTy will fail
2170 -- e.g data T a b where
2171 -- T1 :: Maybe a -- Wrong tycon
2172 -- T2 :: T [a] -- Wrong arity
2173 -- We are detect that later, in checkValidDataCon, but meanwhile
2174 -- we must do *something*, not just crash. So we do something simple
2175 -- albeit bogus, relying on checkValidDataCon to check the
2176 -- bad-result-type error before seeing that the other fields look odd
2177 -- See Note [Checking GADT return types]
2178 = (tmpl_tvs, dc_tvs `minusList` tmpl_tvs, dc_inferred_tvs, dc_specified_tvs,
2179 [], emptyTCvSubst)
2180 where
2181 dc_tvs = dc_inferred_tvs ++ dc_specified_tvs
2182 tmpl_tvs = binderVars tmpl_bndrs
2183
2184 {- Note [mkGADTVars]
2185 ~~~~~~~~~~~~~~~~~~~~
2186 Running example:
2187
2188 data T (k1 :: *) (k2 :: *) (a :: k2) (b :: k2) where
2189 MkT :: forall (x1 : *) (y :: x1) (z :: *).
2190 T x1 * (Proxy (y :: x1), z) z
2191
2192 We need the rejigged type to be
2193
2194 MkT :: forall (x1 :: *) (k2 :: *) (a :: k2) (b :: k2).
2195 forall (y :: x1) (z :: *).
2196 (k2 ~ *, a ~ (Proxy x1 y, z), b ~ z)
2197 => T x1 k2 a b
2198
2199 You might naively expect that z should become a universal tyvar,
2200 not an existential. (After all, x1 becomes a universal tyvar.)
2201 But z has kind * while b has kind k2, so the return type
2202 T x1 k2 a z
2203 is ill-kinded. Another way to say it is this: the universal
2204 tyvars must have exactly the same kinds as the tyConTyVars.
2205
2206 So we need an existential tyvar and a heterogeneous equality
2207 constraint. (The b ~ z is a bit redundant with the k2 ~ * that
2208 comes before in that b ~ z implies k2 ~ *. I'm sure we could do
2209 some analysis that could eliminate k2 ~ *. But we don't do this
2210 yet.)
2211
2212 The data con signature has already been fully kind-checked.
2213 The return type
2214
2215 T x1 * (Proxy (y :: x1), z) z
2216 becomes
2217 qtkvs = [x1 :: *, y :: x1, z :: *]
2218 res_tmpl = T x1 * (Proxy x1 y, z) z
2219
2220 We start off by matching (T k1 k2 a b) with (T x1 * (Proxy x1 y, z) z). We
2221 know this match will succeed because of the validity check (actually done
2222 later, but laziness saves us -- see Note [Checking GADT return types]).
2223 Thus, we get
2224
2225 subst := { k1 |-> x1, k2 |-> *, a |-> (Proxy x1 y, z), b |-> z }
2226
2227 Now, we need to figure out what the GADT equalities should be. In this case,
2228 we *don't* want (k1 ~ x1) to be a GADT equality: it should just be a
2229 renaming. The others should be GADT equalities. We also need to make
2230 sure that the universally-quantified variables of the datacon match up
2231 with the tyvars of the tycon, as required for Core context well-formedness.
2232 (This last bit is why we have to rejig at all!)
2233
2234 `choose` walks down the tycon tyvars, figuring out what to do with each one.
2235 It carries two substitutions:
2236 - t_sub's domain is *template* or *tycon* tyvars, mapping them to variables
2237 mentioned in the datacon signature.
2238 - r_sub's domain is *result* tyvars, names written by the programmer in
2239 the datacon signature. The final rejigged type will use these names, but
2240 the subst is still needed because sometimes the printed name of these variables
2241 is different. (See choose_tv_name, below.)
2242
2243 Before explaining the details of `choose`, let's just look at its operation
2244 on our example:
2245
2246 choose [] [] {} {} [k1, k2, a, b]
2247 --> -- first branch of `case` statement
2248 choose
2249 univs: [x1 :: *]
2250 eq_spec: []
2251 t_sub: {k1 |-> x1}
2252 r_sub: {x1 |-> x1}
2253 t_tvs: [k2, a, b]
2254 --> -- second branch of `case` statement
2255 choose
2256 univs: [k2 :: *, x1 :: *]
2257 eq_spec: [k2 ~ *]
2258 t_sub: {k1 |-> x1, k2 |-> k2}
2259 r_sub: {x1 |-> x1}
2260 t_tvs: [a, b]
2261 --> -- second branch of `case` statement
2262 choose
2263 univs: [a :: k2, k2 :: *, x1 :: *]
2264 eq_spec: [ a ~ (Proxy x1 y, z)
2265 , k2 ~ * ]
2266 t_sub: {k1 |-> x1, k2 |-> k2, a |-> a}
2267 r_sub: {x1 |-> x1}
2268 t_tvs: [b]
2269 --> -- second branch of `case` statement
2270 choose
2271 univs: [b :: k2, a :: k2, k2 :: *, x1 :: *]
2272 eq_spec: [ b ~ z
2273 , a ~ (Proxy x1 y, z)
2274 , k2 ~ * ]
2275 t_sub: {k1 |-> x1, k2 |-> k2, a |-> a, b |-> z}
2276 r_sub: {x1 |-> x1}
2277 t_tvs: []
2278 --> -- end of recursion
2279 ( [x1 :: *, k2 :: *, a :: k2, b :: k2]
2280 , [k2 ~ *, a ~ (Proxy x1 y, z), b ~ z]
2281 , {x1 |-> x1} )
2282
2283 `choose` looks up each tycon tyvar in the matching (it *must* be matched!).
2284
2285 * If it finds a bare result tyvar (the first branch of the `case`
2286 statement), it checks to make sure that the result tyvar isn't yet
2287 in the list of univ_tvs. If it is in that list, then we have a
2288 repeated variable in the return type, and we in fact need a GADT
2289 equality.
2290
2291 * It then checks to make sure that the kind of the result tyvar
2292 matches the kind of the template tyvar. This check is what forces
2293 `z` to be existential, as it should be, explained above.
2294
2295 * Assuming no repeated variables or kind-changing, we wish to use the
2296 variable name given in the datacon signature (that is, `x1` not
2297 `k1`), not the tycon signature (which may have been made up by
2298 GHC). So, we add a mapping from the tycon tyvar to the result tyvar
2299 to t_sub.
2300
2301 * If we discover that a mapping in `subst` gives us a non-tyvar (the
2302 second branch of the `case` statement), then we have a GADT equality
2303 to create. We create a fresh equality, but we don't extend any
2304 substitutions. The template variable substitution is meant for use
2305 in universal tyvar kinds, and these shouldn't be affected by any
2306 GADT equalities.
2307
2308 This whole algorithm is quite delicate, indeed. I (Richard E.) see two ways
2309 of simplifying it:
2310
2311 1) The first branch of the `case` statement is really an optimization, used
2312 in order to get fewer GADT equalities. It might be possible to make a GADT
2313 equality for *every* univ. tyvar, even if the equality is trivial, and then
2314 either deal with the bigger type or somehow reduce it later.
2315
2316 2) This algorithm strives to use the names for type variables as specified
2317 by the user in the datacon signature. If we always used the tycon tyvar
2318 names, for example, this would be simplified. This change would almost
2319 certainly degrade error messages a bit, though.
2320 -}
2321
2322 -- ^ From information about a source datacon definition, extract out
2323 -- what the universal variables and the GADT equalities should be.
2324 -- See Note [mkGADTVars].
2325 mkGADTVars :: [TyVar] -- ^ The tycon vars
2326 -> [TyVar] -- ^ The datacon vars
2327 -> TCvSubst -- ^ The matching between the template result type
2328 -- and the actual result type
2329 -> ( [TyVar]
2330 , [EqSpec]
2331 , TCvSubst ) -- ^ The univ. variables, the GADT equalities,
2332 -- and a subst to apply to the GADT equalities
2333 -- and existentials.
2334 mkGADTVars tmpl_tvs dc_tvs subst
2335 = choose [] [] empty_subst empty_subst tmpl_tvs
2336 where
2337 in_scope = mkInScopeSet (mkVarSet tmpl_tvs `unionVarSet` mkVarSet dc_tvs)
2338 `unionInScope` getTCvInScope subst
2339 empty_subst = mkEmptyTCvSubst in_scope
2340
2341 choose :: [TyVar] -- accumulator of univ tvs, reversed
2342 -> [EqSpec] -- accumulator of GADT equalities, reversed
2343 -> TCvSubst -- template substitution
2344 -> TCvSubst -- res. substitution
2345 -> [TyVar] -- template tvs (the univ tvs passed in)
2346 -> ( [TyVar] -- the univ_tvs
2347 , [EqSpec] -- GADT equalities
2348 , TCvSubst ) -- a substitution to fix kinds in ex_tvs
2349
2350 choose univs eqs _t_sub r_sub []
2351 = (reverse univs, reverse eqs, r_sub)
2352 choose univs eqs t_sub r_sub (t_tv:t_tvs)
2353 | Just r_ty <- lookupTyVar subst t_tv
2354 = case getTyVar_maybe r_ty of
2355 Just r_tv
2356 | not (r_tv `elem` univs)
2357 , tyVarKind r_tv `eqType` (substTy t_sub (tyVarKind t_tv))
2358 -> -- simple, well-kinded variable substitution.
2359 choose (r_tv:univs) eqs
2360 (extendTvSubst t_sub t_tv r_ty')
2361 (extendTvSubst r_sub r_tv r_ty')
2362 t_tvs
2363 where
2364 r_tv1 = setTyVarName r_tv (choose_tv_name r_tv t_tv)
2365 r_ty' = mkTyVarTy r_tv1
2366
2367 -- Not a simple substitution: make an equality predicate
2368 _ -> choose (t_tv':univs) (mkEqSpec t_tv' r_ty : eqs)
2369 (extendTvSubst t_sub t_tv (mkTyVarTy t_tv'))
2370 -- We've updated the kind of t_tv,
2371 -- so add it to t_sub (Trac #14162)
2372 r_sub t_tvs
2373 where
2374 t_tv' = updateTyVarKind (substTy t_sub) t_tv
2375
2376 | otherwise
2377 = pprPanic "mkGADTVars" (ppr tmpl_tvs $$ ppr subst)
2378
2379 -- choose an appropriate name for a univ tyvar.
2380 -- This *must* preserve the Unique of the result tv, so that we
2381 -- can detect repeated variables. It prefers user-specified names
2382 -- over system names. A result variable with a system name can
2383 -- happen with GHC-generated implicit kind variables.
2384 choose_tv_name :: TyVar -> TyVar -> Name
2385 choose_tv_name r_tv t_tv
2386 | isSystemName r_tv_name
2387 = setNameUnique t_tv_name (getUnique r_tv_name)
2388
2389 | otherwise
2390 = r_tv_name
2391
2392 where
2393 r_tv_name = getName r_tv
2394 t_tv_name = getName t_tv
2395
2396 {-
2397 Note [Substitution in template variables kinds]
2398 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2399
2400 data G (a :: Maybe k) where
2401 MkG :: G Nothing
2402
2403 With explicit kind variables
2404
2405 data G k (a :: Maybe k) where
2406 MkG :: G k1 (Nothing k1)
2407
2408 Note how k1 is distinct from k. So, when we match the template
2409 `G k a` against `G k1 (Nothing k1)`, we get a subst
2410 [ k |-> k1, a |-> Nothing k1 ]. Even though this subst has two
2411 mappings, we surely don't want to add (k, k1) to the list of
2412 GADT equalities -- that would be overly complex and would create
2413 more untouchable variables than we need. So, when figuring out
2414 which tyvars are GADT-like and which aren't (the fundamental
2415 job of `choose`), we want to treat `k` as *not* GADT-like.
2416 Instead, we wish to substitute in `a`'s kind, to get (a :: Maybe k1)
2417 instead of (a :: Maybe k). This is the reason for dealing
2418 with a substitution in here.
2419
2420 However, we do not *always* want to substitute. Consider
2421
2422 data H (a :: k) where
2423 MkH :: H Int
2424
2425 With explicit kind variables:
2426
2427 data H k (a :: k) where
2428 MkH :: H * Int
2429
2430 Here, we have a kind-indexed GADT. The subst in question is
2431 [ k |-> *, a |-> Int ]. Now, we *don't* want to substitute in `a`'s
2432 kind, because that would give a constructor with the type
2433
2434 MkH :: forall (k :: *) (a :: *). (k ~ *) -> (a ~ Int) -> H k a
2435
2436 The problem here is that a's kind is wrong -- it needs to be k, not *!
2437 So, if the matching for a variable is anything but another bare variable,
2438 we drop the mapping from the substitution before proceeding. This
2439 was not an issue before kind-indexed GADTs because this case could
2440 never happen.
2441
2442 ************************************************************************
2443 * *
2444 Validity checking
2445 * *
2446 ************************************************************************
2447
2448 Validity checking is done once the mutually-recursive knot has been
2449 tied, so we can look at things freely.
2450 -}
2451
2452 checkValidTyCl :: TyCon -> TcM [TyCon]
2453 -- The returned list is either a singleton (if valid)
2454 -- or a list of "fake tycons" (if not); the fake tycons
2455 -- include any implicits, like promoted data constructors
2456 -- See Note [Recover from validity error]
2457 checkValidTyCl tc
2458 = setSrcSpan (getSrcSpan tc) $
2459 addTyConCtxt tc $
2460 recoverM recovery_code
2461 (do { traceTc "Starting validity for tycon" (ppr tc)
2462 ; checkValidTyCon tc
2463 ; traceTc "Done validity for tycon" (ppr tc)
2464 ; return [tc] })
2465 where
2466 recovery_code -- See Note [Recover from validity error]
2467 = do { traceTc "Aborted validity for tycon" (ppr tc)
2468 ; return (concatMap mk_fake_tc $
2469 ATyCon tc : implicitTyConThings tc) }
2470
2471 mk_fake_tc (ATyCon tc)
2472 | isClassTyCon tc = [tc] -- Ugh! Note [Recover from validity error]
2473 | otherwise = [makeRecoveryTyCon tc]
2474 mk_fake_tc (AConLike (RealDataCon dc))
2475 = [makeRecoveryTyCon (promoteDataCon dc)]
2476 mk_fake_tc _ = []
2477
2478 {- Note [Recover from validity error]
2479 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2480 We recover from a validity error in a type or class, which allows us
2481 to report multiple validity errors. In the failure case we return a
2482 TyCon of the right kind, but with no interesting behaviour
2483 (makeRecoveryTyCon). Why? Suppose we have
2484 type T a = Fun
2485 where Fun is a type family of arity 1. The RHS is invalid, but we
2486 want to go on checking validity of subsequent type declarations.
2487 So we replace T with an abstract TyCon which will do no harm.
2488 See indexed-types/should_fail/BadSock and Trac #10896
2489
2490 Some notes:
2491
2492 * We must make fakes for promoted DataCons too. Consider (Trac #15215)
2493 data T a = MkT ...
2494 data S a = ...T...MkT....
2495 If there is an error in the definition of 'T' we add a "fake type
2496 constructor" to the type environment, so that we can continue to
2497 typecheck 'S'. But we /were not/ adding a fake anything for 'MkT'
2498 and so there was an internal error when we met 'MkT' in the body of
2499 'S'.
2500
2501 * Painfully, we *don't* want to do this for classes.
2502 Consider tcfail041:
2503 class (?x::Int) => C a where ...
2504 instance C Int
2505 The class is invalid because of the superclass constraint. But
2506 we still want it to look like a /class/, else the instance bleats
2507 that the instance is mal-formed because it hasn't got a class in
2508 the head.
2509
2510 This is really bogus; now we have in scope a Class that is invalid
2511 in some way, with unknown downstream consequences. A better
2512 alterantive might be to make a fake class TyCon. A job for another day.
2513 -}
2514
2515 -------------------------
2516 -- For data types declared with record syntax, we require
2517 -- that each constructor that has a field 'f'
2518 -- (a) has the same result type
2519 -- (b) has the same type for 'f'
2520 -- module alpha conversion of the quantified type variables
2521 -- of the constructor.
2522 --
2523 -- Note that we allow existentials to match because the
2524 -- fields can never meet. E.g
2525 -- data T where
2526 -- T1 { f1 :: b, f2 :: a, f3 ::Int } :: T
2527 -- T2 { f1 :: c, f2 :: c, f3 ::Int } :: T
2528 -- Here we do not complain about f1,f2 because they are existential
2529
2530 checkValidTyCon :: TyCon -> TcM ()
2531 checkValidTyCon tc
2532 | isPrimTyCon tc -- Happens when Haddock'ing GHC.Prim
2533 = return ()
2534
2535 | otherwise
2536 = do { traceTc "checkValidTyCon" (ppr tc $$ ppr (tyConClass_maybe tc))
2537 ; if | Just cl <- tyConClass_maybe tc
2538 -> checkValidClass cl
2539
2540 | Just syn_rhs <- synTyConRhs_maybe tc
2541 -> do { checkValidType syn_ctxt syn_rhs
2542 ; checkTySynRhs syn_ctxt syn_rhs }
2543
2544 | Just fam_flav <- famTyConFlav_maybe tc
2545 -> case fam_flav of
2546 { ClosedSynFamilyTyCon (Just ax)
2547 -> tcAddClosedTypeFamilyDeclCtxt tc $
2548 checkValidCoAxiom ax
2549 ; ClosedSynFamilyTyCon Nothing -> return ()
2550 ; AbstractClosedSynFamilyTyCon ->
2551 do { hsBoot <- tcIsHsBootOrSig
2552 ; checkTc hsBoot $
2553 text "You may define an abstract closed type family" $$
2554 text "only in a .hs-boot file" }
2555 ; DataFamilyTyCon {} -> return ()
2556 ; OpenSynFamilyTyCon -> return ()
2557 ; BuiltInSynFamTyCon _ -> return () }
2558
2559 | otherwise -> do
2560 { -- Check the context on the data decl
2561 traceTc "cvtc1" (ppr tc)
2562 ; checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc)
2563
2564 ; traceTc "cvtc2" (ppr tc)
2565
2566 ; dflags <- getDynFlags
2567 ; existential_ok <- xoptM LangExt.ExistentialQuantification
2568 ; gadt_ok <- xoptM LangExt.GADTs
2569 ; let ex_ok = existential_ok || gadt_ok
2570 -- Data cons can have existential context
2571 ; mapM_ (checkValidDataCon dflags ex_ok tc) data_cons
2572 ; mapM_ (checkPartialRecordField data_cons) (tyConFieldLabels tc)
2573
2574 -- Check that fields with the same name share a type
2575 ; mapM_ check_fields groups }}
2576 where
2577 syn_ctxt = TySynCtxt name
2578 name = tyConName tc
2579 data_cons = tyConDataCons tc
2580
2581 groups = equivClasses cmp_fld (concatMap get_fields data_cons)
2582 cmp_fld (f1,_) (f2,_) = flLabel f1 `compare` flLabel f2
2583 get_fields con = dataConFieldLabels con `zip` repeat con
2584 -- dataConFieldLabels may return the empty list, which is fine
2585
2586 -- See Note [GADT record selectors] in TcTyDecls
2587 -- We must check (a) that the named field has the same
2588 -- type in each constructor
2589 -- (b) that those constructors have the same result type
2590 --
2591 -- However, the constructors may have differently named type variable
2592 -- and (worse) we don't know how the correspond to each other. E.g.
2593 -- C1 :: forall a b. { f :: a, g :: b } -> T a b
2594 -- C2 :: forall d c. { f :: c, g :: c } -> T c d
2595 --
2596 -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
2597 -- result type against other candidates' types BOTH WAYS ROUND.
2598 -- If they magically agrees, take the substitution and
2599 -- apply them to the latter ones, and see if they match perfectly.
2600 check_fields ((label, con1) :| other_fields)
2601 -- These fields all have the same name, but are from
2602 -- different constructors in the data type
2603 = recoverM (return ()) $ mapM_ checkOne other_fields
2604 -- Check that all the fields in the group have the same type
2605 -- NB: this check assumes that all the constructors of a given
2606 -- data type use the same type variables
2607 where
2608 (_, _, _, res1) = dataConSig con1
2609 fty1 = dataConFieldType con1 lbl
2610 lbl = flLabel label
2611
2612 checkOne (_, con2) -- Do it both ways to ensure they are structurally identical
2613 = do { checkFieldCompat lbl con1 con2 res1 res2 fty1 fty2
2614 ; checkFieldCompat lbl con2 con1 res2 res1 fty2 fty1 }
2615 where
2616 (_, _, _, res2) = dataConSig con2
2617 fty2 = dataConFieldType con2 lbl
2618
2619 checkPartialRecordField :: [DataCon] -> FieldLabel -> TcM ()
2620 -- Checks the partial record field selector, and warns.
2621 -- See Note [Checking partial record field]
2622 checkPartialRecordField all_cons fld
2623 = setSrcSpan loc $
2624 warnIfFlag Opt_WarnPartialFields
2625 (not is_exhaustive && not (startsWithUnderscore occ_name))
2626 (sep [text "Use of partial record field selector" <> colon,
2627 nest 2 $ quotes (ppr occ_name)])
2628 where
2629 sel_name = flSelector fld
2630 loc = getSrcSpan sel_name
2631 occ_name = getOccName sel_name
2632
2633 (cons_with_field, cons_without_field) = partition has_field all_cons
2634 has_field con = fld `elem` (dataConFieldLabels con)
2635 is_exhaustive = all (dataConCannotMatch inst_tys) cons_without_field
2636
2637 con1 = ASSERT( not (null cons_with_field) ) head cons_with_field
2638 (univ_tvs, _, eq_spec, _, _, _) = dataConFullSig con1
2639 eq_subst = mkTvSubstPrs (map eqSpecPair eq_spec)
2640 inst_tys = substTyVars eq_subst univ_tvs
2641
2642 checkFieldCompat :: FieldLabelString -> DataCon -> DataCon
2643 -> Type -> Type -> Type -> Type -> TcM ()
2644 checkFieldCompat fld con1 con2 res1 res2 fty1 fty2
2645 = do { checkTc (isJust mb_subst1) (resultTypeMisMatch fld con1 con2)
2646 ; checkTc (isJust mb_subst2) (fieldTypeMisMatch fld con1 con2) }
2647 where
2648 mb_subst1 = tcMatchTy res1 res2
2649 mb_subst2 = tcMatchTyX (expectJust "checkFieldCompat" mb_subst1) fty1 fty2
2650
2651 -------------------------------
2652 checkValidDataCon :: DynFlags -> Bool -> TyCon -> DataCon -> TcM ()
2653 checkValidDataCon dflags existential_ok tc con
2654 = setSrcSpan (getSrcSpan con) $
2655 addErrCtxt (dataConCtxt con) $
2656 do { -- Check that the return type of the data constructor
2657 -- matches the type constructor; eg reject this:
2658 -- data T a where { MkT :: Bogus a }
2659 -- It's important to do this first:
2660 -- see Note [Checking GADT return types]
2661 -- and c.f. Note [Check role annotations in a second pass]
2662 let tc_tvs = tyConTyVars tc
2663 res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs)
2664 orig_res_ty = dataConOrigResTy con
2665 ; traceTc "checkValidDataCon" (vcat
2666 [ ppr con, ppr tc, ppr tc_tvs
2667 , ppr res_ty_tmpl <+> dcolon <+> ppr (typeKind res_ty_tmpl)
2668 , ppr orig_res_ty <+> dcolon <+> ppr (typeKind orig_res_ty)])
2669
2670
2671 ; checkTc (isJust (tcMatchTy res_ty_tmpl
2672 orig_res_ty))
2673 (badDataConTyCon con res_ty_tmpl orig_res_ty)
2674 -- Note that checkTc aborts if it finds an error. This is
2675 -- critical to avoid panicking when we call dataConUserType
2676 -- on an un-rejiggable datacon!
2677
2678 ; traceTc "checkValidDataCon 2" (ppr (dataConUserType con))
2679
2680 -- Check that the result type is a *monotype*
2681 -- e.g. reject this: MkT :: T (forall a. a->a)
2682 -- Reason: it's really the argument of an equality constraint
2683 ; checkValidMonoType orig_res_ty
2684
2685 -- Check all argument types for validity
2686 ; checkValidType ctxt (dataConUserType con)
2687 ; mapM_ (checkForLevPoly empty)
2688 (dataConOrigArgTys con)
2689
2690 -- Extra checks for newtype data constructors
2691 ; when (isNewTyCon tc) (checkNewDataCon con)
2692
2693 -- Check that existentials are allowed if they are used
2694 ; checkTc (existential_ok || isVanillaDataCon con)
2695 (badExistential con)
2696
2697 -- Check that UNPACK pragmas and bangs work out
2698 -- E.g. reject data T = MkT {-# UNPACK #-} Int -- No "!"
2699 -- data T = MkT {-# UNPACK #-} !a -- Can't unpack
2700 ; zipWith3M_ check_bang (dataConSrcBangs con) (dataConImplBangs con) [1..]
2701
2702 ; traceTc "Done validity of data con" $
2703 vcat [ ppr con
2704 , text "Datacon user type:" <+> ppr (dataConUserType con)
2705 , text "Datacon rep type:" <+> ppr (dataConRepType con)
2706 , text "Rep typcon binders:" <+> ppr (tyConBinders (dataConTyCon con))
2707 , case tyConFamInst_maybe (dataConTyCon con) of
2708 Nothing -> text "not family"
2709 Just (f, _) -> ppr (tyConBinders f) ]
2710 }
2711 where
2712 ctxt = ConArgCtxt (dataConName con)
2713
2714 check_bang :: HsSrcBang -> HsImplBang -> Int -> TcM ()
2715 check_bang (HsSrcBang _ _ SrcLazy) _ n
2716 | not (xopt LangExt.StrictData dflags)
2717 = addErrTc
2718 (bad_bang n (text "Lazy annotation (~) without StrictData"))
2719 check_bang (HsSrcBang _ want_unpack strict_mark) rep_bang n
2720 | isSrcUnpacked want_unpack, not is_strict
2721 = addWarnTc NoReason (bad_bang n (text "UNPACK pragma lacks '!'"))
2722 | isSrcUnpacked want_unpack
2723 , case rep_bang of { HsUnpack {} -> False; _ -> True }
2724 -- If not optimising, we don't unpack (rep_bang is never
2725 -- HsUnpack), so don't complain! This happens, e.g., in Haddock.
2726 -- See dataConSrcToImplBang.
2727 , not (gopt Opt_OmitInterfacePragmas dflags)
2728 -- When typechecking an indefinite package in Backpack, we
2729 -- may attempt to UNPACK an abstract type. The test here will
2730 -- conclude that this is unusable, but it might become usable
2731 -- when we actually fill in the abstract type. As such, don't
2732 -- warn in this case (it gives users the wrong idea about whether
2733 -- or not UNPACK on abstract types is supported; it is!)
2734 , unitIdIsDefinite (thisPackage dflags)
2735 = addWarnTc NoReason (bad_bang n (text "Ignoring unusable UNPACK pragma"))
2736 where
2737 is_strict = case strict_mark of
2738 NoSrcStrict -> xopt LangExt.StrictData dflags
2739 bang -> isSrcStrict bang
2740
2741 check_bang _ _ _
2742 = return ()
2743
2744 bad_bang n herald
2745 = hang herald 2 (text "on the" <+> speakNth n
2746 <+> text "argument of" <+> quotes (ppr con))
2747 -------------------------------
2748 checkNewDataCon :: DataCon -> TcM ()
2749 -- Further checks for the data constructor of a newtype
2750 checkNewDataCon con
2751 = do { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
2752 -- One argument
2753
2754 ; checkTc (not (isUnliftedType arg_ty1)) $
2755 text "A newtype cannot have an unlifted argument type"
2756
2757 ; check_con (null eq_spec) $
2758 text "A newtype constructor must have a return type of form T a1 ... an"
2759 -- Return type is (T a b c)
2760
2761 ; check_con (null theta) $
2762 text "A newtype constructor cannot have a context in its type"
2763
2764 ; check_con (null ex_tvs) $
2765 text "A newtype constructor cannot have existential type variables"
2766 -- No existentials
2767
2768 ; checkTc (all ok_bang (dataConSrcBangs con))
2769 (newtypeStrictError con)
2770 -- No strictness annotations
2771 }
2772 where
2773 (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
2774 = dataConFullSig con
2775 check_con what msg
2776 = checkTc what (msg $$ ppr con <+> dcolon <+> ppr (dataConUserType con))
2777
2778 (arg_ty1 : _) = arg_tys
2779
2780 ok_bang (HsSrcBang _ _ SrcStrict) = False
2781 ok_bang (HsSrcBang _ _ SrcLazy) = False
2782 ok_bang _ = True
2783
2784 -------------------------------
2785 checkValidClass :: Class -> TcM ()
2786 checkValidClass cls
2787 = do { constrained_class_methods <- xoptM LangExt.ConstrainedClassMethods
2788 ; multi_param_type_classes <- xoptM LangExt.MultiParamTypeClasses
2789 ; nullary_type_classes <- xoptM LangExt.NullaryTypeClasses
2790 ; fundep_classes <- xoptM LangExt.FunctionalDependencies
2791 ; undecidable_super_classes <- xoptM LangExt.UndecidableSuperClasses
2792
2793 -- Check that the class is unary, unless multiparameter type classes
2794 -- are enabled; also recognize deprecated nullary type classes
2795 -- extension (subsumed by multiparameter type classes, Trac #8993)
2796 ; checkTc (multi_param_type_classes || cls_arity == 1 ||
2797 (nullary_type_classes && cls_arity == 0))
2798 (classArityErr cls_arity cls)
2799 ; checkTc (fundep_classes || null fundeps) (classFunDepsErr cls)
2800
2801 -- Check the super-classes
2802 ; checkValidTheta (ClassSCCtxt (className cls)) theta
2803
2804 -- Now check for cyclic superclasses
2805 -- If there are superclass cycles, checkClassCycleErrs bails.
2806 ; unless undecidable_super_classes $
2807 case checkClassCycles cls of
2808 Just err -> setSrcSpan (getSrcSpan cls) $
2809 addErrTc err
2810 Nothing -> return ()
2811
2812 -- Check the class operations.
2813 -- But only if there have been no earlier errors
2814 -- See Note [Abort when superclass cycle is detected]
2815 ; whenNoErrs $
2816 mapM_ (check_op constrained_class_methods) op_stuff
2817
2818 -- Check the associated type defaults are well-formed and instantiated
2819 ; mapM_ check_at at_stuff }
2820 where
2821 (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls
2822 cls_arity = length (tyConVisibleTyVars (classTyCon cls))
2823 -- Ignore invisible variables
2824 cls_tv_set = mkVarSet tyvars
2825 mini_env = zipVarEnv tyvars (mkTyVarTys tyvars)
2826 mb_cls = Just (cls, tyvars, mini_env)
2827
2828 check_op constrained_class_methods (sel_id, dm)
2829 = setSrcSpan (getSrcSpan sel_id) $
2830 addErrCtxt (classOpCtxt sel_id op_ty) $ do
2831 { traceTc "class op type" (ppr op_ty)
2832 ; checkValidType ctxt op_ty
2833 -- This implements the ambiguity check, among other things
2834 -- Example: tc223
2835 -- class Error e => Game b mv e | b -> mv e where
2836 -- newBoard :: MonadState b m => m ()
2837 -- Here, MonadState has a fundep m->b, so newBoard is fine
2838
2839 -- a method cannot be levity polymorphic, as we have to store the
2840 -- method in a dictionary
2841 -- example of what this prevents:
2842 -- class BoundedX (a :: TYPE r) where minBound :: a
2843 -- See Note [Levity polymorphism checking] in DsMonad
2844 ; checkForLevPoly empty tau1
2845
2846 ; unless constrained_class_methods $
2847 mapM_ check_constraint (tail (cls_pred:op_theta))
2848
2849 ; check_dm ctxt sel_id cls_pred tau2 dm
2850 }
2851 where
2852 ctxt = FunSigCtxt op_name True -- Report redundant class constraints
2853 op_name = idName sel_id
2854 op_ty = idType sel_id
2855 (_,cls_pred,tau1) = tcSplitMethodTy op_ty
2856 -- See Note [Splitting nested sigma types in class type signatures]
2857 (_,op_theta,tau2) = tcSplitNestedSigmaTys tau1
2858
2859 check_constraint :: TcPredType -> TcM ()
2860 check_constraint pred -- See Note [Class method constraints]
2861 = when (not (isEmptyVarSet pred_tvs) &&
2862 pred_tvs `subVarSet` cls_tv_set)
2863 (addErrTc (badMethPred sel_id pred))
2864 where
2865 pred_tvs = tyCoVarsOfType pred
2866
2867 check_at (ATI fam_tc m_dflt_rhs)
2868 = do { checkTc (cls_arity == 0 || any (`elemVarSet` cls_tv_set) fam_tvs)
2869 (noClassTyVarErr cls fam_tc)
2870 -- Check that the associated type mentions at least
2871 -- one of the class type variables
2872 -- The check is disabled for nullary type classes,
2873 -- since there is no possible ambiguity (Trac #10020)
2874
2875 -- Check that any default declarations for associated types are valid
2876 ; whenIsJust m_dflt_rhs $ \ (rhs, loc) ->
2877 checkValidTyFamEqn mb_cls fam_tc
2878 fam_tvs [] (mkTyVarTys fam_tvs) rhs pp_lhs loc }
2879 where
2880 fam_tvs = tyConTyVars fam_tc
2881 pp_lhs = ppr (mkTyConApp fam_tc (mkTyVarTys fam_tvs))
2882
2883 check_dm :: UserTypeCtxt -> Id -> PredType -> Type -> DefMethInfo -> TcM ()
2884 -- Check validity of the /top-level/ generic-default type
2885 -- E.g for class C a where
2886 -- default op :: forall b. (a~b) => blah
2887 -- we do not want to do an ambiguity check on a type with
2888 -- a free TyVar 'a' (Trac #11608). See TcType
2889 -- Note [TyVars and TcTyVars during type checking] in TcType
2890 -- Hence the mkDefaultMethodType to close the type.
2891 check_dm ctxt sel_id vanilla_cls_pred vanilla_tau
2892 (Just (dm_name, dm_spec@(GenericDM dm_ty)))
2893 = setSrcSpan (getSrcSpan dm_name) $ do
2894 -- We have carefully set the SrcSpan on the generic
2895 -- default-method Name to be that of the generic
2896 -- default type signature
2897
2898 -- First, we check that that the method's default type signature
2899 -- aligns with the non-default type signature.
2900 -- See Note [Default method type signatures must align]
2901 let cls_pred = mkClassPred cls $ mkTyVarTys $ classTyVars cls
2902 -- Note that the second field of this tuple contains the context
2903 -- of the default type signature, making it apparent that we
2904 -- ignore method contexts completely when validity-checking
2905 -- default type signatures. See the end of
2906 -- Note [Default method type signatures must align]
2907 -- to learn why this is OK.
2908 --
2909 -- See also
2910 -- Note [Splitting nested sigma types in class type signatures]
2911 -- for an explanation of why we don't use tcSplitSigmaTy here.
2912 (_, _, dm_tau) = tcSplitNestedSigmaTys dm_ty
2913
2914 -- Given this class definition:
2915 --
2916 -- class C a b where
2917 -- op :: forall p q. (Ord a, D p q)
2918 -- => a -> b -> p -> (a, b)
2919 -- default op :: forall r s. E r
2920 -- => a -> b -> s -> (a, b)
2921 --
2922 -- We want to match up two types of the form:
2923 --
2924 -- Vanilla type sig: C aa bb => aa -> bb -> p -> (aa, bb)
2925 -- Default type sig: C a b => a -> b -> s -> (a, b)
2926 --
2927 -- Notice that the two type signatures can be quantified over
2928 -- different class type variables! Therefore, it's important that
2929 -- we include the class predicate parts to match up a with aa and
2930 -- b with bb.
2931 vanilla_phi_ty = mkPhiTy [vanilla_cls_pred] vanilla_tau
2932 dm_phi_ty = mkPhiTy [cls_pred] dm_tau
2933
2934 traceTc "check_dm" $ vcat
2935 [ text "vanilla_phi_ty" <+> ppr vanilla_phi_ty
2936 , text "dm_phi_ty" <+> ppr dm_phi_ty ]
2937
2938 -- Actually checking that the types align is done with a call to
2939 -- tcMatchTys. We need to get a match in both directions to rule
2940 -- out degenerate cases like these:
2941 --
2942 -- class Foo a where
2943 -- foo1 :: a -> b
2944 -- default foo1 :: a -> Int
2945 --
2946 -- foo2 :: a -> Int
2947 -- default foo2 :: a -> b
2948 unless (isJust $ tcMatchTys [dm_phi_ty, vanilla_phi_ty]
2949 [vanilla_phi_ty, dm_phi_ty]) $ addErrTc $
2950 hang (text "The default type signature for"
2951 <+> ppr sel_id <> colon)
2952 2 (ppr dm_ty)
2953 $$ (text "does not match its corresponding"
2954 <+> text "non-default type signature")
2955
2956 -- Now do an ambiguity check on the default type signature.
2957 checkValidType ctxt (mkDefaultMethodType cls sel_id dm_spec)
2958 check_dm _ _ _ _ _ = return ()
2959
2960 checkFamFlag :: Name -> TcM ()
2961 -- Check that we don't use families without -XTypeFamilies
2962 -- The parser won't even parse them, but I suppose a GHC API
2963 -- client might have a go!
2964 checkFamFlag tc_name
2965 = do { idx_tys <- xoptM LangExt.TypeFamilies
2966 ; checkTc idx_tys err_msg }
2967 where
2968 err_msg = hang (text "Illegal family declaration for" <+> quotes (ppr tc_name))
2969 2 (text "Enable TypeFamilies to allow indexed type families")
2970
2971 {- Note [Class method constraints]
2972 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2973 Haskell 2010 is supposed to reject
2974 class C a where
2975 op :: Eq a => a -> a
2976 where the method type constrains only the class variable(s). (The extension
2977 -XConstrainedClassMethods switches off this check.) But regardless
2978 we should not reject
2979 class C a where
2980 op :: (?x::Int) => a -> a
2981 as pointed out in Trac #11793. So the test here rejects the program if
2982 * -XConstrainedClassMethods is off
2983 * the tyvars of the constraint are non-empty
2984 * all the tyvars are class tyvars, none are locally quantified
2985
2986 Note [Abort when superclass cycle is detected]
2987 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2988 We must avoid doing the ambiguity check for the methods (in
2989 checkValidClass.check_op) when there are already errors accumulated.
2990 This is because one of the errors may be a superclass cycle, and
2991 superclass cycles cause canonicalization to loop. Here is a
2992 representative example:
2993
2994 class D a => C a where
2995 meth :: D a => ()
2996 class C a => D a
2997
2998 This fixes Trac #9415, #9739
2999
3000 Note [Default method type signatures must align]
3001 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3002 GHC enforces the invariant that a class method's default type signature
3003 must "align" with that of the method's non-default type signature, as per
3004 GHC Trac #12918. For instance, if you have:
3005
3006 class Foo a where
3007 bar :: forall b. Context => a -> b
3008
3009 Then a default type signature for bar must be alpha equivalent to
3010 (forall b. a -> b). That is, the types must be the same modulo differences in
3011 contexts. So the following would be acceptable default type signatures:
3012
3013 default bar :: forall b. Context1 => a -> b
3014 default bar :: forall x. Context2 => a -> x
3015
3016 But the following are NOT acceptable default type signatures:
3017
3018 default bar :: forall b. b -> a
3019 default bar :: forall x. x
3020 default bar :: a -> Int
3021
3022 Note that a is bound by the class declaration for Foo itself, so it is
3023 not allowed to differ in the default type signature.
3024
3025 The default type signature (default bar :: a -> Int) deserves special mention,
3026 since (a -> Int) is a straightforward instantiation of (forall b. a -> b). To
3027 write this, you need to declare the default type signature like so:
3028
3029 default bar :: forall b. (b ~ Int). a -> b
3030
3031 As noted in #12918, there are several reasons to do this:
3032
3033 1. It would make no sense to have a type that was flat-out incompatible with
3034 the non-default type signature. For instance, if you had:
3035
3036 class Foo a where
3037 bar :: a -> Int
3038 default bar :: a -> Bool
3039
3040 Then that would always fail in an instance declaration. So this check
3041 nips such cases in the bud before they have the chance to produce
3042 confusing error messages.
3043
3044 2. Internally, GHC uses TypeApplications to instantiate the default method in
3045 an instance. See Note [Default methods in instances] in TcInstDcls.
3046 Thus, GHC needs to know exactly what the universally quantified type
3047 variables are, and when instantiated that way, the default method's type
3048 must match the expected type.
3049
3050 3. Aesthetically, by only allowing the default type signature to differ in its
3051 context, we are making it more explicit the ways in which the default type
3052 signature is less polymorphic than the non-default type signature.
3053
3054 You might be wondering: why are the contexts allowed to be different, but not
3055 the rest of the type signature? That's because default implementations often
3056 rely on assumptions that the more general, non-default type signatures do not.
3057 For instance, in the Enum class declaration:
3058
3059 class Enum a where
3060 enum :: [a]
3061 default enum :: (Generic a, GEnum (Rep a)) => [a]
3062 enum = map to genum
3063
3064 class GEnum f where
3065 genum :: [f a]
3066
3067 The default implementation for enum only works for types that are instances of
3068 Generic, and for which their generic Rep type is an instance of GEnum. But
3069 clearly enum doesn't _have_ to use this implementation, so naturally, the
3070 context for enum is allowed to be different to accomodate this. As a result,
3071 when we validity-check default type signatures, we ignore contexts completely.
3072
3073 Note that when checking whether two type signatures match, we must take care to
3074 split as many foralls as it takes to retrieve the tau types we which to check.
3075 See Note [Splitting nested sigma types in class type signatures].
3076
3077 Note [Splitting nested sigma types in class type signatures]
3078 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3079 Consider this type synonym and class definition:
3080
3081 type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
3082
3083 class Each s t a b where
3084 each :: Traversal s t a b
3085 default each :: (Traversable g, s ~ g a, t ~ g b) => Traversal s t a b
3086
3087 It might seem obvious that the tau types in both type signatures for `each`
3088 are the same, but actually getting GHC to conclude this is surprisingly tricky.
3089 That is because in general, the form of a class method's non-default type
3090 signature is:
3091
3092 forall a. C a => forall d. D d => E a b
3093
3094 And the general form of a default type signature is:
3095
3096 forall f. F f => E a f -- The variable `a` comes from the class
3097
3098 So it you want to get the tau types in each type signature, you might find it
3099 reasonable to call tcSplitSigmaTy twice on the non-default type signature, and
3100 call it once on the default type signature. For most classes and methods, this
3101 will work, but Each is a bit of an exceptional case. The way `each` is written,
3102 it doesn't quantify any additional type variables besides those of the Each
3103 class itself, so the non-default type signature for `each` is actually this:
3104
3105 forall s t a b. Each s t a b => Traversal s t a b
3106
3107 Notice that there _appears_ to only be one forall. But there's actually another
3108 forall lurking in the Traversal type synonym, so if you call tcSplitSigmaTy
3109 twice, you'll also go under the forall in Traversal! That is, you'll end up
3110 with:
3111
3112 (a -> f b) -> s -> f t
3113
3114 A problem arises because you only call tcSplitSigmaTy once on the default type
3115 signature for `each`, which gives you
3116
3117 Traversal s t a b
3118
3119 Or, equivalently:
3120
3121 forall f. Applicative f => (a -> f b) -> s -> f t
3122
3123 This is _not_ the same thing as (a -> f b) -> s -> f t! So now tcMatchTy will
3124 say that the tau types for `each` are not equal.
3125
3126 A solution to this problem is to use tcSplitNestedSigmaTys instead of
3127 tcSplitSigmaTy. tcSplitNestedSigmaTys will always split any foralls that it
3128 sees until it can't go any further, so if you called it on the default type
3129 signature for `each`, it would return (a -> f b) -> s -> f t like we desired.
3130
3131 Note [Checking partial record field]
3132 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3133 This check checks the partial record field selector, and warns (Trac #7169).
3134
3135 For example:
3136
3137 data T a = A { m1 :: a, m2 :: a } | B { m1 :: a }
3138
3139 The function 'm2' is partial record field, and will fail when it is applied to
3140 'B'. The warning identifies such partial fields. The check is performed at the
3141 declaration of T, not at the call-sites of m2.
3142
3143 The warning can be suppressed by prefixing the field-name with an underscore.
3144 For example:
3145
3146 data T a = A { m1 :: a, _m2 :: a } | B { m1 :: a }
3147
3148 Note [checkValidDependency]
3149 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
3150 Consider
3151
3152 data Proxy k (a :: k)
3153 data Proxy2 k a = P (Proxy k a)
3154
3155 (This is test dependent/should_fail/InferDependency.) While it seems GHC can
3156 figure out the dependency between the arguments to Proxy2, this case errors.
3157 The problem is that when we build the initial kind (getInitialKind) for
3158 a tycon, we need to decide whether an argument is dependent or not. At first,
3159 I thought we could just assume that *all* arguments are dependent, and then
3160 patch it up later. However, this causes problems in error messages (where
3161 tycon's have mysterious kinds "forall (a :: k) -> blah") and in unification
3162 (where we try to unify kappa ~ forall (a :: k) -> blah, failing because the
3163 RHS is not a tau-type). Perhaps a cleverer algorithm could sort this out
3164 (say, by storing the dependency flag in a mutable cell and by avoiding
3165 these fancy kinds in error messages depending on the extension in effect)
3166 but it doesn't seem worth it.
3167
3168 So: we choose the dependency for each argument variable once and for all
3169 in getInitialKind. This means that any dependency must be lexically manifest.
3170
3171 checkValidDependency checks to make sure that no lexically non-dependent
3172 argument actually appears in a kind. Note the example above, where the k
3173 in Proxy2 is a dependent argument, but this fact is not lexically
3174 manifest. checkValidDependency will reject. This function must be called
3175 *before* kind generalization, because kind generalization works with
3176 the result of mkTyConKind, which will think that Proxy2's kind is
3177 Type -> k -> Type, where k is unbound. (It won't use a forall for a
3178 "non-dependent" argument k.)
3179 -}
3180
3181 -- | See Note [checkValidDependency]
3182 checkValidDependency :: [TyConBinder] -- zonked
3183 -> TcKind -- zonked (result kind)
3184 -> TcM ()
3185 checkValidDependency binders res_kind
3186 = go (tyCoVarsOfType res_kind) (reverse binders)
3187 where
3188 go :: TyCoVarSet -- fvs from scope
3189 -> [TyConBinder] -- binders, in reverse order
3190 -> TcM ()
3191 go _ [] = return () -- all set
3192 go fvs (tcb : tcbs)
3193 | not (isNamedTyConBinder tcb) && tcb_var `elemVarSet` fvs
3194 = do { setSrcSpan (getSrcSpan tcb_var) $
3195 addErrTc (vcat [ text "Type constructor argument" <+> quotes (ppr tcb_var) <+>
3196 text "is used dependently."
3197 , text "Any dependent arguments must be obviously so, not inferred"
3198 , text "by the type-checker."
3199 , hang (text "Inferred argument kinds:")
3200 2 (vcat (map pp_binder binders))
3201 , text "Suggestion: use" <+> quotes (ppr tcb_var) <+>
3202 text "in a kind to make the dependency clearer." ])
3203 ; go new_fvs tcbs }
3204
3205 | otherwise
3206 = go new_fvs tcbs
3207 where
3208 new_fvs = fvs `delVarSet` tcb_var
3209 `unionVarSet` tyCoVarsOfType tcb_kind
3210
3211 tcb_var = binderVar tcb
3212 tcb_kind = tyVarKind tcb_var
3213
3214 pp_binder binder = ppr (binderVar binder) <+> dcolon <+> ppr (binderKind binder)
3215
3216 {-
3217 ************************************************************************
3218 * *
3219 Checking role validity
3220 * *
3221 ************************************************************************
3222 -}
3223
3224 checkValidRoleAnnots :: RoleAnnotEnv -> TyCon -> TcM ()
3225 checkValidRoleAnnots role_annots tc
3226 | isTypeSynonymTyCon tc = check_no_roles
3227 | isFamilyTyCon tc = check_no_roles
3228 | isAlgTyCon tc = check_roles
3229 | otherwise = return ()
3230 where
3231 -- Role annotations are given only on *explicit* variables,
3232 -- but a tycon stores roles for all variables.
3233 -- So, we drop the implicit roles (which are all Nominal, anyway).
3234 name = tyConName tc
3235 tyvars = tyConTyVars tc
3236 roles = tyConRoles tc
3237 (vis_roles, vis_vars) = unzip $ snd $
3238 partitionInvisibles tc (mkTyVarTy . snd) $
3239 zip roles tyvars
3240 role_annot_decl_maybe = lookupRoleAnnot role_annots name
3241
3242 check_roles
3243 = whenIsJust role_annot_decl_maybe $
3244 \decl@(L loc (RoleAnnotDecl _ _ the_role_annots)) ->
3245 addRoleAnnotCtxt name $
3246 setSrcSpan loc $ do
3247 { role_annots_ok <- xoptM LangExt.RoleAnnotations
3248 ; checkTc role_annots_ok $ needXRoleAnnotations tc
3249 ; checkTc (vis_vars `equalLength` the_role_annots)
3250 (wrongNumberOfRoles vis_vars decl)
3251 ; _ <- zipWith3M checkRoleAnnot vis_vars the_role_annots vis_roles
3252 -- Representational or phantom roles for class parameters
3253 -- quickly lead to incoherence. So, we require
3254 -- IncoherentInstances to have them. See #8773, #14292
3255 ; incoherent_roles_ok <- xoptM LangExt.IncoherentInstances
3256 ; checkTc ( incoherent_roles_ok
3257 || (not $ isClassTyCon tc)
3258 || (all (== Nominal) vis_roles))
3259 incoherentRoles
3260
3261 ; lint <- goptM Opt_DoCoreLinting
3262 ; when lint $ checkValidRoles tc }
3263
3264 check_no_roles
3265 = whenIsJust role_annot_decl_maybe illegalRoleAnnotDecl
3266
3267 checkRoleAnnot :: TyVar -> Located (Maybe Role) -> Role -> TcM ()
3268 checkRoleAnnot _ (L _ Nothing) _ = return ()
3269 checkRoleAnnot tv (L _ (Just r1)) r2
3270 = when (r1 /= r2) $
3271 addErrTc $ badRoleAnnot (tyVarName tv) r1 r2
3272
3273 -- This is a double-check on the role inference algorithm. It is only run when
3274 -- -dcore-lint is enabled. See Note [Role inference] in TcTyDecls
3275 checkValidRoles :: TyCon -> TcM ()
3276 -- If you edit this function, you may need to update the GHC formalism
3277 -- See Note [GHC Formalism] in CoreLint
3278 checkValidRoles tc
3279 | isAlgTyCon tc
3280 -- tyConDataCons returns an empty list for data families
3281 = mapM_ check_dc_roles (tyConDataCons tc)
3282 | Just rhs <- synTyConRhs_maybe tc
3283 = check_ty_roles (zipVarEnv (tyConTyVars tc) (tyConRoles tc)) Representational rhs
3284 | otherwise
3285 = return ()
3286 where
3287 check_dc_roles datacon
3288 = do { traceTc "check_dc_roles" (ppr datacon <+> ppr (tyConRoles tc))
3289 ; mapM_ (check_ty_roles role_env Representational) $
3290 eqSpecPreds eq_spec ++ theta ++ arg_tys }
3291 -- See Note [Role-checking data constructor arguments] in TcTyDecls
3292 where
3293 (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
3294 = dataConFullSig datacon
3295 univ_roles = zipVarEnv univ_tvs (tyConRoles tc)
3296 -- zipVarEnv uses zipEqual, but we don't want that for ex_tvs
3297 ex_roles = mkVarEnv (map (, Nominal) ex_tvs)
3298 role_env = univ_roles `plusVarEnv` ex_roles
3299
3300 check_ty_roles env role ty
3301 | Just ty' <- coreView ty -- #14101
3302 = check_ty_roles env role ty'
3303
3304 check_ty_roles env role (TyVarTy tv)
3305 = case lookupVarEnv env tv of
3306 Just role' -> unless (role' `ltRole` role || role' == role) $
3307 report_error $ text "type variable" <+> quotes (ppr tv) <+>
3308 text "cannot have role" <+> ppr role <+>
3309 text "because it was assigned role" <+> ppr role'
3310 Nothing -> report_error $ text "type variable" <+> quotes (ppr tv) <+>
3311 text "missing in environment"
3312
3313 check_ty_roles env Representational (TyConApp tc tys)
3314 = let roles' = tyConRoles tc in
3315 zipWithM_ (maybe_check_ty_roles env) roles' tys
3316
3317 check_ty_roles env Nominal (TyConApp _ tys)
3318 = mapM_ (check_ty_roles env Nominal) tys
3319
3320 check_ty_roles _ Phantom ty@(TyConApp {})
3321 = pprPanic "check_ty_roles" (ppr ty)
3322
3323 check_ty_roles env role (AppTy ty1 ty2)
3324 = check_ty_roles env role ty1
3325 >> check_ty_roles env Nominal ty2
3326
3327 check_ty_roles env role (FunTy ty1 ty2)
3328 = check_ty_roles env role ty1
3329 >> check_ty_roles env role ty2
3330
3331 check_ty_roles env role (ForAllTy (TvBndr tv _) ty)
3332 = check_ty_roles env Nominal (tyVarKind tv)
3333 >> check_ty_roles (extendVarEnv env tv Nominal) role ty
3334
3335 check_ty_roles _ _ (LitTy {}) = return ()
3336
3337 check_ty_roles env role (CastTy t _)
3338 = check_ty_roles env role t
3339
3340 check_ty_roles _ role (CoercionTy co)
3341 = unless (role == Phantom) $
3342 report_error $ text "coercion" <+> ppr co <+> text "has bad role" <+> ppr role
3343
3344 maybe_check_ty_roles env role ty
3345 = when (role == Nominal || role == Representational) $
3346 check_ty_roles env role ty
3347
3348 report_error doc
3349 = addErrTc $ vcat [text "Internal error in role inference:",
3350 doc,
3351 text "Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug"]
3352
3353 {-
3354 ************************************************************************
3355 * *
3356 Error messages
3357 * *
3358 ************************************************************************
3359 -}
3360
3361 tcAddTyFamInstCtxt :: TyFamInstDecl GhcRn -> TcM a -> TcM a
3362 tcAddTyFamInstCtxt decl
3363 = tcAddFamInstCtxt (text "type instance") (tyFamInstDeclName decl)
3364
3365 tcMkDataFamInstCtxt :: DataFamInstDecl GhcRn -> SDoc
3366 tcMkDataFamInstCtxt decl@(DataFamInstDecl { dfid_eqn =
3367 HsIB { hsib_body = eqn }})
3368 = tcMkFamInstCtxt (pprDataFamInstFlavour decl <+> text "instance")
3369 (unLoc (feqn_tycon eqn))
3370 tcMkDataFamInstCtxt (DataFamInstDecl (XHsImplicitBndrs _))
3371 = panic "tcMkDataFamInstCtxt"
3372
3373 tcAddDataFamInstCtxt :: DataFamInstDecl GhcRn -> TcM a -> TcM a
3374 tcAddDataFamInstCtxt decl
3375 = addErrCtxt (tcMkDataFamInstCtxt decl)
3376
3377 tcMkFamInstCtxt :: SDoc -> Name -> SDoc
3378 tcMkFamInstCtxt flavour tycon
3379 = hsep [ text "In the" <+> flavour <+> text "declaration for"
3380 , quotes (ppr tycon) ]
3381
3382 tcAddFamInstCtxt :: SDoc -> Name -> TcM a -> TcM a
3383 tcAddFamInstCtxt flavour tycon thing_inside
3384 = addErrCtxt (tcMkFamInstCtxt flavour tycon) thing_inside
3385
3386 tcAddClosedTypeFamilyDeclCtxt :: TyCon -> TcM a -> TcM a
3387 tcAddClosedTypeFamilyDeclCtxt tc
3388 = addErrCtxt ctxt
3389 where
3390 ctxt = text "In the equations for closed type family" <+>
3391 quotes (ppr tc)
3392
3393 resultTypeMisMatch :: FieldLabelString -> DataCon -> DataCon -> SDoc
3394 resultTypeMisMatch field_name con1 con2
3395 = vcat [sep [text "Constructors" <+> ppr con1 <+> text "and" <+> ppr con2,
3396 text "have a common field" <+> quotes (ppr field_name) <> comma],
3397 nest 2 $ text "but have different result types"]
3398
3399 fieldTypeMisMatch :: FieldLabelString -> DataCon -> DataCon -> SDoc
3400 fieldTypeMisMatch field_name con1 con2
3401 = sep [text "Constructors" <+> ppr con1 <+> text "and" <+> ppr con2,
3402 text "give different types for field", quotes (ppr field_name)]
3403
3404 dataConCtxtName :: [Located Name] -> SDoc
3405 dataConCtxtName [con]
3406 = text "In the definition of data constructor" <+> quotes (ppr con)
3407 dataConCtxtName con
3408 = text "In the definition of data constructors" <+> interpp'SP con
3409
3410 dataConCtxt :: Outputable a => a -> SDoc
3411 dataConCtxt con = text "In the definition of data constructor" <+> quotes (ppr con)
3412
3413 classOpCtxt :: Var -> Type -> SDoc
3414 classOpCtxt sel_id tau = sep [text "When checking the class method:",
3415 nest 2 (pprPrefixOcc sel_id <+> dcolon <+> ppr tau)]
3416
3417 classArityErr :: Int -> Class -> SDoc
3418 classArityErr n cls
3419 | n == 0 = mkErr "No" "no-parameter"
3420 | otherwise = mkErr "Too many" "multi-parameter"
3421 where
3422 mkErr howMany allowWhat =
3423 vcat [text (howMany ++ " parameters for class") <+> quotes (ppr cls),
3424 parens (text ("Enable MultiParamTypeClasses to allow "
3425 ++ allowWhat ++ " classes"))]
3426
3427 classFunDepsErr :: Class -> SDoc
3428 classFunDepsErr cls
3429 = vcat [text "Fundeps in class" <+> quotes (ppr cls),
3430 parens (text "Enable FunctionalDependencies to allow fundeps")]
3431
3432 badMethPred :: Id -> TcPredType -> SDoc
3433 badMethPred sel_id pred
3434 = vcat [ hang (text "Constraint" <+> quotes (ppr pred)
3435 <+> text "in the type of" <+> quotes (ppr sel_id))
3436 2 (text "constrains only the class type variables")
3437 , text "Enable ConstrainedClassMethods to allow it" ]
3438
3439 noClassTyVarErr :: Class -> TyCon -> SDoc
3440 noClassTyVarErr clas fam_tc
3441 = sep [ text "The associated type" <+> quotes (ppr fam_tc)
3442 , text "mentions none of the type or kind variables of the class" <+>
3443 quotes (ppr clas <+> hsep (map ppr (classTyVars clas)))]
3444
3445 badDataConTyCon :: DataCon -> Type -> Type -> SDoc
3446 badDataConTyCon data_con res_ty_tmpl actual_res_ty
3447 | tcIsForAllTy actual_res_ty
3448 = nested_foralls_contexts_suggestion
3449 | isJust (tcSplitPredFunTy_maybe actual_res_ty)
3450 = nested_foralls_contexts_suggestion
3451 | otherwise
3452 = hang (text "Data constructor" <+> quotes (ppr data_con) <+>
3453 text "returns type" <+> quotes (ppr actual_res_ty))
3454 2 (text "instead of an instance of its parent type" <+> quotes (ppr res_ty_tmpl))
3455 where
3456 -- This suggestion is useful for suggesting how to correct code like what
3457 -- was reported in Trac #12087:
3458 --
3459 -- data F a where
3460 -- MkF :: Ord a => Eq a => a -> F a
3461 --
3462 -- Although nested foralls or contexts are allowed in function type
3463 -- signatures, it is much more difficult to engineer GADT constructor type
3464 -- signatures to allow something similar, so we error in the latter case.
3465 -- Nevertheless, we can at least suggest how a user might reshuffle their
3466 -- exotic GADT constructor type signature so that GHC will accept.
3467 nested_foralls_contexts_suggestion =
3468 text "GADT constructor type signature cannot contain nested"
3469 <+> quotes forAllLit <> text "s or contexts"
3470 $+$ hang (text "Suggestion: instead use this type signature:")
3471 2 (ppr (dataConName data_con) <+> dcolon <+> ppr suggested_ty)
3472
3473 -- To construct a type that GHC would accept (suggested_ty), we:
3474 --
3475 -- 1) Find the existentially quantified type variables and the class
3476 -- predicates from the datacon. (NB: We don't need the universally
3477 -- quantified type variables, since rejigConRes won't substitute them in
3478 -- the result type if it fails, as in this scenario.)
3479 -- 2) Split apart the return type (which is headed by a forall or a
3480 -- context) using tcSplitNestedSigmaTys, collecting the type variables
3481 -- and class predicates we find, as well as the rho type lurking
3482 -- underneath the nested foralls and contexts.
3483 -- 3) Smash together the type variables and class predicates from 1) and
3484 -- 2), and prepend them to the rho type from 2).
3485 actual_ex_tvs = dataConExTyVars data_con
3486 actual_theta = dataConTheta data_con
3487 (actual_res_tvs, actual_res_theta, actual_res_rho)
3488 = tcSplitNestedSigmaTys actual_res_ty
3489 suggested_ty = mkSpecForAllTys (actual_ex_tvs ++ actual_res_tvs) $
3490 mkFunTys (actual_theta ++ actual_res_theta)
3491 actual_res_rho
3492
3493 badGadtDecl :: Name -> SDoc
3494 badGadtDecl tc_name
3495 = vcat [ text "Illegal generalised algebraic data declaration for" <+> quotes (ppr tc_name)
3496 , nest 2 (parens $ text "Enable the GADTs extension to allow this") ]
3497
3498 badExistential :: DataCon -> SDoc
3499 badExistential con
3500 = hang (text "Data constructor" <+> quotes (ppr con) <+>
3501 text "has existential type variables, a context, or a specialised result type")
3502 2 (vcat [ ppr con <+> dcolon <+> ppr (dataConUserType con)
3503 , parens $ text "Enable ExistentialQuantification or GADTs to allow this" ])
3504
3505 badStupidTheta :: Name -> SDoc
3506 badStupidTheta tc_name
3507 = text "A data type declared in GADT style cannot have a context:" <+> quotes (ppr tc_name)
3508
3509 newtypeConError :: Name -> Int -> SDoc
3510 newtypeConError tycon n
3511 = sep [text "A newtype must have exactly one constructor,",
3512 nest 2 $ text "but" <+> quotes (ppr tycon) <+> text "has" <+> speakN n ]
3513
3514 newtypeStrictError :: DataCon -> SDoc
3515 newtypeStrictError con
3516 = sep [text "A newtype constructor cannot have a strictness annotation,",
3517 nest 2 $ text "but" <+> quotes (ppr con) <+> text "does"]
3518
3519 newtypeFieldErr :: DataCon -> Int -> SDoc
3520 newtypeFieldErr con_name n_flds
3521 = sep [text "The constructor of a newtype must have exactly one field",
3522 nest 2 $ text "but" <+> quotes (ppr con_name) <+> text "has" <+> speakN n_flds]
3523
3524 badSigTyDecl :: Name -> SDoc
3525 badSigTyDecl tc_name
3526 = vcat [ text "Illegal kind signature" <+>
3527 quotes (ppr tc_name)
3528 , nest 2 (parens $ text "Use KindSignatures to allow kind signatures") ]
3529
3530 emptyConDeclsErr :: Name -> SDoc
3531 emptyConDeclsErr tycon
3532 = sep [quotes (ppr tycon) <+> text "has no constructors",
3533 nest 2 $ text "(EmptyDataDecls permits this)"]
3534
3535 wrongKindOfFamily :: TyCon -> SDoc
3536 wrongKindOfFamily family
3537 = text "Wrong category of family instance; declaration was for a"
3538 <+> kindOfFamily
3539 where
3540 kindOfFamily | isTypeFamilyTyCon family = text "type family"
3541 | isDataFamilyTyCon family = text "data family"
3542 | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
3543
3544 wrongNumberOfParmsErr :: Arity -> SDoc
3545 wrongNumberOfParmsErr max_args
3546 = text "Number of parameters must match family declaration; expected"
3547 <+> ppr max_args
3548
3549 defaultAssocKindErr :: TyCon -> SDoc
3550 defaultAssocKindErr fam_tc
3551 = text "Kind mis-match on LHS of default declaration for"
3552 <+> quotes (ppr fam_tc)
3553
3554 wrongTyFamName :: Name -> Name -> SDoc
3555 wrongTyFamName fam_tc_name eqn_tc_name
3556 = hang (text "Mismatched type name in type family instance.")
3557 2 (vcat [ text "Expected:" <+> ppr fam_tc_name
3558 , text " Actual:" <+> ppr eqn_tc_name ])
3559
3560 badRoleAnnot :: Name -> Role -> Role -> SDoc
3561 badRoleAnnot var annot inferred
3562 = hang (text "Role mismatch on variable" <+> ppr var <> colon)
3563 2 (sep [ text "Annotation says", ppr annot
3564 , text "but role", ppr inferred
3565 , text "is required" ])
3566
3567 wrongNumberOfRoles :: [a] -> LRoleAnnotDecl GhcRn -> SDoc
3568 wrongNumberOfRoles tyvars d@(L _ (RoleAnnotDecl _ _ annots))
3569 = hang (text "Wrong number of roles listed in role annotation;" $$
3570 text "Expected" <+> (ppr $ length tyvars) <> comma <+>
3571 text "got" <+> (ppr $ length annots) <> colon)
3572 2 (ppr d)
3573 wrongNumberOfRoles _ (L _ (XRoleAnnotDecl _)) = panic "wrongNumberOfRoles"
3574
3575 illegalRoleAnnotDecl :: LRoleAnnotDecl GhcRn -> TcM ()
3576 illegalRoleAnnotDecl (L loc (RoleAnnotDecl _ tycon _))
3577 = setErrCtxt [] $
3578 setSrcSpan loc $
3579 addErrTc (text "Illegal role annotation for" <+> ppr tycon <> char ';' $$
3580 text "they are allowed only for datatypes and classes.")
3581 illegalRoleAnnotDecl (L _ (XRoleAnnotDecl _)) = panic "illegalRoleAnnotDecl"
3582
3583 needXRoleAnnotations :: TyCon -> SDoc
3584 needXRoleAnnotations tc
3585 = text "Illegal role annotation for" <+> ppr tc <> char ';' $$
3586 text "did you intend to use RoleAnnotations?"
3587
3588 incoherentRoles :: SDoc
3589 incoherentRoles = (text "Roles other than" <+> quotes (text "nominal") <+>
3590 text "for class parameters can lead to incoherence.") $$
3591 (text "Use IncoherentInstances to allow this; bad role found")
3592
3593 addTyConCtxt :: TyCon -> TcM a -> TcM a
3594 addTyConCtxt tc
3595 = addErrCtxt ctxt
3596 where
3597 name = getName tc
3598 flav = ppr (tyConFlavour tc)
3599 ctxt = hsep [ text "In the", flav
3600 , text "declaration for", quotes (ppr name) ]
3601
3602 addRoleAnnotCtxt :: Name -> TcM a -> TcM a
3603 addRoleAnnotCtxt name
3604 = addErrCtxt $
3605 text "while checking a role annotation for" <+> quotes (ppr name)