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