never executed always true always false
1
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE FlexibleContexts #-}
4 {-# LANGUAGE RankNTypes #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE TypeFamilies #-}
7 {-# LANGUAGE ViewPatterns #-}
8
9 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
10
11 {-
12 (c) The University of Glasgow 2006
13 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
14
15 -}
16
17 -- | Typechecking user-specified @MonoTypes@
18 module GHC.Tc.Gen.HsType (
19 -- Type signatures
20 kcClassSigType, tcClassSigType,
21 tcHsSigType, tcHsSigWcType,
22 tcHsPartialSigType,
23 tcStandaloneKindSig,
24 funsSigCtxt, addSigCtxt, pprSigCtxt,
25
26 tcHsClsInstType,
27 tcHsDeriv, tcDerivStrategy,
28 tcHsTypeApp,
29 UserTypeCtxt(..),
30 bindImplicitTKBndrs_Tv, bindImplicitTKBndrs_Skol,
31 bindImplicitTKBndrs_Q_Tv, bindImplicitTKBndrs_Q_Skol,
32 bindExplicitTKBndrs_Tv, bindExplicitTKBndrs_Skol,
33 bindExplicitTKBndrs_Q_Tv, bindExplicitTKBndrs_Q_Skol,
34
35 bindOuterFamEqnTKBndrs, bindOuterFamEqnTKBndrs_Q_Tv,
36 tcOuterTKBndrs, scopedSortOuter,
37 bindOuterSigTKBndrs_Tv,
38 tcExplicitTKBndrs,
39 bindNamedWildCardBinders,
40
41 -- Type checking type and class decls, and instances thereof
42 bindTyClTyVars, tcFamTyPats,
43 etaExpandAlgTyCon, tcbVisibilities,
44
45 -- tyvars
46 zonkAndScopedSort,
47
48 -- Kind-checking types
49 -- No kind generalisation, no checkValidType
50 InitialKindStrategy(..),
51 SAKS_or_CUSK(..),
52 ContextKind(..),
53 kcDeclHeader,
54 tcHsLiftedType, tcHsOpenType,
55 tcHsLiftedTypeNC, tcHsOpenTypeNC,
56 tcInferLHsType, tcInferLHsTypeKind, tcInferLHsTypeUnsaturated,
57 tcCheckLHsType,
58 tcHsContext, tcLHsPredType,
59
60 kindGeneralizeAll, kindGeneralizeSome, kindGeneralizeNone,
61
62 -- Sort-checking kinds
63 tcLHsKindSig, checkDataKindSig, DataSort(..),
64 checkClassKindSig,
65
66 -- Multiplicity
67 tcMult,
68
69 -- Pattern type signatures
70 tcHsPatSigType,
71 HoleMode(..),
72
73 -- Error messages
74 funAppCtxt, addTyConFlavCtxt
75 ) where
76
77 import GHC.Prelude
78
79 import GHC.Hs
80 import GHC.Rename.Utils
81 import GHC.Tc.Errors.Types
82 import GHC.Tc.Utils.Monad
83 import GHC.Tc.Types.Origin
84 import GHC.Core.Predicate
85 import GHC.Tc.Types.Constraint
86 import GHC.Tc.Utils.Env
87 import GHC.Tc.Utils.TcMType
88 import GHC.Tc.Validity
89 import GHC.Tc.Utils.Unify
90 import GHC.IfaceToCore
91 import GHC.Tc.Solver
92 import GHC.Tc.Utils.Zonk
93 import GHC.Core.TyCo.Rep
94 import GHC.Core.TyCo.Ppr
95 import GHC.Tc.Utils.TcType
96 import GHC.Tc.Utils.Instantiate ( tcInstInvisibleTyBinders, tcInstInvisibleTyBindersN,
97 tcInstInvisibleTyBinder )
98 import GHC.Core.Type
99 import GHC.Builtin.Types.Prim
100 import GHC.Types.Error
101 import GHC.Types.Name.Env
102 import GHC.Types.Name.Reader( lookupLocalRdrOcc )
103 import GHC.Types.Var
104 import GHC.Types.Var.Set
105 import GHC.Core.TyCon
106 import GHC.Core.ConLike
107 import GHC.Core.DataCon
108 import GHC.Core.Class
109 import GHC.Types.Name
110 -- import GHC.Types.Name.Set
111 import GHC.Types.Var.Env
112 import GHC.Builtin.Types
113 import GHC.Types.Basic
114 import GHC.Types.SrcLoc
115 import GHC.Types.Unique
116 import GHC.Types.Unique.FM
117 import GHC.Types.Unique.Set
118 import GHC.Utils.Misc
119 import GHC.Types.Unique.Supply
120 import GHC.Utils.Outputable
121 import GHC.Utils.Panic
122 import GHC.Utils.Panic.Plain
123 import GHC.Data.FastString
124 import GHC.Builtin.Names hiding ( wildCardName )
125 import GHC.Driver.Session
126 import qualified GHC.LanguageExtensions as LangExt
127
128 import GHC.Data.Maybe
129 import GHC.Data.Bag( unitBag )
130 import Data.List ( find )
131 import Control.Monad
132
133 {-
134 ----------------------------
135 General notes
136 ----------------------------
137
138 Unlike with expressions, type-checking types both does some checking and
139 desugars at the same time. This is necessary because we often want to perform
140 equality checks on the types right away, and it would be incredibly painful
141 to do this on un-desugared types. Luckily, desugared types are close enough
142 to HsTypes to make the error messages sane.
143
144 During type-checking, we perform as little validity checking as possible.
145 Generally, after type-checking, you will want to do validity checking, say
146 with GHC.Tc.Validity.checkValidType.
147
148 Validity checking
149 ~~~~~~~~~~~~~~~~~
150 Some of the validity check could in principle be done by the kind checker,
151 but not all:
152
153 - During desugaring, we normalise by expanding type synonyms. Only
154 after this step can we check things like type-synonym saturation
155 e.g. type T k = k Int
156 type S a = a
157 Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
158 and then S is saturated. This is a GHC extension.
159
160 - Similarly, also a GHC extension, we look through synonyms before complaining
161 about the form of a class or instance declaration
162
163 - Ambiguity checks involve functional dependencies
164
165 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
166 finished building the loop. So to keep things simple, we postpone most validity
167 checking until step (3).
168
169 %************************************************************************
170 %* *
171 Check types AND do validity checking
172 * *
173 ************************************************************************
174
175 Note [Keeping implicitly quantified variables in order]
176 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
177 When the user implicitly quantifies over variables (say, in a type
178 signature), we need to come up with some ordering on these variables.
179 This is done by bumping the TcLevel, bringing the tyvars into scope,
180 and then type-checking the thing_inside. The constraints are all
181 wrapped in an implication, which is then solved. Finally, we can
182 zonk all the binders and then order them with scopedSort.
183
184 It's critical to solve before zonking and ordering in order to uncover
185 any unifications. You might worry that this eager solving could cause
186 trouble elsewhere. I don't think it will. Because it will solve only
187 in an increased TcLevel, it can't unify anything that was mentioned
188 elsewhere. Additionally, we require that the order of implicitly
189 quantified variables is manifest by the scope of these variables, so
190 we're not going to learn more information later that will help order
191 these variables.
192
193 Note [Recipe for checking a signature]
194 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
195 Kind-checking a user-written signature requires several steps:
196
197 0. Bump the TcLevel
198 1. Bind any lexically-scoped type variables.
199 2. Generate constraints.
200 3. Solve constraints.
201 4. Sort any implicitly-bound variables into dependency order
202 5. Promote tyvars and/or kind-generalize.
203 6. Zonk.
204 7. Check validity.
205
206 Very similar steps also apply when kind-checking a type or class
207 declaration.
208
209 The general pattern looks something like this. (But NB every
210 specific instance varies in one way or another!)
211
212 do { (tclvl, wanted, (spec_tkvs, ty))
213 <- pushLevelAndSolveEqualitiesX "tc_top_lhs_type" $
214 bindImplicitTKBndrs_Skol sig_vars $
215 <kind-check the type>
216
217 ; spec_tkvs <- zonkAndScopedSort spec_tkvs
218
219 ; reportUnsolvedEqualities skol_info spec_tkvs tclvl wanted
220
221 ; let ty1 = mkSpecForAllTys spec_tkvs ty
222 ; kvs <- kindGeneralizeAll ty1
223
224 ; final_ty <- zonkTcTypeToType (mkInfForAllTys kvs ty1)
225
226 ; checkValidType final_ty
227
228 This pattern is repeated many times in GHC.Tc.Gen.HsType,
229 GHC.Tc.Gen.Sig, and GHC.Tc.TyCl, with variations. In more detail:
230
231 * pushLevelAndSolveEqualitiesX (Step 0, step 3) bumps the TcLevel,
232 calls the thing inside to generate constraints, solves those
233 constraints as much as possible, returning the residual unsolved
234 constraints in 'wanted'.
235
236 * bindImplicitTKBndrs_Skol (Step 1) binds the user-specified type
237 variables E.g. when kind-checking f :: forall a. F a -> a we must
238 bring 'a' into scope before kind-checking (F a -> a)
239
240 * zonkAndScopedSort (Step 4) puts those user-specified variables in
241 the dependency order. (For "implicit" variables the order is no
242 user-specified. E.g. forall (a::k1) (b::k2). blah k1 and k2 are
243 implicitly brought into scope.
244
245 * reportUnsolvedEqualities (Step 3 continued) reports any unsolved
246 equalities, carefully wrapping them in an implication that binds the
247 skolems. We can't do that in pushLevelAndSolveEqualitiesX because
248 that function doesn't have access to the skolems.
249
250 * kindGeneralize (Step 5). See Note [Kind generalisation]
251
252 * The final zonkTcTypeToType must happen after promoting/generalizing,
253 because promoting and generalizing fill in metavariables.
254
255
256 Doing Step 3 (constraint solving) eagerly (rather than building an
257 implication constraint and solving later) is necessary for several
258 reasons:
259
260 * Exactly as for Solver.simplifyInfer: when generalising, we solve all
261 the constraints we can so that we don't have to quantify over them
262 or, since we don't quantify over constraints in kinds, float them
263 and inhibit generalisation.
264
265 * Most signatures also bring implicitly quantified variables into
266 scope, and solving is necessary to get these in the right order
267 (Step 4) see Note [Keeping implicitly quantified variables in
268 order]).
269
270 Note [Kind generalisation]
271 ~~~~~~~~~~~~~~~~~~~~~~~~~~
272 Step 5 of Note [Recipe for checking a signature], namely
273 kind-generalisation, is done by
274 kindGeneraliseAll
275 kindGeneraliseSome
276 kindGeneraliseNone
277
278 Here, we have to deal with the fact that metatyvars generated in the
279 type will have a bumped TcLevel, because explicit foralls raise the
280 TcLevel. To avoid these variables from ever being visible in the
281 surrounding context, we must obey the following dictum:
282
283 Every metavariable in a type must either be
284 (A) generalized, or
285 (B) promoted, or See Note [Promotion in signatures]
286 (C) a cause to error See Note [Naughty quantification candidates]
287 in GHC.Tc.Utils.TcMType
288
289 There are three steps (look at kindGeneraliseSome):
290
291 1. candidateQTyVarsOfType finds the free variables of the type or kind,
292 to generalise
293
294 2. filterConstrainedCandidates filters out candidates that appear
295 in the unsolved 'wanteds', and promotes the ones that get filtered out
296 thereby.
297
298 3. quantifyTyVars quantifies the remaining type variables
299
300 The kindGeneralize functions do not require pre-zonking; they zonk as they
301 go.
302
303 kindGeneraliseAll specialises for the case where step (2) is vacuous.
304 kindGeneraliseNone specialises for the case where we do no quantification,
305 but we must still promote.
306
307 If you are actually doing kind-generalization, you need to bump the
308 level before generating constraints, as we will only generalize
309 variables with a TcLevel higher than the ambient one.
310 Hence the "pushLevel" in pushLevelAndSolveEqualities.
311
312 Note [Promotion in signatures]
313 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
314 If an unsolved metavariable in a signature is not generalized
315 (because we're not generalizing the construct -- e.g., pattern
316 sig -- or because the metavars are constrained -- see kindGeneralizeSome)
317 we need to promote to maintain (WantedTvInv) of Note [TcLevel invariants]
318 in GHC.Tc.Utils.TcType. Note that promotion is identical in effect to generalizing
319 and the reinstantiating with a fresh metavariable at the current level.
320 So in some sense, we generalize *all* variables, but then re-instantiate
321 some of them.
322
323 Here is an example of why we must promote:
324 foo (x :: forall a. a -> Proxy b) = ...
325
326 In the pattern signature, `b` is unbound, and will thus be brought into
327 scope. We do not know its kind: it will be assigned kappa[2]. Note that
328 kappa is at TcLevel 2, because it is invented under a forall. (A priori,
329 the kind kappa might depend on `a`, so kappa rightly has a higher TcLevel
330 than the surrounding context.) This kappa cannot be solved for while checking
331 the pattern signature (which is not kind-generalized). When we are checking
332 the *body* of foo, though, we need to unify the type of x with the argument
333 type of bar. At this point, the ambient TcLevel is 1, and spotting a
334 matavariable with level 2 would violate the (WantedTvInv) invariant of
335 Note [TcLevel invariants]. So, instead of kind-generalizing,
336 we promote the metavariable to level 1. This is all done in kindGeneralizeNone.
337
338 -}
339
340 funsSigCtxt :: [LocatedN Name] -> UserTypeCtxt
341 -- Returns FunSigCtxt, with no redundant-context-reporting,
342 -- form a list of located names
343 funsSigCtxt (L _ name1 : _) = FunSigCtxt name1 NoRRC
344 funsSigCtxt [] = panic "funSigCtxt"
345
346 addSigCtxt :: Outputable hs_ty => UserTypeCtxt -> LocatedA hs_ty -> TcM a -> TcM a
347 addSigCtxt ctxt hs_ty thing_inside
348 = setSrcSpan (getLocA hs_ty) $
349 addErrCtxt (pprSigCtxt ctxt hs_ty) $
350 thing_inside
351
352 pprSigCtxt :: Outputable hs_ty => UserTypeCtxt -> LocatedA hs_ty -> SDoc
353 -- (pprSigCtxt ctxt <extra> <type>)
354 -- prints In the type signature for 'f':
355 -- f :: <type>
356 -- The <extra> is either empty or "the ambiguity check for"
357 pprSigCtxt ctxt hs_ty
358 | Just n <- isSigMaybe ctxt
359 = hang (text "In the type signature:")
360 2 (pprPrefixOcc n <+> dcolon <+> ppr hs_ty)
361
362 | otherwise
363 = hang (text "In" <+> pprUserTypeCtxt ctxt <> colon)
364 2 (ppr hs_ty)
365
366 tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type
367 -- This one is used when we have a LHsSigWcType, but in
368 -- a place where wildcards aren't allowed. The renamer has
369 -- already checked this, so we can simply ignore it.
370 tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)
371
372 kcClassSigType :: [LocatedN Name] -> LHsSigType GhcRn -> TcM ()
373 -- This is a special form of tcClassSigType that is used during the
374 -- kind-checking phase to infer the kind of class variables. Cf. tc_lhs_sig_type.
375 -- Importantly, this does *not* kind-generalize. Consider
376 -- class SC f where
377 -- meth :: forall a (x :: f a). Proxy x -> ()
378 -- When instantiating Proxy with kappa, we must unify kappa := f a. But we're
379 -- still working out the kind of f, and thus f a will have a coercion in it.
380 -- Coercions block unification (Note [Equalities with incompatible kinds] in
381 -- TcCanonical) and so we fail to unify. If we try to kind-generalize, we'll
382 -- end up promoting kappa to the top level (because kind-generalization is
383 -- normally done right before adding a binding to the context), and then we
384 -- can't set kappa := f a, because a is local.
385 kcClassSigType names
386 sig_ty@(L _ (HsSig { sig_bndrs = hs_outer_bndrs, sig_body = hs_ty }))
387 = addSigCtxt (funsSigCtxt names) sig_ty $
388 do { _ <- bindOuterSigTKBndrs_Tv hs_outer_bndrs $
389 tcLHsType hs_ty liftedTypeKind
390 ; return () }
391
392 tcClassSigType :: [LocatedN Name] -> LHsSigType GhcRn -> TcM Type
393 -- Does not do validity checking
394 tcClassSigType names sig_ty
395 = addSigCtxt sig_ctxt sig_ty $
396 do { (implic, ty) <- tc_lhs_sig_type skol_info sig_ty (TheKind liftedTypeKind)
397 ; emitImplication implic
398 ; return ty }
399 -- Do not zonk-to-Type, nor perform a validity check
400 -- We are in a knot with the class and associated types
401 -- Zonking and validity checking is done by tcClassDecl
402 --
403 -- No need to fail here if the type has an error:
404 -- If we're in the kind-checking phase, the solveEqualities
405 -- in kcTyClGroup catches the error
406 -- If we're in the type-checking phase, the solveEqualities
407 -- in tcClassDecl1 gets it
408 -- Failing fast here degrades the error message in, e.g., tcfail135:
409 -- class Foo f where
410 -- baa :: f a -> f
411 -- If we fail fast, we're told that f has kind `k1` when we wanted `*`.
412 -- It should be that f has kind `k2 -> *`, but we never get a chance
413 -- to run the solver where the kind of f is touchable. This is
414 -- painfully delicate.
415 where
416 sig_ctxt = funsSigCtxt names
417 skol_info = SigTypeSkol sig_ctxt
418
419 tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
420 -- Does validity checking
421 -- See Note [Recipe for checking a signature]
422 tcHsSigType ctxt sig_ty
423 = addSigCtxt ctxt sig_ty $
424 do { traceTc "tcHsSigType {" (ppr sig_ty)
425
426 -- Generalise here: see Note [Kind generalisation]
427 ; (implic, ty) <- tc_lhs_sig_type skol_info sig_ty (expectedKindInCtxt ctxt)
428
429 -- Float out constraints, failing fast if not possible
430 -- See Note [Failure in local type signatures] in GHC.Tc.Solver
431 ; traceTc "tcHsSigType 2" (ppr implic)
432 ; simplifyAndEmitFlatConstraints (mkImplicWC (unitBag implic))
433
434 ; ty <- zonkTcType ty
435 ; checkValidType ctxt ty
436 ; traceTc "end tcHsSigType }" (ppr ty)
437 ; return ty }
438 where
439 skol_info = SigTypeSkol ctxt
440
441 tc_lhs_sig_type :: SkolemInfo -> LHsSigType GhcRn
442 -> ContextKind -> TcM (Implication, TcType)
443 -- Kind-checks/desugars an 'LHsSigType',
444 -- solve equalities,
445 -- and then kind-generalizes.
446 -- This will never emit constraints, as it uses solveEqualities internally.
447 -- No validity checking or zonking
448 -- Returns also an implication for the unsolved constraints
449 tc_lhs_sig_type skol_info full_hs_ty@(L loc (HsSig { sig_bndrs = hs_outer_bndrs
450 , sig_body = hs_ty })) ctxt_kind
451 = setSrcSpanA loc $
452 do { (tc_lvl, wanted, (exp_kind, (outer_bndrs, ty)))
453 <- pushLevelAndSolveEqualitiesX "tc_lhs_sig_type" $
454 -- See Note [Failure in local type signatures]
455 do { exp_kind <- newExpectedKind ctxt_kind
456 -- See Note [Escaping kind in type signatures]
457 ; stuff <- tcOuterTKBndrs skol_info hs_outer_bndrs $
458 tcLHsType hs_ty exp_kind
459 ; return (exp_kind, stuff) }
460
461 -- Default any unconstrained variables free in the kind
462 -- See Note [Escaping kind in type signatures]
463 ; exp_kind_dvs <- candidateQTyVarsOfType exp_kind
464 ; doNotQuantifyTyVars exp_kind_dvs (mk_doc exp_kind)
465
466 ; traceTc "tc_lhs_sig_type" (ppr hs_outer_bndrs $$ ppr outer_bndrs)
467 ; (outer_tv_bndrs :: [InvisTVBinder]) <- scopedSortOuter outer_bndrs
468
469 ; let ty1 = mkInvisForAllTys outer_tv_bndrs ty
470
471 ; kvs <- kindGeneralizeSome wanted ty1
472
473 -- Build an implication for any as-yet-unsolved kind equalities
474 -- See Note [Skolem escape in type signatures]
475 ; implic <- buildTvImplication skol_info kvs tc_lvl wanted
476
477 ; return (implic, mkInfForAllTys kvs ty1) }
478 where
479 mk_doc exp_kind tidy_env
480 = do { (tidy_env2, exp_kind) <- zonkTidyTcType tidy_env exp_kind
481 ; return (tidy_env2, hang (text "The kind" <+> ppr exp_kind)
482 2 (text "of type signature:" <+> ppr full_hs_ty)) }
483
484
485
486 {- Note [Escaping kind in type signatures]
487 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
488 Consider kind-checking the signature for `foo` (#19495):
489 type family T (r :: RuntimeRep) :: TYPE r
490
491 foo :: forall (r :: RuntimeRep). T r
492 foo = ...
493
494 We kind-check the type with expected kind `TYPE delta` (see newExpectedKind),
495 where `delta :: RuntimeRep` is as-yet unknown. (We can't use `TYPE LiftedRep`
496 because we allow signatures like `foo :: Int#`.)
497
498 Suppose we are at level L currently. We do this
499 * pushLevelAndSolveEqualitiesX: moves to level L+1
500 * newExpectedKind: allocates delta{L+1}
501 * tcOuterTKBndrs: pushes the level again to L+2, binds skolem r{L+2}
502 * kind-check the body (T r) :: TYPE delta{L+1}
503
504 Then
505 * We can't unify delta{L+1} with r{L+2}.
506 And rightly so: skolem would escape.
507
508 * If delta{L+1} is unified with some-kind{L}, that is fine.
509 This can happen
510 \(x::a) -> let y :: a; y = x in ...(x :: Int#)...
511 Here (x :: a :: TYPE gamma) is in the environment when we check
512 the signature y::a. We unify delta := gamma, and all is well.
513
514 * If delta{L+1} is unconstrained, we /must not/ quantify over it!
515 E.g. Consider f :: Any where Any :: forall k. k
516 We kind-check this with expected kind TYPE kappa. We get
517 Any @(TYPE kappa) :: TYPE kappa
518 We don't want to generalise to forall k. Any @k
519 because that is ill-kinded: the kind of the body of the forall,
520 (Any @k :: k) mentions the bound variable k.
521
522 Instead we want to default it to LiftedRep.
523
524 An alternative would be to promote it, similar to the monomorphism
525 restriction, but the MR is pretty confusing. Defaulting seems better
526
527 How does that defaulting happen? Well, since we /currently/ default
528 RuntimeRep variables during generalisation, it'll happen in
529 kindGeneralize. But in principle we might allow generalisation over
530 RuntimeRep variables in future. Moreover, what if we had
531 kappa{L+1} := F alpha{L+1}
532 where F :: Type -> RuntimeRep. Now it's alpha that is free in the kind
533 and it /won't/ be defaulted.
534
535 So we use doNotQuantifyTyVars to either default the free vars of
536 exp_kind (if possible), or error (if not).
537
538 Note [Skolem escape in type signatures]
539 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
540 tcHsSigType is tricky. Consider (T11142)
541 foo :: forall b. (forall k (a :: k). SameKind a b) -> ()
542 This is ill-kinded because of a nested skolem-escape.
543
544 That will show up as an un-solvable constraint in the implication
545 returned by buildTvImplication in tc_lhs_sig_type. See Note [Skolem
546 escape prevention] in GHC.Tc.Utils.TcType for why it is unsolvable
547 (the unification variable for b's kind is untouchable).
548
549 Then, in GHC.Tc.Solver.simplifyAndEmitFlatConstraints (called from tcHsSigType)
550 we'll try to float out the constraint, be unable to do so, and fail.
551 See GHC.Tc.Solver Note [Failure in local type signatures] for more
552 detail on this.
553
554 The separation between tcHsSigType and tc_lhs_sig_type is because
555 tcClassSigType wants to use the latter, but *not* fail fast, because
556 there are skolems from the class decl which are in scope; but it's fine
557 not to because tcClassDecl1 has a solveEqualities wrapped around all
558 the tcClassSigType calls.
559
560 That's why tcHsSigType does simplifyAndEmitFlatConstraints (which
561 fails fast) but tcClassSigType just does emitImplication (which does
562 not). Ugh.
563
564 c.f. see also Note [Skolem escape and forall-types]. The difference
565 is that we don't need to simplify at a forall type, only at the
566 top level of a signature.
567 -}
568
569 -- Does validity checking and zonking.
570 tcStandaloneKindSig :: LStandaloneKindSig GhcRn -> TcM (Name, Kind)
571 tcStandaloneKindSig (L _ (StandaloneKindSig _ (L _ name) ksig))
572 = addSigCtxt ctxt ksig $
573 do { kind <- tc_top_lhs_type KindLevel ctxt ksig
574 ; checkValidType ctxt kind
575 ; return (name, kind) }
576 where
577 ctxt = StandaloneKindSigCtxt name
578
579 tcTopLHsType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
580 tcTopLHsType ctxt lsig_ty
581 = tc_top_lhs_type TypeLevel ctxt lsig_ty
582
583 tc_top_lhs_type :: TypeOrKind -> UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
584 -- tc_top_lhs_type is used for kind-checking top-level LHsSigTypes where
585 -- we want to fully solve /all/ equalities, and report errors
586 -- Does zonking, but not validity checking because it's used
587 -- for things (like deriving and instances) that aren't
588 -- ordinary types
589 -- Used for both types and kinds
590 tc_top_lhs_type tyki ctxt (L loc sig_ty@(HsSig { sig_bndrs = hs_outer_bndrs
591 , sig_body = body }))
592 = setSrcSpanA loc $
593 do { traceTc "tc_top_lhs_type {" (ppr sig_ty)
594 ; (tclvl, wanted, (outer_bndrs, ty))
595 <- pushLevelAndSolveEqualitiesX "tc_top_lhs_type" $
596 tcOuterTKBndrs skol_info hs_outer_bndrs $
597 do { kind <- newExpectedKind (expectedKindInCtxt ctxt)
598 ; tc_lhs_type (mkMode tyki) body kind }
599
600 ; outer_tv_bndrs <- scopedSortOuter outer_bndrs
601 ; let ty1 = mkInvisForAllTys outer_tv_bndrs ty
602
603 ; kvs <- kindGeneralizeAll ty1 -- "All" because it's a top-level type
604 ; reportUnsolvedEqualities skol_info kvs tclvl wanted
605
606 ; ze <- mkEmptyZonkEnv NoFlexi
607 ; final_ty <- zonkTcTypeToTypeX ze (mkInfForAllTys kvs ty1)
608 ; traceTc "tc_top_lhs_type }" (vcat [ppr sig_ty, ppr final_ty])
609 ; return final_ty }
610 where
611 skol_info = SigTypeSkol ctxt
612
613 -----------------
614 tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind])
615 -- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
616 -- Returns the C, [ty1, ty2, and the kinds of C's remaining arguments
617 -- E.g. class C (a::*) (b::k->k)
618 -- data T a b = ... deriving( C Int )
619 -- returns ([k], C, [k, Int], [k->k])
620 -- Return values are fully zonked
621 tcHsDeriv hs_ty
622 = do { ty <- checkNoErrs $ -- Avoid redundant error report
623 -- with "illegal deriving", below
624 tcTopLHsType DerivClauseCtxt hs_ty
625 ; let (tvs, pred) = splitForAllTyCoVars ty
626 (kind_args, _) = splitFunTys (tcTypeKind pred)
627 ; case getClassPredTys_maybe pred of
628 Just (cls, tys) -> return (tvs, cls, tys, map scaledThing kind_args)
629 Nothing -> failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
630 (text "Illegal deriving item" <+> quotes (ppr hs_ty)) }
631
632 -- | Typecheck a deriving strategy. For most deriving strategies, this is a
633 -- no-op, but for the @via@ strategy, this requires typechecking the @via@ type.
634 tcDerivStrategy ::
635 Maybe (LDerivStrategy GhcRn)
636 -- ^ The deriving strategy
637 -> TcM (Maybe (LDerivStrategy GhcTc), [TyVar])
638 -- ^ The typechecked deriving strategy and the tyvars that it binds
639 -- (if using 'ViaStrategy').
640 tcDerivStrategy mb_lds
641 = case mb_lds of
642 Nothing -> boring_case Nothing
643 Just (L loc ds) ->
644 setSrcSpanA loc $ do
645 (ds', tvs) <- tc_deriv_strategy ds
646 pure (Just (L loc ds'), tvs)
647 where
648 tc_deriv_strategy :: DerivStrategy GhcRn
649 -> TcM (DerivStrategy GhcTc, [TyVar])
650 tc_deriv_strategy (StockStrategy _)
651 = boring_case (StockStrategy noExtField)
652 tc_deriv_strategy (AnyclassStrategy _)
653 = boring_case (AnyclassStrategy noExtField)
654 tc_deriv_strategy (NewtypeStrategy _)
655 = boring_case (NewtypeStrategy noExtField)
656 tc_deriv_strategy (ViaStrategy ty) = do
657 ty' <- checkNoErrs $ tcTopLHsType DerivClauseCtxt ty
658 let (via_tvs, via_pred) = splitForAllTyCoVars ty'
659 pure (ViaStrategy via_pred, via_tvs)
660
661 boring_case :: ds -> TcM (ds, [TyVar])
662 boring_case ds = pure (ds, [])
663
664 tcHsClsInstType :: UserTypeCtxt -- InstDeclCtxt or SpecInstCtxt
665 -> LHsSigType GhcRn
666 -> TcM Type
667 -- Like tcHsSigType, but for a class instance declaration
668 tcHsClsInstType user_ctxt hs_inst_ty
669 = setSrcSpan (getLocA hs_inst_ty) $
670 do { -- Fail eagerly if tcTopLHsType fails. We are at top level so
671 -- these constraints will never be solved later. And failing
672 -- eagerly avoids follow-on errors when checkValidInstance
673 -- sees an unsolved coercion hole
674 inst_ty <- checkNoErrs $
675 tcTopLHsType user_ctxt hs_inst_ty
676 ; checkValidInstance user_ctxt hs_inst_ty inst_ty
677 ; return inst_ty }
678
679 ----------------------------------------------
680 -- | Type-check a visible type application
681 tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
682 -- See Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType
683 tcHsTypeApp wc_ty kind
684 | HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty
685 = do { mode <- mkHoleMode TypeLevel HM_VTA
686 -- HM_VTA: See Note [Wildcards in visible type application]
687 ; ty <- addTypeCtxt hs_ty $
688 solveEqualities "tcHsTypeApp" $
689 -- We are looking at a user-written type, very like a
690 -- signature so we want to solve its equalities right now
691 bindNamedWildCardBinders sig_wcs $ \ _ ->
692 tc_lhs_type mode hs_ty kind
693
694 -- We do not kind-generalize type applications: we just
695 -- instantiate with exactly what the user says.
696 -- See Note [No generalization in type application]
697 -- We still must call kindGeneralizeNone, though, according
698 -- to Note [Recipe for checking a signature]
699 ; kindGeneralizeNone ty
700 ; ty <- zonkTcType ty
701 ; checkValidType TypeAppCtxt ty
702 ; return ty }
703
704 {- Note [Wildcards in visible type application]
705 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
706 A HsWildCardBndrs's hswc_ext now only includes /named/ wildcards, so
707 any unnamed wildcards stay unchanged in hswc_body. When called in
708 tcHsTypeApp, tcCheckLHsType will call emitAnonTypeHole
709 on these anonymous wildcards. However, this would trigger
710 error/warning when an anonymous wildcard is passed in as a visible type
711 argument, which we do not want because users should be able to write
712 @_ to skip a instantiating a type variable variable without fuss. The
713 solution is to switch the PartialTypeSignatures flags here to let the
714 typechecker know that it's checking a '@_' and do not emit hole
715 constraints on it. See related Note [Wildcards in visible kind
716 application] and Note [The wildcard story for types] in GHC.Hs.Type
717
718 Ugh!
719
720 Note [No generalization in type application]
721 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
722 We do not kind-generalize type applications. Imagine
723
724 id @(Proxy Nothing)
725
726 If we kind-generalized, we would get
727
728 id @(forall {k}. Proxy @(Maybe k) (Nothing @k))
729
730 which is very sneakily impredicative instantiation.
731
732 There is also the possibility of mentioning a wildcard
733 (`id @(Proxy _)`), which definitely should not be kind-generalized.
734
735 -}
736
737 tcFamTyPats :: TyCon
738 -> HsTyPats GhcRn -- Patterns
739 -> TcM (TcType, TcKind) -- (lhs_type, lhs_kind)
740 -- Check the LHS of a type/data family instance
741 -- e.g. type instance F ty1 .. tyn = ...
742 -- Used for both type and data families
743 tcFamTyPats fam_tc hs_pats
744 = do { traceTc "tcFamTyPats {" $
745 vcat [ ppr fam_tc, text "arity:" <+> ppr fam_arity ]
746
747 ; mode <- mkHoleMode TypeLevel HM_FamPat
748 -- HM_FamPat: See Note [Wildcards in family instances] in
749 -- GHC.Rename.Module
750 ; let fun_ty = mkTyConApp fam_tc []
751 ; (fam_app, res_kind) <- tcInferTyApps mode lhs_fun fun_ty hs_pats
752
753 -- Hack alert: see Note [tcFamTyPats: zonking the result kind]
754 ; res_kind <- zonkTcType res_kind
755
756 ; traceTc "End tcFamTyPats }" $
757 vcat [ ppr fam_tc, text "res_kind:" <+> ppr res_kind ]
758
759 ; return (fam_app, res_kind) }
760 where
761 fam_name = tyConName fam_tc
762 fam_arity = tyConArity fam_tc
763 lhs_fun = noLocA (HsTyVar noAnn NotPromoted (noLocA fam_name))
764
765 {- Note [tcFamTyPats: zonking the result kind]
766 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
767 Consider (#19250)
768 F :: forall k. k -> k
769 type instance F (x :: Constraint) = ()
770
771 The tricky point is this:
772 is that () an empty type tuple (() :: Type), or
773 an empty constraint tuple (() :: Constraint)?
774 We work this out in a hacky way, by looking at the expected kind:
775 see Note [Inferring tuple kinds].
776
777 In this case, we kind-check the RHS using the kind gotten from the LHS:
778 see the call to tcCheckLHsType in tcTyFamInstEqnGuts in GHC.Tc.Tycl.
779
780 But we want the kind from the LHS to be /zonked/, so that when
781 kind-checking the RHS (tcCheckLHsType) we can "see" what we learned
782 from kind-checking the LHS (tcFamTyPats). In our example above, the
783 type of the LHS is just `kappa` (by instantiating the forall k), but
784 then we learn (from x::Constraint) that kappa ~ Constraint. We want
785 that info when kind-checking the RHS.
786
787 Easy solution: just zonk that return kind. Of course this won't help
788 if there is lots of type-family reduction to do, but it works fine in
789 common cases.
790 -}
791
792
793 {-
794 ************************************************************************
795 * *
796 The main kind checker: no validity checks here
797 * *
798 ************************************************************************
799 -}
800
801 ---------------------------
802 tcHsOpenType, tcHsLiftedType,
803 tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> TcM TcType
804 -- Used for type signatures
805 -- Do not do validity checking
806 tcHsOpenType hs_ty = addTypeCtxt hs_ty $ tcHsOpenTypeNC hs_ty
807 tcHsLiftedType hs_ty = addTypeCtxt hs_ty $ tcHsLiftedTypeNC hs_ty
808
809 tcHsOpenTypeNC hs_ty = do { ek <- newOpenTypeKind; tcLHsType hs_ty ek }
810 tcHsLiftedTypeNC hs_ty = tcLHsType hs_ty liftedTypeKind
811
812 -- Like tcHsType, but takes an expected kind
813 tcCheckLHsType :: LHsType GhcRn -> ContextKind -> TcM TcType
814 tcCheckLHsType hs_ty exp_kind
815 = addTypeCtxt hs_ty $
816 do { ek <- newExpectedKind exp_kind
817 ; tcLHsType hs_ty ek }
818
819 tcInferLHsType :: LHsType GhcRn -> TcM TcType
820 tcInferLHsType hs_ty
821 = do { (ty,_kind) <- tcInferLHsTypeKind hs_ty
822 ; return ty }
823
824 tcInferLHsTypeKind :: LHsType GhcRn -> TcM (TcType, TcKind)
825 -- Called from outside: set the context
826 -- Eagerly instantiate any trailing invisible binders
827 tcInferLHsTypeKind lhs_ty@(L loc hs_ty)
828 = addTypeCtxt lhs_ty $
829 setSrcSpanA loc $ -- Cover the tcInstInvisibleTyBinders
830 do { (res_ty, res_kind) <- tc_infer_hs_type typeLevelMode hs_ty
831 ; tcInstInvisibleTyBinders res_ty res_kind }
832 -- See Note [Do not always instantiate eagerly in types]
833
834 -- Used to check the argument of GHCi :kind
835 -- Allow and report wildcards, e.g. :kind T _
836 -- Do not saturate family applications: see Note [Dealing with :kind]
837 -- Does not instantiate eagerly; See Note [Do not always instantiate eagerly in types]
838 tcInferLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
839 tcInferLHsTypeUnsaturated hs_ty
840 = addTypeCtxt hs_ty $
841 do { mode <- mkHoleMode TypeLevel HM_Sig -- Allow and report holes
842 ; case splitHsAppTys (unLoc hs_ty) of
843 Just (hs_fun_ty, hs_args)
844 -> do { (fun_ty, _ki) <- tcInferTyAppHead mode hs_fun_ty
845 ; tcInferTyApps_nosat mode hs_fun_ty fun_ty hs_args }
846 -- Notice the 'nosat'; do not instantiate trailing
847 -- invisible arguments of a type family.
848 -- See Note [Dealing with :kind]
849 Nothing -> tc_infer_lhs_type mode hs_ty }
850
851 {- Note [Dealing with :kind]
852 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
853 Consider this GHCi command
854 ghci> type family F :: Either j k
855 ghci> :kind F
856 F :: forall {j,k}. Either j k
857
858 We will only get the 'forall' if we /refrain/ from saturating those
859 invisible binders. But generally we /do/ saturate those invisible
860 binders (see tcInferTyApps), and we want to do so for nested application
861 even in GHCi. Consider for example (#16287)
862 ghci> type family F :: k
863 ghci> data T :: (forall k. k) -> Type
864 ghci> :kind T F
865 We want to reject this. It's just at the very top level that we want
866 to switch off saturation.
867
868 So tcInferLHsTypeUnsaturated does a little special case for top level
869 applications. Actually the common case is a bare variable, as above.
870
871 Note [Do not always instantiate eagerly in types]
872 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
873 Terms are eagerly instantiated. This means that if you say
874
875 x = id
876
877 then `id` gets instantiated to have type alpha -> alpha. The variable
878 alpha is then unconstrained and regeneralized. But we cannot do this
879 in types, as we have no type-level lambda. So, when we are sure
880 that we will not want to regeneralize later -- because we are done
881 checking a type, for example -- we can instantiate. But we do not
882 instantiate at variables, nor do we in tcInferLHsTypeUnsaturated,
883 which is used by :kind in GHCi.
884
885 ************************************************************************
886 * *
887 Type-checking modes
888 * *
889 ************************************************************************
890
891 The kind-checker is parameterised by a TcTyMode, which contains some
892 information about where we're checking a type.
893
894 The renamer issues errors about what it can. All errors issued here must
895 concern things that the renamer can't handle.
896
897 -}
898
899 tcMult :: HsArrow GhcRn -> TcM Mult
900 tcMult hc = tc_mult typeLevelMode hc
901
902 -- | Info about the context in which we're checking a type. Currently,
903 -- differentiates only between types and kinds, but this will likely
904 -- grow, at least to include the distinction between patterns and
905 -- not-patterns.
906 --
907 -- To find out where the mode is used, search for 'mode_tyki'
908 --
909 -- This data type is purely local, not exported from this module
910 data TcTyMode
911 = TcTyMode { mode_tyki :: TypeOrKind
912 , mode_holes :: HoleInfo }
913
914 -- See Note [Levels for wildcards]
915 -- Nothing <=> no wildcards expected
916 type HoleInfo = Maybe (TcLevel, HoleMode)
917
918 -- HoleMode says how to treat the occurrences
919 -- of anonymous wildcards; see tcAnonWildCardOcc
920 data HoleMode = HM_Sig -- Partial type signatures: f :: _ -> Int
921 | HM_FamPat -- Family instances: F _ Int = Bool
922 | HM_VTA -- Visible type and kind application:
923 -- f @(Maybe _)
924 -- Maybe @(_ -> _)
925 | HM_TyAppPat -- Visible type applications in patterns:
926 -- foo (Con @_ @t x) = ...
927 -- case x of Con @_ @t v -> ...
928
929 mkMode :: TypeOrKind -> TcTyMode
930 mkMode tyki = TcTyMode { mode_tyki = tyki, mode_holes = Nothing }
931
932 typeLevelMode, kindLevelMode :: TcTyMode
933 -- These modes expect no wildcards (holes) in the type
934 kindLevelMode = mkMode KindLevel
935 typeLevelMode = mkMode TypeLevel
936
937 mkHoleMode :: TypeOrKind -> HoleMode -> TcM TcTyMode
938 mkHoleMode tyki hm
939 = do { lvl <- getTcLevel
940 ; return (TcTyMode { mode_tyki = tyki
941 , mode_holes = Just (lvl,hm) }) }
942
943 instance Outputable HoleMode where
944 ppr HM_Sig = text "HM_Sig"
945 ppr HM_FamPat = text "HM_FamPat"
946 ppr HM_VTA = text "HM_VTA"
947 ppr HM_TyAppPat = text "HM_TyAppPat"
948
949 instance Outputable TcTyMode where
950 ppr (TcTyMode { mode_tyki = tyki, mode_holes = hm })
951 = text "TcTyMode" <+> braces (sep [ ppr tyki <> comma
952 , ppr hm ])
953
954 {-
955 Note [Bidirectional type checking]
956 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
957 In expressions, whenever we see a polymorphic identifier, say `id`, we are
958 free to instantiate it with metavariables, knowing that we can always
959 re-generalize with type-lambdas when necessary. For example:
960
961 rank2 :: (forall a. a -> a) -> ()
962 x = rank2 id
963
964 When checking the body of `x`, we can instantiate `id` with a metavariable.
965 Then, when we're checking the application of `rank2`, we notice that we really
966 need a polymorphic `id`, and then re-generalize over the unconstrained
967 metavariable.
968
969 In types, however, we're not so lucky, because *we cannot re-generalize*!
970 There is no lambda. So, we must be careful only to instantiate at the last
971 possible moment, when we're sure we're never going to want the lost polymorphism
972 again. This is done in calls to tcInstInvisibleTyBinders.
973
974 To implement this behavior, we use bidirectional type checking, where we
975 explicitly think about whether we know the kind of the type we're checking
976 or not. Note that there is a difference between not knowing a kind and
977 knowing a metavariable kind: the metavariables are TauTvs, and cannot become
978 forall-quantified kinds. Previously (before dependent types), there were
979 no higher-rank kinds, and so we could instantiate early and be sure that
980 no types would have polymorphic kinds, and so we could always assume that
981 the kind of a type was a fresh metavariable. Not so anymore, thus the
982 need for two algorithms.
983
984 For HsType forms that can never be kind-polymorphic, we implement only the
985 "down" direction, where we safely assume a metavariable kind. For HsType forms
986 that *can* be kind-polymorphic, we implement just the "up" (functions with
987 "infer" in their name) version, as we gain nothing by also implementing the
988 "down" version.
989
990 Note [Future-proofing the type checker]
991 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
992 As discussed in Note [Bidirectional type checking], each HsType form is
993 handled in *either* tc_infer_hs_type *or* tc_hs_type. These functions
994 are mutually recursive, so that either one can work for any type former.
995 But, we want to make sure that our pattern-matches are complete. So,
996 we have a bunch of repetitive code just so that we get warnings if we're
997 missing any patterns.
998
999 -}
1000
1001 ------------------------------------------
1002 -- | Check and desugar a type, returning the core type and its
1003 -- possibly-polymorphic kind. Much like 'tcInferRho' at the expression
1004 -- level.
1005 tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
1006 tc_infer_lhs_type mode (L span ty)
1007 = setSrcSpanA span $
1008 tc_infer_hs_type mode ty
1009
1010 ---------------------------
1011 -- | Call 'tc_infer_hs_type' and check its result against an expected kind.
1012 tc_infer_hs_type_ek :: HasDebugCallStack => TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
1013 tc_infer_hs_type_ek mode hs_ty ek
1014 = do { (ty, k) <- tc_infer_hs_type mode hs_ty
1015 ; checkExpectedKind hs_ty ty k ek }
1016
1017 ---------------------------
1018 -- | Infer the kind of a type and desugar. This is the "up" type-checker,
1019 -- as described in Note [Bidirectional type checking]
1020 tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
1021
1022 tc_infer_hs_type mode (HsParTy _ t)
1023 = tc_infer_lhs_type mode t
1024
1025 tc_infer_hs_type mode ty
1026 | Just (hs_fun_ty, hs_args) <- splitHsAppTys ty
1027 = do { (fun_ty, _ki) <- tcInferTyAppHead mode hs_fun_ty
1028 ; tcInferTyApps mode hs_fun_ty fun_ty hs_args }
1029
1030 tc_infer_hs_type mode (HsKindSig _ ty sig)
1031 = do { let mode' = mode { mode_tyki = KindLevel }
1032 ; sig' <- tc_lhs_kind_sig mode' KindSigCtxt sig
1033 -- We must typecheck the kind signature, and solve all
1034 -- its equalities etc; from this point on we may do
1035 -- things like instantiate its foralls, so it needs
1036 -- to be fully determined (#14904)
1037 ; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
1038 ; ty' <- tc_lhs_type mode ty sig'
1039 ; return (ty', sig') }
1040
1041 -- HsSpliced is an annotation produced by 'GHC.Rename.Splice.rnSpliceType' to communicate
1042 -- the splice location to the typechecker. Here we skip over it in order to have
1043 -- the same kind inferred for a given expression whether it was produced from
1044 -- splices or not.
1045 --
1046 -- See Note [Delaying modFinalizers in untyped splices].
1047 tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty)))
1048 = tc_infer_hs_type mode ty
1049
1050 tc_infer_hs_type mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty
1051
1052 -- See Note [Typechecking HsCoreTys]
1053 tc_infer_hs_type _ (XHsType ty)
1054 = do env <- getLclEnv
1055 -- Raw uniques since we go from NameEnv to TvSubstEnv.
1056 let subst_prs :: [(Unique, TcTyVar)]
1057 subst_prs = [ (getUnique nm, tv)
1058 | ATyVar nm tv <- nonDetNameEnvElts (tcl_env env) ]
1059 subst = mkTvSubst
1060 (mkInScopeSet $ mkVarSet $ map snd subst_prs)
1061 (listToUFM_Directly $ map (liftSnd mkTyVarTy) subst_prs)
1062 ty' = substTy subst ty
1063 return (ty', tcTypeKind ty')
1064
1065 tc_infer_hs_type _ (HsExplicitListTy _ _ tys)
1066 | null tys -- this is so that we can use visible kind application with '[]
1067 -- e.g ... '[] @Bool
1068 = return (mkTyConTy promotedNilDataCon,
1069 mkSpecForAllTys [alphaTyVar] $ mkListTy alphaTy)
1070
1071 tc_infer_hs_type mode other_ty
1072 = do { kv <- newMetaKindVar
1073 ; ty' <- tc_hs_type mode other_ty kv
1074 ; return (ty', kv) }
1075
1076 {-
1077 Note [Typechecking HsCoreTys]
1078 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1079 HsCoreTy is an escape hatch that allows embedding Core Types in HsTypes.
1080 As such, there's not much to be done in order to typecheck an HsCoreTy,
1081 since it's already been typechecked to some extent. There is one thing that
1082 we must do, however: we must substitute the type variables from the tcl_env.
1083 To see why, consider GeneralizedNewtypeDeriving, which is one of the main
1084 clients of HsCoreTy (example adapted from #14579):
1085
1086 newtype T a = MkT a deriving newtype Eq
1087
1088 This will produce an InstInfo GhcPs that looks roughly like this:
1089
1090 instance forall a_1. Eq a_1 => Eq (T a_1) where
1091 (==) = coerce @( a_1 -> a_1 -> Bool) -- The type within @(...) is an HsCoreTy
1092 @(T a_1 -> T a_1 -> Bool) -- So is this
1093 (==)
1094
1095 This is then fed into the renamer. Since all of the type variables in this
1096 InstInfo use Exact RdrNames, the resulting InstInfo GhcRn looks basically
1097 identical. Things get more interesting when the InstInfo is fed into the
1098 typechecker, however. GHC will first generate fresh skolems to instantiate
1099 the instance-bound type variables with. In the example above, we might generate
1100 the skolem a_2 and use that to instantiate a_1, which extends the local type
1101 environment (tcl_env) with [a_1 :-> a_2]. This gives us:
1102
1103 instance forall a_2. Eq a_2 => Eq (T a_2) where ...
1104
1105 To ensure that the body of this instance is well scoped, every occurrence of
1106 the `a` type variable should refer to a_2, the new skolem. However, the
1107 HsCoreTys mention a_1, not a_2. Luckily, the tcl_env provides exactly the
1108 substitution we need ([a_1 :-> a_2]) to fix up the scoping. We apply this
1109 substitution to each HsCoreTy and all is well:
1110
1111 instance forall a_2. Eq a_2 => Eq (T a_2) where
1112 (==) = coerce @( a_2 -> a_2 -> Bool)
1113 @(T a_2 -> T a_2 -> Bool)
1114 (==)
1115 -}
1116
1117 ------------------------------------------
1118 tcLHsType :: LHsType GhcRn -> TcKind -> TcM TcType
1119 tcLHsType hs_ty exp_kind
1120 = tc_lhs_type typeLevelMode hs_ty exp_kind
1121
1122 tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
1123 tc_lhs_type mode (L span ty) exp_kind
1124 = setSrcSpanA span $
1125 tc_hs_type mode ty exp_kind
1126
1127 tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
1128 -- See Note [Bidirectional type checking]
1129
1130 tc_hs_type mode (HsParTy _ ty) exp_kind = tc_lhs_type mode ty exp_kind
1131 tc_hs_type mode (HsDocTy _ ty _) exp_kind = tc_lhs_type mode ty exp_kind
1132 tc_hs_type _ ty@(HsBangTy _ bang _) _
1133 -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
1134 -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of
1135 -- bangs are invalid, so fail. (#7210, #14761)
1136 = do { let bangError err = failWith $ TcRnUnknownMessage $ mkPlainError noHints $
1137 text "Unexpected" <+> text err <+> text "annotation:" <+> ppr ty $$
1138 text err <+> text "annotation cannot appear nested inside a type"
1139 ; case bang of
1140 HsSrcBang _ SrcUnpack _ -> bangError "UNPACK"
1141 HsSrcBang _ SrcNoUnpack _ -> bangError "NOUNPACK"
1142 HsSrcBang _ NoSrcUnpack SrcLazy -> bangError "laziness"
1143 HsSrcBang _ _ _ -> bangError "strictness" }
1144 tc_hs_type _ ty@(HsRecTy {}) _
1145 -- Record types (which only show up temporarily in constructor
1146 -- signatures) should have been removed by now
1147 = failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
1148 (text "Record syntax is illegal here:" <+> ppr ty)
1149
1150 -- HsSpliced is an annotation produced by 'GHC.Rename.Splice.rnSpliceType'.
1151 -- Here we get rid of it and add the finalizers to the global environment
1152 -- while capturing the local environment.
1153 --
1154 -- See Note [Delaying modFinalizers in untyped splices].
1155 tc_hs_type mode (HsSpliceTy _ (HsSpliced _ mod_finalizers (HsSplicedTy ty)))
1156 exp_kind
1157 = do addModFinalizersWithLclEnv mod_finalizers
1158 tc_hs_type mode ty exp_kind
1159
1160 -- This should never happen; type splices are expanded by the renamer
1161 tc_hs_type _ ty@(HsSpliceTy {}) _exp_kind
1162 = failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
1163 (text "Unexpected type splice:" <+> ppr ty)
1164
1165 ---------- Functions and applications
1166 tc_hs_type mode (HsFunTy _ mult ty1 ty2) exp_kind
1167 = tc_fun_type mode mult ty1 ty2 exp_kind
1168
1169 tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind
1170 | op `hasKey` funTyConKey
1171 = tc_fun_type mode (HsUnrestrictedArrow noHsUniTok) ty1 ty2 exp_kind
1172
1173 --------- Foralls
1174 tc_hs_type mode (HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
1175 = do { (tv_bndrs, ty') <- tcTKTelescope mode tele $
1176 tc_lhs_type mode ty exp_kind
1177 -- Pass on the mode from the type, to any wildcards
1178 -- in kind signatures on the forall'd variables
1179 -- e.g. f :: _ -> Int -> forall (a :: _). blah
1180 -- Why exp_kind? See Note [Body kind of HsForAllTy]
1181
1182 -- Do not kind-generalise here! See Note [Kind generalisation]
1183
1184 ; return (mkForAllTys tv_bndrs ty') }
1185
1186 tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
1187 | null (unLoc ctxt)
1188 = tc_lhs_type mode rn_ty exp_kind
1189
1190 -- See Note [Body kind of a HsQualTy]
1191 | tcIsConstraintKind exp_kind
1192 = do { ctxt' <- tc_hs_context mode ctxt
1193 ; ty' <- tc_lhs_type mode rn_ty constraintKind
1194 ; return (mkPhiTy ctxt' ty') }
1195
1196 | otherwise
1197 = do { ctxt' <- tc_hs_context mode ctxt
1198
1199 ; ek <- newOpenTypeKind -- The body kind (result of the function) can
1200 -- be TYPE r, for any r, hence newOpenTypeKind
1201 ; ty' <- tc_lhs_type mode rn_ty ek
1202 ; checkExpectedKind (unLoc rn_ty) (mkPhiTy ctxt' ty')
1203 liftedTypeKind exp_kind }
1204
1205 --------- Lists, arrays, and tuples
1206 tc_hs_type mode rn_ty@(HsListTy _ elt_ty) exp_kind
1207 = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
1208 ; checkWiredInTyCon listTyCon
1209 ; checkExpectedKind rn_ty (mkListTy tau_ty) liftedTypeKind exp_kind }
1210
1211 -- See Note [Distinguishing tuple kinds] in GHC.Hs.Type
1212 -- See Note [Inferring tuple kinds]
1213 tc_hs_type mode rn_ty@(HsTupleTy _ HsBoxedOrConstraintTuple hs_tys) exp_kind
1214 -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
1215 | Just tup_sort <- tupKindSort_maybe exp_kind
1216 = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
1217 tc_tuple rn_ty mode tup_sort hs_tys exp_kind
1218 | otherwise
1219 = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
1220 ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys
1221 ; kinds <- mapM zonkTcType kinds
1222 -- Infer each arg type separately, because errors can be
1223 -- confusing if we give them a shared kind. Eg #7410
1224 -- (Either Int, Int), we do not want to get an error saying
1225 -- "the second argument of a tuple should have kind *->*"
1226
1227 ; let (arg_kind, tup_sort)
1228 = case [ (k,s) | k <- kinds
1229 , Just s <- [tupKindSort_maybe k] ] of
1230 ((k,s) : _) -> (k,s)
1231 [] -> (liftedTypeKind, BoxedTuple)
1232 -- In the [] case, it's not clear what the kind is, so guess *
1233
1234 ; tys' <- sequence [ setSrcSpanA loc $
1235 checkExpectedKind hs_ty ty kind arg_kind
1236 | ((L loc hs_ty),ty,kind) <- zip3 hs_tys tys kinds ]
1237
1238 ; finish_tuple rn_ty tup_sort tys' (map (const arg_kind) tys') exp_kind }
1239
1240
1241 tc_hs_type mode rn_ty@(HsTupleTy _ HsUnboxedTuple tys) exp_kind
1242 = tc_tuple rn_ty mode UnboxedTuple tys exp_kind
1243
1244 tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind
1245 = do { let arity = length hs_tys
1246 ; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
1247 ; tau_tys <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
1248 ; let arg_reps = map kindRep arg_kinds
1249 arg_tys = arg_reps ++ tau_tys
1250 sum_ty = mkTyConApp (sumTyCon arity) arg_tys
1251 sum_kind = unboxedSumKind arg_reps
1252 ; checkExpectedKind rn_ty sum_ty sum_kind exp_kind
1253 }
1254
1255 --------- Promoted lists and tuples
1256 tc_hs_type mode rn_ty@(HsExplicitListTy _ _ tys) exp_kind
1257 = do { tks <- mapM (tc_infer_lhs_type mode) tys
1258 ; (taus', kind) <- unifyKinds tys tks
1259 ; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
1260 ; checkExpectedKind rn_ty ty (mkListTy kind) exp_kind }
1261 where
1262 mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
1263 mk_nil k = mkTyConApp (promoteDataCon nilDataCon) [k]
1264
1265 tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
1266 -- using newMetaKindVar means that we force instantiations of any polykinded
1267 -- types. At first, I just used tc_infer_lhs_type, but that led to #11255.
1268 = do { ks <- replicateM arity newMetaKindVar
1269 ; taus <- zipWithM (tc_lhs_type mode) tys ks
1270 ; let kind_con = tupleTyCon Boxed arity
1271 ty_con = promotedTupleDataCon Boxed arity
1272 tup_k = mkTyConApp kind_con ks
1273 ; checkTupSize arity
1274 ; checkExpectedKind rn_ty (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
1275 where
1276 arity = length tys
1277
1278 --------- Constraint types
1279 tc_hs_type mode rn_ty@(HsIParamTy _ (L _ n) ty) exp_kind
1280 = do { massert (isTypeLevel (mode_tyki mode))
1281 ; ty' <- tc_lhs_type mode ty liftedTypeKind
1282 ; let n' = mkStrLitTy $ hsIPNameFS n
1283 ; ipClass <- tcLookupClass ipClassName
1284 ; checkExpectedKind rn_ty (mkClassPred ipClass [n',ty'])
1285 constraintKind exp_kind }
1286
1287 tc_hs_type _ rn_ty@(HsStarTy _ _) exp_kind
1288 -- Desugaring 'HsStarTy' to 'Data.Kind.Type' here means that we don't have to
1289 -- handle it in 'coreView' and 'tcView'.
1290 = checkExpectedKind rn_ty liftedTypeKind liftedTypeKind exp_kind
1291
1292 --------- Literals
1293 tc_hs_type _ rn_ty@(HsTyLit _ (HsNumTy _ n)) exp_kind
1294 = do { checkWiredInTyCon naturalTyCon
1295 ; checkExpectedKind rn_ty (mkNumLitTy n) naturalTy exp_kind }
1296
1297 tc_hs_type _ rn_ty@(HsTyLit _ (HsStrTy _ s)) exp_kind
1298 = do { checkWiredInTyCon typeSymbolKindCon
1299 ; checkExpectedKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
1300 tc_hs_type _ rn_ty@(HsTyLit _ (HsCharTy _ c)) exp_kind
1301 = do { checkWiredInTyCon charTyCon
1302 ; checkExpectedKind rn_ty (mkCharLitTy c) charTy exp_kind }
1303
1304 --------- Wildcards
1305
1306 tc_hs_type mode ty@(HsWildCardTy _) ek
1307 = tcAnonWildCardOcc NoExtraConstraint mode ty ek
1308
1309 --------- Potentially kind-polymorphic types: call the "up" checker
1310 -- See Note [Future-proofing the type checker]
1311 tc_hs_type mode ty@(HsTyVar {}) ek = tc_infer_hs_type_ek mode ty ek
1312 tc_hs_type mode ty@(HsAppTy {}) ek = tc_infer_hs_type_ek mode ty ek
1313 tc_hs_type mode ty@(HsAppKindTy{}) ek = tc_infer_hs_type_ek mode ty ek
1314 tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek
1315 tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
1316 tc_hs_type mode ty@(XHsType {}) ek = tc_infer_hs_type_ek mode ty ek
1317
1318 {-
1319 Note [Variable Specificity and Forall Visibility]
1320 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1321 A HsForAllTy contains an HsForAllTelescope to denote the visibility of the forall
1322 binder. Furthermore, each invisible type variable binder also has a
1323 Specificity. Together, these determine the variable binders (ArgFlag) for each
1324 variable in the generated ForAllTy type.
1325
1326 This table summarises this relation:
1327 ----------------------------------------------------------------------------
1328 | User-written type HsForAllTelescope Specificity ArgFlag
1329 |---------------------------------------------------------------------------
1330 | f :: forall a. type HsForAllInvis SpecifiedSpec Specified
1331 | f :: forall {a}. type HsForAllInvis InferredSpec Inferred
1332 | f :: forall a -> type HsForAllVis SpecifiedSpec Required
1333 | f :: forall {a} -> type HsForAllVis InferredSpec /
1334 | This last form is non-sensical and is thus rejected.
1335 ----------------------------------------------------------------------------
1336
1337 For more information regarding the interpretation of the resulting ArgFlag, see
1338 Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in "GHC.Core.TyCo.Rep".
1339 -}
1340
1341 ------------------------------------------
1342 tc_mult :: TcTyMode -> HsArrow GhcRn -> TcM Mult
1343 tc_mult mode ty = tc_lhs_type mode (arrowToHsType ty) multiplicityTy
1344 ------------------------------------------
1345 tc_fun_type :: TcTyMode -> HsArrow GhcRn -> LHsType GhcRn -> LHsType GhcRn -> TcKind
1346 -> TcM TcType
1347 tc_fun_type mode mult ty1 ty2 exp_kind = case mode_tyki mode of
1348 TypeLevel ->
1349 do { arg_k <- newOpenTypeKind
1350 ; res_k <- newOpenTypeKind
1351 ; ty1' <- tc_lhs_type mode ty1 arg_k
1352 ; ty2' <- tc_lhs_type mode ty2 res_k
1353 ; mult' <- tc_mult mode mult
1354 ; checkExpectedKind (HsFunTy noAnn mult ty1 ty2) (mkVisFunTy mult' ty1' ty2')
1355 liftedTypeKind exp_kind }
1356 KindLevel -> -- no representation polymorphism in kinds. yet.
1357 do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
1358 ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
1359 ; mult' <- tc_mult mode mult
1360 ; checkExpectedKind (HsFunTy noAnn mult ty1 ty2) (mkVisFunTy mult' ty1' ty2')
1361 liftedTypeKind exp_kind }
1362
1363 {- Note [Skolem escape and forall-types]
1364 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1365 See also Note [Checking telescopes].
1366
1367 Consider
1368 f :: forall a. (forall kb (b :: kb). Proxy '[a, b]) -> ()
1369
1370 The Proxy '[a,b] forces a and b to have the same kind. But a's
1371 kind must be bound outside the 'forall a', and hence escapes.
1372 We discover this by building an implication constraint for
1373 each forall. So the inner implication constraint will look like
1374 forall kb (b::kb). kb ~ ka
1375 where ka is a's kind. We can't unify these two, /even/ if ka is
1376 unification variable, because it would be untouchable inside
1377 this inner implication.
1378
1379 That's what the pushLevelAndCaptureConstraints, plus subsequent
1380 buildTvImplication/emitImplication is all about, when kind-checking
1381 HsForAllTy.
1382
1383 Note that
1384
1385 * We don't need to /simplify/ the constraints here
1386 because we aren't generalising. We just capture them.
1387
1388 * We can't use emitResidualTvConstraint, because that has a fast-path
1389 for empty constraints. We can't take that fast path here, because
1390 we must do the bad-telescope check even if there are no inner wanted
1391 constraints. See Note [Checking telescopes] in
1392 GHC.Tc.Types.Constraint. Lacking this check led to #16247.
1393 -}
1394
1395 {- *********************************************************************
1396 * *
1397 Tuples
1398 * *
1399 ********************************************************************* -}
1400
1401 ---------------------------
1402 tupKindSort_maybe :: TcKind -> Maybe TupleSort
1403 tupKindSort_maybe k
1404 | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k'
1405 | Just k' <- tcView k = tupKindSort_maybe k'
1406 | tcIsConstraintKind k = Just ConstraintTuple
1407 | tcIsLiftedTypeKind k = Just BoxedTuple
1408 | otherwise = Nothing
1409
1410 tc_tuple :: HsType GhcRn -> TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
1411 tc_tuple rn_ty mode tup_sort tys exp_kind
1412 = do { arg_kinds <- case tup_sort of
1413 BoxedTuple -> return (replicate arity liftedTypeKind)
1414 UnboxedTuple -> replicateM arity newOpenTypeKind
1415 ConstraintTuple -> return (replicate arity constraintKind)
1416 ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
1417 ; finish_tuple rn_ty tup_sort tau_tys arg_kinds exp_kind }
1418 where
1419 arity = length tys
1420
1421 finish_tuple :: HsType GhcRn
1422 -> TupleSort
1423 -> [TcType] -- ^ argument types
1424 -> [TcKind] -- ^ of these kinds
1425 -> TcKind -- ^ expected kind of the whole tuple
1426 -> TcM TcType
1427 finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind = do
1428 traceTc "finish_tuple" (ppr tup_sort $$ ppr tau_kinds $$ ppr exp_kind)
1429 case tup_sort of
1430 ConstraintTuple
1431 | [tau_ty] <- tau_tys
1432 -- Drop any uses of 1-tuple constraints here.
1433 -- See Note [Ignore unary constraint tuples]
1434 -> check_expected_kind tau_ty constraintKind
1435 | otherwise
1436 -> do let tycon = cTupleTyCon arity
1437 checkCTupSize arity
1438 check_expected_kind (mkTyConApp tycon tau_tys) constraintKind
1439 BoxedTuple -> do
1440 let tycon = tupleTyCon Boxed arity
1441 checkTupSize arity
1442 checkWiredInTyCon tycon
1443 check_expected_kind (mkTyConApp tycon tau_tys) liftedTypeKind
1444 UnboxedTuple -> do
1445 let tycon = tupleTyCon Unboxed arity
1446 tau_reps = map kindRep tau_kinds
1447 -- See also Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
1448 arg_tys = tau_reps ++ tau_tys
1449 res_kind = unboxedTupleKind tau_reps
1450 checkTupSize arity
1451 check_expected_kind (mkTyConApp tycon arg_tys) res_kind
1452 where
1453 arity = length tau_tys
1454 check_expected_kind ty act_kind =
1455 checkExpectedKind rn_ty ty act_kind exp_kind
1456
1457 {-
1458 Note [Ignore unary constraint tuples]
1459 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1460 GHC provides unary tuples and unboxed tuples (see Note [One-tuples] in
1461 GHC.Builtin.Types) but does *not* provide unary constraint tuples. Why? First,
1462 recall the definition of a unary tuple data type:
1463
1464 data Solo a = Solo a
1465
1466 Note that `Solo a` is *not* the same thing as `a`, since Solo is boxed and
1467 lazy. Therefore, the presence of `Solo` matters semantically. On the other
1468 hand, suppose we had a unary constraint tuple:
1469
1470 class a => Solo% a
1471
1472 This compiles down a newtype (i.e., a cast) in Core, so `Solo% a` is
1473 semantically equivalent to `a`. Therefore, a 1-tuple constraint would have
1474 no user-visible impact, nor would it allow you to express anything that
1475 you couldn't otherwise.
1476
1477 We could simply add Solo% for consistency with tuples (Solo) and unboxed
1478 tuples (Solo#), but that would require even more magic to wire in another
1479 magical class, so we opt not to do so. We must be careful, however, since
1480 one can try to sneak in uses of unary constraint tuples through Template
1481 Haskell, such as in this program (from #17511):
1482
1483 f :: $(pure (ForallT [] [TupleT 1 `AppT` (ConT ''Show `AppT` ConT ''Int)]
1484 (ConT ''String)))
1485 -- f :: Solo% (Show Int) => String
1486 f = "abc"
1487
1488 This use of `TupleT 1` will produce an HsBoxedOrConstraintTuple of arity 1,
1489 and since it is used in a Constraint position, GHC will attempt to treat
1490 it as thought it were a constraint tuple, which can potentially lead to
1491 trouble if one attempts to look up the name of a constraint tuple of arity
1492 1 (as it won't exist). To avoid this trouble, we simply take any unary
1493 constraint tuples discovered when typechecking and drop them—i.e., treat
1494 "Solo% a" as though the user had written "a". This is always safe to do
1495 since the two constraints should be semantically equivalent.
1496 -}
1497
1498 {- *********************************************************************
1499 * *
1500 Type applications
1501 * *
1502 ********************************************************************* -}
1503
1504 splitHsAppTys :: HsType GhcRn -> Maybe (LHsType GhcRn, [LHsTypeArg GhcRn])
1505 splitHsAppTys hs_ty
1506 | is_app hs_ty = Just (go (noLocA hs_ty) [])
1507 | otherwise = Nothing
1508 where
1509 is_app :: HsType GhcRn -> Bool
1510 is_app (HsAppKindTy {}) = True
1511 is_app (HsAppTy {}) = True
1512 is_app (HsOpTy _ _ (L _ op) _) = not (op `hasKey` funTyConKey)
1513 -- I'm not sure why this funTyConKey test is necessary
1514 -- Can it even happen? Perhaps for t1 `(->)` t2
1515 -- but then maybe it's ok to treat that like a normal
1516 -- application rather than using the special rule for HsFunTy
1517 is_app (HsTyVar {}) = True
1518 is_app (HsParTy _ (L _ ty)) = is_app ty
1519 is_app _ = False
1520
1521 go :: LHsType GhcRn
1522 -> [HsArg (LHsType GhcRn) (LHsKind GhcRn)]
1523 -> (LHsType GhcRn,
1524 [HsArg (LHsType GhcRn) (LHsKind GhcRn)]) -- AZ temp
1525 go (L _ (HsAppTy _ f a)) as = go f (HsValArg a : as)
1526 go (L _ (HsAppKindTy l ty k)) as = go ty (HsTypeArg l k : as)
1527 go (L sp (HsParTy _ f)) as = go f (HsArgPar (locA sp) : as)
1528 go (L _ (HsOpTy _ l op@(L sp _) r)) as
1529 = ( L (na2la sp) (HsTyVar noAnn NotPromoted op)
1530 , HsValArg l : HsValArg r : as )
1531 go f as = (f, as)
1532
1533 ---------------------------
1534 tcInferTyAppHead :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
1535 -- Version of tc_infer_lhs_type specialised for the head of an
1536 -- application. In particular, for a HsTyVar (which includes type
1537 -- constructors, it does not zoom off into tcInferTyApps and family
1538 -- saturation
1539 tcInferTyAppHead mode (L _ (HsTyVar _ _ (L _ tv)))
1540 = tcTyVar mode tv
1541 tcInferTyAppHead mode ty
1542 = tc_infer_lhs_type mode ty
1543
1544 ---------------------------
1545 -- | Apply a type of a given kind to a list of arguments. This instantiates
1546 -- invisible parameters as necessary. Always consumes all the arguments,
1547 -- using matchExpectedFunKind as necessary.
1548 -- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.-
1549 -- These kinds should be used to instantiate invisible kind variables;
1550 -- they come from an enclosing class for an associated type/data family.
1551 --
1552 -- tcInferTyApps also arranges to saturate any trailing invisible arguments
1553 -- of a type-family application, which is usually the right thing to do
1554 -- tcInferTyApps_nosat does not do this saturation; it is used only
1555 -- by ":kind" in GHCi
1556 tcInferTyApps, tcInferTyApps_nosat
1557 :: TcTyMode
1558 -> LHsType GhcRn -- ^ Function (for printing only)
1559 -> TcType -- ^ Function
1560 -> [LHsTypeArg GhcRn] -- ^ Args
1561 -> TcM (TcType, TcKind) -- ^ (f args, args, result kind)
1562 tcInferTyApps mode hs_ty fun hs_args
1563 = do { (f_args, res_k) <- tcInferTyApps_nosat mode hs_ty fun hs_args
1564 ; saturateFamApp f_args res_k }
1565
1566 tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
1567 = do { traceTc "tcInferTyApps {" (ppr orig_hs_ty $$ ppr orig_hs_args)
1568 ; (f_args, res_k) <- go_init 1 fun orig_hs_args
1569 ; traceTc "tcInferTyApps }" (ppr f_args <+> dcolon <+> ppr res_k)
1570 ; return (f_args, res_k) }
1571 where
1572
1573 -- go_init just initialises the auxiliary
1574 -- arguments of the 'go' loop
1575 go_init n fun all_args
1576 = go n fun empty_subst fun_ki all_args
1577 where
1578 fun_ki = tcTypeKind fun
1579 -- We do (tcTypeKind fun) here, even though the caller
1580 -- knows the function kind, to absolutely guarantee
1581 -- INVARIANT for 'go'
1582 -- Note that in a typical application (F t1 t2 t3),
1583 -- the 'fun' is just a TyCon, so tcTypeKind is fast
1584
1585 empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
1586 tyCoVarsOfType fun_ki
1587
1588 go :: Int -- The # of the next argument
1589 -> TcType -- Function applied to some args
1590 -> TCvSubst -- Applies to function kind
1591 -> TcKind -- Function kind
1592 -> [LHsTypeArg GhcRn] -- Un-type-checked args
1593 -> TcM (TcType, TcKind) -- Result type and its kind
1594 -- INVARIANT: in any call (go n fun subst fun_ki args)
1595 -- tcTypeKind fun = subst(fun_ki)
1596 -- So the 'subst' and 'fun_ki' arguments are simply
1597 -- there to avoid repeatedly calling tcTypeKind.
1598 --
1599 -- Reason for INVARIANT: to support the Purely Kinded Type Invariant
1600 -- it's important that if fun_ki has a forall, then so does
1601 -- (tcTypeKind fun), because the next thing we are going to do
1602 -- is apply 'fun' to an argument type.
1603
1604 -- Dispatch on all_args first, for performance reasons
1605 go n fun subst fun_ki all_args = case (all_args, tcSplitPiTy_maybe fun_ki) of
1606
1607 ---------------- No user-written args left. We're done!
1608 ([], _) -> return (fun, substTy subst fun_ki)
1609
1610 ---------------- HsArgPar: We don't care about parens here
1611 (HsArgPar _ : args, _) -> go n fun subst fun_ki args
1612
1613 ---------------- HsTypeArg: a kind application (fun @ki)
1614 (HsTypeArg _ hs_ki_arg : hs_args, Just (ki_binder, inner_ki)) ->
1615 case ki_binder of
1616
1617 -- FunTy with PredTy on LHS, or ForAllTy with Inferred
1618 Named (Bndr _ Inferred) -> instantiate ki_binder inner_ki
1619 Anon InvisArg _ -> instantiate ki_binder inner_ki
1620
1621 Named (Bndr _ Specified) -> -- Visible kind application
1622 do { traceTc "tcInferTyApps (vis kind app)"
1623 (vcat [ ppr ki_binder, ppr hs_ki_arg
1624 , ppr (tyBinderType ki_binder)
1625 , ppr subst ])
1626
1627 ; let exp_kind = substTy subst $ tyBinderType ki_binder
1628 ; arg_mode <- mkHoleMode KindLevel HM_VTA
1629 -- HM_VKA: see Note [Wildcards in visible kind application]
1630 ; ki_arg <- addErrCtxt (funAppCtxt orig_hs_ty hs_ki_arg n) $
1631 tc_lhs_type arg_mode hs_ki_arg exp_kind
1632
1633 ; traceTc "tcInferTyApps (vis kind app)" (ppr exp_kind)
1634 ; (subst', fun') <- mkAppTyM subst fun ki_binder ki_arg
1635 ; go (n+1) fun' subst' inner_ki hs_args }
1636
1637 -- Attempted visible kind application (fun @ki), but fun_ki is
1638 -- forall k -> blah or k1 -> k2
1639 -- So we need a normal application. Error.
1640 _ -> ty_app_err hs_ki_arg $ substTy subst fun_ki
1641
1642 -- No binder; try applying the substitution, or fail if that's not possible
1643 (HsTypeArg _ ki_arg : _, Nothing) -> try_again_after_substing_or $
1644 ty_app_err ki_arg substed_fun_ki
1645
1646 ---------------- HsValArg: a normal argument (fun ty)
1647 (HsValArg arg : args, Just (ki_binder, inner_ki))
1648 -- next binder is invisible; need to instantiate it
1649 | isInvisibleBinder ki_binder -- FunTy with InvisArg on LHS;
1650 -- or ForAllTy with Inferred or Specified
1651 -> instantiate ki_binder inner_ki
1652
1653 -- "normal" case
1654 | otherwise
1655 -> do { traceTc "tcInferTyApps (vis normal app)"
1656 (vcat [ ppr ki_binder
1657 , ppr arg
1658 , ppr (tyBinderType ki_binder)
1659 , ppr subst ])
1660 ; let exp_kind = substTy subst $ tyBinderType ki_binder
1661 ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
1662 tc_lhs_type mode arg exp_kind
1663 ; traceTc "tcInferTyApps (vis normal app) 2" (ppr exp_kind)
1664 ; (subst', fun') <- mkAppTyM subst fun ki_binder arg'
1665 ; go (n+1) fun' subst' inner_ki args }
1666
1667 -- no binder; try applying the substitution, or infer another arrow in fun kind
1668 (HsValArg _ : _, Nothing)
1669 -> try_again_after_substing_or $
1670 do { let arrows_needed = n_initial_val_args all_args
1671 ; co <- matchExpectedFunKind hs_ty arrows_needed substed_fun_ki
1672
1673 ; fun' <- zonkTcType (fun `mkTcCastTy` co)
1674 -- This zonk is essential, to expose the fruits
1675 -- of matchExpectedFunKind to the 'go' loop
1676
1677 ; traceTc "tcInferTyApps (no binder)" $
1678 vcat [ ppr fun <+> dcolon <+> ppr fun_ki
1679 , ppr arrows_needed
1680 , ppr co
1681 , ppr fun' <+> dcolon <+> ppr (tcTypeKind fun')]
1682 ; go_init n fun' all_args }
1683 -- Use go_init to establish go's INVARIANT
1684 where
1685 instantiate ki_binder inner_ki
1686 = do { traceTc "tcInferTyApps (need to instantiate)"
1687 (vcat [ ppr ki_binder, ppr subst])
1688 ; (subst', arg') <- tcInstInvisibleTyBinder subst ki_binder
1689 ; go n (mkAppTy fun arg') subst' inner_ki all_args }
1690 -- Because tcInvisibleTyBinder instantiate ki_binder,
1691 -- the kind of arg' will have the same shape as the kind
1692 -- of ki_binder. So we don't need mkAppTyM here.
1693
1694 try_again_after_substing_or fallthrough
1695 | not (isEmptyTCvSubst subst)
1696 = go n fun zapped_subst substed_fun_ki all_args
1697 | otherwise
1698 = fallthrough
1699
1700 zapped_subst = zapTCvSubst subst
1701 substed_fun_ki = substTy subst fun_ki
1702 hs_ty = appTypeToArg orig_hs_ty (take (n-1) orig_hs_args)
1703
1704 n_initial_val_args :: [HsArg tm ty] -> Arity
1705 -- Count how many leading HsValArgs we have
1706 n_initial_val_args (HsValArg {} : args) = 1 + n_initial_val_args args
1707 n_initial_val_args (HsArgPar {} : args) = n_initial_val_args args
1708 n_initial_val_args _ = 0
1709
1710 ty_app_err arg ty
1711 = failWith $ TcRnUnknownMessage $ mkPlainError noHints $
1712 text "Cannot apply function of kind" <+> quotes (ppr ty)
1713 $$ text "to visible kind argument" <+> quotes (ppr arg)
1714
1715
1716 mkAppTyM :: TCvSubst
1717 -> TcType -> TyCoBinder -- fun, plus its top-level binder
1718 -> TcType -- arg
1719 -> TcM (TCvSubst, TcType) -- Extended subst, plus (fun arg)
1720 -- Precondition: the application (fun arg) is well-kinded after zonking
1721 -- That is, the application makes sense
1722 --
1723 -- Precondition: for (mkAppTyM subst fun bndr arg)
1724 -- tcTypeKind fun = Pi bndr. body
1725 -- That is, fun always has a ForAllTy or FunTy at the top
1726 -- and 'bndr' is fun's pi-binder
1727 --
1728 -- Postcondition: if fun and arg satisfy (PKTI), the purely-kinded type
1729 -- invariant, then so does the result type (fun arg)
1730 --
1731 -- We do not require that
1732 -- tcTypeKind arg = tyVarKind (binderVar bndr)
1733 -- This must be true after zonking (precondition 1), but it's not
1734 -- required for the (PKTI).
1735 mkAppTyM subst fun ki_binder arg
1736 | -- See Note [mkAppTyM]: Nasty case 2
1737 TyConApp tc args <- fun
1738 , isTypeSynonymTyCon tc
1739 , args `lengthIs` (tyConArity tc - 1)
1740 , any isTrickyTvBinder (tyConTyVars tc) -- We could cache this in the synonym
1741 = do { arg' <- zonkTcType arg
1742 ; args' <- zonkTcTypes args
1743 ; let subst' = case ki_binder of
1744 Anon {} -> subst
1745 Named (Bndr tv _) -> extendTvSubstAndInScope subst tv arg'
1746 ; return (subst', mkTyConApp tc (args' ++ [arg'])) }
1747
1748
1749 mkAppTyM subst fun (Anon {}) arg
1750 = return (subst, mk_app_ty fun arg)
1751
1752 mkAppTyM subst fun (Named (Bndr tv _)) arg
1753 = do { arg' <- if isTrickyTvBinder tv
1754 then -- See Note [mkAppTyM]: Nasty case 1
1755 zonkTcType arg
1756 else return arg
1757 ; return ( extendTvSubstAndInScope subst tv arg'
1758 , mk_app_ty fun arg' ) }
1759
1760 mk_app_ty :: TcType -> TcType -> TcType
1761 -- This function just adds an ASSERT for mkAppTyM's precondition
1762 mk_app_ty fun arg
1763 = assertPpr (isPiTy fun_kind)
1764 (ppr fun <+> dcolon <+> ppr fun_kind $$ ppr arg) $
1765 mkAppTy fun arg
1766 where
1767 fun_kind = tcTypeKind fun
1768
1769 isTrickyTvBinder :: TcTyVar -> Bool
1770 -- NB: isTrickyTvBinder is just an optimisation
1771 -- It would be absolutely sound to return True always
1772 isTrickyTvBinder tv = isPiTy (tyVarKind tv)
1773
1774 {- Note [The Purely Kinded Type Invariant (PKTI)]
1775 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1776 During type inference, we maintain this invariant
1777
1778 (PKTI) It is legal to call 'tcTypeKind' on any Type ty,
1779 on any sub-term of ty, /without/ zonking ty
1780
1781 Moreover, any such returned kind
1782 will itself satisfy (PKTI)
1783
1784 By "legal to call tcTypeKind" we mean "tcTypeKind will not crash".
1785 The way in which tcTypeKind can crash is in applications
1786 (a t1 t2 .. tn)
1787 if 'a' is a type variable whose kind doesn't have enough arrows
1788 or foralls. (The crash is in piResultTys.)
1789
1790 The loop in tcInferTyApps has to be very careful to maintain the (PKTI).
1791 For example, suppose
1792 kappa is a unification variable
1793 We have already unified kappa := Type
1794 yielding co :: Refl (Type -> Type)
1795 a :: kappa
1796 then consider the type
1797 (a Int)
1798 If we call tcTypeKind on that, we'll crash, because the (un-zonked)
1799 kind of 'a' is just kappa, not an arrow kind. So we must zonk first.
1800
1801 So the type inference engine is very careful when building applications.
1802 This happens in tcInferTyApps. Suppose we are kind-checking the type (a Int),
1803 where (a :: kappa). Then in tcInferApps we'll run out of binders on
1804 a's kind, so we'll call matchExpectedFunKind, and unify
1805 kappa := kappa1 -> kappa2, with evidence co :: kappa ~ (kappa1 ~ kappa2)
1806 At this point we must zonk the function type to expose the arrrow, so
1807 that (a Int) will satisfy (PKTI).
1808
1809 The absence of this caused #14174 and #14520.
1810
1811 The calls to mkAppTyM is the other place we are very careful; see Note [mkAppTyM].
1812
1813 Wrinkle around FunTy:
1814 Note that the PKTI does *not* guarantee anything about the shape of FunTys.
1815 Specifically, when we have (FunTy vis mult arg res), it should be the case
1816 that arg :: TYPE rr1 and res :: TYPE rr2, for some rr1 and rr2. However, we
1817 might not have this. Example: if the user writes (a -> b), then we might
1818 invent a :: kappa1 and b :: kappa2. We soon will check whether kappa1 ~ TYPE rho1
1819 (for some rho1), and that will lead to kappa1 := TYPE rho1 (ditto for kappa2).
1820 However, when we build the FunTy, we might not have zonked `a`, and so the
1821 FunTy will be built without being able to purely extract the RuntimeReps.
1822
1823 Because the PKTI does not guarantee that the RuntimeReps are available in a FunTy,
1824 we must be aware of this when splitting: splitTyConApp and splitAppTy will *not*
1825 split a FunTy if the RuntimeReps are not available. See also Note [Decomposing FunTy]
1826 in GHC.Tc.Solver.Canonical.
1827
1828 Note [mkAppTyM]
1829 ~~~~~~~~~~~~~~~
1830 mkAppTyM is trying to guarantee the Purely Kinded Type Invariant
1831 (PKTI) for its result type (fun arg). There are two ways it can go wrong:
1832
1833 * Nasty case 1: forall types (polykinds/T14174a)
1834 T :: forall (p :: *->*). p Int -> p Bool
1835 Now kind-check (T x), where x::kappa.
1836 Well, T and x both satisfy the PKTI, but
1837 T x :: x Int -> x Bool
1838 and (x Int) does /not/ satisfy the PKTI.
1839
1840 * Nasty case 2: type synonyms
1841 type S f a = f a
1842 Even though (S ff aa) would satisfy the (PKTI) if S was a data type
1843 (i.e. nasty case 1 is dealt with), it might still not satisfy (PKTI)
1844 if S is a type synonym, because the /expansion/ of (S ff aa) is
1845 (ff aa), and /that/ does not satisfy (PKTI). E.g. perhaps
1846 (ff :: kappa), where 'kappa' has already been unified with (*->*).
1847
1848 We check for nasty case 2 on the final argument of a type synonym.
1849
1850 Notice that in both cases the trickiness only happens if the
1851 bound variable has a pi-type. Hence isTrickyTvBinder.
1852 -}
1853
1854
1855 saturateFamApp :: TcType -> TcKind -> TcM (TcType, TcKind)
1856 -- Precondition for (saturateFamApp ty kind):
1857 -- tcTypeKind ty = kind
1858 --
1859 -- If 'ty' is an unsaturated family application with trailing
1860 -- invisible arguments, instantiate them.
1861 -- See Note [saturateFamApp]
1862
1863 saturateFamApp ty kind
1864 | Just (tc, args) <- tcSplitTyConApp_maybe ty
1865 , mustBeSaturated tc
1866 , let n_to_inst = tyConArity tc - length args
1867 = do { (extra_args, ki') <- tcInstInvisibleTyBindersN n_to_inst kind
1868 ; return (ty `mkTcAppTys` extra_args, ki') }
1869 | otherwise
1870 = return (ty, kind)
1871
1872 {- Note [saturateFamApp]
1873 ~~~~~~~~~~~~~~~~~~~~~~~~
1874 Consider
1875 type family F :: Either j k
1876 type instance F @Type = Right Maybe
1877 type instance F @Type = Right Either```
1878
1879 Then F :: forall {j,k}. Either j k
1880
1881 The two type instances do a visible kind application that instantiates
1882 'j' but not 'k'. But we want to end up with instances that look like
1883 type instance F @Type @(*->*) = Right @Type @(*->*) Maybe
1884
1885 so that F has arity 2. We must instantiate that trailing invisible
1886 binder. In general, Invisible binders precede Specified and Required,
1887 so this is only going to bite for apparently-nullary families.
1888
1889 Note that
1890 type family F2 :: forall k. k -> *
1891 is quite different and really does have arity 0.
1892
1893 It's not just type instances where we need to saturate those
1894 unsaturated arguments: see #11246. Hence doing this in tcInferApps.
1895 -}
1896
1897 appTypeToArg :: LHsType GhcRn -> [LHsTypeArg GhcRn] -> LHsType GhcRn
1898 appTypeToArg f [] = f
1899 appTypeToArg f (HsValArg arg : args) = appTypeToArg (mkHsAppTy f arg) args
1900 appTypeToArg f (HsArgPar _ : args) = appTypeToArg f args
1901 appTypeToArg f (HsTypeArg l arg : args)
1902 = appTypeToArg (mkHsAppKindTy l f arg) args
1903
1904
1905 {- *********************************************************************
1906 * *
1907 checkExpectedKind
1908 * *
1909 ********************************************************************* -}
1910
1911 -- | This instantiates invisible arguments for the type being checked if it must
1912 -- be saturated and is not yet saturated. It then calls and uses the result
1913 -- from checkExpectedKindX to build the final type
1914 checkExpectedKind :: HasDebugCallStack
1915 => HsType GhcRn -- ^ type we're checking (for printing)
1916 -> TcType -- ^ type we're checking
1917 -> TcKind -- ^ the known kind of that type
1918 -> TcKind -- ^ the expected kind
1919 -> TcM TcType
1920 -- Just a convenience wrapper to save calls to 'ppr'
1921 checkExpectedKind hs_ty ty act_kind exp_kind
1922 = do { traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind)
1923
1924 ; (new_args, act_kind') <- tcInstInvisibleTyBindersN n_to_inst act_kind
1925
1926 ; let origin = TypeEqOrigin { uo_actual = act_kind'
1927 , uo_expected = exp_kind
1928 , uo_thing = Just (ppr hs_ty)
1929 , uo_visible = True } -- the hs_ty is visible
1930
1931 ; traceTc "checkExpectedKindX" $
1932 vcat [ ppr hs_ty
1933 , text "act_kind':" <+> ppr act_kind'
1934 , text "exp_kind:" <+> ppr exp_kind ]
1935
1936 ; let res_ty = ty `mkTcAppTys` new_args
1937
1938 ; if act_kind' `tcEqType` exp_kind
1939 then return res_ty -- This is very common
1940 else do { co_k <- uType KindLevel origin act_kind' exp_kind
1941 ; traceTc "checkExpectedKind" (vcat [ ppr act_kind
1942 , ppr exp_kind
1943 , ppr co_k ])
1944 ; return (res_ty `mkTcCastTy` co_k) } }
1945 where
1946 -- We need to make sure that both kinds have the same number of implicit
1947 -- foralls out front. If the actual kind has more, instantiate accordingly.
1948 -- Otherwise, just pass the type & kind through: the errors are caught
1949 -- in unifyType.
1950 n_exp_invis_bndrs = invisibleTyBndrCount exp_kind
1951 n_act_invis_bndrs = invisibleTyBndrCount act_kind
1952 n_to_inst = n_act_invis_bndrs - n_exp_invis_bndrs
1953
1954 ---------------------------
1955
1956 tcHsContext :: Maybe (LHsContext GhcRn) -> TcM [PredType]
1957 tcHsContext Nothing = return []
1958 tcHsContext (Just cxt) = tc_hs_context typeLevelMode cxt
1959
1960 tcLHsPredType :: LHsType GhcRn -> TcM PredType
1961 tcLHsPredType pred = tc_lhs_pred typeLevelMode pred
1962
1963 tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [PredType]
1964 tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt)
1965
1966 tc_lhs_pred :: TcTyMode -> LHsType GhcRn -> TcM PredType
1967 tc_lhs_pred mode pred = tc_lhs_type mode pred constraintKind
1968
1969 ---------------------------
1970 tcTyVar :: TcTyMode -> Name -> TcM (TcType, TcKind)
1971 -- See Note [Type checking recursive type and class declarations]
1972 -- in GHC.Tc.TyCl
1973 -- This does not instantiate. See Note [Do not always instantiate eagerly in types]
1974 tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
1975 = do { traceTc "lk1" (ppr name)
1976 ; thing <- tcLookup name
1977 ; case thing of
1978 ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)
1979
1980 -- See Note [Recursion through the kinds]
1981 ATcTyCon tc_tc
1982 -> do { check_tc tc_tc
1983 ; return (mkTyConTy tc_tc, tyConKind tc_tc) }
1984
1985 AGlobal (ATyCon tc)
1986 -> do { check_tc tc
1987 ; return (mkTyConTy tc, tyConKind tc) }
1988
1989 AGlobal (AConLike (RealDataCon dc))
1990 -> do { data_kinds <- xoptM LangExt.DataKinds
1991 ; unless (data_kinds || specialPromotedDc dc) $
1992 promotionErr name NoDataKindsDC
1993 ; when (isFamInstTyCon (dataConTyCon dc)) $
1994 -- see #15245
1995 promotionErr name FamDataConPE
1996 ; let (_, _, _, theta, _, _) = dataConFullSig dc
1997 ; traceTc "tcTyVar" (ppr dc <+> ppr theta $$ ppr (dc_theta_illegal_constraint theta))
1998 ; case dc_theta_illegal_constraint theta of
1999 Just pred -> promotionErr name $
2000 ConstrainedDataConPE pred
2001 Nothing -> pure ()
2002 ; let tc = promoteDataCon dc
2003 ; return (mkTyConApp tc [], tyConKind tc) }
2004
2005 APromotionErr err -> promotionErr name err
2006
2007 _ -> wrongThingErr "type" thing name }
2008 where
2009 check_tc :: TyCon -> TcM ()
2010 check_tc tc = do { data_kinds <- xoptM LangExt.DataKinds
2011 ; unless (isTypeLevel (mode_tyki mode) ||
2012 data_kinds ||
2013 isKindTyCon tc) $
2014 promotionErr name NoDataKindsTC }
2015
2016 -- We cannot promote a data constructor with a context that contains
2017 -- constraints other than equalities, so error if we find one.
2018 -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
2019 dc_theta_illegal_constraint :: ThetaType -> Maybe PredType
2020 dc_theta_illegal_constraint = find (not . isEqPred)
2021
2022 {-
2023 Note [Recursion through the kinds]
2024 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2025 Consider these examples
2026
2027 Ticket #11554:
2028 data P (x :: k) = Q
2029 data A :: Type where
2030 MkA :: forall (a :: A). P a -> A
2031
2032 Ticket #12174
2033 data V a
2034 data T = forall (a :: T). MkT (V a)
2035
2036 The type is recursive (which is fine) but it is recursive /through the
2037 kinds/. In earlier versions of GHC this caused a loop in the compiler
2038 (to do with knot-tying) but there is nothing fundamentally wrong with
2039 the code (kinds are types, and the recursive declarations are OK). But
2040 it's hard to distinguish "recursion through the kinds" from "recursion
2041 through the types". Consider this (also #11554):
2042
2043 data PB k (x :: k) = Q
2044 data B :: Type where
2045 MkB :: P B a -> B
2046
2047 Here the occurrence of B is not obviously in a kind position.
2048
2049 So now GHC allows all these programs. #12081 and #15942 are other
2050 examples.
2051
2052 Note [Body kind of a HsForAllTy]
2053 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2054 The body of a forall is usually a type, but in principle
2055 there's no reason to prohibit *unlifted* types.
2056 In fact, GHC can itself construct a function with an
2057 unboxed tuple inside a for-all (via CPR analysis; see
2058 typecheck/should_compile/tc170).
2059
2060 Moreover in instance heads we get forall-types with
2061 kind Constraint.
2062
2063 It's tempting to check that the body kind is either * or #. But this is
2064 wrong. For example:
2065
2066 class C a b
2067 newtype N = Mk Foo deriving (C a)
2068
2069 We're doing newtype-deriving for C. But notice how `a` isn't in scope in
2070 the predicate `C a`. So we quantify, yielding `forall a. C a` even though
2071 `C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but
2072 convenient. Bottom line: don't check for * or # here.
2073
2074 Note [Body kind of a HsQualTy]
2075 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2076 If ctxt is non-empty, the HsQualTy really is a /function/, so the
2077 kind of the result really is '*', and in that case the kind of the
2078 body-type can be lifted or unlifted.
2079
2080 However, consider
2081 instance Eq a => Eq [a] where ...
2082 or
2083 f :: (Eq a => Eq [a]) => blah
2084 Here both body-kind of the HsQualTy is Constraint rather than *.
2085 Rather crudely we tell the difference by looking at exp_kind. It's
2086 very convenient to typecheck instance types like any other HsSigType.
2087
2088 Admittedly the '(Eq a => Eq [a]) => blah' case is erroneous, but it's
2089 better to reject in checkValidType. If we say that the body kind
2090 should be '*' we risk getting TWO error messages, one saying that Eq
2091 [a] doesn't have kind '*', and one saying that we need a Constraint to
2092 the left of the outer (=>).
2093
2094 How do we figure out the right body kind? Well, it's a bit of a
2095 kludge: I just look at the expected kind. If it's Constraint, we
2096 must be in this instance situation context. It's a kludge because it
2097 wouldn't work if any unification was involved to compute that result
2098 kind -- but it isn't. (The true way might be to use the 'mode'
2099 parameter, but that seemed like a sledgehammer to crack a nut.)
2100
2101 Note [Inferring tuple kinds]
2102 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2103 Give a tuple type (a,b,c), which the parser labels as HsBoxedOrConstraintTuple,
2104 we try to figure out whether it's a tuple of kind * or Constraint.
2105 Step 1: look at the expected kind
2106 Step 2: infer argument kinds
2107
2108 If after Step 2 it's not clear from the arguments that it's
2109 Constraint, then it must be *. Once having decided that we re-check
2110 the arguments to give good error messages in
2111 e.g. (Maybe, Maybe)
2112
2113 Note that we will still fail to infer the correct kind in this case:
2114
2115 type T a = ((a,a), D a)
2116 type family D :: Constraint -> Constraint
2117
2118 While kind checking T, we do not yet know the kind of D, so we will default the
2119 kind of T to * -> *. It works if we annotate `a` with kind `Constraint`.
2120
2121 Note [Desugaring types]
2122 ~~~~~~~~~~~~~~~~~~~~~~~
2123 The type desugarer is phase 2 of dealing with HsTypes. Specifically:
2124
2125 * It transforms from HsType to Type
2126
2127 * It zonks any kinds. The returned type should have no mutable kind
2128 or type variables (hence returning Type not TcType):
2129 - any unconstrained kind variables are defaulted to (Any *) just
2130 as in GHC.Tc.Utils.Zonk.
2131 - there are no mutable type variables because we are
2132 kind-checking a type
2133 Reason: the returned type may be put in a TyCon or DataCon where
2134 it will never subsequently be zonked.
2135
2136 You might worry about nested scopes:
2137 ..a:kappa in scope..
2138 let f :: forall b. T '[a,b] -> Int
2139 In this case, f's type could have a mutable kind variable kappa in it;
2140 and we might then default it to (Any *) when dealing with f's type
2141 signature. But we don't expect this to happen because we can't get a
2142 lexically scoped type variable with a mutable kind variable in it. A
2143 delicate point, this. If it becomes an issue we might need to
2144 distinguish top-level from nested uses.
2145
2146 Moreover
2147 * it cannot fail,
2148 * it does no unifications
2149 * it does no validity checking, except for structural matters, such as
2150 (a) spurious ! annotations.
2151 (b) a class used as a type
2152
2153 Note [Kind of a type splice]
2154 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2155 Consider these terms, each with TH type splice inside:
2156 [| e1 :: Maybe $(..blah..) |]
2157 [| e2 :: $(..blah..) |]
2158 When kind-checking the type signature, we'll kind-check the splice
2159 $(..blah..); we want to give it a kind that can fit in any context,
2160 as if $(..blah..) :: forall k. k.
2161
2162 In the e1 example, the context of the splice fixes kappa to *. But
2163 in the e2 example, we'll desugar the type, zonking the kind unification
2164 variables as we go. When we encounter the unconstrained kappa, we
2165 want to default it to '*', not to (Any *).
2166
2167 -}
2168
2169 addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a
2170 -- Wrap a context around only if we want to show that contexts.
2171 -- Omit invisible ones and ones user's won't grok
2172 addTypeCtxt (L _ (HsWildCardTy _)) thing = thing -- "In the type '_'" just isn't helpful.
2173 addTypeCtxt (L _ ty) thing
2174 = addErrCtxt doc thing
2175 where
2176 doc = text "In the type" <+> quotes (ppr ty)
2177
2178
2179 {- *********************************************************************
2180 * *
2181 Type-variable binders
2182 * *
2183 ********************************************************************* -}
2184
2185 bindNamedWildCardBinders :: [Name]
2186 -> ([(Name, TcTyVar)] -> TcM a)
2187 -> TcM a
2188 -- Bring into scope the /named/ wildcard binders. Remember that
2189 -- plain wildcards _ are anonymous and dealt with by HsWildCardTy
2190 -- Soe Note [The wildcard story for types] in GHC.Hs.Type
2191 bindNamedWildCardBinders wc_names thing_inside
2192 = do { wcs <- mapM newNamedWildTyVar wc_names
2193 ; let wc_prs = wc_names `zip` wcs
2194 ; tcExtendNameTyVarEnv wc_prs $
2195 thing_inside wc_prs }
2196
2197 newNamedWildTyVar :: Name -> TcM TcTyVar
2198 -- ^ New unification variable '_' for a wildcard
2199 newNamedWildTyVar _name -- Currently ignoring the "_x" wildcard name used in the type
2200 = do { kind <- newMetaKindVar
2201 ; details <- newMetaDetails TauTv
2202 ; wc_name <- newMetaTyVarName (fsLit "w") -- See Note [Wildcard names]
2203 ; let tyvar = mkTcTyVar wc_name kind details
2204 ; traceTc "newWildTyVar" (ppr tyvar)
2205 ; return tyvar }
2206
2207 ---------------------------
2208 tcAnonWildCardOcc :: IsExtraConstraint
2209 -> TcTyMode -> HsType GhcRn -> Kind -> TcM TcType
2210 tcAnonWildCardOcc is_extra (TcTyMode { mode_holes = Just (hole_lvl, hole_mode) })
2211 ty exp_kind
2212 -- hole_lvl: see Note [Checking partial type signatures]
2213 -- esp the bullet on nested forall types
2214 = do { kv_details <- newTauTvDetailsAtLevel hole_lvl
2215 ; kv_name <- newMetaTyVarName (fsLit "k")
2216 ; wc_details <- newTauTvDetailsAtLevel hole_lvl
2217 ; wc_name <- newMetaTyVarName (fsLit wc_nm)
2218 ; let kv = mkTcTyVar kv_name liftedTypeKind kv_details
2219 wc_kind = mkTyVarTy kv
2220 wc_tv = mkTcTyVar wc_name wc_kind wc_details
2221
2222 ; traceTc "tcAnonWildCardOcc" (ppr hole_lvl <+> ppr emit_holes)
2223 ; when emit_holes $
2224 emitAnonTypeHole is_extra wc_tv
2225 -- Why the 'when' guard?
2226 -- See Note [Wildcards in visible kind application]
2227
2228 -- You might think that this would always just unify
2229 -- wc_kind with exp_kind, so we could avoid even creating kv
2230 -- But the level numbers might not allow that unification,
2231 -- so we have to do it properly (T14140a)
2232 ; checkExpectedKind ty (mkTyVarTy wc_tv) wc_kind exp_kind }
2233 where
2234 -- See Note [Wildcard names]
2235 wc_nm = case hole_mode of
2236 HM_Sig -> "w"
2237 HM_FamPat -> "_"
2238 HM_VTA -> "w"
2239 HM_TyAppPat -> "_"
2240
2241 emit_holes = case hole_mode of
2242 HM_Sig -> True
2243 HM_FamPat -> False
2244 HM_VTA -> False
2245 HM_TyAppPat -> False
2246
2247 tcAnonWildCardOcc _ mode ty _
2248 -- mode_holes is Nothing. Should not happen, because renamer
2249 -- should already have rejected holes in unexpected places
2250 = pprPanic "tcWildCardOcc" (ppr mode $$ ppr ty)
2251
2252 {- Note [Wildcard names]
2253 ~~~~~~~~~~~~~~~~~~~~~~~~
2254 So we hackily use the mode_holes flag to control the name used
2255 for wildcards:
2256
2257 * For proper holes (whether in a visible type application (VTA) or no),
2258 we rename the '_' to 'w'. This is so that we see variables like 'w0'
2259 or 'w1' in error messages, a vast improvement upon '_0' and '_1'. For
2260 example, we prefer
2261 Found type wildcard ‘_’ standing for ‘w0’
2262 over
2263 Found type wildcard ‘_’ standing for ‘_1’
2264
2265 Even in the VTA case, where we do not emit an error to be printed, we
2266 want to do the renaming, as the variables may appear in other,
2267 non-wildcard error messages.
2268
2269 * However, holes in the left-hand sides of type families ("type
2270 patterns") stand for type variables which we do not care to name --
2271 much like the use of an underscore in an ordinary term-level
2272 pattern. When we spot these, we neither wish to generate an error
2273 message nor to rename the variable. We don't rename the variable so
2274 that we can pretty-print a type family LHS as, e.g.,
2275 F _ Int _ = ...
2276 and not
2277 F w1 Int w2 = ...
2278
2279 See also Note [Wildcards in family instances] in
2280 GHC.Rename.Module. The choice of HM_FamPat is made in
2281 tcFamTyPats. There is also some unsavory magic, relying on that
2282 underscore, in GHC.Core.Coercion.tidyCoAxBndrsForUser.
2283
2284 Note [Wildcards in visible kind application]
2285 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2286 There are cases where users might want to pass in a wildcard as a visible kind
2287 argument, for instance:
2288
2289 data T :: forall k1 k2. k1 → k2 → Type where
2290 MkT :: T a b
2291 x :: T @_ @Nat False n
2292 x = MkT
2293
2294 So we should allow '@_' without emitting any hole constraints, and
2295 regardless of whether PartialTypeSignatures is enabled or not. But how
2296 would the typechecker know which '_' is being used in VKA and which is
2297 not when it calls emitNamedTypeHole in
2298 tcHsPartialSigType on all HsWildCardBndrs? The solution is to neither
2299 rename nor include unnamed wildcards in HsWildCardBndrs, but instead
2300 give every anonymous wildcard a fresh wild tyvar in tcAnonWildCardOcc.
2301
2302 And whenever we see a '@', we set mode_holes to HM_VKA, so that
2303 we do not call emitAnonTypeHole in tcAnonWildCardOcc.
2304 See related Note [Wildcards in visible type application] here and
2305 Note [The wildcard story for types] in GHC.Hs.Type
2306 -}
2307
2308 {- *********************************************************************
2309 * *
2310 Kind inference for type declarations
2311 * *
2312 ********************************************************************* -}
2313
2314 -- See Note [kcCheckDeclHeader vs kcInferDeclHeader]
2315 data InitialKindStrategy
2316 = InitialKindCheck SAKS_or_CUSK
2317 | InitialKindInfer
2318
2319 -- Does the declaration have a standalone kind signature (SAKS) or a complete
2320 -- user-specified kind (CUSK)?
2321 data SAKS_or_CUSK
2322 = SAKS Kind -- Standalone kind signature, fully zonked! (zonkTcTypeToType)
2323 | CUSK -- Complete user-specified kind (CUSK)
2324
2325 instance Outputable SAKS_or_CUSK where
2326 ppr (SAKS k) = text "SAKS" <+> ppr k
2327 ppr CUSK = text "CUSK"
2328
2329 -- See Note [kcCheckDeclHeader vs kcInferDeclHeader]
2330 kcDeclHeader
2331 :: InitialKindStrategy
2332 -> Name -- ^ of the thing being checked
2333 -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
2334 -> LHsQTyVars GhcRn -- ^ Binders in the header
2335 -> TcM ContextKind -- ^ The result kind
2336 -> TcM TcTyCon -- ^ A suitably-kinded TcTyCon
2337 kcDeclHeader (InitialKindCheck msig) = kcCheckDeclHeader msig
2338 kcDeclHeader InitialKindInfer = kcInferDeclHeader
2339
2340 {- Note [kcCheckDeclHeader vs kcInferDeclHeader]
2341 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2342 kcCheckDeclHeader and kcInferDeclHeader are responsible for getting the initial kind
2343 of a type constructor.
2344
2345 * kcCheckDeclHeader: the TyCon has a standalone kind signature or a CUSK. In that
2346 case, find the full, final, poly-kinded kind of the TyCon. It's very like a
2347 term-level binding where we have a complete type signature for the function.
2348
2349 * kcInferDeclHeader: the TyCon has neither a standalone kind signature nor a
2350 CUSK. Find a monomorphic kind, with unification variables in it; they will be
2351 generalised later. It's very like a term-level binding where we do not have a
2352 type signature (or, more accurately, where we have a partial type signature),
2353 so we infer the type and generalise.
2354 -}
2355
2356 ------------------------------
2357 kcCheckDeclHeader
2358 :: SAKS_or_CUSK
2359 -> Name -- ^ of the thing being checked
2360 -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
2361 -> LHsQTyVars GhcRn -- ^ Binders in the header
2362 -> TcM ContextKind -- ^ The result kind. AnyKind == no result signature
2363 -> TcM TcTyCon -- ^ A suitably-kinded generalized TcTyCon
2364 kcCheckDeclHeader (SAKS sig) = kcCheckDeclHeader_sig sig
2365 kcCheckDeclHeader CUSK = kcCheckDeclHeader_cusk
2366
2367 kcCheckDeclHeader_cusk
2368 :: Name -- ^ of the thing being checked
2369 -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
2370 -> LHsQTyVars GhcRn -- ^ Binders in the header
2371 -> TcM ContextKind -- ^ The result kind
2372 -> TcM TcTyCon -- ^ A suitably-kinded generalized TcTyCon
2373 kcCheckDeclHeader_cusk name flav
2374 (HsQTvs { hsq_ext = kv_ns
2375 , hsq_explicit = hs_tvs }) kc_res_ki
2376 -- CUSK case
2377 -- See note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl
2378 = addTyConFlavCtxt name flav $
2379 do { (tclvl, wanted, (scoped_kvs, (tc_tvs, res_kind)))
2380 <- pushLevelAndSolveEqualitiesX "kcCheckDeclHeader_cusk" $
2381 bindImplicitTKBndrs_Q_Skol kv_ns $
2382 bindExplicitTKBndrs_Q_Skol ctxt_kind hs_tvs $
2383 newExpectedKind =<< kc_res_ki
2384
2385 -- Now, because we're in a CUSK,
2386 -- we quantify over the mentioned kind vars
2387 ; let spec_req_tkvs = scoped_kvs ++ tc_tvs
2388 all_kinds = res_kind : map tyVarKind spec_req_tkvs
2389
2390 ; candidates' <- candidateQTyVarsOfKinds all_kinds
2391 -- 'candidates' are all the variables that we are going to
2392 -- skolemise and then quantify over. We do not include spec_req_tvs
2393 -- because they are /already/ skolems
2394
2395 ; let non_tc_candidates = filter (not . isTcTyVar) (nonDetEltsUniqSet (tyCoVarsOfTypes all_kinds))
2396 candidates = candidates' { dv_kvs = dv_kvs candidates' `extendDVarSetList` non_tc_candidates }
2397 inf_candidates = candidates `delCandidates` spec_req_tkvs
2398
2399 ; inferred <- quantifyTyVars allVarsOfKindDefault inf_candidates
2400 -- NB: 'inferred' comes back sorted in dependency order
2401
2402 ; scoped_kvs <- mapM zonkTyCoVarKind scoped_kvs
2403 ; tc_tvs <- mapM zonkTyCoVarKind tc_tvs
2404 ; res_kind <- zonkTcType res_kind
2405
2406 ; let mentioned_kv_set = candidateKindVars candidates
2407 specified = scopedSort scoped_kvs
2408 -- NB: maintain the L-R order of scoped_kvs
2409
2410 final_tc_binders = mkNamedTyConBinders Inferred inferred
2411 ++ mkNamedTyConBinders Specified specified
2412 ++ map (mkRequiredTyConBinder mentioned_kv_set) tc_tvs
2413
2414 all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs)
2415 tycon = mkTcTyCon name final_tc_binders res_kind all_tv_prs
2416 True -- it is generalised
2417 flav
2418
2419 ; reportUnsolvedEqualities skol_info (binderVars final_tc_binders)
2420 tclvl wanted
2421
2422 -- If the ordering from
2423 -- Note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl
2424 -- doesn't work, we catch it here, before an error cascade
2425 ; checkTyConTelescope tycon
2426
2427 ; traceTc "kcCheckDeclHeader_cusk " $
2428 vcat [ text "name" <+> ppr name
2429 , text "kv_ns" <+> ppr kv_ns
2430 , text "hs_tvs" <+> ppr hs_tvs
2431 , text "scoped_kvs" <+> ppr scoped_kvs
2432 , text "tc_tvs" <+> ppr tc_tvs
2433 , text "res_kind" <+> ppr res_kind
2434 , text "candidates" <+> ppr candidates
2435 , text "inferred" <+> ppr inferred
2436 , text "specified" <+> ppr specified
2437 , text "final_tc_binders" <+> ppr final_tc_binders
2438 , text "mkTyConKind final_tc_bndrs res_kind"
2439 <+> ppr (mkTyConKind final_tc_binders res_kind)
2440 , text "all_tv_prs" <+> ppr all_tv_prs ]
2441
2442 ; return tycon }
2443 where
2444 skol_info = TyConSkol flav name
2445 ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind
2446 | otherwise = AnyKind
2447
2448 -- | Kind-check a 'LHsQTyVars'. Used in 'inferInitialKind' (for tycon kinds and
2449 -- other kinds).
2450 --
2451 -- This function does not do telescope checking.
2452 kcInferDeclHeader
2453 :: Name -- ^ of the thing being checked
2454 -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
2455 -> LHsQTyVars GhcRn
2456 -> TcM ContextKind -- ^ The result kind
2457 -> TcM TcTyCon -- ^ A suitably-kinded non-generalized TcTyCon
2458 kcInferDeclHeader name flav
2459 (HsQTvs { hsq_ext = kv_ns
2460 , hsq_explicit = hs_tvs }) kc_res_ki
2461 -- No standalane kind signature and no CUSK.
2462 -- See note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl
2463 = addTyConFlavCtxt name flav $
2464 do { (scoped_kvs, (tc_tvs, res_kind))
2465 -- Why bindImplicitTKBndrs_Q_Tv which uses newTyVarTyVar?
2466 -- See Note [Inferring kinds for type declarations] in GHC.Tc.TyCl
2467 <- bindImplicitTKBndrs_Q_Tv kv_ns $
2468 bindExplicitTKBndrs_Q_Tv ctxt_kind hs_tvs $
2469 newExpectedKind =<< kc_res_ki
2470 -- Why "_Tv" not "_Skol"? See third wrinkle in
2471 -- Note [Inferring kinds for type declarations] in GHC.Tc.TyCl,
2472
2473 ; let -- NB: Don't add scoped_kvs to tyConTyVars, because they
2474 -- might unify with kind vars in other types in a mutually
2475 -- recursive group.
2476 -- See Note [Inferring kinds for type declarations] in GHC.Tc.TyCl
2477
2478 tc_binders = mkAnonTyConBinders VisArg tc_tvs
2479 -- Also, note that tc_binders has the tyvars from only the
2480 -- user-written tyvarbinders. See S1 in Note [How TcTyCons work]
2481 -- in GHC.Tc.TyCl
2482 --
2483 -- mkAnonTyConBinder: see Note [No polymorphic recursion]
2484
2485 all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs)
2486 -- NB: bindExplicitTKBndrs_Q_Tv does not clone;
2487 -- ditto Implicit
2488 -- See Note [Cloning for type variable binders]
2489
2490 tycon = mkTcTyCon name tc_binders res_kind all_tv_prs
2491 False -- not yet generalised
2492 flav
2493
2494 ; traceTc "kcInferDeclHeader: not-cusk" $
2495 vcat [ ppr name, ppr kv_ns, ppr hs_tvs
2496 , ppr scoped_kvs
2497 , ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ]
2498 ; return tycon }
2499 where
2500 ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind
2501 | otherwise = AnyKind
2502
2503 -- | Kind-check a declaration header against a standalone kind signature.
2504 -- See Note [Arity inference in kcCheckDeclHeader_sig]
2505 kcCheckDeclHeader_sig
2506 :: Kind -- ^ Standalone kind signature, fully zonked! (zonkTcTypeToType)
2507 -> Name -- ^ of the thing being checked
2508 -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
2509 -> LHsQTyVars GhcRn -- ^ Binders in the header
2510 -> TcM ContextKind -- ^ The result kind. AnyKind == no result signature
2511 -> TcM TcTyCon -- ^ A suitably-kinded TcTyCon
2512 kcCheckDeclHeader_sig kisig name flav
2513 (HsQTvs { hsq_ext = implicit_nms
2514 , hsq_explicit = explicit_nms }) kc_res_ki
2515 = addTyConFlavCtxt name flav $
2516 do { -- Step 1: zip user-written binders with quantifiers from the kind signature.
2517 -- For example:
2518 --
2519 -- type F :: forall k -> k -> forall j. j -> Type
2520 -- data F i a b = ...
2521 --
2522 -- Results in the following 'zipped_binders':
2523 --
2524 -- TyBinder LHsTyVarBndr
2525 -- ---------------------------------------
2526 -- ZippedBinder forall k -> i
2527 -- ZippedBinder k -> a
2528 -- ZippedBinder forall j.
2529 -- ZippedBinder j -> b
2530 --
2531 let (zipped_binders, excess_bndrs, kisig') = zipBinders kisig explicit_nms
2532
2533 -- Report binders that don't have a corresponding quantifier.
2534 -- For example:
2535 --
2536 -- type T :: Type -> Type
2537 -- data T b1 b2 b3 = ...
2538 --
2539 -- Here, b1 is zipped with Type->, while b2 and b3 are excess binders.
2540 --
2541 ; unless (null excess_bndrs) $ failWithTc (tooManyBindersErr kisig' excess_bndrs)
2542
2543 -- Convert each ZippedBinder to TyConBinder for tyConBinders
2544 -- and to [(Name, TcTyVar)] for tcTyConScopedTyVars
2545 ; (vis_tcbs, concat -> explicit_tv_prs) <- mapAndUnzipM zipped_to_tcb zipped_binders
2546
2547 ; (tclvl, wanted, (implicit_tvs, (invis_binders, r_ki)))
2548 <- pushLevelAndSolveEqualitiesX "kcCheckDeclHeader_sig" $ -- #16687
2549 bindImplicitTKBndrs_Tv implicit_nms $
2550 tcExtendNameTyVarEnv explicit_tv_prs $
2551 do { -- Check that inline kind annotations on binders are valid.
2552 -- For example:
2553 --
2554 -- type T :: Maybe k -> Type
2555 -- data T (a :: Maybe j) = ...
2556 --
2557 -- Here we unify Maybe k ~ Maybe j
2558 mapM_ check_zipped_binder zipped_binders
2559
2560 -- Kind-check the result kind annotation, if present:
2561 --
2562 -- data T a b :: res_ki where
2563 -- ^^^^^^^^^
2564 -- We do it here because at this point the environment has been
2565 -- extended with both 'implicit_tcv_prs' and 'explicit_tv_prs'.
2566 ; ctx_k <- kc_res_ki
2567 ; m_res_ki <- case ctx_k of
2568 AnyKind -> return Nothing
2569 _ -> Just <$> newExpectedKind ctx_k
2570
2571 -- Step 2: split off invisible binders.
2572 -- For example:
2573 --
2574 -- type F :: forall k1 k2. (k1, k2) -> Type
2575 -- type family F
2576 --
2577 -- Does 'forall k1 k2' become a part of 'tyConBinders' or 'tyConResKind'?
2578 -- See Note [Arity inference in kcCheckDeclHeader_sig]
2579 ; let (invis_binders, r_ki) = split_invis kisig' m_res_ki
2580
2581 -- Check that the inline result kind annotation is valid.
2582 -- For example:
2583 --
2584 -- type T :: Type -> Maybe k
2585 -- type family T a :: Maybe j where
2586 --
2587 -- Here we unify Maybe k ~ Maybe j
2588 ; whenIsJust m_res_ki $ \res_ki ->
2589 discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig]
2590 unifyKind Nothing r_ki res_ki
2591
2592 ; return (invis_binders, r_ki) }
2593
2594 -- Convert each invisible TyCoBinder to TyConBinder for tyConBinders.
2595 ; invis_tcbs <- mapM invis_to_tcb invis_binders
2596
2597 -- Zonk the implicitly quantified variables.
2598 ; implicit_tvs <- mapM zonkTcTyVarToTyVar implicit_tvs
2599
2600 -- Build the final, generalized TcTyCon
2601 ; let tcbs = vis_tcbs ++ invis_tcbs
2602 implicit_tv_prs = implicit_nms `zip` implicit_tvs
2603 all_tv_prs = implicit_tv_prs ++ explicit_tv_prs
2604 tc = mkTcTyCon name tcbs r_ki all_tv_prs True flav
2605 skol_info = TyConSkol flav name
2606
2607 -- Check that there are no unsolved equalities
2608 ; reportUnsolvedEqualities skol_info (binderVars tcbs) tclvl wanted
2609
2610 ; traceTc "kcCheckDeclHeader_sig done:" $ vcat
2611 [ text "tyConName = " <+> ppr (tyConName tc)
2612 , text "kisig =" <+> debugPprType kisig
2613 , text "tyConKind =" <+> debugPprType (tyConKind tc)
2614 , text "tyConBinders = " <+> ppr (tyConBinders tc)
2615 , text "tcTyConScopedTyVars" <+> ppr (tcTyConScopedTyVars tc)
2616 , text "tyConResKind" <+> debugPprType (tyConResKind tc)
2617 ]
2618 ; return tc }
2619 where
2620 -- Consider this declaration:
2621 --
2622 -- type T :: forall a. forall b -> (a~b) => Proxy a -> Type
2623 -- data T x p = MkT
2624 --
2625 -- Here, we have every possible variant of ZippedBinder:
2626 --
2627 -- TyBinder LHsTyVarBndr
2628 -- ----------------------------------------------
2629 -- ZippedBinder forall {k}.
2630 -- ZippedBinder forall (a::k).
2631 -- ZippedBinder forall (b::k) -> x
2632 -- ZippedBinder (a~b) =>
2633 -- ZippedBinder Proxy a -> p
2634 --
2635 -- Given a ZippedBinder zipped_to_tcb produces:
2636 --
2637 -- * TyConBinder for tyConBinders
2638 -- * (Name, TcTyVar) for tcTyConScopedTyVars, if there's a user-written LHsTyVarBndr
2639 --
2640 zipped_to_tcb :: ZippedBinder -> TcM (TyConBinder, [(Name, TcTyVar)])
2641 zipped_to_tcb zb = case zb of
2642
2643 -- Inferred variable, no user-written binder.
2644 -- Example: forall {k}.
2645 ZippedBinder (Named (Bndr v Specified)) Nothing ->
2646 return (mkNamedTyConBinder Specified v, [])
2647
2648 -- Specified variable, no user-written binder.
2649 -- Example: forall (a::k).
2650 ZippedBinder (Named (Bndr v Inferred)) Nothing ->
2651 return (mkNamedTyConBinder Inferred v, [])
2652
2653 -- Constraint, no user-written binder.
2654 -- Example: (a~b) =>
2655 ZippedBinder (Anon InvisArg bndr_ki) Nothing -> do
2656 name <- newSysName (mkTyVarOccFS (fsLit "ev"))
2657 let tv = mkTyVar name (scaledThing bndr_ki)
2658 return (mkAnonTyConBinder InvisArg tv, [])
2659
2660 -- Non-dependent visible argument with a user-written binder.
2661 -- Example: Proxy a ->
2662 ZippedBinder (Anon VisArg bndr_ki) (Just b) ->
2663 return $
2664 let v_name = getName b
2665 tv = mkTyVar v_name (scaledThing bndr_ki)
2666 tcb = mkAnonTyConBinder VisArg tv
2667 in (tcb, [(v_name, tv)])
2668
2669 -- Dependent visible argument with a user-written binder.
2670 -- Example: forall (b::k) ->
2671 ZippedBinder (Named (Bndr v Required)) (Just b) ->
2672 return $
2673 let v_name = getName b
2674 tcb = mkNamedTyConBinder Required v
2675 in (tcb, [(v_name, v)])
2676
2677 -- 'zipBinders' does not produce any other variants of ZippedBinder.
2678 _ -> panic "goVis: invalid ZippedBinder"
2679
2680 -- Given an invisible binder that comes from 'split_invis',
2681 -- convert it to TyConBinder.
2682 invis_to_tcb :: TyCoBinder -> TcM TyConBinder
2683 invis_to_tcb tb = do
2684 (tcb, stv) <- zipped_to_tcb (ZippedBinder tb Nothing)
2685 massert (null stv)
2686 return tcb
2687
2688 -- Check that the inline kind annotation on a binder is valid
2689 -- by unifying it with the kind of the quantifier.
2690 check_zipped_binder :: ZippedBinder -> TcM ()
2691 check_zipped_binder (ZippedBinder _ Nothing) = return ()
2692 check_zipped_binder (ZippedBinder tb (Just b)) =
2693 case unLoc b of
2694 UserTyVar _ _ _ -> return ()
2695 KindedTyVar _ _ v v_hs_ki -> do
2696 v_ki <- tcLHsKindSig (TyVarBndrKindCtxt (unLoc v)) v_hs_ki
2697 discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig]
2698 unifyKind (Just (ppr v))
2699 (tyBinderType tb)
2700 v_ki
2701
2702 -- Split the invisible binders that should become a part of 'tyConBinders'
2703 -- rather than 'tyConResKind'.
2704 -- See Note [Arity inference in kcCheckDeclHeader_sig]
2705 split_invis :: Kind -> Maybe Kind -> ([TyCoBinder], Kind)
2706 split_invis sig_ki Nothing =
2707 -- instantiate all invisible binders
2708 splitInvisPiTys sig_ki
2709 split_invis sig_ki (Just res_ki) =
2710 -- subtraction a la checkExpectedKind
2711 let n_res_invis_bndrs = invisibleTyBndrCount res_ki
2712 n_sig_invis_bndrs = invisibleTyBndrCount sig_ki
2713 n_inst = n_sig_invis_bndrs - n_res_invis_bndrs
2714 in splitInvisPiTysN n_inst sig_ki
2715
2716 -- A quantifier from a kind signature zipped with a user-written binder for it.
2717 data ZippedBinder = ZippedBinder TyBinder (Maybe (LHsTyVarBndr () GhcRn))
2718
2719 -- See Note [Arity inference in kcCheckDeclHeader_sig]
2720 zipBinders
2721 :: Kind -- Kind signature
2722 -> [LHsTyVarBndr () GhcRn] -- User-written binders
2723 -> ( [ZippedBinder] -- Zipped binders
2724 , [LHsTyVarBndr () GhcRn] -- Leftover user-written binders
2725 , Kind ) -- Remainder of the kind signature
2726 zipBinders = zip_binders [] emptyTCvSubst
2727 where
2728 -- subst: we substitute as we go, to ensure that the resulting
2729 -- binders in the [ZippedBndr] all have distinct uniques.
2730 -- If not, the TyCon may get multiple binders with the same unique,
2731 -- which results in chaos (see #19092,3,4)
2732 -- (The incoming kind might be forall k. k -> forall k. k -> Type
2733 -- where those two k's have the same unique. Without the substitution
2734 -- we'd get a repeated 'k'.)
2735 zip_binders acc subst ki bs
2736 | (b:bs') <- bs -- Stop as soon as 'bs' becomes empty
2737 , Just (tb,ki') <- tcSplitPiTy_maybe ki
2738 , let (subst', tb') = substTyCoBndr subst tb
2739 = if isInvisibleBinder tb
2740 then zip_binders (ZippedBinder tb' Nothing : acc) subst' ki' bs
2741 else zip_binders (ZippedBinder tb' (Just b) : acc) subst' ki' bs'
2742
2743 | otherwise
2744 = (reverse acc, bs, substTy subst ki)
2745
2746 tooManyBindersErr :: Kind -> [LHsTyVarBndr () GhcRn] -> TcRnMessage
2747 tooManyBindersErr ki bndrs = TcRnUnknownMessage $ mkPlainError noHints $
2748 hang (text "Not a function kind:")
2749 4 (ppr ki) $$
2750 hang (text "but extra binders found:")
2751 4 (fsep (map ppr bndrs))
2752
2753 {- Note [Arity inference in kcCheckDeclHeader_sig]
2754 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2755 Given a kind signature 'kisig' and a declaration header, kcCheckDeclHeader_sig
2756 verifies that the declaration conforms to the signature. The end result is a
2757 TcTyCon 'tc' such that:
2758
2759 tyConKind tc == kisig
2760
2761 This TcTyCon would be rather easy to produce if we didn't have to worry about
2762 arity. Consider these declarations:
2763
2764 type family S1 :: forall k. k -> Type
2765 type family S2 (a :: k) :: Type
2766
2767 Both S1 and S2 can be given the same standalone kind signature:
2768
2769 type S2 :: forall k. k -> Type
2770
2771 And, indeed, tyConKind S1 == tyConKind S2. However, tyConKind is built from
2772 tyConBinders and tyConResKind, such that
2773
2774 tyConKind tc == mkTyConKind (tyConBinders tc) (tyConResKind tc)
2775
2776 For S1 and S2, tyConBinders and tyConResKind are different:
2777
2778 tyConBinders S1 == []
2779 tyConResKind S1 == forall k. k -> Type
2780 tyConKind S1 == forall k. k -> Type
2781
2782 tyConBinders S2 == [spec k, anon-vis (a :: k)]
2783 tyConResKind S2 == Type
2784 tyConKind S1 == forall k. k -> Type
2785
2786 This difference determines the arity:
2787
2788 tyConArity tc == length (tyConBinders tc)
2789
2790 That is, the arity of S1 is 0, while the arity of S2 is 2.
2791
2792 'kcCheckDeclHeader_sig' needs to infer the desired arity to split the standalone
2793 kind signature into binders and the result kind. It does so in two rounds:
2794
2795 1. zip user-written binders (vis_tcbs)
2796 2. split off invisible binders (invis_tcbs)
2797
2798 Consider the following declarations:
2799
2800 type F :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type
2801 type family F a b
2802
2803 type G :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type
2804 type family G a b :: forall r2. (r1, r2) -> Type
2805
2806 In step 1 (zip user-written binders), we zip the quantifiers in the signature
2807 with the binders in the header using 'zipBinders'. In both F and G, this results in
2808 the following zipped binders:
2809
2810 TyBinder LHsTyVarBndr
2811 ---------------------------------------
2812 ZippedBinder Type -> a
2813 ZippedBinder forall j.
2814 ZippedBinder j -> b
2815
2816
2817 At this point, we have accumulated three zipped binders which correspond to a
2818 prefix of the standalone kind signature:
2819
2820 Type -> forall j. j -> ...
2821
2822 In step 2 (split off invisible binders), we have to decide how much remaining
2823 invisible binders of the standalone kind signature to split off:
2824
2825 forall k1 k2. (k1, k2) -> Type
2826 ^^^^^^^^^^^^^
2827 split off or not?
2828
2829 This decision is made in 'split_invis':
2830
2831 * If a user-written result kind signature is not provided, as in F,
2832 then split off all invisible binders. This is why we need special treatment
2833 for AnyKind.
2834 * If a user-written result kind signature is provided, as in G,
2835 then do as checkExpectedKind does and split off (n_sig - n_res) binders.
2836 That is, split off such an amount of binders that the remainder of the
2837 standalone kind signature and the user-written result kind signature have the
2838 same amount of invisible quantifiers.
2839
2840 For F, split_invis splits away all invisible binders, and we have 2:
2841
2842 forall k1 k2. (k1, k2) -> Type
2843 ^^^^^^^^^^^^^
2844 split away both binders
2845
2846 The resulting arity of F is 3+2=5. (length vis_tcbs = 3,
2847 length invis_tcbs = 2,
2848 length tcbs = 5)
2849
2850 For G, split_invis decides to split off 1 invisible binder, so that we have the
2851 same amount of invisible quantifiers left:
2852
2853 res_ki = forall r2. (r1, r2) -> Type
2854 kisig = forall k1 k2. (k1, k2) -> Type
2855 ^^^
2856 split off this one.
2857
2858 The resulting arity of G is 3+1=4. (length vis_tcbs = 3,
2859 length invis_tcbs = 1,
2860 length tcbs = 4)
2861
2862 -}
2863
2864 {- Note [discardResult in kcCheckDeclHeader_sig]
2865 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2866 We use 'unifyKind' to check inline kind annotations in declaration headers
2867 against the signature.
2868
2869 type T :: [i] -> Maybe j -> Type
2870 data T (a :: [k1]) (b :: Maybe k2) :: Type where ...
2871
2872 Here, we will unify:
2873
2874 [k1] ~ [i]
2875 Maybe k2 ~ Maybe j
2876 Type ~ Type
2877
2878 The end result is that we fill in unification variables k1, k2:
2879
2880 k1 := i
2881 k2 := j
2882
2883 We also validate that the user isn't confused:
2884
2885 type T :: Type -> Type
2886 data T (a :: Bool) = ...
2887
2888 This will report that (Type ~ Bool) failed to unify.
2889
2890 Now, consider the following example:
2891
2892 type family Id a where Id x = x
2893 type T :: Bool -> Type
2894 type T (a :: Id Bool) = ...
2895
2896 We will unify (Bool ~ Id Bool), and this will produce a non-reflexive coercion.
2897 However, we are free to discard it, as the kind of 'T' is determined by the
2898 signature, not by the inline kind annotation:
2899
2900 we have T :: Bool -> Type
2901 rather than T :: Id Bool -> Type
2902
2903 This (Id Bool) will not show up anywhere after we're done validating it, so we
2904 have no use for the produced coercion.
2905 -}
2906
2907 {- Note [No polymorphic recursion]
2908 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2909 Should this kind-check?
2910 data T ka (a::ka) b = MkT (T Type Int Bool)
2911 (T (Type -> Type) Maybe Bool)
2912
2913 Notice that T is used at two different kinds in its RHS. No!
2914 This should not kind-check. Polymorphic recursion is known to
2915 be a tough nut.
2916
2917 Previously, we laboriously (with help from the renamer)
2918 tried to give T the polymorphic kind
2919 T :: forall ka -> ka -> kappa -> Type
2920 where kappa is a unification variable, even in the inferInitialKinds
2921 phase (which is what kcInferDeclHeader is all about). But
2922 that is dangerously fragile (see the ticket).
2923
2924 Solution: make kcInferDeclHeader give T a straightforward
2925 monomorphic kind, with no quantification whatsoever. That's why
2926 we use mkAnonTyConBinder for all arguments when figuring out
2927 tc_binders.
2928
2929 But notice that (#16322 comment:3)
2930
2931 * The algorithm successfully kind-checks this declaration:
2932 data T2 ka (a::ka) = MkT2 (T2 Type a)
2933
2934 Starting with (inferInitialKinds)
2935 T2 :: (kappa1 :: kappa2 :: *) -> (kappa3 :: kappa4 :: *) -> *
2936 we get
2937 kappa4 := kappa1 -- from the (a:ka) kind signature
2938 kappa1 := Type -- From application T2 Type
2939
2940 These constraints are soluble so generaliseTcTyCon gives
2941 T2 :: forall (k::Type) -> k -> *
2942
2943 But now the /typechecking/ (aka desugaring, tcTyClDecl) phase
2944 fails, because the call (T2 Type a) in the RHS is ill-kinded.
2945
2946 We'd really prefer all errors to show up in the kind checking
2947 phase.
2948
2949 * This algorithm still accepts (in all phases)
2950 data T3 ka (a::ka) = forall b. MkT3 (T3 Type b)
2951 although T3 is really polymorphic-recursive too.
2952 Perhaps we should somehow reject that.
2953
2954 Note [Kind variable ordering for associated types]
2955 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2956 What should be the kind of `T` in the following example? (#15591)
2957
2958 class C (a :: Type) where
2959 type T (x :: f a)
2960
2961 As per Note [Ordering of implicit variables] in GHC.Rename.HsType, we want to quantify
2962 the kind variables in left-to-right order of first occurrence in order to
2963 support visible kind application. But we cannot perform this analysis on just
2964 T alone, since its variable `a` actually occurs /before/ `f` if you consider
2965 the fact that `a` was previously bound by the parent class `C`. That is to say,
2966 the kind of `T` should end up being:
2967
2968 T :: forall a f. f a -> Type
2969
2970 (It wouldn't necessarily be /wrong/ if the kind ended up being, say,
2971 forall f a. f a -> Type, but that would not be as predictable for users of
2972 visible kind application.)
2973
2974 In contrast, if `T` were redefined to be a top-level type family, like `T2`
2975 below:
2976
2977 type family T2 (x :: f (a :: Type))
2978
2979 Then `a` first appears /after/ `f`, so the kind of `T2` should be:
2980
2981 T2 :: forall f a. f a -> Type
2982
2983 In order to make this distinction, we need to know (in kcCheckDeclHeader) which
2984 type variables have been bound by the parent class (if there is one). With
2985 the class-bound variables in hand, we can ensure that we always quantify
2986 these first.
2987 -}
2988
2989
2990 {- *********************************************************************
2991 * *
2992 Expected kinds
2993 * *
2994 ********************************************************************* -}
2995
2996 -- | Describes the kind expected in a certain context.
2997 data ContextKind = TheKind Kind -- ^ a specific kind
2998 | AnyKind -- ^ any kind will do
2999 | OpenKind -- ^ something of the form @TYPE _@
3000
3001 -----------------------
3002 newExpectedKind :: ContextKind -> TcM Kind
3003 newExpectedKind (TheKind k) = return k
3004 newExpectedKind AnyKind = newMetaKindVar
3005 newExpectedKind OpenKind = newOpenTypeKind
3006
3007 -----------------------
3008 expectedKindInCtxt :: UserTypeCtxt -> ContextKind
3009 -- Depending on the context, we might accept any kind (for instance, in a TH
3010 -- splice), or only certain kinds (like in type signatures).
3011 expectedKindInCtxt (TySynCtxt _) = AnyKind
3012 expectedKindInCtxt (GhciCtxt {}) = AnyKind
3013 -- The types in a 'default' decl can have varying kinds
3014 -- See Note [Extended defaults]" in GHC.Tc.Utils.Env
3015 expectedKindInCtxt DefaultDeclCtxt = AnyKind
3016 expectedKindInCtxt DerivClauseCtxt = AnyKind
3017 expectedKindInCtxt TypeAppCtxt = AnyKind
3018 expectedKindInCtxt (ForSigCtxt _) = TheKind liftedTypeKind
3019 expectedKindInCtxt (InstDeclCtxt {}) = TheKind constraintKind
3020 expectedKindInCtxt SpecInstCtxt = TheKind constraintKind
3021 expectedKindInCtxt _ = OpenKind
3022
3023
3024 {- *********************************************************************
3025 * *
3026 Bringing type variables into scope
3027 * *
3028 ********************************************************************* -}
3029
3030 --------------------------------------
3031 -- HsForAllTelescope
3032 --------------------------------------
3033
3034 tcTKTelescope :: TcTyMode
3035 -> HsForAllTelescope GhcRn
3036 -> TcM a
3037 -> TcM ([TcTyVarBinder], a)
3038 tcTKTelescope mode tele thing_inside = case tele of
3039 HsForAllVis { hsf_vis_bndrs = bndrs }
3040 -> do { (req_tv_bndrs, thing) <- tcExplicitTKBndrsX skol_mode bndrs thing_inside
3041 -- req_tv_bndrs :: [VarBndr TyVar ()],
3042 -- but we want [VarBndr TyVar ArgFlag]
3043 ; return (tyVarReqToBinders req_tv_bndrs, thing) }
3044
3045 HsForAllInvis { hsf_invis_bndrs = bndrs }
3046 -> do { (inv_tv_bndrs, thing) <- tcExplicitTKBndrsX skol_mode bndrs thing_inside
3047 -- inv_tv_bndrs :: [VarBndr TyVar Specificity],
3048 -- but we want [VarBndr TyVar ArgFlag]
3049 ; return (tyVarSpecToBinders inv_tv_bndrs, thing) }
3050 where
3051 skol_mode = smVanilla { sm_clone = False, sm_holes = mode_holes mode }
3052
3053 --------------------------------------
3054 -- HsOuterTyVarBndrs
3055 --------------------------------------
3056
3057 bindOuterTKBndrsX :: OutputableBndrFlag flag 'Renamed
3058 => SkolemMode
3059 -> HsOuterTyVarBndrs flag GhcRn
3060 -> TcM a
3061 -> TcM (HsOuterTyVarBndrs flag GhcTc, a)
3062 bindOuterTKBndrsX skol_mode outer_bndrs thing_inside
3063 = case outer_bndrs of
3064 HsOuterImplicit{hso_ximplicit = imp_tvs} ->
3065 do { (imp_tvs', thing) <- bindImplicitTKBndrsX skol_mode imp_tvs thing_inside
3066 ; return ( HsOuterImplicit{hso_ximplicit = imp_tvs'}
3067 , thing) }
3068 HsOuterExplicit{hso_bndrs = exp_bndrs} ->
3069 do { (exp_tvs', thing) <- bindExplicitTKBndrsX skol_mode exp_bndrs thing_inside
3070 ; return ( HsOuterExplicit { hso_xexplicit = exp_tvs'
3071 , hso_bndrs = exp_bndrs }
3072 , thing) }
3073
3074 getOuterTyVars :: HsOuterTyVarBndrs flag GhcTc -> [TcTyVar]
3075 -- The returned [TcTyVar] is not necessarily in dependency order
3076 -- at least for the HsOuterImplicit case
3077 getOuterTyVars (HsOuterImplicit { hso_ximplicit = tvs }) = tvs
3078 getOuterTyVars (HsOuterExplicit { hso_xexplicit = tvbs }) = binderVars tvbs
3079
3080 ---------------
3081 scopedSortOuter :: HsOuterTyVarBndrs Specificity GhcTc -> TcM [InvisTVBinder]
3082 -- Sort any /implicit/ binders into dependency order
3083 -- (zonking first so we can see the dependencies)
3084 -- /Explicit/ ones are already in the right order
3085 scopedSortOuter (HsOuterImplicit{hso_ximplicit = imp_tvs})
3086 = do { imp_tvs <- zonkAndScopedSort imp_tvs
3087 ; return [Bndr tv SpecifiedSpec | tv <- imp_tvs] }
3088 scopedSortOuter (HsOuterExplicit{hso_xexplicit = exp_tvs})
3089 = -- No need to dependency-sort (or zonk) explicit quantifiers
3090 return exp_tvs
3091
3092 ---------------
3093 bindOuterSigTKBndrs_Tv :: HsOuterSigTyVarBndrs GhcRn
3094 -> TcM a -> TcM (HsOuterSigTyVarBndrs GhcTc, a)
3095 bindOuterSigTKBndrs_Tv
3096 = bindOuterTKBndrsX (smVanilla { sm_clone = True, sm_tvtv = True })
3097
3098 bindOuterSigTKBndrs_Tv_M :: TcTyMode
3099 -> HsOuterSigTyVarBndrs GhcRn
3100 -> TcM a -> TcM (HsOuterSigTyVarBndrs GhcTc, a)
3101 -- Do not push level; do not make implication constraint; use Tvs
3102 -- Two major clients of this "bind-only" path are:
3103 -- Note [Using TyVarTvs for kind-checking GADTs] in GHC.Tc.TyCl
3104 -- Note [Checking partial type signatures]
3105 bindOuterSigTKBndrs_Tv_M mode
3106 = bindOuterTKBndrsX (smVanilla { sm_clone = True, sm_tvtv = True
3107 , sm_holes = mode_holes mode })
3108
3109 bindOuterFamEqnTKBndrs_Q_Tv :: HsOuterFamEqnTyVarBndrs GhcRn
3110 -> TcM a
3111 -> TcM ([TcTyVar], a)
3112 bindOuterFamEqnTKBndrs_Q_Tv hs_bndrs thing_inside
3113 = liftFstM getOuterTyVars $
3114 bindOuterTKBndrsX (smVanilla { sm_clone = False, sm_parent = True
3115 , sm_tvtv = True })
3116 hs_bndrs thing_inside
3117 -- sm_clone=False: see Note [Cloning for type variable binders]
3118
3119 bindOuterFamEqnTKBndrs :: HsOuterFamEqnTyVarBndrs GhcRn
3120 -> TcM a
3121 -> TcM ([TcTyVar], a)
3122 bindOuterFamEqnTKBndrs hs_bndrs thing_inside
3123 = liftFstM getOuterTyVars $
3124 bindOuterTKBndrsX (smVanilla { sm_clone = False, sm_parent = True })
3125 hs_bndrs thing_inside
3126 -- sm_clone=False: see Note [Cloning for type variable binders]
3127
3128 ---------------
3129 tcOuterTKBndrs :: OutputableBndrFlag flag 'Renamed
3130 => SkolemInfo
3131 -> HsOuterTyVarBndrs flag GhcRn
3132 -> TcM a -> TcM (HsOuterTyVarBndrs flag GhcTc, a)
3133 tcOuterTKBndrs = tcOuterTKBndrsX (smVanilla { sm_clone = False })
3134 -- Do not clone the outer binders
3135 -- See Note [Cloning for type variable binder] under "must not"
3136
3137 tcOuterTKBndrsX :: OutputableBndrFlag flag 'Renamed
3138 => SkolemMode -> SkolemInfo
3139 -> HsOuterTyVarBndrs flag GhcRn
3140 -> TcM a -> TcM (HsOuterTyVarBndrs flag GhcTc, a)
3141 -- Push level, capture constraints, make implication
3142 tcOuterTKBndrsX skol_mode skol_info outer_bndrs thing_inside
3143 = case outer_bndrs of
3144 HsOuterImplicit{hso_ximplicit = imp_tvs} ->
3145 do { (imp_tvs', thing) <- tcImplicitTKBndrsX skol_mode skol_info imp_tvs thing_inside
3146 ; return ( HsOuterImplicit{hso_ximplicit = imp_tvs'}
3147 , thing) }
3148 HsOuterExplicit{hso_bndrs = exp_bndrs} ->
3149 do { (exp_tvs', thing) <- tcExplicitTKBndrsX skol_mode exp_bndrs thing_inside
3150 ; return ( HsOuterExplicit { hso_xexplicit = exp_tvs'
3151 , hso_bndrs = exp_bndrs }
3152 , thing) }
3153
3154 --------------------------------------
3155 -- Explicit tyvar binders
3156 --------------------------------------
3157
3158 tcExplicitTKBndrs :: OutputableBndrFlag flag 'Renamed
3159 => [LHsTyVarBndr flag GhcRn]
3160 -> TcM a
3161 -> TcM ([VarBndr TyVar flag], a)
3162 tcExplicitTKBndrs = tcExplicitTKBndrsX (smVanilla { sm_clone = True })
3163
3164 tcExplicitTKBndrsX :: OutputableBndrFlag flag 'Renamed
3165 => SkolemMode
3166 -> [LHsTyVarBndr flag GhcRn]
3167 -> TcM a
3168 -> TcM ([VarBndr TyVar flag], a)
3169 -- Push level, capture constraints,
3170 -- and emit an implication constraint with a ForAllSkol ic_info,
3171 -- so that it is subject to a telescope test.
3172 tcExplicitTKBndrsX skol_mode bndrs thing_inside
3173 = do { (tclvl, wanted, (skol_tvs, res))
3174 <- pushLevelAndCaptureConstraints $
3175 bindExplicitTKBndrsX skol_mode bndrs $
3176 thing_inside
3177
3178 ; let skol_info = ForAllSkol (fsep (map ppr bndrs))
3179 -- Notice that we use ForAllSkol here, ignoring the enclosing
3180 -- skol_info unlike tc_implicit_tk_bndrs, because the bad-telescope
3181 -- test applies only to ForAllSkol
3182 ; emitResidualTvConstraint skol_info (binderVars skol_tvs) tclvl wanted
3183
3184 ; return (skol_tvs, res) }
3185
3186 ----------------
3187 -- | Skolemise the 'HsTyVarBndr's in an 'HsForAllTelescope' with the supplied
3188 -- 'TcTyMode'.
3189 bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv
3190 :: (OutputableBndrFlag flag 'Renamed)
3191 => [LHsTyVarBndr flag GhcRn]
3192 -> TcM a
3193 -> TcM ([VarBndr TyVar flag], a)
3194
3195 bindExplicitTKBndrs_Skol = bindExplicitTKBndrsX (smVanilla { sm_clone = False })
3196 bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (smVanilla { sm_clone = True, sm_tvtv = True })
3197 -- sm_clone: see Note [Cloning for type variable binders]
3198
3199 bindExplicitTKBndrs_Q_Skol, bindExplicitTKBndrs_Q_Tv
3200 :: ContextKind
3201 -> [LHsTyVarBndr () GhcRn]
3202 -> TcM a
3203 -> TcM ([TcTyVar], a)
3204 -- These do not clone: see Note [Cloning for type variable binders]
3205 bindExplicitTKBndrs_Q_Skol ctxt_kind hs_bndrs thing_inside
3206 = liftFstM binderVars $
3207 bindExplicitTKBndrsX (smVanilla { sm_clone = False, sm_parent = True
3208 , sm_kind = ctxt_kind })
3209 hs_bndrs thing_inside
3210 -- sm_clone=False: see Note [Cloning for type variable binders]
3211
3212 bindExplicitTKBndrs_Q_Tv ctxt_kind hs_bndrs thing_inside
3213 = liftFstM binderVars $
3214 bindExplicitTKBndrsX (smVanilla { sm_clone = False, sm_parent = True
3215 , sm_tvtv = True, sm_kind = ctxt_kind })
3216 hs_bndrs thing_inside
3217 -- sm_clone=False: see Note [Cloning for type variable binders]
3218
3219 bindExplicitTKBndrsX :: (OutputableBndrFlag flag 'Renamed)
3220 => SkolemMode
3221 -> [LHsTyVarBndr flag GhcRn]
3222 -> TcM a
3223 -> TcM ([VarBndr TyVar flag], a) -- Returned [TcTyVar] are in 1-1 correspondence
3224 -- with the passed-in [LHsTyVarBndr]
3225 bindExplicitTKBndrsX skol_mode@(SM { sm_parent = check_parent, sm_kind = ctxt_kind
3226 , sm_holes = hole_info })
3227 hs_tvs thing_inside
3228 = do { traceTc "bindExplicitTKBndrs" (ppr hs_tvs)
3229 ; go hs_tvs }
3230 where
3231 tc_ki_mode = TcTyMode { mode_tyki = KindLevel, mode_holes = hole_info }
3232 -- Inherit the HoleInfo from the context
3233
3234 go [] = do { res <- thing_inside
3235 ; return ([], res) }
3236 go (L _ hs_tv : hs_tvs)
3237 = do { lcl_env <- getLclTypeEnv
3238 ; tv <- tc_hs_bndr lcl_env hs_tv
3239 -- Extend the environment as we go, in case a binder
3240 -- is mentioned in the kind of a later binder
3241 -- e.g. forall k (a::k). blah
3242 -- NB: tv's Name may differ from hs_tv's
3243 -- See Note [Cloning for type variable binders]
3244 ; (tvs,res) <- tcExtendNameTyVarEnv [(hsTyVarName hs_tv, tv)] $
3245 go hs_tvs
3246 ; return (Bndr tv (hsTyVarBndrFlag hs_tv):tvs, res) }
3247
3248
3249 tc_hs_bndr lcl_env (UserTyVar _ _ (L _ name))
3250 | check_parent
3251 , Just (ATyVar _ tv) <- lookupNameEnv lcl_env name
3252 = return tv
3253 | otherwise
3254 = do { kind <- newExpectedKind ctxt_kind
3255 ; newTyVarBndr skol_mode name kind }
3256
3257 tc_hs_bndr lcl_env (KindedTyVar _ _ (L _ name) lhs_kind)
3258 | check_parent
3259 , Just (ATyVar _ tv) <- lookupNameEnv lcl_env name
3260 = do { kind <- tc_lhs_kind_sig tc_ki_mode (TyVarBndrKindCtxt name) lhs_kind
3261 ; discardResult $
3262 unifyKind (Just (ppr name)) kind (tyVarKind tv)
3263 -- This unify rejects:
3264 -- class C (m :: * -> *) where
3265 -- type F (m :: *) = ...
3266 ; return tv }
3267
3268 | otherwise
3269 = do { kind <- tc_lhs_kind_sig tc_ki_mode (TyVarBndrKindCtxt name) lhs_kind
3270 ; newTyVarBndr skol_mode name kind }
3271
3272 newTyVarBndr :: SkolemMode -> Name -> Kind -> TcM TcTyVar
3273 newTyVarBndr (SM { sm_clone = clone, sm_tvtv = tvtv }) name kind
3274 = do { name <- case clone of
3275 True -> do { uniq <- newUnique
3276 ; return (setNameUnique name uniq) }
3277 False -> return name
3278 ; details <- case tvtv of
3279 True -> newMetaDetails TyVarTv
3280 False -> do { lvl <- getTcLevel
3281 ; return (SkolemTv lvl False) }
3282 ; return (mkTcTyVar name kind details) }
3283
3284 --------------------------------------
3285 -- Implicit tyvar binders
3286 --------------------------------------
3287
3288 tcImplicitTKBndrsX :: SkolemMode -> SkolemInfo
3289 -> [Name]
3290 -> TcM a
3291 -> TcM ([TcTyVar], a)
3292 -- The workhorse:
3293 -- push level, capture constraints,
3294 -- and emit an implication constraint with a ForAllSkol ic_info,
3295 -- so that it is subject to a telescope test.
3296 tcImplicitTKBndrsX skol_mode skol_info bndrs thing_inside
3297 | null bndrs -- Short-cut the common case with no quantifiers
3298 -- E.g. f :: Int -> Int
3299 -- makes a HsOuterImplicit with empty bndrs,
3300 -- and tcOuterTKBndrsX goes via here
3301 = do { res <- thing_inside; return ([], res) }
3302 | otherwise
3303 = do { (tclvl, wanted, (skol_tvs, res))
3304 <- pushLevelAndCaptureConstraints $
3305 bindImplicitTKBndrsX skol_mode bndrs $
3306 thing_inside
3307
3308 ; emitResidualTvConstraint skol_info skol_tvs tclvl wanted
3309
3310 ; return (skol_tvs, res) }
3311
3312 ------------------
3313 bindImplicitTKBndrs_Skol, bindImplicitTKBndrs_Tv,
3314 bindImplicitTKBndrs_Q_Skol, bindImplicitTKBndrs_Q_Tv
3315 :: [Name] -> TcM a -> TcM ([TcTyVar], a)
3316 bindImplicitTKBndrs_Skol = bindImplicitTKBndrsX (smVanilla { sm_clone = True })
3317 bindImplicitTKBndrs_Tv = bindImplicitTKBndrsX (smVanilla { sm_clone = True, sm_tvtv = True })
3318 bindImplicitTKBndrs_Q_Skol = bindImplicitTKBndrsX (smVanilla { sm_clone = False, sm_parent = True })
3319 bindImplicitTKBndrs_Q_Tv = bindImplicitTKBndrsX (smVanilla { sm_clone = False, sm_parent = True, sm_tvtv = True })
3320
3321 bindImplicitTKBndrsX
3322 :: SkolemMode
3323 -> [Name]
3324 -> TcM a
3325 -> TcM ([TcTyVar], a) -- Returned [TcTyVar] are in 1-1 correspondence
3326 -- with the passed in [Name]
3327 bindImplicitTKBndrsX skol_mode@(SM { sm_parent = check_parent, sm_kind = ctxt_kind })
3328 tv_names thing_inside
3329 = do { lcl_env <- getLclTypeEnv
3330 ; tkvs <- mapM (new_tv lcl_env) tv_names
3331 ; traceTc "bindImplicitTKBndrsX" (ppr tv_names $$ ppr tkvs)
3332 ; res <- tcExtendNameTyVarEnv (tv_names `zip` tkvs)
3333 thing_inside
3334 ; return (tkvs, res) }
3335 where
3336 new_tv lcl_env name
3337 | check_parent
3338 , Just (ATyVar _ tv) <- lookupNameEnv lcl_env name
3339 = return tv
3340 | otherwise
3341 = do { kind <- newExpectedKind ctxt_kind
3342 ; newTyVarBndr skol_mode name kind }
3343
3344 --------------------------------------
3345 -- SkolemMode
3346 --------------------------------------
3347
3348 -- | 'SkolemMode' describes how to typecheck an explicit ('HsTyVarBndr') or
3349 -- implicit ('Name') binder in a type. It is just a record of flags
3350 -- that describe what sort of 'TcTyVar' to create.
3351 data SkolemMode
3352 = SM { sm_parent :: Bool -- True <=> check the in-scope parent type variable
3353 -- Used only for asssociated types
3354
3355 , sm_clone :: Bool -- True <=> fresh unique
3356 -- See Note [Cloning for type variable binders]
3357
3358 , sm_tvtv :: Bool -- True <=> use a TyVarTv, rather than SkolemTv
3359 -- Why? See Note [Inferring kinds for type declarations]
3360 -- in GHC.Tc.TyCl, and (in this module)
3361 -- Note [Checking partial type signatures]
3362
3363 , sm_kind :: ContextKind -- Use this for the kind of any new binders
3364
3365 , sm_holes :: HoleInfo -- What to do for wildcards in the kind
3366 }
3367
3368 smVanilla :: SkolemMode
3369 smVanilla = SM { sm_clone = panic "sm_clone" -- We always override this
3370 , sm_parent = False
3371 , sm_tvtv = False
3372 , sm_kind = AnyKind
3373 , sm_holes = Nothing }
3374
3375 {- Note [Cloning for type variable binders]
3376 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3377 Sometimes we must clone the Name of a type variable binder (written in
3378 the source program); and sometimes we must not. This is controlled by
3379 the sm_clone field of SkolemMode.
3380
3381 In some cases it doesn't matter whether or not we clone. Perhaps
3382 it'd be better to use MustClone/MayClone/MustNotClone.
3383
3384 When we /must not/ clone
3385 * In the binders of a type signature (tcOuterTKBndrs)
3386 f :: forall a{27}. blah
3387 f = rhs
3388 Then 'a' scopes over 'rhs'. When we kind-check the signature (tcHsSigType),
3389 we must get the type (forall a{27}. blah) for the Id f, because
3390 we bring that type variable into scope when we typecheck 'rhs'.
3391
3392 * In the binders of a data family instance (bindOuterFamEqnTKBndrs)
3393 data instance
3394 forall p q. D (p,q) = D1 p | D2 q
3395 We kind-check the LHS in tcDataFamInstHeader, and then separately
3396 (in tcDataFamInstDecl) bring p,q into scope before looking at the
3397 the constructor decls.
3398
3399 * bindExplicitTKBndrs_Q_Tv/bindImplicitTKBndrs_Q_Tv do not clone
3400 We take advantage of this in kcInferDeclHeader:
3401 all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs)
3402 If we cloned, we'd need to take a bit more care here; not hard.
3403
3404 * bindExplicitTKBndrs_Q_Skol, bindExplicitTKBndrs_Skol, do not clone.
3405 There is no need, I think.
3406
3407 The payoff here is that avoiding gratuitous cloning means that we can
3408 almost always take the fast path in swizzleTcTyConBndrs.
3409
3410 When we /must/ clone.
3411 * bindOuterSigTKBndrs_Tv, bindExplicitTKBndrs_Tv do cloning
3412
3413 This for a narrow and tricky reason which, alas, I couldn't find a
3414 simpler way round. #16221 is the poster child:
3415
3416 data SameKind :: k -> k -> *
3417 data T a = forall k2 (b :: k2). MkT (SameKind a b) !Int
3418
3419 When kind-checking T, we give (a :: kappa1). Then:
3420
3421 - In kcConDecl we make a TyVarTv unification variable kappa2 for k2
3422 (as described in Note [Using TyVarTvs for kind-checking GADTs],
3423 even though this example is an existential)
3424 - So we get (b :: kappa2) via bindExplicitTKBndrs_Tv
3425 - We end up unifying kappa1 := kappa2, because of the (SameKind a b)
3426
3427 Now we generalise over kappa2. But if kappa2's Name is precisely k2
3428 (i.e. we did not clone) we'll end up giving T the utterly final kind
3429 T :: forall k2. k2 -> *
3430 Nothing directly wrong with that but when we typecheck the data constructor
3431 we have k2 in scope; but then it's brought into scope /again/ when we find
3432 the forall k2. This is chaotic, and we end up giving it the type
3433 MkT :: forall k2 (a :: k2) k2 (b :: k2).
3434 SameKind @k2 a b -> Int -> T @{k2} a
3435 which is bogus -- because of the shadowing of k2, we can't
3436 apply T to the kind or a!
3437
3438 And there no reason /not/ to clone the Name when making a unification
3439 variable. So that's what we do.
3440 -}
3441
3442 --------------------------------------
3443 -- Binding type/class variables in the
3444 -- kind-checking and typechecking phases
3445 --------------------------------------
3446
3447 bindTyClTyVars :: Name
3448 -> (TcTyCon -> [TyConBinder] -> Kind -> TcM a) -> TcM a
3449 -- ^ Used for the type variables of a type or class decl
3450 -- in the "kind checking" and "type checking" pass,
3451 -- but not in the initial-kind run.
3452 bindTyClTyVars tycon_name thing_inside
3453 = do { tycon <- tcLookupTcTyCon tycon_name
3454 ; let scoped_prs = tcTyConScopedTyVars tycon
3455 res_kind = tyConResKind tycon
3456 binders = tyConBinders tycon
3457 ; traceTc "bindTyClTyVars" (ppr tycon_name <+> ppr binders $$ ppr scoped_prs)
3458 ; tcExtendNameTyVarEnv scoped_prs $
3459 thing_inside tycon binders res_kind }
3460
3461
3462 {- *********************************************************************
3463 * *
3464 Kind generalisation
3465 * *
3466 ********************************************************************* -}
3467
3468 zonkAndScopedSort :: [TcTyVar] -> TcM [TcTyVar]
3469 zonkAndScopedSort spec_tkvs
3470 = do { spec_tkvs <- mapM zonkTcTyVarToTyVar spec_tkvs
3471 -- Zonk the kinds, to we can do the dependency analayis
3472
3473 -- Do a stable topological sort, following
3474 -- Note [Ordering of implicit variables] in GHC.Rename.HsType
3475 ; return (scopedSort spec_tkvs) }
3476
3477 -- | Generalize some of the free variables in the given type.
3478 -- All such variables should be *kind* variables; any type variables
3479 -- should be explicitly quantified (with a `forall`) before now.
3480 --
3481 -- The WantedConstraints are un-solved kind constraints. Generally
3482 -- they'll be reported as errors later, but meanwhile we refrain
3483 -- from quantifying over any variable free in these unsolved
3484 -- constraints. See Note [Failure in local type signatures].
3485 --
3486 -- But in all cases, generalize only those variables whose TcLevel is
3487 -- strictly greater than the ambient level. This "strictly greater
3488 -- than" means that you likely need to push the level before creating
3489 -- whatever type gets passed here.
3490 --
3491 -- Any variable whose level is greater than the ambient level but is
3492 -- not selected to be generalized will be promoted. (See [Promoting
3493 -- unification variables] in "GHC.Tc.Solver" and Note [Recipe for
3494 -- checking a signature].)
3495 --
3496 -- The resulting KindVar are the variables to quantify over, in the
3497 -- correct, well-scoped order. They should generally be Inferred, not
3498 -- Specified, but that's really up to the caller of this function.
3499 kindGeneralizeSome :: WantedConstraints
3500 -> TcType -- ^ needn't be zonked
3501 -> TcM [KindVar]
3502 kindGeneralizeSome wanted kind_or_type
3503 = do { -- Use the "Kind" variant here, as any types we see
3504 -- here will already have all type variables quantified;
3505 -- thus, every free variable is really a kv, never a tv.
3506 ; dvs <- candidateQTyVarsOfKind kind_or_type
3507 ; dvs <- filterConstrainedCandidates wanted dvs
3508 ; quantifyTyVars allVarsOfKindDefault dvs }
3509
3510 filterConstrainedCandidates
3511 :: WantedConstraints -- Don't quantify over variables free in these
3512 -- Not necessarily fully zonked
3513 -> CandidatesQTvs -- Candidates for quantification
3514 -> TcM CandidatesQTvs
3515 -- filterConstrainedCandidates removes any candidates that are free in
3516 -- 'wanted'; instead, it promotes them. This bit is very much like
3517 -- decideMonoTyVars in GHC.Tc.Solver, but constraints are so much
3518 -- simpler in kinds, it is much easier here. (In particular, we never
3519 -- quantify over a constraint in a type.)
3520 filterConstrainedCandidates wanted dvs
3521 | isEmptyWC wanted -- Fast path for a common case
3522 = return dvs
3523 | otherwise
3524 = do { wc_tvs <- zonkTyCoVarsAndFV (tyCoVarsOfWC wanted)
3525 ; let (to_promote, dvs') = partitionCandidates dvs (`elemVarSet` wc_tvs)
3526 ; _ <- promoteTyVarSet to_promote
3527 ; return dvs' }
3528
3529 -- |- Specialised version of 'kindGeneralizeSome', but with empty
3530 -- WantedConstraints, so no filtering is needed
3531 -- i.e. kindGeneraliseAll = kindGeneralizeSome emptyWC
3532 kindGeneralizeAll :: TcType -> TcM [KindVar]
3533 kindGeneralizeAll kind_or_type
3534 = do { traceTc "kindGeneralizeAll" (ppr kind_or_type)
3535 ; dvs <- candidateQTyVarsOfKind kind_or_type
3536 ; quantifyTyVars allVarsOfKindDefault dvs }
3537
3538 -- | Specialized version of 'kindGeneralizeSome', but where no variables
3539 -- can be generalized, but perhaps some may need to be promoted.
3540 -- Use this variant when it is unknowable whether metavariables might
3541 -- later be constrained.
3542 --
3543 -- To see why this promotion is needed, see
3544 -- Note [Recipe for checking a signature], and especially
3545 -- Note [Promotion in signatures].
3546 kindGeneralizeNone :: TcType -- needn't be zonked
3547 -> TcM ()
3548 kindGeneralizeNone kind_or_type
3549 = do { traceTc "kindGeneralizeNone" (ppr kind_or_type)
3550 ; dvs <- candidateQTyVarsOfKind kind_or_type
3551 ; _ <- promoteTyVarSet (candidateKindVars dvs)
3552 ; return () }
3553
3554 {- Note [Levels and generalisation]
3555 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3556 Consider
3557 f x = e
3558 with no type signature. We are currently at level i.
3559 We must
3560 * Push the level to level (i+1)
3561 * Allocate a fresh alpha[i+1] for the result type
3562 * Check that e :: alpha[i+1], gathering constraint WC
3563 * Solve WC as far as possible
3564 * Zonking the result type alpha[i+1], say to beta[i-1] -> gamma[i]
3565 * Find the free variables with level > i, in this case gamma[i]
3566 * Skolemise those free variables and quantify over them, giving
3567 f :: forall g. beta[i-1] -> g
3568 * Emit the residiual constraint wrapped in an implication for g,
3569 thus forall g. WC
3570
3571 All of this happens for types too. Consider
3572 f :: Int -> (forall a. Proxy a -> Int)
3573
3574 Note [Kind generalisation]
3575 ~~~~~~~~~~~~~~~~~~~~~~~~~~
3576 We do kind generalisation only at the outer level of a type signature.
3577 For example, consider
3578 T :: forall k. k -> *
3579 f :: (forall a. T a -> Int) -> Int
3580 When kind-checking f's type signature we generalise the kind at
3581 the outermost level, thus:
3582 f1 :: forall k. (forall (a:k). T k a -> Int) -> Int -- YES!
3583 and *not* at the inner forall:
3584 f2 :: (forall k. forall (a:k). T k a -> Int) -> Int -- NO!
3585 Reason: same as for HM inference on value level declarations,
3586 we want to infer the most general type. The f2 type signature
3587 would be *less applicable* than f1, because it requires a more
3588 polymorphic argument.
3589
3590 NB: There are no explicit kind variables written in f's signature.
3591 When there are, the renamer adds these kind variables to the list of
3592 variables bound by the forall, so you can indeed have a type that's
3593 higher-rank in its kind. But only by explicit request.
3594
3595 Note [Kinds of quantified type variables]
3596 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3597 tcTyVarBndrsGen quantifies over a specified list of type variables,
3598 *and* over the kind variables mentioned in the kinds of those tyvars.
3599
3600 Note that we must zonk those kinds (obviously) but less obviously, we
3601 must return type variables whose kinds are zonked too. Example
3602 (a :: k7) where k7 := k9 -> k9
3603 We must return
3604 [k9, a:k9->k9]
3605 and NOT
3606 [k9, a:k7]
3607 Reason: we're going to turn this into a for-all type,
3608 forall k9. forall (a:k7). blah
3609 which the type checker will then instantiate, and instantiate does not
3610 look through unification variables!
3611
3612 Hence using zonked_kinds when forming tvs'.
3613
3614 -}
3615
3616 -----------------------------------
3617 etaExpandAlgTyCon :: [TyConBinder]
3618 -> Kind -- must be zonked
3619 -> TcM ([TyConBinder], Kind)
3620 -- GADT decls can have a (perhaps partial) kind signature
3621 -- e.g. data T a :: * -> * -> * where ...
3622 -- This function makes up suitable (kinded) TyConBinders for the
3623 -- argument kinds. E.g. in this case it might return
3624 -- ([b::*, c::*], *)
3625 -- Never emits constraints.
3626 -- It's a little trickier than you might think: see
3627 -- Note [TyConBinders for the result kind signature of a data type]
3628 -- See Note [Datatype return kinds] in GHC.Tc.TyCl
3629 etaExpandAlgTyCon tc_bndrs kind
3630 = do { loc <- getSrcSpanM
3631 ; uniqs <- newUniqueSupply
3632 ; rdr_env <- getLocalRdrEnv
3633 ; let new_occs = [ occ
3634 | str <- allNameStrings
3635 , let occ = mkOccName tvName str
3636 , isNothing (lookupLocalRdrOcc rdr_env occ)
3637 -- Note [Avoid name clashes for associated data types]
3638 , not (occ `elem` lhs_occs) ]
3639 new_uniqs = uniqsFromSupply uniqs
3640 subst = mkEmptyTCvSubst (mkInScopeSet (mkVarSet lhs_tvs))
3641 ; return (go loc new_occs new_uniqs subst [] kind) }
3642 where
3643 lhs_tvs = map binderVar tc_bndrs
3644 lhs_occs = map getOccName lhs_tvs
3645
3646 go loc occs uniqs subst acc kind
3647 = case splitPiTy_maybe kind of
3648 Nothing -> (reverse acc, substTy subst kind)
3649
3650 Just (Anon af arg, kind')
3651 -> go loc occs' uniqs' subst' (tcb : acc) kind'
3652 where
3653 arg' = substTy subst (scaledThing arg)
3654 tv = mkTyVar (mkInternalName uniq occ loc) arg'
3655 subst' = extendTCvInScope subst tv
3656 tcb = Bndr tv (AnonTCB af)
3657 (uniq:uniqs') = uniqs
3658 (occ:occs') = occs
3659
3660 Just (Named (Bndr tv vis), kind')
3661 -> go loc occs uniqs subst' (tcb : acc) kind'
3662 where
3663 (subst', tv') = substTyVarBndr subst tv
3664 tcb = Bndr tv' (NamedTCB vis)
3665
3666 -- | A description of whether something is a
3667 --
3668 -- * @data@ or @newtype@ ('DataDeclSort')
3669 --
3670 -- * @data instance@ or @newtype instance@ ('DataInstanceSort')
3671 --
3672 -- * @data family@ ('DataFamilySort')
3673 --
3674 -- At present, this data type is only consumed by 'checkDataKindSig'.
3675 data DataSort
3676 = DataDeclSort NewOrData
3677 | DataInstanceSort NewOrData
3678 | DataFamilySort
3679
3680 -- | Local helper type used in 'checkDataKindSig'.
3681 --
3682 -- Superficially similar to 'ContextKind', but it lacks 'AnyKind'
3683 -- and 'AnyBoxedKind', and instead of @'TheKind' liftedTypeKind@
3684 -- provides 'LiftedKind', which is much simpler to match on and
3685 -- handle in 'isAllowedDataResKind'.
3686 data AllowedDataResKind
3687 = AnyTYPEKind
3688 | AnyBoxedKind
3689 | LiftedKind
3690
3691 isAllowedDataResKind :: AllowedDataResKind -> Kind -> Bool
3692 isAllowedDataResKind AnyTYPEKind kind = tcIsRuntimeTypeKind kind
3693 isAllowedDataResKind AnyBoxedKind kind = tcIsBoxedTypeKind kind
3694 isAllowedDataResKind LiftedKind kind = tcIsLiftedTypeKind kind
3695
3696 -- | Checks that the return kind in a data declaration's kind signature is
3697 -- permissible. There are three cases:
3698 --
3699 -- If dealing with a @data@, @newtype@, @data instance@, or @newtype instance@
3700 -- declaration, check that the return kind is @Type@.
3701 --
3702 -- If the declaration is a @newtype@ or @newtype instance@ and the
3703 -- @UnliftedNewtypes@ extension is enabled, this check is slightly relaxed so
3704 -- that a return kind of the form @TYPE r@ (for some @r@) is permitted.
3705 -- See @Note [Implementation of UnliftedNewtypes]@ in "GHC.Tc.TyCl".
3706 --
3707 -- If dealing with a @data family@ declaration, check that the return kind is
3708 -- either of the form:
3709 --
3710 -- 1. @TYPE r@ (for some @r@), or
3711 --
3712 -- 2. @k@ (where @k@ is a bare kind variable; see #12369)
3713 --
3714 -- See also Note [Datatype return kinds] in "GHC.Tc.TyCl"
3715 checkDataKindSig :: DataSort -> Kind -- any arguments in the kind are stripped off
3716 -> TcM ()
3717 checkDataKindSig data_sort kind
3718 = do { dflags <- getDynFlags
3719 ; traceTc "checkDataKindSig" (ppr kind)
3720 ; checkTc (tYPE_ok dflags || is_kind_var)
3721 (err_msg dflags) }
3722 where
3723 res_kind = snd (tcSplitPiTys kind)
3724 -- Look for the result kind after
3725 -- peeling off any foralls and arrows
3726
3727 pp_dec :: SDoc
3728 pp_dec = text $
3729 case data_sort of
3730 DataDeclSort DataType -> "Data type"
3731 DataDeclSort NewType -> "Newtype"
3732 DataInstanceSort DataType -> "Data instance"
3733 DataInstanceSort NewType -> "Newtype instance"
3734 DataFamilySort -> "Data family"
3735
3736 is_newtype :: Bool
3737 is_newtype =
3738 case data_sort of
3739 DataDeclSort new_or_data -> new_or_data == NewType
3740 DataInstanceSort new_or_data -> new_or_data == NewType
3741 DataFamilySort -> False
3742
3743 is_datatype :: Bool
3744 is_datatype =
3745 case data_sort of
3746 DataDeclSort DataType -> True
3747 DataInstanceSort DataType -> True
3748 _ -> False
3749
3750 is_data_family :: Bool
3751 is_data_family =
3752 case data_sort of
3753 DataDeclSort{} -> False
3754 DataInstanceSort{} -> False
3755 DataFamilySort -> True
3756
3757 allowed_kind :: DynFlags -> AllowedDataResKind
3758 allowed_kind dflags
3759 | is_newtype && xopt LangExt.UnliftedNewtypes dflags
3760 -- With UnliftedNewtypes, we allow kinds other than Type, but they
3761 -- must still be of the form `TYPE r` since we don't want to accept
3762 -- Constraint or Nat.
3763 -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl.
3764 = AnyTYPEKind
3765 | is_data_family
3766 -- If this is a `data family` declaration, we don't need to check if
3767 -- UnliftedNewtypes is enabled, since data family declarations can
3768 -- have return kind `TYPE r` unconditionally (#16827).
3769 = AnyTYPEKind
3770 | is_datatype && xopt LangExt.UnliftedDatatypes dflags
3771 -- With UnliftedDatatypes, we allow kinds other than Type, but they
3772 -- must still be of the form `TYPE (BoxedRep l)`, so that we don't
3773 -- accept result kinds like `TYPE IntRep`.
3774 -- See Note [Implementation of UnliftedDatatypes] in GHC.Tc.TyCl.
3775 = AnyBoxedKind
3776 | otherwise
3777 = LiftedKind
3778
3779 tYPE_ok :: DynFlags -> Bool
3780 tYPE_ok dflags = isAllowedDataResKind (allowed_kind dflags) res_kind
3781
3782 -- In the particular case of a data family, permit a return kind of the
3783 -- form `:: k` (where `k` is a bare kind variable).
3784 is_kind_var :: Bool
3785 is_kind_var | is_data_family = isJust (tcGetCastedTyVar_maybe res_kind)
3786 | otherwise = False
3787
3788 pp_allowed_kind dflags =
3789 case allowed_kind dflags of
3790 AnyTYPEKind -> ppr tYPETyCon
3791 AnyBoxedKind -> ppr boxedRepDataConTyCon
3792 LiftedKind -> ppr liftedTypeKind
3793
3794 err_msg :: DynFlags -> TcRnMessage
3795 err_msg dflags = TcRnUnknownMessage $ mkPlainError noHints $
3796 sep [ sep [ pp_dec <+>
3797 text "has non-" <>
3798 pp_allowed_kind dflags
3799 , (if is_data_family then text "and non-variable" else empty) <+>
3800 text "return kind" <+> quotes (ppr kind) ]
3801 , ext_hint dflags ]
3802
3803 ext_hint dflags
3804 | tcIsRuntimeTypeKind kind
3805 , is_newtype
3806 , not (xopt LangExt.UnliftedNewtypes dflags)
3807 = text "Perhaps you intended to use UnliftedNewtypes"
3808 | tcIsBoxedTypeKind kind
3809 , is_datatype
3810 , not (xopt LangExt.UnliftedDatatypes dflags)
3811 = text "Perhaps you intended to use UnliftedDatatypes"
3812 | otherwise
3813 = empty
3814
3815 -- | Checks that the result kind of a class is exactly `Constraint`, rejecting
3816 -- type synonyms and type families that reduce to `Constraint`. See #16826.
3817 checkClassKindSig :: Kind -> TcM ()
3818 checkClassKindSig kind = checkTc (tcIsConstraintKind kind) err_msg
3819 where
3820 err_msg :: TcRnMessage
3821 err_msg = TcRnUnknownMessage $ mkPlainError noHints $
3822 text "Kind signature on a class must end with" <+> ppr constraintKind $$
3823 text "unobscured by type families"
3824
3825 tcbVisibilities :: TyCon -> [Type] -> [TyConBndrVis]
3826 -- Result is in 1-1 correspondence with orig_args
3827 tcbVisibilities tc orig_args
3828 = go (tyConKind tc) init_subst orig_args
3829 where
3830 init_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfTypes orig_args))
3831 go _ _ []
3832 = []
3833
3834 go fun_kind subst all_args@(arg : args)
3835 | Just (tcb, inner_kind) <- splitPiTy_maybe fun_kind
3836 = case tcb of
3837 Anon af _ -> AnonTCB af : go inner_kind subst args
3838 Named (Bndr tv vis) -> NamedTCB vis : go inner_kind subst' args
3839 where
3840 subst' = extendTCvSubst subst tv arg
3841
3842 | not (isEmptyTCvSubst subst)
3843 = go (substTy subst fun_kind) init_subst all_args
3844
3845 | otherwise
3846 = pprPanic "addTcbVisibilities" (ppr tc <+> ppr orig_args)
3847
3848
3849 {- Note [TyConBinders for the result kind signature of a data type]
3850 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3851 Given
3852 data T (a::*) :: * -> forall k. k -> *
3853 we want to generate the extra TyConBinders for T, so we finally get
3854 (a::*) (b::*) (k::*) (c::k)
3855 The function etaExpandAlgTyCon generates these extra TyConBinders from
3856 the result kind signature.
3857
3858 We need to take care to give the TyConBinders
3859 (a) OccNames that are fresh (because the TyConBinders of a TyCon
3860 must have distinct OccNames
3861
3862 (b) Uniques that are fresh (obviously)
3863
3864 For (a) we need to avoid clashes with the tyvars declared by
3865 the user before the "::"; in the above example that is 'a'.
3866 And also see Note [Avoid name clashes for associated data types].
3867
3868 For (b) suppose we have
3869 data T :: forall k. k -> forall k. k -> *
3870 where the two k's are identical even up to their uniques. Surprisingly,
3871 this can happen: see #14515.
3872
3873 It's reasonably easy to solve all this; just run down the list with a
3874 substitution; hence the recursive 'go' function. But it has to be
3875 done.
3876
3877 Note [Avoid name clashes for associated data types]
3878 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3879 Consider class C a b where
3880 data D b :: * -> *
3881 When typechecking the decl for D, we'll invent an extra type variable
3882 for D, to fill out its kind. Ideally we don't want this type variable
3883 to be 'a', because when pretty printing we'll get
3884 class C a b where
3885 data D b a0
3886 (NB: the tidying happens in the conversion to Iface syntax, which happens
3887 as part of pretty-printing a TyThing.)
3888
3889 That's why we look in the LocalRdrEnv to see what's in scope. This is
3890 important only to get nice-looking output when doing ":info C" in GHCi.
3891 It isn't essential for correctness.
3892
3893
3894 ************************************************************************
3895 * *
3896 Partial signatures
3897 * *
3898 ************************************************************************
3899
3900 -}
3901
3902 tcHsPartialSigType
3903 :: UserTypeCtxt
3904 -> LHsSigWcType GhcRn -- The type signature
3905 -> TcM ( [(Name, TcTyVar)] -- Wildcards
3906 , Maybe TcType -- Extra-constraints wildcard
3907 , [(Name,InvisTVBinder)] -- Original tyvar names, in correspondence with
3908 -- the implicitly and explicitly bound type variables
3909 , TcThetaType -- Theta part
3910 , TcType ) -- Tau part
3911 -- See Note [Checking partial type signatures]
3912 tcHsPartialSigType ctxt sig_ty
3913 | HsWC { hswc_ext = sig_wcs, hswc_body = sig_ty } <- sig_ty
3914 , L _ (HsSig{sig_bndrs = hs_outer_bndrs, sig_body = body_ty}) <- sig_ty
3915 , (hs_ctxt, hs_tau) <- splitLHsQualTy body_ty
3916 = addSigCtxt ctxt sig_ty $
3917 do { mode <- mkHoleMode TypeLevel HM_Sig
3918 ; (outer_bndrs, (wcs, wcx, theta, tau))
3919 <- solveEqualities "tcHsPartialSigType" $
3920 -- See Note [Failure in local type signatures]
3921 bindNamedWildCardBinders sig_wcs $ \ wcs ->
3922 bindOuterSigTKBndrs_Tv_M mode hs_outer_bndrs $
3923 do { -- Instantiate the type-class context; but if there
3924 -- is an extra-constraints wildcard, just discard it here
3925 (theta, wcx) <- tcPartialContext mode hs_ctxt
3926
3927 ; ek <- newOpenTypeKind
3928 ; tau <- addTypeCtxt hs_tau $
3929 tc_lhs_type mode hs_tau ek
3930
3931 ; return (wcs, wcx, theta, tau) }
3932
3933 ; traceTc "tcHsPartialSigType 2" empty
3934 ; outer_tv_bndrs <- scopedSortOuter outer_bndrs
3935 ; traceTc "tcHsPartialSigType 3" empty
3936
3937 -- No kind-generalization here:
3938 ; kindGeneralizeNone (mkInvisForAllTys outer_tv_bndrs $
3939 mkPhiTy theta $
3940 tau)
3941
3942 -- Spit out the wildcards (including the extra-constraints one)
3943 -- as "hole" constraints, so that they'll be reported if necessary
3944 -- See Note [Extra-constraint holes in partial type signatures]
3945 ; mapM_ emitNamedTypeHole wcs
3946
3947 -- Zonk, so that any nested foralls can "see" their occurrences
3948 -- See Note [Checking partial type signatures], and in particular
3949 -- Note [Levels for wildcards]
3950 ; outer_tv_bndrs <- mapM zonkInvisTVBinder outer_tv_bndrs
3951 ; theta <- mapM zonkTcType theta
3952 ; tau <- zonkTcType tau
3953
3954 -- We return a proper (Name,InvisTVBinder) environment, to be sure that
3955 -- we bring the right name into scope in the function body.
3956 -- Test case: partial-sigs/should_compile/LocalDefinitionBug
3957 ; let outer_bndr_names :: [Name]
3958 outer_bndr_names = hsOuterTyVarNames hs_outer_bndrs
3959 tv_prs :: [(Name,InvisTVBinder)]
3960 tv_prs = outer_bndr_names `zip` outer_tv_bndrs
3961
3962 -- NB: checkValidType on the final inferred type will be
3963 -- done later by checkInferredPolyId. We can't do it
3964 -- here because we don't have a complete type to check
3965
3966 ; traceTc "tcHsPartialSigType" (ppr tv_prs)
3967 ; return (wcs, wcx, tv_prs, theta, tau) }
3968
3969 tcPartialContext :: TcTyMode -> Maybe (LHsContext GhcRn) -> TcM (TcThetaType, Maybe TcType)
3970 tcPartialContext _ Nothing = return ([], Nothing)
3971 tcPartialContext mode (Just (L _ hs_theta))
3972 | Just (hs_theta1, hs_ctxt_last) <- snocView hs_theta
3973 , L wc_loc ty@(HsWildCardTy _) <- ignoreParens hs_ctxt_last
3974 = do { wc_tv_ty <- setSrcSpanA wc_loc $
3975 tcAnonWildCardOcc YesExtraConstraint mode ty constraintKind
3976 ; theta <- mapM (tc_lhs_pred mode) hs_theta1
3977 ; return (theta, Just wc_tv_ty) }
3978 | otherwise
3979 = do { theta <- mapM (tc_lhs_pred mode) hs_theta
3980 ; return (theta, Nothing) }
3981
3982 {- Note [Checking partial type signatures]
3983 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3984 This Note is about tcHsPartialSigType. See also
3985 Note [Recipe for checking a signature]
3986
3987 When we have a partial signature like
3988 f :: forall a. a -> _
3989 we do the following
3990
3991 * tcHsPartialSigType does not make quantified type (forall a. blah)
3992 and then instantiate it -- it makes no sense to instantiate a type
3993 with wildcards in it. Rather, tcHsPartialSigType just returns the
3994 'a' and the 'blah' separately.
3995
3996 Nor, for the same reason, do we push a level in tcHsPartialSigType.
3997
3998 * We instantiate 'a' to a unification variable, a TyVarTv, and /not/
3999 a skolem; hence the "_Tv" in bindExplicitTKBndrs_Tv. Consider
4000 f :: forall a. a -> _
4001 g :: forall b. _ -> b
4002 f = g
4003 g = f
4004 They are typechecked as a recursive group, with monomorphic types,
4005 so 'a' and 'b' will get unified together. Very like kind inference
4006 for mutually recursive data types (sans CUSKs or SAKS); see
4007 Note [Cloning for type variable binders]
4008
4009 * In GHC.Tc.Gen.Sig.tcUserSigType we return a PartialSig, which (unlike
4010 the companion CompleteSig) contains the original, as-yet-unchecked
4011 source-code LHsSigWcType
4012
4013 * Then, for f and g /separately/, we call tcInstSig, which in turn
4014 call tchsPartialSig (defined near this Note). It kind-checks the
4015 LHsSigWcType, creating fresh unification variables for each "_"
4016 wildcard. It's important that the wildcards for f and g are distinct
4017 because they might get instantiated completely differently. E.g.
4018 f,g :: forall a. a -> _
4019 f x = a
4020 g x = True
4021 It's really as if we'd written two distinct signatures.
4022
4023 * Nested foralls. See Note [Levels for wildcards]
4024
4025 * Just as for ordinary signatures, we must solve local equalities and
4026 zonk the type after kind-checking it, to ensure that all the nested
4027 forall binders can "see" their occurrenceds
4028
4029 Just as for ordinary signatures, this zonk also gets any Refl casts
4030 out of the way of instantiation. Example: #18008 had
4031 foo :: (forall a. (Show a => blah) |> Refl) -> _
4032 and that Refl cast messed things up. See #18062.
4033
4034 Note [Levels for wildcards]
4035 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
4036 Consider
4037 f :: forall b. (forall a. a -> _) -> b
4038 We do /not/ allow the "_" to be instantiated to 'a'; although we do
4039 (as before) allow it to be instantiated to the (top level) 'b'.
4040 Why not? Suppose
4041 f x = (x True, x 'c')
4042
4043 During typecking the RHS we must instantiate that (forall a. a -> _),
4044 so we must know /precisely/ where all the a's are; they must not be
4045 hidden under (possibly-not-yet-filled-in) unification variables!
4046
4047 We achieve this as follows:
4048
4049 - For /named/ wildcards such sas
4050 g :: forall b. (forall la. a -> _x) -> b
4051 there is no problem: we create them at the outer level (ie the
4052 ambient level of the signature itself), and push the level when we
4053 go inside a forall. So now the unification variable for the "_x"
4054 can't unify with skolem 'a'.
4055
4056 - For /anonymous/ wildcards, such as 'f' above, we carry the ambient
4057 level of the signature to the hole in the TcLevel part of the
4058 mode_holes field of TcTyMode. Then, in tcAnonWildCardOcc we us that
4059 level (and /not/ the level ambient at the occurrence of "_") to
4060 create the unification variable for the wildcard. That is the sole
4061 purpose of the TcLevel in the mode_holes field: to transport the
4062 ambient level of the signature down to the anonymous wildcard
4063 occurrences.
4064
4065 Note [Extra-constraint holes in partial type signatures]
4066 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4067 Consider
4068 f :: (_) => a -> a
4069 f x = ...
4070
4071 * The renamer leaves '_' untouched.
4072
4073 * Then, in tcHsPartialSigType, we make a new hole TcTyVar, in
4074 tcWildCardBinders.
4075
4076 * GHC.Tc.Gen.Bind.chooseInferredQuantifiers fills in that hole TcTyVar
4077 with the inferred constraints, e.g. (Eq a, Show a)
4078
4079 * GHC.Tc.Errors.mkHoleError finally reports the error.
4080
4081 An annoying difficulty happens if there are more than 64 inferred
4082 constraints. Then we need to fill in the TcTyVar with (say) a 70-tuple.
4083 Where do we find the TyCon? For good reasons we only have constraint
4084 tuples up to 62 (see Note [How tuples work] in GHC.Builtin.Types). So how
4085 can we make a 70-tuple? This was the root cause of #14217.
4086
4087 It's incredibly tiresome, because we only need this type to fill
4088 in the hole, to communicate to the error reporting machinery. Nothing
4089 more. So I use a HACK:
4090
4091 * I make an /ordinary/ tuple of the constraints, in
4092 GHC.Tc.Gen.Bind.chooseInferredQuantifiers. This is ill-kinded because
4093 ordinary tuples can't contain constraints, but it works fine. And for
4094 ordinary tuples we don't have the same limit as for constraint
4095 tuples (which need selectors and an associated class).
4096
4097 * Because it is ill-kinded (unifying something of kind Constraint with
4098 something of kind Type), it should trip an assert in writeMetaTyVarRef.
4099 However, writeMetaTyVarRef uses eqType, not tcEqType, to avoid falling
4100 over in this scenario (and another scenario, as detailed in
4101 Note [coreView vs tcView] in GHC.Core.Type).
4102
4103 Result works fine, but it may eventually bite us.
4104
4105 See also Note [Do not simplify ConstraintHoles] in GHC.Tc.Solver for
4106 information about how these are printed.
4107
4108 ************************************************************************
4109 * *
4110 Pattern signatures (i.e signatures that occur in patterns)
4111 * *
4112 ********************************************************************* -}
4113
4114 tcHsPatSigType :: UserTypeCtxt
4115 -> HoleMode -- HM_Sig when in a SigPat, HM_TyAppPat when in a ConPat checking type applications.
4116 -> HsPatSigType GhcRn -- The type signature
4117 -> ContextKind -- What kind is expected
4118 -> TcM ( [(Name, TcTyVar)] -- Wildcards
4119 , [(Name, TcTyVar)] -- The new bit of type environment, binding
4120 -- the scoped type variables
4121 , TcType) -- The type
4122 -- Used for type-checking type signatures in
4123 -- (a) patterns e.g f (x::Int) = e
4124 -- (b) RULE forall bndrs e.g. forall (x::Int). f x = x
4125 -- See Note [Pattern signature binders and scoping] in GHC.Hs.Type
4126 --
4127 -- This may emit constraints
4128 -- See Note [Recipe for checking a signature]
4129 tcHsPatSigType ctxt hole_mode
4130 (HsPS { hsps_ext = HsPSRn { hsps_nwcs = sig_wcs, hsps_imp_tvs = sig_ns }
4131 , hsps_body = hs_ty })
4132 ctxt_kind
4133 = addSigCtxt ctxt hs_ty $
4134 do { sig_tkv_prs <- mapM new_implicit_tv sig_ns
4135 ; mode <- mkHoleMode TypeLevel hole_mode
4136 ; (wcs, sig_ty)
4137 <- addTypeCtxt hs_ty $
4138 solveEqualities "tcHsPatSigType" $
4139 -- See Note [Failure in local type signatures]
4140 -- and c.f #16033
4141 bindNamedWildCardBinders sig_wcs $ \ wcs ->
4142 tcExtendNameTyVarEnv sig_tkv_prs $
4143 do { ek <- newExpectedKind ctxt_kind
4144 ; sig_ty <- tc_lhs_type mode hs_ty ek
4145 ; return (wcs, sig_ty) }
4146
4147 ; mapM_ emitNamedTypeHole wcs
4148
4149 -- sig_ty might have tyvars that are at a higher TcLevel (if hs_ty
4150 -- contains a forall). Promote these.
4151 -- Ex: f (x :: forall a. Proxy a -> ()) = ... x ...
4152 -- When we instantiate x, we have to compare the kind of the argument
4153 -- to a's kind, which will be a metavariable.
4154 -- kindGeneralizeNone does this:
4155 ; kindGeneralizeNone sig_ty
4156 ; sig_ty <- zonkTcType sig_ty
4157 ; checkValidType ctxt sig_ty
4158
4159 ; traceTc "tcHsPatSigType" (ppr sig_tkv_prs)
4160 ; return (wcs, sig_tkv_prs, sig_ty) }
4161 where
4162 new_implicit_tv name
4163 = do { kind <- newMetaKindVar
4164 ; tv <- case ctxt of
4165 RuleSigCtxt {} -> newSkolemTyVar name kind
4166 _ -> newPatSigTyVar name kind
4167 -- See Note [Typechecking pattern signature binders]
4168 -- NB: tv's Name may be fresh (in the case of newPatSigTyVar)
4169 ; return (name, tv) }
4170
4171 {- Note [Typechecking pattern signature binders]
4172 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4173 See also Note [Type variables in the type environment] in GHC.Tc.Utils.
4174 Consider
4175
4176 data T where
4177 MkT :: forall a. a -> (a -> Int) -> T
4178
4179 f :: T -> ...
4180 f (MkT x (f :: b -> c)) = <blah>
4181
4182 Here
4183 * The pattern (MkT p1 p2) creates a *skolem* type variable 'a_sk',
4184 It must be a skolem so that it retains its identity, and
4185 GHC.Tc.Errors.getSkolemInfo can thereby find the binding site for the skolem.
4186
4187 * The type signature pattern (f :: b -> c) makes fresh meta-tyvars
4188 beta and gamma (TauTvs), and binds "b" :-> beta, "c" :-> gamma in the
4189 environment
4190
4191 * Then unification makes beta := a_sk, gamma := Int
4192 That's why we must make beta and gamma a MetaTv,
4193 not a SkolemTv, so that it can unify to a_sk (or Int, respectively).
4194
4195 * Finally, in '<blah>' we have the envt "b" :-> beta, "c" :-> gamma,
4196 so we return the pairs ("b" :-> beta, "c" :-> gamma) from tcHsPatSigType,
4197
4198 Another example (#13881):
4199 fl :: forall (l :: [a]). Sing l -> Sing l
4200 fl (SNil :: Sing (l :: [y])) = SNil
4201 When we reach the pattern signature, 'l' is in scope from the
4202 outer 'forall':
4203 "a" :-> a_sk :: *
4204 "l" :-> l_sk :: [a_sk]
4205 We make up a fresh meta-TauTv, y_sig, for 'y', and kind-check
4206 the pattern signature
4207 Sing (l :: [y])
4208 That unifies y_sig := a_sk. We return from tcHsPatSigType with
4209 the pair ("y" :-> y_sig).
4210
4211 For RULE binders, though, things are a bit different (yuk).
4212 RULE "foo" forall (x::a) (y::[a]). f x y = ...
4213 Here this really is the binding site of the type variable so we'd like
4214 to use a skolem, so that we get a complaint if we unify two of them
4215 together. Hence the new_implicit_tv function in tcHsPatSigType.
4216
4217
4218 ************************************************************************
4219 * *
4220 Checking kinds
4221 * *
4222 ************************************************************************
4223
4224 -}
4225
4226 unifyKinds :: [LHsType GhcRn] -> [(TcType, TcKind)] -> TcM ([TcType], TcKind)
4227 unifyKinds rn_tys act_kinds
4228 = do { kind <- newMetaKindVar
4229 ; let check rn_ty (ty, act_kind)
4230 = checkExpectedKind (unLoc rn_ty) ty act_kind kind
4231 ; tys' <- zipWithM check rn_tys act_kinds
4232 ; return (tys', kind) }
4233
4234 {-
4235 ************************************************************************
4236 * *
4237 Sort checking kinds
4238 * *
4239 ************************************************************************
4240
4241 tcLHsKindSig converts a user-written kind to an internal, sort-checked kind.
4242 It does sort checking and desugaring at the same time, in one single pass.
4243 -}
4244
4245 tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
4246 tcLHsKindSig ctxt hs_kind
4247 = tc_lhs_kind_sig kindLevelMode ctxt hs_kind
4248
4249 tc_lhs_kind_sig :: TcTyMode -> UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
4250 tc_lhs_kind_sig mode ctxt hs_kind
4251 -- See Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType
4252 -- Result is zonked
4253 = do { kind <- addErrCtxt (text "In the kind" <+> quotes (ppr hs_kind)) $
4254 solveEqualities "tcLHsKindSig" $
4255 tc_lhs_type mode hs_kind liftedTypeKind
4256 ; traceTc "tcLHsKindSig" (ppr hs_kind $$ ppr kind)
4257 -- No generalization:
4258 ; kindGeneralizeNone kind
4259 ; kind <- zonkTcType kind
4260 -- This zonk is very important in the case of higher rank kinds
4261 -- E.g. #13879 f :: forall (p :: forall z (y::z). <blah>).
4262 -- <more blah>
4263 -- When instantiating p's kind at occurrences of p in <more blah>
4264 -- it's crucial that the kind we instantiate is fully zonked,
4265 -- else we may fail to substitute properly
4266
4267 ; checkValidType ctxt kind
4268 ; traceTc "tcLHsKindSig2" (ppr kind)
4269 ; return kind }
4270
4271 promotionErr :: Name -> PromotionErr -> TcM a
4272 promotionErr name err
4273 = failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
4274 (hang (pprPECategory err <+> quotes (ppr name) <+> text "cannot be used here")
4275 2 (parens reason))
4276 where
4277 reason = case err of
4278 ConstrainedDataConPE pred
4279 -> text "it has an unpromotable context"
4280 <+> quotes (ppr pred)
4281 FamDataConPE -> text "it comes from a data family instance"
4282 NoDataKindsTC -> text "perhaps you intended to use DataKinds"
4283 NoDataKindsDC -> text "perhaps you intended to use DataKinds"
4284 PatSynPE -> text "pattern synonyms cannot be promoted"
4285 RecDataConPE -> same_rec_group_msg
4286 ClassPE -> same_rec_group_msg
4287 TyConPE -> same_rec_group_msg
4288
4289 same_rec_group_msg = text "it is defined and used in the same recursive group"
4290
4291 {-
4292 ************************************************************************
4293 * *
4294 Error messages and such
4295 * *
4296 ************************************************************************
4297 -}
4298
4299
4300 -- | Make an appropriate message for an error in a function argument.
4301 -- Used for both expressions and types.
4302 funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc
4303 funAppCtxt fun arg arg_no
4304 = hang (hsep [ text "In the", speakNth arg_no, text "argument of",
4305 quotes (ppr fun) <> text ", namely"])
4306 2 (quotes (ppr arg))
4307
4308 -- | Add a "In the data declaration for T" or some such.
4309 addTyConFlavCtxt :: Name -> TyConFlavour -> TcM a -> TcM a
4310 addTyConFlavCtxt name flav
4311 = addErrCtxt $ hsep [ text "In the", ppr flav
4312 , text "declaration for", quotes (ppr name) ]