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