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