Expose enabled language extensions to TH
[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
11 module TcTyClsDecls (
12 tcTyAndClassDecls, tcAddImplicits,
13
14 -- Functions used by TcInstDcls to check
15 -- data/type family instance declarations
16 kcDataDefn, tcConDecls, dataDeclChecks, checkValidTyCon,
17 tcFamTyPats, tcTyFamInstEqn, famTyConShape,
18 tcAddTyFamInstCtxt, tcMkDataFamInstCtxt, tcAddDataFamInstCtxt,
19 wrongKindOfFamily, dataConCtxt
20 ) where
21
22 #include "HsVersions.h"
23
24 import HsSyn
25 import HscTypes
26 import BuildTyCl
27 import TcRnMonad
28 import TcEnv
29 import TcValidity
30 import TcHsSyn
31 import TcTyDecls
32 import TcClassDcl
33 import TcUnify
34 import TcHsType
35 import TcMType
36 import RnTypes( collectAnonWildCards )
37 import TcType
38 import FamInst
39 import FamInstEnv
40 import Coercion
41 import Type
42 import TyCoRep -- for checkValidRoles
43 import Kind
44 import Class
45 import CoAxiom
46 import TyCon
47 import DataCon
48 import Id
49 -- import IdInfo
50 import Var
51 import VarEnv
52 import VarSet
53 import Module
54 import Name
55 import NameSet
56 import NameEnv
57 import RnEnv
58 import Outputable
59 import Maybes
60 import Unify
61 import Util
62 import SrcLoc
63 import ListSetOps
64 import Digraph
65 import DynFlags
66 import FastString
67 import Unique
68 import BasicTypes
69 import qualified GHC.LanguageExtensions as LangExt
70
71 import Control.Monad
72 import Data.List
73 #if __GLASGOW_HASKELL__ < 709
74 import Data.Monoid ( mempty )
75 #endif
76
77 {-
78 ************************************************************************
79 * *
80 \subsection{Type checking for type and class declarations}
81 * *
82 ************************************************************************
83
84 Note [Grouping of type and class declarations]
85 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
86 tcTyAndClassDecls is called on a list of `TyClGroup`s. Each group is a strongly
87 connected component of mutually dependent types and classes. We kind check and
88 type check each group separately to enhance kind polymorphism. Take the
89 following example:
90
91 type Id a = a
92 data X = X (Id Int)
93
94 If we were to kind check the two declarations together, we would give Id the
95 kind * -> *, since we apply it to an Int in the definition of X. But we can do
96 better than that, since Id really is kind polymorphic, and should get kind
97 forall (k::*). k -> k. Since it does not depend on anything else, it can be
98 kind-checked by itself, hence getting the most general kind. We then kind check
99 X, which works fine because we then know the polymorphic kind of Id, and simply
100 instantiate k to *.
101
102 Note [Check role annotations in a second pass]
103 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
104 Role inference potentially depends on the types of all of the datacons declared
105 in a mutually recursive group. The validity of a role annotation, in turn,
106 depends on the result of role inference. Because the types of datacons might
107 be ill-formed (see #7175 and Note [Checking GADT return types]) we must check
108 *all* the tycons in a group for validity before checking *any* of the roles.
109 Thus, we take two passes over the resulting tycons, first checking for general
110 validity and then checking for valid role annotations.
111 -}
112
113 tcTyAndClassDecls :: [TyClGroup Name] -- Mutually-recursive groups in dependency order
114 -> TcM TcGblEnv -- Input env extended by types and classes
115 -- and their implicit Ids,DataCons
116 -- Fails if there are any errors
117 tcTyAndClassDecls tyclds_s
118 = checkNoErrs $ -- The code recovers internally, but if anything gave rise to
119 -- an error we'd better stop now, to avoid a cascade
120 fold_env tyclds_s -- Type check each group in dependency order folding the global env
121 where
122 fold_env :: [TyClGroup Name] -> TcM TcGblEnv
123 fold_env [] = getGblEnv
124 fold_env (tyclds:tyclds_s)
125 = do { tcg_env <- tcTyClGroup tyclds
126 ; setGblEnv tcg_env $ fold_env tyclds_s }
127 -- remaining groups are typecheck in the extended global env
128
129 tcTyClGroup :: TyClGroup Name -> TcM TcGblEnv
130 -- Typecheck one strongly-connected component of type and class decls
131 tcTyClGroup tyclds
132 = do { -- Step 1: kind-check this group and returns the final
133 -- (possibly-polymorphic) kind of each TyCon and Class
134 -- See Note [Kind checking for type and class decls]
135 names_w_poly_kinds <- kcTyClGroup tyclds
136 ; traceTc "tcTyAndCl generalized kinds" (ppr names_w_poly_kinds)
137
138 -- Step 2: type-check all groups together, returning
139 -- the final TyCons and Classes
140 ; let role_annots = extractRoleAnnots tyclds
141 decls = group_tyclds tyclds
142 ; tyclss <- fixM $ \ ~rec_tyclss -> do
143 { is_boot <- tcIsHsBootOrSig
144 ; self_boot <- tcSelfBootInfo
145 ; let rec_flags = calcRecFlags self_boot is_boot
146 role_annots rec_tyclss
147
148 -- Populate environment with knot-tied ATyCon for TyCons
149 -- NB: if the decls mention any ill-staged data cons
150 -- (see Note [Recusion and promoting data constructors])
151 -- we will have failed already in kcTyClGroup, so no worries here
152 ; tcExtendRecEnv (zipRecTyClss names_w_poly_kinds rec_tyclss) $
153
154 -- Also extend the local type envt with bindings giving
155 -- the (polymorphic) kind of each knot-tied TyCon or Class
156 -- See Note [Type checking recursive type and class declarations]
157 tcExtendKindEnv names_w_poly_kinds $
158
159 -- Kind and type check declarations for this group
160 mapM (tcTyClDecl rec_flags) decls }
161
162 -- Step 3: Perform the validity check
163 -- We can do this now because we are done with the recursive knot
164 -- Do it before Step 4 (adding implicit things) because the latter
165 -- expects well-formed TyCons
166 ; traceTc "Starting validity check" (ppr tyclss)
167 ; tyclss <- mapM checkValidTyCl tyclss
168 ; traceTc "Done validity check" (ppr tyclss)
169 ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
170 -- See Note [Check role annotations in a second pass]
171
172 -- Step 4: Add the implicit things;
173 -- we want them in the environment because
174 -- they may be mentioned in interface files
175 ; tcExtendTyConEnv tyclss $
176 tcAddImplicits tyclss }
177
178 zipRecTyClss :: [(Name, Kind)]
179 -> [TyCon] -- Knot-tied
180 -> [(Name,TyThing)]
181 -- Build a name-TyThing mapping for the TyCons bound by decls
182 -- being careful not to look at the knot-tied [TyThing]
183 -- The TyThings in the result list must have a visible ATyCon,
184 -- because typechecking types (in, say, tcTyClDecl) looks at
185 -- this outer constructor
186 zipRecTyClss kind_pairs rec_tycons
187 = [ (name, ATyCon (get name)) | (name, _kind) <- kind_pairs ]
188 where
189 rec_tc_env :: NameEnv TyCon
190 rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
191
192 add_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
193 add_tc tc env = foldr add_one_tc env (tc : tyConATs tc)
194
195 add_one_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
196 add_one_tc tc env = extendNameEnv env (tyConName tc) tc
197
198 get name = case lookupNameEnv rec_tc_env name of
199 Just tc -> tc
200 other -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
201
202 {-
203 ************************************************************************
204 * *
205 Kind checking
206 * *
207 ************************************************************************
208
209 Note [Kind checking for type and class decls]
210 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
211 Kind checking is done thus:
212
213 1. Make up a kind variable for each parameter of the *data* type, class,
214 and closed type family decls, and extend the kind environment (which is
215 in the TcLclEnv)
216
217 2. Dependency-analyse the type *synonyms* (which must be non-recursive),
218 and kind-check them in dependency order. Extend the kind envt.
219
220 3. Kind check the data type and class decls
221
222 We need to kind check all types in the mutually recursive group
223 before we know the kind of the type variables. For example:
224
225 class C a where
226 op :: D b => a -> b -> b
227
228 class D c where
229 bop :: (Monad c) => ...
230
231 Here, the kind of the locally-polymorphic type variable "b"
232 depends on *all the uses of class D*. For example, the use of
233 Monad c in bop's type signature means that D must have kind Type->Type.
234
235 However type synonyms work differently. They can have kinds which don't
236 just involve (->) and *:
237 type R = Int# -- Kind #
238 type S a = Array# a -- Kind * -> #
239 type T a b = (# a,b #) -- Kind * -> * -> (# a,b #)
240 and a kind variable can't unify with UnboxedTypeKind.
241
242 So we must infer the kinds of type synonyms from their right-hand
243 sides *first* and then use them, whereas for the mutually recursive
244 data types D we bring into scope kind bindings D -> k, where k is a
245 kind variable, and do inference.
246
247 NB: synonyms can be mutually recursive with data type declarations though!
248 type T = D -> D
249 data D = MkD Int T
250
251 Open type families
252 ~~~~~~~~~~~~~~~~~~
253 This treatment of type synonyms only applies to Haskell 98-style synonyms.
254 General type functions can be recursive, and hence, appear in `alg_decls'.
255
256 The kind of an open type family is solely determinded by its kind signature;
257 hence, only kind signatures participate in the construction of the initial
258 kind environment (as constructed by `getInitialKind'). In fact, we ignore
259 instances of families altogether in the following. However, we need to include
260 the kinds of *associated* families into the construction of the initial kind
261 environment. (This is handled by `allDecls').
262
263
264 See also Note [Kind checking recursive type and class declarations]
265
266 -}
267
268 kcTyClGroup :: TyClGroup Name -> TcM [(Name,Kind)]
269 -- Kind check this group, kind generalize, and return the resulting local env
270 -- This bindds the TyCons and Classes of the group, but not the DataCons
271 -- See Note [Kind checking for type and class decls]
272 kcTyClGroup (TyClGroup { group_tyclds = decls })
273 = do { mod <- getModule
274 ; traceTc "kcTyClGroup" (ptext (sLit "module") <+> ppr mod $$ vcat (map ppr decls))
275
276 -- Kind checking;
277 -- 1. Bind kind variables for non-synonyms
278 -- 2. Kind-check synonyms, and bind kinds of those synonyms
279 -- 3. Kind-check non-synonyms
280 -- 4. Generalise the inferred kinds
281 -- See Note [Kind checking for type and class decls]
282
283 ; lcl_env <- checkNoErrs $
284 solveEqualities $
285 do {
286 -- Step 1: Bind kind variables for non-synonyms
287 let (syn_decls, non_syn_decls) = partition (isSynDecl . unLoc) decls
288 ; initial_kinds <- getInitialKinds non_syn_decls
289 ; traceTc "kcTyClGroup: initial kinds" (ppr initial_kinds)
290
291 -- Step 2: Set initial envt, kind-check the synonyms
292 ; lcl_env <- tcExtendKindEnv2 initial_kinds $
293 kcSynDecls (calcSynCycles syn_decls)
294
295 -- Step 3: Set extended envt, kind-check the non-synonyms
296 ; setLclEnv lcl_env $
297 tcExtendRecEnv (tcTyConPairs initial_kinds) $
298 -- See Note [Kind checking recursive type and class declarations]
299 mapM_ kcLTyClDecl non_syn_decls
300
301 ; return lcl_env }
302
303 -- Step 4: generalisation
304 -- Kind checking done for this group
305 -- Now we have to kind generalize the flexis
306 ; res <- concatMapM (generaliseTCD (tcl_env lcl_env)) decls
307
308 ; traceTc "kcTyClGroup result" (ppr res)
309 ; return res }
310
311 where
312 tcTyConPairs :: [(Name,TcTyThing)] -> [(Name,TyThing)]
313 tcTyConPairs initial_kinds = [ (name, ATyCon tc)
314 | (name, AThing kind) <- initial_kinds
315 , let tc = mkTcTyCon name kind ]
316
317 generalise :: TcTypeEnv -> Name -> TcM (Name, Kind)
318 -- For polymorphic things this is a no-op
319 generalise kind_env name
320 = do { let kc_kind = case lookupNameEnv kind_env name of
321 Just (AThing k) -> k
322 _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
323 ; kvs <- kindGeneralize kc_kind
324 ; kc_kind' <- zonkTcTypeToType emptyZonkEnv kc_kind
325
326 -- Make sure kc_kind' has the final, zonked kind variables
327 ; traceTc "Generalise kind" (vcat [ ppr name, ppr kc_kind, ppr kvs, ppr kc_kind' ])
328 ; return (name, mkInvForAllTys kvs kc_kind') }
329
330 generaliseTCD :: TcTypeEnv
331 -> LTyClDecl Name -> TcM [(Name, Kind)]
332 generaliseTCD kind_env (L _ decl)
333 | ClassDecl { tcdLName = (L _ name), tcdATs = ats } <- decl
334 = do { first <- generalise kind_env name
335 ; rest <- mapM ((generaliseFamDecl kind_env) . unLoc) ats
336 ; return (first : rest) }
337
338 | FamDecl { tcdFam = fam } <- decl
339 = do { res <- generaliseFamDecl kind_env fam
340 ; return [res] }
341
342 | otherwise
343 = do { res <- generalise kind_env (tcdName decl)
344 ; return [res] }
345
346 generaliseFamDecl :: TcTypeEnv
347 -> FamilyDecl Name -> TcM (Name, Kind)
348 generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
349 = generalise kind_env name
350
351 mk_thing_env :: [LTyClDecl Name] -> [(Name, TcTyThing)]
352 mk_thing_env [] = []
353 mk_thing_env (decl : decls)
354 | L _ (ClassDecl { tcdLName = L _ nm, tcdATs = ats }) <- decl
355 = (nm, APromotionErr ClassPE) :
356 (map (, APromotionErr TyConPE) $ map (unLoc . fdLName . unLoc) ats) ++
357 (mk_thing_env decls)
358
359 | otherwise
360 = (tcdName (unLoc decl), APromotionErr TyConPE) :
361 (mk_thing_env decls)
362
363 getInitialKinds :: [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
364 getInitialKinds decls
365 = tcExtendKindEnv2 (mk_thing_env decls) $
366 do { pairss <- mapM (addLocM getInitialKind) decls
367 ; return (concat pairss) }
368
369 getInitialKind :: TyClDecl Name -> TcM [(Name, TcTyThing)]
370 -- Allocate a fresh kind variable for each TyCon and Class
371 -- For each tycon, return (tc, AThing k)
372 -- where k is the kind of tc, derived from the LHS
373 -- of the definition (and probably including
374 -- kind unification variables)
375 -- Example: data T a b = ...
376 -- return (T, kv1 -> kv2 -> kv3)
377 --
378 -- This pass deals with (ie incorporates into the kind it produces)
379 -- * The kind signatures on type-variable binders
380 -- * The result kinds signature on a TyClDecl
381 --
382 -- ALSO for each datacon, return (dc, APromotionErr RecDataConPE)
383 -- Note [ARecDataCon: Recursion and promoting data constructors]
384 --
385 -- No family instances are passed to getInitialKinds
386
387 getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
388 = do { (cl_kind, inner_prs) <-
389 kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $ \_ _ ->
390 do { inner_prs <- getFamDeclInitialKinds ats
391 ; return (constraintKind, inner_prs) }
392 ; cl_kind <- zonkTcType cl_kind
393 ; let main_pr = (name, AThing cl_kind)
394 ; return (main_pr : inner_prs) }
395
396 getInitialKind decl@(DataDecl { tcdLName = L _ name
397 , tcdTyVars = ktvs
398 , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
399 , dd_cons = cons' } })
400 = let cons = cons' -- AZ list monad coming
401 in
402 do { (decl_kind, _) <-
403 kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $ \_ _ ->
404 do { res_k <- case m_sig of
405 Just ksig -> tcLHsKind ksig
406 Nothing -> return liftedTypeKind
407 ; return (res_k, ()) }
408 ; decl_kind <- zonkTcType decl_kind
409 ; let main_pr = (name, AThing decl_kind)
410 inner_prs = [ (unLoc con, APromotionErr RecDataConPE)
411 | L _ con' <- cons, con <- getConNames con' ]
412 ; return (main_pr : inner_prs) }
413
414 getInitialKind (FamDecl { tcdFam = decl })
415 = getFamDeclInitialKind decl
416
417 getInitialKind decl@(SynDecl {})
418 = pprPanic "getInitialKind" (ppr decl)
419
420 ---------------------------------
421 getFamDeclInitialKinds :: [LFamilyDecl Name] -> TcM [(Name, TcTyThing)]
422 getFamDeclInitialKinds decls
423 = tcExtendKindEnv2 [ (n, APromotionErr TyConPE)
424 | L _ (FamilyDecl { fdLName = L _ n }) <- decls] $
425 concatMapM (addLocM getFamDeclInitialKind) decls
426
427 getFamDeclInitialKind :: FamilyDecl Name
428 -> TcM [(Name, TcTyThing)]
429 getFamDeclInitialKind decl@(FamilyDecl { fdLName = L _ name
430 , fdTyVars = ktvs
431 , fdResultSig = L _ resultSig })
432 = do { (fam_kind, _) <-
433 kcHsTyVarBndrs (famDeclHasCusk decl) ktvs $ \_ _ ->
434 do { res_k <- case resultSig of
435 KindSig ki -> tcLHsKind ki
436 TyVarSig (L _ (KindedTyVar _ ki)) -> tcLHsKind ki
437 _ -- open type families have * return kind by default
438 | famDeclHasCusk decl -> return liftedTypeKind
439 -- closed type families have their return kind inferred
440 -- by default
441 | otherwise -> newMetaKindVar
442 ; return (res_k, ()) }
443 ; fam_kind <- zonkTcType fam_kind
444 ; return [ (name, AThing fam_kind) ] }
445
446 ----------------
447 kcSynDecls :: [SCC (LTyClDecl Name)]
448 -> TcM TcLclEnv -- Kind bindings
449 kcSynDecls [] = getLclEnv
450 kcSynDecls (group : groups)
451 = do { (n,k) <- kcSynDecl1 group
452 ; lcl_env <- tcExtendKindEnv [(n,k)] (kcSynDecls groups)
453 ; return lcl_env }
454
455 kcSynDecl1 :: SCC (LTyClDecl Name)
456 -> TcM (Name,TcKind) -- Kind bindings
457 kcSynDecl1 (AcyclicSCC (L _ decl)) = kcSynDecl decl
458 kcSynDecl1 (CyclicSCC decls) = do { recSynErr decls; failM }
459 -- Fail here to avoid error cascade
460 -- of out-of-scope tycons
461
462 kcSynDecl :: TyClDecl Name -> TcM (Name, TcKind)
463 kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name
464 , tcdRhs = rhs })
465 -- Returns a possibly-unzonked kind
466 = tcAddDeclCtxt decl $
467 do { (syn_kind, _) <-
468 kcHsTyVarBndrs (hsDeclHasCusk decl) hs_tvs $ \_ _ ->
469 do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs))
470 ; (_, rhs_kind) <- tcLHsType rhs
471 ; traceTc "kcd2" (ppr name)
472 ; return (rhs_kind, ()) }
473 ; return (name, syn_kind) }
474 kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl)
475
476 ------------------------------------------------------------------------
477 kcLTyClDecl :: LTyClDecl Name -> TcM ()
478 -- See Note [Kind checking for type and class decls]
479 kcLTyClDecl (L loc decl)
480 = setSrcSpan loc $ tcAddDeclCtxt decl $ kcTyClDecl decl
481
482 kcTyClDecl :: TyClDecl Name -> TcM ()
483 -- This function is used solely for its side effect on kind variables
484 -- NB kind signatures on the type variables and
485 -- result kind signature have already been dealt with
486 -- by getInitialKind, so we can ignore them here.
487
488 kcTyClDecl (DataDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdDataDefn = defn })
489 | HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn
490 = mapM_ (wrapLocM kcConDecl) cons
491 -- hs_tvs and dd_kindSig already dealt with in getInitialKind
492 -- If dd_kindSig is Just, this must be a GADT-style decl,
493 -- (see invariants of DataDefn declaration)
494 -- so (a) we don't need to bring the hs_tvs into scope, because the
495 -- ConDecls bind all their own variables
496 -- (b) dd_ctxt is not allowed for GADT-style decls, so we can ignore it
497
498 | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
499 = kcTyClTyVars name hs_tvs $
500 do { _ <- tcHsContext ctxt
501 ; mapM_ (wrapLocM kcConDecl) cons }
502
503 kcTyClDecl decl@(SynDecl {}) = pprPanic "kcTyClDecl" (ppr decl)
504
505 kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs
506 , tcdCtxt = ctxt, tcdSigs = sigs })
507 = kcTyClTyVars name hs_tvs $
508 do { _ <- tcHsContext ctxt
509 ; mapM_ (wrapLocM kc_sig) sigs }
510 where
511 kc_sig (ClassOpSig _ nms op_ty) = kcHsSigType nms op_ty
512 kc_sig _ = return ()
513
514 kcTyClDecl (FamDecl (FamilyDecl { fdLName = L _ fam_tc_name
515 , fdTyVars = hs_tvs
516 , fdInfo = fd_info }))
517 -- closed type families look at their equations, but other families don't
518 -- do anything here
519 = case fd_info of
520 ClosedTypeFamily (Just eqns) ->
521 do { tc_kind <- kcLookupKind fam_tc_name
522 ; let fam_tc_shape = ( fam_tc_name
523 , length $ hsQTvExplicit hs_tvs
524 , tc_kind )
525 ; mapM_ (kcTyFamInstEqn fam_tc_shape) eqns }
526 _ -> return ()
527
528 -------------------
529 kcConDecl :: ConDecl Name -> TcM ()
530 kcConDecl (ConDeclH98 { con_name = name, con_qvars = ex_tvs
531 , con_cxt = ex_ctxt, con_details = details })
532 = addErrCtxt (dataConCtxtName [name]) $
533 -- the 'False' says that the existentials don't have a CUSK, as the
534 -- concept doesn't really apply here. We just need to bring the variables
535 -- into scope.
536 do { _ <- kcHsTyVarBndrs False ((fromMaybe (HsQTvs mempty []) ex_tvs)) $
537 \ _ _ ->
538 do { _ <- tcHsContext (fromMaybe (noLoc []) ex_ctxt)
539 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
540 ; return (panic "kcConDecl", ()) }
541 -- We don't need to check the telescope here, because that's
542 -- done in tcConDecl
543 ; return () }
544
545 kcConDecl (ConDeclGADT { con_names = names
546 , con_type = ty })
547 = addErrCtxt (dataConCtxtName names) $
548 do { _ <- tcGadtSigType (ppr names) (unLoc $ head names) ty
549 ; return () }
550
551
552 {-
553 Note [Recursion and promoting data constructors]
554 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
555 We don't want to allow promotion in a strongly connected component
556 when kind checking.
557
558 Consider:
559 data T f = K (f (K Any))
560
561 When kind checking the `data T' declaration the local env contains the
562 mappings:
563 T -> AThing <some initial kind>
564 K -> ARecDataCon
565
566 ANothing is only used for DataCons, and only used during type checking
567 in tcTyClGroup.
568
569
570 ************************************************************************
571 * *
572 \subsection{Type checking}
573 * *
574 ************************************************************************
575
576 Note [Type checking recursive type and class declarations]
577 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
578 At this point we have completed *kind-checking* of a mutually
579 recursive group of type/class decls (done in kcTyClGroup). However,
580 we discarded the kind-checked types (eg RHSs of data type decls);
581 note that kcTyClDecl returns (). There are two reasons:
582
583 * It's convenient, because we don't have to rebuild a
584 kinded HsDecl (a fairly elaborate type)
585
586 * It's necessary, because after kind-generalisation, the
587 TyCons/Classes may now be kind-polymorphic, and hence need
588 to be given kind arguments.
589
590 Example:
591 data T f a = MkT (f a) (T f a)
592 During kind-checking, we give T the kind T :: k1 -> k2 -> *
593 and figure out constraints on k1, k2 etc. Then we generalise
594 to get T :: forall k. (k->*) -> k -> *
595 So now the (T f a) in the RHS must be elaborated to (T k f a).
596
597 However, during tcTyClDecl of T (above) we will be in a recursive
598 "knot". So we aren't allowed to look at the TyCon T itself; we are only
599 allowed to put it (lazily) in the returned structures. But when
600 kind-checking the RHS of T's decl, we *do* need to know T's kind (so
601 that we can correctly elaboarate (T k f a). How can we get T's kind
602 without looking at T? Delicate answer: during tcTyClDecl, we extend
603
604 *Global* env with T -> ATyCon (the (not yet built) TyCon for T)
605 *Local* env with T -> AThing (polymorphic kind of T)
606
607 Then:
608
609 * During TcHsType.kcTyVar we look in the *local* env, to get the
610 known kind for T.
611
612 * But in TcHsType.ds_type (and ds_var_app in particular) we look in
613 the *global* env to get the TyCon. But we must be careful not to
614 force the TyCon or we'll get a loop.
615
616 This fancy footwork (with two bindings for T) is only necessary for the
617 TyCons or Classes of this recursive group. Earlier, finished groups,
618 live in the global env only.
619
620 See also Note [Kind checking recursive type and class declarations]
621
622 Note [Kind checking recursive type and class declarations]
623 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
624 Before we can type-check the decls, we must kind check them. This
625 is done by establishing an "initial kind", which is a rather uninformed
626 guess at a tycon's kind (by counting arguments, mainly) and then
627 using this initial kind for recursive occurrences.
628
629 The initial kind is stored in exactly the same way during kind-checking
630 as it is during type-checking (Note [Type checking recursive type and class
631 declarations]): in the *local* environment, with AThing. But we still
632 must store *something* in the *global* environment. Even though we
633 discard the result of kind-checking, we sometimes need to produce error
634 messages. These error messages will want to refer to the tycons being
635 checked, except that they don't exist yet, and it would be Terribly
636 Annoying to get the error messages to refer back to HsSyn. So we
637 create a TcTyCon and put it in the global env. This tycon can
638 print out its name and knows its kind,
639 but any other action taken on it will panic. Note
640 that TcTyCons are *not* knot-tied, unlike the rather valid but
641 knot-tied ones that occur during type-checking.
642
643 Note [Declarations for wired-in things]
644 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
645 For wired-in things we simply ignore the declaration
646 and take the wired-in information. That avoids complications.
647 e.g. the need to make the data constructor worker name for
648 a constraint tuple match the wired-in one
649 -}
650
651 tcTyClDecl :: RecTyInfo -> LTyClDecl Name -> TcM TyCon
652 tcTyClDecl rec_info (L loc decl)
653 | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
654 = case thing of -- See Note [Declarations for wired-in things]
655 ATyCon tc -> return tc
656 _ -> pprPanic "tcTyClDecl" (ppr thing)
657
658 | otherwise
659 = setSrcSpan loc $ tcAddDeclCtxt decl $
660 do { traceTc "tcTyAndCl-x" (ppr decl)
661 ; tcTyClDecl1 Nothing rec_info decl }
662
663 -- "type family" declarations
664 tcTyClDecl1 :: Maybe Class -> RecTyInfo -> TyClDecl Name -> TcM TyCon
665 tcTyClDecl1 parent _rec_info (FamDecl { tcdFam = fd })
666 = tcFamDecl1 parent fd
667
668 -- "type" synonym declaration
669 tcTyClDecl1 _parent rec_info
670 (SynDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdRhs = rhs })
671 = ASSERT( isNothing _parent )
672 tcTyClTyVars tc_name tvs $ \ kvs' tvs' full_kind res_kind ->
673 tcTySynRhs rec_info tc_name (kvs' ++ tvs') full_kind res_kind rhs
674
675 -- "data/newtype" declaration
676 tcTyClDecl1 _parent rec_info
677 (DataDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdDataDefn = defn })
678 = ASSERT( isNothing _parent )
679 tcTyClTyVars tc_name tvs $ \ kvs' tvs' tycon_kind res_kind ->
680 tcDataDefn rec_info tc_name (kvs' ++ tvs') tycon_kind res_kind defn
681
682 tcTyClDecl1 _parent rec_info
683 (ClassDecl { tcdLName = L _ class_name, tcdTyVars = tvs
684 , tcdCtxt = ctxt, tcdMeths = meths
685 , tcdFDs = fundeps, tcdSigs = sigs
686 , tcdATs = ats, tcdATDefs = at_defs })
687 = ASSERT( isNothing _parent )
688 do { clas <- fixM $ \ clas ->
689 tcTyClTyVars class_name tvs $ \ kvs' tvs' full_kind res_kind ->
690 do { MASSERT( isConstraintKind res_kind )
691 -- This little knot is just so we can get
692 -- hold of the name of the class TyCon, which we
693 -- need to look up its recursiveness
694 ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr kvs' $$
695 ppr tvs' $$ ppr full_kind)
696 ; let tycon_name = tyConName (classTyCon clas)
697 tc_isrec = rti_is_rec rec_info tycon_name
698 roles = rti_roles rec_info tycon_name
699
700 ; ctxt' <- solveEqualities $ tcHsContext ctxt
701 ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
702 -- Squeeze out any kind unification variables
703 ; fds' <- mapM (addLocM tc_fundep) fundeps
704 ; sig_stuff <- tcClassSigs class_name sigs meths
705 ; at_stuff <- tcClassATs class_name clas ats at_defs
706 ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
707 ; clas <- buildClass
708 class_name (kvs' ++ tvs') roles ctxt' full_kind
709 fds' at_stuff
710 sig_stuff mindef tc_isrec
711 ; traceTc "tcClassDecl" (ppr fundeps $$ ppr (kvs' ++ tvs') $$
712 ppr fds')
713 ; return clas }
714
715 ; return (classTyCon clas) }
716 where
717 tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ;
718 ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
719 ; return (tvs1', tvs2') }
720
721 tcFamDecl1 :: Maybe Class -> FamilyDecl Name -> TcM TyCon
722 tcFamDecl1 parent (FamilyDecl { fdInfo = OpenTypeFamily, fdLName = L _ tc_name
723 , fdTyVars = tvs, fdResultSig = L _ sig
724 , fdInjectivityAnn = inj })
725 = tcTyClTyVars tc_name tvs $ \ kvs' tvs' full_kind _res_kind -> do
726 { traceTc "open type family:" (ppr tc_name)
727 ; checkFamFlag tc_name
728 ; let all_tvs = kvs' ++ tvs'
729 ; inj' <- tcInjectivity all_tvs inj
730 ; let tycon = mkFamilyTyCon tc_name full_kind all_tvs
731 (resultVariableName sig) OpenSynFamilyTyCon
732 parent inj'
733 ; return tycon }
734
735 tcFamDecl1 parent
736 (FamilyDecl { fdInfo = ClosedTypeFamily mb_eqns
737 , fdLName = L _ tc_name, fdTyVars = tvs
738 , fdResultSig = L _ sig, fdInjectivityAnn = inj })
739 -- Closed type families are a little tricky, because they contain the definition
740 -- of both the type family and the equations for a CoAxiom.
741 = do { traceTc "Closed type family:" (ppr tc_name)
742 -- the variables in the header scope only over the injectivity
743 -- declaration but this is not involved here
744 ; (tvs', inj', kind) <- tcTyClTyVars tc_name tvs
745 $ \ kvs' tvs' full_kind _res_kind ->
746 do { let all_tvs = kvs' ++ tvs'
747 ; inj' <- tcInjectivity all_tvs inj
748 ; return (all_tvs, inj', full_kind) }
749
750 ; checkFamFlag tc_name -- make sure we have -XTypeFamilies
751
752 -- If Nothing, this is an abstract family in a hs-boot file;
753 -- but eqns might be empty in the Just case as well
754 ; case mb_eqns of
755 Nothing ->
756 return $ mkFamilyTyCon tc_name kind tvs'
757 (resultVariableName sig)
758 AbstractClosedSynFamilyTyCon parent
759 inj'
760 Just eqns -> do {
761
762 -- Process the equations, creating CoAxBranches
763 ; let fam_tc_shape = (tc_name, length $ hsQTvExplicit tvs, kind)
764
765 ; branches <- mapM (tcTyFamInstEqn fam_tc_shape Nothing) eqns
766 -- Do not attempt to drop equations dominated by earlier
767 -- ones here; in the case of mutual recursion with a data
768 -- type, we get a knot-tying failure. Instead we check
769 -- for this afterwards, in TcValidity.checkValidCoAxiom
770 -- Example: tc265
771
772 -- Create a CoAxiom, with the correct src location. It is Vitally
773 -- Important that we do not pass the branches into
774 -- newFamInstAxiomName. They have types that have been zonked inside
775 -- the knot and we will die if we look at them. This is OK here
776 -- because there will only be one axiom, so we don't need to
777 -- differentiate names.
778 -- See [Zonking inside the knot] in TcHsType
779 ; loc <- getSrcSpanM
780 ; co_ax_name <- newFamInstAxiomName loc tc_name []
781
782 ; let mb_co_ax
783 | null eqns = Nothing -- mkBranchedCoAxiom fails on empty list
784 | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches)
785
786 fam_tc = mkFamilyTyCon tc_name kind tvs' (resultVariableName sig)
787 (ClosedSynFamilyTyCon mb_co_ax) parent inj'
788
789 ; return fam_tc } }
790
791 -- We check for instance validity later, when doing validity checking for
792 -- the tycon. Exception: checking equations overlap done by dropDominatedAxioms
793
794 tcFamDecl1 parent
795 (FamilyDecl { fdInfo = DataFamily, fdLName = L _ tc_name
796 , fdTyVars = tvs, fdResultSig = L _ sig })
797 = tcTyClTyVars tc_name tvs $ \ kvs' tvs' tycon_kind res_kind -> do
798 { traceTc "data family:" (ppr tc_name)
799 ; checkFamFlag tc_name
800 ; extra_tvs <- tcDataKindSig res_kind
801 ; tc_rep_name <- newTyConRepName tc_name
802 ; let final_tvs = (kvs' ++ tvs') `chkAppend` extra_tvs -- we may not need these
803 tycon = mkFamilyTyCon tc_name tycon_kind final_tvs
804 (resultVariableName sig)
805 (DataFamilyTyCon tc_rep_name)
806 parent NotInjective
807
808 ; return tycon }
809
810 -- | Maybe return a list of Bools that say whether a type family was declared
811 -- injective in the corresponding type arguments. Length of the list is equal to
812 -- the number of arguments (including implicit kind/coercion arguments).
813 -- True on position
814 -- N means that a function is injective in its Nth argument. False means it is
815 -- not.
816 tcInjectivity :: [TyVar] -> Maybe (LInjectivityAnn Name)
817 -> TcM Injectivity
818 tcInjectivity _ Nothing
819 = return NotInjective
820
821 -- User provided an injectivity annotation, so for each tyvar argument we
822 -- check whether a type family was declared injective in that argument. We
823 -- return a list of Bools, where True means that corresponding type variable
824 -- was mentioned in lInjNames (type family is injective in that argument) and
825 -- False means that it was not mentioned in lInjNames (type family is not
826 -- injective in that type variable). We also extend injectivity information to
827 -- kind variables, so if a user declares:
828 --
829 -- type family F (a :: k1) (b :: k2) = (r :: k3) | r -> a
830 --
831 -- then we mark both `a` and `k1` as injective.
832 -- NB: the return kind is considered to be *input* argument to a type family.
833 -- Since injectivity allows to infer input arguments from the result in theory
834 -- we should always mark the result kind variable (`k3` in this example) as
835 -- injective. The reason is that result type has always an assigned kind and
836 -- therefore we can always infer the result kind if we know the result type.
837 -- But this does not seem to be useful in any way so we don't do it. (Another
838 -- reason is that the implementation would not be straightforward.)
839 tcInjectivity tvs (Just (L loc (InjectivityAnn _ lInjNames)))
840 = setSrcSpan loc $
841 do { inj_tvs <- mapM (tcLookupTyVar . unLoc) lInjNames
842 ; let inj_ktvs = filterVarSet isTyVar $ -- no injective coercion vars
843 closeOverKinds (mkVarSet inj_tvs)
844 ; let inj_bools = map (`elemVarSet` inj_ktvs) tvs
845 ; traceTc "tcInjectivity" (vcat [ ppr tvs, ppr lInjNames, ppr inj_tvs
846 , ppr inj_ktvs, ppr inj_bools ])
847 ; return $ Injective inj_bools }
848
849 tcTySynRhs :: RecTyInfo
850 -> Name
851 -> [TyVar] -> Kind -> Kind
852 -> LHsType Name -> TcM TyCon
853 tcTySynRhs rec_info tc_name tvs full_kind res_kind hs_ty
854 = do { env <- getLclEnv
855 ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
856 ; rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
857 ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
858 ; let roles = rti_roles rec_info tc_name
859 tycon = mkSynonymTyCon tc_name full_kind tvs roles rhs_ty
860 ; return tycon }
861
862 tcDataDefn :: RecTyInfo -> Name
863 -> [TyVar] -> Kind -> Kind
864 -> HsDataDefn Name -> TcM TyCon
865 -- NB: not used for newtype/data instances (whether associated or not)
866 tcDataDefn rec_info -- Knot-tied; don't look at this eagerly
867 tc_name tvs tycon_kind res_kind
868 (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
869 , dd_ctxt = ctxt, dd_kindSig = mb_ksig
870 , dd_cons = cons' })
871 = let cons = cons' -- AZ List monad coming
872 in do { extra_tvs <- tcDataKindSig res_kind
873 ; let final_tvs = tvs `chkAppend` extra_tvs
874 roles = rti_roles rec_info tc_name
875
876 ; stupid_tc_theta <- solveEqualities $ tcHsContext ctxt
877 ; stupid_theta <- zonkTcTypeToTypes emptyZonkEnv
878 stupid_tc_theta
879 ; kind_signatures <- xoptM LangExt.KindSignatures
880 ; is_boot <- tcIsHsBootOrSig -- Are we compiling an hs-boot file?
881
882 -- Check that we don't use kind signatures without Glasgow extensions
883 ; when (isJust mb_ksig) $
884 checkTc (kind_signatures) (badSigTyDecl tc_name)
885
886 ; gadt_syntax <- dataDeclChecks tc_name new_or_data stupid_theta cons
887
888 ; tycon <- fixM $ \ tycon -> do
889 { let res_ty = mkTyConApp tycon (mkTyVarTys final_tvs)
890 ; data_cons <- tcConDecls new_or_data tycon (final_tvs, res_ty) cons
891 ; tc_rhs <- mk_tc_rhs is_boot tycon data_cons
892 ; tc_rep_nm <- newTyConRepName tc_name
893 ; return (mkAlgTyCon tc_name tycon_kind final_tvs roles
894 (fmap unLoc cType)
895 stupid_theta tc_rhs
896 (VanillaAlgTyCon tc_rep_nm)
897 (rti_is_rec rec_info tc_name)
898 gadt_syntax) }
899 ; return tycon }
900 where
901 mk_tc_rhs is_boot tycon data_cons
902 | null data_cons, is_boot -- In a hs-boot file, empty cons means
903 = return totallyAbstractTyConRhs -- "don't know"; hence totally Abstract
904 | otherwise
905 = case new_or_data of
906 DataType -> return (mkDataTyConRhs data_cons)
907 NewType -> ASSERT( not (null data_cons) )
908 mkNewTyConRhs tc_name tycon (head data_cons)
909
910 {-
911 ************************************************************************
912 * *
913 Typechecking associated types (in class decls)
914 (including the associated-type defaults)
915 * *
916 ************************************************************************
917
918 Note [Associated type defaults]
919 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
920
921 The following is an example of associated type defaults:
922 class C a where
923 data D a
924
925 type F a b :: *
926 type F a b = [a] -- Default
927
928 Note that we can get default definitions only for type families, not data
929 families.
930 -}
931
932 tcClassATs :: Name -- The class name (not knot-tied)
933 -> Class -- The class parent of this associated type
934 -> [LFamilyDecl Name] -- Associated types.
935 -> [LTyFamDefltEqn Name] -- Associated type defaults.
936 -> TcM [ClassATItem]
937 tcClassATs class_name cls ats at_defs
938 = do { -- Complain about associated type defaults for non associated-types
939 sequence_ [ failWithTc (badATErr class_name n)
940 | n <- map at_def_tycon at_defs
941 , not (n `elemNameSet` at_names) ]
942 ; mapM tc_at ats }
943 where
944 at_def_tycon :: LTyFamDefltEqn Name -> Name
945 at_def_tycon (L _ eqn) = unLoc (tfe_tycon eqn)
946
947 at_fam_name :: LFamilyDecl Name -> Name
948 at_fam_name (L _ decl) = unLoc (fdLName decl)
949
950 at_names = mkNameSet (map at_fam_name ats)
951
952 at_defs_map :: NameEnv [LTyFamDefltEqn Name]
953 -- Maps an AT in 'ats' to a list of all its default defs in 'at_defs'
954 at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv
955 (at_def_tycon at_def) [at_def])
956 emptyNameEnv at_defs
957
958 tc_at at = do { fam_tc <- addLocM (tcFamDecl1 (Just cls)) at
959 ; let at_defs = lookupNameEnv at_defs_map (at_fam_name at)
960 `orElse` []
961 ; atd <- tcDefaultAssocDecl fam_tc at_defs
962 ; return (ATI fam_tc atd) }
963
964 -------------------------
965 tcDefaultAssocDecl :: TyCon -- ^ Family TyCon (not knot-tied)
966 -> [LTyFamDefltEqn Name] -- ^ Defaults
967 -> TcM (Maybe (Type, SrcSpan)) -- ^ Type checked RHS
968 tcDefaultAssocDecl _ []
969 = return Nothing -- No default declaration
970
971 tcDefaultAssocDecl _ (d1:_:_)
972 = failWithTc (ptext (sLit "More than one default declaration for")
973 <+> ppr (tfe_tycon (unLoc d1)))
974
975 tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
976 , tfe_pats = hs_tvs
977 , tfe_rhs = rhs })]
978 = setSrcSpan loc $
979 tcAddFamInstCtxt (ptext (sLit "default type instance")) tc_name $
980 do { traceTc "tcDefaultAssocDecl" (ppr tc_name)
981 ; let shape@(fam_name, fam_pat_arity, _) = famTyConShape fam_tc
982 fam_tc_tvs = tyConTyVars fam_tc
983
984 -- Kind of family check
985 ; checkTc (isTypeFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
986
987 -- Arity check
988 ; ASSERT( fam_name == tc_name )
989 checkTc (length (hsQTvExplicit hs_tvs) == fam_pat_arity)
990 (wrongNumberOfParmsErr fam_pat_arity)
991
992 -- Typecheck RHS
993 -- Oddly, we don't pass in any enclosing class info, and we treat
994 -- this as a top-level type instance. Type family defaults are renamed
995 -- outside the scope of their enclosing class and so the ClsInfo would
996 -- be of no use.
997 ; let HsQTvs { hsq_implicit = imp_vars, hsq_explicit = exp_vars } = hs_tvs
998 pats = HsIB { hsib_vars = imp_vars ++ map hsLTyVarName exp_vars
999 , hsib_body = map hsLTyVarBndrToType exp_vars }
1000 -- NB: Use tcFamTyPats, not tcTyClTyVars. The latter expects to get
1001 -- the LHsQTyVars used for declaring a tycon, but the names here
1002 -- are different.
1003 ; (ktvs, rhs_ty)
1004 <- tcFamTyPats shape Nothing pats
1005 (discardResult . tcCheckLHsType rhs) $ \ktvs _ rhs_kind ->
1006 do { rhs_ty <- solveEqualities $
1007 tcCheckLHsType rhs rhs_kind
1008 ; return (ktvs, rhs_ty) }
1009
1010 ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
1011 ; let subst = zipTopTCvSubst ktvs (mkTyVarTys fam_tc_tvs)
1012 ; return ( Just (substTy subst rhs_ty, loc) ) }
1013 -- We check for well-formedness and validity later, in checkValidClass
1014
1015 -------------------------
1016 kcTyFamInstEqn :: FamTyConShape -> LTyFamInstEqn Name -> TcM ()
1017 kcTyFamInstEqn fam_tc_shape
1018 (L loc (TyFamEqn { tfe_pats = pats, tfe_rhs = hs_ty }))
1019 = setSrcSpan loc $
1020 discardResult $
1021 tc_fam_ty_pats fam_tc_shape Nothing -- not an associated type
1022 pats (discardResult . (tcCheckLHsType hs_ty))
1023
1024 tcTyFamInstEqn :: FamTyConShape -> Maybe ClsInfo -> LTyFamInstEqn Name -> TcM CoAxBranch
1025 -- Needs to be here, not in TcInstDcls, because closed families
1026 -- (typechecked here) have TyFamInstEqns
1027 tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_) mb_clsinfo
1028 (L loc (TyFamEqn { tfe_tycon = L _ eqn_tc_name
1029 , tfe_pats = pats
1030 , tfe_rhs = hs_ty }))
1031 = setSrcSpan loc $
1032 tcFamTyPats fam_tc_shape mb_clsinfo pats (discardResult . (tcCheckLHsType hs_ty)) $
1033 \tvs' pats' res_kind ->
1034 do { checkTc (fam_tc_name == eqn_tc_name)
1035 (wrongTyFamName fam_tc_name eqn_tc_name)
1036 ; rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
1037 ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
1038 ; traceTc "tcTyFamInstEqn" (ppr fam_tc_name <+> pprTvBndrs tvs')
1039 -- don't print out the pats here, as they might be zonked inside the knot
1040 ; return (mkCoAxBranch tvs' [] pats' rhs_ty loc) }
1041
1042 kcDataDefn :: Name -- ^ the family name, for error msgs only
1043 -> HsTyPats Name -- ^ the patterns, for error msgs only
1044 -> HsDataDefn Name -- ^ the RHS
1045 -> TcKind -- ^ the expected kind
1046 -> TcM ()
1047 -- Used for 'data instance' only
1048 -- Ordinary 'data' is handled by kcTyClDec
1049 kcDataDefn fam_name (HsIB { hsib_body = pats })
1050 (HsDataDefn { dd_ctxt = ctxt, dd_cons = cons, dd_kindSig = mb_kind }) res_k
1051 = do { _ <- tcHsContext ctxt
1052 ; checkNoErrs $ mapM_ (wrapLocM kcConDecl) cons
1053 -- See Note [Failing early in kcDataDefn]
1054 ; discardResult $
1055 case mb_kind of
1056 Nothing -> unifyKind (Just hs_ty_pats) res_k liftedTypeKind
1057 Just k -> do { k' <- tcLHsKind k
1058 ; unifyKind (Just hs_ty_pats) res_k k' } }
1059 where
1060 hs_ty_pats = mkHsAppTys (noLoc $ HsTyVar (noLoc fam_name)) pats
1061
1062 {-
1063 Kind check type patterns and kind annotate the embedded type variables.
1064 type instance F [a] = rhs
1065
1066 * Here we check that a type instance matches its kind signature, but we do
1067 not check whether there is a pattern for each type index; the latter
1068 check is only required for type synonym instances.
1069
1070 Note [tc_fam_ty_pats vs tcFamTyPats]
1071 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1072 tc_fam_ty_pats does the type checking of the patterns, but it doesn't
1073 zonk or generate any desugaring. It is used when kind-checking closed
1074 type families.
1075
1076 tcFamTyPats type checks the patterns, zonks, and then calls thing_inside
1077 to generate a desugaring. It is used during type-checking (not kind-checking).
1078
1079 Note [Type-checking type patterns]
1080 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1081 When typechecking the patterns of a family instance declaration, we can't
1082 rely on using the family TyCon, because this is sometimes called
1083 from within a type-checking knot. (Specifically for closed type families.)
1084 The type FamTyConShape gives just enough information to do the job.
1085
1086 See also Note [tc_fam_ty_pats vs tcFamTyPats]
1087
1088 Note [Failing early in kcDataDefn]
1089 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1090 We need to use checkNoErrs when calling kcConDecl. This is because kcConDecl
1091 calls tcConDecl, which checks that the return type of a GADT-like constructor
1092 is actually an instance of the type head. Without the checkNoErrs, potentially
1093 two bad things could happen:
1094
1095 1) Duplicate error messages, because tcConDecl will be called again during
1096 *type* checking (as opposed to kind checking)
1097 2) If we just keep blindly forging forward after both kind checking and type
1098 checking, we can get a panic in rejigConRes. See Trac #8368.
1099 -}
1100
1101 -----------------
1102 type FamTyConShape = (Name, Arity, Kind) -- See Note [Type-checking type patterns]
1103
1104 famTyConShape :: TyCon -> FamTyConShape
1105 famTyConShape fam_tc
1106 = ( tyConName fam_tc
1107 , length $ filterOutInvisibleTyVars fam_tc (tyConTyVars fam_tc)
1108 , tyConKind fam_tc )
1109
1110 tc_fam_ty_pats :: FamTyConShape
1111 -> Maybe ClsInfo
1112 -> HsTyPats Name -- Patterns
1113 -> (TcKind -> TcM ()) -- Kind checker for RHS
1114 -- result is ignored
1115 -> TcM ([Type], Kind)
1116 -- Check the type patterns of a type or data family instance
1117 -- type instance F <pat1> <pat2> = <type>
1118 -- The 'tyvars' are the free type variables of pats
1119 --
1120 -- NB: The family instance declaration may be an associated one,
1121 -- nested inside an instance decl, thus
1122 -- instance C [a] where
1123 -- type F [a] = ...
1124 -- In that case, the type variable 'a' will *already be in scope*
1125 -- (and, if C is poly-kinded, so will its kind parameter).
1126
1127 tc_fam_ty_pats (name, _, kind) mb_clsinfo
1128 (HsIB { hsib_body = arg_pats, hsib_vars = vars })
1129 kind_checker
1130 = do { -- See Note [Wild cards in family instances]
1131 ; let wcs = concatMap collectAnonWildCards arg_pats
1132 tv_names = vars ++ wcs
1133
1134 -- Kind-check and quantify
1135 -- See Note [Quantifying over family patterns]
1136 ; (_, (res_kind, typats)) <- tcImplicitTKBndrs tv_names $
1137 do { (res_kind, args, leftovers, n)
1138 <- tcInferArgs name kind (snd <$> mb_clsinfo) arg_pats
1139 ; case leftovers of
1140 hs_ty:_ -> addErrTc $ too_many_args hs_ty n
1141 _ -> return ()
1142 ; kind_checker res_kind
1143 ; return ((res_kind, args), emptyVarSet) }
1144
1145 ; return (typats, res_kind) }
1146 where
1147 too_many_args hs_ty n
1148 = hang (text "Too many parameters to" <+> ppr name <> colon)
1149 2 (vcat [ ppr hs_ty <+> text "is unexpected;"
1150 , text "expected only" <+>
1151 speakNOf (n-1) (text "parameter") ])
1152
1153 -- See Note [tc_fam_ty_pats vs tcFamTyPats]
1154 tcFamTyPats :: FamTyConShape
1155 -> Maybe ClsInfo
1156 -> HsTyPats Name -- patterns
1157 -> (TcKind -> TcM ()) -- kind-checker for RHS
1158 -> ( [TyVar] -- Kind and type variables
1159 -> [TcType] -- Kind and type arguments
1160 -> Kind -> TcM a) -- NB: You can use solveEqualities here.
1161 -> TcM a
1162 tcFamTyPats fam_shape@(name,_,_) mb_clsinfo pats kind_checker thing_inside
1163 = do { (typats, res_kind)
1164 <- checkNoErrs $ -- we'll get duplicate errors if we continue.
1165 solveEqualities $ -- See Note [Constraints in patterns]
1166 tc_fam_ty_pats fam_shape mb_clsinfo pats kind_checker
1167
1168 {- TODO (RAE): This should be cleverer. Consider this:
1169
1170 type family F a
1171
1172 data G a where
1173 MkG :: F a ~ Bool => G a
1174
1175 type family Foo (x :: G a) :: F a
1176 type instance Foo MkG = False
1177
1178 This should probably be accepted. Yet the solveEqualities
1179 will fail, unable to solve (F a ~ Bool)
1180 We want to quantify over that proof.
1181 But see Note [Constraints in patterns]
1182 below, which is missing this piece. -}
1183
1184
1185 -- Find free variables (after zonking) and turn
1186 -- them into skolems, so that we don't subsequently
1187 -- replace a meta kind var with (Any *)
1188 -- Very like kindGeneralize
1189 ; qtkvs <- quantifyTyVars emptyVarSet $
1190 splitDepVarsOfTypes typats
1191
1192 ; MASSERT( isEmptyVarSet $ coVarsOfTypes typats )
1193 -- This should be the case, because otherwise the solveEqualities
1194 -- above would fail. TODO (RAE): Update once the solveEqualities
1195 -- bit is cleverer.
1196
1197 -- Zonk the patterns etc into the Type world
1198 ; (ze, qtkvs') <- zonkTyBndrsX emptyZonkEnv qtkvs
1199 ; typats' <- zonkTcTypeToTypes ze typats
1200 ; res_kind' <- zonkTcTypeToType ze res_kind
1201
1202 ; traceTc "tcFamTyPats" (ppr name $$ ppr typats)
1203 -- don't print out too much, as we might be in the knot
1204 ; tcExtendTyVarEnv qtkvs' $
1205 thing_inside qtkvs' typats' res_kind' }
1206
1207 {-
1208 Note [Constraints in patterns]
1209 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1210 NB: This isn't the whole story. See comment in tcFamTyPats.
1211
1212 At first glance, it seems there is a complicated story to tell in tcFamTyPats
1213 around constraint solving. After all, type family patterns can now do
1214 GADT pattern-matching, which is jolly complicated. But, there's a key fact
1215 which makes this all simple: everything is at top level! There cannot
1216 be untouchable type variables. There can't be weird interaction between
1217 case branches. There can't be global skolems.
1218
1219 This means that the semantics of type-level GADT matching is a little
1220 different than term level. If we have
1221
1222 data G a where
1223 MkGBool :: G Bool
1224
1225 And then
1226
1227 type family F (a :: G k) :: k
1228 type instance F MkGBool = True
1229
1230 we get
1231
1232 axF : F Bool (MkGBool <Bool>) ~ True
1233
1234 Simple! No casting on the RHS, because we can affect the kind parameter
1235 to F.
1236
1237 If we ever introduce local type families, this all gets a lot more
1238 complicated, and will end up looking awfully like term-level GADT
1239 pattern-matching.
1240
1241
1242 ** The new story **
1243
1244 Here is really what we want:
1245
1246 The matcher really can't deal with covars in arbitrary spots in coercions.
1247 But it can deal with covars that are arguments to GADT data constructors.
1248 So we somehow want to allow covars only in precisely those spots, then use
1249 them as givens when checking the RHS. TODO (RAE): Implement plan.
1250
1251
1252 Note [Quantifying over family patterns]
1253 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1254 We need to quantify over two different lots of kind variables:
1255
1256 First, the ones that come from the kinds of the tyvar args of
1257 tcTyVarBndrsKindGen, as usual
1258 data family Dist a
1259
1260 -- Proxy :: forall k. k -> *
1261 data instance Dist (Proxy a) = DP
1262 -- Generates data DistProxy = DP
1263 -- ax8 k (a::k) :: Dist * (Proxy k a) ~ DistProxy k a
1264 -- The 'k' comes from the tcTyVarBndrsKindGen (a::k)
1265
1266 Second, the ones that come from the kind argument of the type family
1267 which we pick up using the (tyCoVarsOfTypes typats) in the result of
1268 the thing_inside of tcHsTyvarBndrsGen.
1269 -- Any :: forall k. k
1270 data instance Dist Any = DA
1271 -- Generates data DistAny k = DA
1272 -- ax7 k :: Dist k (Any k) ~ DistAny k
1273 -- The 'k' comes from kindGeneralizeKinds (Any k)
1274
1275 Note [Quantified kind variables of a family pattern]
1276 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1277 Consider type family KindFam (p :: k1) (q :: k1)
1278 data T :: Maybe k1 -> k2 -> *
1279 type instance KindFam (a :: Maybe k) b = T a b -> Int
1280 The HsBSig for the family patterns will be ([k], [a])
1281
1282 Then in the family instance we want to
1283 * Bring into scope [ "k" -> k:*, "a" -> a:k ]
1284 * Kind-check the RHS
1285 * Quantify the type instance over k and k', as well as a,b, thus
1286 type instance [k, k', a:Maybe k, b:k']
1287 KindFam (Maybe k) k' a b = T k k' a b -> Int
1288
1289 Notice that in the third step we quantify over all the visibly-mentioned
1290 type variables (a,b), but also over the implicitly mentioned kind variables
1291 (k, k'). In this case one is bound explicitly but often there will be
1292 none. The role of the kind signature (a :: Maybe k) is to add a constraint
1293 that 'a' must have that kind, and to bring 'k' into scope.
1294
1295
1296 Note [Wild cards in family instances]
1297 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1298
1299 Wild cards can be used in type/data family instance declarations to indicate
1300 that the name of a type variable doesn't matter. Each wild card will be
1301 replaced with a new unique type variable. For instance:
1302
1303 type family F a b :: *
1304 type instance F Int _ = Int
1305
1306 is the same as
1307
1308 type family F a b :: *
1309 type instance F Int b = Int
1310
1311 This is implemented as follows: during renaming anonymous wild cards are given
1312 freshly generated names. These names are collected after renaming
1313 (rnFamInstDecl) and used to make new type variables during type checking
1314 (tc_fam_ty_pats). One should not confuse these wild cards with the ones from
1315 partial type signatures. The latter generate fresh meta-variables whereas the
1316 former generate fresh skolems.
1317
1318 Named and extra-constraints wild cards are not supported in type/data family
1319 instance declarations.
1320
1321 Relevant tickets: #3699 and #10586.
1322
1323 ************************************************************************
1324 * *
1325 Data types
1326 * *
1327 ************************************************************************
1328 -}
1329
1330 dataDeclChecks :: Name -> NewOrData -> ThetaType -> [LConDecl Name] -> TcM Bool
1331 dataDeclChecks tc_name new_or_data stupid_theta cons
1332 = do { -- Check that we don't use GADT syntax in H98 world
1333 gadtSyntax_ok <- xoptM LangExt.GADTSyntax
1334 ; let gadt_syntax = consUseGadtSyntax cons
1335 ; checkTc (gadtSyntax_ok || not gadt_syntax) (badGadtDecl tc_name)
1336
1337 -- Check that the stupid theta is empty for a GADT-style declaration
1338 ; checkTc (null stupid_theta || not gadt_syntax) (badStupidTheta tc_name)
1339
1340 -- Check that a newtype has exactly one constructor
1341 -- Do this before checking for empty data decls, so that
1342 -- we don't suggest -XEmptyDataDecls for newtypes
1343 ; checkTc (new_or_data == DataType || isSingleton cons)
1344 (newtypeConError tc_name (length cons))
1345
1346 -- Check that there's at least one condecl,
1347 -- or else we're reading an hs-boot file, or -XEmptyDataDecls
1348 ; empty_data_decls <- xoptM LangExt.EmptyDataDecls
1349 ; is_boot <- tcIsHsBootOrSig -- Are we compiling an hs-boot file?
1350 ; checkTc (not (null cons) || empty_data_decls || is_boot)
1351 (emptyConDeclsErr tc_name)
1352 ; return gadt_syntax }
1353
1354
1355 -----------------------------------
1356 consUseGadtSyntax :: [LConDecl a] -> Bool
1357 consUseGadtSyntax (L _ (ConDeclGADT { }) : _) = True
1358 consUseGadtSyntax _ = False
1359 -- All constructors have same shape
1360
1361 -----------------------------------
1362 tcConDecls :: NewOrData -> TyCon -> ([TyVar], Type)
1363 -> [LConDecl Name] -> TcM [DataCon]
1364 tcConDecls new_or_data rep_tycon (tmpl_tvs, res_tmpl)
1365 = concatMapM $ addLocM $
1366 tcConDecl new_or_data rep_tycon tmpl_tvs res_tmpl
1367
1368 tcConDecl :: NewOrData
1369 -> TyCon -- Representation tycon. Knot-tied!
1370 -> [TyVar] -> Type -- Return type template (with its template tyvars)
1371 -- (tvs, T tys), where T is the family TyCon
1372 -> ConDecl Name
1373 -> TcM [DataCon]
1374
1375 tcConDecl new_or_data rep_tycon tmpl_tvs res_tmpl
1376 (ConDeclH98 { con_name = name
1377 , con_qvars = hs_qvars, con_cxt = hs_ctxt
1378 , con_details = hs_details })
1379 = addErrCtxt (dataConCtxtName [name]) $
1380 do { traceTc "tcConDecl 1" (ppr name)
1381 ; let (hs_kvs, hs_tvs) = case hs_qvars of
1382 Nothing -> ([], [])
1383 Just (HsQTvs { hsq_implicit = kvs, hsq_explicit = tvs })
1384 -> (kvs, tvs)
1385 ; (kvs, (ctxt, arg_tys, field_lbls, stricts, tvs))
1386 <- solveEqualities $
1387 tcImplicitTKBndrs hs_kvs $
1388 tcHsTyVarBndrs hs_tvs $ \tvs ->
1389 do { traceTc "tcConDecl" (ppr name <+> text "tvs:" <+> ppr hs_tvs)
1390 ; ctxt <- tcHsContext (fromMaybe (noLoc []) hs_ctxt)
1391 ; btys <- tcConArgs new_or_data hs_details
1392 ; field_lbls <- lookupConstructorFields (unLoc name)
1393 ; let (arg_tys, stricts) = unzip btys
1394 bound_vars = allBoundVariabless ctxt `unionVarSet`
1395 allBoundVariabless arg_tys
1396 ; return ((ctxt, arg_tys, field_lbls, stricts, tvs), bound_vars)
1397 }
1398
1399 -- Zonk to Types
1400 ; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv (kvs ++ tvs)
1401 ; arg_tys <- zonkTcTypeToTypes ze arg_tys
1402 ; ctxt <- zonkTcTypeToTypes ze ctxt
1403
1404 ; fam_envs <- tcGetFamInstEnvs
1405
1406 -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
1407 ; traceTc "tcConDecl 2" (ppr name $$ ppr field_lbls)
1408 ; let
1409 buildOneDataCon (L _ name) = do
1410 { is_infix <- tcConIsInfixH98 name hs_details
1411 ; rep_nm <- newTyConRepName name
1412
1413 ; buildDataCon fam_envs name is_infix rep_nm
1414 stricts Nothing field_lbls
1415 tmpl_tvs qtkvs [{- no eq_preds -}] ctxt arg_tys
1416 res_tmpl rep_tycon
1417 -- NB: we put data_tc, the type constructor gotten from the
1418 -- constructor type signature into the data constructor;
1419 -- that way checkValidDataCon can complain if it's wrong.
1420 }
1421 ; traceTc "tcConDecl 2" (ppr name)
1422 ; mapM buildOneDataCon [name]
1423 }
1424
1425 tcConDecl _new_or_data rep_tycon tmpl_tvs res_tmpl
1426 (ConDeclGADT { con_names = names, con_type = ty })
1427 = addErrCtxt (dataConCtxtName names) $
1428 do { traceTc "tcConDecl 1" (ppr names)
1429 ; (ctxt, stricts, field_lbls, arg_tys, res_ty,hs_details)
1430 <- tcGadtSigType (ppr names) (unLoc $ head names) ty
1431 ; tkvs <- quantifyTyVars emptyVarSet
1432 (splitDepVarsOfTypes (res_ty:ctxt++arg_tys))
1433
1434 -- Zonk to Types
1435 ; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv tkvs
1436 ; arg_tys <- zonkTcTypeToTypes ze arg_tys
1437 ; ctxt <- zonkTcTypeToTypes ze ctxt
1438 ; res_ty <- zonkTcTypeToType ze res_ty
1439
1440 ; let (univ_tvs, ex_tvs, eq_preds, res_ty', arg_subst)
1441 = rejigConRes tmpl_tvs res_tmpl qtkvs res_ty
1442 -- NB: this is a /lazy/ binding, so we pass five thunks to buildDataCon
1443 -- without yet forcing the guards in rejigConRes
1444 -- See Note [Checking GADT return types]
1445
1446 ; fam_envs <- tcGetFamInstEnvs
1447
1448 -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
1449 ; traceTc "tcConDecl 2" (ppr names $$ ppr field_lbls)
1450 ; let
1451 buildOneDataCon (L _ name) = do
1452 { is_infix <- tcConIsInfixGADT name hs_details
1453 ; rep_nm <- newTyConRepName name
1454
1455 ; buildDataCon fam_envs name is_infix
1456 rep_nm
1457 stricts Nothing field_lbls
1458 univ_tvs ex_tvs eq_preds
1459 (substTys arg_subst ctxt)
1460 (substTys arg_subst arg_tys)
1461 (substTy arg_subst res_ty')
1462 rep_tycon
1463 -- NB: we put data_tc, the type constructor gotten from the
1464 -- constructor type signature into the data constructor;
1465 -- that way checkValidDataCon can complain if it's wrong.
1466 }
1467 ; traceTc "tcConDecl 2" (ppr names)
1468 ; mapM buildOneDataCon names
1469 }
1470
1471
1472 tcGadtSigType :: SDoc -> Name -> LHsSigType Name
1473 -> TcM ( [PredType],[HsSrcBang], [FieldLabel], [Type], Type
1474 , HsConDetails (LHsType Name)
1475 (Located [LConDeclField Name]) )
1476 tcGadtSigType doc name ty@(HsIB { hsib_vars = vars })
1477 = do { let (hs_details', res_ty', cxt, gtvs) = gadtDeclDetails ty
1478 ; (hs_details, res_ty) <- tcUpdateConResult doc hs_details' res_ty'
1479 ; (_, (ctxt, arg_tys, res_ty, field_lbls, stricts))
1480 <- solveEqualities $
1481 tcImplicitTKBndrs vars $
1482 tcHsTyVarBndrs gtvs $ \ _ ->
1483 do { ctxt <- tcHsContext cxt
1484 ; btys <- tcConArgs DataType hs_details
1485 ; ty' <- tcHsLiftedType res_ty
1486 ; field_lbls <- lookupConstructorFields name
1487 ; let (arg_tys, stricts) = unzip btys
1488 bound_vars = allBoundVariabless ctxt `unionVarSet`
1489 allBoundVariabless arg_tys
1490
1491 ; return ((ctxt, arg_tys, ty', field_lbls, stricts), bound_vars)
1492 }
1493 ; return (ctxt,stricts,field_lbls,arg_tys,res_ty,hs_details)
1494 }
1495
1496 tcUpdateConResult :: SDoc
1497 -> HsConDetails (LHsType Name) (Located [LConDeclField Name])
1498 -- Original details
1499 -> LHsType Name -- The original result type
1500 -> TcM (HsConDetails (LHsType Name) (Located [LConDeclField Name]),
1501 LHsType Name)
1502 tcUpdateConResult doc details ty
1503 = do { let (arg_tys, res_ty) = splitHsFunType ty
1504 -- We can finally split it up,
1505 -- now the renamer has dealt with fixities
1506 -- See Note [Sorting out the result type] in RdrHsSyn
1507
1508 ; case details of
1509 InfixCon {} -> pprPanic "tcUpdateConResult" (ppr ty)
1510 -- See Note [Sorting out the result type] in RdrHsSyn
1511
1512 RecCon {} -> do { unless (null arg_tys)
1513 (failWithTc (badRecResTy doc))
1514 -- AZ: This error used to be reported during
1515 -- renaming, will now be reported in type
1516 -- checking. Is this a problem?
1517 ; return (details, res_ty) }
1518
1519 PrefixCon {} -> return (PrefixCon arg_tys, res_ty)}
1520 where
1521 badRecResTy :: SDoc -> SDoc
1522 badRecResTy ctxt = ctxt <+>
1523 ptext (sLit "Malformed constructor signature")
1524
1525 tcConIsInfixH98 :: Name
1526 -> HsConDetails (LHsType Name) (Located [LConDeclField Name])
1527 -> TcM Bool
1528 tcConIsInfixH98 _ details
1529 = case details of
1530 InfixCon {} -> return True
1531 _ -> return False
1532
1533 tcConIsInfixGADT :: Name
1534 -> HsConDetails (LHsType Name) (Located [LConDeclField Name])
1535 -> TcM Bool
1536 tcConIsInfixGADT con details
1537 = case details of
1538 InfixCon {} -> return True
1539 RecCon {} -> return False
1540 PrefixCon arg_tys -- See Note [Infix GADT constructors]
1541 | isSymOcc (getOccName con)
1542 , [_ty1,_ty2] <- arg_tys
1543 -> do { fix_env <- getFixityEnv
1544 ; return (con `elemNameEnv` fix_env) }
1545 | otherwise -> return False
1546
1547
1548
1549 tcConArgs :: NewOrData -> HsConDeclDetails Name
1550 -> TcM [(TcType, HsSrcBang)]
1551 tcConArgs new_or_data (PrefixCon btys)
1552 = mapM (tcConArg new_or_data) btys
1553 tcConArgs new_or_data (InfixCon bty1 bty2)
1554 = do { bty1' <- tcConArg new_or_data bty1
1555 ; bty2' <- tcConArg new_or_data bty2
1556 ; return [bty1', bty2'] }
1557 tcConArgs new_or_data (RecCon fields)
1558 = mapM (tcConArg new_or_data) btys
1559 where
1560 -- We need a one-to-one mapping from field_names to btys
1561 combined = map (\(L _ f) -> (cd_fld_names f,cd_fld_type f)) (unLoc fields)
1562 explode (ns,ty) = zip ns (repeat ty)
1563 exploded = concatMap explode combined
1564 (_,btys) = unzip exploded
1565
1566
1567 tcConArg :: NewOrData -> LHsType Name -> TcM (TcType, HsSrcBang)
1568 tcConArg new_or_data bty
1569 = do { traceTc "tcConArg 1" (ppr bty)
1570 ; arg_ty <- tcHsConArgType new_or_data bty
1571 ; traceTc "tcConArg 2" (ppr bty)
1572 ; return (arg_ty, getBangStrictness bty) }
1573
1574 {-
1575 Note [Infix GADT constructors]
1576 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1577 We do not currently have syntax to declare an infix constructor in GADT syntax,
1578 but it makes a (small) difference to the Show instance. So as a slightly
1579 ad-hoc solution, we regard a GADT data constructor as infix if
1580 a) it is an operator symbol
1581 b) it has two arguments
1582 c) there is a fixity declaration for it
1583 For example:
1584 infix 6 (:--:)
1585 data T a where
1586 (:--:) :: t1 -> t2 -> T Int
1587
1588
1589 Note [Checking GADT return types]
1590 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1591 There is a delicacy around checking the return types of a datacon. The
1592 central problem is dealing with a declaration like
1593
1594 data T a where
1595 MkT :: T a -> Q a
1596
1597 Note that the return type of MkT is totally bogus. When creating the T
1598 tycon, we also need to create the MkT datacon, which must have a "rejigged"
1599 return type. That is, the MkT datacon's type must be transformed to have
1600 a uniform return type with explicit coercions for GADT-like type parameters.
1601 This rejigging is what rejigConRes does. The problem is, though, that checking
1602 that the return type is appropriate is much easier when done over *Type*,
1603 not *HsType*, and doing a call to tcMatchTy will loop because T isn't fully
1604 defined yet.
1605
1606 So, we want to make rejigConRes lazy and then check the validity of
1607 the return type in checkValidDataCon. To do this we /always/ return a
1608 5-tuple from rejigConRes (so that we can extract ret_ty from it, which
1609 checkValidDataCon needs), but the first four fields may be bogus if
1610 the return type isn't valid (the last equation for rejigConRes).
1611
1612 This is better than an earlier solution which reduced the number of
1613 errors reported in one pass. See Trac #7175, and #10836.
1614 -}
1615
1616 -- Example
1617 -- data instance T (b,c) where
1618 -- TI :: forall e. e -> T (e,e)
1619 --
1620 -- The representation tycon looks like this:
1621 -- data :R7T b c where
1622 -- TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1
1623 -- In this case orig_res_ty = T (e,e)
1624
1625 rejigConRes :: [TyVar] -> Type -- Template for result type; e.g.
1626 -- data instance T [a] b c = ...
1627 -- gives template ([a,b,c], T [a] b c)
1628 -- Type must be of kind *!
1629 -> [TyVar] -- where MkT :: forall x y z. ...
1630 -> Type -- res_ty type must be of kind *
1631 -> ([TyVar], -- Universal
1632 [TyVar], -- Existential (distinct OccNames from univs)
1633 [EqSpec], -- Equality predicates
1634 Type, -- Typechecked return type
1635 TCvSubst) -- Substitution to apply to argument types
1636 -- We don't check that the TyCon given in the ResTy is
1637 -- the same as the parent tycon, because checkValidDataCon will do it
1638
1639 rejigConRes tmpl_tvs res_tmpl dc_tvs res_ty
1640 -- E.g. data T [a] b c where
1641 -- MkT :: forall x y z. T [(x,y)] z z
1642 -- The {a,b,c} are the tmpl_tvs, and the {x,y,z} are the dc_tvs
1643 -- (NB: unlike the H98 case, the dc_tvs are not all existential)
1644 -- Then we generate
1645 -- Univ tyvars Eq-spec
1646 -- a a~(x,y)
1647 -- b b~z
1648 -- z
1649 -- Existentials are the leftover type vars: [x,y]
1650 -- So we return ([a,b,z], [x,y], [a~(x,y),b~z], T [(x,y)] z z)
1651 | Just subst <- ASSERT( isLiftedTypeKind (typeKind res_ty) )
1652 ASSERT( isLiftedTypeKind (typeKind res_tmpl) )
1653 tcMatchTy (mkVarSet tmpl_tvs) res_tmpl res_ty
1654 = let (univ_tvs, raw_eqs, kind_subst) = mkGADTVars tmpl_tvs dc_tvs subst
1655 raw_ex_tvs = dc_tvs `minusList` univ_tvs
1656 (arg_subst, substed_ex_tvs)
1657 = mapAccumL substTyVarBndr kind_subst raw_ex_tvs
1658
1659 -- don't use substCoVarBndr because we don't want fresh uniques!
1660 -- substed_ex_tvs and raw_eq_cvs may dependent on one another
1661 substed_eqs = map (substEqSpec arg_subst) raw_eqs
1662 in
1663 (univ_tvs, substed_ex_tvs, substed_eqs, res_ty, arg_subst)
1664
1665 | otherwise
1666 -- If the return type of the data constructor doesn't match the parent
1667 -- type constructor, or the arity is wrong, the tcMatchTy will fail
1668 -- e.g data T a b where
1669 -- T1 :: Maybe a -- Wrong tycon
1670 -- T2 :: T [a] -- Wrong arity
1671 -- We are detect that later, in checkValidDataCon, but meanwhile
1672 -- we must do *something*, not just crash. So we do something simple
1673 -- albeit bogus, relying on checkValidDataCon to check the
1674 -- bad-result-type error before seeing that the other fields look odd
1675 -- See Note [Checking GADT return types]
1676 = (tmpl_tvs, dc_tvs `minusList` tmpl_tvs, [], res_ty, emptyTCvSubst)
1677
1678 where
1679 {-
1680 Note [mkGADTVars]
1681 ~~~~~~~~~~~~~~~~~
1682
1683 Running example:
1684
1685 data T (k1 :: *) (k2 :: *) (a :: k2) (b :: k2) where
1686 MkT :: T x1 * (Proxy (y :: x1), z) z
1687
1688 We need the rejigged type to be
1689
1690 MkT :: forall (x1 :: *) (k2 :: *) (a :: k2) (b :: k2).
1691 forall (y :: x1) (z :: *).
1692 (k2 ~ *, a ~ (Proxy x1 y, z), b ~ z)
1693 => T x1 k2 a b
1694
1695 You might naively expect that z should become a universal tyvar,
1696 not an existential. (After all, x1 becomes a universal tyvar.)
1697 The problem is that the universal tyvars must have exactly the
1698 same kinds as the tyConTyVars. z has kind * while b has kind k2.
1699 So we need an existential tyvar and a heterogeneous equality
1700 constraint. (The b ~ z is a bit redundant with the k2 ~ * that
1701 comes before in that b ~ z implies k2 ~ *. I'm sure we could do
1702 some analysis that could eliminate k2 ~ *. But we don't do this
1703 yet.)
1704
1705 The HsTypes have already been desugared to proper Types:
1706
1707 T x1 * (Proxy (y :: x1), z) z
1708 becomes
1709 [x1 :: *, y :: x1, z :: *]. T x1 * (Proxy x1 y, z) z
1710
1711 We start off by matching (T k1 k2 a b) with (T x1 * (Proxy x1 y, z) z). We
1712 know this match will succeed because of the validity check (actually done
1713 later, but laziness saves us -- see Note [Checking GADT return types]).
1714 Thus, we get
1715
1716 subst := { k1 |-> x1, k2 |-> *, a |-> (Proxy x1 y, z), b |-> z }
1717
1718 Now, we need to figure out what the GADT equalities should be. In this case,
1719 we *don't* want (k1 ~ x1) to be a GADT equality: it should just be a
1720 renaming. The others should be GADT equalities. We also need to make
1721 sure that the universally-quantified variables of the datacon match up
1722 with the tyvars of the tycon, as required for Core context well-formedness.
1723 (This last bit is why we have to rejig at all!)
1724
1725 `choose` walks down the tycon tyvars, figuring out what to do with each one.
1726 It carries two substitutions:
1727 - t_sub's domain is *template* or *tycon* tyvars, mapping them to variables
1728 mentioned in the datacon signature.
1729 - r_sub's domain is *result* tyvars, names written by the programmer in
1730 the datacon signature. The final rejigged type will use these names, but
1731 the subst is still needed because sometimes the printed name of these variables
1732 is different. (See choose_tv_name, below.)
1733
1734 Before explaining the details of `choose`, let's just look at its operation
1735 on our example:
1736
1737 choose [] [] {} {} [k1, k2, a, b]
1738 --> -- first branch of `case` statement
1739 choose
1740 univs: [x1 :: *]
1741 eq_spec: []
1742 t_sub: {k1 |-> x1}
1743 r_sub: {x1 |-> x1}
1744 t_tvs: [k2, a, b]
1745 --> -- second branch of `case` statement
1746 choose
1747 univs: [k2 :: *, x1 :: *]
1748 eq_spec: [k2 ~ *]
1749 t_sub: {k1 |-> x1, k2 |-> k2}
1750 r_sub: {x1 |-> x1}
1751 t_tvs: [a, b]
1752 --> -- second branch of `case` statement
1753 choose
1754 univs: [a :: k2, k2 :: *, x1 :: *]
1755 eq_spec: [ a ~ (Proxy x1 y, z)
1756 , k2 ~ * ]
1757 t_sub: {k1 |-> x1, k2 |-> k2, a |-> a}
1758 r_sub: {x1 |-> x1}
1759 t_tvs: [b]
1760 --> -- second branch of `case` statement
1761 choose
1762 univs: [b :: k2, a :: k2, k2 :: *, x1 :: *]
1763 eq_spec: [ b ~ z
1764 , a ~ (Proxy x1 y, z)
1765 , k2 ~ * ]
1766 t_sub: {k1 |-> x1, k2 |-> k2, a |-> a, b |-> z}
1767 r_sub: {x1 |-> x1}
1768 t_tvs: []
1769 --> -- end of recursion
1770 ( [x1 :: *, k2 :: *, a :: k2, b :: k2]
1771 , [k2 ~ *, a ~ (Proxy x1 y, z), b ~ z]
1772 , {x1 |-> x1} )
1773
1774 `choose` looks up each tycon tyvar in the matching (it *must* be matched!). If
1775 it finds a bare result tyvar (the first branch of the `case` statement), it
1776 checks to make sure that the result tyvar isn't yet in the list of univ_tvs.
1777 If it is in that list, then we have a repeated variable in the return type,
1778 and we in fact need a GADT equality. We then check to make sure that the
1779 kind of the result tyvar matches the kind of the template tyvar. This
1780 check is what forces `z` to be existential, as it should be, explained above.
1781 Assuming no repeated variables or kind-changing, we wish
1782 to use the variable name given in the datacon signature (that is, `x1` not
1783 `k1`), not the tycon signature (which may have been made up by
1784 GHC). So, we add a mapping from the tycon tyvar to the result tyvar to t_sub.
1785
1786 If we discover that a mapping in `subst` gives us a non-tyvar (the second
1787 branch of the `case` statement), then we have a GADT equality to create.
1788 We create a fresh equality, but we don't extend any substitutions. The
1789 template variable substitution is meant for use in universal tyvar kinds,
1790 and these shouldn't be affected by any GADT equalities.
1791
1792 This whole algorithm is quite delicate, indeed. I (Richard E.) see two ways
1793 of simplifying it:
1794
1795 1) The first branch of the `case` statement is really an optimization, used
1796 in order to get fewer GADT equalities. It might be possible to make a GADT
1797 equality for *every* univ. tyvar, even if the equality is trivial, and then
1798 either deal with the bigger type or somehow reduce it later.
1799
1800 2) This algorithm strives to use the names for type variables as specified
1801 by the user in the datacon signature. If we always used the tycon tyvar
1802 names, for example, this would be simplified. This change would almost
1803 certainly degrade error messages a bit, though.
1804 -}
1805
1806 -- ^ From information about a source datacon definition, extract out
1807 -- what the universal variables and the GADT equalities should be.
1808 -- See Note [mkGADTVars].
1809 mkGADTVars :: [TyVar] -- ^ The tycon vars
1810 -> [TyVar] -- ^ The datacon vars
1811 -> TCvSubst -- ^ The matching between the template result type
1812 -- and the actual result type
1813 -> ( [TyVar]
1814 , [EqSpec]
1815 , TCvSubst ) -- ^ The univ. variables, the GADT equalities,
1816 -- and a subst to apply to the GADT equalities
1817 -- and existentials.
1818 mkGADTVars tmpl_tvs dc_tvs subst
1819 = choose [] [] empty_subst empty_subst tmpl_tvs
1820 where
1821 in_scope = mkInScopeSet (mkVarSet tmpl_tvs `unionVarSet` mkVarSet dc_tvs)
1822 empty_subst = mkEmptyTCvSubst in_scope
1823
1824 choose :: [TyVar] -- accumulator of univ tvs, reversed
1825 -> [EqSpec] -- accumulator of GADT equalities, reversed
1826 -> TCvSubst -- template substutition
1827 -> TCvSubst -- res. substitution
1828 -> [TyVar] -- template tvs (the univ tvs passed in)
1829 -> ( [TyVar] -- the univ_tvs
1830 , [EqSpec] -- GADT equalities
1831 , TCvSubst ) -- a substitution to fix kinds in ex_tvs
1832
1833 choose univs eqs _t_sub r_sub []
1834 = (reverse univs, reverse eqs, r_sub)
1835 choose univs eqs t_sub r_sub (t_tv:t_tvs)
1836 | Just r_ty <- lookupTyVar subst t_tv
1837 = case getTyVar_maybe r_ty of
1838 Just r_tv
1839 | not (r_tv `elem` univs)
1840 , tyVarKind r_tv `eqType` (substTy t_sub (tyVarKind t_tv))
1841 -> -- simple, well-kinded variable substitution.
1842 choose (r_tv:univs) eqs
1843 (extendTCvSubst t_sub t_tv r_ty)
1844 (extendTCvSubst r_sub r_tv r_ty)
1845 t_tvs
1846 where
1847 r_tv1 = setTyVarName r_tv (choose_tv_name r_tv t_tv)
1848 r_ty = mkTyVarTy r_tv1
1849
1850 -- not a simple substitution. make an equality predicate
1851 _ -> choose (t_tv':univs) (mkEqSpec t_tv' r_ty : eqs)
1852 t_sub r_sub t_tvs
1853 where t_tv' = updateTyVarKind (substTy t_sub) t_tv
1854
1855 | otherwise
1856 = pprPanic "mkGADTVars" (ppr tmpl_tvs $$ ppr subst)
1857
1858 -- choose an appropriate name for a univ tyvar.
1859 -- This *must* preserve the Unique of the result tv, so that we
1860 -- can detect repeated variables. It prefers user-specified names
1861 -- over system names. A result variable with a system name can
1862 -- happen with GHC-generated implicit kind variables.
1863 choose_tv_name :: TyVar -> TyVar -> Name
1864 choose_tv_name r_tv t_tv
1865 | isSystemName r_tv_name
1866 = setNameUnique t_tv_name (getUnique r_tv_name)
1867
1868 | otherwise
1869 = r_tv_name
1870
1871 where
1872 r_tv_name = getName r_tv
1873 t_tv_name = getName t_tv
1874
1875 {-
1876 Note [Substitution in template variables kinds]
1877 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1878
1879 data G (a :: Maybe k) where
1880 MkG :: G Nothing
1881
1882 With explicit kind variables
1883
1884 data G k (a :: Maybe k) where
1885 MkG :: G k1 (Nothing k1)
1886
1887 Note how k1 is distinct from k. So, when we match the template
1888 `G k a` against `G k1 (Nothing k1)`, we get a subst
1889 [ k |-> k1, a |-> Nothing k1 ]. Even though this subst has two
1890 mappings, we surely don't want to add (k, k1) to the list of
1891 GADT equalities -- that would be overly complex and would create
1892 more untouchable variables than we need. So, when figuring out
1893 which tyvars are GADT-like and which aren't (the fundamental
1894 job of `choose`), we want to treat `k` as *not* GADT-like.
1895 Instead, we wish to substitute in `a`'s kind, to get (a :: Maybe k1)
1896 instead of (a :: Maybe k). This is the reason for dealing
1897 with a substitution in here.
1898
1899 However, we do not *always* want to substitute. Consider
1900
1901 data H (a :: k) where
1902 MkH :: H Int
1903
1904 With explicit kind variables:
1905
1906 data H k (a :: k) where
1907 MkH :: H * Int
1908
1909 Here, we have a kind-indexed GADT. The subst in question is
1910 [ k |-> *, a |-> Int ]. Now, we *don't* want to substitute in `a`'s
1911 kind, because that would give a constructor with the type
1912
1913 MkH :: forall (k :: *) (a :: *). (k ~ *) -> (a ~ Int) -> H k a
1914
1915 The problem here is that a's kind is wrong -- it needs to be k, not *!
1916 So, if the matching for a variable is anything but another bare variable,
1917 we drop the mapping from the substitution before proceeding. This
1918 was not an issue before kind-indexed GADTs because this case could
1919 never happen.
1920
1921 ************************************************************************
1922 * *
1923 Validity checking
1924 * *
1925 ************************************************************************
1926
1927 Validity checking is done once the mutually-recursive knot has been
1928 tied, so we can look at things freely.
1929 -}
1930
1931 checkValidTyCl :: TyCon -> TcM TyCon
1932 checkValidTyCl tc
1933 = setSrcSpan (getSrcSpan tc) $
1934 addTyConCtxt tc $
1935 recoverM (do { traceTc "Aborted validity for tycon" (ppr tc)
1936 ; return (makeTyConAbstract tc) })
1937 (do { traceTc "Starting validity for tycon" (ppr tc)
1938 ; checkValidTyCon tc
1939 ; traceTc "Done validity for tycon" (ppr tc)
1940 ; return tc })
1941 -- We recover, which allows us to report multiple validity errors
1942 -- In the failure case we return a TyCon of the right kind, but
1943 -- with no interesting behaviour (makeTyConAbstract). Why?
1944 -- Suppose we have
1945 -- type T a = Fun
1946 -- where Fun is a type family of arity 1. The RHS is invalid, but we
1947 -- want to go on checking validity of subsequent type declarations.
1948 -- So we replace T with an abstract TyCon which will do no harm.
1949 -- See indexed-types/should_fail/BadSock ande Trac #10896
1950
1951 -------------------------
1952 -- For data types declared with record syntax, we require
1953 -- that each constructor that has a field 'f'
1954 -- (a) has the same result type
1955 -- (b) has the same type for 'f'
1956 -- module alpha conversion of the quantified type variables
1957 -- of the constructor.
1958 --
1959 -- Note that we allow existentials to match because the
1960 -- fields can never meet. E.g
1961 -- data T where
1962 -- T1 { f1 :: b, f2 :: a, f3 ::Int } :: T
1963 -- T2 { f1 :: c, f2 :: c, f3 ::Int } :: T
1964 -- Here we do not complain about f1,f2 because they are existential
1965
1966 checkValidTyCon :: TyCon -> TcM ()
1967 checkValidTyCon tc
1968 | isPrimTyCon tc -- Happens when Haddock'ing GHC.Prim
1969 = return ()
1970
1971 | otherwise
1972 = do { checkValidTyConTyVars tc
1973 ; if | Just cl <- tyConClass_maybe tc
1974 -> checkValidClass cl
1975
1976 | Just syn_rhs <- synTyConRhs_maybe tc
1977 -> checkValidType syn_ctxt syn_rhs
1978
1979 | Just fam_flav <- famTyConFlav_maybe tc
1980 -> case fam_flav of
1981 { ClosedSynFamilyTyCon (Just ax)
1982 -> tcAddClosedTypeFamilyDeclCtxt tc $
1983 checkValidCoAxiom ax
1984 ; ClosedSynFamilyTyCon Nothing -> return ()
1985 ; AbstractClosedSynFamilyTyCon ->
1986 do { hsBoot <- tcIsHsBootOrSig
1987 ; checkTc hsBoot $
1988 text "You may define an abstract closed type family" $$
1989 text "only in a .hs-boot file" }
1990 ; DataFamilyTyCon {} -> return ()
1991 ; OpenSynFamilyTyCon -> return ()
1992 ; BuiltInSynFamTyCon _ -> return () }
1993
1994 | otherwise -> do
1995 { -- Check the context on the data decl
1996 traceTc "cvtc1" (ppr tc)
1997 ; checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc)
1998
1999 ; traceTc "cvtc2" (ppr tc)
2000
2001 ; dflags <- getDynFlags
2002 ; existential_ok <- xoptM LangExt.ExistentialQuantification
2003 ; gadt_ok <- xoptM LangExt.GADTs
2004 ; let ex_ok = existential_ok || gadt_ok
2005 -- Data cons can have existential context
2006 ; mapM_ (checkValidDataCon dflags ex_ok tc) data_cons
2007
2008 -- Check that fields with the same name share a type
2009 ; mapM_ check_fields groups }}
2010 where
2011 syn_ctxt = TySynCtxt name
2012 name = tyConName tc
2013 data_cons = tyConDataCons tc
2014
2015 groups = equivClasses cmp_fld (concatMap get_fields data_cons)
2016 cmp_fld (f1,_) (f2,_) = flLabel f1 `compare` flLabel f2
2017 get_fields con = dataConFieldLabels con `zip` repeat con
2018 -- dataConFieldLabels may return the empty list, which is fine
2019
2020 -- See Note [GADT record selectors] in TcTyDecls
2021 -- We must check (a) that the named field has the same
2022 -- type in each constructor
2023 -- (b) that those constructors have the same result type
2024 --
2025 -- However, the constructors may have differently named type variable
2026 -- and (worse) we don't know how the correspond to each other. E.g.
2027 -- C1 :: forall a b. { f :: a, g :: b } -> T a b
2028 -- C2 :: forall d c. { f :: c, g :: c } -> T c d
2029 --
2030 -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
2031 -- result type against other candidates' types BOTH WAYS ROUND.
2032 -- If they magically agrees, take the substitution and
2033 -- apply them to the latter ones, and see if they match perfectly.
2034 check_fields ((label, con1) : other_fields)
2035 -- These fields all have the same name, but are from
2036 -- different constructors in the data type
2037 = recoverM (return ()) $ mapM_ checkOne other_fields
2038 -- Check that all the fields in the group have the same type
2039 -- NB: this check assumes that all the constructors of a given
2040 -- data type use the same type variables
2041 where
2042 (tvs1, _, _, res1) = dataConSig con1
2043 ts1 = mkVarSet tvs1
2044 fty1 = dataConFieldType con1 lbl
2045 lbl = flLabel label
2046
2047 checkOne (_, con2) -- Do it bothways to ensure they are structurally identical
2048 = do { checkFieldCompat lbl con1 con2 ts1 res1 res2 fty1 fty2
2049 ; checkFieldCompat lbl con2 con1 ts2 res2 res1 fty2 fty1 }
2050 where
2051 (tvs2, _, _, res2) = dataConSig con2
2052 ts2 = mkVarSet tvs2
2053 fty2 = dataConFieldType con2 lbl
2054 check_fields [] = panic "checkValidTyCon/check_fields []"
2055
2056 checkFieldCompat :: FieldLabelString -> DataCon -> DataCon -> TyVarSet
2057 -> Type -> Type -> Type -> Type -> TcM ()
2058 checkFieldCompat fld con1 con2 tvs1 res1 res2 fty1 fty2
2059 = do { checkTc (isJust mb_subst1) (resultTypeMisMatch fld con1 con2)
2060 ; checkTc (isJust mb_subst2) (fieldTypeMisMatch fld con1 con2) }
2061 where
2062 mb_subst1 = tcMatchTy tvs1 res1 res2
2063 mb_subst2 = tcMatchTyX tvs1 (expectJust "checkFieldCompat" mb_subst1) fty1 fty2
2064
2065 -------------------------------
2066 -- | Check for ill-scoped telescopes in a tycon.
2067 -- For example:
2068 --
2069 -- > data SameKind :: k -> k -> * -- this is OK
2070 -- > data Bad a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
2071 --
2072 -- The problem is that @b@ should be bound (implicitly) at the beginning,
2073 -- but its kind mentions @a@, which is not yet in scope. Kind generalization
2074 -- makes a mess of this, and ends up including @a@ twice in the final
2075 -- tyvars. So this function checks for duplicates and, if there are any,
2076 -- produces the appropriate error message.
2077 checkValidTyConTyVars :: TyCon -> TcM ()
2078 checkValidTyConTyVars tc
2079 = when duplicate_vars $
2080 do { -- strip off the duplicates and look for ill-scoped things
2081 -- but keep the *last* occurrence of each variable, as it's
2082 -- most likely the one the user wrote
2083 let stripped_tvs = reverse $ nub $ reverse tvs
2084 vis_tvs = filterOutInvisibleTyVars tc tvs
2085 extra | not (vis_tvs `equalLength` stripped_tvs)
2086 = text "NB: Implicitly declared kind variables are put first."
2087 | otherwise
2088 = empty
2089 ; checkValidTelescope (pprTvBndrs vis_tvs) stripped_tvs extra }
2090 where
2091 tvs = tyConTyVars tc
2092 duplicate_vars = sizeVarSet (mkVarSet tvs) < length tvs
2093
2094 -------------------------------
2095 checkValidDataCon :: DynFlags -> Bool -> TyCon -> DataCon -> TcM ()
2096 checkValidDataCon dflags existential_ok tc con
2097 = setSrcSpan (srcLocSpan (getSrcLoc con)) $
2098 addErrCtxt (dataConCtxt con) $
2099 do { -- Check that the return type of the data constructor
2100 -- matches the type constructor; eg reject this:
2101 -- data T a where { MkT :: Bogus a }
2102 -- It's important to do this first:
2103 -- see Note [Checking GADT return types]
2104 -- and c.f. Note [Check role annotations in a second pass]
2105 let tc_tvs = tyConTyVars tc
2106 res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs)
2107 orig_res_ty = dataConOrigResTy con
2108 ; traceTc "checkValidDataCon" (vcat
2109 [ ppr con, ppr tc, ppr tc_tvs
2110 , ppr res_ty_tmpl <+> dcolon <+> ppr (typeKind res_ty_tmpl)
2111 , ppr orig_res_ty <+> dcolon <+> ppr (typeKind orig_res_ty)])
2112
2113
2114 ; checkTc (isJust (tcMatchTy (mkVarSet tc_tvs)
2115 res_ty_tmpl
2116 orig_res_ty))
2117 (badDataConTyCon con res_ty_tmpl orig_res_ty)
2118 -- Note that checkTc aborts if it finds an error. This is
2119 -- critical to avoid panicking when we call dataConUserType
2120 -- on an un-rejiggable datacon!
2121
2122 ; traceTc "checkValidDataCon 2" (ppr (dataConUserType con))
2123
2124 -- Check that existentials are allowed if they are used
2125 ; checkTc (existential_ok || isVanillaDataCon con)
2126 (badExistential con)
2127
2128 -- Check that the result type is a *monotype*
2129 -- e.g. reject this: MkT :: T (forall a. a->a)
2130 -- Reason: it's really the argument of an equality constraint
2131 ; checkValidMonoType orig_res_ty
2132
2133 -- Check all argument types for validity
2134 ; checkValidType ctxt (dataConUserType con)
2135
2136 -- Extra checks for newtype data constructors
2137 ; when (isNewTyCon tc) (checkNewDataCon con)
2138
2139 -- Check that UNPACK pragmas and bangs work out
2140 -- E.g. reject data T = MkT {-# UNPACK #-} Int -- No "!"
2141 -- data T = MkT {-# UNPACK #-} !a -- Can't unpack
2142 ; mapM_ check_bang (zip3 (dataConSrcBangs con) (dataConImplBangs con) [1..])
2143
2144 ; traceTc "Done validity of data con" (ppr con <+> ppr (dataConRepType con))
2145 }
2146 where
2147 ctxt = ConArgCtxt (dataConName con)
2148
2149 check_bang (HsSrcBang _ _ SrcLazy, _, n)
2150 | not (xopt LangExt.StrictData dflags)
2151 = addErrTc
2152 (bad_bang n (ptext (sLit "Lazy annotation (~) without StrictData")))
2153 check_bang (HsSrcBang _ want_unpack strict_mark, rep_bang, n)
2154 | isSrcUnpacked want_unpack, not is_strict
2155 = addWarnTc (bad_bang n (ptext (sLit "UNPACK pragma lacks '!'")))
2156 | isSrcUnpacked want_unpack
2157 , case rep_bang of { HsUnpack {} -> False; _ -> True }
2158 , not (gopt Opt_OmitInterfacePragmas dflags)
2159 -- If not optimising, se don't unpack, so don't complain!
2160 -- See MkId.dataConArgRep, the (HsBang True) case
2161 = addWarnTc (bad_bang n (ptext (sLit "Ignoring unusable UNPACK pragma")))
2162 where
2163 is_strict = case strict_mark of
2164 NoSrcStrict -> xopt LangExt.StrictData dflags
2165 bang -> isSrcStrict bang
2166
2167 check_bang _
2168 = return ()
2169
2170 bad_bang n herald
2171 = hang herald 2 (ptext (sLit "on the") <+> speakNth n
2172 <+> ptext (sLit "argument of") <+> quotes (ppr con))
2173 -------------------------------
2174 checkNewDataCon :: DataCon -> TcM ()
2175 -- Further checks for the data constructor of a newtype
2176 checkNewDataCon con
2177 = do { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
2178 -- One argument
2179
2180 ; check_con (null eq_spec) $
2181 ptext (sLit "A newtype constructor must have a return type of form T a1 ... an")
2182 -- Return type is (T a b c)
2183
2184 ; check_con (null theta) $
2185 ptext (sLit "A newtype constructor cannot have a context in its type")
2186
2187 ; check_con (null ex_tvs) $
2188 ptext (sLit "A newtype constructor cannot have existential type variables")
2189 -- No existentials
2190
2191 ; checkTc (all ok_bang (dataConSrcBangs con))
2192 (newtypeStrictError con)
2193 -- No strictness annotations
2194 }
2195 where
2196 (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
2197 = dataConFullSig con
2198 check_con what msg
2199 = checkTc what (msg $$ ppr con <+> dcolon <+> ppr (dataConUserType con))
2200
2201 ok_bang (HsSrcBang _ _ SrcStrict) = False
2202 ok_bang (HsSrcBang _ _ SrcLazy) = False
2203 ok_bang _ = True
2204
2205 -------------------------------
2206 checkValidClass :: Class -> TcM ()
2207 checkValidClass cls
2208 = do { constrained_class_methods <- xoptM LangExt.ConstrainedClassMethods
2209 ; multi_param_type_classes <- xoptM LangExt.MultiParamTypeClasses
2210 ; nullary_type_classes <- xoptM LangExt.NullaryTypeClasses
2211 ; fundep_classes <- xoptM LangExt.FunctionalDependencies
2212 ; undecidable_super_classes <- xoptM LangExt.UndecidableSuperClasses
2213
2214 -- Check that the class is unary, unless multiparameter type classes
2215 -- are enabled; also recognize deprecated nullary type classes
2216 -- extension (subsumed by multiparameter type classes, Trac #8993)
2217 ; checkTc (multi_param_type_classes || cls_arity == 1 ||
2218 (nullary_type_classes && cls_arity == 0))
2219 (classArityErr cls_arity cls)
2220 ; checkTc (fundep_classes || null fundeps) (classFunDepsErr cls)
2221
2222 -- Check the super-classes
2223 ; checkValidTheta (ClassSCCtxt (className cls)) theta
2224
2225 -- Now check for cyclic superclasses
2226 -- If there are superclass cycles, checkClassCycleErrs bails.
2227 ; unless undecidable_super_classes $
2228 case checkClassCycles cls of
2229 Just err -> setSrcSpan (getSrcSpan cls) $
2230 addErrTc err
2231 Nothing -> return ()
2232
2233 -- Check the class operations.
2234 -- But only if there have been no earlier errors
2235 -- See Note [Abort when superclass cycle is detected]
2236 ; whenNoErrs $
2237 mapM_ (check_op constrained_class_methods) op_stuff
2238
2239 -- Check the associated type defaults are well-formed and instantiated
2240 ; mapM_ check_at at_stuff }
2241 where
2242 (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls
2243 cls_arity = length $ filterOutInvisibleTyVars (classTyCon cls) tyvars
2244 -- Ignore invisible variables
2245 cls_tv_set = mkVarSet tyvars
2246
2247 check_op constrained_class_methods (sel_id, dm)
2248 = setSrcSpan (getSrcSpan sel_id) $
2249 addErrCtxt (classOpCtxt sel_id op_ty) $ do
2250 { traceTc "class op type" (ppr op_ty)
2251 ; checkValidType ctxt op_ty
2252 -- This implements the ambiguity check, among other things
2253 -- Example: tc223
2254 -- class Error e => Game b mv e | b -> mv e where
2255 -- newBoard :: MonadState b m => m ()
2256 -- Here, MonadState has a fundep m->b, so newBoard is fine
2257
2258 ; unless constrained_class_methods $
2259 mapM_ check_constraint (tail (theta1 ++ theta2))
2260
2261 ; case dm of
2262 Just (_, GenericDM ty) -> checkValidType ctxt ty
2263 _ -> return ()
2264 }
2265 where
2266 ctxt = FunSigCtxt op_name True -- Report redundant class constraints
2267 op_name = idName sel_id
2268 op_ty = idType sel_id
2269 (_,theta1,tau1) = tcSplitSigmaTy op_ty
2270 (_,theta2,_) = tcSplitSigmaTy tau1
2271
2272 check_constraint :: TcPredType -> TcM ()
2273 check_constraint pred
2274 = when (tyCoVarsOfType pred `subVarSet` cls_tv_set)
2275 (addErrTc (badMethPred sel_id pred))
2276
2277 check_at (ATI fam_tc m_dflt_rhs)
2278 = do { checkTc (cls_arity == 0 || any (`elemVarSet` cls_tv_set) fam_tvs)
2279 (noClassTyVarErr cls fam_tc)
2280 -- Check that the associated type mentions at least
2281 -- one of the class type variables
2282 -- The check is disabled for nullary type classes,
2283 -- since there is no possible ambiguity (Trac #10020)
2284 ; whenIsJust m_dflt_rhs $ \ (rhs, loc) ->
2285 checkValidTyFamEqn (Just (cls, mini_env)) fam_tc
2286 fam_tvs [] (mkTyVarTys fam_tvs) rhs loc }
2287 where
2288 fam_tvs = tyConTyVars fam_tc
2289 mini_env = zipVarEnv tyvars (mkTyVarTys tyvars)
2290
2291 checkFamFlag :: Name -> TcM ()
2292 -- Check that we don't use families without -XTypeFamilies
2293 -- The parser won't even parse them, but I suppose a GHC API
2294 -- client might have a go!
2295 checkFamFlag tc_name
2296 = do { idx_tys <- xoptM LangExt.TypeFamilies
2297 ; checkTc idx_tys err_msg }
2298 where
2299 err_msg = hang (ptext (sLit "Illegal family declaration for") <+> quotes (ppr tc_name))
2300 2 (ptext (sLit "Use TypeFamilies to allow indexed type families"))
2301
2302 {-
2303 Note [Abort when superclass cycle is detected]
2304 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2305 We must avoid doing the ambiguity check for the methods (in
2306 checkValidClass.check_op) when there are already errors accumulated.
2307 This is because one of the errors may be a superclass cycle, and
2308 superclass cycles cause canonicalization to loop. Here is a
2309 representative example:
2310
2311 class D a => C a where
2312 meth :: D a => ()
2313 class C a => D a
2314
2315 This fixes Trac #9415, #9739
2316
2317 ************************************************************************
2318 * *
2319 Checking role validity
2320 * *
2321 ************************************************************************
2322 -}
2323
2324 checkValidRoleAnnots :: RoleAnnots -> TyCon -> TcM ()
2325 checkValidRoleAnnots role_annots tc
2326 | isTypeSynonymTyCon tc = check_no_roles
2327 | isFamilyTyCon tc = check_no_roles
2328 | isAlgTyCon tc = check_roles
2329 | otherwise = return ()
2330 where
2331 -- Role annotations are given only on *explicit* variables,
2332 -- but a tycon stores roles for all variables.
2333 -- So, we drop the implicit roles (which are all Nominal, anyway).
2334 name = tyConName tc
2335 tyvars = tyConTyVars tc
2336 roles = tyConRoles tc
2337 (vis_roles, vis_vars) = unzip $ snd $
2338 partitionInvisibles tc (mkTyVarTy . snd) $
2339 zip roles tyvars
2340 role_annot_decl_maybe = lookupRoleAnnots role_annots name
2341
2342 check_roles
2343 = whenIsJust role_annot_decl_maybe $
2344 \decl@(L loc (RoleAnnotDecl _ the_role_annots)) ->
2345 addRoleAnnotCtxt name $
2346 setSrcSpan loc $ do
2347 { role_annots_ok <- xoptM LangExt.RoleAnnotations
2348 ; checkTc role_annots_ok $ needXRoleAnnotations tc
2349 ; checkTc (vis_vars `equalLength` the_role_annots)
2350 (wrongNumberOfRoles vis_vars decl)
2351 ; _ <- zipWith3M checkRoleAnnot vis_vars the_role_annots vis_roles
2352 -- Representational or phantom roles for class parameters
2353 -- quickly lead to incoherence. So, we require
2354 -- IncoherentInstances to have them. See #8773.
2355 ; incoherent_roles_ok <- xoptM LangExt.IncoherentInstances
2356 ; checkTc ( incoherent_roles_ok
2357 || (not $ isClassTyCon tc)
2358 || (all (== Nominal) vis_roles))
2359 incoherentRoles
2360
2361 ; lint <- goptM Opt_DoCoreLinting
2362 ; when lint $ checkValidRoles tc }
2363
2364 check_no_roles
2365 = whenIsJust role_annot_decl_maybe illegalRoleAnnotDecl
2366
2367 checkRoleAnnot :: TyVar -> Located (Maybe Role) -> Role -> TcM ()
2368 checkRoleAnnot _ (L _ Nothing) _ = return ()
2369 checkRoleAnnot tv (L _ (Just r1)) r2
2370 = when (r1 /= r2) $
2371 addErrTc $ badRoleAnnot (tyVarName tv) r1 r2
2372
2373 -- This is a double-check on the role inference algorithm. It is only run when
2374 -- -dcore-lint is enabled. See Note [Role inference] in TcTyDecls
2375 checkValidRoles :: TyCon -> TcM ()
2376 -- If you edit this function, you may need to update the GHC formalism
2377 -- See Note [GHC Formalism] in CoreLint
2378 checkValidRoles tc
2379 | isAlgTyCon tc
2380 -- tyConDataCons returns an empty list for data families
2381 = mapM_ check_dc_roles (tyConDataCons tc)
2382 | Just rhs <- synTyConRhs_maybe tc
2383 = check_ty_roles (zipVarEnv (tyConTyVars tc) (tyConRoles tc)) Representational rhs
2384 | otherwise
2385 = return ()
2386 where
2387 check_dc_roles datacon
2388 = do { traceTc "check_dc_roles" (ppr datacon <+> ppr (tyConRoles tc))
2389 ; mapM_ (check_ty_roles role_env Representational) $
2390 eqSpecPreds eq_spec ++ theta ++ arg_tys }
2391 -- See Note [Role-checking data constructor arguments] in TcTyDecls
2392 where
2393 (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
2394 = dataConFullSig datacon
2395 univ_roles = zipVarEnv univ_tvs (tyConRoles tc)
2396 -- zipVarEnv uses zipEqual, but we don't want that for ex_tvs
2397 ex_roles = mkVarEnv (map (, Nominal) ex_tvs)
2398 role_env = univ_roles `plusVarEnv` ex_roles
2399
2400 check_ty_roles env role (TyVarTy tv)
2401 = case lookupVarEnv env tv of
2402 Just role' -> unless (role' `ltRole` role || role' == role) $
2403 report_error $ ptext (sLit "type variable") <+> quotes (ppr tv) <+>
2404 ptext (sLit "cannot have role") <+> ppr role <+>
2405 ptext (sLit "because it was assigned role") <+> ppr role'
2406 Nothing -> report_error $ ptext (sLit "type variable") <+> quotes (ppr tv) <+>
2407 ptext (sLit "missing in environment")
2408
2409 check_ty_roles env Representational (TyConApp tc tys)
2410 = let roles' = tyConRoles tc in
2411 zipWithM_ (maybe_check_ty_roles env) roles' tys
2412
2413 check_ty_roles env Nominal (TyConApp _ tys)
2414 = mapM_ (check_ty_roles env Nominal) tys
2415
2416 check_ty_roles _ Phantom ty@(TyConApp {})
2417 = pprPanic "check_ty_roles" (ppr ty)
2418
2419 check_ty_roles env role (AppTy ty1 ty2)
2420 = check_ty_roles env role ty1
2421 >> check_ty_roles env Nominal ty2
2422
2423 check_ty_roles env role (ForAllTy (Anon ty1) ty2)
2424 = check_ty_roles env role ty1
2425 >> check_ty_roles env role ty2
2426
2427 check_ty_roles env role (ForAllTy (Named tv _) ty)
2428 = check_ty_roles env Nominal (tyVarKind tv)
2429 >> check_ty_roles (extendVarEnv env tv Nominal) role ty
2430
2431 check_ty_roles _ _ (LitTy {}) = return ()
2432
2433 check_ty_roles env role (CastTy t _)
2434 = check_ty_roles env role t
2435
2436 check_ty_roles _ role (CoercionTy co)
2437 = unless (role == Phantom) $
2438 report_error $ text "coercion" <+> ppr co <+> text "has bad role" <+> ppr role
2439
2440 maybe_check_ty_roles env role ty
2441 = when (role == Nominal || role == Representational) $
2442 check_ty_roles env role ty
2443
2444 report_error doc
2445 = addErrTc $ vcat [ptext (sLit "Internal error in role inference:"),
2446 doc,
2447 ptext (sLit "Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug")]
2448
2449 {-
2450 ************************************************************************
2451 * *
2452 Error messages
2453 * *
2454 ************************************************************************
2455 -}
2456
2457 tcAddTyFamInstCtxt :: TyFamInstDecl Name -> TcM a -> TcM a
2458 tcAddTyFamInstCtxt decl
2459 = tcAddFamInstCtxt (ptext (sLit "type instance")) (tyFamInstDeclName decl)
2460
2461 tcMkDataFamInstCtxt :: DataFamInstDecl Name -> SDoc
2462 tcMkDataFamInstCtxt decl
2463 = tcMkFamInstCtxt (pprDataFamInstFlavour decl <+> text "instance")
2464 (unLoc (dfid_tycon decl))
2465
2466 tcAddDataFamInstCtxt :: DataFamInstDecl Name -> TcM a -> TcM a
2467 tcAddDataFamInstCtxt decl
2468 = addErrCtxt (tcMkDataFamInstCtxt decl)
2469
2470 tcMkFamInstCtxt :: SDoc -> Name -> SDoc
2471 tcMkFamInstCtxt flavour tycon
2472 = hsep [ text "In the" <+> flavour <+> text "declaration for"
2473 , quotes (ppr tycon) ]
2474
2475 tcAddFamInstCtxt :: SDoc -> Name -> TcM a -> TcM a
2476 tcAddFamInstCtxt flavour tycon thing_inside
2477 = addErrCtxt (tcMkFamInstCtxt flavour tycon) thing_inside
2478
2479 tcAddClosedTypeFamilyDeclCtxt :: TyCon -> TcM a -> TcM a
2480 tcAddClosedTypeFamilyDeclCtxt tc
2481 = addErrCtxt ctxt
2482 where
2483 ctxt = ptext (sLit "In the equations for closed type family") <+>
2484 quotes (ppr tc)
2485
2486 resultTypeMisMatch :: FieldLabelString -> DataCon -> DataCon -> SDoc
2487 resultTypeMisMatch field_name con1 con2
2488 = vcat [sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2,
2489 ptext (sLit "have a common field") <+> quotes (ppr field_name) <> comma],
2490 nest 2 $ ptext (sLit "but have different result types")]
2491
2492 fieldTypeMisMatch :: FieldLabelString -> DataCon -> DataCon -> SDoc
2493 fieldTypeMisMatch field_name con1 con2
2494 = sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2,
2495 ptext (sLit "give different types for field"), quotes (ppr field_name)]
2496
2497 dataConCtxtName :: [Located Name] -> SDoc
2498 dataConCtxtName [con]
2499 = ptext (sLit "In the definition of data constructor") <+> quotes (ppr con)
2500 dataConCtxtName con
2501 = ptext (sLit "In the definition of data constructors") <+> interpp'SP con
2502
2503 dataConCtxt :: Outputable a => a -> SDoc
2504 dataConCtxt con = ptext (sLit "In the definition of data constructor") <+> quotes (ppr con)
2505
2506 classOpCtxt :: Var -> Type -> SDoc
2507 classOpCtxt sel_id tau = sep [ptext (sLit "When checking the class method:"),
2508 nest 2 (pprPrefixOcc sel_id <+> dcolon <+> ppr tau)]
2509
2510 classArityErr :: Int -> Class -> SDoc
2511 classArityErr n cls
2512 | n == 0 = mkErr "No" "no-parameter"
2513 | otherwise = mkErr "Too many" "multi-parameter"
2514 where
2515 mkErr howMany allowWhat =
2516 vcat [ptext (sLit $ howMany ++ " parameters for class") <+> quotes (ppr cls),
2517 parens (ptext (sLit $ "Use MultiParamTypeClasses to allow "
2518 ++ allowWhat ++ " classes"))]
2519
2520 classFunDepsErr :: Class -> SDoc
2521 classFunDepsErr cls
2522 = vcat [ptext (sLit "Fundeps in class") <+> quotes (ppr cls),
2523 parens (ptext (sLit "Use FunctionalDependencies to allow fundeps"))]
2524
2525 badMethPred :: Id -> TcPredType -> SDoc
2526 badMethPred sel_id pred
2527 = vcat [ hang (ptext (sLit "Constraint") <+> quotes (ppr pred)
2528 <+> ptext (sLit "in the type of") <+> quotes (ppr sel_id))
2529 2 (ptext (sLit "constrains only the class type variables"))
2530 , ptext (sLit "Use ConstrainedClassMethods to allow it") ]
2531
2532 noClassTyVarErr :: Class -> TyCon -> SDoc
2533 noClassTyVarErr clas fam_tc
2534 = sep [ ptext (sLit "The associated type") <+> quotes (ppr fam_tc)
2535 , ptext (sLit "mentions none of the type or kind variables of the class") <+>
2536 quotes (ppr clas <+> hsep (map ppr (classTyVars clas)))]
2537
2538 recSynErr :: [LTyClDecl Name] -> TcRn ()
2539 recSynErr syn_decls
2540 = setSrcSpan (getLoc (head sorted_decls)) $
2541 addErr (sep [ptext (sLit "Cycle in type synonym declarations:"),
2542 nest 2 (vcat (map ppr_decl sorted_decls))])
2543 where
2544 sorted_decls = sortLocated syn_decls
2545 ppr_decl (L loc decl) = ppr loc <> colon <+> ppr decl
2546
2547 badDataConTyCon :: DataCon -> Type -> Type -> SDoc
2548 badDataConTyCon data_con res_ty_tmpl actual_res_ty
2549 = hang (ptext (sLit "Data constructor") <+> quotes (ppr data_con) <+>
2550 ptext (sLit "returns type") <+> quotes (ppr actual_res_ty))
2551 2 (ptext (sLit "instead of an instance of its parent type") <+> quotes (ppr res_ty_tmpl))
2552
2553 badGadtDecl :: Name -> SDoc
2554 badGadtDecl tc_name
2555 = vcat [ ptext (sLit "Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
2556 , nest 2 (parens $ ptext (sLit "Use GADTs to allow GADTs")) ]
2557
2558 badExistential :: DataCon -> SDoc
2559 badExistential con
2560 = hang (ptext (sLit "Data constructor") <+> quotes (ppr con) <+>
2561 ptext (sLit "has existential type variables, a context, or a specialised result type"))
2562 2 (vcat [ ppr con <+> dcolon <+> ppr (dataConUserType con)
2563 , parens $ ptext (sLit "Use ExistentialQuantification or GADTs to allow this") ])
2564
2565 badStupidTheta :: Name -> SDoc
2566 badStupidTheta tc_name
2567 = ptext (sLit "A data type declared in GADT style cannot have a context:") <+> quotes (ppr tc_name)
2568
2569 newtypeConError :: Name -> Int -> SDoc
2570 newtypeConError tycon n
2571 = sep [ptext (sLit "A newtype must have exactly one constructor,"),
2572 nest 2 $ ptext (sLit "but") <+> quotes (ppr tycon) <+> ptext (sLit "has") <+> speakN n ]
2573
2574 newtypeStrictError :: DataCon -> SDoc
2575 newtypeStrictError con
2576 = sep [ptext (sLit "A newtype constructor cannot have a strictness annotation,"),
2577 nest 2 $ ptext (sLit "but") <+> quotes (ppr con) <+> ptext (sLit "does")]
2578
2579 newtypeFieldErr :: DataCon -> Int -> SDoc
2580 newtypeFieldErr con_name n_flds
2581 = sep [ptext (sLit "The constructor of a newtype must have exactly one field"),
2582 nest 2 $ ptext (sLit "but") <+> quotes (ppr con_name) <+> ptext (sLit "has") <+> speakN n_flds]
2583
2584 badSigTyDecl :: Name -> SDoc
2585 badSigTyDecl tc_name
2586 = vcat [ ptext (sLit "Illegal kind signature") <+>
2587 quotes (ppr tc_name)
2588 , nest 2 (parens $ ptext (sLit "Use KindSignatures to allow kind signatures")) ]
2589
2590 emptyConDeclsErr :: Name -> SDoc
2591 emptyConDeclsErr tycon
2592 = sep [quotes (ppr tycon) <+> ptext (sLit "has no constructors"),
2593 nest 2 $ ptext (sLit "(EmptyDataDecls permits this)")]
2594
2595 wrongKindOfFamily :: TyCon -> SDoc
2596 wrongKindOfFamily family
2597 = ptext (sLit "Wrong category of family instance; declaration was for a")
2598 <+> kindOfFamily
2599 where
2600 kindOfFamily | isTypeFamilyTyCon family = text "type family"
2601 | isDataFamilyTyCon family = text "data family"
2602 | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
2603
2604 wrongNumberOfParmsErr :: Arity -> SDoc
2605 wrongNumberOfParmsErr max_args
2606 = ptext (sLit "Number of parameters must match family declaration; expected")
2607 <+> ppr max_args
2608
2609 wrongTyFamName :: Name -> Name -> SDoc
2610 wrongTyFamName fam_tc_name eqn_tc_name
2611 = hang (ptext (sLit "Mismatched type name in type family instance."))
2612 2 (vcat [ ptext (sLit "Expected:") <+> ppr fam_tc_name
2613 , ptext (sLit " Actual:") <+> ppr eqn_tc_name ])
2614
2615 badRoleAnnot :: Name -> Role -> Role -> SDoc
2616 badRoleAnnot var annot inferred
2617 = hang (ptext (sLit "Role mismatch on variable") <+> ppr var <> colon)
2618 2 (sep [ ptext (sLit "Annotation says"), ppr annot
2619 , ptext (sLit "but role"), ppr inferred
2620 , ptext (sLit "is required") ])
2621
2622 wrongNumberOfRoles :: [a] -> LRoleAnnotDecl Name -> SDoc
2623 wrongNumberOfRoles tyvars d@(L _ (RoleAnnotDecl _ annots))
2624 = hang (ptext (sLit "Wrong number of roles listed in role annotation;") $$
2625 ptext (sLit "Expected") <+> (ppr $ length tyvars) <> comma <+>
2626 ptext (sLit "got") <+> (ppr $ length annots) <> colon)
2627 2 (ppr d)
2628
2629 illegalRoleAnnotDecl :: LRoleAnnotDecl Name -> TcM ()
2630 illegalRoleAnnotDecl (L loc (RoleAnnotDecl tycon _))
2631 = setErrCtxt [] $
2632 setSrcSpan loc $
2633 addErrTc (ptext (sLit "Illegal role annotation for") <+> ppr tycon <> char ';' $$
2634 ptext (sLit "they are allowed only for datatypes and classes."))
2635
2636 needXRoleAnnotations :: TyCon -> SDoc
2637 needXRoleAnnotations tc
2638 = ptext (sLit "Illegal role annotation for") <+> ppr tc <> char ';' $$
2639 ptext (sLit "did you intend to use RoleAnnotations?")
2640
2641 incoherentRoles :: SDoc
2642 incoherentRoles = (text "Roles other than" <+> quotes (text "nominal") <+>
2643 text "for class parameters can lead to incoherence.") $$
2644 (text "Use IncoherentInstances to allow this; bad role found")
2645
2646 addTyConCtxt :: TyCon -> TcM a -> TcM a
2647 addTyConCtxt tc
2648 = addErrCtxt ctxt
2649 where
2650 name = getName tc
2651 flav = text (tyConFlavour tc)
2652 ctxt = hsep [ ptext (sLit "In the"), flav
2653 , ptext (sLit "declaration for"), quotes (ppr name) ]
2654
2655 addRoleAnnotCtxt :: Name -> TcM a -> TcM a
2656 addRoleAnnotCtxt name
2657 = addErrCtxt $
2658 text "while checking a role annotation for" <+> quotes (ppr name)