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