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