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