never executed always true always false
1 {-
2 (c) The University of Glasgow 2006
3 (c) The AQUA Project, Glasgow University, 1996-1998
4
5 -}
6
7 {-# LANGUAGE CPP #-}
8 {-# LANGUAGE TupleSections, ScopedTypeVariables, MultiWayIf #-}
9 {-# LANGUAGE TypeFamilies #-}
10 {-# LANGUAGE ViewPatterns #-}
11 {-# LANGUAGE LambdaCase #-}
12
13 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
14
15 -- | Typecheck type and class declarations
16 module GHC.Tc.TyCl (
17 tcTyAndClassDecls,
18
19 -- Functions used by GHC.Tc.TyCl.Instance to check
20 -- data/type family instance declarations
21 kcConDecls, tcConDecls, DataDeclInfo(..),
22 dataDeclChecks, checkValidTyCon,
23 tcFamTyPats, tcTyFamInstEqn,
24 tcAddTyFamInstCtxt, tcMkDataFamInstCtxt, tcAddDataFamInstCtxt,
25 unravelFamInstPats, addConsistencyConstraints,
26 wrongKindOfFamily
27 ) where
28
29 import GHC.Prelude
30
31 import GHC.Driver.Env
32 import GHC.Driver.Session
33
34 import GHC.Hs
35
36 import GHC.Tc.Errors.Types ( TcRnMessage(..), FixedRuntimeRepProvenance(..) )
37 import GHC.Tc.TyCl.Build
38 import GHC.Tc.Solver( pushLevelAndSolveEqualities, pushLevelAndSolveEqualitiesX
39 , reportUnsolvedEqualities )
40 import GHC.Tc.Utils.Monad
41 import GHC.Tc.Utils.Env
42 import GHC.Tc.Utils.Unify( unifyType, emitResidualTvConstraint )
43 import GHC.Tc.Types.Constraint( emptyWC )
44 import GHC.Tc.Validity
45 import GHC.Tc.Utils.Zonk
46 import GHC.Tc.TyCl.Utils
47 import GHC.Tc.TyCl.Class
48 import {-# SOURCE #-} GHC.Tc.TyCl.Instance( tcInstDecls1 )
49 import GHC.Tc.Deriv (DerivInfo(..))
50 import GHC.Tc.Gen.HsType
51 import GHC.Tc.Instance.Class( AssocInstInfo(..) )
52 import GHC.Tc.Utils.TcMType
53 import GHC.Tc.Utils.TcType
54 import GHC.Tc.Instance.Family
55 import GHC.Tc.Types.Origin
56
57 import GHC.Builtin.Types (oneDataConTy, unitTy, makeRecoveryTyCon )
58
59 import GHC.Rename.Env( lookupConstructorFields )
60
61 import GHC.Core.Multiplicity
62 import GHC.Core.FamInstEnv
63 import GHC.Core.Coercion
64 import GHC.Core.Type
65 import GHC.Core.TyCo.Rep -- for checkValidRoles
66 import GHC.Core.TyCo.Ppr( pprTyVars )
67 import GHC.Core.Class
68 import GHC.Core.Coercion.Axiom
69 import GHC.Core.TyCon
70 import GHC.Core.DataCon
71 import GHC.Core.Unify
72
73 import GHC.Types.Error
74 import GHC.Types.Id
75 import GHC.Types.Var
76 import GHC.Types.Var.Env
77 import GHC.Types.Var.Set
78 import GHC.Types.Name
79 import GHC.Types.Name.Set
80 import GHC.Types.Name.Env
81 import GHC.Types.SrcLoc
82 import GHC.Types.SourceFile
83 import GHC.Types.Unique
84 import GHC.Types.Basic
85 import qualified GHC.LanguageExtensions as LangExt
86
87 import GHC.Data.FastString
88 import GHC.Data.Maybe
89 import GHC.Data.List.SetOps
90
91 import GHC.Unit
92
93 import GHC.Utils.Outputable
94 import GHC.Utils.Panic
95 import GHC.Utils.Panic.Plain
96 import GHC.Utils.Constants (debugIsOn)
97 import GHC.Utils.Misc
98
99 import Control.Monad
100 import Data.Function ( on )
101 import Data.Functor.Identity
102 import Data.List (nubBy, partition)
103 import Data.List.NonEmpty ( NonEmpty(..) )
104 import qualified Data.Set as Set
105 import Data.Tuple( swap )
106
107 {-
108 ************************************************************************
109 * *
110 \subsection{Type checking for type and class declarations}
111 * *
112 ************************************************************************
113
114 Note [Grouping of type and class declarations]
115 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
116 tcTyAndClassDecls is called on a list of `TyClGroup`s. Each group is a strongly
117 connected component of mutually dependent types and classes. We kind check and
118 type check each group separately to enhance kind polymorphism. Take the
119 following example:
120
121 type Id a = a
122 data X = X (Id Int)
123
124 If we were to kind check the two declarations together, we would give Id the
125 kind * -> *, since we apply it to an Int in the definition of X. But we can do
126 better than that, since Id really is kind polymorphic, and should get kind
127 forall (k::*). k -> k. Since it does not depend on anything else, it can be
128 kind-checked by itself, hence getting the most general kind. We then kind check
129 X, which works fine because we then know the polymorphic kind of Id, and simply
130 instantiate k to *.
131
132 Note [Check role annotations in a second pass]
133 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
134 Role inference potentially depends on the types of all of the datacons declared
135 in a mutually recursive group. The validity of a role annotation, in turn,
136 depends on the result of role inference. Because the types of datacons might
137 be ill-formed (see #7175 and Note [rejigConRes]) we must check
138 *all* the tycons in a group for validity before checking *any* of the roles.
139 Thus, we take two passes over the resulting tycons, first checking for general
140 validity and then checking for valid role annotations.
141 -}
142
143 tcTyAndClassDecls :: [TyClGroup GhcRn] -- Mutually-recursive groups in
144 -- dependency order
145 -> TcM ( TcGblEnv -- Input env extended by types and
146 -- classes
147 -- and their implicit Ids,DataCons
148 , [InstInfo GhcRn] -- Source-code instance decls info
149 , [DerivInfo] -- Deriving info
150 , ClassScopedTVEnv -- Class scoped type variables
151 , ThBindEnv -- TH binding levels
152 )
153 -- Fails if there are any errors
154 tcTyAndClassDecls tyclds_s
155 -- The code recovers internally, but if anything gave rise to
156 -- an error we'd better stop now, to avoid a cascade
157 -- Type check each group in dependency order folding the global env
158 = checkNoErrs $ fold_env [] [] emptyNameEnv emptyNameEnv tyclds_s
159 where
160 fold_env :: [InstInfo GhcRn]
161 -> [DerivInfo]
162 -> ClassScopedTVEnv
163 -> ThBindEnv
164 -> [TyClGroup GhcRn]
165 -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo], ClassScopedTVEnv, ThBindEnv)
166 fold_env inst_info deriv_info class_scoped_tv_env th_bndrs []
167 = do { gbl_env <- getGblEnv
168 ; return (gbl_env, inst_info, deriv_info, class_scoped_tv_env, th_bndrs) }
169 fold_env inst_info deriv_info class_scoped_tv_env th_bndrs (tyclds:tyclds_s)
170 = do { (tcg_env, inst_info', deriv_info', class_scoped_tv_env', th_bndrs')
171 <- tcTyClGroup tyclds
172 ; setGblEnv tcg_env $
173 -- remaining groups are typechecked in the extended global env.
174 fold_env (inst_info' ++ inst_info)
175 (deriv_info' ++ deriv_info)
176 (class_scoped_tv_env' `plusNameEnv` class_scoped_tv_env)
177 (th_bndrs' `plusNameEnv` th_bndrs)
178 tyclds_s }
179
180 tcTyClGroup :: TyClGroup GhcRn
181 -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo], ClassScopedTVEnv, ThBindEnv)
182 -- Typecheck one strongly-connected component of type, class, and instance decls
183 -- See Note [TyClGroups and dependency analysis] in GHC.Hs.Decls
184 tcTyClGroup (TyClGroup { group_tyclds = tyclds
185 , group_roles = roles
186 , group_kisigs = kisigs
187 , group_instds = instds })
188 = do { let role_annots = mkRoleAnnotEnv roles
189
190 -- Step 1: Typecheck the standalone kind signatures and type/class declarations
191 ; traceTc "---- tcTyClGroup ---- {" empty
192 ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds))
193 ; (tyclss, data_deriv_info, class_scoped_tv_env, kindless) <-
194 tcExtendKindEnv (mkPromotionErrorEnv tyclds) $ -- See Note [Type environment evolution]
195 do { kisig_env <- mkNameEnv <$> traverse tcStandaloneKindSig kisigs
196 ; tcTyClDecls tyclds kisig_env role_annots }
197
198 -- Step 1.5: Make sure we don't have any type synonym cycles
199 ; traceTc "Starting synonym cycle check" (ppr tyclss)
200 ; home_unit <- hsc_home_unit <$> getTopEnv
201 ; checkSynCycles (homeUnitAsUnit home_unit) tyclss tyclds
202 ; traceTc "Done synonym cycle check" (ppr tyclss)
203
204 -- Step 2: Perform the validity check on those types/classes
205 -- We can do this now because we are done with the recursive knot
206 -- Do it before Step 3 (adding implicit things) because the latter
207 -- expects well-formed TyCons
208 ; traceTc "Starting validity check" (ppr tyclss)
209 ; tyclss <- concatMapM checkValidTyCl tyclss
210 ; traceTc "Done validity check" (ppr tyclss)
211 ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
212 -- See Note [Check role annotations in a second pass]
213
214 ; traceTc "---- end tcTyClGroup ---- }" empty
215
216 -- Step 3: Add the implicit things;
217 -- we want them in the environment because
218 -- they may be mentioned in interface files
219 ; (gbl_env, th_bndrs) <- addTyConsToGblEnv tyclss
220
221 -- Step 4: check instance declarations
222 ; (gbl_env', inst_info, datafam_deriv_info, th_bndrs') <-
223 setGblEnv gbl_env $
224 tcInstDecls1 instds
225
226 ; let deriv_info = datafam_deriv_info ++ data_deriv_info
227 ; let gbl_env'' = gbl_env'
228 { tcg_ksigs = tcg_ksigs gbl_env' `unionNameSet` kindless }
229 ; return (gbl_env'', inst_info, deriv_info, class_scoped_tv_env,
230 th_bndrs' `plusNameEnv` th_bndrs) }
231
232 -- Gives the kind for every TyCon that has a standalone kind signature
233 type KindSigEnv = NameEnv Kind
234
235 tcTyClDecls
236 :: [LTyClDecl GhcRn]
237 -> KindSigEnv
238 -> RoleAnnotEnv
239 -> TcM ([TyCon], [DerivInfo], ClassScopedTVEnv, NameSet)
240 tcTyClDecls tyclds kisig_env role_annots
241 = do { -- Step 1: kind-check this group and returns the final
242 -- (possibly-polymorphic) kind of each TyCon and Class
243 -- See Note [Kind checking for type and class decls]
244 (tc_tycons, kindless) <- kcTyClGroup kisig_env tyclds
245 ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons))
246
247 -- Step 2: type-check all groups together, returning
248 -- the final TyCons and Classes
249 --
250 -- NB: We have to be careful here to NOT eagerly unfold
251 -- type synonyms, as we have not tested for type synonym
252 -- loops yet and could fall into a black hole.
253 ; fixM $ \ ~(rec_tyclss, _, _, _) -> do
254 { tcg_env <- getGblEnv
255 -- Forced so we don't retain a reference to the TcGblEnv
256 ; let !src = tcg_src tcg_env
257 roles = inferRoles src role_annots rec_tyclss
258 class_scoped_tv_env = mk_class_scoped_tv_env tc_tycons
259
260 -- Populate environment with knot-tied ATyCon for TyCons
261 -- NB: if the decls mention any ill-staged data cons
262 -- (see Note [Recursion and promoting data constructors])
263 -- we will have failed already in kcTyClGroup, so no worries here
264 ; (tycons, data_deriv_infos) <-
265 tcExtendRecEnv (zipRecTyClss tc_tycons rec_tyclss) $
266
267 -- Also extend the local type envt with bindings giving
268 -- a TcTyCon for each knot-tied TyCon or Class
269 -- See Note [Type checking recursive type and class declarations]
270 -- and Note [Type environment evolution]
271 tcExtendKindEnvWithTyCons tc_tycons $
272
273 -- Kind and type check declarations for this group
274 mapAndUnzipM (tcTyClDecl roles) tyclds
275 ; return (tycons, concat data_deriv_infos, class_scoped_tv_env, kindless)
276 } }
277 where
278 ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma
279 , ppr (tyConBinders tc) <> comma
280 , ppr (tyConResKind tc)
281 , ppr (isTcTyCon tc) ])
282
283 -- Map each class TcTyCon to their tcTyConScopedTyVars. This is ultimately
284 -- meant to be passed to GHC.Tc.TyCl.Class.tcClassDecl2, which consults
285 -- it when bringing type variables into scope over class method defaults.
286 -- See @Note [Scoped tyvars in a TcTyCon]@ in "GHC.Core.TyCon".
287 mk_class_scoped_tv_env :: [TcTyCon] -> ClassScopedTVEnv
288 mk_class_scoped_tv_env tc_tycons =
289 mkNameEnv [ (tyConName tc_tycon, tcTyConScopedTyVars tc_tycon)
290 | tc_tycon <- tc_tycons, tyConFlavour tc_tycon == ClassFlavour
291 ]
292
293 zipRecTyClss :: [TcTyCon]
294 -> [TyCon] -- Knot-tied
295 -> [(Name,TyThing)]
296 -- Build a name-TyThing mapping for the TyCons bound by decls
297 -- being careful not to look at the knot-tied [TyThing]
298 -- The TyThings in the result list must have a visible ATyCon,
299 -- because typechecking types (in, say, tcTyClDecl) looks at
300 -- this outer constructor
301 zipRecTyClss tc_tycons rec_tycons
302 = [ (name, ATyCon (get name)) | tc_tycon <- tc_tycons, let name = getName tc_tycon ]
303 where
304 rec_tc_env :: NameEnv TyCon
305 rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
306
307 add_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
308 add_tc tc env = foldr add_one_tc env (tc : tyConATs tc)
309
310 add_one_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
311 add_one_tc tc env = extendNameEnv env (tyConName tc) tc
312
313 get name = case lookupNameEnv rec_tc_env name of
314 Just tc -> tc
315 other -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
316
317 {-
318 ************************************************************************
319 * *
320 Kind checking
321 * *
322 ************************************************************************
323
324 Note [Kind checking for type and class decls]
325 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
326 Kind checking is done thus:
327
328 1. Make up a kind variable for each parameter of the declarations,
329 and extend the kind environment (which is in the TcLclEnv)
330
331 2. Kind check the declarations
332
333 We need to kind check all types in the mutually recursive group
334 before we know the kind of the type variables. For example:
335
336 class C a where
337 op :: D b => a -> b -> b
338
339 class D c where
340 bop :: (Monad c) => ...
341
342 Here, the kind of the locally-polymorphic type variable "b"
343 depends on *all the uses of class D*. For example, the use of
344 Monad c in bop's type signature means that D must have kind Type->Type.
345
346 Note: we don't treat type synonyms specially (we used to, in the past);
347 in particular, even if we have a type synonym cycle, we still kind check
348 it normally, and test for cycles later (checkSynCycles). The reason
349 we can get away with this is because we have more systematic TYPE r
350 inference, which means that we can do unification between kinds that
351 aren't lifted (this historically was not true.)
352
353 The downside of not directly reading off the kinds of the RHS of
354 type synonyms in topological order is that we don't transparently
355 support making synonyms of types with higher-rank kinds. But
356 you can always specify a CUSK directly to make this work out.
357 See tc269 for an example.
358
359 Note [CUSKs and PolyKinds]
360 ~~~~~~~~~~~~~~~~~~~~~~~~~~
361 Consider
362
363 data T (a :: *) = MkT (S a) -- Has CUSK
364 data S a = MkS (T Int) (S a) -- No CUSK
365
366 Via inferInitialKinds we get
367 T :: * -> *
368 S :: kappa -> *
369
370 Then we call kcTyClDecl on each decl in the group, to constrain the
371 kind unification variables. BUT we /skip/ the RHS of any decl with
372 a CUSK. Here we skip the RHS of T, so we eventually get
373 S :: forall k. k -> *
374
375 This gets us more polymorphism than we would otherwise get, similar
376 (but implemented strangely differently from) the treatment of type
377 signatures in value declarations.
378
379 However, we only want to do so when we have PolyKinds.
380 When we have NoPolyKinds, we don't skip those decls, because we have defaulting
381 (#16609). Skipping won't bring us more polymorphism when we have defaulting.
382 Consider
383
384 data T1 a = MkT1 T2 -- No CUSK
385 data T2 = MkT2 (T1 Maybe) -- Has CUSK
386
387 If we skip the rhs of T2 during kind-checking, the kind of a remains unsolved.
388 With PolyKinds, we do generalization to get T1 :: forall a. a -> *. And the
389 program type-checks.
390 But with NoPolyKinds, we do defaulting to get T1 :: * -> *. Defaulting happens
391 in quantifyTyVars, which is called from generaliseTcTyCon. Then type-checking
392 (T1 Maybe) will throw a type error.
393
394 Summary: with PolyKinds, we must skip; with NoPolyKinds, we must /not/ skip.
395
396 Open type families
397 ~~~~~~~~~~~~~~~~~~
398 This treatment of type synonyms only applies to Haskell 98-style synonyms.
399 General type functions can be recursive, and hence, appear in `alg_decls'.
400
401 The kind of an open type family is solely determinded by its kind signature;
402 hence, only kind signatures participate in the construction of the initial
403 kind environment (as constructed by `inferInitialKind'). In fact, we ignore
404 instances of families altogether in the following. However, we need to include
405 the kinds of *associated* families into the construction of the initial kind
406 environment. (This is handled by `allDecls').
407
408 See also Note [Kind checking recursive type and class declarations]
409
410 Note [How TcTyCons work]
411 ~~~~~~~~~~~~~~~~~~~~~~~~
412 TcTyCons are used for two distinct purposes
413
414 1. When recovering from a type error in a type declaration,
415 we want to put the erroneous TyCon in the environment in a
416 way that won't lead to more errors. We use a TcTyCon for this;
417 see makeRecoveryTyCon.
418
419 2. When checking a type/class declaration (in module GHC.Tc.TyCl), we come
420 upon knowledge of the eventual tycon in bits and pieces.
421
422 S1) First, we use inferInitialKinds to look over the user-provided
423 kind signature of a tycon (including, for example, the number
424 of parameters written to the tycon) to get an initial shape of
425 the tycon's kind. We record that shape in a TcTyCon.
426
427 For CUSK tycons, the TcTyCon has the final, generalised kind.
428 For non-CUSK tycons, the TcTyCon has as its tyConBinders only
429 the explicit arguments given -- no kind variables, etc.
430
431 S2) Then, using these initial kinds, we kind-check the body of the
432 tycon (class methods, data constructors, etc.), filling in the
433 metavariables in the tycon's initial kind.
434
435 S3) We then generalize to get the (non-CUSK) tycon's final, fixed
436 kind. Finally, once this has happened for all tycons in a
437 mutually recursive group, we can desugar the lot.
438
439 For convenience, we store partially-known tycons in TcTyCons, which
440 might store meta-variables. These TcTyCons are stored in the local
441 environment in GHC.Tc.TyCl, until the real full TyCons can be created
442 during desugaring. A desugared program should never have a TcTyCon.
443
444 3. In a TcTyCon, everything is zonked after the kind-checking pass (S2).
445
446 4. tyConScopedTyVars. A challenging piece in all of this is that we
447 end up taking three separate passes over every declaration:
448 - one in inferInitialKind (this pass look only at the head, not the body)
449 - one in kcTyClDecls (to kind-check the body)
450 - a final one in tcTyClDecls (to desugar)
451
452 In the latter two passes, we need to connect the user-written type
453 variables in an LHsQTyVars with the variables in the tycon's
454 inferred kind. Because the tycon might not have a CUSK, this
455 matching up is, in general, quite hard to do. (Look through the
456 git history between Dec 2015 and Apr 2016 for
457 GHC.Tc.Gen.HsType.splitTelescopeTvs!)
458
459 Instead of trying, we just store the list of type variables to
460 bring into scope, in the tyConScopedTyVars field of the TcTyCon.
461 These tyvars are brought into scope in GHC.Tc.Gen.HsType.bindTyClTyVars.
462
463 In a TcTyCon, why is tyConScopedTyVars :: [(Name,TcTyVar)] rather
464 than just [TcTyVar]? Consider these mutually-recursive decls
465 data T (a :: k1) b = MkT (S a b)
466 data S (c :: k2) d = MkS (T c d)
467 We start with k1 bound to kappa1, and k2 to kappa2; so initially
468 in the (Name,TcTyVar) pairs the Name is that of the TcTyVar. But
469 then kappa1 and kappa2 get unified; so after the zonking in
470 'generalise' in 'kcTyClGroup' the Name and TcTyVar may differ.
471
472 See also Note [Type checking recursive type and class declarations].
473
474 Note [Swizzling the tyvars before generaliseTcTyCon]
475 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
476 This Note only applies when /inferring/ the kind of a TyCon.
477 If there is a separate kind signature, or a CUSK, we take an entirely
478 different code path.
479
480 For inference, consider
481 class C (f :: k) x where
482 type T f
483 op :: D f => blah
484 class D (g :: j) y where
485 op :: C g => y -> blah
486
487 Here C and D are considered mutually recursive. Neither has a CUSK.
488 Just before generalisation we have the (un-quantified) kinds
489 C :: k1 -> k2 -> Constraint
490 T :: k1 -> Type
491 D :: k1 -> Type -> Constraint
492 Notice that f's kind and g's kind have been unified to 'k1'. We say
493 that k1 is the "representative" of k in C's decl, and of j in D's decl.
494
495 Now when quantifying, we'd like to end up with
496 C :: forall {k2}. forall k. k -> k2 -> Constraint
497 T :: forall k. k -> Type
498 D :: forall j. j -> Type -> Constraint
499
500 That is, we want to swizzle the representative to have the Name given
501 by the user. Partly this is to improve error messages and the output of
502 :info in GHCi. But it is /also/ important because the code for a
503 default method may mention the class variable(s), but at that point
504 (tcClassDecl2), we only have the final class tyvars available.
505 (Alternatively, we could record the scoped type variables in the
506 TyCon, but it's a nuisance to do so.)
507
508 Notes:
509
510 * On the input to generaliseTyClDecl, the mapping between the
511 user-specified Name and the representative TyVar is recorded in the
512 tyConScopedTyVars of the TcTyCon. NB: you first need to zonk to see
513 this representative TyVar.
514
515 * The swizzling is actually performed by swizzleTcTyConBndrs
516
517 * We must do the swizzling across the whole class decl. Consider
518 class C f where
519 type S (f :: k)
520 type T f
521 Here f's kind k is a parameter of C, and its identity is shared
522 with S and T. So if we swizzle the representative k at all, we
523 must do so consistently for the entire declaration.
524
525 Hence the call to check_duplicate_tc_binders is in generaliseTyClDecl,
526 rather than in generaliseTcTyCon.
527
528 There are errors to catch here. Suppose we had
529 class E (f :: j) (g :: k) where
530 op :: SameKind f g -> blah
531
532 Then, just before generalisation we will have the (unquantified)
533 E :: k1 -> k1 -> Constraint
534
535 That's bad! Two distinctly-named tyvars (j and k) have ended up with
536 the same representative k1. So when swizzling, we check (in
537 check_duplicate_tc_binders) that two distinct source names map
538 to the same representative.
539
540 Here's an interesting case:
541 class C1 f where
542 type S (f :: k1)
543 type T (f :: k2)
544 Here k1 and k2 are different Names, but they end up mapped to the
545 same representative TyVar. To make the swizzling consistent (remember
546 we must have a single k across C1, S and T) we reject the program.
547
548 Another interesting case
549 class C2 f where
550 type S (f :: k) (p::Type)
551 type T (f :: k) (p::Type->Type)
552
553 Here the two k's (and the two p's) get distinct Uniques, because they
554 are seen by the renamer as locally bound in S and T resp. But again
555 the two (distinct) k's end up bound to the same representative TyVar.
556 You might argue that this should be accepted, but it's definitely
557 rejected (via an entirely different code path) if you add a kind sig:
558 type C2' :: j -> Constraint
559 class C2' f where
560 type S (f :: k) (p::Type)
561 We get
562 • Expected kind ‘j’, but ‘f’ has kind ‘k’
563 • In the associated type family declaration for ‘S’
564
565 So we reject C2 too, even without the kind signature. We have
566 to do a bit of work to get a good error message, since both k's
567 look the same to the user.
568
569 Another case
570 class C3 (f :: k1) where
571 type S (f :: k2)
572
573 This will be rejected too.
574
575
576 Note [Type environment evolution]
577 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
578 As we typecheck a group of declarations the type environment evolves.
579 Consider for example:
580 data B (a :: Type) = MkB (Proxy 'MkB)
581
582 We do the following steps:
583
584 1. Start of tcTyClDecls: use mkPromotionErrorEnv to initialise the
585 type env with promotion errors
586 B :-> TyConPE
587 MkB :-> DataConPE
588
589 2. kcTyCLGroup
590 - Do inferInitialKinds, which will signal a promotion
591 error if B is used in any of the kinds needed to initialise
592 B's kind (e.g. (a :: Type)) here
593
594 - Extend the type env with these initial kinds (monomorphic for
595 decls that lack a CUSK)
596 B :-> TcTyCon <initial kind>
597 (thereby overriding the B :-> TyConPE binding)
598 and do kcLTyClDecl on each decl to get equality constraints on
599 all those initial kinds
600
601 - Generalise the initial kind, making a poly-kinded TcTyCon
602
603 3. Back in tcTyDecls, extend the envt with bindings of the poly-kinded
604 TcTyCons, again overriding the promotion-error bindings.
605
606 But note that the data constructor promotion errors are still in place
607 so that (in our example) a use of MkB will still be signalled as
608 an error.
609
610 4. Typecheck the decls.
611
612 5. In tcTyClGroup, extend the envt with bindings for TyCon and DataCons
613
614
615 Note [Missed opportunity to retain higher-rank kinds]
616 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
617 In 'kcTyClGroup', there is a missed opportunity to make kind
618 inference work in a few more cases. The idea is analogous
619 to Note [Single function non-recursive binding special-case]:
620
621 * If we have an SCC with a single decl, which is non-recursive,
622 instead of creating a unification variable representing the
623 kind of the decl and unifying it with the rhs, we can just
624 read the type directly of the rhs.
625
626 * Furthermore, we can update our SCC analysis to ignore
627 dependencies on declarations which have CUSKs: we don't
628 have to kind-check these all at once, since we can use
629 the CUSK to initialize the kind environment.
630
631 Unfortunately this requires reworking a bit of the code in
632 'kcLTyClDecl' so I've decided to punt unless someone shouts about it.
633
634 Note [Don't process associated types in getInitialKind]
635 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
636 Previously, we processed associated types in the thing_inside in getInitialKind,
637 but this was wrong -- we want to do ATs sepearately.
638 The consequence for not doing it this way is #15142:
639
640 class ListTuple (tuple :: Type) (as :: [(k, Type)]) where
641 type ListToTuple as :: Type
642
643 We assign k a kind kappa[1]. When checking the tuple (k, Type), we try to unify
644 kappa ~ Type, but this gets deferred because we bumped the TcLevel as we bring
645 `tuple` into scope. Thus, when we check ListToTuple, kappa[1] still hasn't
646 unified with Type. And then, when we generalize the kind of ListToTuple (which
647 indeed has a CUSK, according to the rules), we skolemize the free metavariable
648 kappa. Note that we wouldn't skolemize kappa when generalizing the kind of ListTuple,
649 because the solveEqualities in kcInferDeclHeader is at TcLevel 1 and so kappa[1]
650 will unify with Type.
651
652 Bottom line: as associated types should have no effect on a CUSK enclosing class,
653 we move processing them to a separate action, run after the outer kind has
654 been generalized.
655
656 -}
657
658 kcTyClGroup :: KindSigEnv -> [LTyClDecl GhcRn] -> TcM ([TcTyCon], NameSet)
659
660 -- Kind check this group, kind generalize, and return the resulting local env
661 -- This binds the TyCons and Classes of the group, but not the DataCons
662 -- See Note [Kind checking for type and class decls]
663 -- and Note [Inferring kinds for type declarations]
664 --
665 -- The NameSet returned contains kindless tycon names, without CUSK or SAKS.
666 kcTyClGroup kisig_env decls
667 = do { mod <- getModule
668 ; traceTc "---- kcTyClGroup ---- {"
669 (text "module" <+> ppr mod $$ vcat (map ppr decls))
670
671 -- Kind checking;
672 -- 1. Bind kind variables for decls
673 -- 2. Kind-check decls
674 -- 3. Generalise the inferred kinds
675 -- See Note [Kind checking for type and class decls]
676
677 ; cusks_enabled <- xoptM LangExt.CUSKs <&&> xoptM LangExt.PolyKinds
678 -- See Note [CUSKs and PolyKinds]
679 ; let (kindless_decls, kinded_decls) = partitionWith get_kind decls
680 kindless_names = mkNameSet $ map get_name kindless_decls
681
682 get_name d = tcdName (unLoc d)
683
684 get_kind d
685 | Just ki <- lookupNameEnv kisig_env (get_name d)
686 = Right (d, SAKS ki)
687
688 | cusks_enabled && hsDeclHasCusk (unLoc d)
689 = Right (d, CUSK)
690
691 | otherwise = Left d
692
693 ; checked_tcs <- checkNoErrs $
694 checkInitialKinds kinded_decls
695 -- checkNoErrs because we are about to extend
696 -- the envt with these tycons, and we get
697 -- knock-on errors if we have tycons with
698 -- malformed kinds
699
700 ; inferred_tcs
701 <- tcExtendKindEnvWithTyCons checked_tcs $
702 pushLevelAndSolveEqualities UnkSkol [] $
703 -- We are going to kind-generalise, so unification
704 -- variables in here must be one level in
705 do { -- Step 1: Bind kind variables for all decls
706 mono_tcs <- inferInitialKinds kindless_decls
707
708 ; traceTc "kcTyClGroup: initial kinds" $
709 ppr_tc_kinds mono_tcs
710
711 -- Step 2: Set extended envt, kind-check the decls
712 -- NB: the environment extension overrides the tycon
713 -- promotion-errors bindings
714 -- See Note [Type environment evolution]
715 ; checkNoErrs $
716 tcExtendKindEnvWithTyCons mono_tcs $
717 mapM_ kcLTyClDecl kindless_decls
718
719 ; return mono_tcs }
720
721 -- Step 3: generalisation
722 -- Finally, go through each tycon and give it its final kind,
723 -- with all the required, specified, and inferred variables
724 -- in order.
725 ; let inferred_tc_env = mkNameEnv $
726 map (\tc -> (tyConName tc, tc)) inferred_tcs
727 ; generalized_tcs <- concatMapM (generaliseTyClDecl inferred_tc_env)
728 kindless_decls
729
730 ; let poly_tcs = checked_tcs ++ generalized_tcs
731 ; traceTc "---- kcTyClGroup end ---- }" (ppr_tc_kinds poly_tcs)
732 ; return (poly_tcs, kindless_names) }
733 where
734 ppr_tc_kinds tcs = vcat (map pp_tc tcs)
735 pp_tc tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc)
736
737 type ScopedPairs = [(Name, TcTyVar)]
738 -- The ScopedPairs for a TcTyCon are precisely
739 -- specified-tvs ++ required-tvs
740 -- You can distinguish them because there are tyConArity required-tvs
741
742 generaliseTyClDecl :: NameEnv TcTyCon -> LTyClDecl GhcRn -> TcM [TcTyCon]
743 -- See Note [Swizzling the tyvars before generaliseTcTyCon]
744 generaliseTyClDecl inferred_tc_env (L _ decl)
745 = do { let names_in_this_decl :: [Name]
746 names_in_this_decl = tycld_names decl
747
748 -- Extract the specified/required binders and skolemise them
749 ; tc_with_tvs <- mapM skolemise_tc_tycon names_in_this_decl
750
751 -- Zonk, to manifest the side-effects of skolemisation to the swizzler
752 -- NB: it's important to skolemise them all before this step. E.g.
753 -- class C f where { type T (f :: k) }
754 -- We only skolemise k when looking at T's binders,
755 -- but k appears in f's kind in C's binders.
756 ; tc_infos <- mapM zonk_tc_tycon tc_with_tvs
757
758 -- Swizzle
759 ; swizzled_infos <- tcAddDeclCtxt decl (swizzleTcTyConBndrs tc_infos)
760
761 -- And finally generalise
762 ; mapAndReportM generaliseTcTyCon swizzled_infos }
763 where
764 tycld_names :: TyClDecl GhcRn -> [Name]
765 tycld_names decl = tcdName decl : at_names decl
766
767 at_names :: TyClDecl GhcRn -> [Name]
768 at_names (ClassDecl { tcdATs = ats }) = map (familyDeclName . unLoc) ats
769 at_names _ = [] -- Only class decls have associated types
770
771 skolemise_tc_tycon :: Name -> TcM (TcTyCon, ScopedPairs)
772 -- Zonk and skolemise the Specified and Required binders
773 skolemise_tc_tycon tc_name
774 = do { let tc = lookupNameEnv_NF inferred_tc_env tc_name
775 -- This lookup should not fail
776 ; scoped_prs <- mapSndM zonkAndSkolemise (tcTyConScopedTyVars tc)
777 ; return (tc, scoped_prs) }
778
779 zonk_tc_tycon :: (TcTyCon, ScopedPairs) -> TcM (TcTyCon, ScopedPairs, TcKind)
780 zonk_tc_tycon (tc, scoped_prs)
781 = do { scoped_prs <- mapSndM zonkTcTyVarToTyVar scoped_prs
782 -- We really have to do this again, even though
783 -- we have just done zonkAndSkolemise
784 ; res_kind <- zonkTcType (tyConResKind tc)
785 ; return (tc, scoped_prs, res_kind) }
786
787 swizzleTcTyConBndrs :: [(TcTyCon, ScopedPairs, TcKind)]
788 -> TcM [(TcTyCon, ScopedPairs, TcKind)]
789 swizzleTcTyConBndrs tc_infos
790 | all no_swizzle swizzle_prs
791 -- This fast path happens almost all the time
792 -- See Note [Cloning for type variable binders] in GHC.Tc.Gen.HsType
793 -- "Almost all the time" means not the case of mutual recursion with
794 -- polymorphic kinds.
795 = do { traceTc "Skipping swizzleTcTyConBndrs for" (ppr (map fstOf3 tc_infos))
796 ; return tc_infos }
797
798 | otherwise
799 = do { check_duplicate_tc_binders
800
801 ; traceTc "swizzleTcTyConBndrs" $
802 vcat [ text "before" <+> ppr_infos tc_infos
803 , text "swizzle_prs" <+> ppr swizzle_prs
804 , text "after" <+> ppr_infos swizzled_infos ]
805
806 ; return swizzled_infos }
807
808 where
809 swizzled_infos = [ (tc, mapSnd swizzle_var scoped_prs, swizzle_ty kind)
810 | (tc, scoped_prs, kind) <- tc_infos ]
811
812 swizzle_prs :: [(Name,TyVar)]
813 -- Pairs the user-specified Name with its representative TyVar
814 -- See Note [Swizzling the tyvars before generaliseTcTyCon]
815 swizzle_prs = [ pr | (_, prs, _) <- tc_infos, pr <- prs ]
816
817 no_swizzle :: (Name,TyVar) -> Bool
818 no_swizzle (nm, tv) = nm == tyVarName tv
819
820 ppr_infos infos = vcat [ ppr tc <+> pprTyVars (map snd prs)
821 | (tc, prs, _) <- infos ]
822
823 -- Check for duplicates
824 -- E.g. data SameKind (a::k) (b::k)
825 -- data T (a::k1) (b::k2) = MkT (SameKind a b)
826 -- Here k1 and k2 start as TyVarTvs, and get unified with each other
827 -- If this happens, things get very confused later, so fail fast
828 check_duplicate_tc_binders :: TcM ()
829 check_duplicate_tc_binders = unless (null err_prs) $
830 do { mapM_ report_dup err_prs; failM }
831
832 -------------- Error reporting ------------
833 err_prs :: [(Name,Name)]
834 err_prs = [ (n1,n2)
835 | pr :| prs <- findDupsEq ((==) `on` snd) swizzle_prs
836 , (n1,_):(n2,_):_ <- [nubBy ((==) `on` fst) (pr:prs)] ]
837 -- This nubBy avoids bogus error reports when we have
838 -- [("f", f), ..., ("f",f)....] in swizzle_prs
839 -- which happens with class C f where { type T f }
840
841 report_dup :: (Name,Name) -> TcM ()
842 report_dup (n1,n2)
843 = setSrcSpan (getSrcSpan n2) $ addErrTc $ TcRnUnknownMessage $ mkPlainError noHints $
844 hang (text "Different names for the same type variable:") 2 info
845 where
846 info | nameOccName n1 /= nameOccName n2
847 = quotes (ppr n1) <+> text "and" <+> quotes (ppr n2)
848 | otherwise -- Same OccNames! See C2 in
849 -- Note [Swizzling the tyvars before generaliseTcTyCon]
850 = vcat [ quotes (ppr n1) <+> text "bound at" <+> ppr (getSrcLoc n1)
851 , quotes (ppr n2) <+> text "bound at" <+> ppr (getSrcLoc n2) ]
852
853 -------------- The swizzler ------------
854 -- This does a deep traverse, simply doing a
855 -- Name-to-Name change, governed by swizzle_env
856 -- The 'swap' is what gets from the representative TyVar
857 -- back to the original user-specified Name
858 swizzle_env = mkVarEnv (map swap swizzle_prs)
859
860 swizzleMapper :: TyCoMapper () Identity
861 swizzleMapper = TyCoMapper { tcm_tyvar = swizzle_tv
862 , tcm_covar = swizzle_cv
863 , tcm_hole = swizzle_hole
864 , tcm_tycobinder = swizzle_bndr
865 , tcm_tycon = swizzle_tycon }
866 swizzle_hole _ hole = pprPanic "swizzle_hole" (ppr hole)
867 -- These types are pre-zonked
868 swizzle_tycon tc = pprPanic "swizzle_tc" (ppr tc)
869 -- TcTyCons can't appear in kinds (yet)
870 swizzle_tv _ tv = return (mkTyVarTy (swizzle_var tv))
871 swizzle_cv _ cv = return (mkCoVarCo (swizzle_var cv))
872
873 swizzle_bndr _ tcv _
874 = return ((), swizzle_var tcv)
875
876 swizzle_var :: Var -> Var
877 swizzle_var v
878 | Just nm <- lookupVarEnv swizzle_env v
879 = updateVarType swizzle_ty (v `setVarName` nm)
880 | otherwise
881 = updateVarType swizzle_ty v
882
883 (map_type, _, _, _) = mapTyCo swizzleMapper
884 swizzle_ty ty = runIdentity (map_type ty)
885
886
887 generaliseTcTyCon :: (TcTyCon, ScopedPairs, TcKind) -> TcM TcTyCon
888 generaliseTcTyCon (tc, scoped_prs, tc_res_kind)
889 -- See Note [Required, Specified, and Inferred for types]
890 = setSrcSpan (getSrcSpan tc) $
891 addTyConCtxt tc $
892 do { -- Step 1: Separate Specified from Required variables
893 -- NB: spec_req_tvs = spec_tvs ++ req_tvs
894 -- And req_tvs is 1-1 with tyConTyVars
895 -- See Note [Scoped tyvars in a TcTyCon] in GHC.Core.TyCon
896 ; let spec_req_tvs = map snd scoped_prs
897 n_spec = length spec_req_tvs - tyConArity tc
898 (spec_tvs, req_tvs) = splitAt n_spec spec_req_tvs
899 sorted_spec_tvs = scopedSort spec_tvs
900 -- NB: We can't do the sort until we've zonked
901 -- Maintain the L-R order of scoped_tvs
902
903 -- Step 2a: find all the Inferred variables we want to quantify over
904 ; dvs1 <- candidateQTyVarsOfKinds $
905 (tc_res_kind : map tyVarKind spec_req_tvs)
906 ; let dvs2 = dvs1 `delCandidates` spec_req_tvs
907
908 -- Step 2b: quantify, mainly meaning skolemise the free variables
909 -- Returned 'inferred' are scope-sorted and skolemised
910 ; inferred <- quantifyTyVars allVarsOfKindDefault dvs2
911
912 ; traceTc "generaliseTcTyCon: pre zonk"
913 (vcat [ text "tycon =" <+> ppr tc
914 , text "spec_req_tvs =" <+> pprTyVars spec_req_tvs
915 , text "tc_res_kind =" <+> ppr tc_res_kind
916 , text "dvs1 =" <+> ppr dvs1
917 , text "inferred =" <+> pprTyVars inferred ])
918
919 -- Step 3: Final zonk (following kind generalisation)
920 -- See Note [Swizzling the tyvars before generaliseTcTyCon]
921 ; ze <- mkEmptyZonkEnv NoFlexi
922 ; (ze, inferred) <- zonkTyBndrsX ze inferred
923 ; (ze, sorted_spec_tvs) <- zonkTyBndrsX ze sorted_spec_tvs
924 ; (ze, req_tvs) <- zonkTyBndrsX ze req_tvs
925 ; tc_res_kind <- zonkTcTypeToTypeX ze tc_res_kind
926
927 ; traceTc "generaliseTcTyCon: post zonk" $
928 vcat [ text "tycon =" <+> ppr tc
929 , text "inferred =" <+> pprTyVars inferred
930 , text "spec_req_tvs =" <+> pprTyVars spec_req_tvs
931 , text "sorted_spec_tvs =" <+> pprTyVars sorted_spec_tvs
932 , text "req_tvs =" <+> ppr req_tvs
933 , text "zonk-env =" <+> ppr ze ]
934
935 -- Step 4: Make the TyConBinders.
936 ; let dep_fv_set = candidateKindVars dvs1
937 inferred_tcbs = mkNamedTyConBinders Inferred inferred
938 specified_tcbs = mkNamedTyConBinders Specified sorted_spec_tvs
939 required_tcbs = map (mkRequiredTyConBinder dep_fv_set) req_tvs
940
941 -- Step 5: Assemble the final list.
942 final_tcbs = concat [ inferred_tcbs
943 , specified_tcbs
944 , required_tcbs ]
945
946 -- Step 6: Make the result TcTyCon
947 tycon = mkTcTyCon (tyConName tc) final_tcbs tc_res_kind
948 (mkTyVarNamePairs (sorted_spec_tvs ++ req_tvs))
949 True {- it's generalised now -}
950 (tyConFlavour tc)
951
952 ; traceTc "generaliseTcTyCon done" $
953 vcat [ text "tycon =" <+> ppr tc
954 , text "tc_res_kind =" <+> ppr tc_res_kind
955 , text "dep_fv_set =" <+> ppr dep_fv_set
956 , text "inferred_tcbs =" <+> ppr inferred_tcbs
957 , text "specified_tcbs =" <+> ppr specified_tcbs
958 , text "required_tcbs =" <+> ppr required_tcbs
959 , text "final_tcbs =" <+> ppr final_tcbs ]
960
961 -- Step 7: Check for validity.
962 -- We do this here because we're about to put the tycon into the
963 -- the environment, and we don't want anything malformed there
964 ; checkTyConTelescope tycon
965
966 ; return tycon }
967
968 {- Note [Required, Specified, and Inferred for types]
969 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
970 Each forall'd type variable in a type or kind is one of
971
972 * Required: an argument must be provided at every call site
973
974 * Specified: the argument can be inferred at call sites, but
975 may be instantiated with visible type/kind application
976
977 * Inferred: the argument must be inferred at call sites; it
978 is unavailable for use with visible type/kind application.
979
980 Why have Inferred at all? Because we just can't make user-facing
981 promises about the ordering of some variables. These might swizzle
982 around even between minor released. By forbidding visible type
983 application, we ensure users aren't caught unawares.
984
985 Go read Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in GHC.Core.TyCo.Rep.
986
987 The question for this Note is this:
988 given a TyClDecl, how are its quantified type variables classified?
989 Much of the debate is memorialized in #15743.
990
991 Here is our design choice. When inferring the ordering of variables
992 for a TyCl declaration (that is, for those variables that the user
993 has not specified the order with an explicit `forall`), we use the
994 following order:
995
996 1. Inferred variables
997 2. Specified variables; in the left-to-right order in which
998 the user wrote them, modified by scopedSort (see below)
999 to put them in depdendency order.
1000 3. Required variables before a top-level ::
1001 4. All variables after a top-level ::
1002
1003 If this ordering does not make a valid telescope, we reject the definition.
1004
1005 Example:
1006 data SameKind :: k -> k -> *
1007 data Bad a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
1008
1009 For Bad:
1010 - a, c, d, x are Required; they are explicitly listed by the user
1011 as the positional arguments of Bad
1012 - b is Specified; it appears explicitly in a kind signature
1013 - k, the kind of a, is Inferred; it is not mentioned explicitly at all
1014
1015 Putting variables in the order Inferred, Specified, Required
1016 gives us this telescope:
1017 Inferred: k
1018 Specified: b : Proxy a
1019 Required : (a : k) (c : Proxy b) (d : Proxy a) (x : SameKind b d)
1020
1021 But this order is ill-scoped, because b's kind mentions a, which occurs
1022 after b in the telescope. So we reject Bad.
1023
1024 Associated types
1025 ~~~~~~~~~~~~~~~~
1026 For associated types everything above is determined by the
1027 associated-type declaration alone, ignoring the class header.
1028 Here is an example (#15592)
1029 class C (a :: k) b where
1030 type F (x :: b a)
1031
1032 In the kind of C, 'k' is Specified. But what about F?
1033 In the kind of F,
1034
1035 * Should k be Inferred or Specified? It's Specified for C,
1036 but not mentioned in F's declaration.
1037
1038 * In which order should the Specified variables a and b occur?
1039 It's clearly 'a' then 'b' in C's declaration, but the L-R ordering
1040 in F's declaration is 'b' then 'a'.
1041
1042 In both cases we make the choice by looking at F's declaration alone,
1043 so it gets the kind
1044 F :: forall {k}. forall b a. b a -> Type
1045
1046 How it works
1047 ~~~~~~~~~~~~
1048 These design choices are implemented by two completely different code
1049 paths for
1050
1051 * Declarations with a standalone kind signature or a complete user-specified
1052 kind signature (CUSK). Handled by the kcCheckDeclHeader.
1053
1054 * Declarations without a kind signature (standalone or CUSK) are handled by
1055 kcInferDeclHeader; see Note [Inferring kinds for type declarations].
1056
1057 Note that neither code path worries about point (4) above, as this
1058 is nicely handled by not mangling the res_kind. (Mangling res_kinds is done
1059 *after* all this stuff, in tcDataDefn's call to etaExpandAlgTyCon.)
1060
1061 We can tell Inferred apart from Specified by looking at the scoped
1062 tyvars; Specified are always included there.
1063
1064 Design alternatives
1065 ~~~~~~~~~~~~~~~~~~~
1066 * For associated types we considered putting the class variables
1067 before the local variables, in a nod to the treatment for class
1068 methods. But it got too compilicated; see #15592, comment:21ff.
1069
1070 * We rigidly require the ordering above, even though we could be much more
1071 permissive. Relevant musings are at
1072 https://gitlab.haskell.org/ghc/ghc/issues/15743#note_161623
1073 The bottom line conclusion is that, if the user wants a different ordering,
1074 then can specify it themselves, and it is better to be predictable and dumb
1075 than clever and capricious.
1076
1077 I (Richard) conjecture we could be fully permissive, allowing all classes
1078 of variables to intermix. We would have to augment ScopedSort to refuse to
1079 reorder Required variables (or check that it wouldn't have). But this would
1080 allow more programs. See #15743 for examples. Interestingly, Idris seems
1081 to allow this intermixing. The intermixing would be fully specified, in that
1082 we can be sure that inference wouldn't change between versions. However,
1083 would users be able to predict it? That I cannot answer.
1084
1085 Test cases (and tickets) relevant to these design decisions
1086 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1087 T15591*
1088 T15592*
1089 T15743*
1090
1091 Note [Inferring kinds for type declarations]
1092 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1093 This note deals with /inference/ for type declarations
1094 that do not have a CUSK. Consider
1095 data T (a :: k1) k2 (x :: k2) = MkT (S a k2 x)
1096 data S (b :: k3) k4 (y :: k4) = MkS (T b k4 y)
1097
1098 We do kind inference as follows:
1099
1100 * Step 1: inferInitialKinds, and in particular kcInferDeclHeader.
1101 Make a unification variable for each of the Required and Specified
1102 type variables in the header.
1103
1104 Record the connection between the Names the user wrote and the
1105 fresh unification variables in the tcTyConScopedTyVars field
1106 of the TcTyCon we are making
1107 [ (a, aa)
1108 , (k1, kk1)
1109 , (k2, kk2)
1110 , (x, xx) ]
1111 (I'm using the convention that double letter like 'aa' or 'kk'
1112 mean a unification variable.)
1113
1114 These unification variables
1115 - Are TyVarTvs: that is, unification variables that can
1116 unify only with other type variables.
1117 See Note [TyVarTv] in GHC.Tc.Utils.TcMType
1118
1119 - Have complete fresh Names; see GHC.Tc.Utils.TcMType
1120 Note [Unification variables need fresh Names]
1121
1122 Assign initial monomorphic kinds to S, T
1123 T :: kk1 -> * -> kk2 -> *
1124 S :: kk3 -> * -> kk4 -> *
1125
1126 * Step 2: kcTyClDecl. Extend the environment with a TcTyCon for S and
1127 T, with these monomorphic kinds. Now kind-check the declarations,
1128 and solve the resulting equalities. The goal here is to discover
1129 constraints on all these unification variables.
1130
1131 Here we find that kk1 := kk3, and kk2 := kk4.
1132
1133 This is why we can't use skolems for kk1 etc; they have to
1134 unify with each other.
1135
1136 * Step 3: generaliseTcTyCon. Generalise each TyCon in turn.
1137 We find the free variables of the kind, skolemise them,
1138 sort them out into Inferred/Required/Specified (see the above
1139 Note [Required, Specified, and Inferred for types]),
1140 and perform some validity checks.
1141
1142 This makes the utterly-final TyConBinders for the TyCon.
1143
1144 All this is very similar at the level of terms: see GHC.Tc.Gen.Bind
1145 Note [Quantified variables in partial type signatures]
1146
1147 But there are some tricky corners: Note [Tricky scoping in generaliseTcTyCon]
1148
1149 * Step 4. Extend the type environment with a TcTyCon for S and T, now
1150 with their utterly-final polymorphic kinds (needed for recursive
1151 occurrences of S, T). Now typecheck the declarations, and build the
1152 final AlgTyCon for S and T resp.
1153
1154 The first three steps are in kcTyClGroup; the fourth is in
1155 tcTyClDecls.
1156
1157 There are some wrinkles
1158
1159 * Do not default TyVarTvs. We always want to kind-generalise over
1160 TyVarTvs, and /not/ default them to Type. By definition a TyVarTv is
1161 not allowed to unify with a type; it must stand for a type
1162 variable. Hence the check in GHC.Tc.Solver.defaultTyVarTcS, and
1163 GHC.Tc.Utils.TcMType.defaultTyVar. Here's another example (#14555):
1164 data Exp :: [TYPE rep] -> TYPE rep -> Type where
1165 Lam :: Exp (a:xs) b -> Exp xs (a -> b)
1166 We want to kind-generalise over the 'rep' variable.
1167 #14563 is another example.
1168
1169 * Duplicate type variables. Consider #11203
1170 data SameKind :: k -> k -> *
1171 data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b)
1172 Here we will unify k1 with k2, but this time doing so is an error,
1173 because k1 and k2 are bound in the same declaration.
1174
1175 We spot this during validity checking (findDupTyVarTvs),
1176 in generaliseTcTyCon.
1177
1178 * Required arguments. Even the Required arguments should be made
1179 into TyVarTvs, not skolems. Consider
1180 data T k (a :: k)
1181 Here, k is a Required, dependent variable. For uniformity, it is helpful
1182 to have k be a TyVarTv, in parallel with other dependent variables.
1183
1184 * Duplicate skolemisation is expected. When generalising in Step 3,
1185 we may find that one of the variables we want to quantify has
1186 already been skolemised. For example, suppose we have already
1187 generalise S. When we come to T we'll find that kk1 (now the same as
1188 kk3) has already been skolemised.
1189
1190 That's fine -- but it means that
1191 a) when collecting quantification candidates, in
1192 candidateQTyVarsOfKind, we must collect skolems
1193 b) quantifyTyVars should be a no-op on such a skolem
1194
1195 Note [Tricky scoping in generaliseTcTyCon]
1196 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1197 Consider #16342
1198 class C (a::ka) x where
1199 cop :: D a x => x -> Proxy a -> Proxy a
1200 cop _ x = x :: Proxy (a::ka)
1201
1202 class D (b::kb) y where
1203 dop :: C b y => y -> Proxy b -> Proxy b
1204 dop _ x = x :: Proxy (b::kb)
1205
1206 C and D are mutually recursive, by the time we get to
1207 generaliseTcTyCon we'll have unified kka := kkb.
1208
1209 But when typechecking the default declarations for 'cop' and 'dop' in
1210 tcDlassDecl2 we need {a, ka} and {b, kb} respectively to be in scope.
1211 But at that point all we have is the utterly-final Class itself.
1212
1213 Conclusion: the classTyVars of a class must have the same Name as
1214 that originally assigned by the user. In our example, C must have
1215 classTyVars {a, ka, x} while D has classTyVars {a, kb, y}. Despite
1216 the fact that kka and kkb got unified!
1217
1218 We achieve this sleight of hand in generaliseTcTyCon, using
1219 the specialised function zonkRecTyVarBndrs. We make the call
1220 zonkRecTyVarBndrs [ka,a,x] [kkb,aa,xxx]
1221 where the [ka,a,x] are the Names originally assigned by the user, and
1222 [kkb,aa,xx] are the corresponding (post-zonking, skolemised) TcTyVars.
1223 zonkRecTyVarBndrs builds a recursive ZonkEnv that binds
1224 kkb :-> (ka :: <zonked kind of kkb>)
1225 aa :-> (a :: <konked kind of aa>)
1226 etc
1227 That is, it maps each skolemised TcTyVars to the utterly-final
1228 TyVar to put in the class, with its correct user-specified name.
1229 When generalising D we'll do the same thing, but the ZonkEnv will map
1230 kkb :-> (kb :: <zonked kind of kkb>)
1231 bb :-> (b :: <konked kind of bb>)
1232 etc
1233 Note that 'kkb' again appears in the domain of the mapping, but this
1234 time mapped to 'kb'. That's how C and D end up with differently-named
1235 final TyVars despite the fact that we unified kka:=kkb
1236
1237 zonkRecTyVarBndrs we need to do knot-tying because of the need to
1238 apply this same substitution to the kind of each.
1239
1240 Note [Inferring visible dependent quantification]
1241 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1242 Consider
1243
1244 data T k :: k -> Type where
1245 MkT1 :: T Type Int
1246 MkT2 :: T (Type -> Type) Maybe
1247
1248 This looks like it should work. However, it is polymorphically recursive,
1249 as the uses of T in the constructor types specialize the k in the kind
1250 of T. This trips up our dear users (#17131, #17541), and so we add
1251 a "landmark" context (which cannot be suppressed) whenever we
1252 spot inferred visible dependent quantification (VDQ).
1253
1254 It's hard to know when we've actually been tripped up by polymorphic recursion
1255 specifically, so we just include a note to users whenever we infer VDQ. The
1256 testsuite did not show up a single spurious inclusion of this message.
1257
1258 The context is added in addVDQNote, which looks for a visible TyConBinder
1259 that also appears in the TyCon's kind. (I first looked at the kind for
1260 a visible, dependent quantifier, but Note [No polymorphic recursion] in
1261 GHC.Tc.Gen.HsType defeats that approach.) addVDQNote is used in kcTyClDecl,
1262 which is used only when inferring the kind of a tycon (never with a CUSK or
1263 SAK).
1264
1265 Once upon a time, I (Richard E) thought that the tycon-kind could
1266 not be a forall-type. But this is wrong: data T :: forall k. k -> Type
1267 (with -XNoCUSKs) could end up here. And this is all OK.
1268
1269
1270 -}
1271
1272 --------------
1273 tcExtendKindEnvWithTyCons :: [TcTyCon] -> TcM a -> TcM a
1274 tcExtendKindEnvWithTyCons tcs
1275 = tcExtendKindEnvList [ (tyConName tc, ATcTyCon tc) | tc <- tcs ]
1276
1277 --------------
1278 mkPromotionErrorEnv :: [LTyClDecl GhcRn] -> TcTypeEnv
1279 -- Maps each tycon/datacon to a suitable promotion error
1280 -- tc :-> APromotionErr TyConPE
1281 -- dc :-> APromotionErr RecDataConPE
1282 -- See Note [Recursion and promoting data constructors]
1283
1284 mkPromotionErrorEnv decls
1285 = foldr (plusNameEnv . mk_prom_err_env . unLoc)
1286 emptyNameEnv decls
1287
1288 mk_prom_err_env :: TyClDecl GhcRn -> TcTypeEnv
1289 mk_prom_err_env (ClassDecl { tcdLName = L _ nm, tcdATs = ats })
1290 = unitNameEnv nm (APromotionErr ClassPE)
1291 `plusNameEnv`
1292 mkNameEnv [ (familyDeclName at, APromotionErr TyConPE)
1293 | L _ at <- ats ]
1294
1295 mk_prom_err_env (DataDecl { tcdLName = L _ name
1296 , tcdDataDefn = HsDataDefn { dd_cons = cons } })
1297 = unitNameEnv name (APromotionErr TyConPE)
1298 `plusNameEnv`
1299 mkNameEnv [ (con, APromotionErr RecDataConPE)
1300 | L _ con' <- cons
1301 , L _ con <- getConNames con' ]
1302
1303 mk_prom_err_env decl
1304 = unitNameEnv (tcdName decl) (APromotionErr TyConPE)
1305 -- Works for family declarations too
1306
1307 --------------
1308 inferInitialKinds :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
1309 -- Returns a TcTyCon for each TyCon bound by the decls,
1310 -- each with its initial kind
1311
1312 inferInitialKinds decls
1313 = do { traceTc "inferInitialKinds {" $ ppr (map (tcdName . unLoc) decls)
1314 ; tcs <- concatMapM infer_initial_kind decls
1315 ; traceTc "inferInitialKinds done }" empty
1316 ; return tcs }
1317 where
1318 infer_initial_kind = addLocMA (getInitialKind InitialKindInfer)
1319
1320 -- Check type/class declarations against their standalone kind signatures or
1321 -- CUSKs, producing a generalized TcTyCon for each.
1322 checkInitialKinds :: [(LTyClDecl GhcRn, SAKS_or_CUSK)] -> TcM [TcTyCon]
1323 checkInitialKinds decls
1324 = do { traceTc "checkInitialKinds {" $ ppr (mapFst (tcdName . unLoc) decls)
1325 ; tcs <- concatMapM check_initial_kind decls
1326 ; traceTc "checkInitialKinds done }" empty
1327 ; return tcs }
1328 where
1329 check_initial_kind (ldecl, msig) =
1330 addLocMA (getInitialKind (InitialKindCheck msig)) ldecl
1331
1332 -- | Get the initial kind of a TyClDecl, either generalized or non-generalized,
1333 -- depending on the 'InitialKindStrategy'.
1334 getInitialKind :: InitialKindStrategy -> TyClDecl GhcRn -> TcM [TcTyCon]
1335
1336 -- Allocate a fresh kind variable for each TyCon and Class
1337 -- For each tycon, return a TcTyCon with kind k
1338 -- where k is the kind of tc, derived from the LHS
1339 -- of the definition (and probably including
1340 -- kind unification variables)
1341 -- Example: data T a b = ...
1342 -- return (T, kv1 -> kv2 -> kv3)
1343 --
1344 -- This pass deals with (ie incorporates into the kind it produces)
1345 -- * The kind signatures on type-variable binders
1346 -- * The result kinds signature on a TyClDecl
1347 --
1348 -- No family instances are passed to checkInitialKinds/inferInitialKinds
1349 getInitialKind strategy
1350 (ClassDecl { tcdLName = L _ name
1351 , tcdTyVars = ktvs
1352 , tcdATs = ats })
1353 = do { cls <- kcDeclHeader strategy name ClassFlavour ktvs $
1354 return (TheKind constraintKind)
1355 ; let parent_tv_prs = tcTyConScopedTyVars cls
1356 -- See Note [Don't process associated types in getInitialKind]
1357 ; inner_tcs <-
1358 tcExtendNameTyVarEnv parent_tv_prs $
1359 mapM (addLocMA (getAssocFamInitialKind cls)) ats
1360 ; return (cls : inner_tcs) }
1361 where
1362 getAssocFamInitialKind cls =
1363 case strategy of
1364 InitialKindInfer -> get_fam_decl_initial_kind (Just cls)
1365 InitialKindCheck _ -> check_initial_kind_assoc_fam cls
1366
1367 getInitialKind strategy
1368 (DataDecl { tcdLName = L _ name
1369 , tcdTyVars = ktvs
1370 , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
1371 , dd_ND = new_or_data } })
1372 = do { let flav = newOrDataToFlavour new_or_data
1373 ctxt = DataKindCtxt name
1374 ; tc <- kcDeclHeader strategy name flav ktvs $
1375 case m_sig of
1376 Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig
1377 Nothing -> return $ dataDeclDefaultResultKind strategy new_or_data
1378 ; return [tc] }
1379
1380 getInitialKind InitialKindInfer (FamDecl { tcdFam = decl })
1381 = do { tc <- get_fam_decl_initial_kind Nothing decl
1382 ; return [tc] }
1383
1384 getInitialKind (InitialKindCheck msig) (FamDecl { tcdFam =
1385 FamilyDecl { fdLName = unLoc -> name
1386 , fdTyVars = ktvs
1387 , fdResultSig = unLoc -> resultSig
1388 , fdInfo = info } } )
1389 = do { let flav = getFamFlav Nothing info
1390 ctxt = TyFamResKindCtxt name
1391 ; tc <- kcDeclHeader (InitialKindCheck msig) name flav ktvs $
1392 case famResultKindSignature resultSig of
1393 Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig
1394 Nothing ->
1395 case msig of
1396 CUSK -> return (TheKind liftedTypeKind)
1397 SAKS _ -> return AnyKind
1398 ; return [tc] }
1399
1400 getInitialKind strategy
1401 (SynDecl { tcdLName = L _ name
1402 , tcdTyVars = ktvs
1403 , tcdRhs = rhs })
1404 = do { let ctxt = TySynKindCtxt name
1405 ; tc <- kcDeclHeader strategy name TypeSynonymFlavour ktvs $
1406 case hsTyKindSig rhs of
1407 Just rhs_sig -> TheKind <$> tcLHsKindSig ctxt rhs_sig
1408 Nothing -> return AnyKind
1409 ; return [tc] }
1410
1411 get_fam_decl_initial_kind
1412 :: Maybe TcTyCon -- ^ Just cls <=> this is an associated family of class cls
1413 -> FamilyDecl GhcRn
1414 -> TcM TcTyCon
1415 get_fam_decl_initial_kind mb_parent_tycon
1416 FamilyDecl { fdLName = L _ name
1417 , fdTyVars = ktvs
1418 , fdResultSig = L _ resultSig
1419 , fdInfo = info }
1420 = kcDeclHeader InitialKindInfer name flav ktvs $
1421 case resultSig of
1422 KindSig _ ki -> TheKind <$> tcLHsKindSig ctxt ki
1423 TyVarSig _ (L _ (KindedTyVar _ _ _ ki)) -> TheKind <$> tcLHsKindSig ctxt ki
1424 _ -- open type families have * return kind by default
1425 | tcFlavourIsOpen flav -> return (TheKind liftedTypeKind)
1426 -- closed type families have their return kind inferred
1427 -- by default
1428 | otherwise -> return AnyKind
1429 where
1430 flav = getFamFlav mb_parent_tycon info
1431 ctxt = TyFamResKindCtxt name
1432
1433 -- See Note [Standalone kind signatures for associated types]
1434 check_initial_kind_assoc_fam
1435 :: TcTyCon -- parent class
1436 -> FamilyDecl GhcRn
1437 -> TcM TcTyCon
1438 check_initial_kind_assoc_fam cls
1439 FamilyDecl
1440 { fdLName = unLoc -> name
1441 , fdTyVars = ktvs
1442 , fdResultSig = unLoc -> resultSig
1443 , fdInfo = info }
1444 = kcDeclHeader (InitialKindCheck CUSK) name flav ktvs $
1445 case famResultKindSignature resultSig of
1446 Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig
1447 Nothing -> return (TheKind liftedTypeKind)
1448 where
1449 ctxt = TyFamResKindCtxt name
1450 flav = getFamFlav (Just cls) info
1451
1452 {- Note [Standalone kind signatures for associated types]
1453 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1454
1455 If associated types had standalone kind signatures, would they wear them
1456
1457 ---------------------------+------------------------------
1458 like this? (OUT) | or like this? (IN)
1459 ---------------------------+------------------------------
1460 type T :: Type -> Type | class C a where
1461 class C a where | type T :: Type -> Type
1462 type T a | type T a
1463
1464 The (IN) variant is syntactically ambiguous:
1465
1466 class C a where
1467 type T :: a -- standalone kind signature?
1468 type T :: a -- declaration header?
1469
1470 The (OUT) variant does not suffer from this issue, but it might not be the
1471 direction in which we want to take Haskell: we seek to unify type families and
1472 functions, and, by extension, associated types with class methods. And yet we
1473 give class methods their signatures inside the class, not outside. Neither do
1474 we have the counterpart of InstanceSigs for StandaloneKindSignatures.
1475
1476 For now, we dodge the question by using CUSKs for associated types instead of
1477 standalone kind signatures. This is a simple addition to the rule we used to
1478 have before standalone kind signatures:
1479
1480 old rule: associated type has a CUSK iff its parent class has a CUSK
1481 new rule: associated type has a CUSK iff its parent class has a CUSK or a standalone kind signature
1482
1483 -}
1484
1485 -- See Note [Data declaration default result kind]
1486 dataDeclDefaultResultKind :: InitialKindStrategy -> NewOrData -> ContextKind
1487 dataDeclDefaultResultKind strategy new_or_data
1488 | NewType <- new_or_data
1489 = OpenKind -- See Note [Implementation of UnliftedNewtypes], point <Error Messages>.
1490 | DataType <- new_or_data
1491 , InitialKindCheck (SAKS _) <- strategy
1492 = OpenKind -- See Note [Implementation of UnliftedDatatypes]
1493 | otherwise
1494 = TheKind liftedTypeKind
1495
1496 {- Note [Data declaration default result kind]
1497 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1498 When the user has not written an inline result kind annotation on a data
1499 declaration, we assume it to be 'Type'. That is, the following declarations
1500 D1 and D2 are considered equivalent:
1501
1502 data D1 where ...
1503 data D2 :: Type where ...
1504
1505 The consequence of this assumption is that we reject D3 even though we
1506 accept D4:
1507
1508 data D3 where
1509 MkD3 :: ... -> D3 param
1510
1511 data D4 :: Type -> Type where
1512 MkD4 :: ... -> D4 param
1513
1514 However, there are two twists:
1515
1516 * For unlifted newtypes, we must relax the assumed result kind to (TYPE r):
1517
1518 newtype D5 where
1519 MkD5 :: Int# -> D5
1520
1521 See Note [Implementation of UnliftedNewtypes], STEP 1 and it's sub-note
1522 <Error Messages>.
1523
1524 * For unlifted datatypes, we must relax the assumed result kind to
1525 (TYPE (BoxedRep l)) in the presence of a SAKS:
1526
1527 type D6 :: Type -> TYPE (BoxedRep Unlifted)
1528 data D6 a = MkD6 a
1529
1530 Otherwise, it would be impossible to declare unlifted data types in H98
1531 syntax (which doesn't allow specification of a result kind).
1532
1533 -}
1534
1535 ---------------------------------
1536 getFamFlav
1537 :: Maybe TcTyCon -- ^ Just cls <=> this is an associated family of class cls
1538 -> FamilyInfo pass
1539 -> TyConFlavour
1540 getFamFlav mb_parent_tycon info =
1541 case info of
1542 DataFamily -> DataFamilyFlavour mb_parent_tycon
1543 OpenTypeFamily -> OpenTypeFamilyFlavour mb_parent_tycon
1544 ClosedTypeFamily _ -> assert (isNothing mb_parent_tycon) -- See Note [Closed type family mb_parent_tycon]
1545 ClosedTypeFamilyFlavour
1546
1547 {- Note [Closed type family mb_parent_tycon]
1548 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1549 There's no way to write a closed type family inside a class declaration:
1550
1551 class C a where
1552 type family F a where -- error: parse error on input ‘where’
1553
1554 In fact, it is not clear what the meaning of such a declaration would be.
1555 Therefore, 'mb_parent_tycon' of any closed type family has to be Nothing.
1556 -}
1557
1558 ------------------------------------------------------------------------
1559 kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
1560 -- See Note [Kind checking for type and class decls]
1561 -- Called only for declarations without a signature (no CUSKs or SAKs here)
1562 kcLTyClDecl (L loc decl)
1563 = setSrcSpanA loc $
1564 do { tycon <- tcLookupTcTyCon tc_name
1565 ; traceTc "kcTyClDecl {" (ppr tc_name)
1566 ; addVDQNote tycon $ -- See Note [Inferring visible dependent quantification]
1567 addErrCtxt (tcMkDeclCtxt decl) $
1568 kcTyClDecl decl tycon
1569 ; traceTc "kcTyClDecl done }" (ppr tc_name) }
1570 where
1571 tc_name = tcdName decl
1572
1573 kcTyClDecl :: TyClDecl GhcRn -> TcTyCon -> TcM ()
1574 -- This function is used solely for its side effect on kind variables
1575 -- NB kind signatures on the type variables and
1576 -- result kind signature have already been dealt with
1577 -- by inferInitialKind, so we can ignore them here.
1578
1579 kcTyClDecl (DataDecl { tcdLName = (L _ name), tcdDataDefn = defn }) tycon
1580 | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons, dd_ND = new_or_data } <- defn
1581 = bindTyClTyVars name $ \ _ _ _ ->
1582 -- NB: binding these tyvars isn't necessary for GADTs, but it does no
1583 -- harm. For GADTs, each data con brings its own tyvars into scope,
1584 -- and the ones from this bindTyClTyVars are either not mentioned or
1585 -- (conceivably) shadowed.
1586 do { traceTc "kcTyClDecl" (ppr tycon $$ ppr (tyConTyVars tycon) $$ ppr (tyConResKind tycon))
1587 ; _ <- tcHsContext ctxt
1588 ; kcConDecls new_or_data (tyConResKind tycon) cons
1589 }
1590
1591 kcTyClDecl (SynDecl { tcdLName = L _ name, tcdRhs = rhs }) _tycon
1592 = bindTyClTyVars name $ \ _ _ res_kind ->
1593 discardResult $ tcCheckLHsType rhs (TheKind res_kind)
1594 -- NB: check against the result kind that we allocated
1595 -- in inferInitialKinds.
1596
1597 kcTyClDecl (ClassDecl { tcdLName = L _ name
1598 , tcdCtxt = ctxt, tcdSigs = sigs }) _tycon
1599 = bindTyClTyVars name $ \ _ _ _ ->
1600 do { _ <- tcHsContext ctxt
1601 ; mapM_ (wrapLocMA_ kc_sig) sigs }
1602 where
1603 kc_sig (ClassOpSig _ _ nms op_ty) = kcClassSigType nms op_ty
1604 kc_sig _ = return ()
1605
1606 kcTyClDecl (FamDecl _ (FamilyDecl { fdInfo = fd_info })) fam_tc
1607 -- closed type families look at their equations, but other families don't
1608 -- do anything here
1609 = case fd_info of
1610 ClosedTypeFamily (Just eqns) -> mapM_ (kcTyFamInstEqn fam_tc) eqns
1611 _ -> return ()
1612
1613 -------------------
1614
1615 -- Kind-check the types of the arguments to a data constructor.
1616 -- This includes doing kind unification if the type is a newtype.
1617 -- See Note [Implementation of UnliftedNewtypes] for why we need
1618 -- the first two arguments.
1619 kcConArgTys :: NewOrData -> Kind -> [HsScaled GhcRn (LHsType GhcRn)] -> TcM ()
1620 kcConArgTys new_or_data res_kind arg_tys = do
1621 { let exp_kind = getArgExpKind new_or_data res_kind
1622 ; forM_ arg_tys (\(HsScaled mult ty) -> do _ <- tcCheckLHsType (getBangType ty) exp_kind
1623 tcMult mult)
1624 -- See Note [Implementation of UnliftedNewtypes], STEP 2
1625 }
1626
1627 -- Kind-check the types of arguments to a Haskell98 data constructor.
1628 kcConH98Args :: NewOrData -> Kind -> HsConDeclH98Details GhcRn -> TcM ()
1629 kcConH98Args new_or_data res_kind con_args = case con_args of
1630 PrefixCon _ tys -> kcConArgTys new_or_data res_kind tys
1631 InfixCon ty1 ty2 -> kcConArgTys new_or_data res_kind [ty1, ty2]
1632 RecCon (L _ flds) -> kcConArgTys new_or_data res_kind $
1633 map (hsLinear . cd_fld_type . unLoc) flds
1634
1635 -- Kind-check the types of arguments to a GADT data constructor.
1636 kcConGADTArgs :: NewOrData -> Kind -> HsConDeclGADTDetails GhcRn -> TcM ()
1637 kcConGADTArgs new_or_data res_kind con_args = case con_args of
1638 PrefixConGADT tys -> kcConArgTys new_or_data res_kind tys
1639 RecConGADT (L _ flds) _ -> kcConArgTys new_or_data res_kind $
1640 map (hsLinear . cd_fld_type . unLoc) flds
1641
1642 kcConDecls :: NewOrData
1643 -> Kind -- The result kind signature
1644 -- Used only in H98 case
1645 -> [LConDecl GhcRn] -- The data constructors
1646 -> TcM ()
1647 -- See Note [kcConDecls: kind-checking data type decls]
1648 kcConDecls new_or_data tc_res_kind cons
1649 = mapM_ (wrapLocMA_ (kcConDecl new_or_data tc_res_kind)) cons
1650
1651 -- Kind check a data constructor. In additional to the data constructor,
1652 -- we also need to know about whether or not its corresponding type was
1653 -- declared with data or newtype, and we need to know the result kind of
1654 -- this type. See Note [Implementation of UnliftedNewtypes] for why
1655 -- we need the first two arguments.
1656 kcConDecl :: NewOrData
1657 -> Kind -- Result kind of the type constructor
1658 -- Usually Type but can be TYPE UnliftedRep
1659 -- or even TYPE r, in the case of unlifted newtype
1660 -- Used only in H98 case
1661 -> ConDecl GhcRn
1662 -> TcM ()
1663 kcConDecl new_or_data tc_res_kind (ConDeclH98
1664 { con_name = name, con_ex_tvs = ex_tvs
1665 , con_mb_cxt = ex_ctxt, con_args = args })
1666 = addErrCtxt (dataConCtxt [name]) $
1667 discardResult $
1668 bindExplicitTKBndrs_Tv ex_tvs $
1669 do { _ <- tcHsContext ex_ctxt
1670 ; kcConH98Args new_or_data tc_res_kind args
1671 -- We don't need to check the telescope here,
1672 -- because that's done in tcConDecl
1673 }
1674
1675 kcConDecl new_or_data
1676 _tc_res_kind -- Not used in GADT case (and doesn't make sense)
1677 (ConDeclGADT
1678 { con_names = names, con_bndrs = L _ outer_bndrs, con_mb_cxt = cxt
1679 , con_g_args = args, con_res_ty = res_ty })
1680 = -- See Note [kcConDecls: kind-checking data type decls]
1681 addErrCtxt (dataConCtxt names) $
1682 discardResult $
1683 bindOuterSigTKBndrs_Tv outer_bndrs $
1684 -- Why "_Tv"? See Note [Using TyVarTvs for kind-checking GADTs]
1685 do { _ <- tcHsContext cxt
1686 ; traceTc "kcConDecl:GADT {" (ppr names $$ ppr res_ty)
1687 ; con_res_kind <- newOpenTypeKind
1688 ; _ <- tcCheckLHsType res_ty (TheKind con_res_kind)
1689 ; kcConGADTArgs new_or_data con_res_kind args
1690 ; traceTc "kcConDecl:GADT }" (ppr names $$ ppr con_res_kind)
1691 ; return () }
1692
1693 {- Note [kcConDecls: kind-checking data type decls]
1694 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1695 kcConDecls is used when we are inferring the kind of the type
1696 constructor in a data type declaration. E.g.
1697 data T f a = MkT (f a)
1698 we want to infer the kind of 'f' and 'a'. The basic plan is described
1699 in Note [Inferring kinds for type declarations]; here we are doing Step 2.
1700
1701 In the GADT case we may have this:
1702 data T f a where
1703 MkT :: forall g b. g b -> T g b
1704
1705 Notice that the variables f,a, and g,b are quite distinct.
1706 Nevertheless, the type signature for MkT must still influence the kind
1707 T which is (remember Step 1) something like
1708 T :: kappa1 -> kappa2 -> Type
1709 Otherwise we'd infer the bogus kind
1710 T :: forall k1 k2. k1 -> k2 -> Type.
1711
1712 The type signature for MkT influences the kind of T simply by
1713 kind-checking the result type (T g b), which will force 'f' and 'g' to
1714 have the same kinds. This is the call to
1715 tcCheckLHsType res_ty (TheKind con_res_kind)
1716 Because this is the result type of an arrow, we know the kind must be
1717 of form (TYPE rr), and we get better error messages if we enforce that
1718 here (e.g. test gadt10).
1719
1720 For unlifted newtypes only, we must ensure that the argument kind
1721 and result kind are the same:
1722 * In the H98 case, we need the result kind of the TyCon, to unify with
1723 the argument kind.
1724
1725 * In GADT syntax, this unification happens via the result kind passed
1726 to kcConGADTArgs. The tycon's result kind is not used at all in the
1727 GADT case.
1728
1729 Note [Using TyVarTvs for kind-checking GADTs]
1730 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1731 Consider
1732
1733 data Proxy a where
1734 MkProxy1 :: forall k (b :: k). Proxy b
1735 MkProxy2 :: forall j (c :: j). Proxy c
1736
1737 It seems reasonable that this should be accepted. But something very strange
1738 is going on here: when we're kind-checking this declaration, we need to unify
1739 the kind of `a` with k and j -- even though k and j's scopes are local to the type of
1740 MkProxy{1,2}.
1741
1742 In effect, we are simply gathering constraints on the shape of Proxy's
1743 kind, with no skolemisation or implication constraints involved at all.
1744
1745 The best approach we've come up with is to use TyVarTvs during the
1746 kind-checking pass, rather than ordinary skolems. This is why we use
1747 the "_Tv" variant, bindOuterSigTKBndrs_Tv.
1748
1749 Our only goal is to gather constraints on the kind of the type constructor;
1750 we do not certify that the data declaration is well-kinded. For example:
1751
1752 data SameKind :: k -> k -> Type
1753 data Bad a where
1754 MkBad :: forall k1 k2 (a :: k1) (b :: k2). Bad (SameKind a b)
1755
1756 which would be accepted by kcConDecl because k1 and k2 are
1757 TyVarTvs. It is correctly rejected in the second pass, tcConDecl.
1758 (Test case: polykinds/TyVarTvKinds3)
1759
1760 One drawback of this approach is sometimes it will accept a definition that
1761 a (hypothetical) declarative specification would likely reject. As a general
1762 rule, we don't want to allow polymorphic recursion without a CUSK. Indeed,
1763 the whole point of CUSKs is to allow polymorphic recursion. Yet, the TyVarTvs
1764 approach allows a limited form of polymorphic recursion *without* a CUSK.
1765
1766 To wit:
1767 data T a = forall k (b :: k). MkT (T b) Int
1768 (test case: dependent/should_compile/T14066a)
1769
1770 Note that this is polymorphically recursive, with the recursive occurrence
1771 of T used at a kind other than a's kind. The approach outlined here accepts
1772 this definition, because this kind is still a kind variable (and so the
1773 TyVarTvs unify). Stepping back, I (Richard) have a hard time envisioning a
1774 way to describe exactly what declarations will be accepted and which will
1775 be rejected (without a CUSK). However, the accepted definitions are indeed
1776 well-kinded and any rejected definitions would be accepted with a CUSK,
1777 and so this wrinkle need not cause anyone to lose sleep.
1778
1779 Note [Recursion and promoting data constructors]
1780 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1781 We don't want to allow promotion in a strongly connected component
1782 when kind checking.
1783
1784 Consider:
1785 data T f = K (f (K Any))
1786
1787 When kind checking the `data T' declaration the local env contains the
1788 mappings:
1789 T -> ATcTyCon <some initial kind>
1790 K -> APromotionErr
1791
1792 APromotionErr is only used for DataCons, and only used during type checking
1793 in tcTyClGroup.
1794
1795
1796 ************************************************************************
1797 * *
1798 \subsection{Type checking}
1799 * *
1800 ************************************************************************
1801
1802 Note [Type checking recursive type and class declarations]
1803 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1804 At this point we have completed *kind-checking* of a mutually
1805 recursive group of type/class decls (done in kcTyClGroup). However,
1806 we discarded the kind-checked types (eg RHSs of data type decls);
1807 note that kcTyClDecl returns (). There are two reasons:
1808
1809 * It's convenient, because we don't have to rebuild a
1810 kinded HsDecl (a fairly elaborate type)
1811
1812 * It's necessary, because after kind-generalisation, the
1813 TyCons/Classes may now be kind-polymorphic, and hence need
1814 to be given kind arguments.
1815
1816 Example:
1817 data T f a = MkT (f a) (T f a)
1818 During kind-checking, we give T the kind T :: k1 -> k2 -> *
1819 and figure out constraints on k1, k2 etc. Then we generalise
1820 to get T :: forall k. (k->*) -> k -> *
1821 So now the (T f a) in the RHS must be elaborated to (T k f a).
1822
1823 However, during tcTyClDecl of T (above) we will be in a recursive
1824 "knot". So we aren't allowed to look at the TyCon T itself; we are only
1825 allowed to put it (lazily) in the returned structures. But when
1826 kind-checking the RHS of T's decl, we *do* need to know T's kind (so
1827 that we can correctly elaboarate (T k f a). How can we get T's kind
1828 without looking at T? Delicate answer: during tcTyClDecl, we extend
1829
1830 *Global* env with T -> ATyCon (the (not yet built) final TyCon for T)
1831 *Local* env with T -> ATcTyCon (TcTyCon with the polymorphic kind of T)
1832
1833 Then:
1834
1835 * During GHC.Tc.Gen.HsType.tcTyVar we look in the *local* env, to get the
1836 fully-known, not knot-tied TcTyCon for T.
1837
1838 * Then, in GHC.Tc.Utils.Zonk.zonkTcTypeToType (and zonkTcTyCon in particular)
1839 we look in the *global* env to get the TyCon.
1840
1841 This fancy footwork (with two bindings for T) is only necessary for the
1842 TyCons or Classes of this recursive group. Earlier, finished groups,
1843 live in the global env only.
1844
1845 See also Note [Kind checking recursive type and class declarations]
1846
1847 Note [Kind checking recursive type and class declarations]
1848 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1849 Before we can type-check the decls, we must kind check them. This
1850 is done by establishing an "initial kind", which is a rather uninformed
1851 guess at a tycon's kind (by counting arguments, mainly) and then
1852 using this initial kind for recursive occurrences.
1853
1854 The initial kind is stored in exactly the same way during
1855 kind-checking as it is during type-checking (Note [Type checking
1856 recursive type and class declarations]): in the *local* environment,
1857 with ATcTyCon. But we still must store *something* in the *global*
1858 environment. Even though we discard the result of kind-checking, we
1859 sometimes need to produce error messages. These error messages will
1860 want to refer to the tycons being checked, except that they don't
1861 exist yet, and it would be Terribly Annoying to get the error messages
1862 to refer back to HsSyn. So we create a TcTyCon and put it in the
1863 global env. This tycon can print out its name and knows its kind, but
1864 any other action taken on it will panic. Note that TcTyCons are *not*
1865 knot-tied, unlike the rather valid but knot-tied ones that occur
1866 during type-checking.
1867
1868 Note [Declarations for wired-in things]
1869 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1870 For wired-in things we simply ignore the declaration
1871 and take the wired-in information. That avoids complications.
1872 e.g. the need to make the data constructor worker name for
1873 a constraint tuple match the wired-in one
1874
1875 Note [Datatype return kinds]
1876 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1877 There are several poorly lit corners around datatype/newtype return kinds.
1878 This Note explains these. We cover data/newtype families and instances
1879 in Note [Data family/instance return kinds].
1880
1881 data T a :: <kind> where ... -- See Point DT4
1882 newtype T a :: <kind> where ... -- See Point DT5
1883
1884 DT1 Where this applies: Only GADT syntax for data/newtype/instance declarations
1885 can have declared return kinds. This Note does not apply to Haskell98
1886 syntax.
1887
1888 DT2 Where these kinds come from: The return kind is part of the TyCon kind, gotten either
1889 by checkInitialKind (standalone kind signature / CUSK) or
1890 inferInitialKind. It is extracted by bindTyClTyVars in tcTyClDecl1. It is
1891 then passed to tcDataDefn.
1892
1893 DT3 Eta-expansion: Any forall-bound variables and function arguments in a result kind
1894 become parameters to the type. That is, when we say
1895
1896 data T a :: Type -> Type where ...
1897
1898 we really mean for T to have two parameters. The second parameter
1899 is produced by processing the return kind in etaExpandAlgTyCon,
1900 called in tcDataDefn.
1901
1902 See also Note [TyConBinders for the result kind signatures of a data type]
1903 in GHC.Tc.Gen.HsType.
1904
1905 DT4 Datatype return kind restriction: A data type return kind must end
1906 in a type that, after type-synonym expansion, yields `TYPE LiftedRep`. By
1907 "end in", we mean we strip any foralls and function arguments off before
1908 checking.
1909
1910 Examples:
1911 data T1 :: Type -- good
1912 data T2 :: Bool -> Type -- good
1913 data T3 :: Bool -> forall k. Type -- strange, but still accepted
1914 data T4 :: forall k. k -> Type -- good
1915 data T5 :: Bool -- bad
1916 data T6 :: Type -> Bool -- bad
1917
1918 Exactly the same applies to data instance (but not data family)
1919 declarations. Examples
1920 data instance D1 :: Type -- good
1921 data instance D2 :: Bool -> Type -- good
1922
1923 We can "look through" type synonyms
1924 type Star = Type
1925 data T7 :: Bool -> Star -- good (synonym expansion ok)
1926 type Arrow = (->)
1927 data T8 :: Arrow Bool Type -- good (ditto)
1928
1929 But we specifically do *not* do type family reduction here.
1930 type family ARROW where
1931 ARROW = (->)
1932 data T9 :: ARROW Bool Type -- bad
1933
1934 type family F a where
1935 F Int = Bool
1936 F Bool = Type
1937 data T10 :: Bool -> F Bool -- bad
1938
1939 The /principle/ here is that in the TyCon for a data type or data instance,
1940 we must be able to lay out all the type-variable binders, one by one, until
1941 we reach (TYPE xx). There is no place for a cast here. We could add one,
1942 but let's not!
1943
1944 This check is done in checkDataKindSig. For data declarations, this
1945 call is in tcDataDefn; for data instances, this call is in tcDataFamInstDecl.
1946
1947 DT5 Newtype return kind restriction.
1948 If -XUnliftedNewtypes is not on, then newtypes are treated just
1949 like datatypes --- see (4) above.
1950
1951 If -XUnliftedNewtypes is on, then a newtype return kind must end in
1952 TYPE xyz, for some xyz (after type synonym expansion). The "xyz"
1953 may include type families, but the TYPE part must be visible
1954 /without/ expanding type families (only synonyms).
1955
1956 This kind is unified with the kind of the representation type (the
1957 type of the one argument to the one constructor). See also steps
1958 (2) and (3) of Note [Implementation of UnliftedNewtypes].
1959
1960 The checks are done in the same places as for datatypes.
1961 Examples (assume -XUnliftedNewtypes):
1962
1963 newtype N1 :: Type -- good
1964 newtype N2 :: Bool -> Type -- good
1965 newtype N3 :: forall r. Bool -> TYPE r -- good
1966
1967 type family F (t :: Type) :: RuntimeRep
1968 newtype N4 :: forall t -> TYPE (F t) -- good
1969
1970 type family STAR where
1971 STAR = Type
1972 newtype N5 :: Bool -> STAR -- bad
1973
1974 Note [Data family/instance return kinds]
1975 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1976 Within this note, understand "instance" to mean data or newtype
1977 instance, and understand "family" to mean data family. No type
1978 families or classes here. Some examples:
1979
1980 data family T a :: <kind> -- See Point DF56
1981
1982 data instance T [a] :: <kind> where ... -- See Point DF2
1983 newtype instance T [a] :: <kind> where ... -- See Point DF2
1984
1985 Here is the Plan for Data Families:
1986
1987 DF0 Where these kinds come from:
1988
1989 Families: The return kind is either written in a standalone signature
1990 or extracted from a family declaration in getInitialKind.
1991 If a family declaration is missing a result kind, it is assumed to be
1992 Type. This assumption is in getInitialKind for CUSKs or
1993 get_fam_decl_initial_kind for non-signature & non-CUSK cases.
1994
1995 Instances: The data family already has a known kind. The return kind
1996 of an instance is then calculated by applying the data family tycon
1997 to the patterns provided, as computed by the typeKind lhs_ty in the
1998 end of tcDataFamInstHeader. In the case of an instance written in GADT
1999 syntax, there are potentially *two* return kinds: the one computed from
2000 applying the data family tycon to the patterns, and the one given by
2001 the user. This second kind is checked by the tc_kind_sig function within
2002 tcDataFamInstHeader. See also DF3, below.
2003
2004 DF1 In a data/newtype instance, we treat the kind of the /data family/,
2005 once instantiated, as the "master kind" for the representation
2006 TyCon. For example:
2007 data family T1 :: Type -> Type -> Type
2008 data instance T1 Int :: F Bool -> Type where ...
2009 The "master kind" for the representation TyCon R:T1Int comes
2010 from T1, not from the signature on the data instance. It is as
2011 if we declared
2012 data R:T1Int :: Type -> Type where ...
2013 See Note [Liberalising data family return kinds] for an alternative
2014 plan. But this current plan is simple, and ensures that all instances
2015 are simple instantiations of the master, without strange casts.
2016
2017 An example with non-trivial instantiation:
2018 data family T2 :: forall k. Type -> k
2019 data instance T2 :: Type -> Type -> Type where ...
2020 Here 'k' gets instantiated with (Type -> Type), driven by
2021 the signature on the 'data instance'. (See also DT3 of
2022 Note [Datatype return kinds] about eta-expansion, which applies here,
2023 too; see tcDataFamInstDecl's call of etaExpandAlgTyCon.)
2024
2025 A newtype example:
2026
2027 data Color = Red | Blue
2028 type family Interpret (x :: Color) :: RuntimeRep where
2029 Interpret 'Red = 'IntRep
2030 Interpret 'Blue = 'WordRep
2031 data family Foo (x :: Color) :: TYPE (Interpret x)
2032 newtype instance Foo 'Red :: TYPE IntRep where
2033 FooRedC :: Int# -> Foo 'Red
2034
2035 Here we get that Foo 'Red :: TYPE (Interpret Red), and our
2036 representation newtype looks like
2037 newtype R:FooRed :: TYPE (Interpret Red) where
2038 FooRedC :: Int# -> R:FooRed
2039 Remember: the master kind comes from the /family/ tycon.
2040
2041 DF2 /After/ this instantiation, the return kind of the master kind
2042 must obey the usual rules for data/newtype return kinds (DT4, DT5)
2043 of Note [Datatype return kinds]. Examples:
2044 data family T3 k :: k
2045 data instance T3 Type where ... -- OK
2046 data instance T3 (Type->Type) where ... -- OK
2047 data instance T3 (F Int) where ... -- Not OK
2048
2049 DF3 Any kind signatures on the data/newtype instance are checked for
2050 equality with the master kind (and hence may guide instantiation)
2051 but are otherwise ignored. So in the T1 example above, we check
2052 that (F Int ~ Type) by unification; but otherwise ignore the
2053 user-supplied signature from the /family/ not the /instance/.
2054
2055 We must be sure to instantiate any trailing invisible binders
2056 before doing this unification. See the call to tcInstInvisibleBinders
2057 in tcDataFamInstHeader. For example:
2058 data family D :: forall k. k
2059 data instance D :: Type -- forall k. k <: Type
2060 data instance D :: Type -> Type -- forall k. k <: Type -> Type
2061 -- NB: these do not overlap
2062 we must instantiate D before unifying with the signature in the
2063 data instance declaration
2064
2065 DF4 We also (redundantly) check that any user-specified return kind
2066 signature in the data instance also obeys DT4/DT5. For example we
2067 reject
2068 data family T1 :: Type -> Type -> Type
2069 data instance T1 Int :: Type -> F Int
2070 even if (F Int ~ Type). We could omit this check, because we
2071 use the master kind; but it seems more uniform to check it, again
2072 with checkDataKindSig.
2073
2074 DF5 Data /family/ return kind restrictions. Consider
2075 data family D8 a :: F a
2076 where F is a type family. No data/newtype instance can instantiate
2077 this so that it obeys the rules of DT4 or DT5. So GHC proactively
2078 rejects the data /family/ declaration if it can never satisfy (DT4)/(DT5).
2079 Remember that a data family supports both data and newtype instances.
2080
2081 More precisely, the return kind of a data family must be either
2082 * TYPE xyz (for some type xyz) or
2083 * a kind variable
2084 Only in these cases can a data/newtype instance possibly satisfy (DT4)/(DT5).
2085 This is checked by the call to checkDataKindSig in tcFamDecl1. Examples:
2086
2087 data family D1 :: Type -- good
2088 data family D2 :: Bool -> Type -- good
2089 data family D3 k :: k -- good
2090 data family D4 :: forall k -> k -- good
2091 data family D5 :: forall k. k -> k -- good
2092 data family D6 :: forall r. TYPE r -- good
2093 data family D7 :: Bool -> STAR -- bad (see STAR from point 5)
2094
2095 DF6 Two return kinds for instances: If an instance has two return kinds,
2096 one from the family declaration and one from the instance declaration
2097 (see point DF3 above), they are unified. More accurately, we make sure
2098 that the kind of the applied data family is a subkind of the user-written
2099 kind. GHC.Tc.Gen.HsType.checkExpectedKind normally does this check for types, but
2100 that's overkill for our needs here. Instead, we just instantiate any
2101 invisible binders in the (instantiated) kind of the data family
2102 (called lhs_kind in tcDataFamInstHeader) with tcInstInvisibleTyBinders
2103 and then unify the resulting kind with the kind written by the user.
2104 This unification naturally produces a coercion, which we can drop, as
2105 the kind annotation on the instance is redundant (except perhaps for
2106 effects of unification).
2107
2108 This all is Wrinkle (3) in Note [Implementation of UnliftedNewtypes].
2109
2110 Note [Liberalising data family return kinds]
2111 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2112 Could we allow this?
2113 type family F a where { F Int = Type }
2114 data family T a :: F a
2115 data instance T Int where
2116 MkT :: T Int
2117
2118 In the 'data instance', T Int :: F Int, and F Int = Type, so all seems
2119 well. But there are lots of complications:
2120
2121 * The representation constructor R:TInt presumably has kind Type.
2122 So the axiom connecting the two would have to look like
2123 axTInt :: T Int ~ R:TInt |> sym axFInt
2124 and that doesn't match expectation in DataFamInstTyCon
2125 in AlgTyConFlav
2126
2127 * The wrapper can't have type
2128 $WMkT :: Int -> T Int
2129 because T Int has the wrong kind. It would have to be
2130 $WMkT :: Int -> (T Int) |> axFInt
2131
2132 * The code for $WMkT would also be more complicated, needing
2133 two coherence coercions. Try it!
2134
2135 * Code for pattern matching would be complicated in an
2136 exactly dual way.
2137
2138 So yes, we could allow this, but we currently do not. That's
2139 why we have DF2 in Note [Data family/instance return kinds].
2140
2141 Note [Implementation of UnliftedNewtypes]
2142 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2143 Expected behavior of UnliftedNewtypes:
2144
2145 * Proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0013-unlifted-newtypes.rst
2146 * Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/98
2147
2148 What follows is a high-level overview of the implementation of the
2149 proposal.
2150
2151 STEP 1: Getting the initial kind, as done by inferInitialKind. We have
2152 two sub-cases:
2153
2154 * With a SAK/CUSK: no change in kind-checking; the tycon is given the kind
2155 the user writes, whatever it may be.
2156
2157 * Without a SAK/CUSK: If there is no kind signature, the tycon is given
2158 a kind `TYPE r`, for a fresh unification variable `r`. We do this even
2159 when -XUnliftedNewtypes is not on; see <Error Messages>, below.
2160
2161 STEP 2: Kind-checking, as done by kcTyClDecl. This step is skipped for CUSKs.
2162 The key function here is kcConDecl, which looks at an individual constructor
2163 declaration. When we are processing a newtype (but whether or not -XUnliftedNewtypes
2164 is enabled; see <Error Messages>, below), we generate a correct ContextKind
2165 for the checking argument types: see getArgExpKind.
2166
2167 Examples of newtypes affected by STEP 2, assuming -XUnliftedNewtypes is
2168 enabled (we use r0 to denote a unification variable):
2169
2170 newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
2171 + kcConDecl unifies (TYPE r0) with (TYPE rep), where (TYPE r0)
2172 is the kind that inferInitialKind invented for (Foo rep).
2173
2174 data Color = Red | Blue
2175 type family Interpret (x :: Color) :: RuntimeRep where
2176 Interpret 'Red = 'IntRep
2177 Interpret 'Blue = 'WordRep
2178 data family Foo (x :: Color) :: TYPE (Interpret x)
2179 newtype instance Foo 'Red = FooRedC Int#
2180 + kcConDecl unifies TYPE (Interpret 'Red) with TYPE 'IntRep
2181
2182 Note that, in the GADT case, we might have a kind signature with arrows
2183 (newtype XYZ a b :: Type -> Type where ...). We want only the final
2184 component of the kind for checking in kcConDecl, so we call etaExpandAlgTyCon
2185 in kcTyClDecl.
2186
2187 STEP 3: Type-checking (desugaring), as done by tcTyClDecl. The key function
2188 here is tcConDecl. Once again, we must use getArgExpKind to ensure that the
2189 representation type's kind matches that of the newtype, for two reasons:
2190
2191 A. It is possible that a GADT has a CUSK. (Note that this is *not*
2192 possible for H98 types.) Recall that CUSK types don't go through
2193 kcTyClDecl, so we might not have done this kind check.
2194 B. We need to produce the coercion to put on the argument type
2195 if the kinds are different (for both H98 and GADT).
2196
2197 Example of (B):
2198
2199 type family F a where
2200 F Int = LiftedRep
2201
2202 newtype N :: TYPE (F Int) where
2203 MkN :: Int -> N
2204
2205 We really need to have the argument to MkN be (Int |> TYPE (sym axF)), where
2206 axF :: F Int ~ LiftedRep. That way, the argument kind is the same as the
2207 newtype kind, which is the principal correctness condition for newtypes.
2208
2209 Wrinkle: Consider (#17021, typecheck/should_fail/T17021)
2210
2211 type family Id (x :: a) :: a where
2212 Id x = x
2213
2214 newtype T :: TYPE (Id LiftedRep) where
2215 MkT :: Int -> T
2216
2217 In the type of MkT, we must end with (Int |> TYPE (sym axId)) -> T,
2218 never Int -> (T |> TYPE axId); otherwise, the result type of the
2219 constructor wouldn't match the datatype. However, type-checking the
2220 HsType T might reasonably result in (T |> hole). We thus must ensure
2221 that this cast is dropped, forcing the type-checker to add one to
2222 the Int instead.
2223
2224 Why is it always safe to drop the cast? This result type is type-checked by
2225 tcHsOpenType, so its kind definitely looks like TYPE r, for some r. It is
2226 important that even after dropping the cast, the type's kind has the form
2227 TYPE r. This is guaranteed by restrictions on the kinds of datatypes.
2228 For example, a declaration like `newtype T :: Id Type` is rejected: a
2229 newtype's final kind always has the form TYPE r, just as we want.
2230
2231 Note that this is possible in the H98 case only for a data family, because
2232 the H98 syntax doesn't permit a kind signature on the newtype itself.
2233
2234 There are also some changes for dealing with families:
2235
2236 1. In tcFamDecl1, we suppress a tcIsLiftedTypeKind check if
2237 UnliftedNewtypes is on. This allows us to write things like:
2238 data family Foo :: TYPE 'IntRep
2239
2240 2. In a newtype instance (with -XUnliftedNewtypes), if the user does
2241 not write a kind signature, we want to allow the possibility that
2242 the kind is not Type, so we use newOpenTypeKind instead of liftedTypeKind.
2243 This is done in tcDataFamInstHeader in GHC.Tc.TyCl.Instance. Example:
2244
2245 data family Bar (a :: RuntimeRep) :: TYPE a
2246 newtype instance Bar 'IntRep = BarIntC Int#
2247 newtype instance Bar 'WordRep :: TYPE 'WordRep where
2248 BarWordC :: Word# -> Bar 'WordRep
2249
2250 The data instance corresponding to IntRep does not specify a kind signature,
2251 so tc_kind_sig just returns `TYPE r0` (where `r0` is a fresh metavariable).
2252 The data instance corresponding to WordRep does have a kind signature, so
2253 we use that kind signature.
2254
2255 3. A data family and its newtype instance may be declared with slightly
2256 different kinds. See point DF6 in Note [Data family/instance return kinds]
2257
2258 There's also a change in the renamer:
2259
2260 * In GHC.RenameSource.rnTyClDecl, enabling UnliftedNewtypes changes what is means
2261 for a newtype to have a CUSK. This is necessary since UnliftedNewtypes
2262 means that, for newtypes without kind signatures, we must use the field
2263 inside the data constructor to determine the result kind.
2264 See Note [Unlifted Newtypes and CUSKs] for more detail.
2265
2266 For completeness, it was also necessary to make coerce work on
2267 unlifted types, resolving #13595.
2268
2269 <Error Messages>: It's tempting to think that the expected kind for a newtype
2270 constructor argument when -XUnliftedNewtypes is *not* enabled should just be Type.
2271 But this leads to difficulty in suggesting to enable UnliftedNewtypes. Here is
2272 an example:
2273
2274 newtype A = MkA Int#
2275
2276 If we expect the argument to MkA to have kind Type, then we get a kind-mismatch
2277 error. The problem is that there is no way to connect this mismatch error to
2278 -XUnliftedNewtypes, and suggest enabling the extension. So, instead, we allow
2279 the A to type-check, but then find the problem when doing validity checking (and
2280 where we get make a suitable error message). One potential worry is
2281
2282 {-# LANGUAGE PolyKinds #-}
2283 newtype B a = MkB a
2284
2285 This turns out OK, because unconstrained RuntimeReps default to LiftedRep, just
2286 as we would like. Another potential problem comes in a case like
2287
2288 -- no UnliftedNewtypes
2289
2290 data family D :: k
2291 newtype instance D = MkD Any
2292
2293 Here, we want inference to tell us that k should be instantiated to Type in
2294 the instance. With the approach described here (checking for Type only in
2295 the validity checker), that will not happen. But I cannot think of a non-contrived
2296 example that will notice this lack of inference, so it seems better to improve
2297 error messages than be able to infer this instantiation.
2298
2299 Note [Implementation of UnliftedDatatypes]
2300 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2301 Expected behavior of UnliftedDatatypes:
2302
2303 * Proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0265-unlifted-datatypes.rst
2304 * Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/265
2305
2306 The implementation heavily leans on Note [Implementation of UnliftedNewtypes].
2307
2308 In the frontend, the following tweaks have been made in the typechecker:
2309
2310 * STEP 1: In the inferInitialKinds phase, newExpectedKind gives data type
2311 constructors a result kind of `TYPE r` with a fresh unification variable
2312 `r :: RuntimeRep` when there is a SAKS. (Same as for UnliftedNewtypes.)
2313 Not needed with a CUSK, because it can't specify result kinds.
2314 If there's a GADTSyntax result kind signature, we keep on using that kind.
2315
2316 Similarly, for data instances without a kind signature, we use
2317 `TYPE r` as the result kind, to support the following code:
2318
2319 data family F a :: UnliftedType
2320 data instance F Int = TInt
2321
2322 The ommission of a kind signature for `F` should not mean a result kind
2323 of `Type` (and thus a kind error) here.
2324
2325 * STEP 2: No change to kcTyClDecl.
2326
2327 * STEP 3: In GHC.Tc.Gen.HsType.checkDataKindSig, we make sure that the result
2328 kind of the data declaration is actually `Type` or `TYPE (BoxedRep l)`,
2329 for some `l`. If UnliftedDatatypes is not activated, we emit an error with a
2330 suggestion in the latter case.
2331
2332 Why not start out with `TYPE (BoxedRep l)` in the first place? Because then
2333 we get worse kind error messages in e.g. saks_fail010:
2334
2335 - Couldn't match expected kind: TYPE ('GHC.Types.BoxedRep t0)
2336 - with actual kind: * -> *
2337 + Expected a type, but found something with kind ‘* -> *’
2338 In the data type declaration for ‘T’
2339
2340 It seems `TYPE r` already has appropriate pretty-printing support.
2341
2342 The changes to Core, STG and Cmm are of rather cosmetic nature.
2343 The IRs are already well-equipped to handle unlifted types, and unlifted
2344 datatypes are just a new sub-class thereof.
2345 -}
2346
2347 tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM (TyCon, [DerivInfo])
2348 tcTyClDecl roles_info (L loc decl)
2349 | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
2350 = case thing of -- See Note [Declarations for wired-in things]
2351 ATyCon tc -> return (tc, wiredInDerivInfo tc decl)
2352 _ -> pprPanic "tcTyClDecl" (ppr thing)
2353
2354 | otherwise
2355 = setSrcSpanA loc $ tcAddDeclCtxt decl $
2356 do { traceTc "---- tcTyClDecl ---- {" (ppr decl)
2357 ; (tc, deriv_infos) <- tcTyClDecl1 Nothing roles_info decl
2358 ; traceTc "---- tcTyClDecl end ---- }" (ppr tc)
2359 ; return (tc, deriv_infos) }
2360
2361 noDerivInfos :: a -> (a, [DerivInfo])
2362 noDerivInfos a = (a, [])
2363
2364 wiredInDerivInfo :: TyCon -> TyClDecl GhcRn -> [DerivInfo]
2365 wiredInDerivInfo tycon decl
2366 | DataDecl { tcdDataDefn = dataDefn } <- decl
2367 , HsDataDefn { dd_derivs = derivs } <- dataDefn
2368 = [ DerivInfo { di_rep_tc = tycon
2369 , di_scoped_tvs =
2370 if isFunTyCon tycon || isPrimTyCon tycon
2371 then [] -- no tyConTyVars
2372 else mkTyVarNamePairs (tyConTyVars tycon)
2373 , di_clauses = derivs
2374 , di_ctxt = tcMkDeclCtxt decl } ]
2375 wiredInDerivInfo _ _ = []
2376
2377 -- "type family" declarations
2378 tcTyClDecl1 :: Maybe Class -> RolesInfo -> TyClDecl GhcRn -> TcM (TyCon, [DerivInfo])
2379 tcTyClDecl1 parent _roles_info (FamDecl { tcdFam = fd })
2380 = fmap noDerivInfos $
2381 tcFamDecl1 parent fd
2382
2383 -- "type" synonym declaration
2384 tcTyClDecl1 _parent roles_info
2385 (SynDecl { tcdLName = L _ tc_name
2386 , tcdRhs = rhs })
2387 = assert (isNothing _parent )
2388 fmap noDerivInfos $
2389 tcTySynRhs roles_info tc_name rhs
2390
2391 -- "data/newtype" declaration
2392 tcTyClDecl1 _parent roles_info
2393 decl@(DataDecl { tcdLName = L _ tc_name
2394 , tcdDataDefn = defn })
2395 = assert (isNothing _parent) $
2396 tcDataDefn (tcMkDeclCtxt decl) roles_info tc_name defn
2397
2398 tcTyClDecl1 _parent roles_info
2399 (ClassDecl { tcdLName = L _ class_name
2400 , tcdCtxt = hs_ctxt
2401 , tcdMeths = meths
2402 , tcdFDs = fundeps
2403 , tcdSigs = sigs
2404 , tcdATs = ats
2405 , tcdATDefs = at_defs })
2406 = assert (isNothing _parent) $
2407 do { clas <- tcClassDecl1 roles_info class_name hs_ctxt
2408 meths fundeps sigs ats at_defs
2409 ; return (noDerivInfos (classTyCon clas)) }
2410
2411
2412 {- *********************************************************************
2413 * *
2414 Class declarations
2415 * *
2416 ********************************************************************* -}
2417
2418 tcClassDecl1 :: RolesInfo -> Name -> Maybe (LHsContext GhcRn)
2419 -> LHsBinds GhcRn -> [LHsFunDep GhcRn] -> [LSig GhcRn]
2420 -> [LFamilyDecl GhcRn] -> [LTyFamDefltDecl GhcRn]
2421 -> TcM Class
2422 tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
2423 = fixM $ \ clas ->
2424 -- We need the knot because 'clas' is passed into tcClassATs
2425 bindTyClTyVars class_name $ \ _ binders res_kind ->
2426 do { checkClassKindSig res_kind
2427 ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders)
2428 ; let tycon_name = class_name -- We use the same name
2429 roles = roles_info tycon_name -- for TyCon and Class
2430
2431 ; (ctxt, fds, sig_stuff, at_stuff)
2432 <- pushLevelAndSolveEqualities skol_info (binderVars binders) $
2433 -- The (binderVars binders) is needed bring into scope the
2434 -- skolems bound by the class decl header (#17841)
2435 do { ctxt <- tcHsContext hs_ctxt
2436 ; fds <- mapM (addLocMA tc_fundep) fundeps
2437 ; sig_stuff <- tcClassSigs class_name sigs meths
2438 ; at_stuff <- tcClassATs class_name clas ats at_defs
2439 ; return (ctxt, fds, sig_stuff, at_stuff) }
2440
2441 -- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
2442 -- Example: (typecheck/should_fail/T17562)
2443 -- type C :: Type -> Type -> Constraint
2444 -- class (forall a. a b ~ a c) => C b c
2445 -- The kind of `a` is unconstrained.
2446 ; dvs <- candidateQTyVarsOfTypes ctxt
2447 ; let mk_doc tidy_env = do { (tidy_env2, ctxt) <- zonkTidyTcTypes tidy_env ctxt
2448 ; return ( tidy_env2
2449 , sep [ text "the class context:"
2450 , pprTheta ctxt ] ) }
2451 ; doNotQuantifyTyVars dvs mk_doc
2452
2453 -- The pushLevelAndSolveEqualities will report errors for any
2454 -- unsolved equalities, so these zonks should not encounter
2455 -- any unfilled coercion variables unless there is such an error
2456 -- The zonk also squeeze out the TcTyCons, and converts
2457 -- Skolems to tyvars.
2458 ; ze <- mkEmptyZonkEnv NoFlexi
2459 ; ctxt <- zonkTcTypesToTypesX ze ctxt
2460 ; sig_stuff <- mapM (zonkTcMethInfoToMethInfoX ze) sig_stuff
2461 -- ToDo: do we need to zonk at_stuff?
2462
2463 -- TODO: Allow us to distinguish between abstract class,
2464 -- and concrete class with no methods (maybe by
2465 -- specifying a trailing where or not
2466
2467 ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
2468 ; is_boot <- tcIsHsBootOrSig
2469 ; let body | is_boot, null ctxt, null at_stuff, null sig_stuff
2470 = Nothing
2471 | otherwise
2472 = Just (ctxt, at_stuff, sig_stuff, mindef)
2473
2474 ; clas <- buildClass class_name binders roles fds body
2475 ; traceTc "tcClassDecl" (ppr fundeps $$ ppr binders $$
2476 ppr fds)
2477 ; return clas }
2478 where
2479 skol_info = TyConSkol ClassFlavour class_name
2480 tc_fundep :: GHC.Hs.FunDep GhcRn -> TcM ([Var],[Var])
2481 tc_fundep (FunDep _ tvs1 tvs2)
2482 = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ;
2483 ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
2484 ; return (tvs1',tvs2') }
2485
2486
2487 {- Note [Associated type defaults]
2488 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2489
2490 The following is an example of associated type defaults:
2491 class C a where
2492 data D a
2493
2494 type F a b :: *
2495 type F a b = [a] -- Default
2496
2497 Note that we can get default definitions only for type families, not data
2498 families.
2499 -}
2500
2501 tcClassATs :: Name -- The class name (not knot-tied)
2502 -> Class -- The class parent of this associated type
2503 -> [LFamilyDecl GhcRn] -- Associated types.
2504 -> [LTyFamDefltDecl GhcRn] -- Associated type defaults.
2505 -> TcM [ClassATItem]
2506 tcClassATs class_name cls ats at_defs
2507 = do { -- Complain about associated type defaults for non associated-types
2508 sequence_ [ failWithTc (TcRnBadAssociatedType class_name n)
2509 | n <- map at_def_tycon at_defs
2510 , not (n `elemNameSet` at_names) ]
2511 ; mapM tc_at ats }
2512 where
2513 at_def_tycon :: LTyFamDefltDecl GhcRn -> Name
2514 at_def_tycon = tyFamInstDeclName . unLoc
2515
2516 at_fam_name :: LFamilyDecl GhcRn -> Name
2517 at_fam_name = familyDeclName . unLoc
2518
2519 at_names = mkNameSet (map at_fam_name ats)
2520
2521 at_defs_map :: NameEnv [LTyFamDefltDecl GhcRn]
2522 -- Maps an AT in 'ats' to a list of all its default defs in 'at_defs'
2523 at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv
2524 (at_def_tycon at_def) [at_def])
2525 emptyNameEnv at_defs
2526
2527 tc_at at = do { fam_tc <- addLocMA (tcFamDecl1 (Just cls)) at
2528 ; let at_defs = lookupNameEnv at_defs_map (at_fam_name at)
2529 `orElse` []
2530 ; atd <- tcDefaultAssocDecl fam_tc at_defs
2531 ; return (ATI fam_tc atd) }
2532
2533 -------------------------
2534 tcDefaultAssocDecl ::
2535 TyCon -- ^ Family TyCon (not knot-tied)
2536 -> [LTyFamDefltDecl GhcRn] -- ^ Defaults
2537 -> TcM (Maybe (KnotTied Type, ATValidityInfo)) -- ^ Type checked RHS
2538 tcDefaultAssocDecl _ []
2539 = return Nothing -- No default declaration
2540
2541 tcDefaultAssocDecl _ (d1:_:_)
2542 = failWithTc (TcRnUnknownMessage $ mkPlainError noHints $
2543 text "More than one default declaration for"
2544 <+> ppr (tyFamInstDeclName (unLoc d1)))
2545
2546 tcDefaultAssocDecl fam_tc
2547 [L loc (TyFamInstDecl { tfid_eqn =
2548 FamEqn { feqn_tycon = L _ tc_name
2549 , feqn_bndrs = outer_bndrs
2550 , feqn_pats = hs_pats
2551 , feqn_rhs = hs_rhs_ty }})]
2552 = -- See Note [Type-checking default assoc decls]
2553 setSrcSpanA loc $
2554 tcAddFamInstCtxt (text "default type instance") tc_name $
2555 do { traceTc "tcDefaultAssocDecl 1" (ppr tc_name)
2556 ; let fam_tc_name = tyConName fam_tc
2557 vis_arity = length (tyConVisibleTyVars fam_tc)
2558 vis_pats = numVisibleArgs hs_pats
2559
2560 -- Kind of family check
2561 ; assert (fam_tc_name == tc_name) $
2562 checkTc (isTypeFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
2563
2564 -- Arity check
2565 ; checkTc (vis_pats == vis_arity)
2566 (wrongNumberOfParmsErr vis_arity)
2567
2568 -- Typecheck RHS
2569 --
2570 -- You might think we should pass in some AssocInstInfo, as we're looking
2571 -- at an associated type. But this would be wrong, because an associated
2572 -- type default LHS can mention *different* type variables than the
2573 -- enclosing class. So it's treated more as a freestanding beast.
2574 ; (qtvs, pats, rhs_ty) <- tcTyFamInstEqnGuts fam_tc NotAssociated
2575 outer_bndrs hs_pats hs_rhs_ty
2576
2577 ; let fam_tvs = tyConTyVars fam_tc
2578 ; traceTc "tcDefaultAssocDecl 2" (vcat
2579 [ text "hs_pats" <+> ppr hs_pats
2580 , text "hs_rhs_ty" <+> ppr hs_rhs_ty
2581 , text "fam_tvs" <+> ppr fam_tvs
2582 , text "qtvs" <+> ppr qtvs
2583 -- NB: Do *not* print `pats` or rhs_ty here, as they can mention
2584 -- knot-tied TyCons. See #18648.
2585 ])
2586 ; let subst = case traverse getTyVar_maybe pats of
2587 Just cpt_tvs -> zipTvSubst cpt_tvs (mkTyVarTys fam_tvs)
2588 Nothing -> emptyTCvSubst
2589 -- The Nothing case can only be reached in invalid
2590 -- associated type family defaults. In such cases, we
2591 -- simply create an empty substitution and let GHC fall
2592 -- over later, in GHC.Tc.Validity.checkValidAssocTyFamDeflt.
2593 -- See Note [Type-checking default assoc decls].
2594 ; pure $ Just (substTyUnchecked subst rhs_ty, ATVI (locA loc) pats)
2595 -- We perform checks for well-formedness and validity later, in
2596 -- GHC.Tc.Validity.checkValidAssocTyFamDeflt.
2597 }
2598
2599 {- Note [Type-checking default assoc decls]
2600 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2601 Consider this default declaration for an associated type
2602
2603 class C a where
2604 type F (a :: k) b :: Type
2605 type F (x :: j) y = Proxy x -> y
2606
2607 Note that the class variable 'a' doesn't scope over the default assoc
2608 decl, nor do the type variables `k` and `b`. Instead, the default decl is
2609 treated more like a top-level type instance. However, we store the default rhs
2610 (Proxy x -> y) in F's TyCon, using F's own type variables, so we need to
2611 convert it to (Proxy a -> b). We do this in the tcDefaultAssocDecl function by
2612 creating a substitution [j |-> k, x |-> a, b |-> y] and applying this
2613 substitution to the RHS.
2614
2615 In order to create this substitution, we must first ensure that all of
2616 the arguments in the default instance consist of distinct type variables.
2617 Checking for this property proves surprisingly tricky. Three potential places
2618 where GHC could check for this property include:
2619
2620 1. Before typechecking (in the parser or renamer)
2621 2. During typechecking (in tcDefaultAssocDecl)
2622 3. After typechecking (using GHC.Tc.Validity)
2623
2624 Currently, GHC picks option (3) and implements this check using
2625 GHC.Tc.Validity.checkValidAssocTyFamDeflt. GHC previously used options (1) and
2626 (2), but neither option quite worked out for reasons that we will explain
2627 shortly.
2628
2629 The first thing that checkValidAssocTyFamDeflt does is check that all arguments
2630 in an associated type family default are type variables. As a motivating
2631 example, consider this erroneous program (inspired by #11361):
2632
2633 class C a where
2634 type F (a :: k) b :: Type
2635 type F x b = x
2636
2637 If you squint, you'll notice that the kind of `x` is actually Type. However,
2638 we cannot substitute from [Type |-> k], so we reject this default. This also
2639 explains why GHC no longer implements option (1) above, since figuring out that
2640 `x`'s kind is Type would be much more difficult without the knowledge that the
2641 typechecker provides.
2642
2643 Next, checkValidAssocTyFamDeflt checks that all arguments are distinct. Here is
2644 another offending example, this time taken from #13971:
2645
2646 class C2 (a :: j) where
2647 type F2 (a :: j) (b :: k)
2648 type F2 (x :: z) y = SameKind x y
2649 data SameKind :: k -> k -> Type
2650
2651 All of the arguments in the default equation for `F2` are type variables, so
2652 that passes the first check. However, if we were to build this substitution,
2653 then both `j` and `k` map to `z`! In terms of visible kind application, it's as
2654 if we had written `type F2 @z @z x y = SameKind @z x y`, which makes it clear
2655 that we have duplicated a use of `z` on the LHS. Therefore, `F2`'s default is
2656 also rejected.
2657
2658 There is one more design consideration in play here: what error message should
2659 checkValidAssocTyFamDeflt produce if one of its checks fails? Ideally, it would
2660 be something like this:
2661
2662 Illegal duplicate variable ‘z’ in:
2663 ‘type F2 @z @z x y = ...’
2664 The arguments to ‘F2’ must all be distinct type variables
2665
2666 This requires printing out the arguments to the associated type family. This
2667 can be dangerous, however. Consider this example, adapted from #18648:
2668
2669 class C3 a where
2670 type F3 a
2671 type F3 (F3 a) = a
2672
2673 F3's default is illegal, since its argument is not a bare type variable. But
2674 note that when we typecheck F3's default, the F3 type constructor is knot-tied.
2675 Therefore, if we print the type `F3 a` in an error message, GHC will diverge!
2676 This is the reason why GHC no longer implements option (2) above and instead
2677 waits until /after/ typechecking has finished, at which point the typechecker
2678 knot has been worked out.
2679
2680 As one final point, one might worry that the typechecker knot could cause the
2681 substitution that tcDefaultAssocDecl creates to diverge, but this is not the
2682 case. Since the LHS of a valid associated type family default is always just
2683 variables, it won't contain any tycons. Accordingly, the patterns used in the
2684 substitution won't actually be knot-tied, even though we're in the knot. (This
2685 is too delicate for my taste, but it works.) If we're dealing with /invalid/
2686 default, such as F3's above, then we simply create an empty substitution and
2687 rely on checkValidAssocTyFamDeflt throwing an error message afterwards before
2688 any damage is done.
2689 -}
2690
2691 {- *********************************************************************
2692 * *
2693 Type family declarations
2694 * *
2695 ********************************************************************* -}
2696
2697 tcFamDecl1 :: Maybe Class -> FamilyDecl GhcRn -> TcM TyCon
2698 tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
2699 , fdLName = tc_lname@(L _ tc_name)
2700 , fdResultSig = L _ sig
2701 , fdInjectivityAnn = inj })
2702 | DataFamily <- fam_info
2703 = bindTyClTyVars tc_name $ \ _ binders res_kind -> do
2704 { traceTc "tcFamDecl1 data family:" (ppr tc_name)
2705 ; checkFamFlag tc_name
2706
2707 -- Check that the result kind is OK
2708 -- We allow things like
2709 -- data family T (a :: Type) :: forall k. k -> Type
2710 -- We treat T as having arity 1, but result kind forall k. k -> Type
2711 -- But we want to check that the result kind finishes in
2712 -- Type or a kind-variable
2713 -- For the latter, consider
2714 -- data family D a :: forall k. Type -> k
2715 -- When UnliftedNewtypes is enabled, we loosen this restriction
2716 -- on the return kind. See Note [Implementation of UnliftedNewtypes], wrinkle (1).
2717 -- See also Note [Datatype return kinds]
2718 ; checkDataKindSig DataFamilySort res_kind
2719 ; tc_rep_name <- newTyConRepName tc_name
2720 ; let inj = Injective $ replicate (length binders) True
2721 tycon = mkFamilyTyCon tc_name binders
2722 res_kind
2723 (resultVariableName sig)
2724 (DataFamilyTyCon tc_rep_name)
2725 parent inj
2726 ; return tycon }
2727
2728 | OpenTypeFamily <- fam_info
2729 = bindTyClTyVars tc_name $ \ _ binders res_kind -> do
2730 { traceTc "tcFamDecl1 open type family:" (ppr tc_name)
2731 ; checkFamFlag tc_name
2732 ; inj' <- tcInjectivity binders inj
2733 ; checkResultSigFlag tc_name sig -- check after injectivity for better errors
2734 ; let tycon = mkFamilyTyCon tc_name binders res_kind
2735 (resultVariableName sig) OpenSynFamilyTyCon
2736 parent inj'
2737 ; return tycon }
2738
2739 | ClosedTypeFamily mb_eqns <- fam_info
2740 = -- Closed type families are a little tricky, because they contain the definition
2741 -- of both the type family and the equations for a CoAxiom.
2742 do { traceTc "tcFamDecl1 Closed type family:" (ppr tc_name)
2743 -- the variables in the header scope only over the injectivity
2744 -- declaration but this is not involved here
2745 ; (inj', binders, res_kind)
2746 <- bindTyClTyVars tc_name $ \ _ binders res_kind ->
2747 do { inj' <- tcInjectivity binders inj
2748 ; return (inj', binders, res_kind) }
2749
2750 ; checkFamFlag tc_name -- make sure we have -XTypeFamilies
2751 ; checkResultSigFlag tc_name sig
2752
2753 -- If Nothing, this is an abstract family in a hs-boot file;
2754 -- but eqns might be empty in the Just case as well
2755 ; case mb_eqns of
2756 Nothing ->
2757 return $ mkFamilyTyCon tc_name binders res_kind
2758 (resultVariableName sig)
2759 AbstractClosedSynFamilyTyCon parent
2760 inj'
2761 Just eqns -> do {
2762
2763 -- Process the equations, creating CoAxBranches
2764 ; let tc_fam_tc = mkTcTyCon tc_name binders res_kind
2765 noTcTyConScopedTyVars
2766 False {- this doesn't matter here -}
2767 ClosedTypeFamilyFlavour
2768
2769 ; branches <- mapAndReportM (tcTyFamInstEqn tc_fam_tc NotAssociated) eqns
2770 -- Do not attempt to drop equations dominated by earlier
2771 -- ones here; in the case of mutual recursion with a data
2772 -- type, we get a knot-tying failure. Instead we check
2773 -- for this afterwards, in GHC.Tc.Validity.checkValidCoAxiom
2774 -- Example: tc265
2775
2776 -- Create a CoAxiom, with the correct src location.
2777 ; co_ax_name <- newFamInstAxiomName tc_lname []
2778
2779 ; let mb_co_ax
2780 | null eqns = Nothing -- mkBranchedCoAxiom fails on empty list
2781 | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches)
2782
2783 fam_tc = mkFamilyTyCon tc_name binders res_kind (resultVariableName sig)
2784 (ClosedSynFamilyTyCon mb_co_ax) parent inj'
2785
2786 -- We check for instance validity later, when doing validity
2787 -- checking for the tycon. Exception: checking equations
2788 -- overlap done by dropDominatedAxioms
2789 ; return fam_tc } }
2790
2791 #if __GLASGOW_HASKELL__ <= 810
2792 | otherwise = panic "tcFamInst1" -- Silence pattern-exhaustiveness checker
2793 #endif
2794
2795 -- | Maybe return a list of Bools that say whether a type family was declared
2796 -- injective in the corresponding type arguments. Length of the list is equal to
2797 -- the number of arguments (including implicit kind/coercion arguments).
2798 -- True on position
2799 -- N means that a function is injective in its Nth argument. False means it is
2800 -- not.
2801 tcInjectivity :: [TyConBinder] -> Maybe (LInjectivityAnn GhcRn)
2802 -> TcM Injectivity
2803 tcInjectivity _ Nothing
2804 = return NotInjective
2805
2806 -- User provided an injectivity annotation, so for each tyvar argument we
2807 -- check whether a type family was declared injective in that argument. We
2808 -- return a list of Bools, where True means that corresponding type variable
2809 -- was mentioned in lInjNames (type family is injective in that argument) and
2810 -- False means that it was not mentioned in lInjNames (type family is not
2811 -- injective in that type variable). We also extend injectivity information to
2812 -- kind variables, so if a user declares:
2813 --
2814 -- type family F (a :: k1) (b :: k2) = (r :: k3) | r -> a
2815 --
2816 -- then we mark both `a` and `k1` as injective.
2817 -- NB: the return kind is considered to be *input* argument to a type family.
2818 -- Since injectivity allows to infer input arguments from the result in theory
2819 -- we should always mark the result kind variable (`k3` in this example) as
2820 -- injective. The reason is that result type has always an assigned kind and
2821 -- therefore we can always infer the result kind if we know the result type.
2822 -- But this does not seem to be useful in any way so we don't do it. (Another
2823 -- reason is that the implementation would not be straightforward.)
2824 tcInjectivity tcbs (Just (L loc (InjectivityAnn _ _ lInjNames)))
2825 = setSrcSpanA loc $
2826 do { let tvs = binderVars tcbs
2827 ; dflags <- getDynFlags
2828 ; checkTc (xopt LangExt.TypeFamilyDependencies dflags)
2829 (TcRnUnknownMessage $ mkPlainError noHints $
2830 text "Illegal injectivity annotation" $$
2831 text "Use TypeFamilyDependencies to allow this")
2832 ; inj_tvs <- mapM (tcLookupTyVar . unLoc) lInjNames
2833 ; inj_tvs <- mapM zonkTcTyVarToTyVar inj_tvs -- zonk the kinds
2834 ; let inj_ktvs = filterVarSet isTyVar $ -- no injective coercion vars
2835 closeOverKinds (mkVarSet inj_tvs)
2836 ; let inj_bools = map (`elemVarSet` inj_ktvs) tvs
2837 ; traceTc "tcInjectivity" (vcat [ ppr tvs, ppr lInjNames, ppr inj_tvs
2838 , ppr inj_ktvs, ppr inj_bools ])
2839 ; return $ Injective inj_bools }
2840
2841 tcTySynRhs :: RolesInfo -> Name
2842 -> LHsType GhcRn -> TcM TyCon
2843 tcTySynRhs roles_info tc_name hs_ty
2844 = bindTyClTyVars tc_name $ \ _ binders res_kind ->
2845 do { env <- getLclEnv
2846 ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
2847 ; rhs_ty <- pushLevelAndSolveEqualities skol_info (binderVars binders) $
2848 tcCheckLHsType hs_ty (TheKind res_kind)
2849
2850 -- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
2851 -- Example: (typecheck/should_fail/T17567)
2852 -- type T = forall a. Proxy a
2853 -- The kind of `a` is unconstrained.
2854 ; dvs <- candidateQTyVarsOfType rhs_ty
2855 ; let mk_doc tidy_env = do { (tidy_env2, rhs_ty) <- zonkTidyTcType tidy_env rhs_ty
2856 ; return ( tidy_env2
2857 , sep [ text "the type synonym right-hand side:"
2858 , ppr rhs_ty ] ) }
2859 ; doNotQuantifyTyVars dvs mk_doc
2860
2861 ; ze <- mkEmptyZonkEnv NoFlexi
2862 ; rhs_ty <- zonkTcTypeToTypeX ze rhs_ty
2863 ; let roles = roles_info tc_name
2864 ; return (buildSynTyCon tc_name binders res_kind roles rhs_ty) }
2865 where
2866 skol_info = TyConSkol TypeSynonymFlavour tc_name
2867
2868 tcDataDefn :: SDoc -> RolesInfo -> Name
2869 -> HsDataDefn GhcRn -> TcM (TyCon, [DerivInfo])
2870 -- NB: not used for newtype/data instances (whether associated or not)
2871 tcDataDefn err_ctxt roles_info tc_name
2872 (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
2873 , dd_ctxt = ctxt
2874 , dd_kindSig = mb_ksig -- Already in tc's kind
2875 -- via inferInitialKinds
2876 , dd_cons = cons
2877 , dd_derivs = derivs })
2878 = bindTyClTyVars tc_name $ \ tctc tycon_binders res_kind ->
2879 -- 'tctc' is a 'TcTyCon' and has the 'tcTyConScopedTyVars' that we need
2880 -- unlike the finalized 'tycon' defined above which is an 'AlgTyCon'
2881 --
2882 -- The TyCon tyvars must scope over
2883 -- - the stupid theta (dd_ctxt)
2884 -- - for H98 constructors only, the ConDecl
2885 -- But it does no harm to bring them into scope
2886 -- over GADT ConDecls as well; and it's awkward not to
2887 do { gadt_syntax <- dataDeclChecks tc_name new_or_data ctxt cons
2888 -- see Note [Datatype return kinds]
2889 ; (extra_bndrs, final_res_kind) <- etaExpandAlgTyCon tycon_binders res_kind
2890
2891 ; tcg_env <- getGblEnv
2892 ; let hsc_src = tcg_src tcg_env
2893 ; unless (mk_permissive_kind hsc_src cons) $
2894 checkDataKindSig (DataDeclSort new_or_data) final_res_kind
2895
2896 ; let skol_tvs = binderVars tycon_binders
2897 ; stupid_tc_theta <- pushLevelAndSolveEqualities skol_info skol_tvs $
2898 tcHsContext ctxt
2899
2900 -- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
2901 -- Example: (typecheck/should_fail/T17567StupidTheta)
2902 -- data (forall a. a b ~ a c) => T b c
2903 -- The kind of 'a' is unconstrained.
2904 ; dvs <- candidateQTyVarsOfTypes stupid_tc_theta
2905 ; let mk_doc tidy_env
2906 = do { (tidy_env2, theta) <- zonkTidyTcTypes tidy_env stupid_tc_theta
2907 ; return ( tidy_env2
2908 , sep [ text "the datatype context:"
2909 , pprTheta theta ] ) }
2910 ; doNotQuantifyTyVars dvs mk_doc
2911
2912 ; ze <- mkEmptyZonkEnv NoFlexi
2913 ; stupid_theta <- zonkTcTypesToTypesX ze stupid_tc_theta
2914
2915 -- Check that we don't use kind signatures without the extension
2916 ; kind_signatures <- xoptM LangExt.KindSignatures
2917 ; when (isJust mb_ksig) $
2918 checkTc (kind_signatures) (badSigTyDecl tc_name)
2919
2920 ; tycon <- fixM $ \ rec_tycon -> do
2921 { let final_bndrs = tycon_binders `chkAppend` extra_bndrs
2922 roles = roles_info tc_name
2923 ; data_cons <- tcConDecls
2924 new_or_data DDataType
2925 rec_tycon final_bndrs final_res_kind
2926 cons
2927 ; tc_rhs <- mk_tc_rhs hsc_src rec_tycon data_cons
2928 ; tc_rep_nm <- newTyConRepName tc_name
2929 ; return (mkAlgTyCon tc_name
2930 final_bndrs
2931 final_res_kind
2932 roles
2933 (fmap unLoc cType)
2934 stupid_theta tc_rhs
2935 (VanillaAlgTyCon tc_rep_nm)
2936 gadt_syntax) }
2937 ; let deriv_info = DerivInfo { di_rep_tc = tycon
2938 , di_scoped_tvs = tcTyConScopedTyVars tctc
2939 , di_clauses = derivs
2940 , di_ctxt = err_ctxt }
2941 ; traceTc "tcDataDefn" (ppr tc_name $$ ppr tycon_binders $$ ppr extra_bndrs)
2942 ; return (tycon, [deriv_info]) }
2943 where
2944 skol_info = TyConSkol flav tc_name
2945 flav = newOrDataToFlavour new_or_data
2946
2947 -- Abstract data types in hsig files can have arbitrary kinds,
2948 -- because they may be implemented by type synonyms
2949 -- (which themselves can have arbitrary kinds, not just *). See #13955.
2950 --
2951 -- Note that this is only a property that data type declarations possess,
2952 -- so one could not have, say, a data family instance in an hsig file that
2953 -- has kind `Bool`. Therefore, this check need only occur in the code that
2954 -- typechecks data type declarations.
2955 mk_permissive_kind HsigFile [] = True
2956 mk_permissive_kind _ _ = False
2957
2958 -- In an hs-boot or a signature file,
2959 -- a 'data' declaration with no constructors
2960 -- indicates a nominally distinct abstract data type.
2961 mk_tc_rhs (isHsBootOrSig -> True) _ []
2962 = return AbstractTyCon
2963
2964 mk_tc_rhs _ tycon data_cons
2965 = case new_or_data of
2966 DataType -> return $
2967 mkLevPolyDataTyConRhs
2968 (isFixedRuntimeRepKind (tyConResKind tycon))
2969 data_cons
2970 NewType -> assert (not (null data_cons)) $
2971 mkNewTyConRhs tc_name tycon (head data_cons)
2972
2973 -------------------------
2974 kcTyFamInstEqn :: TcTyCon -> LTyFamInstEqn GhcRn -> TcM ()
2975 -- Used for the equations of a closed type family only
2976 -- Not used for data/type instances
2977 kcTyFamInstEqn tc_fam_tc
2978 (L loc (FamEqn { feqn_tycon = L _ eqn_tc_name
2979 , feqn_bndrs = outer_bndrs
2980 , feqn_pats = hs_pats
2981 , feqn_rhs = hs_rhs_ty }))
2982 = setSrcSpanA loc $
2983 do { traceTc "kcTyFamInstEqn" (vcat
2984 [ text "tc_name =" <+> ppr eqn_tc_name
2985 , text "fam_tc =" <+> ppr tc_fam_tc <+> dcolon <+> ppr (tyConKind tc_fam_tc)
2986 , text "feqn_bndrs =" <+> ppr outer_bndrs
2987 , text "feqn_pats =" <+> ppr hs_pats ])
2988
2989 ; checkTyFamInstEqn tc_fam_tc eqn_tc_name hs_pats
2990
2991 ; discardResult $
2992 bindOuterFamEqnTKBndrs_Q_Tv outer_bndrs $
2993 do { (_fam_app, res_kind) <- tcFamTyPats tc_fam_tc hs_pats
2994 ; tcCheckLHsType hs_rhs_ty (TheKind res_kind) }
2995 -- Why "_Tv" here? Consider (#14066)
2996 -- type family Bar x y where
2997 -- Bar (x :: a) (y :: b) = Int
2998 -- Bar (x :: c) (y :: d) = Bool
2999 -- During kind-checking, a,b,c,d should be TyVarTvs and unify appropriately
3000 }
3001
3002 --------------------------
3003 tcTyFamInstEqn :: TcTyCon -> AssocInstInfo -> LTyFamInstEqn GhcRn
3004 -> TcM (KnotTied CoAxBranch)
3005 -- Needs to be here, not in GHC.Tc.TyCl.Instance, because closed families
3006 -- (typechecked here) have TyFamInstEqns
3007
3008 tcTyFamInstEqn fam_tc mb_clsinfo
3009 (L loc (FamEqn { feqn_tycon = L _ eqn_tc_name
3010 , feqn_bndrs = outer_bndrs
3011 , feqn_pats = hs_pats
3012 , feqn_rhs = hs_rhs_ty }))
3013 = setSrcSpanA loc $
3014 do { traceTc "tcTyFamInstEqn" $
3015 vcat [ ppr loc, ppr fam_tc <+> ppr hs_pats
3016 , text "fam tc bndrs" <+> pprTyVars (tyConTyVars fam_tc)
3017 , case mb_clsinfo of
3018 NotAssociated {} -> empty
3019 InClsInst { ai_class = cls } -> text "class" <+> ppr cls <+> pprTyVars (classTyVars cls) ]
3020
3021 ; checkTyFamInstEqn fam_tc eqn_tc_name hs_pats
3022
3023 ; (qtvs, pats, rhs_ty) <- tcTyFamInstEqnGuts fam_tc mb_clsinfo
3024 outer_bndrs hs_pats hs_rhs_ty
3025 -- Don't print results they may be knot-tied
3026 -- (tcFamInstEqnGuts zonks to Type)
3027 ; return (mkCoAxBranch qtvs [] [] pats rhs_ty
3028 (map (const Nominal) qtvs)
3029 (locA loc)) }
3030
3031 checkTyFamInstEqn :: TcTyCon -> Name -> [HsArg tm ty] -> TcM ()
3032 checkTyFamInstEqn tc_fam_tc eqn_tc_name hs_pats =
3033 do { -- Ensure that each equation's type constructor is for the right
3034 -- type family. E.g. barf on
3035 -- type family F a where { G Int = Bool }
3036 let tc_fam_tc_name = getName tc_fam_tc
3037 ; checkTc (tc_fam_tc_name == eqn_tc_name) $
3038 wrongTyFamName tc_fam_tc_name eqn_tc_name
3039
3040 -- Check the arity of visible arguments
3041 -- If we wait until validity checking, we'll get kind errors
3042 -- below when an arity error will be much easier to understand.
3043 ; let vis_arity = length (tyConVisibleTyVars tc_fam_tc)
3044 vis_pats = numVisibleArgs hs_pats
3045 ; checkTc (vis_pats == vis_arity) $
3046 wrongNumberOfParmsErr vis_arity
3047 }
3048
3049 {- Note [Instantiating a family tycon]
3050 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3051 It's possible that kind-checking the result of a family tycon applied to
3052 its patterns will instantiate the tycon further. For example, we might
3053 have
3054
3055 type family F :: k where
3056 F = Int
3057 F = Maybe
3058
3059 After checking (F :: forall k. k) (with no visible patterns), we still need
3060 to instantiate the k. With data family instances, this problem can be even
3061 more intricate, due to Note [Arity of data families] in GHC.Core.FamInstEnv. See
3062 indexed-types/should_compile/T12369 for an example.
3063
3064 So, the kind-checker must return the new skolems and args (that is, Type
3065 or (Type -> Type) for the equations above) and the instantiated kind.
3066
3067 Note [Generalising in tcTyFamInstEqnGuts]
3068 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3069 Suppose we have something like
3070 type instance forall (a::k) b. F (Proxy t1) _ = rhs
3071
3072 Then imp_vars = [k], exp_bndrs = [a::k, b]
3073
3074 We want to quantify over all the free vars of the LHS including
3075 * any invisible kind variables arising from instantiating tycons,
3076 such as Proxy
3077 * wildcards such as '_' above
3078
3079 The wildcards are particularly awkward: they may need to be quantified
3080 - before the explicit variables k,a,b
3081 - after them
3082 - or even interleaved with them
3083 c.f. Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType
3084
3085 So, we use bindOuterFamEqnTKBndrs (which does not create an implication for
3086 the telescope), and generalise over /all/ the variables in the LHS,
3087 without treating the explicitly-quanfitifed ones specially. Wrinkles:
3088
3089 - When generalising, include the explicit user-specified forall'd
3090 variables, so that we get an error from Validity.checkFamPatBinders
3091 if a forall'd variable is not bound on the LHS
3092
3093 - We still want to complain about a bad telescope among the user-specified
3094 variables. So in checkFamTelescope we emit an implication constraint
3095 quantifying only over them, purely so that we get a good telescope error.
3096
3097 - Note that, unlike a type signature like
3098 f :: forall (a::k). blah
3099 we do /not/ care about the Inferred/Specified designation or order for
3100 the final quantified tyvars. Type-family instances are not invoked
3101 directly in Haskell source code, so visible type application etc plays
3102 no role.
3103
3104 See also Note [Re-quantify type variables in rules] in
3105 GHC.Tc.Gen.Rule, which explains a /very/ similar design when
3106 generalising over the type of a rewrite rule.
3107
3108 -}
3109
3110 --------------------------
3111 tcTyFamInstEqnGuts :: TyCon -> AssocInstInfo
3112 -> HsOuterFamEqnTyVarBndrs GhcRn -- Implicit and explicit binders
3113 -> HsTyPats GhcRn -- Patterns
3114 -> LHsType GhcRn -- RHS
3115 -> TcM ([TyVar], [TcType], TcType) -- (tyvars, pats, rhs)
3116 -- Used only for type families, not data families
3117 tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_hs_bndrs hs_pats hs_rhs_ty
3118 = do { traceTc "tcTyFamInstEqnGuts {" (ppr fam_tc)
3119
3120 -- By now, for type families (but not data families) we should
3121 -- have checked that the number of patterns matches tyConArity
3122
3123 -- This code is closely related to the code
3124 -- in GHC.Tc.Gen.HsType.kcCheckDeclHeader_cusk
3125 ; (tclvl, wanted, (outer_tvs, (lhs_ty, rhs_ty)))
3126 <- pushLevelAndSolveEqualitiesX "tcTyFamInstEqnGuts" $
3127 bindOuterFamEqnTKBndrs outer_hs_bndrs $
3128 do { (lhs_ty, rhs_kind) <- tcFamTyPats fam_tc hs_pats
3129 -- Ensure that the instance is consistent with its
3130 -- parent class (#16008)
3131 ; addConsistencyConstraints mb_clsinfo lhs_ty
3132 ; rhs_ty <- tcCheckLHsType hs_rhs_ty (TheKind rhs_kind)
3133 ; return (lhs_ty, rhs_ty) }
3134
3135 -- This code (and the stuff immediately above) is very similar
3136 -- to that in tcDataFamInstHeader. Maybe we should abstract the
3137 -- common code; but for the moment I concluded that it's
3138 -- clearer to duplicate it. Still, if you fix a bug here,
3139 -- check there too!
3140
3141 -- See Note [Generalising in tcTyFamInstEqnGuts]
3142 ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys outer_tvs)
3143 ; qtvs <- quantifyTyVars noVarsOfKindDefault dvs
3144 ; reportUnsolvedEqualities FamInstSkol qtvs tclvl wanted
3145 ; checkFamTelescope tclvl outer_hs_bndrs outer_tvs
3146
3147 ; traceTc "tcTyFamInstEqnGuts 2" $
3148 vcat [ ppr fam_tc
3149 , text "lhs_ty" <+> ppr lhs_ty
3150 , text "qtvs" <+> pprTyVars qtvs ]
3151
3152 -- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
3153 -- Example: typecheck/should_fail/T17301
3154 ; dvs_rhs <- candidateQTyVarsOfType rhs_ty
3155 ; let mk_doc tidy_env
3156 = do { (tidy_env2, rhs_ty) <- zonkTidyTcType tidy_env rhs_ty
3157 ; return ( tidy_env2
3158 , sep [ text "type family equation right-hand side:"
3159 , ppr rhs_ty ] ) }
3160 ; doNotQuantifyTyVars dvs_rhs mk_doc
3161
3162 ; ze <- mkEmptyZonkEnv NoFlexi
3163 ; (ze, qtvs) <- zonkTyBndrsX ze qtvs
3164 ; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty
3165 ; rhs_ty <- zonkTcTypeToTypeX ze rhs_ty
3166
3167 ; let pats = unravelFamInstPats lhs_ty
3168 -- Note that we do this after solveEqualities
3169 -- so that any strange coercions inside lhs_ty
3170 -- have been solved before we attempt to unravel it
3171 ; traceTc "tcTyFamInstEqnGuts }" (ppr fam_tc <+> pprTyVars qtvs)
3172 ; return (qtvs, pats, rhs_ty) }
3173
3174
3175 checkFamTelescope :: TcLevel -> HsOuterFamEqnTyVarBndrs GhcRn
3176 -> [TcTyVar] -> TcM ()
3177 -- Emit a constraint (forall a b c. <empty>), so that
3178 -- we will do telescope-checking on a,b,c
3179 -- See Note [Generalising in tcTyFamInstEqnGuts]
3180 checkFamTelescope tclvl hs_outer_bndrs outer_tvs
3181 | HsOuterExplicit { hso_bndrs = bndrs } <- hs_outer_bndrs
3182 , (b_first : _) <- bndrs
3183 , let b_last = last bndrs
3184 skol_info = ForAllSkol (fsep (map ppr bndrs))
3185 = setSrcSpan (combineSrcSpans (getLocA b_first) (getLocA b_last)) $
3186 emitResidualTvConstraint skol_info outer_tvs tclvl emptyWC
3187 | otherwise
3188 = return ()
3189
3190 -----------------
3191 unravelFamInstPats :: TcType -> [TcType]
3192 -- Decompose fam_app to get the argument patterns
3193 --
3194 -- We expect fam_app to look like (F t1 .. tn)
3195 -- tcFamTyPats is capable of returning ((F ty1 |> co) ty2),
3196 -- but that can't happen here because we already checked the
3197 -- arity of F matches the number of pattern
3198 unravelFamInstPats fam_app
3199 = case splitTyConApp_maybe fam_app of
3200 Just (_, pats) -> pats
3201 Nothing -> panic "unravelFamInstPats: Ill-typed LHS of family instance"
3202 -- The Nothing case cannot happen for type families, because
3203 -- we don't call unravelFamInstPats until we've solved the
3204 -- equalities. For data families, it shouldn't happen either,
3205 -- we need to fail hard and early if it does. See trac issue #15905
3206 -- for an example of this happening.
3207
3208 addConsistencyConstraints :: AssocInstInfo -> TcType -> TcM ()
3209 -- In the corresponding positions of the class and type-family,
3210 -- ensure the family argument is the same as the class argument
3211 -- E.g class C a b c d where
3212 -- F c x y a :: Type
3213 -- Here the first arg of F should be the same as the third of C
3214 -- and the fourth arg of F should be the same as the first of C
3215 --
3216 -- We emit /Derived/ constraints (a bit like fundeps) to encourage
3217 -- unification to happen, but without actually reporting errors.
3218 -- If, despite the efforts, corresponding positions do not match,
3219 -- checkConsistentFamInst will complain
3220 addConsistencyConstraints mb_clsinfo fam_app
3221 | InClsInst { ai_inst_env = inst_env } <- mb_clsinfo
3222 , Just (fam_tc, pats) <- tcSplitTyConApp_maybe fam_app
3223 = do { let eqs = [ (cls_ty, pat)
3224 | (fam_tc_tv, pat) <- tyConTyVars fam_tc `zip` pats
3225 , Just cls_ty <- [lookupVarEnv inst_env fam_tc_tv] ]
3226 ; traceTc "addConsistencyConstraints" (ppr eqs)
3227 ; emitDerivedEqs AssocFamPatOrigin eqs }
3228 -- Improve inference
3229 -- Any mis-match is reports by checkConsistentFamInst
3230 | otherwise
3231 = return ()
3232
3233 {- Note [Constraints in patterns]
3234 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3235 NB: This isn't the whole story. See comment in tcFamTyPats.
3236
3237 At first glance, it seems there is a complicated story to tell in tcFamTyPats
3238 around constraint solving. After all, type family patterns can now do
3239 GADT pattern-matching, which is jolly complicated. But, there's a key fact
3240 which makes this all simple: everything is at top level! There cannot
3241 be untouchable type variables. There can't be weird interaction between
3242 case branches. There can't be global skolems.
3243
3244 This means that the semantics of type-level GADT matching is a little
3245 different than term level. If we have
3246
3247 data G a where
3248 MkGBool :: G Bool
3249
3250 And then
3251
3252 type family F (a :: G k) :: k
3253 type instance F MkGBool = True
3254
3255 we get
3256
3257 axF : F Bool (MkGBool <Bool>) ~ True
3258
3259 Simple! No casting on the RHS, because we can affect the kind parameter
3260 to F.
3261
3262 If we ever introduce local type families, this all gets a lot more
3263 complicated, and will end up looking awfully like term-level GADT
3264 pattern-matching.
3265
3266
3267 ** The new story **
3268
3269 Here is really what we want:
3270
3271 The matcher really can't deal with covars in arbitrary spots in coercions.
3272 But it can deal with covars that are arguments to GADT data constructors.
3273 So we somehow want to allow covars only in precisely those spots, then use
3274 them as givens when checking the RHS. TODO (RAE): Implement plan.
3275
3276 Note [Quantified kind variables of a family pattern]
3277 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3278 Consider type family KindFam (p :: k1) (q :: k1)
3279 data T :: Maybe k1 -> k2 -> *
3280 type instance KindFam (a :: Maybe k) b = T a b -> Int
3281 The HsBSig for the family patterns will be ([k], [a])
3282
3283 Then in the family instance we want to
3284 * Bring into scope [ "k" -> k:*, "a" -> a:k ]
3285 * Kind-check the RHS
3286 * Quantify the type instance over k and k', as well as a,b, thus
3287 type instance [k, k', a:Maybe k, b:k']
3288 KindFam (Maybe k) k' a b = T k k' a b -> Int
3289
3290 Notice that in the third step we quantify over all the visibly-mentioned
3291 type variables (a,b), but also over the implicitly mentioned kind variables
3292 (k, k'). In this case one is bound explicitly but often there will be
3293 none. The role of the kind signature (a :: Maybe k) is to add a constraint
3294 that 'a' must have that kind, and to bring 'k' into scope.
3295
3296
3297
3298 ************************************************************************
3299 * *
3300 Data types
3301 * *
3302 ************************************************************************
3303 -}
3304
3305 dataDeclChecks :: Name -> NewOrData
3306 -> Maybe (LHsContext GhcRn) -> [LConDecl GhcRn]
3307 -> TcM Bool
3308 dataDeclChecks tc_name new_or_data mctxt cons
3309 = do { let stupid_theta = fromMaybeContext mctxt
3310 -- Check that we don't use GADT syntax in H98 world
3311 ; gadtSyntax_ok <- xoptM LangExt.GADTSyntax
3312 ; let gadt_syntax = consUseGadtSyntax cons
3313 ; checkTc (gadtSyntax_ok || not gadt_syntax) (badGadtDecl tc_name)
3314
3315 -- Check that the stupid theta is empty for a GADT-style declaration
3316 ; checkTc (null stupid_theta || not gadt_syntax) (badStupidTheta tc_name)
3317
3318 -- Check that a newtype has exactly one constructor
3319 -- Do this before checking for empty data decls, so that
3320 -- we don't suggest -XEmptyDataDecls for newtypes
3321 ; checkTc (new_or_data == DataType || isSingleton cons)
3322 (newtypeConError tc_name (length cons))
3323
3324 -- Check that there's at least one condecl,
3325 -- or else we're reading an hs-boot file, or -XEmptyDataDecls
3326 ; empty_data_decls <- xoptM LangExt.EmptyDataDecls
3327 ; is_boot <- tcIsHsBootOrSig -- Are we compiling an hs-boot file?
3328 ; checkTc (not (null cons) || empty_data_decls || is_boot)
3329 (emptyConDeclsErr tc_name)
3330 ; return gadt_syntax }
3331
3332
3333 -----------------------------------
3334 consUseGadtSyntax :: [LConDecl GhcRn] -> Bool
3335 consUseGadtSyntax (L _ (ConDeclGADT {}) : _) = True
3336 consUseGadtSyntax _ = False
3337 -- All constructors have same shape
3338
3339 -----------------------------------
3340 data DataDeclInfo
3341 = DDataType -- data T a b = T1 a | T2 b
3342 | DDataInstance -- data instance D [a] = D1 a | D2
3343 Type -- The header D [a]
3344
3345 mkDDHeaderTy :: DataDeclInfo -> TyCon -> [TyConBinder] -> Type
3346 mkDDHeaderTy dd_info rep_tycon tc_bndrs
3347 = case dd_info of
3348 DDataType -> mkTyConApp rep_tycon $
3349 mkTyVarTys (binderVars tc_bndrs)
3350 DDataInstance header_ty -> header_ty
3351
3352 tcConDecls :: NewOrData
3353 -> DataDeclInfo
3354 -> KnotTied TyCon -- Representation TyCon
3355 -> [TyConBinder] -- Binders of representation TyCon
3356 -> TcKind -- Result kind
3357 -> [LConDecl GhcRn] -> TcM [DataCon]
3358 tcConDecls new_or_data dd_info rep_tycon tmpl_bndrs res_kind
3359 = concatMapM $ addLocMA $
3360 tcConDecl new_or_data dd_info rep_tycon tmpl_bndrs res_kind
3361 (mkTyConTagMap rep_tycon)
3362 -- mkTyConTagMap: it's important that we pay for tag allocation here,
3363 -- once per TyCon. See Note [Constructor tag allocation], fixes #14657
3364
3365 tcConDecl :: NewOrData
3366 -> DataDeclInfo
3367 -> KnotTied TyCon -- Representation tycon. Knot-tied!
3368 -> [TyConBinder] -- Binders of representation TyCon
3369 -> TcKind -- Result kind
3370 -> NameEnv ConTag
3371 -> ConDecl GhcRn
3372 -> TcM [DataCon]
3373
3374 tcConDecl new_or_data dd_info rep_tycon tc_bndrs res_kind tag_map
3375 (ConDeclH98 { con_name = lname@(L _ name)
3376 , con_ex_tvs = explicit_tkv_nms
3377 , con_mb_cxt = hs_ctxt
3378 , con_args = hs_args })
3379 = addErrCtxt (dataConCtxt [lname]) $
3380 do { -- NB: the tyvars from the declaration header are in scope
3381
3382 -- Get hold of the existential type variables
3383 -- e.g. data T a = forall k (b::k) f. MkT a (f b)
3384 -- Here tc_bndrs = {a}
3385 -- hs_qvars = HsQTvs { hsq_implicit = {k}
3386 -- , hsq_explicit = {f,b} }
3387
3388 ; traceTc "tcConDecl 1" (vcat [ ppr name, ppr explicit_tkv_nms ])
3389
3390 ; (tclvl, wanted, (exp_tvbndrs, (ctxt, arg_tys, field_lbls, stricts)))
3391 <- pushLevelAndSolveEqualitiesX "tcConDecl:H98" $
3392 tcExplicitTKBndrs explicit_tkv_nms $
3393 do { ctxt <- tcHsContext hs_ctxt
3394 ; let exp_kind = getArgExpKind new_or_data res_kind
3395 ; btys <- tcConH98Args exp_kind hs_args
3396 ; field_lbls <- lookupConstructorFields name
3397 ; let (arg_tys, stricts) = unzip btys
3398 ; return (ctxt, arg_tys, field_lbls, stricts)
3399 }
3400
3401
3402 ; let tc_tvs = binderVars tc_bndrs
3403 fake_ty = mkSpecForAllTys tc_tvs $
3404 mkInvisForAllTys exp_tvbndrs $
3405 mkPhiTy ctxt $
3406 mkVisFunTys arg_tys $
3407 unitTy
3408 -- That type is a lie, of course. (It shouldn't end in ()!)
3409 -- And we could construct a proper result type from the info
3410 -- at hand. But the result would mention only the univ_tvs,
3411 -- and so it just creates more work to do it right. Really,
3412 -- we're only doing this to find the right kind variables to
3413 -- quantify over, and this type is fine for that purpose.
3414
3415 -- exp_tvbndrs have explicit, user-written binding sites
3416 -- the kvs below are those kind variables entirely unmentioned by the user
3417 -- and discovered only by generalization
3418
3419 ; kvs <- kindGeneralizeAll fake_ty
3420
3421 ; let skol_tvs = tc_tvs ++ kvs ++ binderVars exp_tvbndrs
3422 ; reportUnsolvedEqualities skol_info skol_tvs tclvl wanted
3423 -- The skol_info claims that all the variables are bound
3424 -- by the data constructor decl, whereas actually the
3425 -- univ_tvs are bound by the data type decl itself. It
3426 -- would be better to have a doubly-nested implication.
3427 -- But that just doesn't seem worth it.
3428 -- See test dependent/should_fail/T13780a
3429
3430 -- Zonk to Types
3431 ; ze <- mkEmptyZonkEnv NoFlexi
3432 ; (ze, qkvs) <- zonkTyBndrsX ze kvs
3433 ; (ze, user_qtvbndrs) <- zonkTyVarBindersX ze exp_tvbndrs
3434 ; arg_tys <- zonkScaledTcTypesToTypesX ze arg_tys
3435 ; ctxt <- zonkTcTypesToTypesX ze ctxt
3436
3437 -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
3438 ; traceTc "tcConDecl 2" (ppr name $$ ppr field_lbls)
3439 ; let univ_tvbs = tyConInvisTVBinders tc_bndrs
3440 ex_tvbs = mkTyVarBinders InferredSpec qkvs ++ user_qtvbndrs
3441 ex_tvs = binderVars ex_tvbs
3442 -- For H98 datatypes, the user-written tyvar binders are precisely
3443 -- the universals followed by the existentials.
3444 -- See Note [DataCon user type variable binders] in GHC.Core.DataCon.
3445 user_tvbs = univ_tvbs ++ ex_tvbs
3446 user_res_ty = mkDDHeaderTy dd_info rep_tycon tc_bndrs
3447
3448 ; traceTc "tcConDecl 2" (ppr name)
3449 ; is_infix <- tcConIsInfixH98 name hs_args
3450 ; rep_nm <- newTyConRepName name
3451 ; fam_envs <- tcGetFamInstEnvs
3452 ; dc <- buildDataCon fam_envs name is_infix rep_nm
3453 stricts Nothing field_lbls
3454 tc_tvs ex_tvs user_tvbs
3455 [{- no eq_preds -}] ctxt arg_tys
3456 user_res_ty rep_tycon tag_map
3457 -- NB: we put data_tc, the type constructor gotten from the
3458 -- constructor type signature into the data constructor;
3459 -- that way checkValidDataCon can complain if it's wrong.
3460
3461 ; return [dc] }
3462 where
3463 skol_info = DataConSkol name
3464
3465 tcConDecl new_or_data dd_info rep_tycon tc_bndrs _res_kind tag_map
3466 -- NB: don't use res_kind here, as it's ill-scoped. Instead,
3467 -- we get the res_kind by typechecking the result type.
3468 (ConDeclGADT { con_names = names
3469 , con_bndrs = L _ outer_hs_bndrs
3470 , con_mb_cxt = cxt, con_g_args = hs_args
3471 , con_res_ty = hs_res_ty })
3472 = addErrCtxt (dataConCtxt names) $
3473 do { traceTc "tcConDecl 1 gadt" (ppr names)
3474 ; let (L _ name : _) = names
3475
3476 ; (tclvl, wanted, (outer_bndrs, (ctxt, arg_tys, res_ty, field_lbls, stricts)))
3477 <- pushLevelAndSolveEqualitiesX "tcConDecl:GADT" $
3478 tcOuterTKBndrs skol_info outer_hs_bndrs $
3479 do { ctxt <- tcHsContext cxt
3480 ; (res_ty, res_kind) <- tcInferLHsTypeKind hs_res_ty
3481 -- See Note [GADT return kinds]
3482
3483 -- For data instances (only), ensure that the return type,
3484 -- res_ty, is a substitution instance of the header.
3485 -- See Note [GADT return types]
3486 ; case dd_info of
3487 DDataType -> return ()
3488 DDataInstance hdr_ty ->
3489 do { (subst, _meta_tvs) <- newMetaTyVars (binderVars tc_bndrs)
3490 ; let head_shape = substTy subst hdr_ty
3491 ; discardResult $
3492 popErrCtxt $ -- Drop dataConCtxt
3493 addErrCtxt (dataConResCtxt names) $
3494 unifyType Nothing res_ty head_shape }
3495
3496 -- See Note [Datatype return kinds]
3497 ; let exp_kind = getArgExpKind new_or_data res_kind
3498 ; btys <- tcConGADTArgs exp_kind hs_args
3499
3500 ; let (arg_tys, stricts) = unzip btys
3501 ; field_lbls <- lookupConstructorFields name
3502 ; return (ctxt, arg_tys, res_ty, field_lbls, stricts)
3503 }
3504
3505 ; outer_tv_bndrs <- scopedSortOuter outer_bndrs
3506
3507 ; tkvs <- kindGeneralizeAll (mkInvisForAllTys outer_tv_bndrs $
3508 mkPhiTy ctxt $
3509 mkVisFunTys arg_tys $
3510 res_ty)
3511 ; traceTc "tcConDecl:GADT" (ppr names $$ ppr res_ty $$ ppr tkvs)
3512 ; reportUnsolvedEqualities skol_info tkvs tclvl wanted
3513
3514 ; let tvbndrs = mkTyVarBinders InferredSpec tkvs ++ outer_tv_bndrs
3515
3516 -- Zonk to Types
3517 ; ze <- mkEmptyZonkEnv NoFlexi
3518 ; (ze, tvbndrs) <- zonkTyVarBindersX ze tvbndrs
3519 ; arg_tys <- zonkScaledTcTypesToTypesX ze arg_tys
3520 ; ctxt <- zonkTcTypesToTypesX ze ctxt
3521 ; res_ty <- zonkTcTypeToTypeX ze res_ty
3522
3523 ; let res_tmpl = mkDDHeaderTy dd_info rep_tycon tc_bndrs
3524 (univ_tvs, ex_tvs, tvbndrs', eq_preds, arg_subst)
3525 = rejigConRes tc_bndrs res_tmpl tvbndrs res_ty
3526 -- See Note [rejigConRes]
3527
3528 ctxt' = substTys arg_subst ctxt
3529 arg_tys' = substScaledTys arg_subst arg_tys
3530 res_ty' = substTy arg_subst res_ty
3531
3532 -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
3533 ; traceTc "tcConDecl 2" (ppr names $$ ppr field_lbls)
3534 ; fam_envs <- tcGetFamInstEnvs
3535 ; let
3536 buildOneDataCon (L _ name) = do
3537 { is_infix <- tcConIsInfixGADT name hs_args
3538 ; rep_nm <- newTyConRepName name
3539
3540 ; buildDataCon fam_envs name is_infix
3541 rep_nm
3542 stricts Nothing field_lbls
3543 univ_tvs ex_tvs tvbndrs' eq_preds
3544 ctxt' arg_tys' res_ty' rep_tycon tag_map
3545 -- NB: we put data_tc, the type constructor gotten from the
3546 -- constructor type signature into the data constructor;
3547 -- that way checkValidDataCon can complain if it's wrong.
3548 }
3549 ; mapM buildOneDataCon names }
3550 where
3551 skol_info = DataConSkol (unLoc (head names))
3552
3553 {- Note [GADT return types]
3554 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
3555 Consider
3556 data family T :: forall k. k -> Type
3557 data instance T (a :: Type) where
3558 MkT :: forall b. T b
3559
3560 What kind does `b` have in the signature for MkT?
3561 Since the return type must be an instance of the type in the header,
3562 we must have (b :: Type), but you can't tell that by looking only at
3563 the type of the data constructor; you have to look at the header too.
3564 If you wrote it out fully, it'd look like
3565 data instance T @Type (a :: Type) where
3566 MkT :: forall (b::Type). T @Type b
3567
3568 We could reject the program, and expect the user to add kind
3569 annotations to `MkT` to restrict the signature. But an easy and
3570 helpful alternative is this: simply instantiate the type from the
3571 header with fresh unification variables, and unify with the return
3572 type of `MkT`. That will force `b` to have kind `Type`. See #8707
3573 and #14111.
3574
3575 Wrikles
3576 * At first sight it looks as though this would completely subsume the
3577 return-type check in checkValidDataCon. But it does not. Suppose we
3578 have
3579 data instance T [a] where
3580 MkT :: T (F (Maybe a))
3581
3582 where F is a type function. Then maybe (F (Maybe a)) evaluates to
3583 [a], so unifyType will succeed. But we discard the coercion
3584 returned by unifyType; and we really don't want to accept this
3585 program. The check in checkValidDataCon will, however, reject it.
3586 TL;DR: keep the check in checkValidDataCon.
3587
3588 * Consider a data type, rather than a data instance, declaration
3589 data S a where { MkS :: b -> S [b] }
3590 In tcConDecl, S is knot-tied, so we don't want to unify (S alpha)
3591 with (S [b]). To put it another way, unifyType should never see a
3592 TcTycon. Simple solution: do *not* do the extra unifyType for
3593 data types (DDataType) only for data instances (DDataInstance); in
3594 the latter the family constructor is not knot-tied so there is no
3595 problem.
3596
3597 * Consider this (from an earlier form of GHC itself):
3598
3599 data Pass = Parsed | ...
3600 data GhcPass (c :: Pass) where
3601 GhcPs :: GhcPs
3602 ...
3603 type GhcPs = GhcPass 'Parsed
3604
3605 Now GhcPs and GhcPass are mutually recursive. If we did unifyType
3606 for datatypes like GhcPass, we would not be able to expand the type
3607 synonym (it'd still be a TcTyCon). So again, we don't do unifyType
3608 for data types; we leave it to checkValidDataCon.
3609
3610 We /do/ perform the unifyType for data /instances/, but a data
3611 instance doesn't declare a new (user-visible) type constructor, so
3612 there is no mutual recursion with type synonyms to worry about.
3613 All good.
3614
3615 TL;DR we do support mutual recursion between type synonyms and
3616 data type/instance declarations, as above.
3617
3618 Note [GADT return kinds]
3619 ~~~~~~~~~~~~~~~~~~~~~~~~
3620 Consider
3621 type family Star where Star = Type
3622 data T :: Type where
3623 MkT :: Int -> T
3624
3625 If, for some stupid reason, tcInferLHsTypeKind on the return type of
3626 MkT returned (T |> ax, Star), then the return-type check in
3627 checkValidDataCon would reject the decl (although of course there is
3628 nothing wrong with it). We are implicitly requiring tha
3629 tcInferLHsTypeKind doesn't any gratuitous top-level casts.
3630 -}
3631
3632 -- | Produce an "expected kind" for the arguments of a data/newtype.
3633 -- If the declaration is indeed for a newtype,
3634 -- then this expected kind will be the kind provided. Otherwise,
3635 -- it is OpenKind for datatypes and liftedTypeKind.
3636 -- Why do we not check for -XUnliftedNewtypes? See point <Error Messages>
3637 -- in Note [Implementation of UnliftedNewtypes]
3638 getArgExpKind :: NewOrData -> Kind -> ContextKind
3639 getArgExpKind NewType res_ki = TheKind res_ki
3640 getArgExpKind DataType _ = OpenKind
3641
3642 tcConIsInfixH98 :: Name
3643 -> HsConDeclH98Details GhcRn
3644 -> TcM Bool
3645 tcConIsInfixH98 _ details
3646 = case details of
3647 InfixCon{} -> return True
3648 RecCon{} -> return False
3649 PrefixCon{} -> return False
3650
3651 tcConIsInfixGADT :: Name
3652 -> HsConDeclGADTDetails GhcRn
3653 -> TcM Bool
3654 tcConIsInfixGADT con details
3655 = case details of
3656 RecConGADT{} -> return False
3657 PrefixConGADT arg_tys -- See Note [Infix GADT constructors]
3658 | isSymOcc (getOccName con)
3659 , [_ty1,_ty2] <- map hsScaledThing arg_tys
3660 -> do { fix_env <- getFixityEnv
3661 ; return (con `elemNameEnv` fix_env) }
3662 | otherwise -> return False
3663
3664 tcConH98Args :: ContextKind -- expected kind of arguments
3665 -- always OpenKind for datatypes, but unlifted newtypes
3666 -- might have a specific kind
3667 -> HsConDeclH98Details GhcRn
3668 -> TcM [(Scaled TcType, HsSrcBang)]
3669 tcConH98Args exp_kind (PrefixCon _ btys)
3670 = mapM (tcConArg exp_kind) btys
3671 tcConH98Args exp_kind (InfixCon bty1 bty2)
3672 = do { bty1' <- tcConArg exp_kind bty1
3673 ; bty2' <- tcConArg exp_kind bty2
3674 ; return [bty1', bty2'] }
3675 tcConH98Args exp_kind (RecCon fields)
3676 = tcRecConDeclFields exp_kind fields
3677
3678 tcConGADTArgs :: ContextKind -- expected kind of arguments
3679 -- always OpenKind for datatypes, but unlifted newtypes
3680 -- might have a specific kind
3681 -> HsConDeclGADTDetails GhcRn
3682 -> TcM [(Scaled TcType, HsSrcBang)]
3683 tcConGADTArgs exp_kind (PrefixConGADT btys)
3684 = mapM (tcConArg exp_kind) btys
3685 tcConGADTArgs exp_kind (RecConGADT fields _)
3686 = tcRecConDeclFields exp_kind fields
3687
3688 tcConArg :: ContextKind -- expected kind for args; always OpenKind for datatypes,
3689 -- but might be an unlifted type with UnliftedNewtypes
3690 -> HsScaled GhcRn (LHsType GhcRn) -> TcM (Scaled TcType, HsSrcBang)
3691 tcConArg exp_kind (HsScaled w bty)
3692 = do { traceTc "tcConArg 1" (ppr bty)
3693 ; arg_ty <- tcCheckLHsType (getBangType bty) exp_kind
3694 ; w' <- tcDataConMult w
3695 ; traceTc "tcConArg 2" (ppr bty)
3696 ; return (Scaled w' arg_ty, getBangStrictness bty) }
3697
3698 tcRecConDeclFields :: ContextKind
3699 -> LocatedL [LConDeclField GhcRn]
3700 -> TcM [(Scaled TcType, HsSrcBang)]
3701 tcRecConDeclFields exp_kind fields
3702 = mapM (tcConArg exp_kind) btys
3703 where
3704 -- We need a one-to-one mapping from field_names to btys
3705 combined = map (\(L _ f) -> (cd_fld_names f,hsLinear (cd_fld_type f)))
3706 (unLoc fields)
3707 explode (ns,ty) = zip ns (repeat ty)
3708 exploded = concatMap explode combined
3709 (_,btys) = unzip exploded
3710
3711 tcDataConMult :: HsArrow GhcRn -> TcM Mult
3712 tcDataConMult arr@(HsUnrestrictedArrow _) = do
3713 -- See Note [Function arrows in GADT constructors]
3714 linearEnabled <- xoptM LangExt.LinearTypes
3715 if linearEnabled then tcMult arr else return oneDataConTy
3716 tcDataConMult arr = tcMult arr
3717
3718 {-
3719 Note [Function arrows in GADT constructors]
3720 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3721 In the absence of -XLinearTypes, we always interpret function arrows
3722 in GADT constructor types as linear, even if the user wrote an
3723 unrestricted arrow. See the "Without -XLinearTypes" section of the
3724 linear types GHC proposal (#111). We opt to do this in the
3725 typechecker, and not in an earlier pass, to ensure that the AST
3726 matches what the user wrote (#18791).
3727
3728 Note [Infix GADT constructors]
3729 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3730 We do not currently have syntax to declare an infix constructor in GADT syntax,
3731 but it makes a (small) difference to the Show instance. So as a slightly
3732 ad-hoc solution, we regard a GADT data constructor as infix if
3733 a) it is an operator symbol
3734 b) it has two arguments
3735 c) there is a fixity declaration for it
3736 For example:
3737 infix 6 (:--:)
3738 data T a where
3739 (:--:) :: t1 -> t2 -> T Int
3740
3741
3742 Note [rejigConRes]
3743 ~~~~~~~~~~~~~~~~~~
3744 There is a delicacy around checking the return types of a datacon. The
3745 central problem is dealing with a declaration like
3746
3747 data T a where
3748 MkT :: T a -> Q a
3749
3750 Note that the return type of MkT is totally bogus. When creating the T
3751 tycon, we also need to create the MkT datacon, which must have a "rejigged"
3752 return type. That is, the MkT datacon's type must be transformed to have
3753 a uniform return type with explicit coercions for GADT-like type parameters.
3754 This rejigging is what rejigConRes does. The problem is, though, that checking
3755 that the return type is appropriate is much easier when done over *Type*,
3756 not *HsType*, and doing a call to tcMatchTy will loop because T isn't fully
3757 defined yet.
3758
3759 So, we want to make rejigConRes lazy and then check the validity of
3760 the return type in checkValidDataCon. To do this we /always/ return a
3761 6-tuple from rejigConRes (so that we can compute the return type from it, which
3762 checkValidDataCon needs), but the first three fields may be bogus if
3763 the return type isn't valid (the last equation for rejigConRes).
3764
3765 This is better than an earlier solution which reduced the number of
3766 errors reported in one pass. See #7175, and #10836.
3767 -}
3768
3769 -- Example
3770 -- data instance T (b,c) where
3771 -- TI :: forall e. e -> T (e,e)
3772 --
3773 -- The representation tycon looks like this:
3774 -- data :R7T b c where
3775 -- TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1
3776 -- In this case orig_res_ty = T (e,e)
3777
3778 rejigConRes :: [KnotTied TyConBinder] -- Template for result type; e.g.
3779 -> KnotTied Type -- data instance T [a] b c ...
3780 -- gives template ([a,b,c], T [a] b c)
3781 -> [InvisTVBinder] -- The constructor's type variables (both inferred and user-written)
3782 -> KnotTied Type -- res_ty
3783 -> ([TyVar], -- Universal
3784 [TyVar], -- Existential (distinct OccNames from univs)
3785 [InvisTVBinder], -- The constructor's rejigged, user-written
3786 -- type variables
3787 [EqSpec], -- Equality predicates
3788 TCvSubst) -- Substitution to apply to argument types
3789 -- We don't check that the TyCon given in the ResTy is
3790 -- the same as the parent tycon, because checkValidDataCon will do it
3791 -- NB: All arguments may potentially be knot-tied
3792 rejigConRes tc_tvbndrs res_tmpl dc_tvbndrs res_ty
3793 -- E.g. data T [a] b c where
3794 -- MkT :: forall x y z. T [(x,y)] z z
3795 -- The {a,b,c} are the tc_tvs, and the {x,y,z} are the dc_tvs
3796 -- (NB: unlike the H98 case, the dc_tvs are not all existential)
3797 -- Then we generate
3798 -- Univ tyvars Eq-spec
3799 -- a a~(x,y)
3800 -- b b~z
3801 -- z
3802 -- Existentials are the leftover type vars: [x,y]
3803 -- The user-written type variables are what is listed in the forall:
3804 -- [x, y, z] (all specified). We must rejig these as well.
3805 -- See Note [DataCon user type variable binders] in GHC.Core.DataCon.
3806 -- So we return ( [a,b,z], [x,y]
3807 -- , [], [x,y,z]
3808 -- , [a~(x,y),b~z], <arg-subst> )
3809 | Just subst <- tcMatchTy res_tmpl res_ty
3810 = let (univ_tvs, raw_eqs, kind_subst) = mkGADTVars tc_tvs dc_tvs subst
3811 raw_ex_tvs = dc_tvs `minusList` univ_tvs
3812 (arg_subst, substed_ex_tvs) = substTyVarBndrs kind_subst raw_ex_tvs
3813
3814 -- After rejigging the existential tyvars, the resulting substitution
3815 -- gives us exactly what we need to rejig the user-written tyvars,
3816 -- since the dcUserTyVarBinders invariant guarantees that the
3817 -- substitution has *all* the tyvars in its domain.
3818 -- See Note [DataCon user type variable binders] in GHC.Core.DataCon.
3819 subst_user_tvs = mapVarBndrs (getTyVar "rejigConRes" . substTyVar arg_subst)
3820 substed_tvbndrs = subst_user_tvs dc_tvbndrs
3821
3822 substed_eqs = map (substEqSpec arg_subst) raw_eqs
3823 in
3824 (univ_tvs, substed_ex_tvs, substed_tvbndrs, substed_eqs, arg_subst)
3825
3826 | otherwise
3827 -- If the return type of the data constructor doesn't match the parent
3828 -- type constructor, or the arity is wrong, the tcMatchTy will fail
3829 -- e.g data T a b where
3830 -- T1 :: Maybe a -- Wrong tycon
3831 -- T2 :: T [a] -- Wrong arity
3832 -- We are detect that later, in checkValidDataCon, but meanwhile
3833 -- we must do *something*, not just crash. So we do something simple
3834 -- albeit bogus, relying on checkValidDataCon to check the
3835 -- bad-result-type error before seeing that the other fields look odd
3836 -- See Note [rejigConRes]
3837 = (tc_tvs, dc_tvs `minusList` tc_tvs, dc_tvbndrs, [], emptyTCvSubst)
3838 where
3839 dc_tvs = binderVars dc_tvbndrs
3840 tc_tvs = binderVars tc_tvbndrs
3841
3842 {- Note [mkGADTVars]
3843 ~~~~~~~~~~~~~~~~~~~~
3844 Running example:
3845
3846 data T (k1 :: *) (k2 :: *) (a :: k2) (b :: k2) where
3847 MkT :: forall (x1 : *) (y :: x1) (z :: *).
3848 T x1 * (Proxy (y :: x1), z) z
3849
3850 We need the rejigged type to be
3851
3852 MkT :: forall (x1 :: *) (k2 :: *) (a :: k2) (b :: k2).
3853 forall (y :: x1) (z :: *).
3854 (k2 ~ *, a ~ (Proxy x1 y, z), b ~ z)
3855 => T x1 k2 a b
3856
3857 You might naively expect that z should become a universal tyvar,
3858 not an existential. (After all, x1 becomes a universal tyvar.)
3859 But z has kind * while b has kind k2, so the return type
3860 T x1 k2 a z
3861 is ill-kinded. Another way to say it is this: the universal
3862 tyvars must have exactly the same kinds as the tyConTyVars.
3863
3864 So we need an existential tyvar and a heterogeneous equality
3865 constraint. (The b ~ z is a bit redundant with the k2 ~ * that
3866 comes before in that b ~ z implies k2 ~ *. I'm sure we could do
3867 some analysis that could eliminate k2 ~ *. But we don't do this
3868 yet.)
3869
3870 The data con signature has already been fully kind-checked.
3871 The return type
3872
3873 T x1 * (Proxy (y :: x1), z) z
3874 becomes
3875 qtkvs = [x1 :: *, y :: x1, z :: *]
3876 res_tmpl = T x1 * (Proxy x1 y, z) z
3877
3878 We start off by matching (T k1 k2 a b) with (T x1 * (Proxy x1 y, z) z). We
3879 know this match will succeed because of the validity check (actually done
3880 later, but laziness saves us -- see Note [rejigConRes]).
3881 Thus, we get
3882
3883 subst := { k1 |-> x1, k2 |-> *, a |-> (Proxy x1 y, z), b |-> z }
3884
3885 Now, we need to figure out what the GADT equalities should be. In this case,
3886 we *don't* want (k1 ~ x1) to be a GADT equality: it should just be a
3887 renaming. The others should be GADT equalities. We also need to make
3888 sure that the universally-quantified variables of the datacon match up
3889 with the tyvars of the tycon, as required for Core context well-formedness.
3890 (This last bit is why we have to rejig at all!)
3891
3892 `choose` walks down the tycon tyvars, figuring out what to do with each one.
3893 It carries two substitutions:
3894 - t_sub's domain is *template* or *tycon* tyvars, mapping them to variables
3895 mentioned in the datacon signature.
3896 - r_sub's domain is *result* tyvars, names written by the programmer in
3897 the datacon signature. The final rejigged type will use these names, but
3898 the subst is still needed because sometimes the printed name of these variables
3899 is different. (See choose_tv_name, below.)
3900
3901 Before explaining the details of `choose`, let's just look at its operation
3902 on our example:
3903
3904 choose [] [] {} {} [k1, k2, a, b]
3905 --> -- first branch of `case` statement
3906 choose
3907 univs: [x1 :: *]
3908 eq_spec: []
3909 t_sub: {k1 |-> x1}
3910 r_sub: {x1 |-> x1}
3911 t_tvs: [k2, a, b]
3912 --> -- second branch of `case` statement
3913 choose
3914 univs: [k2 :: *, x1 :: *]
3915 eq_spec: [k2 ~ *]
3916 t_sub: {k1 |-> x1, k2 |-> k2}
3917 r_sub: {x1 |-> x1}
3918 t_tvs: [a, b]
3919 --> -- second branch of `case` statement
3920 choose
3921 univs: [a :: k2, k2 :: *, x1 :: *]
3922 eq_spec: [ a ~ (Proxy x1 y, z)
3923 , k2 ~ * ]
3924 t_sub: {k1 |-> x1, k2 |-> k2, a |-> a}
3925 r_sub: {x1 |-> x1}
3926 t_tvs: [b]
3927 --> -- second branch of `case` statement
3928 choose
3929 univs: [b :: k2, a :: k2, k2 :: *, x1 :: *]
3930 eq_spec: [ b ~ z
3931 , a ~ (Proxy x1 y, z)
3932 , k2 ~ * ]
3933 t_sub: {k1 |-> x1, k2 |-> k2, a |-> a, b |-> z}
3934 r_sub: {x1 |-> x1}
3935 t_tvs: []
3936 --> -- end of recursion
3937 ( [x1 :: *, k2 :: *, a :: k2, b :: k2]
3938 , [k2 ~ *, a ~ (Proxy x1 y, z), b ~ z]
3939 , {x1 |-> x1} )
3940
3941 `choose` looks up each tycon tyvar in the matching (it *must* be matched!).
3942
3943 * If it finds a bare result tyvar (the first branch of the `case`
3944 statement), it checks to make sure that the result tyvar isn't yet
3945 in the list of univ_tvs. If it is in that list, then we have a
3946 repeated variable in the return type, and we in fact need a GADT
3947 equality.
3948
3949 * It then checks to make sure that the kind of the result tyvar
3950 matches the kind of the template tyvar. This check is what forces
3951 `z` to be existential, as it should be, explained above.
3952
3953 * Assuming no repeated variables or kind-changing, we wish to use the
3954 variable name given in the datacon signature (that is, `x1` not
3955 `k1`), not the tycon signature (which may have been made up by
3956 GHC). So, we add a mapping from the tycon tyvar to the result tyvar
3957 to t_sub.
3958
3959 * If we discover that a mapping in `subst` gives us a non-tyvar (the
3960 second branch of the `case` statement), then we have a GADT equality
3961 to create. We create a fresh equality, but we don't extend any
3962 substitutions. The template variable substitution is meant for use
3963 in universal tyvar kinds, and these shouldn't be affected by any
3964 GADT equalities.
3965
3966 This whole algorithm is quite delicate, indeed. I (Richard E.) see two ways
3967 of simplifying it:
3968
3969 1) The first branch of the `case` statement is really an optimization, used
3970 in order to get fewer GADT equalities. It might be possible to make a GADT
3971 equality for *every* univ. tyvar, even if the equality is trivial, and then
3972 either deal with the bigger type or somehow reduce it later.
3973
3974 2) This algorithm strives to use the names for type variables as specified
3975 by the user in the datacon signature. If we always used the tycon tyvar
3976 names, for example, this would be simplified. This change would almost
3977 certainly degrade error messages a bit, though.
3978 -}
3979
3980 -- ^ From information about a source datacon definition, extract out
3981 -- what the universal variables and the GADT equalities should be.
3982 -- See Note [mkGADTVars].
3983 mkGADTVars :: [TyVar] -- ^ The tycon vars
3984 -> [TyVar] -- ^ The datacon vars
3985 -> TCvSubst -- ^ The matching between the template result type
3986 -- and the actual result type
3987 -> ( [TyVar]
3988 , [EqSpec]
3989 , TCvSubst ) -- ^ The univ. variables, the GADT equalities,
3990 -- and a subst to apply to the GADT equalities
3991 -- and existentials.
3992 mkGADTVars tmpl_tvs dc_tvs subst
3993 = choose [] [] empty_subst empty_subst tmpl_tvs
3994 where
3995 in_scope = mkInScopeSet (mkVarSet tmpl_tvs `unionVarSet` mkVarSet dc_tvs)
3996 `unionInScope` getTCvInScope subst
3997 empty_subst = mkEmptyTCvSubst in_scope
3998
3999 choose :: [TyVar] -- accumulator of univ tvs, reversed
4000 -> [EqSpec] -- accumulator of GADT equalities, reversed
4001 -> TCvSubst -- template substitution
4002 -> TCvSubst -- res. substitution
4003 -> [TyVar] -- template tvs (the univ tvs passed in)
4004 -> ( [TyVar] -- the univ_tvs
4005 , [EqSpec] -- GADT equalities
4006 , TCvSubst ) -- a substitution to fix kinds in ex_tvs
4007
4008 choose univs eqs _t_sub r_sub []
4009 = (reverse univs, reverse eqs, r_sub)
4010 choose univs eqs t_sub r_sub (t_tv:t_tvs)
4011 | Just r_ty <- lookupTyVar subst t_tv
4012 = case getTyVar_maybe r_ty of
4013 Just r_tv
4014 | not (r_tv `elem` univs)
4015 , tyVarKind r_tv `eqType` (substTy t_sub (tyVarKind t_tv))
4016 -> -- simple, well-kinded variable substitution.
4017 choose (r_tv:univs) eqs
4018 (extendTvSubst t_sub t_tv r_ty')
4019 (extendTvSubst r_sub r_tv r_ty')
4020 t_tvs
4021 where
4022 r_tv1 = setTyVarName r_tv (choose_tv_name r_tv t_tv)
4023 r_ty' = mkTyVarTy r_tv1
4024
4025 -- Not a simple substitution: make an equality predicate
4026 _ -> choose (t_tv':univs) (mkEqSpec t_tv' r_ty : eqs)
4027 (extendTvSubst t_sub t_tv (mkTyVarTy t_tv'))
4028 -- We've updated the kind of t_tv,
4029 -- so add it to t_sub (#14162)
4030 r_sub t_tvs
4031 where
4032 t_tv' = updateTyVarKind (substTy t_sub) t_tv
4033
4034 | otherwise
4035 = pprPanic "mkGADTVars" (ppr tmpl_tvs $$ ppr subst)
4036
4037 -- choose an appropriate name for a univ tyvar.
4038 -- This *must* preserve the Unique of the result tv, so that we
4039 -- can detect repeated variables. It prefers user-specified names
4040 -- over system names. A result variable with a system name can
4041 -- happen with GHC-generated implicit kind variables.
4042 choose_tv_name :: TyVar -> TyVar -> Name
4043 choose_tv_name r_tv t_tv
4044 | isSystemName r_tv_name
4045 = setNameUnique t_tv_name (getUnique r_tv_name)
4046
4047 | otherwise
4048 = r_tv_name
4049
4050 where
4051 r_tv_name = getName r_tv
4052 t_tv_name = getName t_tv
4053
4054 {-
4055 Note [Substitution in template variables kinds]
4056 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4057
4058 data G (a :: Maybe k) where
4059 MkG :: G Nothing
4060
4061 With explicit kind variables
4062
4063 data G k (a :: Maybe k) where
4064 MkG :: G k1 (Nothing k1)
4065
4066 Note how k1 is distinct from k. So, when we match the template
4067 `G k a` against `G k1 (Nothing k1)`, we get a subst
4068 [ k |-> k1, a |-> Nothing k1 ]. Even though this subst has two
4069 mappings, we surely don't want to add (k, k1) to the list of
4070 GADT equalities -- that would be overly complex and would create
4071 more untouchable variables than we need. So, when figuring out
4072 which tyvars are GADT-like and which aren't (the fundamental
4073 job of `choose`), we want to treat `k` as *not* GADT-like.
4074 Instead, we wish to substitute in `a`'s kind, to get (a :: Maybe k1)
4075 instead of (a :: Maybe k). This is the reason for dealing
4076 with a substitution in here.
4077
4078 However, we do not *always* want to substitute. Consider
4079
4080 data H (a :: k) where
4081 MkH :: H Int
4082
4083 With explicit kind variables:
4084
4085 data H k (a :: k) where
4086 MkH :: H * Int
4087
4088 Here, we have a kind-indexed GADT. The subst in question is
4089 [ k |-> *, a |-> Int ]. Now, we *don't* want to substitute in `a`'s
4090 kind, because that would give a constructor with the type
4091
4092 MkH :: forall (k :: *) (a :: *). (k ~ *) -> (a ~ Int) -> H k a
4093
4094 The problem here is that a's kind is wrong -- it needs to be k, not *!
4095 So, if the matching for a variable is anything but another bare variable,
4096 we drop the mapping from the substitution before proceeding. This
4097 was not an issue before kind-indexed GADTs because this case could
4098 never happen.
4099
4100 ************************************************************************
4101 * *
4102 Validity checking
4103 * *
4104 ************************************************************************
4105
4106 Validity checking is done once the mutually-recursive knot has been
4107 tied, so we can look at things freely.
4108 -}
4109
4110 checkValidTyCl :: TyCon -> TcM [TyCon]
4111 -- The returned list is either a singleton (if valid)
4112 -- or a list of "fake tycons" (if not); the fake tycons
4113 -- include any implicits, like promoted data constructors
4114 -- See Note [Recover from validity error]
4115 checkValidTyCl tc
4116 = setSrcSpan (getSrcSpan tc) $
4117 addTyConCtxt tc $
4118 recoverM recovery_code $
4119 do { traceTc "Starting validity for tycon" (ppr tc)
4120 ; checkValidTyCon tc
4121 ; traceTc "Done validity for tycon" (ppr tc)
4122 ; return [tc] }
4123 where
4124 recovery_code -- See Note [Recover from validity error]
4125 = do { traceTc "Aborted validity for tycon" (ppr tc)
4126 ; return (map mk_fake_tc $
4127 tc : child_tycons tc) }
4128
4129 mk_fake_tc tc
4130 | isClassTyCon tc = tc -- Ugh! Note [Recover from validity error]
4131 | otherwise = makeRecoveryTyCon tc
4132
4133 child_tycons tc = tyConATs tc ++ map promoteDataCon (tyConDataCons tc)
4134
4135 {- Note [Recover from validity error]
4136 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4137 We recover from a validity error in a type or class, which allows us
4138 to report multiple validity errors. In the failure case we return a
4139 TyCon of the right kind, but with no interesting behaviour
4140 (makeRecoveryTyCon). Why? Suppose we have
4141 type T a = Fun
4142 where Fun is a type family of arity 1. The RHS is invalid, but we
4143 want to go on checking validity of subsequent type declarations.
4144 So we replace T with an abstract TyCon which will do no harm.
4145 See indexed-types/should_fail/BadSock and #10896
4146
4147 Some notes:
4148
4149 * We must make fakes for promoted DataCons too. Consider (#15215)
4150 data T a = MkT ...
4151 data S a = ...T...MkT....
4152 If there is an error in the definition of 'T' we add a "fake type
4153 constructor" to the type environment, so that we can continue to
4154 typecheck 'S'. But we /were not/ adding a fake anything for 'MkT'
4155 and so there was an internal error when we met 'MkT' in the body of
4156 'S'.
4157
4158 Similarly for associated types.
4159
4160 * Painfully, we *don't* want to do this for classes.
4161 Consider tcfail041:
4162 class (?x::Int) => C a where ...
4163 instance C Int
4164 The class is invalid because of the superclass constraint. But
4165 we still want it to look like a /class/, else the instance bleats
4166 that the instance is mal-formed because it hasn't got a class in
4167 the head.
4168
4169 This is really bogus; now we have in scope a Class that is invalid
4170 in some way, with unknown downstream consequences. A better
4171 alternative might be to make a fake class TyCon. A job for another day.
4172
4173 * Previously, we used implicitTyConThings to snaffle out the parts
4174 to add to the context. The problem is that this also grabs data con
4175 wrapper Ids. These could be filtered out. But, painfully, getting
4176 the wrapper Ids checks the DataConRep, and forcing the DataConRep
4177 can panic if there is a representation-polymorphic argument. This is #18534.
4178 We don't need the wrapper Ids here anyway. So the code just takes what
4179 it needs, via child_tycons.
4180 -}
4181
4182 -------------------------
4183 -- For data types declared with record syntax, we require
4184 -- that each constructor that has a field 'f'
4185 -- (a) has the same result type
4186 -- (b) has the same type for 'f'
4187 -- module alpha conversion of the quantified type variables
4188 -- of the constructor.
4189 --
4190 -- Note that we allow existentials to match because the
4191 -- fields can never meet. E.g
4192 -- data T where
4193 -- T1 { f1 :: b, f2 :: a, f3 ::Int } :: T
4194 -- T2 { f1 :: c, f2 :: c, f3 ::Int } :: T
4195 -- Here we do not complain about f1,f2 because they are existential
4196
4197 checkValidTyCon :: TyCon -> TcM ()
4198 checkValidTyCon tc
4199 | isPrimTyCon tc -- Happens when Haddock'ing GHC.Prim
4200 = return ()
4201
4202 | isWiredIn tc -- validity-checking wired-in tycons is a waste of
4203 -- time. More importantly, a wired-in tycon might
4204 -- violate assumptions. Example: (~) has a superclass
4205 -- mentioning (~#), which is ill-kinded in source Haskell
4206 = traceTc "Skipping validity check for wired-in" (ppr tc)
4207
4208 | otherwise
4209 = do { traceTc "checkValidTyCon" (ppr tc $$ ppr (tyConClass_maybe tc))
4210 ; if | Just cl <- tyConClass_maybe tc
4211 -> checkValidClass cl
4212
4213 | Just syn_rhs <- synTyConRhs_maybe tc
4214 -> do { checkValidType syn_ctxt syn_rhs
4215 ; checkTySynRhs syn_ctxt syn_rhs }
4216
4217 | Just fam_flav <- famTyConFlav_maybe tc
4218 -> case fam_flav of
4219 { ClosedSynFamilyTyCon (Just ax)
4220 -> tcAddClosedTypeFamilyDeclCtxt tc $
4221 checkValidCoAxiom ax
4222 ; ClosedSynFamilyTyCon Nothing -> return ()
4223 ; AbstractClosedSynFamilyTyCon ->
4224 do { hsBoot <- tcIsHsBootOrSig
4225 ; checkTc hsBoot $ TcRnUnknownMessage $ mkPlainError noHints $
4226 text "You may define an abstract closed type family" $$
4227 text "only in a .hs-boot file" }
4228 ; DataFamilyTyCon {} -> return ()
4229 ; OpenSynFamilyTyCon -> return ()
4230 ; BuiltInSynFamTyCon _ -> return () }
4231
4232 | otherwise -> do
4233 { -- Check the context on the data decl
4234 traceTc "cvtc1" (ppr tc)
4235 ; checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc)
4236
4237 ; traceTc "cvtc2" (ppr tc)
4238
4239 ; dflags <- getDynFlags
4240 ; existential_ok <- xoptM LangExt.ExistentialQuantification
4241 ; gadt_ok <- xoptM LangExt.GADTs
4242 ; let ex_ok = existential_ok || gadt_ok
4243 -- Data cons can have existential context
4244 ; mapM_ (checkValidDataCon dflags ex_ok tc) data_cons
4245 ; mapM_ (checkPartialRecordField data_cons) (tyConFieldLabels tc)
4246
4247 -- Check that fields with the same name share a type
4248 ; mapM_ check_fields groups }}
4249 where
4250 syn_ctxt = TySynCtxt name
4251 name = tyConName tc
4252 data_cons = tyConDataCons tc
4253
4254 groups = equivClasses cmp_fld (concatMap get_fields data_cons)
4255 -- This spot seems OK with non-determinism. cmp_fld is used only in equivClasses
4256 -- which produces equivalence classes.
4257 -- The order of these equivalence classes might conceivably (non-deterministically)
4258 -- depend on the result of this comparison, but that just affects the order in which
4259 -- fields are checked for compatibility. It will not affect the compiled binary.
4260 cmp_fld (f1,_) (f2,_) = flLabel f1 `uniqCompareFS` flLabel f2
4261 get_fields con = dataConFieldLabels con `zip` repeat con
4262 -- dataConFieldLabels may return the empty list, which is fine
4263
4264 -- See Note [GADT record selectors] in GHC.Tc.TyCl.Utils
4265 -- We must check (a) that the named field has the same
4266 -- type in each constructor
4267 -- (b) that those constructors have the same result type
4268 --
4269 -- However, the constructors may have differently named type variable
4270 -- and (worse) we don't know how the correspond to each other. E.g.
4271 -- C1 :: forall a b. { f :: a, g :: b } -> T a b
4272 -- C2 :: forall d c. { f :: c, g :: c } -> T c d
4273 --
4274 -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
4275 -- result type against other candidates' types BOTH WAYS ROUND.
4276 -- If they magically agrees, take the substitution and
4277 -- apply them to the latter ones, and see if they match perfectly.
4278 check_fields ((label, con1) :| other_fields)
4279 -- These fields all have the same name, but are from
4280 -- different constructors in the data type
4281 = recoverM (return ()) $ mapM_ checkOne other_fields
4282 -- Check that all the fields in the group have the same type
4283 -- NB: this check assumes that all the constructors of a given
4284 -- data type use the same type variables
4285 where
4286 res1 = dataConOrigResTy con1
4287 fty1 = dataConFieldType con1 lbl
4288 lbl = flLabel label
4289
4290 checkOne (_, con2) -- Do it both ways to ensure they are structurally identical
4291 = do { checkFieldCompat lbl con1 con2 res1 res2 fty1 fty2
4292 ; checkFieldCompat lbl con2 con1 res2 res1 fty2 fty1 }
4293 where
4294 res2 = dataConOrigResTy con2
4295 fty2 = dataConFieldType con2 lbl
4296
4297 checkPartialRecordField :: [DataCon] -> FieldLabel -> TcM ()
4298 -- Checks the partial record field selector, and warns.
4299 -- See Note [Checking partial record field]
4300 checkPartialRecordField all_cons fld
4301 = setSrcSpan loc $
4302 warnIf (not is_exhaustive && not (startsWithUnderscore occ_name))
4303 (TcRnUnknownMessage $ mkPlainDiagnostic (WarningWithFlag Opt_WarnPartialFields) noHints $
4304 sep [text "Use of partial record field selector" <> colon,
4305 nest 2 $ quotes (ppr occ_name)])
4306 where
4307 loc = getSrcSpan (flSelector fld)
4308 occ_name = occName fld
4309
4310 (cons_with_field, cons_without_field) = partition has_field all_cons
4311 has_field con = fld `elem` (dataConFieldLabels con)
4312 is_exhaustive = all (dataConCannotMatch inst_tys) cons_without_field
4313
4314 con1 = assert (not (null cons_with_field)) $ head cons_with_field
4315 (univ_tvs, _, eq_spec, _, _, _) = dataConFullSig con1
4316 eq_subst = mkTvSubstPrs (map eqSpecPair eq_spec)
4317 inst_tys = substTyVars eq_subst univ_tvs
4318
4319 checkFieldCompat :: FieldLabelString -> DataCon -> DataCon
4320 -> Type -> Type -> Type -> Type -> TcM ()
4321 checkFieldCompat fld con1 con2 res1 res2 fty1 fty2
4322 = do { checkTc (isJust mb_subst1) (resultTypeMisMatch fld con1 con2)
4323 ; checkTc (isJust mb_subst2) (fieldTypeMisMatch fld con1 con2) }
4324 where
4325 mb_subst1 = tcMatchTy res1 res2
4326 mb_subst2 = tcMatchTyX (expectJust "checkFieldCompat" mb_subst1) fty1 fty2
4327
4328 -------------------------------
4329 checkValidDataCon :: DynFlags -> Bool -> TyCon -> DataCon -> TcM ()
4330 checkValidDataCon dflags existential_ok tc con
4331 = setSrcSpan con_loc $
4332 addErrCtxt (dataConCtxt [L (noAnnSrcSpan con_loc) con_name]) $
4333 do { let tc_tvs = tyConTyVars tc
4334 res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs)
4335 orig_res_ty = dataConOrigResTy con
4336 ; traceTc "checkValidDataCon" (vcat
4337 [ ppr con, ppr tc, ppr tc_tvs
4338 , ppr res_ty_tmpl <+> dcolon <+> ppr (tcTypeKind res_ty_tmpl)
4339 , ppr orig_res_ty <+> dcolon <+> ppr (tcTypeKind orig_res_ty)])
4340
4341
4342 -- Check that the return type of the data constructor
4343 -- matches the type constructor; eg reject this:
4344 -- data T a where { MkT :: Bogus a }
4345 -- It's important to do this first:
4346 -- see Note [rejigCon
4347 -- and c.f. Note [Check role annotations in a second pass]
4348
4349 -- Check that the return type of the data constructor is an instance
4350 -- of the header of the header of data decl. This checks for
4351 -- data T a where { MkT :: S a }
4352 -- data instance D [a] where { MkD :: D (Maybe b) }
4353 -- see Note [GADT return types]
4354 ; checkTc (isJust (tcMatchTyKi res_ty_tmpl orig_res_ty))
4355 (badDataConTyCon con res_ty_tmpl)
4356 -- Note that checkTc aborts if it finds an error. This is
4357 -- critical to avoid panicking when we call dataConDisplayType
4358 -- on an un-rejiggable datacon!
4359 -- Also NB that we match the *kind* as well as the *type* (#18357)
4360 -- However, if the kind is the only thing that doesn't match, the
4361 -- error message is terrible. E.g. test T18357b
4362 -- type family Star where Star = Type
4363 -- newtype T :: Type where MkT :: Int -> (T :: Star)
4364
4365 ; traceTc "checkValidDataCon 2" (ppr data_con_display_type)
4366
4367 -- Check that the result type is a *monotype*
4368 -- e.g. reject this: MkT :: T (forall a. a->a)
4369 -- Reason: it's really the argument of an equality constraint
4370 ; checkValidMonoType orig_res_ty
4371
4372 -- If we are dealing with a newtype, we allow representation
4373 -- polymorphism regardless of whether or not UnliftedNewtypes
4374 -- is enabled. A later check in checkNewDataCon handles this,
4375 -- producing a better error message than checkTypeHasFixedRuntimeRep would.
4376 ; unless (isNewTyCon tc) $
4377 checkNoErrs $
4378 mapM_ (checkTypeHasFixedRuntimeRep FixedRuntimeRepDataConField)
4379 (map scaledThing $ dataConOrigArgTys con)
4380 -- the checkNoErrs is to prevent a panic in isVanillaDataCon
4381 -- (called a a few lines down), which can fall over if there is a
4382 -- bang on a representation-polymorphic argument. This is #18534,
4383 -- typecheck/should_fail/T18534
4384
4385 -- Extra checks for newtype data constructors. Importantly, these
4386 -- checks /must/ come before the call to checkValidType below. This
4387 -- is because checkValidType invokes the constraint solver, and
4388 -- invoking the solver on an ill formed newtype constructor can
4389 -- confuse GHC to the point of panicking. See #17955 for an example.
4390 ; when (isNewTyCon tc) (checkNewDataCon con)
4391
4392 -- Check all argument types for validity
4393 ; checkValidType ctxt data_con_display_type
4394
4395 -- Check that existentials are allowed if they are used
4396 ; checkTc (existential_ok || isVanillaDataCon con)
4397 (badExistential con)
4398
4399 -- Check that UNPACK pragmas and bangs work out
4400 -- E.g. reject data T = MkT {-# UNPACK #-} Int -- No "!"
4401 -- data T = MkT {-# UNPACK #-} !a -- Can't unpack
4402 ; hsc_env <- getTopEnv
4403 ; let check_bang :: Type -> HsSrcBang -> HsImplBang -> Int -> TcM ()
4404 check_bang orig_arg_ty bang rep_bang n
4405 | HsSrcBang _ _ SrcLazy <- bang
4406 , not (xopt LangExt.StrictData dflags)
4407 = addErrTc $ TcRnUnknownMessage $ mkPlainError noHints $
4408 (bad_bang n (text "Lazy annotation (~) without StrictData"))
4409
4410 | HsSrcBang _ want_unpack strict_mark <- bang
4411 , isSrcUnpacked want_unpack, not (is_strict strict_mark)
4412 , not (isUnliftedType orig_arg_ty)
4413 = addDiagnosticTc $ TcRnUnknownMessage $
4414 mkPlainDiagnostic WarningWithoutFlag noHints (bad_bang n (text "UNPACK pragma lacks '!'"))
4415
4416 -- Warn about a redundant ! on an unlifted type
4417 -- e.g. data T = MkT !Int#
4418 | HsSrcBang _ _ SrcStrict <- bang
4419 , isUnliftedType orig_arg_ty
4420 = addDiagnosticTc $ TcRnBangOnUnliftedType orig_arg_ty
4421
4422 | HsSrcBang _ want_unpack _ <- bang
4423 , isSrcUnpacked want_unpack
4424 , case rep_bang of { HsUnpack {} -> False; _ -> True }
4425 -- If not optimising, we don't unpack (rep_bang is never
4426 -- HsUnpack), so don't complain! This happens, e.g., in Haddock.
4427 -- See dataConSrcToImplBang.
4428 , not (gopt Opt_OmitInterfacePragmas dflags)
4429 -- When typechecking an indefinite package in Backpack, we
4430 -- may attempt to UNPACK an abstract type. The test here will
4431 -- conclude that this is unusable, but it might become usable
4432 -- when we actually fill in the abstract type. As such, don't
4433 -- warn in this case (it gives users the wrong idea about whether
4434 -- or not UNPACK on abstract types is supported; it is!)
4435 , isHomeUnitDefinite (hsc_home_unit hsc_env)
4436 = addDiagnosticTc $ TcRnUnknownMessage $
4437 mkPlainDiagnostic WarningWithoutFlag noHints (bad_bang n (text "Ignoring unusable UNPACK pragma"))
4438
4439 | otherwise
4440 = return ()
4441
4442 ; void $ zipWith4M check_bang (map scaledThing $ dataConOrigArgTys con)
4443 (dataConSrcBangs con) (dataConImplBangs con) [1..]
4444
4445 -- Check the dcUserTyVarBinders invariant
4446 -- See Note [DataCon user type variable binders] in GHC.Core.DataCon
4447 -- checked here because we sometimes build invalid DataCons before
4448 -- erroring above here
4449 ; when debugIsOn $
4450 do { let (univs, exs, eq_spec, _, _, _) = dataConFullSig con
4451 user_tvs = dataConUserTyVars con
4452 user_tvbs_invariant
4453 = Set.fromList (filterEqSpec eq_spec univs ++ exs)
4454 == Set.fromList user_tvs
4455 ; massertPpr user_tvbs_invariant
4456 $ vcat ([ ppr con
4457 , ppr univs
4458 , ppr exs
4459 , ppr eq_spec
4460 , ppr user_tvs ]) }
4461
4462 ; traceTc "Done validity of data con" $
4463 vcat [ ppr con
4464 , text "Datacon wrapper type:" <+> ppr (dataConWrapperType con)
4465 , text "Datacon rep type:" <+> ppr (dataConRepType con)
4466 , text "Datacon display type:" <+> ppr data_con_display_type
4467 , text "Rep typcon binders:" <+> ppr (tyConBinders (dataConTyCon con))
4468 , case tyConFamInst_maybe (dataConTyCon con) of
4469 Nothing -> text "not family"
4470 Just (f, _) -> ppr (tyConBinders f) ]
4471 }
4472 where
4473 con_name = dataConName con
4474 con_loc = nameSrcSpan con_name
4475 ctxt = ConArgCtxt con_name
4476 is_strict = \case
4477 NoSrcStrict -> xopt LangExt.StrictData dflags
4478 bang -> isSrcStrict bang
4479
4480 bad_bang n herald
4481 = hang herald 2 (text "on the" <+> speakNth n
4482 <+> text "argument of" <+> quotes (ppr con))
4483
4484 show_linear_types = xopt LangExt.LinearTypes dflags
4485 data_con_display_type = dataConDisplayType show_linear_types con
4486
4487 -------------------------------
4488 checkNewDataCon :: DataCon -> TcM ()
4489 -- Further checks for the data constructor of a newtype
4490 checkNewDataCon con
4491 = do { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
4492 -- One argument
4493
4494 ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
4495 ; let allowedArgType =
4496 unlifted_newtypes || isLiftedType_maybe (scaledThing arg_ty1) == Just True
4497 ; checkTc allowedArgType $ TcRnUnknownMessage $ mkPlainError noHints $ vcat
4498 [ text "A newtype cannot have an unlifted argument type"
4499 , text "Perhaps you intended to use UnliftedNewtypes"
4500 ]
4501 ; show_linear_types <- xopt LangExt.LinearTypes <$> getDynFlags
4502
4503 ; let check_con what msg =
4504 checkTc what $ TcRnUnknownMessage $ mkPlainError noHints $
4505 (msg $$ ppr con <+> dcolon <+> ppr (dataConDisplayType show_linear_types con))
4506
4507 ; checkTc (ok_mult (scaledMult arg_ty1)) $
4508 TcRnUnknownMessage $ mkPlainError noHints $ text "A newtype constructor must be linear"
4509
4510 ; check_con (null eq_spec) $
4511 text "A newtype constructor must have a return type of form T a1 ... an"
4512 -- Return type is (T a b c)
4513
4514 ; check_con (null theta) $
4515 text "A newtype constructor cannot have a context in its type"
4516
4517 ; check_con (null ex_tvs) $
4518 text "A newtype constructor cannot have existential type variables"
4519 -- No existentials
4520
4521 ; checkTc (all ok_bang (dataConSrcBangs con))
4522 (newtypeStrictError con)
4523 -- No strictness annotations
4524 }
4525 where
4526 (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
4527 = dataConFullSig con
4528
4529 (arg_ty1 : _) = arg_tys
4530
4531 ok_bang (HsSrcBang _ _ SrcStrict) = False
4532 ok_bang (HsSrcBang _ _ SrcLazy) = False
4533 ok_bang _ = True
4534
4535 ok_mult One = True
4536 ok_mult _ = False
4537
4538 -------------------------------
4539 checkValidClass :: Class -> TcM ()
4540 checkValidClass cls
4541 = do { constrained_class_methods <- xoptM LangExt.ConstrainedClassMethods
4542 ; multi_param_type_classes <- xoptM LangExt.MultiParamTypeClasses
4543 ; nullary_type_classes <- xoptM LangExt.NullaryTypeClasses
4544 ; fundep_classes <- xoptM LangExt.FunctionalDependencies
4545 ; undecidable_super_classes <- xoptM LangExt.UndecidableSuperClasses
4546
4547 -- Check that the class is unary, unless multiparameter type classes
4548 -- are enabled; also recognize deprecated nullary type classes
4549 -- extension (subsumed by multiparameter type classes, #8993)
4550 ; checkTc (multi_param_type_classes || cls_arity == 1 ||
4551 (nullary_type_classes && cls_arity == 0))
4552 (classArityErr cls_arity cls)
4553 ; checkTc (fundep_classes || null fundeps) (classFunDepsErr cls)
4554
4555 -- Check the super-classes
4556 ; checkValidTheta (ClassSCCtxt (className cls)) theta
4557
4558 -- Now check for cyclic superclasses
4559 -- If there are superclass cycles, checkClassCycleErrs bails.
4560 ; unless undecidable_super_classes $
4561 case checkClassCycles cls of
4562 Just err -> setSrcSpan (getSrcSpan cls) $
4563 addErrTc (TcRnUnknownMessage $ mkPlainError noHints err)
4564 Nothing -> return ()
4565
4566 -- Check the class operations.
4567 -- But only if there have been no earlier errors
4568 -- See Note [Abort when superclass cycle is detected]
4569 ; whenNoErrs $
4570 mapM_ (check_op constrained_class_methods) op_stuff
4571
4572 -- Check the associated type defaults are well-formed and instantiated
4573 ; mapM_ check_at at_stuff }
4574 where
4575 (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls
4576 cls_arity = length (tyConVisibleTyVars (classTyCon cls))
4577 -- Ignore invisible variables
4578 cls_tv_set = mkVarSet tyvars
4579
4580 check_op constrained_class_methods (sel_id, dm)
4581 = setSrcSpan (getSrcSpan sel_id) $
4582 addErrCtxt (classOpCtxt sel_id op_ty) $ do
4583 { traceTc "class op type" (ppr op_ty)
4584 ; checkValidType ctxt op_ty
4585 -- This implements the ambiguity check, among other things
4586 -- Example: tc223
4587 -- class Error e => Game b mv e | b -> mv e where
4588 -- newBoard :: MonadState b m => m ()
4589 -- Here, MonadState has a fundep m->b, so newBoard is fine
4590
4591 -- NB: we don't check that the class method is not representation-polymorphic here,
4592 -- as GHC.TcGen.TyCl.tcClassSigType already includes a subtype check that guarantees
4593 -- typeclass methods always have kind 'Type'.
4594 --
4595 -- Test case: rep-poly/RepPolyClassMethod.
4596
4597 ; unless constrained_class_methods $
4598 mapM_ check_constraint (tail (cls_pred:op_theta))
4599
4600 ; check_dm ctxt sel_id cls_pred tau2 dm
4601 }
4602 where
4603 ctxt = FunSigCtxt op_name (WantRRC (getSrcSpan cls)) -- Report redundant class constraints
4604 op_name = idName sel_id
4605 op_ty = idType sel_id
4606 (_,cls_pred,tau1) = tcSplitMethodTy op_ty
4607 -- See Note [Splitting nested sigma types in class type signatures]
4608 (_,op_theta,tau2) = tcSplitNestedSigmaTys tau1
4609
4610 check_constraint :: TcPredType -> TcM ()
4611 check_constraint pred -- See Note [Class method constraints]
4612 = when (not (isEmptyVarSet pred_tvs) &&
4613 pred_tvs `subVarSet` cls_tv_set)
4614 (addErrTc (badMethPred sel_id pred))
4615 where
4616 pred_tvs = tyCoVarsOfType pred
4617
4618 check_at (ATI fam_tc m_dflt_rhs)
4619 = do { checkTc (cls_arity == 0 || any (`elemVarSet` cls_tv_set) fam_tvs)
4620 (noClassTyVarErr cls fam_tc)
4621 -- Check that the associated type mentions at least
4622 -- one of the class type variables
4623 -- The check is disabled for nullary type classes,
4624 -- since there is no possible ambiguity (#10020)
4625
4626 -- Check that any default declarations for associated types are valid
4627 ; whenIsJust m_dflt_rhs $ \ (rhs, at_validity_info) ->
4628 case at_validity_info of
4629 NoATVI -> pure ()
4630 ATVI loc pats ->
4631 setSrcSpan loc $
4632 tcAddFamInstCtxt (text "default type instance") (getName fam_tc) $
4633 do { checkValidAssocTyFamDeflt fam_tc pats
4634 ; checkValidTyFamEqn fam_tc fam_tvs (mkTyVarTys fam_tvs) rhs }}
4635 where
4636 fam_tvs = tyConTyVars fam_tc
4637
4638 check_dm :: UserTypeCtxt -> Id -> PredType -> Type -> DefMethInfo -> TcM ()
4639 -- Check validity of the /top-level/ generic-default type
4640 -- E.g for class C a where
4641 -- default op :: forall b. (a~b) => blah
4642 -- we do not want to do an ambiguity check on a type with
4643 -- a free TyVar 'a' (#11608). See TcType
4644 -- Note [TyVars and TcTyVars during type checking] in GHC.Tc.Utils.TcType
4645 -- Hence the mkDefaultMethodType to close the type.
4646 check_dm ctxt sel_id vanilla_cls_pred vanilla_tau
4647 (Just (dm_name, dm_spec@(GenericDM dm_ty)))
4648 = setSrcSpan (getSrcSpan dm_name) $ do
4649 -- We have carefully set the SrcSpan on the generic
4650 -- default-method Name to be that of the generic
4651 -- default type signature
4652
4653 -- First, we check that the method's default type signature
4654 -- aligns with the non-default type signature.
4655 -- See Note [Default method type signatures must align]
4656 let cls_pred = mkClassPred cls $ mkTyVarTys $ classTyVars cls
4657 -- Note that the second field of this tuple contains the context
4658 -- of the default type signature, making it apparent that we
4659 -- ignore method contexts completely when validity-checking
4660 -- default type signatures. See the end of
4661 -- Note [Default method type signatures must align]
4662 -- to learn why this is OK.
4663 --
4664 -- See also
4665 -- Note [Splitting nested sigma types in class type signatures]
4666 -- for an explanation of why we don't use tcSplitSigmaTy here.
4667 (_, _, dm_tau) = tcSplitNestedSigmaTys dm_ty
4668
4669 -- Given this class definition:
4670 --
4671 -- class C a b where
4672 -- op :: forall p q. (Ord a, D p q)
4673 -- => a -> b -> p -> (a, b)
4674 -- default op :: forall r s. E r
4675 -- => a -> b -> s -> (a, b)
4676 --
4677 -- We want to match up two types of the form:
4678 --
4679 -- Vanilla type sig: C aa bb => aa -> bb -> p -> (aa, bb)
4680 -- Default type sig: C a b => a -> b -> s -> (a, b)
4681 --
4682 -- Notice that the two type signatures can be quantified over
4683 -- different class type variables! Therefore, it's important that
4684 -- we include the class predicate parts to match up a with aa and
4685 -- b with bb.
4686 vanilla_phi_ty = mkPhiTy [vanilla_cls_pred] vanilla_tau
4687 dm_phi_ty = mkPhiTy [cls_pred] dm_tau
4688
4689 traceTc "check_dm" $ vcat
4690 [ text "vanilla_phi_ty" <+> ppr vanilla_phi_ty
4691 , text "dm_phi_ty" <+> ppr dm_phi_ty ]
4692
4693 -- Actually checking that the types align is done with a call to
4694 -- tcMatchTys. We need to get a match in both directions to rule
4695 -- out degenerate cases like these:
4696 --
4697 -- class Foo a where
4698 -- foo1 :: a -> b
4699 -- default foo1 :: a -> Int
4700 --
4701 -- foo2 :: a -> Int
4702 -- default foo2 :: a -> b
4703 unless (isJust $ tcMatchTys [dm_phi_ty, vanilla_phi_ty]
4704 [vanilla_phi_ty, dm_phi_ty]) $ addErrTc $
4705 TcRnUnknownMessage $ mkPlainError noHints $
4706 hang (text "The default type signature for"
4707 <+> ppr sel_id <> colon)
4708 2 (ppr dm_ty)
4709 $$ (text "does not match its corresponding"
4710 <+> text "non-default type signature")
4711
4712 -- Now do an ambiguity check on the default type signature.
4713 checkValidType ctxt (mkDefaultMethodType cls sel_id dm_spec)
4714 check_dm _ _ _ _ _ = return ()
4715
4716 checkFamFlag :: Name -> TcM ()
4717 -- Check that we don't use families without -XTypeFamilies
4718 -- The parser won't even parse them, but I suppose a GHC API
4719 -- client might have a go!
4720 checkFamFlag tc_name
4721 = do { idx_tys <- xoptM LangExt.TypeFamilies
4722 ; checkTc idx_tys err_msg }
4723 where
4724 err_msg :: TcRnMessage
4725 err_msg = TcRnUnknownMessage $ mkPlainError noHints $
4726 hang (text "Illegal family declaration for" <+> quotes (ppr tc_name))
4727 2 (text "Enable TypeFamilies to allow indexed type families")
4728
4729 checkResultSigFlag :: Name -> FamilyResultSig GhcRn -> TcM ()
4730 checkResultSigFlag tc_name (TyVarSig _ tvb)
4731 = do { ty_fam_deps <- xoptM LangExt.TypeFamilyDependencies
4732 ; checkTc ty_fam_deps $ TcRnUnknownMessage $ mkPlainError noHints $
4733 hang (text "Illegal result type variable" <+> ppr tvb <+> text "for" <+> quotes (ppr tc_name))
4734 2 (text "Enable TypeFamilyDependencies to allow result variable names") }
4735 checkResultSigFlag _ _ = return () -- other cases OK
4736
4737 {- Note [Class method constraints]
4738 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4739 Haskell 2010 is supposed to reject
4740 class C a where
4741 op :: Eq a => a -> a
4742 where the method type constrains only the class variable(s). (The extension
4743 -XConstrainedClassMethods switches off this check.) But regardless
4744 we should not reject
4745 class C a where
4746 op :: (?x::Int) => a -> a
4747 as pointed out in #11793. So the test here rejects the program if
4748 * -XConstrainedClassMethods is off
4749 * the tyvars of the constraint are non-empty
4750 * all the tyvars are class tyvars, none are locally quantified
4751
4752 Note [Abort when superclass cycle is detected]
4753 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4754 We must avoid doing the ambiguity check for the methods (in
4755 checkValidClass.check_op) when there are already errors accumulated.
4756 This is because one of the errors may be a superclass cycle, and
4757 superclass cycles cause canonicalization to loop. Here is a
4758 representative example:
4759
4760 class D a => C a where
4761 meth :: D a => ()
4762 class C a => D a
4763
4764 This fixes #9415, #9739
4765
4766 Note [Default method type signatures must align]
4767 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4768 GHC enforces the invariant that a class method's default type signature
4769 must "align" with that of the method's non-default type signature, as per
4770 GHC #12918. For instance, if you have:
4771
4772 class Foo a where
4773 bar :: forall b. Context => a -> b
4774
4775 Then a default type signature for bar must be alpha equivalent to
4776 (forall b. a -> b). That is, the types must be the same modulo differences in
4777 contexts. So the following would be acceptable default type signatures:
4778
4779 default bar :: forall b. Context1 => a -> b
4780 default bar :: forall x. Context2 => a -> x
4781
4782 But the following are NOT acceptable default type signatures:
4783
4784 default bar :: forall b. b -> a
4785 default bar :: forall x. x
4786 default bar :: a -> Int
4787
4788 Note that a is bound by the class declaration for Foo itself, so it is
4789 not allowed to differ in the default type signature.
4790
4791 The default type signature (default bar :: a -> Int) deserves special mention,
4792 since (a -> Int) is a straightforward instantiation of (forall b. a -> b). To
4793 write this, you need to declare the default type signature like so:
4794
4795 default bar :: forall b. (b ~ Int). a -> b
4796
4797 As noted in #12918, there are several reasons to do this:
4798
4799 1. It would make no sense to have a type that was flat-out incompatible with
4800 the non-default type signature. For instance, if you had:
4801
4802 class Foo a where
4803 bar :: a -> Int
4804 default bar :: a -> Bool
4805
4806 Then that would always fail in an instance declaration. So this check
4807 nips such cases in the bud before they have the chance to produce
4808 confusing error messages.
4809
4810 2. Internally, GHC uses TypeApplications to instantiate the default method in
4811 an instance. See Note [Default methods in instances] in GHC.Tc.TyCl.Instance.
4812 Thus, GHC needs to know exactly what the universally quantified type
4813 variables are, and when instantiated that way, the default method's type
4814 must match the expected type.
4815
4816 3. Aesthetically, by only allowing the default type signature to differ in its
4817 context, we are making it more explicit the ways in which the default type
4818 signature is less polymorphic than the non-default type signature.
4819
4820 You might be wondering: why are the contexts allowed to be different, but not
4821 the rest of the type signature? That's because default implementations often
4822 rely on assumptions that the more general, non-default type signatures do not.
4823 For instance, in the Enum class declaration:
4824
4825 class Enum a where
4826 enum :: [a]
4827 default enum :: (Generic a, GEnum (Rep a)) => [a]
4828 enum = map to genum
4829
4830 class GEnum f where
4831 genum :: [f a]
4832
4833 The default implementation for enum only works for types that are instances of
4834 Generic, and for which their generic Rep type is an instance of GEnum. But
4835 clearly enum doesn't _have_ to use this implementation, so naturally, the
4836 context for enum is allowed to be different to accommodate this. As a result,
4837 when we validity-check default type signatures, we ignore contexts completely.
4838
4839 Note that when checking whether two type signatures match, we must take care to
4840 split as many foralls as it takes to retrieve the tau types we which to check.
4841 See Note [Splitting nested sigma types in class type signatures].
4842
4843 Note [Splitting nested sigma types in class type signatures]
4844 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4845 Consider this type synonym and class definition:
4846
4847 type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
4848
4849 class Each s t a b where
4850 each :: Traversal s t a b
4851 default each :: (Traversable g, s ~ g a, t ~ g b) => Traversal s t a b
4852
4853 It might seem obvious that the tau types in both type signatures for `each`
4854 are the same, but actually getting GHC to conclude this is surprisingly tricky.
4855 That is because in general, the form of a class method's non-default type
4856 signature is:
4857
4858 forall a. C a => forall d. D d => E a b
4859
4860 And the general form of a default type signature is:
4861
4862 forall f. F f => E a f -- The variable `a` comes from the class
4863
4864 So it you want to get the tau types in each type signature, you might find it
4865 reasonable to call tcSplitSigmaTy twice on the non-default type signature, and
4866 call it once on the default type signature. For most classes and methods, this
4867 will work, but Each is a bit of an exceptional case. The way `each` is written,
4868 it doesn't quantify any additional type variables besides those of the Each
4869 class itself, so the non-default type signature for `each` is actually this:
4870
4871 forall s t a b. Each s t a b => Traversal s t a b
4872
4873 Notice that there _appears_ to only be one forall. But there's actually another
4874 forall lurking in the Traversal type synonym, so if you call tcSplitSigmaTy
4875 twice, you'll also go under the forall in Traversal! That is, you'll end up
4876 with:
4877
4878 (a -> f b) -> s -> f t
4879
4880 A problem arises because you only call tcSplitSigmaTy once on the default type
4881 signature for `each`, which gives you
4882
4883 Traversal s t a b
4884
4885 Or, equivalently:
4886
4887 forall f. Applicative f => (a -> f b) -> s -> f t
4888
4889 This is _not_ the same thing as (a -> f b) -> s -> f t! So now tcMatchTy will
4890 say that the tau types for `each` are not equal.
4891
4892 A solution to this problem is to use tcSplitNestedSigmaTys instead of
4893 tcSplitSigmaTy. tcSplitNestedSigmaTys will always split any foralls that it
4894 sees until it can't go any further, so if you called it on the default type
4895 signature for `each`, it would return (a -> f b) -> s -> f t like we desired.
4896
4897 Note [Checking partial record field]
4898 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4899 This check checks the partial record field selector, and warns (#7169).
4900
4901 For example:
4902
4903 data T a = A { m1 :: a, m2 :: a } | B { m1 :: a }
4904
4905 The function 'm2' is partial record field, and will fail when it is applied to
4906 'B'. The warning identifies such partial fields. The check is performed at the
4907 declaration of T, not at the call-sites of m2.
4908
4909 The warning can be suppressed by prefixing the field-name with an underscore.
4910 For example:
4911
4912 data T a = A { m1 :: a, _m2 :: a } | B { m1 :: a }
4913
4914 ************************************************************************
4915 * *
4916 Checking role validity
4917 * *
4918 ************************************************************************
4919 -}
4920
4921 checkValidRoleAnnots :: RoleAnnotEnv -> TyCon -> TcM ()
4922 checkValidRoleAnnots role_annots tc
4923 | isTypeSynonymTyCon tc = check_no_roles
4924 | isFamilyTyCon tc = check_no_roles
4925 | isAlgTyCon tc = check_roles
4926 | otherwise = return ()
4927 where
4928 -- Role annotations are given only on *explicit* variables,
4929 -- but a tycon stores roles for all variables.
4930 -- So, we drop the implicit roles (which are all Nominal, anyway).
4931 name = tyConName tc
4932 roles = tyConRoles tc
4933 (vis_roles, vis_vars) = unzip $ mapMaybe pick_vis $
4934 zip roles (tyConBinders tc)
4935 role_annot_decl_maybe = lookupRoleAnnot role_annots name
4936
4937 pick_vis :: (Role, TyConBinder) -> Maybe (Role, TyVar)
4938 pick_vis (role, tvb)
4939 | isVisibleTyConBinder tvb = Just (role, binderVar tvb)
4940 | otherwise = Nothing
4941
4942 check_roles
4943 = whenIsJust role_annot_decl_maybe $
4944 \decl@(L loc (RoleAnnotDecl _ _ the_role_annots)) ->
4945 addRoleAnnotCtxt name $
4946 setSrcSpanA loc $ do
4947 { role_annots_ok <- xoptM LangExt.RoleAnnotations
4948 ; checkTc role_annots_ok $ needXRoleAnnotations tc
4949 ; checkTc (vis_vars `equalLength` the_role_annots)
4950 (wrongNumberOfRoles vis_vars decl)
4951 ; _ <- zipWith3M checkRoleAnnot vis_vars the_role_annots vis_roles
4952 -- Representational or phantom roles for class parameters
4953 -- quickly lead to incoherence. So, we require
4954 -- IncoherentInstances to have them. See #8773, #14292
4955 ; incoherent_roles_ok <- xoptM LangExt.IncoherentInstances
4956 ; checkTc ( incoherent_roles_ok
4957 || (not $ isClassTyCon tc)
4958 || (all (== Nominal) vis_roles))
4959 incoherentRoles
4960
4961 ; lint <- goptM Opt_DoCoreLinting
4962 ; when lint $ checkValidRoles tc }
4963
4964 check_no_roles
4965 = whenIsJust role_annot_decl_maybe illegalRoleAnnotDecl
4966
4967 checkRoleAnnot :: TyVar -> LocatedAn NoEpAnns (Maybe Role) -> Role -> TcM ()
4968 checkRoleAnnot _ (L _ Nothing) _ = return ()
4969 checkRoleAnnot tv (L _ (Just r1)) r2
4970 = when (r1 /= r2) $
4971 addErrTc $ badRoleAnnot (tyVarName tv) r1 r2
4972
4973 -- This is a double-check on the role inference algorithm. It is only run when
4974 -- -dcore-lint is enabled. See Note [Role inference] in GHC.Tc.TyCl.Utils
4975 checkValidRoles :: TyCon -> TcM ()
4976 -- If you edit this function, you may need to update the GHC formalism
4977 -- See Note [GHC Formalism] in GHC.Core.Lint
4978 checkValidRoles tc
4979 | isAlgTyCon tc
4980 -- tyConDataCons returns an empty list for data families
4981 = mapM_ check_dc_roles (tyConDataCons tc)
4982 | Just rhs <- synTyConRhs_maybe tc
4983 = check_ty_roles (zipVarEnv (tyConTyVars tc) (tyConRoles tc)) Representational rhs
4984 | otherwise
4985 = return ()
4986 where
4987 check_dc_roles datacon
4988 = do { traceTc "check_dc_roles" (ppr datacon <+> ppr (tyConRoles tc))
4989 ; mapM_ (check_ty_roles role_env Representational) $
4990 eqSpecPreds eq_spec ++ theta ++ (map scaledThing arg_tys) }
4991 -- See Note [Role-checking data constructor arguments] in GHC.Tc.TyCl.Utils
4992 where
4993 (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
4994 = dataConFullSig datacon
4995 univ_roles = zipVarEnv univ_tvs (tyConRoles tc)
4996 -- zipVarEnv uses zipEqual, but we don't want that for ex_tvs
4997 ex_roles = mkVarEnv (map (, Nominal) ex_tvs)
4998 role_env = univ_roles `plusVarEnv` ex_roles
4999
5000 check_ty_roles env role ty
5001 | Just ty' <- coreView ty -- #14101
5002 = check_ty_roles env role ty'
5003
5004 check_ty_roles env role (TyVarTy tv)
5005 = case lookupVarEnv env tv of
5006 Just role' -> unless (role' `ltRole` role || role' == role) $
5007 report_error $ text "type variable" <+> quotes (ppr tv) <+>
5008 text "cannot have role" <+> ppr role <+>
5009 text "because it was assigned role" <+> ppr role'
5010 Nothing -> report_error $ text "type variable" <+> quotes (ppr tv) <+>
5011 text "missing in environment"
5012
5013 check_ty_roles env Representational (TyConApp tc tys)
5014 = let roles' = tyConRoles tc in
5015 zipWithM_ (maybe_check_ty_roles env) roles' tys
5016
5017 check_ty_roles env Nominal (TyConApp _ tys)
5018 = mapM_ (check_ty_roles env Nominal) tys
5019
5020 check_ty_roles _ Phantom ty@(TyConApp {})
5021 = pprPanic "check_ty_roles" (ppr ty)
5022
5023 check_ty_roles env role (AppTy ty1 ty2)
5024 = check_ty_roles env role ty1
5025 >> check_ty_roles env Nominal ty2
5026
5027 check_ty_roles env role (FunTy _ w ty1 ty2)
5028 = check_ty_roles env Nominal w
5029 >> check_ty_roles env role ty1
5030 >> check_ty_roles env role ty2
5031
5032 check_ty_roles env role (ForAllTy (Bndr tv _) ty)
5033 = check_ty_roles env Nominal (tyVarKind tv)
5034 >> check_ty_roles (extendVarEnv env tv Nominal) role ty
5035
5036 check_ty_roles _ _ (LitTy {}) = return ()
5037
5038 check_ty_roles env role (CastTy t _)
5039 = check_ty_roles env role t
5040
5041 check_ty_roles _ role (CoercionTy co)
5042 = unless (role == Phantom) $
5043 report_error $ text "coercion" <+> ppr co <+> text "has bad role" <+> ppr role
5044
5045 maybe_check_ty_roles env role ty
5046 = when (role == Nominal || role == Representational) $
5047 check_ty_roles env role ty
5048
5049 report_error doc
5050 = addErrTc $ TcRnUnknownMessage $ mkPlainError noHints $
5051 vcat [text "Internal error in role inference:",
5052 doc,
5053 text "Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug"]
5054
5055 {-
5056 ************************************************************************
5057 * *
5058 Error messages
5059 * *
5060 ************************************************************************
5061 -}
5062
5063 tcMkDeclCtxt :: TyClDecl GhcRn -> SDoc
5064 tcMkDeclCtxt decl = hsep [text "In the", pprTyClDeclFlavour decl,
5065 text "declaration for", quotes (ppr (tcdName decl))]
5066
5067 addVDQNote :: TcTyCon -> TcM a -> TcM a
5068 -- See Note [Inferring visible dependent quantification]
5069 -- Only types without a signature (CUSK or SAK) here
5070 addVDQNote tycon thing_inside
5071 | assertPpr (isTcTyCon tycon) (ppr tycon) $
5072 assertPpr (not (tcTyConIsPoly tycon)) (ppr tycon $$ ppr tc_kind)
5073 has_vdq
5074 = addLandmarkErrCtxt vdq_warning thing_inside
5075 | otherwise
5076 = thing_inside
5077 where
5078 -- Check whether a tycon has visible dependent quantification.
5079 -- This will *always* be a TcTyCon. Furthermore, it will *always*
5080 -- be an ungeneralised TcTyCon, straight out of kcInferDeclHeader.
5081 -- Thus, all the TyConBinders will be anonymous. Thus, the
5082 -- free variables of the tycon's kind will be the same as the free
5083 -- variables from all the binders.
5084 has_vdq = any is_vdq_tcb (tyConBinders tycon)
5085 tc_kind = tyConKind tycon
5086 kind_fvs = tyCoVarsOfType tc_kind
5087
5088 is_vdq_tcb tcb = (binderVar tcb `elemVarSet` kind_fvs) &&
5089 isVisibleTyConBinder tcb
5090
5091 vdq_warning = vcat
5092 [ text "NB: Type" <+> quotes (ppr tycon) <+>
5093 text "was inferred to use visible dependent quantification."
5094 , text "Most types with visible dependent quantification are"
5095 , text "polymorphically recursive and need a standalone kind"
5096 , text "signature. Perhaps supply one, with StandaloneKindSignatures."
5097 ]
5098
5099 tcAddDeclCtxt :: TyClDecl GhcRn -> TcM a -> TcM a
5100 tcAddDeclCtxt decl thing_inside
5101 = addErrCtxt (tcMkDeclCtxt decl) thing_inside
5102
5103 tcAddTyFamInstCtxt :: TyFamInstDecl GhcRn -> TcM a -> TcM a
5104 tcAddTyFamInstCtxt decl
5105 = tcAddFamInstCtxt (text "type instance") (tyFamInstDeclName decl)
5106
5107 tcMkDataFamInstCtxt :: DataFamInstDecl GhcRn -> SDoc
5108 tcMkDataFamInstCtxt decl@(DataFamInstDecl { dfid_eqn = eqn })
5109 = tcMkFamInstCtxt (pprDataFamInstFlavour decl <+> text "instance")
5110 (unLoc (feqn_tycon eqn))
5111
5112 tcAddDataFamInstCtxt :: DataFamInstDecl GhcRn -> TcM a -> TcM a
5113 tcAddDataFamInstCtxt decl
5114 = addErrCtxt (tcMkDataFamInstCtxt decl)
5115
5116 tcMkFamInstCtxt :: SDoc -> Name -> SDoc
5117 tcMkFamInstCtxt flavour tycon
5118 = hsep [ text "In the" <+> flavour <+> text "declaration for"
5119 , quotes (ppr tycon) ]
5120
5121 tcAddFamInstCtxt :: SDoc -> Name -> TcM a -> TcM a
5122 tcAddFamInstCtxt flavour tycon thing_inside
5123 = addErrCtxt (tcMkFamInstCtxt flavour tycon) thing_inside
5124
5125 tcAddClosedTypeFamilyDeclCtxt :: TyCon -> TcM a -> TcM a
5126 tcAddClosedTypeFamilyDeclCtxt tc
5127 = addErrCtxt ctxt
5128 where
5129 ctxt = text "In the equations for closed type family" <+>
5130 quotes (ppr tc)
5131
5132 resultTypeMisMatch :: FieldLabelString -> DataCon -> DataCon -> TcRnMessage
5133 resultTypeMisMatch field_name con1 con2
5134 = TcRnUnknownMessage $ mkPlainError noHints $
5135 vcat [sep [text "Constructors" <+> ppr con1 <+> text "and" <+> ppr con2,
5136 text "have a common field" <+> quotes (ppr field_name) <> comma],
5137 nest 2 $ text "but have different result types"]
5138
5139 fieldTypeMisMatch :: FieldLabelString -> DataCon -> DataCon -> TcRnMessage
5140 fieldTypeMisMatch field_name con1 con2
5141 = TcRnUnknownMessage $ mkPlainError noHints $
5142 sep [text "Constructors" <+> ppr con1 <+> text "and" <+> ppr con2,
5143 text "give different types for field", quotes (ppr field_name)]
5144
5145 dataConCtxt :: [LocatedN Name] -> SDoc
5146 dataConCtxt cons = text "In the definition of data constructor" <> plural cons
5147 <+> ppr_cons cons
5148
5149 dataConResCtxt :: [LocatedN Name] -> SDoc
5150 dataConResCtxt cons = text "In the result type of data constructor" <> plural cons
5151 <+> ppr_cons cons
5152
5153 ppr_cons :: [LocatedN Name] -> SDoc
5154 ppr_cons [con] = quotes (ppr con)
5155 ppr_cons cons = interpp'SP cons
5156
5157 classOpCtxt :: Var -> Type -> SDoc
5158 classOpCtxt sel_id tau = sep [text "When checking the class method:",
5159 nest 2 (pprPrefixOcc sel_id <+> dcolon <+> ppr tau)]
5160
5161 classArityErr :: Int -> Class -> TcRnMessage
5162 classArityErr n cls
5163 | n == 0 = mkErr "No" "no-parameter"
5164 | otherwise = mkErr "Too many" "multi-parameter"
5165 where
5166 mkErr howMany allowWhat = TcRnUnknownMessage $ mkPlainError noHints $
5167 vcat [text (howMany ++ " parameters for class") <+> quotes (ppr cls),
5168 parens (text ("Enable MultiParamTypeClasses to allow "
5169 ++ allowWhat ++ " classes"))]
5170
5171 classFunDepsErr :: Class -> TcRnMessage
5172 classFunDepsErr cls
5173 = TcRnUnknownMessage $ mkPlainError noHints $
5174 vcat [text "Fundeps in class" <+> quotes (ppr cls),
5175 parens (text "Enable FunctionalDependencies to allow fundeps")]
5176
5177 badMethPred :: Id -> TcPredType -> TcRnMessage
5178 badMethPred sel_id pred
5179 = TcRnUnknownMessage $ mkPlainError noHints $
5180 vcat [ hang (text "Constraint" <+> quotes (ppr pred)
5181 <+> text "in the type of" <+> quotes (ppr sel_id))
5182 2 (text "constrains only the class type variables")
5183 , text "Enable ConstrainedClassMethods to allow it" ]
5184
5185 noClassTyVarErr :: Class -> TyCon -> TcRnMessage
5186 noClassTyVarErr clas fam_tc
5187 = TcRnUnknownMessage $ mkPlainError noHints $
5188 sep [ text "The associated type" <+> quotes (ppr fam_tc <+> hsep (map ppr (tyConTyVars fam_tc)))
5189 , text "mentions none of the type or kind variables of the class" <+>
5190 quotes (ppr clas <+> hsep (map ppr (classTyVars clas)))]
5191
5192 badDataConTyCon :: DataCon -> Type -> TcRnMessage
5193 badDataConTyCon data_con res_ty_tmpl
5194 = TcRnUnknownMessage $ mkPlainError noHints $
5195 hang (text "Data constructor" <+> quotes (ppr data_con) <+>
5196 text "returns type" <+> quotes (ppr actual_res_ty))
5197 2 (text "instead of an instance of its parent type" <+> quotes (ppr res_ty_tmpl))
5198 where
5199 actual_res_ty = dataConOrigResTy data_con
5200
5201 badGadtDecl :: Name -> TcRnMessage
5202 badGadtDecl tc_name
5203 = TcRnUnknownMessage $ mkPlainError noHints $
5204 vcat [ text "Illegal generalised algebraic data declaration for" <+> quotes (ppr tc_name)
5205 , nest 2 (parens $ text "Enable the GADTs extension to allow this") ]
5206
5207 badExistential :: DataCon -> TcRnMessage
5208 badExistential con
5209 = TcRnUnknownMessage $ mkPlainError noHints $
5210 sdocOption sdocLinearTypes (\show_linear_types ->
5211 hang (text "Data constructor" <+> quotes (ppr con) <+>
5212 text "has existential type variables, a context, or a specialised result type")
5213 2 (vcat [ ppr con <+> dcolon <+> ppr (dataConDisplayType show_linear_types con)
5214 , parens $ text "Enable ExistentialQuantification or GADTs to allow this" ]))
5215
5216 badStupidTheta :: Name -> TcRnMessage
5217 badStupidTheta tc_name
5218 = TcRnUnknownMessage $ mkPlainError noHints $
5219 text "A data type declared in GADT style cannot have a context:" <+> quotes (ppr tc_name)
5220
5221 newtypeConError :: Name -> Int -> TcRnMessage
5222 newtypeConError tycon n
5223 = TcRnUnknownMessage $ mkPlainError noHints $
5224 sep [text "A newtype must have exactly one constructor,",
5225 nest 2 $ text "but" <+> quotes (ppr tycon) <+> text "has" <+> speakN n ]
5226
5227 newtypeStrictError :: DataCon -> TcRnMessage
5228 newtypeStrictError con
5229 = TcRnUnknownMessage $ mkPlainError noHints $
5230 sep [text "A newtype constructor cannot have a strictness annotation,",
5231 nest 2 $ text "but" <+> quotes (ppr con) <+> text "does"]
5232
5233 newtypeFieldErr :: DataCon -> Int -> TcRnMessage
5234 newtypeFieldErr con_name n_flds
5235 = TcRnUnknownMessage $ mkPlainError noHints $
5236 sep [text "The constructor of a newtype must have exactly one field",
5237 nest 2 $ text "but" <+> quotes (ppr con_name) <+> text "has" <+> speakN n_flds]
5238
5239 badSigTyDecl :: Name -> TcRnMessage
5240 badSigTyDecl tc_name
5241 = TcRnUnknownMessage $ mkPlainError noHints $
5242 vcat [ text "Illegal kind signature" <+>
5243 quotes (ppr tc_name)
5244 , nest 2 (parens $ text "Use KindSignatures to allow kind signatures") ]
5245
5246 emptyConDeclsErr :: Name -> TcRnMessage
5247 emptyConDeclsErr tycon
5248 = TcRnUnknownMessage $ mkPlainError noHints $
5249 sep [quotes (ppr tycon) <+> text "has no constructors",
5250 nest 2 $ text "(EmptyDataDecls permits this)"]
5251
5252 wrongKindOfFamily :: TyCon -> TcRnMessage
5253 wrongKindOfFamily family
5254 = TcRnUnknownMessage $ mkPlainError noHints $
5255 text "Wrong category of family instance; declaration was for a"
5256 <+> kindOfFamily
5257 where
5258 kindOfFamily | isTypeFamilyTyCon family = text "type family"
5259 | isDataFamilyTyCon family = text "data family"
5260 | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
5261
5262 -- | Produce an error for oversaturated type family equations with too many
5263 -- required arguments.
5264 -- See Note [Oversaturated type family equations] in "GHC.Tc.Validity".
5265 wrongNumberOfParmsErr :: Arity -> TcRnMessage
5266 wrongNumberOfParmsErr max_args
5267 = TcRnUnknownMessage $ mkPlainError noHints $
5268 text "Number of parameters must match family declaration; expected"
5269 <+> ppr max_args
5270
5271 badRoleAnnot :: Name -> Role -> Role -> TcRnMessage
5272 badRoleAnnot var annot inferred
5273 = TcRnUnknownMessage $ mkPlainError noHints $
5274 hang (text "Role mismatch on variable" <+> ppr var <> colon)
5275 2 (sep [ text "Annotation says", ppr annot
5276 , text "but role", ppr inferred
5277 , text "is required" ])
5278
5279 wrongNumberOfRoles :: [a] -> LRoleAnnotDecl GhcRn -> TcRnMessage
5280 wrongNumberOfRoles tyvars d@(L _ (RoleAnnotDecl _ _ annots))
5281 = TcRnUnknownMessage $ mkPlainError noHints $
5282 hang (text "Wrong number of roles listed in role annotation;" $$
5283 text "Expected" <+> (ppr $ length tyvars) <> comma <+>
5284 text "got" <+> (ppr $ length annots) <> colon)
5285 2 (ppr d)
5286
5287
5288 illegalRoleAnnotDecl :: LRoleAnnotDecl GhcRn -> TcM ()
5289 illegalRoleAnnotDecl (L loc (RoleAnnotDecl _ tycon _))
5290 = setErrCtxt [] $
5291 setSrcSpanA loc $
5292 addErrTc $ TcRnUnknownMessage $ mkPlainError noHints $
5293 (text "Illegal role annotation for" <+> ppr tycon <> char ';' $$
5294 text "they are allowed only for datatypes and classes.")
5295
5296 needXRoleAnnotations :: TyCon -> TcRnMessage
5297 needXRoleAnnotations tc
5298 = TcRnUnknownMessage $ mkPlainError noHints $
5299 text "Illegal role annotation for" <+> ppr tc <> char ';' $$
5300 text "did you intend to use RoleAnnotations?"
5301
5302 incoherentRoles :: TcRnMessage
5303 incoherentRoles = TcRnUnknownMessage $ mkPlainError noHints $
5304 (text "Roles other than" <+> quotes (text "nominal") <+>
5305 text "for class parameters can lead to incoherence.") $$
5306 (text "Use IncoherentInstances to allow this; bad role found")
5307
5308 wrongTyFamName :: Name -> Name -> TcRnMessage
5309 wrongTyFamName fam_tc_name eqn_tc_name
5310 = TcRnUnknownMessage $ mkPlainError noHints $
5311 hang (text "Mismatched type name in type family instance.")
5312 2 (vcat [ text "Expected:" <+> ppr fam_tc_name
5313 , text " Actual:" <+> ppr eqn_tc_name ])
5314
5315 addTyConCtxt :: TyCon -> TcM a -> TcM a
5316 addTyConCtxt tc = addTyConFlavCtxt name flav
5317 where
5318 name = getName tc
5319 flav = tyConFlavour tc
5320
5321 addRoleAnnotCtxt :: Name -> TcM a -> TcM a
5322 addRoleAnnotCtxt name
5323 = addErrCtxt $
5324 text "while checking a role annotation for" <+> quotes (ppr name)