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