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