never executed always true always false
1
2 {-# LANGUAGE DerivingStrategies #-}
3
4 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
5 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
6
7 {-
8 (c) The University of Glasgow 2006
9 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
10 -}
11
12 module GHC.Tc.Validity (
13 Rank(..), UserTypeCtxt(..), checkValidType, checkValidMonoType,
14 checkValidTheta,
15 checkValidInstance, checkValidInstHead, validDerivPred,
16 checkTySynRhs,
17 checkValidCoAxiom, checkValidCoAxBranch,
18 checkValidTyFamEqn, checkValidAssocTyFamDeflt, checkConsistentFamInst,
19 arityErr,
20 checkTyConTelescope,
21 allDistinctTyVars
22 ) where
23
24 import GHC.Prelude
25
26 import GHC.Data.Maybe
27
28 -- friends:
29 import GHC.Tc.Utils.Unify ( tcSubTypeSigma )
30 import GHC.Tc.Solver ( simplifyAmbiguityCheck )
31 import GHC.Tc.Instance.Class ( matchGlobalInst, ClsInstResult(..), InstanceWhat(..), AssocInstInfo(..) )
32 import GHC.Core.TyCo.FVs
33 import GHC.Core.TyCo.Rep
34 import GHC.Core.TyCo.Ppr
35 import GHC.Tc.Utils.TcType hiding ( sizeType, sizeTypes )
36 import GHC.Builtin.Types
37 import GHC.Builtin.Names
38 import GHC.Core.Type
39 import GHC.Core.Unify ( tcMatchTyX_BM, BindFlag(..) )
40 import GHC.Core.Coercion
41 import GHC.Core.Coercion.Axiom
42 import GHC.Core.Class
43 import GHC.Core.TyCon
44 import GHC.Core.Predicate
45 import GHC.Tc.Types.Origin
46 import GHC.Tc.Types.Rank
47 import GHC.Tc.Errors.Types
48
49 -- others:
50 import GHC.Iface.Type ( pprIfaceType, pprIfaceTypeApp )
51 import GHC.CoreToIface ( toIfaceTyCon, toIfaceTcArgs, toIfaceType )
52 import GHC.Hs
53 import GHC.Tc.Utils.Monad
54 import GHC.Tc.Utils.Env ( tcInitTidyEnv, tcInitOpenTidyEnv )
55 import GHC.Tc.Instance.FunDeps
56 import GHC.Core.FamInstEnv
57 ( isDominatedBy, injectiveBranches, InjectivityCheckResult(..) )
58 import GHC.Tc.Instance.Family
59 import GHC.Types.Name
60 import GHC.Types.Var.Env
61 import GHC.Types.Var.Set
62 import GHC.Types.Var ( VarBndr(..), mkTyVar )
63 import GHC.Utils.FV
64 import GHC.Utils.Error
65 import GHC.Driver.Session
66 import GHC.Utils.Misc
67 import GHC.Data.List.SetOps
68 import GHC.Types.SrcLoc
69 import GHC.Utils.Outputable as Outputable
70 import GHC.Utils.Panic
71 import GHC.Builtin.Uniques ( mkAlphaTyVarUnique )
72 import qualified GHC.LanguageExtensions as LangExt
73
74 import Control.Monad
75 import Data.Foldable
76 import Data.Function
77 import Data.List ( (\\), nub )
78 import qualified Data.List.NonEmpty as NE
79
80 {-
81 ************************************************************************
82 * *
83 Checking for ambiguity
84 * *
85 ************************************************************************
86
87 Note [The ambiguity check for type signatures]
88 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
89 checkAmbiguity is a check on *user-supplied type signatures*. It is
90 *purely* there to report functions that cannot possibly be called. So for
91 example we want to reject:
92 f :: C a => Int
93 The idea is there can be no legal calls to 'f' because every call will
94 give rise to an ambiguous constraint. We could soundly omit the
95 ambiguity check on type signatures entirely, at the expense of
96 delaying ambiguity errors to call sites. Indeed, the flag
97 -XAllowAmbiguousTypes switches off the ambiguity check.
98
99 What about things like this:
100 class D a b | a -> b where ..
101 h :: D Int b => Int
102 The Int may well fix 'b' at the call site, so that signature should
103 not be rejected. Moreover, using *visible* fundeps is too
104 conservative. Consider
105 class X a b where ...
106 class D a b | a -> b where ...
107 instance D a b => X [a] b where...
108 h :: X a b => a -> a
109 Here h's type looks ambiguous in 'b', but here's a legal call:
110 ...(h [True])...
111 That gives rise to a (X [Bool] beta) constraint, and using the
112 instance means we need (D Bool beta) and that fixes 'beta' via D's
113 fundep!
114
115 Behind all these special cases there is a simple guiding principle.
116 Consider
117
118 f :: <type>
119 f = ...blah...
120
121 g :: <type>
122 g = f
123
124 You would think that the definition of g would surely typecheck!
125 After all f has exactly the same type, and g=f. But in fact f's type
126 is instantiated and the instantiated constraints are solved against
127 the originals, so in the case of an ambiguous type it won't work.
128 Consider our earlier example f :: C a => Int. Then in g's definition,
129 we'll instantiate to (C alpha) and try to deduce (C alpha) from (C a),
130 and fail.
131
132 So in fact we use this as our *definition* of ambiguity. We use a
133 very similar test for *inferred* types, to ensure that they are
134 unambiguous. See Note [Impedance matching] in GHC.Tc.Gen.Bind.
135
136 This test is very conveniently implemented by calling
137 tcSubType <type> <type>
138 This neatly takes account of the functional dependency stuff above,
139 and implicit parameter (see Note [Implicit parameters and ambiguity]).
140 And this is what checkAmbiguity does.
141
142 What about this, though?
143 g :: C [a] => Int
144 Is every call to 'g' ambiguous? After all, we might have
145 instance C [a] where ...
146 at the call site. So maybe that type is ok! Indeed even f's
147 quintessentially ambiguous type might, just possibly be callable:
148 with -XFlexibleInstances we could have
149 instance C a where ...
150 and now a call could be legal after all! Well, we'll reject this
151 unless the instance is available *here*.
152
153 Note [When to call checkAmbiguity]
154 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
155 We call checkAmbiguity
156 (a) on user-specified type signatures
157 (b) in checkValidType
158
159 Conncerning (b), you might wonder about nested foralls. What about
160 f :: forall b. (forall a. Eq a => b) -> b
161 The nested forall is ambiguous. Originally we called checkAmbiguity
162 in the forall case of check_type, but that had two bad consequences:
163 * We got two error messages about (Eq b) in a nested forall like this:
164 g :: forall a. Eq a => forall b. Eq b => a -> a
165 * If we try to check for ambiguity of a nested forall like
166 (forall a. Eq a => b), the implication constraint doesn't bind
167 all the skolems, which results in "No skolem info" in error
168 messages (see #10432).
169
170 To avoid this, we call checkAmbiguity once, at the top, in checkValidType.
171 (I'm still a bit worried about unbound skolems when the type mentions
172 in-scope type variables.)
173
174 In fact, because of the co/contra-variance implemented in tcSubType,
175 this *does* catch function f above. too.
176
177 Concerning (a) the ambiguity check is only used for *user* types, not
178 for types coming from interface files. The latter can legitimately
179 have ambiguous types. Example
180
181 class S a where s :: a -> (Int,Int)
182 instance S Char where s _ = (1,1)
183 f:: S a => [a] -> Int -> (Int,Int)
184 f (_::[a]) x = (a*x,b)
185 where (a,b) = s (undefined::a)
186
187 Here the worker for f gets the type
188 fw :: forall a. S a => Int -> (# Int, Int #)
189
190
191 Note [Implicit parameters and ambiguity]
192 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
193 Only a *class* predicate can give rise to ambiguity
194 An *implicit parameter* cannot. For example:
195 foo :: (?x :: [a]) => Int
196 foo = length ?x
197 is fine. The call site will supply a particular 'x'
198
199 Furthermore, the type variables fixed by an implicit parameter
200 propagate to the others. E.g.
201 foo :: (Show a, ?x::[a]) => Int
202 foo = show (?x++?x)
203 The type of foo looks ambiguous. But it isn't, because at a call site
204 we might have
205 let ?x = 5::Int in foo
206 and all is well. In effect, implicit parameters are, well, parameters,
207 so we can take their type variables into account as part of the
208 "tau-tvs" stuff. This is done in the function 'GHC.Tc.Instance.FunDeps.grow'.
209 -}
210
211 checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
212 checkAmbiguity ctxt ty
213 | wantAmbiguityCheck ctxt
214 = do { traceTc "Ambiguity check for" (ppr ty)
215 -- Solve the constraints eagerly because an ambiguous type
216 -- can cause a cascade of further errors. Since the free
217 -- tyvars are skolemised, we can safely use tcSimplifyTop
218 ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
219 ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
220 captureConstraints $
221 tcSubTypeSigma ctxt ty ty
222 ; simplifyAmbiguityCheck ty wanted
223
224 ; traceTc "Done ambiguity check for" (ppr ty) }
225
226 | otherwise
227 = return ()
228 where
229 mk_msg allow_ambiguous
230 = vcat [ text "In the ambiguity check for" <+> what
231 , ppUnless allow_ambiguous ambig_msg ]
232 ambig_msg = text "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes"
233 what | Just n <- isSigMaybe ctxt = quotes (ppr n)
234 | otherwise = pprUserTypeCtxt ctxt
235
236 wantAmbiguityCheck :: UserTypeCtxt -> Bool
237 wantAmbiguityCheck ctxt
238 = case ctxt of -- See Note [When we don't check for ambiguity]
239 GhciCtxt {} -> False
240 TySynCtxt {} -> False
241 TypeAppCtxt -> False
242 StandaloneKindSigCtxt{} -> False
243 _ -> True
244
245 -- | Check whether the type signature contains custom type errors,
246 -- and fail if so.
247 --
248 -- Note that some custom type errors are acceptable:
249 --
250 -- - in the RHS of a type synonym, e.g. to allow users to define
251 -- type synonyms for custom type errors with large messages (#20181),
252 -- - inside a type family application, as a custom type error
253 -- might evaporate after performing type family reduction (#20241).
254 checkUserTypeError :: UserTypeCtxt -> Type -> TcM ()
255 -- Very unsatisfactorily (#11144) we need to tidy the type
256 -- because it may have come from an /inferred/ signature, not a
257 -- user-supplied one. This is really only a half-baked fix;
258 -- the other errors in checkValidType don't do tidying, and so
259 -- may give bad error messages when given an inferred type.
260 checkUserTypeError ctxt ty
261 | TySynCtxt {} <- ctxt -- Do not complain about TypeError on the
262 = return () -- RHS of type synonyms. See #20181
263
264 | otherwise
265 = check ty
266 where
267 check ty
268 | Just msg <- userTypeError_maybe ty = fail_with msg
269 | Just (_,t1) <- splitForAllTyCoVar_maybe ty = check t1
270 | let (_,tys) = splitAppTys ty = mapM_ check tys
271 -- splitAppTys keeps type family applications saturated.
272 -- This means we don't go looking for user type errors
273 -- inside type family arguments (see #20241).
274
275 fail_with :: Type -> TcM ()
276 fail_with msg = do { env0 <- tcInitTidyEnv
277 ; let (env1, tidy_msg) = tidyOpenType env0 msg
278 ; failWithTcM (env1, TcRnUserTypeError tidy_msg)
279 }
280
281
282 {- Note [When we don't check for ambiguity]
283 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
284 In a few places we do not want to check a user-specified type for ambiguity
285
286 * GhciCtxt: Allow ambiguous types in GHCi's :kind command
287 E.g. type family T a :: * -- T :: forall k. k -> *
288 Then :k T should work in GHCi, not complain that
289 (T k) is ambiguous!
290
291 * TySynCtxt: type T a b = C a b => blah
292 It may be that when we /use/ T, we'll give an 'a' or 'b' that somehow
293 cure the ambiguity. So we defer the ambiguity check to the use site.
294
295 There is also an implementation reason (#11608). In the RHS of
296 a type synonym we don't (currently) instantiate 'a' and 'b' with
297 TcTyVars before calling checkValidType, so we get assertion failures
298 from doing an ambiguity check on a type with TyVars in it. Fixing this
299 would not be hard, but let's wait till there's a reason.
300
301 * TypeAppCtxt: visible type application
302 f @ty
303 No need to check ty for ambiguity
304
305 * StandaloneKindSigCtxt: type T :: ksig
306 Kinds need a different ambiguity check than types, and the currently
307 implemented check is only good for types. See #14419, in particular
308 https://gitlab.haskell.org/ghc/ghc/issues/14419#note_160844
309
310 ************************************************************************
311 * *
312 Checking validity of a user-defined type
313 * *
314 ************************************************************************
315
316 When dealing with a user-written type, we first translate it from an HsType
317 to a Type, performing kind checking, and then check various things that should
318 be true about it. We don't want to perform these checks at the same time
319 as the initial translation because (a) they are unnecessary for interface-file
320 types and (b) when checking a mutually recursive group of type and class decls,
321 we can't "look" at the tycons/classes yet. Also, the checks are rather
322 diverse, and used to really mess up the other code.
323
324 One thing we check for is 'rank'.
325
326 Rank 0: monotypes (no foralls)
327 Rank 1: foralls at the front only, Rank 0 inside
328 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
329
330 basic ::= tyvar | T basic ... basic
331
332 r2 ::= forall tvs. cxt => r2a
333 r2a ::= r1 -> r2a | basic
334 r1 ::= forall tvs. cxt => r0
335 r0 ::= r0 -> r0 | basic
336
337 Another thing is to check that type synonyms are saturated.
338 This might not necessarily show up in kind checking.
339 type A i = i
340 data T k = MkT (k Int)
341 f :: T A -- BAD!
342 -}
343
344 checkValidType :: UserTypeCtxt -> Type -> TcM ()
345 -- Checks that a user-written type is valid for the given context
346 -- Assumes argument is fully zonked
347 -- Not used for instance decls; checkValidInstance instead
348 checkValidType ctxt ty
349 = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty))
350 ; rankn_flag <- xoptM LangExt.RankNTypes
351 ; impred_flag <- xoptM LangExt.ImpredicativeTypes
352 ; let gen_rank :: Rank -> Rank
353 gen_rank r | rankn_flag = ArbitraryRank
354 | otherwise = r
355
356 rank1 = gen_rank r1
357 rank0 = gen_rank MonoTypeRankZero
358
359 r1 = LimitedRank True MonoTypeRankZero
360
361 rank
362 = case ctxt of
363 DefaultDeclCtxt-> MustBeMonoType
364 PatSigCtxt -> rank0
365 RuleSigCtxt _ -> rank1
366 TySynCtxt _ -> rank0
367
368 ExprSigCtxt {} -> rank1
369 KindSigCtxt -> rank1
370 StandaloneKindSigCtxt{} -> rank1
371 TypeAppCtxt | impred_flag -> ArbitraryRank
372 | otherwise -> MonoTypeTyConArg
373 -- Normally, ImpredicativeTypes is handled in check_arg_type,
374 -- but visible type applications don't go through there.
375 -- So we do this check here.
376
377 FunSigCtxt {} -> rank1
378 InfSigCtxt {} -> rank1 -- Inferred types should obey the
379 -- same rules as declared ones
380
381 ConArgCtxt _ -> rank1 -- We are given the type of the entire
382 -- constructor, hence rank 1
383 PatSynCtxt _ -> rank1
384
385 ForSigCtxt _ -> rank1
386 SpecInstCtxt -> rank1
387 GhciCtxt {} -> ArbitraryRank
388
389 TyVarBndrKindCtxt _ -> rank0
390 DataKindCtxt _ -> rank1
391 TySynKindCtxt _ -> rank1
392 TyFamResKindCtxt _ -> rank1
393
394 _ -> panic "checkValidType"
395 -- Can't happen; not used for *user* sigs
396
397 ; env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
398 ; expand <- initialExpandMode
399 ; let ve = ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
400 , ve_rank = rank, ve_expand = expand }
401
402 -- Check the internal validity of the type itself
403 -- Fail if bad things happen, else we misleading
404 -- (and more complicated) errors in checkAmbiguity
405 ; checkNoErrs $
406 do { check_type ve ty
407 ; checkUserTypeError ctxt ty
408 ; traceTc "done ct" (ppr ty) }
409
410 -- Check for ambiguous types. See Note [When to call checkAmbiguity]
411 -- NB: this will happen even for monotypes, but that should be cheap;
412 -- and there may be nested foralls for the subtype test to examine
413 ; checkAmbiguity ctxt ty
414
415 ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty)) }
416
417 checkValidMonoType :: Type -> TcM ()
418 -- Assumes argument is fully zonked
419 checkValidMonoType ty
420 = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
421 ; expand <- initialExpandMode
422 ; let ve = ValidityEnv{ ve_tidy_env = env, ve_ctxt = SigmaCtxt
423 , ve_rank = MustBeMonoType, ve_expand = expand }
424 ; check_type ve ty }
425
426 checkTySynRhs :: UserTypeCtxt -> TcType -> TcM ()
427 checkTySynRhs ctxt ty
428 | tcReturnsConstraintKind actual_kind
429 = do { ck <- xoptM LangExt.ConstraintKinds
430 ; if ck
431 then when (tcIsConstraintKind actual_kind)
432 (do { dflags <- getDynFlags
433 ; expand <- initialExpandMode
434 ; check_pred_ty emptyTidyEnv dflags ctxt expand ty })
435 else addErrTcM ( emptyTidyEnv
436 , TcRnIllegalConstraintSynonymOfKind (tidyKind emptyTidyEnv actual_kind)
437 ) }
438
439 | otherwise
440 = return ()
441 where
442 actual_kind = tcTypeKind ty
443
444 funArgResRank :: Rank -> (Rank, Rank) -- Function argument and result
445 funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
446 funArgResRank other_rank = (other_rank, other_rank)
447
448 forAllAllowed :: Rank -> Bool
449 forAllAllowed ArbitraryRank = True
450 forAllAllowed (LimitedRank forall_ok _) = forall_ok
451 forAllAllowed _ = False
452
453 -- | Indicates whether a 'UserTypeCtxt' represents type-level contexts,
454 -- kind-level contexts, or both.
455 data TypeOrKindCtxt
456 = OnlyTypeCtxt
457 -- ^ A 'UserTypeCtxt' that only represents type-level positions.
458 | OnlyKindCtxt
459 -- ^ A 'UserTypeCtxt' that only represents kind-level positions.
460 | BothTypeAndKindCtxt
461 -- ^ A 'UserTypeCtxt' that can represent both type- and kind-level positions.
462 deriving Eq
463
464 instance Outputable TypeOrKindCtxt where
465 ppr ctxt = text $ case ctxt of
466 OnlyTypeCtxt -> "OnlyTypeCtxt"
467 OnlyKindCtxt -> "OnlyKindCtxt"
468 BothTypeAndKindCtxt -> "BothTypeAndKindCtxt"
469
470 -- | Determine whether a 'UserTypeCtxt' can represent type-level contexts,
471 -- kind-level contexts, or both.
472 typeOrKindCtxt :: UserTypeCtxt -> TypeOrKindCtxt
473 typeOrKindCtxt (FunSigCtxt {}) = OnlyTypeCtxt
474 typeOrKindCtxt (InfSigCtxt {}) = OnlyTypeCtxt
475 typeOrKindCtxt (ExprSigCtxt {}) = OnlyTypeCtxt
476 typeOrKindCtxt (TypeAppCtxt {}) = OnlyTypeCtxt
477 typeOrKindCtxt (PatSynCtxt {}) = OnlyTypeCtxt
478 typeOrKindCtxt (PatSigCtxt {}) = OnlyTypeCtxt
479 typeOrKindCtxt (RuleSigCtxt {}) = OnlyTypeCtxt
480 typeOrKindCtxt (ForSigCtxt {}) = OnlyTypeCtxt
481 typeOrKindCtxt (DefaultDeclCtxt {}) = OnlyTypeCtxt
482 typeOrKindCtxt (InstDeclCtxt {}) = OnlyTypeCtxt
483 typeOrKindCtxt (SpecInstCtxt {}) = OnlyTypeCtxt
484 typeOrKindCtxt (GenSigCtxt {}) = OnlyTypeCtxt
485 typeOrKindCtxt (ClassSCCtxt {}) = OnlyTypeCtxt
486 typeOrKindCtxt (SigmaCtxt {}) = OnlyTypeCtxt
487 typeOrKindCtxt (DataTyCtxt {}) = OnlyTypeCtxt
488 typeOrKindCtxt (DerivClauseCtxt {}) = OnlyTypeCtxt
489 typeOrKindCtxt (ConArgCtxt {}) = OnlyTypeCtxt
490 -- Although data constructors can be promoted with DataKinds, we always
491 -- validity-check them as though they are the types of terms. We may need
492 -- to revisit this decision if we ever allow visible dependent quantification
493 -- in the types of data constructors.
494
495 typeOrKindCtxt (KindSigCtxt {}) = OnlyKindCtxt
496 typeOrKindCtxt (StandaloneKindSigCtxt {}) = OnlyKindCtxt
497 typeOrKindCtxt (TyVarBndrKindCtxt {}) = OnlyKindCtxt
498 typeOrKindCtxt (DataKindCtxt {}) = OnlyKindCtxt
499 typeOrKindCtxt (TySynKindCtxt {}) = OnlyKindCtxt
500 typeOrKindCtxt (TyFamResKindCtxt {}) = OnlyKindCtxt
501
502 typeOrKindCtxt (TySynCtxt {}) = BothTypeAndKindCtxt
503 -- Type synonyms can have types and kinds on their RHSs
504 typeOrKindCtxt (GhciCtxt {}) = BothTypeAndKindCtxt
505 -- GHCi's :kind command accepts both types and kinds
506
507 -- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
508 -- context for a kind of a type.
509 -- If the 'UserTypeCtxt' can refer to both types and kinds, this function
510 -- conservatively returns 'True'.
511 --
512 -- An example of something that is unambiguously the kind of a type is the
513 -- @Show a => a -> a@ in @type Foo :: Show a => a -> a@. On the other hand, the
514 -- same type in @foo :: Show a => a -> a@ is unambiguously the type of a term,
515 -- not the kind of a type, so it is permitted.
516 typeLevelUserTypeCtxt :: UserTypeCtxt -> Bool
517 typeLevelUserTypeCtxt ctxt = case typeOrKindCtxt ctxt of
518 OnlyTypeCtxt -> True
519 OnlyKindCtxt -> False
520 BothTypeAndKindCtxt -> True
521
522 -- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
523 -- context for a kind of a type, where the arbitrary use of constraints is
524 -- currently disallowed.
525 -- (See @Note [Constraints in kinds]@ in "GHC.Core.TyCo.Rep".)
526 allConstraintsAllowed :: UserTypeCtxt -> Bool
527 allConstraintsAllowed = typeLevelUserTypeCtxt
528
529 -- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
530 -- context for a kind of a type, where all function arrows currently
531 -- must be unrestricted.
532 linearityAllowed :: UserTypeCtxt -> Bool
533 linearityAllowed = typeLevelUserTypeCtxt
534
535 -- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
536 -- context for the type of a term, where visible, dependent quantification is
537 -- currently disallowed. If the 'UserTypeCtxt' can refer to both types and
538 -- kinds, this function conservatively returns 'True'.
539 --
540 -- An example of something that is unambiguously the type of a term is the
541 -- @forall a -> a -> a@ in @foo :: forall a -> a -> a@. On the other hand, the
542 -- same type in @type family Foo :: forall a -> a -> a@ is unambiguously the
543 -- kind of a type, not the type of a term, so it is permitted.
544 --
545 -- For more examples, see
546 -- @testsuite/tests/dependent/should_compile/T16326_Compile*.hs@ (for places
547 -- where VDQ is permitted) and
548 -- @testsuite/tests/dependent/should_fail/T16326_Fail*.hs@ (for places where
549 -- VDQ is disallowed).
550 vdqAllowed :: UserTypeCtxt -> Bool
551 vdqAllowed ctxt = case typeOrKindCtxt ctxt of
552 OnlyTypeCtxt -> False
553 OnlyKindCtxt -> True
554 BothTypeAndKindCtxt -> True
555
556 {-
557 Note [Correctness and performance of type synonym validity checking]
558 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
559 Consider the type A arg1 arg2, where A is a type synonym. How should we check
560 this type for validity? We have three distinct choices, corresponding to the
561 three constructors of ExpandMode:
562
563 1. Expand the application of A, and check the resulting type (`Expand`).
564 2. Don't expand the application of A. Only check the arguments (`NoExpand`).
565 3. Check the arguments *and* check the expanded type (`Both`).
566
567 It's tempting to think that we could always just pick choice (3), but this
568 results in serious performance issues when checking a type like in the
569 signature for `f` below:
570
571 type S = ...
572 f :: S (S (S (S (S (S ....(S Int)...))))
573
574 When checking the type of `f`, we'll check the outer `S` application with and
575 without expansion, and in *each* of those checks, we'll check the next `S`
576 application with and without expansion... the result is exponential blowup! So
577 clearly we don't want to use `Both` 100% of the time.
578
579 On the other hand, neither is it correct to use exclusively `Expand` or
580 exclusively `NoExpand` 100% of the time:
581
582 * If one always expands, then one can miss erroneous programs like the one in
583 the `tcfail129` test case:
584
585 type Foo a = String -> Maybe a
586 type Bar m = m Int
587 blah = undefined :: Bar Foo
588
589 If we expand `Bar Foo` immediately, we'll miss the fact that the `Foo` type
590 synonyms is unsaturated.
591 * If one never expands and only checks the arguments, then one can miss
592 erroneous programs like the one in #16059:
593
594 type Foo b = Eq b => b
595 f :: forall b (a :: Foo b). Int
596
597 The kind of `a` contains a constraint, which is illegal, but this will only
598 be caught if `Foo b` is expanded.
599
600 Therefore, it's impossible to have these validity checks be simultaneously
601 correct and performant if one sticks exclusively to a single `ExpandMode`. In
602 that case, the solution is to vary the `ExpandMode`s! In more detail:
603
604 1. When we start validity checking, we start with `Expand` if
605 LiberalTypeSynonyms is enabled (see Note [Liberal type synonyms] for why we
606 do this), and we start with `Both` otherwise. The `initialExpandMode`
607 function is responsible for this.
608 2. When expanding an application of a type synonym (in `check_syn_tc_app`), we
609 determine which things to check based on the current `ExpandMode` argument.
610 Importantly, if the current mode is `Both`, then we check the arguments in
611 `NoExpand` mode and check the expanded type in `Both` mode.
612
613 Switching to `NoExpand` when checking the arguments is vital to avoid
614 exponential blowup. One consequence of this choice is that if you have
615 the following type synonym in one module (with RankNTypes enabled):
616
617 {-# LANGUAGE RankNTypes #-}
618 module A where
619 type A = forall a. a
620
621 And you define the following in a separate module *without* RankNTypes
622 enabled:
623
624 module B where
625
626 import A
627
628 type Const a b = a
629 f :: Const Int A -> Int
630
631 Then `f` will be accepted, even though `A` (which is technically a rank-n
632 type) appears in its type. We view this as an acceptable compromise, since
633 `A` never appears in the type of `f` post-expansion. If `A` _did_ appear in
634 a type post-expansion, such as in the following variant:
635
636 g :: Const A A -> Int
637
638 Then that would be rejected unless RankNTypes were enabled.
639 -}
640
641 -- | When validity-checking an application of a type synonym, should we
642 -- check the arguments, check the expanded type, or both?
643 -- See Note [Correctness and performance of type synonym validity checking]
644 data ExpandMode
645 = Expand -- ^ Only check the expanded type.
646 | NoExpand -- ^ Only check the arguments.
647 | Both -- ^ Check both the arguments and the expanded type.
648
649 instance Outputable ExpandMode where
650 ppr e = text $ case e of
651 Expand -> "Expand"
652 NoExpand -> "NoExpand"
653 Both -> "Both"
654
655 -- | If @LiberalTypeSynonyms@ is enabled, we start in 'Expand' mode for the
656 -- reasons explained in @Note [Liberal type synonyms]@. Otherwise, we start
657 -- in 'Both' mode.
658 initialExpandMode :: TcM ExpandMode
659 initialExpandMode = do
660 liberal_flag <- xoptM LangExt.LiberalTypeSynonyms
661 pure $ if liberal_flag then Expand else Both
662
663 -- | Information about a type being validity-checked.
664 data ValidityEnv = ValidityEnv
665 { ve_tidy_env :: TidyEnv
666 , ve_ctxt :: UserTypeCtxt
667 , ve_rank :: Rank
668 , ve_expand :: ExpandMode }
669
670 instance Outputable ValidityEnv where
671 ppr (ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
672 , ve_rank = rank, ve_expand = expand }) =
673 hang (text "ValidityEnv")
674 2 (vcat [ text "ve_tidy_env" <+> ppr env
675 , text "ve_ctxt" <+> pprUserTypeCtxt ctxt
676 , text "ve_rank" <+> ppr rank
677 , text "ve_expand" <+> ppr expand ])
678
679 ----------------------------------------
680 check_type :: ValidityEnv -> Type -> TcM ()
681 -- The args say what the *type context* requires, independent
682 -- of *flag* settings. You test the flag settings at usage sites.
683 --
684 -- Rank is allowed rank for function args
685 -- Rank 0 means no for-alls anywhere
686
687 check_type _ (TyVarTy _) = return ()
688
689 check_type ve (AppTy ty1 ty2)
690 = do { check_type ve ty1
691 ; check_arg_type False ve ty2 }
692
693 check_type ve ty@(TyConApp tc tys)
694 | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
695 = check_syn_tc_app ve ty tc tys
696 | isUnboxedTupleTyCon tc
697 = check_ubx_tuple ve ty tys
698 | otherwise
699 = mapM_ (check_arg_type False ve) tys
700
701 check_type _ (LitTy {}) = return ()
702
703 check_type ve (CastTy ty _) = check_type ve ty
704
705 -- Check for rank-n types, such as (forall x. x -> x) or (Show x => x).
706 --
707 -- Critically, this case must come *after* the case for TyConApp.
708 -- See Note [Liberal type synonyms].
709 check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
710 , ve_rank = rank, ve_expand = expand }) ty
711 | not (null tvbs && null theta)
712 = do { traceTc "check_type" (ppr ty $$ ppr rank)
713 ; checkTcM (forAllAllowed rank) (env, TcRnForAllRankErr rank (tidyType env ty))
714 -- Reject e.g. (Maybe (?x::Int => Int)),
715 -- with a decent error message
716
717 ; checkConstraintsOK ve theta ty
718 -- Reject forall (a :: Eq b => b). blah
719 -- In a kind signature we don't allow constraints
720
721 ; checkTcM (all (isInvisibleArgFlag . binderArgFlag) tvbs
722 || vdqAllowed ctxt)
723 (env, TcRnVDQInTermType (tidyType env ty))
724 -- Reject visible, dependent quantification in the type of a
725 -- term (e.g., `f :: forall a -> a -> Maybe a`)
726
727 ; check_valid_theta env' SigmaCtxt expand theta
728 -- Allow type T = ?x::Int => Int -> Int
729 -- but not type T = ?x::Int
730
731 ; check_type (ve{ve_tidy_env = env'}) tau
732 -- Allow foralls to right of arrow
733
734 ; checkEscapingKind env' tvbs' theta tau }
735 where
736 (tvbs, phi) = tcSplitForAllTyVarBinders ty
737 (theta, tau) = tcSplitPhiTy phi
738 (env', tvbs') = tidyTyCoVarBinders env tvbs
739
740 check_type (ve@ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
741 , ve_rank = rank })
742 ty@(FunTy _ mult arg_ty res_ty)
743 = do { failIfTcM (not (linearityAllowed ctxt) && not (isManyDataConTy mult))
744 (env, TcRnLinearFuncInKind (tidyType env ty))
745 ; check_type (ve{ve_rank = arg_rank}) arg_ty
746 ; check_type (ve{ve_rank = res_rank}) res_ty }
747 where
748 (arg_rank, res_rank) = funArgResRank rank
749
750 check_type _ ty = pprPanic "check_type" (ppr ty)
751
752 ----------------------------------------
753 check_syn_tc_app :: ValidityEnv
754 -> KindOrType -> TyCon -> [KindOrType] -> TcM ()
755 -- Used for type synonyms and type synonym families,
756 -- which must be saturated,
757 -- but not data families, which need not be saturated
758 check_syn_tc_app (ve@ValidityEnv{ ve_ctxt = ctxt, ve_expand = expand })
759 ty tc tys
760 | tys `lengthAtLeast` tc_arity -- Saturated
761 -- Check that the synonym has enough args
762 -- This applies equally to open and closed synonyms
763 -- It's OK to have an *over-applied* type synonym
764 -- data Tree a b = ...
765 -- type Foo a = Tree [a]
766 -- f :: Foo a b -> ...
767 = case expand of
768 _ | isTypeFamilyTyCon tc
769 -> check_args_only expand
770 -- See Note [Correctness and performance of type synonym validity
771 -- checking]
772 Expand -> check_expansion_only expand
773 NoExpand -> check_args_only expand
774 Both -> check_args_only NoExpand *> check_expansion_only Both
775
776 | GhciCtxt True <- ctxt -- Accept outermost under-saturated type synonym or
777 -- type family constructors in GHCi :kind commands.
778 -- See Note [Unsaturated type synonyms in GHCi]
779 = check_args_only expand
780
781 | otherwise
782 = failWithTc (tyConArityErr tc tys)
783 where
784 tc_arity = tyConArity tc
785
786 check_arg :: ExpandMode -> KindOrType -> TcM ()
787 check_arg expand =
788 check_arg_type (isTypeSynonymTyCon tc) (ve{ve_expand = expand})
789
790 check_args_only, check_expansion_only :: ExpandMode -> TcM ()
791 check_args_only expand = mapM_ (check_arg expand) tys
792
793 check_expansion_only expand
794 = assertPpr (isTypeSynonymTyCon tc) (ppr tc) $
795 case tcView ty of
796 Just ty' -> let err_ctxt = text "In the expansion of type synonym"
797 <+> quotes (ppr tc)
798 in addErrCtxt err_ctxt $
799 check_type (ve{ve_expand = expand}) ty'
800 Nothing -> pprPanic "check_syn_tc_app" (ppr ty)
801
802 {-
803 Note [Unsaturated type synonyms in GHCi]
804 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
805 Generally speaking, GHC disallows unsaturated uses of type synonyms or type
806 families. For instance, if one defines `type Const a b = a`, then GHC will not
807 permit using `Const` unless it is applied to (at least) two arguments. There is
808 an exception to this rule, however: GHCi's :kind command. For instance, it
809 is quite common to look up the kind of a type constructor like so:
810
811 λ> :kind Const
812 Const :: j -> k -> j
813 λ> :kind Const Int
814 Const Int :: k -> Type
815
816 Strictly speaking, the two uses of `Const` above are unsaturated, but this
817 is an extremely benign (and useful) example of unsaturation, so we allow it
818 here as a special case.
819
820 That being said, we do not allow unsaturation carte blanche in GHCi. Otherwise,
821 this GHCi interaction would be possible:
822
823 λ> newtype Fix f = MkFix (f (Fix f))
824 λ> type Id a = a
825 λ> :kind Fix Id
826 Fix Id :: Type
827
828 This is rather dodgy, so we move to disallow this. We only permit unsaturated
829 synonyms in GHCi if they are *top-level*—that is, if the synonym is the
830 outermost type being applied. This allows `Const` and `Const Int` in the
831 first example, but not `Fix Id` in the second example, as `Id` is not the
832 outermost type being applied (`Fix` is).
833
834 We track this outermost property in the GhciCtxt constructor of UserTypeCtxt.
835 A field of True in GhciCtxt indicates that we're in an outermost position. Any
836 time we invoke `check_arg` to check the validity of an argument, we switch the
837 field to False.
838 -}
839
840 ----------------------------------------
841 check_ubx_tuple :: ValidityEnv -> KindOrType -> [KindOrType] -> TcM ()
842 check_ubx_tuple (ve@ValidityEnv{ve_tidy_env = env}) ty tys
843 = do { ub_tuples_allowed <- xoptM LangExt.UnboxedTuples
844 ; checkTcM ub_tuples_allowed (env, TcRnUnboxedTupleTypeFuncArg (tidyType env ty))
845
846 ; impred <- xoptM LangExt.ImpredicativeTypes
847 ; let rank' = if impred then ArbitraryRank else MonoTypeTyConArg
848 -- c.f. check_arg_type
849 -- However, args are allowed to be unlifted, or
850 -- more unboxed tuples, so can't use check_arg_ty
851 ; mapM_ (check_type (ve{ve_rank = rank'})) tys }
852
853 ----------------------------------------
854 check_arg_type
855 :: Bool -- ^ Is this the argument to a type synonym?
856 -> ValidityEnv -> KindOrType -> TcM ()
857 -- The sort of type that can instantiate a type variable,
858 -- or be the argument of a type constructor.
859 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
860 -- Other unboxed types are very occasionally allowed as type
861 -- arguments depending on the kind of the type constructor
862 --
863 -- For example, we want to reject things like:
864 --
865 -- instance Ord a => Ord (forall s. T s a)
866 -- and
867 -- g :: T s (forall b.b)
868 --
869 -- NB: unboxed tuples can have polymorphic or unboxed args.
870 -- This happens in the workers for functions returning
871 -- product types with polymorphic components.
872 -- But not in user code.
873 -- Anyway, they are dealt with by a special case in check_tau_type
874
875 check_arg_type _ _ (CoercionTy {}) = return ()
876
877 check_arg_type type_syn (ve@ValidityEnv{ve_ctxt = ctxt, ve_rank = rank}) ty
878 = do { impred <- xoptM LangExt.ImpredicativeTypes
879 ; let rank' = case rank of -- Predictive => must be monotype
880 -- Rank-n arguments to type synonyms are OK, provided
881 -- that LiberalTypeSynonyms is enabled.
882 _ | type_syn -> MonoTypeSynArg
883 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
884 _other | impred -> ArbitraryRank
885 | otherwise -> MonoTypeTyConArg
886 -- Make sure that MustBeMonoType is propagated,
887 -- so that we don't suggest -XImpredicativeTypes in
888 -- (Ord (forall a.a)) => a -> a
889 -- and so that if it Must be a monotype, we check that it is!
890 ctxt' :: UserTypeCtxt
891 ctxt'
892 | GhciCtxt _ <- ctxt = GhciCtxt False
893 -- When checking an argument, set the field of GhciCtxt to
894 -- False to indicate that we are no longer in an outermost
895 -- position (and thus unsaturated synonyms are no longer
896 -- allowed).
897 -- See Note [Unsaturated type synonyms in GHCi]
898 | otherwise = ctxt
899
900 ; check_type (ve{ve_ctxt = ctxt', ve_rank = rank'}) ty }
901
902 ----------------------------------------
903
904 -- | Reject type variables that would escape their escape through a kind.
905 -- See @Note [Type variables escaping through kinds]@.
906 checkEscapingKind :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> TcM ()
907 checkEscapingKind env tvbs theta tau =
908 case occCheckExpand (binderVars tvbs) phi_kind of
909 -- Ensure that none of the tvs occur in the kind of the forall
910 -- /after/ expanding type synonyms.
911 -- See Note [Phantom type variables in kinds] in GHC.Core.Type
912 Nothing -> failWithTcM $ forAllEscapeErr env tvbs theta tau tau_kind
913 Just _ -> pure ()
914 where
915 tau_kind = tcTypeKind tau
916 phi_kind | null theta = tau_kind
917 | otherwise = liftedTypeKind
918 -- If there are any constraints, the kind is *. (#11405)
919
920 forAllEscapeErr :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> Kind
921 -> (TidyEnv, TcRnMessage)
922 forAllEscapeErr env tvbs theta tau tau_kind
923 -- NB: Don't tidy the sigma type since the tvbs were already tidied
924 -- previously, and re-tidying them will make the names of type
925 -- variables different from tau_kind.
926 = (env, TcRnForAllEscapeError (mkSigmaTy tvbs theta tau) (tidyKind env tau_kind))
927
928 {-
929 Note [Type variables escaping through kinds]
930 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
931 Consider:
932
933 type family T (r :: RuntimeRep) :: TYPE r
934 foo :: forall r. T r
935
936 Something smells funny about the type of `foo`. If you spell out the kind
937 explicitly, it becomes clearer from where the smell originates:
938
939 foo :: ((forall r. T r) :: TYPE r)
940
941 The type variable `r` appears in the result kind, which escapes the scope of
942 its binding site! This is not desirable, so we establish a validity check
943 (`checkEscapingKind`) to catch any type variables that might escape through
944 kinds in this way.
945 -}
946
947 checkConstraintsOK :: ValidityEnv -> ThetaType -> Type -> TcM ()
948 checkConstraintsOK ve theta ty
949 | null theta = return ()
950 | allConstraintsAllowed (ve_ctxt ve) = return ()
951 | otherwise
952 = -- We are in a kind, where we allow only equality predicates
953 -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep, and #16263
954 checkTcM (all isEqPred theta) (env, TcRnConstraintInKind (tidyType env ty))
955 where env = ve_tidy_env ve
956
957 {-
958 Note [Liberal type synonyms]
959 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
960 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
961 doing validity checking. This allows us to instantiate a synonym defn
962 with a for-all type, or with a partially-applied type synonym.
963 e.g. type T a b = a
964 type S m = m ()
965 f :: S (T Int)
966 Here, T is partially applied, so it's illegal in H98. But if you
967 expand S first, then T we get just
968 f :: Int
969 which is fine.
970
971 IMPORTANT: suppose T is a type synonym. Then we must do validity
972 checking on an application (T ty1 ty2)
973
974 *either* before expansion (i.e. check ty1, ty2)
975 *or* after expansion (i.e. expand T ty1 ty2, and then check)
976 BUT NOT BOTH
977
978 If we do both, we get exponential behaviour!!
979
980 data TIACons1 i r c = c i ::: r c
981 type TIACons2 t x = TIACons1 t (TIACons1 t x)
982 type TIACons3 t x = TIACons2 t (TIACons1 t x)
983 type TIACons4 t x = TIACons2 t (TIACons2 t x)
984 type TIACons7 t x = TIACons4 t (TIACons3 t x)
985
986 The order in which you do validity checking is also somewhat delicate. Consider
987 the `check_type` function, which drives the validity checking for unsaturated
988 uses of type synonyms. There is a special case for rank-n types, such as
989 (forall x. x -> x) or (Show x => x), since those require at least one language
990 extension to use. It used to be the case that this case came before every other
991 case, but this can lead to bugs. Imagine you have this scenario (from #15954):
992
993 type A a = Int
994 type B (a :: Type -> Type) = forall x. x -> x
995 type C = B A
996
997 If the rank-n case came first, then in the process of checking for `forall`s
998 or contexts, we would expand away `B A` to `forall x. x -> x`. This is because
999 the functions that split apart `forall`s/contexts
1000 (tcSplitForAllTyVarBinders/tcSplitPhiTy) expand type synonyms! If `B A` is expanded
1001 away to `forall x. x -> x` before the actually validity checks occur, we will
1002 have completely obfuscated the fact that we had an unsaturated application of
1003 the `A` type synonym.
1004
1005 We have since learned from our mistakes and now put this rank-n case /after/
1006 the case for TyConApp, which ensures that an unsaturated `A` TyConApp will be
1007 caught properly. But be careful! We can't make the rank-n case /last/ either,
1008 as the FunTy case must came after the rank-n case. Otherwise, something like
1009 (Eq a => Int) would be treated as a function type (FunTy), which just
1010 wouldn't do.
1011
1012 ************************************************************************
1013 * *
1014 \subsection{Checking a theta or source type}
1015 * *
1016 ************************************************************************
1017
1018 Note [Implicit parameters in instance decls]
1019 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1020 Implicit parameters _only_ allowed in type signatures; not in instance
1021 decls, superclasses etc. The reason for not allowing implicit params in
1022 instances is a bit subtle. If we allowed
1023 instance (?x::Int, Eq a) => Foo [a] where ...
1024 then when we saw
1025 (e :: (?x::Int) => t)
1026 it would be unclear how to discharge all the potential uses of the ?x
1027 in e. For example, a constraint Foo [Int] might come out of e, and
1028 applying the instance decl would show up two uses of ?x. #8912.
1029 -}
1030
1031 checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
1032 -- Assumes argument is fully zonked
1033 checkValidTheta ctxt theta
1034 = addErrCtxtM (checkThetaCtxt ctxt theta) $
1035 do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypesList theta)
1036 ; expand <- initialExpandMode
1037 ; check_valid_theta env ctxt expand theta }
1038
1039 -------------------------
1040 check_valid_theta :: TidyEnv -> UserTypeCtxt -> ExpandMode
1041 -> [PredType] -> TcM ()
1042 check_valid_theta _ _ _ []
1043 = return ()
1044 check_valid_theta env ctxt expand theta
1045 = do { dflags <- getDynFlags
1046 ; traceTc "check_valid_theta" (ppr theta)
1047 ; mapM_ (check_pred_ty env dflags ctxt expand) theta }
1048
1049 -------------------------
1050 {- Note [Validity checking for constraints]
1051 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1052 We look through constraint synonyms so that we can see the underlying
1053 constraint(s). For example
1054 type Foo = ?x::Int
1055 instance Foo => C T
1056 We should reject the instance because it has an implicit parameter in
1057 the context.
1058
1059 But we record, in 'under_syn', whether we have looked under a synonym
1060 to avoid requiring language extensions at the use site. Main example
1061 (#9838):
1062
1063 {-# LANGUAGE ConstraintKinds #-}
1064 module A where
1065 type EqShow a = (Eq a, Show a)
1066
1067 module B where
1068 import A
1069 foo :: EqShow a => a -> String
1070
1071 We don't want to require ConstraintKinds in module B.
1072 -}
1073
1074 check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> ExpandMode
1075 -> PredType -> TcM ()
1076 -- Check the validity of a predicate in a signature
1077 -- See Note [Validity checking for constraints]
1078 check_pred_ty env dflags ctxt expand pred
1079 = do { check_type ve pred
1080 ; check_pred_help False env dflags ctxt pred }
1081 where
1082 rank | xopt LangExt.QuantifiedConstraints dflags
1083 = ArbitraryRank
1084 | otherwise
1085 = MonoTypeConstraint
1086
1087 ve :: ValidityEnv
1088 ve = ValidityEnv{ ve_tidy_env = env
1089 , ve_ctxt = SigmaCtxt
1090 , ve_rank = rank
1091 , ve_expand = expand }
1092
1093 check_pred_help :: Bool -- True <=> under a type synonym
1094 -> TidyEnv
1095 -> DynFlags -> UserTypeCtxt
1096 -> PredType -> TcM ()
1097 check_pred_help under_syn env dflags ctxt pred
1098 | Just pred' <- tcView pred -- Switch on under_syn when going under a
1099 -- synonym (#9838, yuk)
1100 = check_pred_help True env dflags ctxt pred'
1101
1102 | otherwise -- A bit like classifyPredType, but not the same
1103 -- E.g. we treat (~) like (~#); and we look inside tuples
1104 = case classifyPredType pred of
1105 ClassPred cls tys
1106 | isCTupleClass cls -> check_tuple_pred under_syn env dflags ctxt pred tys
1107 | otherwise -> check_class_pred env dflags ctxt pred cls tys
1108
1109 EqPred _ _ _ -> pprPanic "check_pred_help" (ppr pred)
1110 -- EqPreds, such as (t1 ~ #t2) or (t1 ~R# t2), don't even have kind Constraint
1111 -- and should never appear before the '=>' of a type. Thus
1112 -- f :: (a ~# b) => blah
1113 -- is wrong. For user written signatures, it'll be rejected by kind-checking
1114 -- well before we get to validity checking. For inferred types we are careful
1115 -- to box such constraints in GHC.Tc.Utils.TcType.pickQuantifiablePreds, as described
1116 -- in Note [Lift equality constraints when quantifying] in GHC.Tc.Utils.TcType
1117
1118 ForAllPred _ theta head -> check_quant_pred env dflags ctxt pred theta head
1119 _ -> return ()
1120
1121 check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TcM ()
1122 check_eq_pred env dflags pred
1123 = -- Equational constraints are valid in all contexts if type
1124 -- families are permitted
1125 checkTcM (xopt LangExt.TypeFamilies dflags
1126 || xopt LangExt.GADTs dflags)
1127 (env, TcRnIllegalEqualConstraints (tidyType env pred))
1128
1129 check_quant_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
1130 -> PredType -> ThetaType -> PredType -> TcM ()
1131 check_quant_pred env dflags ctxt pred theta head_pred
1132 = addErrCtxt (text "In the quantified constraint" <+> quotes (ppr pred)) $
1133 do { -- Check the instance head
1134 case classifyPredType head_pred of
1135 -- SigmaCtxt tells checkValidInstHead that
1136 -- this is the head of a quantified constraint
1137 ClassPred cls tys -> do { checkValidInstHead SigmaCtxt cls tys
1138 ; check_pred_help False env dflags ctxt head_pred }
1139 -- need check_pred_help to do extra pred-only validity
1140 -- checks, such as for (~). Otherwise, we get #17563
1141 -- NB: checks for the context are covered by the check_type
1142 -- in check_pred_ty
1143 IrredPred {} | hasTyVarHead head_pred
1144 -> return ()
1145 _ -> failWithTcM (env, TcRnBadQuantPredHead (tidyType env pred))
1146
1147 -- Check for termination
1148 ; unless (xopt LangExt.UndecidableInstances dflags) $
1149 checkInstTermination theta head_pred
1150 }
1151
1152 check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
1153 check_tuple_pred under_syn env dflags ctxt pred ts
1154 = do { -- See Note [ConstraintKinds in predicates]
1155 checkTcM (under_syn || xopt LangExt.ConstraintKinds dflags)
1156 (env, TcRnIllegalTupleConstraint (tidyType env pred))
1157 ; mapM_ (check_pred_help under_syn env dflags ctxt) ts }
1158 -- This case will not normally be executed because without
1159 -- -XConstraintKinds tuple types are only kind-checked as *
1160
1161 {- Note [ConstraintKinds in predicates]
1162 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1163 Don't check for -XConstraintKinds under a type synonym, because that
1164 was done at the type synonym definition site; see #9838
1165 e.g. module A where
1166 type C a = (Eq a, Ix a) -- Needs -XConstraintKinds
1167 module B where
1168 import A
1169 f :: C a => a -> a -- Does *not* need -XConstraintKinds
1170 -}
1171
1172 -------------------------
1173 check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
1174 -> PredType -> Class -> [TcType] -> TcM ()
1175 check_class_pred env dflags ctxt pred cls tys
1176 | isEqPredClass cls -- (~) and (~~) are classified as classes,
1177 -- but here we want to treat them as equalities
1178 = check_eq_pred env dflags pred
1179
1180 | isIPClass cls
1181 = do { check_arity
1182 ; checkTcM (okIPCtxt ctxt) (env, TcRnIllegalImplicitParam (tidyType env pred)) }
1183
1184 | otherwise -- Includes Coercible
1185 = do { check_arity
1186 ; checkSimplifiableClassConstraint env dflags ctxt cls tys
1187 ; checkTcM arg_tys_ok (env, TcRnNonTypeVarArgInConstraint (tidyType env pred)) }
1188 where
1189 check_arity = checkTc (tys `lengthIs` classArity cls)
1190 (tyConArityErr (classTyCon cls) tys)
1191
1192 -- Check the arguments of a class constraint
1193 flexible_contexts = xopt LangExt.FlexibleContexts dflags
1194 arg_tys_ok = case ctxt of
1195 SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1196 InstDeclCtxt {} -> checkValidClsArgs flexible_contexts cls tys
1197 -- Further checks on head and theta
1198 -- in checkInstTermination
1199 _ -> checkValidClsArgs flexible_contexts cls tys
1200
1201 checkSimplifiableClassConstraint :: TidyEnv -> DynFlags -> UserTypeCtxt
1202 -> Class -> [TcType] -> TcM ()
1203 -- See Note [Simplifiable given constraints]
1204 checkSimplifiableClassConstraint env dflags ctxt cls tys
1205 | not (wopt Opt_WarnSimplifiableClassConstraints dflags)
1206 = return ()
1207 | xopt LangExt.MonoLocalBinds dflags
1208 = return ()
1209
1210 | DataTyCtxt {} <- ctxt -- Don't do this check for the "stupid theta"
1211 = return () -- of a data type declaration
1212
1213 | cls `hasKey` coercibleTyConKey
1214 = return () -- Oddly, we treat (Coercible t1 t2) as unconditionally OK
1215 -- matchGlobalInst will reply "yes" because we can reduce
1216 -- (Coercible a b) to (a ~R# b)
1217
1218 | otherwise
1219 = do { result <- matchGlobalInst dflags False cls tys
1220 ; case result of
1221 OneInst { cir_what = what }
1222 -> let dia = TcRnUnknownMessage $
1223 mkPlainDiagnostic (WarningWithFlag Opt_WarnSimplifiableClassConstraints)
1224 noHints
1225 (simplifiable_constraint_warn what)
1226 in addDiagnosticTc dia
1227 _ -> return () }
1228 where
1229 pred = mkClassPred cls tys
1230
1231 simplifiable_constraint_warn :: InstanceWhat -> SDoc
1232 simplifiable_constraint_warn what
1233 = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred))
1234 <+> text "matches")
1235 2 (ppr what)
1236 , hang (text "This makes type inference for inner bindings fragile;")
1237 2 (text "either use MonoLocalBinds, or simplify it using the instance") ]
1238
1239 {- Note [Simplifiable given constraints]
1240 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1241 A type signature like
1242 f :: Eq [(a,b)] => a -> b
1243 is very fragile, for reasons described at length in GHC.Tc.Solver.Interact
1244 Note [Instance and Given overlap]. As that Note discusses, for the
1245 most part the clever stuff in GHC.Tc.Solver.Interact means that we don't use a
1246 top-level instance if a local Given might fire, so there is no
1247 fragility. But if we /infer/ the type of a local let-binding, things
1248 can go wrong (#11948 is an example, discussed in the Note).
1249
1250 So this warning is switched on only if we have NoMonoLocalBinds; in
1251 that case the warning discourages users from writing simplifiable
1252 class constraints.
1253
1254 The warning only fires if the constraint in the signature
1255 matches the top-level instances in only one way, and with no
1256 unifiers -- that is, under the same circumstances that
1257 GHC.Tc.Solver.Interact.matchInstEnv fires an interaction with the top
1258 level instances. For example (#13526), consider
1259
1260 instance {-# OVERLAPPABLE #-} Eq (T a) where ...
1261 instance Eq (T Char) where ..
1262 f :: Eq (T a) => ...
1263
1264 We don't want to complain about this, even though the context
1265 (Eq (T a)) matches an instance, because the user may be
1266 deliberately deferring the choice so that the Eq (T Char)
1267 has a chance to fire when 'f' is called. And the fragility
1268 only matters when there's a risk that the instance might
1269 fire instead of the local 'given'; and there is no such
1270 risk in this case. Just use the same rules as for instance
1271 firing!
1272 -}
1273
1274 -------------------------
1275 okIPCtxt :: UserTypeCtxt -> Bool
1276 -- See Note [Implicit parameters in instance decls]
1277 okIPCtxt (FunSigCtxt {}) = True
1278 okIPCtxt (InfSigCtxt {}) = True
1279 okIPCtxt (ExprSigCtxt {}) = True
1280 okIPCtxt TypeAppCtxt = True
1281 okIPCtxt PatSigCtxt = True
1282 okIPCtxt GenSigCtxt = True
1283 okIPCtxt (ConArgCtxt {}) = True
1284 okIPCtxt (ForSigCtxt {}) = True -- ??
1285 okIPCtxt (GhciCtxt {}) = True
1286 okIPCtxt SigmaCtxt = True
1287 okIPCtxt (DataTyCtxt {}) = True
1288 okIPCtxt (PatSynCtxt {}) = True
1289 okIPCtxt (TySynCtxt {}) = True -- e.g. type Blah = ?x::Int
1290 -- #11466
1291
1292 okIPCtxt (KindSigCtxt {}) = False
1293 okIPCtxt (StandaloneKindSigCtxt {}) = False
1294 okIPCtxt (ClassSCCtxt {}) = False
1295 okIPCtxt (InstDeclCtxt {}) = False
1296 okIPCtxt (SpecInstCtxt {}) = False
1297 okIPCtxt (RuleSigCtxt {}) = False
1298 okIPCtxt DefaultDeclCtxt = False
1299 okIPCtxt DerivClauseCtxt = False
1300 okIPCtxt (TyVarBndrKindCtxt {}) = False
1301 okIPCtxt (DataKindCtxt {}) = False
1302 okIPCtxt (TySynKindCtxt {}) = False
1303 okIPCtxt (TyFamResKindCtxt {}) = False
1304
1305 {-
1306 Note [Kind polymorphic type classes]
1307 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1308 MultiParam check:
1309
1310 class C f where... -- C :: forall k. k -> Constraint
1311 instance C Maybe where...
1312
1313 The dictionary gets type [C * Maybe] even if it's not a MultiParam
1314 type class.
1315
1316 Flexibility check:
1317
1318 class C f where... -- C :: forall k. k -> Constraint
1319 data D a = D a
1320 instance C D where
1321
1322 The dictionary gets type [C * (D *)]. IA0_TODO it should be
1323 generalized actually.
1324 -}
1325
1326 checkThetaCtxt :: UserTypeCtxt -> ThetaType -> TidyEnv -> TcM (TidyEnv, SDoc)
1327 checkThetaCtxt ctxt theta env
1328 = return ( env
1329 , vcat [ text "In the context:" <+> pprTheta (tidyTypes env theta)
1330 , text "While checking" <+> pprUserTypeCtxt ctxt ] )
1331
1332 tyConArityErr :: TyCon -> [TcType] -> TcRnMessage
1333 -- For type-constructor arity errors, be careful to report
1334 -- the number of /visible/ arguments required and supplied,
1335 -- ignoring the /invisible/ arguments, which the user does not see.
1336 -- (e.g. #10516)
1337 tyConArityErr tc tks
1338 = arityErr (ppr (tyConFlavour tc)) (tyConName tc)
1339 tc_type_arity tc_type_args
1340 where
1341 vis_tks = filterOutInvisibleTypes tc tks
1342
1343 -- tc_type_arity = number of *type* args expected
1344 -- tc_type_args = number of *type* args encountered
1345 tc_type_arity = count isVisibleTyConBinder (tyConBinders tc)
1346 tc_type_args = length vis_tks
1347
1348 arityErr :: Outputable a => SDoc -> a -> Int -> Int -> TcRnMessage
1349 arityErr what name n m
1350 = TcRnUnknownMessage $ mkPlainError noHints $
1351 hsep [ text "The" <+> what, quotes (ppr name), text "should have",
1352 n_arguments <> comma, text "but has been given",
1353 if m==0 then text "none" else int m]
1354 where
1355 n_arguments | n == 0 = text "no arguments"
1356 | n == 1 = text "1 argument"
1357 | True = hsep [int n, text "arguments"]
1358
1359 {-
1360 ************************************************************************
1361 * *
1362 \subsection{Checking for a decent instance head type}
1363 * *
1364 ************************************************************************
1365
1366 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1367 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1368
1369 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1370 flag is on, or (2)~the instance is imported (they must have been
1371 compiled elsewhere). In these cases, we let them go through anyway.
1372
1373 We can also have instances for functions: @instance Foo (a -> b) ...@.
1374 -}
1375
1376 checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
1377 checkValidInstHead ctxt clas cls_args
1378 = do { dflags <- getDynFlags
1379 ; is_boot <- tcIsHsBootOrSig
1380 ; is_sig <- tcIsHsig
1381 ; check_special_inst_head dflags is_boot is_sig ctxt clas cls_args
1382 ; checkValidTypePats (classTyCon clas) cls_args
1383 }
1384
1385 {-
1386
1387 Note [Instances of built-in classes in signature files]
1388 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1389
1390 User defined instances for KnownNat, KnownSymbol, KnownChar,
1391 and Typeable are disallowed
1392 -- they are generated when needed by GHC itself, on-the-fly.
1393
1394 However, if they occur in a Backpack signature file, they have an
1395 entirely different meaning. To illustrate, suppose in M.hsig we see
1396
1397 signature M where
1398 data T :: Nat
1399 instance KnownNat T
1400
1401 That says that any module satisfying M.hsig must provide a KnownNat
1402 instance for T. We absolultely need that instance when compiling a
1403 module that imports M.hsig: see #15379 and
1404 Note [Fabricating Evidence for Literals in Backpack] in GHC.Tc.Instance.Class.
1405
1406 Hence, checkValidInstHead accepts a user-written instance declaration
1407 in hsig files, where `is_sig` is True.
1408
1409 -}
1410
1411 check_special_inst_head :: DynFlags -> Bool -> Bool
1412 -> UserTypeCtxt -> Class -> [Type] -> TcM ()
1413 -- Wow! There are a surprising number of ad-hoc special cases here.
1414 -- TODO: common up the logic for special typeclasses (see GHC ticket #20441).
1415 check_special_inst_head dflags is_boot is_sig ctxt clas cls_args
1416
1417 -- If not in an hs-boot file, abstract classes cannot have instances
1418 | isAbstractClass clas
1419 , not is_boot
1420 = failWithTc (TcRnAbstractClassInst clas)
1421
1422 -- For Typeable, don't complain about instances for
1423 -- standalone deriving; they are no-ops, and we warn about
1424 -- it in GHC.Tc.Deriv.deriveStandalone.
1425 | clas_nm == typeableClassName
1426 , not is_sig
1427 -- Note [Instances of built-in classes in signature files]
1428 , hand_written_bindings
1429 = failWithTc $ TcRnSpecialClassInst clas False
1430
1431 -- Handwritten instances of KnownNat/KnownSymbol
1432 -- are forbidden outside of signature files (#12837)
1433 | clas_nm `elem` [ knownNatClassName, knownSymbolClassName ]
1434 , not is_sig
1435 -- Note [Instances of built-in classes in signature files]
1436 , hand_written_bindings
1437 = failWithTc $ TcRnSpecialClassInst clas False
1438
1439 -- For the most part we don't allow
1440 -- instances for (~), (~~), or Coercible;
1441 -- but we DO want to allow them in quantified constraints:
1442 -- f :: (forall a b. Coercible a b => Coercible (m a) (m b)) => ...m...
1443 | clas_nm `elem` [ heqTyConName, eqTyConName, coercibleTyConName ]
1444 , not quantified_constraint
1445 = failWithTc $ TcRnSpecialClassInst clas False
1446
1447 -- Check for hand-written Generic instances (disallowed in Safe Haskell)
1448 | clas_nm `elem` genericClassNames
1449 , hand_written_bindings
1450 = do { failIfTc (safeLanguageOn dflags) (TcRnSpecialClassInst clas True)
1451 ; when (safeInferOn dflags) (recordUnsafeInfer emptyMessages) }
1452
1453 | clas_nm == hasFieldClassName
1454 = checkHasFieldInst clas cls_args
1455
1456 | isCTupleClass clas
1457 = failWithTc (TcRnTupleConstraintInst clas)
1458
1459 -- Check language restrictions on the args to the class
1460 | check_h98_arg_shape
1461 , Just msg <- mb_ty_args_msg
1462 = failWithTc (instTypeErr clas cls_args msg)
1463
1464 | otherwise
1465 = pure ()
1466 where
1467 clas_nm = getName clas
1468 ty_args = filterOutInvisibleTypes (classTyCon clas) cls_args
1469
1470 hand_written_bindings
1471 = case ctxt of
1472 InstDeclCtxt stand_alone -> not stand_alone
1473 SpecInstCtxt -> False
1474 DerivClauseCtxt -> False
1475 SigmaCtxt -> False
1476 _ -> True
1477
1478 check_h98_arg_shape = case ctxt of
1479 SpecInstCtxt -> False
1480 DerivClauseCtxt -> False
1481 SigmaCtxt -> False
1482 _ -> True
1483 -- SigmaCtxt: once we are in quantified-constraint land, we
1484 -- aren't so picky about enforcing H98-language restrictions
1485 -- E.g. we want to allow a head like Coercible (m a) (m b)
1486
1487
1488 -- When we are looking at the head of a quantified constraint,
1489 -- check_quant_pred sets ctxt to SigmaCtxt
1490 quantified_constraint = case ctxt of
1491 SigmaCtxt -> True
1492 _ -> False
1493
1494 head_type_synonym_msg = parens (
1495 text "All instance types must be of the form (T t1 ... tn)" $$
1496 text "where T is not a synonym." $$
1497 text "Use TypeSynonymInstances if you want to disable this.")
1498
1499 head_type_args_tyvars_msg = parens (vcat [
1500 text "All instance types must be of the form (T a1 ... an)",
1501 text "where a1 ... an are *distinct type variables*,",
1502 text "and each type variable appears at most once in the instance head.",
1503 text "Use FlexibleInstances if you want to disable this."])
1504
1505 head_one_type_msg = parens $
1506 text "Only one type can be given in an instance head." $$
1507 text "Use MultiParamTypeClasses if you want to allow more, or zero."
1508
1509 mb_ty_args_msg
1510 | not (xopt LangExt.TypeSynonymInstances dflags)
1511 , not (all tcInstHeadTyNotSynonym ty_args)
1512 = Just head_type_synonym_msg
1513
1514 | not (xopt LangExt.FlexibleInstances dflags)
1515 , not (all tcInstHeadTyAppAllTyVars ty_args)
1516 = Just head_type_args_tyvars_msg
1517
1518 | length ty_args /= 1
1519 , not (xopt LangExt.MultiParamTypeClasses dflags)
1520 , not (xopt LangExt.NullaryTypeClasses dflags && null ty_args)
1521 = Just head_one_type_msg
1522
1523 | otherwise
1524 = Nothing
1525
1526 tcInstHeadTyNotSynonym :: Type -> Bool
1527 -- Used in Haskell-98 mode, for the argument types of an instance head
1528 -- These must not be type synonyms, but everywhere else type synonyms
1529 -- are transparent, so we need a special function here
1530 tcInstHeadTyNotSynonym ty
1531 = case ty of -- Do not use splitTyConApp,
1532 -- because that expands synonyms!
1533 TyConApp tc _ -> not (isTypeSynonymTyCon tc) || tc == unrestrictedFunTyCon
1534 -- Allow (->), e.g. instance Category (->),
1535 -- even though it's a type synonym for FUN 'Many
1536 _ -> True
1537
1538 tcInstHeadTyAppAllTyVars :: Type -> Bool
1539 -- Used in Haskell-98 mode, for the argument types of an instance head
1540 -- These must be a constructor applied to type variable arguments
1541 -- or a type-level literal.
1542 -- But we allow
1543 -- 1) kind instantiations
1544 -- 2) the type (->) = FUN 'Many, even though it's not in this form.
1545 tcInstHeadTyAppAllTyVars ty
1546 | Just (tc, tys) <- tcSplitTyConApp_maybe (dropCasts ty)
1547 = let tys' = filterOutInvisibleTypes tc tys -- avoid kinds
1548 tys'' | tc == funTyCon, tys_h:tys_t <- tys', tys_h `eqType` manyDataConTy = tys_t
1549 | otherwise = tys'
1550 in ok tys''
1551 | LitTy _ <- ty = True -- accept type literals (#13833)
1552 | otherwise
1553 = False
1554 where
1555 -- Check that all the types are type variables,
1556 -- and that each is distinct
1557 ok tys = equalLength tvs tys && hasNoDups tvs
1558 where
1559 tvs = mapMaybe tcGetTyVar_maybe tys
1560
1561 dropCasts :: Type -> Type
1562 -- See Note [Casts during validity checking]
1563 -- This function can turn a well-kinded type into an ill-kinded
1564 -- one, so I've kept it local to this module
1565 -- To consider: drop only HoleCo casts
1566 dropCasts (CastTy ty _) = dropCasts ty
1567 dropCasts (AppTy t1 t2) = mkAppTy (dropCasts t1) (dropCasts t2)
1568 dropCasts ty@(FunTy _ w t1 t2) = ty { ft_mult = dropCasts w, ft_arg = dropCasts t1, ft_res = dropCasts t2 }
1569 dropCasts (TyConApp tc tys) = mkTyConApp tc (map dropCasts tys)
1570 dropCasts (ForAllTy b ty) = ForAllTy (dropCastsB b) (dropCasts ty)
1571 dropCasts ty = ty -- LitTy, TyVarTy, CoercionTy
1572
1573 dropCastsB :: TyVarBinder -> TyVarBinder
1574 dropCastsB b = b -- Don't bother in the kind of a forall
1575
1576 instTypeErr :: Class -> [Type] -> SDoc -> TcRnMessage
1577 instTypeErr cls tys msg
1578 = TcRnUnknownMessage $ mkPlainError noHints $
1579 hang (hang (text "Illegal instance declaration for")
1580 2 (quotes (pprClassPred cls tys)))
1581 2 msg
1582
1583 -- | See Note [Validity checking of HasField instances]
1584 checkHasFieldInst :: Class -> [Type] -> TcM ()
1585 checkHasFieldInst cls tys@[_k_ty, x_ty, r_ty, _a_ty] =
1586 case splitTyConApp_maybe r_ty of
1587 Nothing -> whoops (text "Record data type must be specified")
1588 Just (tc, _)
1589 | isFamilyTyCon tc
1590 -> whoops (text "Record data type may not be a data family")
1591 | otherwise -> case isStrLitTy x_ty of
1592 Just lbl
1593 | isJust (lookupTyConFieldLabel lbl tc)
1594 -> whoops (ppr tc <+> text "already has a field"
1595 <+> quotes (ppr lbl))
1596 | otherwise -> return ()
1597 Nothing
1598 | null (tyConFieldLabels tc) -> return ()
1599 | otherwise -> whoops (ppr tc <+> text "has fields")
1600 where
1601 whoops = addErrTc . instTypeErr cls tys
1602 checkHasFieldInst _ tys = pprPanic "checkHasFieldInst" (ppr tys)
1603
1604 {- Note [Casts during validity checking]
1605 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1606 Consider the (bogus)
1607 instance Eq Char#
1608 We elaborate to 'Eq (Char# |> UnivCo(hole))' where the hole is an
1609 insoluble equality constraint for * ~ #. We'll report the insoluble
1610 constraint separately, but we don't want to *also* complain that Eq is
1611 not applied to a type constructor. So we look gaily look through
1612 CastTys here.
1613
1614 Another example: Eq (Either a). Then we actually get a cast in
1615 the middle:
1616 Eq ((Either |> g) a)
1617
1618
1619 Note [Validity checking of HasField instances]
1620 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1621 The HasField class has magic constraint solving behaviour (see Note
1622 [HasField instances] in GHC.Tc.Solver.Interact). However, we permit users to
1623 declare their own instances, provided they do not clash with the
1624 built-in behaviour. In particular, we forbid:
1625
1626 1. `HasField _ r _` where r is a variable
1627
1628 2. `HasField _ (T ...) _` if T is a data family
1629 (because it might have fields introduced later)
1630
1631 3. `HasField x (T ...) _` where x is a variable,
1632 if T has any fields at all
1633
1634 4. `HasField "foo" (T ...) _` if T has a "foo" field
1635
1636 The usual functional dependency checks also apply.
1637
1638
1639 Note [Valid 'deriving' predicate]
1640 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1641 validDerivPred checks for OK 'deriving' context. See Note [Exotic
1642 derived instance contexts] in GHC.Tc.Deriv. However the predicate is
1643 here because it uses sizeTypes, fvTypes.
1644
1645 It checks for three things
1646
1647 * No repeated variables (hasNoDups fvs)
1648
1649 * No type constructors. This is done by comparing
1650 sizeTypes tys == length (fvTypes tys)
1651 sizeTypes counts variables and constructors; fvTypes returns variables.
1652 So if they are the same, there must be no constructors. But there
1653 might be applications thus (f (g x)).
1654
1655 Note that tys only includes the visible arguments of the class type
1656 constructor. Including the non-visible arguments can cause the following,
1657 perfectly valid instance to be rejected:
1658 class Category (cat :: k -> k -> *) where ...
1659 newtype T (c :: * -> * -> *) a b = MkT (c a b)
1660 instance Category c => Category (T c) where ...
1661 since the first argument to Category is a non-visible *, which sizeTypes
1662 would count as a constructor! See #11833.
1663
1664 * Also check for a bizarre corner case, when the derived instance decl
1665 would look like
1666 instance C a b => D (T a) where ...
1667 Note that 'b' isn't a parameter of T. This gives rise to all sorts of
1668 problems; in particular, it's hard to compare solutions for equality
1669 when finding the fixpoint, and that means the inferContext loop does
1670 not converge. See #5287.
1671
1672 Note [Equality class instances]
1673 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1674 We can't have users writing instances for the equality classes. But we
1675 still need to be able to write instances for them ourselves. So we allow
1676 instances only in the defining module.
1677
1678 -}
1679
1680 validDerivPred :: TyVarSet -> PredType -> Bool
1681 -- See Note [Valid 'deriving' predicate]
1682 validDerivPred tv_set pred
1683 = case classifyPredType pred of
1684 ClassPred cls tys -> cls `hasKey` typeableClassKey
1685 -- Typeable constraints are bigger than they appear due
1686 -- to kind polymorphism, but that's OK
1687 || check_tys cls tys
1688 EqPred {} -> False -- reject equality constraints
1689 _ -> True -- Non-class predicates are ok
1690 where
1691 check_tys cls tys
1692 = hasNoDups fvs
1693 -- use sizePred to ignore implicit args
1694 && lengthIs fvs (sizePred pred)
1695 && all (`elemVarSet` tv_set) fvs
1696 where tys' = filterOutInvisibleTypes (classTyCon cls) tys
1697 fvs = fvTypes tys'
1698
1699 {-
1700 ************************************************************************
1701 * *
1702 \subsection{Checking instance for termination}
1703 * *
1704 ************************************************************************
1705 -}
1706
1707 {- Note [Instances and constraint synonyms]
1708 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1709 Currently, we don't allow instances for constraint synonyms at all.
1710 Consider these (#13267):
1711 type C1 a = Show (a -> Bool)
1712 instance C1 Int where -- I1
1713 show _ = "ur"
1714
1715 This elicits "show is not a (visible) method of class C1", which isn't
1716 a great message. But it comes from the renamer, so it's hard to improve.
1717
1718 This needs a bit more care:
1719 type C2 a = (Show a, Show Int)
1720 instance C2 Int -- I2
1721
1722 If we use (splitTyConApp_maybe tau) in checkValidInstance to decompose
1723 the instance head, we'll expand the synonym on fly, and it'll look like
1724 instance (%,%) (Show Int, Show Int)
1725 and we /really/ don't want that. So we carefully do /not/ expand
1726 synonyms, by matching on TyConApp directly.
1727 -}
1728
1729 checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type -> TcM ()
1730 checkValidInstance ctxt hs_type ty
1731 | not is_tc_app
1732 = failWithTc (TcRnNoClassInstHead tau)
1733
1734 | isNothing mb_cls
1735 = failWithTc (TcRnIllegalClassInst (tyConFlavour tc))
1736
1737 | otherwise
1738 = do { setSrcSpanA head_loc $
1739 checkValidInstHead ctxt clas inst_tys
1740
1741 ; traceTc "checkValidInstance {" (ppr ty)
1742
1743 ; env0 <- tcInitTidyEnv
1744 ; expand <- initialExpandMode
1745 ; check_valid_theta env0 ctxt expand theta
1746
1747 -- The Termination and Coverate Conditions
1748 -- Check that instance inference will terminate (if we care)
1749 -- For Haskell 98 this will already have been done by checkValidTheta,
1750 -- but as we may be using other extensions we need to check.
1751 --
1752 -- Note that the Termination Condition is *more conservative* than
1753 -- the checkAmbiguity test we do on other type signatures
1754 -- e.g. Bar a => Bar Int is ambiguous, but it also fails
1755 -- the termination condition, because 'a' appears more often
1756 -- in the constraint than in the head
1757 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
1758 ; if undecidable_ok
1759 then checkAmbiguity ctxt ty
1760 else checkInstTermination theta tau
1761
1762 ; traceTc "cvi 2" (ppr ty)
1763
1764 ; case (checkInstCoverage undecidable_ok clas theta inst_tys) of
1765 IsValid -> return () -- Check succeeded
1766 NotValid msg -> addErrTc (instTypeErr clas inst_tys msg)
1767
1768 ; traceTc "End checkValidInstance }" empty
1769
1770 ; return () }
1771 where
1772 (_tvs, theta, tau) = tcSplitSigmaTy ty
1773 is_tc_app = case tau of { TyConApp {} -> True; _ -> False }
1774 TyConApp tc inst_tys = tau -- See Note [Instances and constraint synonyms]
1775 mb_cls = tyConClass_maybe tc
1776 Just clas = mb_cls
1777
1778 -- The location of the "head" of the instance
1779 head_loc = getLoc (getLHsInstDeclHead hs_type)
1780
1781 {-
1782 Note [Paterson conditions]
1783 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1784 Termination test: the so-called "Paterson conditions" (see Section 5 of
1785 "Understanding functional dependencies via Constraint Handling Rules,
1786 JFP Jan 2007).
1787
1788 We check that each assertion in the context satisfies:
1789 (1) no variable has more occurrences in the assertion than in the head, and
1790 (2) the assertion has fewer constructors and variables (taken together
1791 and counting repetitions) than the head.
1792 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1793 (which have already been checked) guarantee termination.
1794
1795 The underlying idea is that
1796
1797 for any ground substitution, each assertion in the
1798 context has fewer type constructors than the head.
1799 -}
1800
1801 checkInstTermination :: ThetaType -> TcPredType -> TcM ()
1802 -- See Note [Paterson conditions]
1803 checkInstTermination theta head_pred
1804 = check_preds emptyVarSet theta
1805 where
1806 head_fvs = fvType head_pred
1807 head_size = sizeType head_pred
1808
1809 check_preds :: VarSet -> [PredType] -> TcM ()
1810 check_preds foralld_tvs preds = mapM_ (check foralld_tvs) preds
1811
1812 check :: VarSet -> PredType -> TcM ()
1813 check foralld_tvs pred
1814 = case classifyPredType pred of
1815 EqPred {} -> return () -- See #4200.
1816 SpecialPred {} -> return ()
1817 IrredPred {} -> check2 foralld_tvs pred (sizeType pred)
1818 ClassPred cls tys
1819 | isTerminatingClass cls
1820 -> return ()
1821
1822 | isCTupleClass cls -- Look inside tuple predicates; #8359
1823 -> check_preds foralld_tvs tys
1824
1825 | otherwise -- Other ClassPreds
1826 -> check2 foralld_tvs pred bogus_size
1827 where
1828 bogus_size = 1 + sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys)
1829 -- See Note [Invisible arguments and termination]
1830
1831 ForAllPred tvs _ head_pred'
1832 -> check (foralld_tvs `extendVarSetList` tvs) head_pred'
1833 -- Termination of the quantified predicate itself is checked
1834 -- when the predicates are individually checked for validity
1835
1836 check2 foralld_tvs pred pred_size
1837 | not (null bad_tvs) = failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
1838 (noMoreMsg bad_tvs what (ppr head_pred))
1839 | not (isTyFamFree pred) = failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
1840 (nestedMsg what)
1841 | pred_size >= head_size = failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
1842 (smallerMsg what (ppr head_pred))
1843 | otherwise = return ()
1844 -- isTyFamFree: see Note [Type families in instance contexts]
1845 where
1846 what = text "constraint" <+> quotes (ppr pred)
1847 bad_tvs = filterOut (`elemVarSet` foralld_tvs) (fvType pred)
1848 \\ head_fvs
1849
1850 smallerMsg :: SDoc -> SDoc -> SDoc
1851 smallerMsg what inst_head
1852 = vcat [ hang (text "The" <+> what)
1853 2 (sep [ text "is no smaller than"
1854 , text "the instance head" <+> quotes inst_head ])
1855 , parens undecidableMsg ]
1856
1857 noMoreMsg :: [TcTyVar] -> SDoc -> SDoc -> SDoc
1858 noMoreMsg tvs what inst_head
1859 = vcat [ hang (text "Variable" <> plural tvs1 <+> quotes (pprWithCommas ppr tvs1)
1860 <+> occurs <+> text "more often")
1861 2 (sep [ text "in the" <+> what
1862 , text "than in the instance head" <+> quotes inst_head ])
1863 , parens undecidableMsg ]
1864 where
1865 tvs1 = nub tvs
1866 occurs = if isSingleton tvs1 then text "occurs"
1867 else text "occur"
1868
1869 undecidableMsg :: SDoc
1870 undecidableMsg = text "Use UndecidableInstances to permit this"
1871
1872 {- Note [Type families in instance contexts]
1873 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1874 Are these OK?
1875 type family F a
1876 instance F a => C (Maybe [a]) where ...
1877 instance C (F a) => C [[[a]]] where ...
1878
1879 No: the type family in the instance head might blow up to an
1880 arbitrarily large type, depending on how 'a' is instantiated.
1881 So we require UndecidableInstances if we have a type family
1882 in the instance head. #15172.
1883
1884 Note [Invisible arguments and termination]
1885 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1886 When checking the ​Paterson conditions for termination an instance
1887 declaration, we check for the number of "constructors and variables"
1888 in the instance head and constraints. Question: Do we look at
1889
1890 * All the arguments, visible or invisible?
1891 * Just the visible arguments?
1892
1893 I think both will ensure termination, provided we are consistent.
1894 Currently we are /not/ consistent, which is really a bug. It's
1895 described in #15177, which contains a number of examples.
1896 The suspicious bits are the calls to filterOutInvisibleTypes.
1897 -}
1898
1899
1900 {-
1901 ************************************************************************
1902 * *
1903 Checking type instance well-formedness and termination
1904 * *
1905 ************************************************************************
1906 -}
1907
1908 checkValidCoAxiom :: CoAxiom Branched -> TcM ()
1909 checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
1910 = do { mapM_ (checkValidCoAxBranch fam_tc) branch_list
1911 ; foldlM_ check_branch_compat [] branch_list }
1912 where
1913 branch_list = fromBranches branches
1914 injectivity = tyConInjectivityInfo fam_tc
1915
1916 check_branch_compat :: [CoAxBranch] -- previous branches in reverse order
1917 -> CoAxBranch -- current branch
1918 -> TcM [CoAxBranch]-- current branch : previous branches
1919 -- Check for
1920 -- (a) this branch is dominated by previous ones
1921 -- (b) failure of injectivity
1922 check_branch_compat prev_branches cur_branch
1923 | cur_branch `isDominatedBy` prev_branches
1924 = do { let dia = TcRnUnknownMessage $
1925 mkPlainDiagnostic WarningWithoutFlag noHints (inaccessibleCoAxBranch fam_tc cur_branch)
1926 ; addDiagnosticAt (coAxBranchSpan cur_branch) dia
1927 ; return prev_branches }
1928 | otherwise
1929 = do { check_injectivity prev_branches cur_branch
1930 ; return (cur_branch : prev_branches) }
1931
1932 -- Injectivity check: check whether a new (CoAxBranch) can extend
1933 -- already checked equations without violating injectivity
1934 -- annotation supplied by the user.
1935 -- See Note [Verifying injectivity annotation] in GHC.Core.FamInstEnv
1936 check_injectivity prev_branches cur_branch
1937 | Injective inj <- injectivity
1938 = do { dflags <- getDynFlags
1939 ; let conflicts =
1940 fst $ foldl' (gather_conflicts inj prev_branches cur_branch)
1941 ([], 0) prev_branches
1942 ; reportConflictingInjectivityErrs fam_tc conflicts cur_branch
1943 ; reportInjectivityErrors dflags ax cur_branch inj }
1944 | otherwise
1945 = return ()
1946
1947 gather_conflicts inj prev_branches cur_branch (acc, n) branch
1948 -- n is 0-based index of branch in prev_branches
1949 = case injectiveBranches inj cur_branch branch of
1950 -- Case 1B2 in Note [Verifying injectivity annotation] in GHC.Core.FamInstEnv
1951 InjectivityUnified ax1 ax2
1952 | ax1 `isDominatedBy` (replace_br prev_branches n ax2)
1953 -> (acc, n + 1)
1954 | otherwise
1955 -> (branch : acc, n + 1)
1956 InjectivityAccepted -> (acc, n + 1)
1957
1958 -- Replace n-th element in the list. Assumes 0-based indexing.
1959 replace_br :: [CoAxBranch] -> Int -> CoAxBranch -> [CoAxBranch]
1960 replace_br brs n br = take n brs ++ [br] ++ drop (n+1) brs
1961
1962
1963 -- Check that a "type instance" is well-formed (which includes decidability
1964 -- unless -XUndecidableInstances is given).
1965 --
1966 checkValidCoAxBranch :: TyCon -> CoAxBranch -> TcM ()
1967 checkValidCoAxBranch fam_tc
1968 (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
1969 , cab_lhs = typats
1970 , cab_rhs = rhs, cab_loc = loc })
1971 = setSrcSpan loc $
1972 checkValidTyFamEqn fam_tc (tvs++cvs) typats rhs
1973
1974 -- | Do validity checks on a type family equation, including consistency
1975 -- with any enclosing class instance head, termination, and lack of
1976 -- polytypes.
1977 checkValidTyFamEqn :: TyCon -- ^ of the type family
1978 -> [Var] -- ^ Bound variables in the equation
1979 -> [Type] -- ^ Type patterns
1980 -> Type -- ^ Rhs
1981 -> TcM ()
1982 checkValidTyFamEqn fam_tc qvs typats rhs
1983 = do { checkValidTypePats fam_tc typats
1984
1985 -- Check for things used on the right but not bound on the left
1986 ; checkFamPatBinders fam_tc qvs typats rhs
1987
1988 -- Check for oversaturated visible kind arguments in a type family
1989 -- equation.
1990 -- See Note [Oversaturated type family equations]
1991 ; when (isTypeFamilyTyCon fam_tc) $
1992 case drop (tyConArity fam_tc) typats of
1993 [] -> pure ()
1994 spec_arg:_ ->
1995 addErr (TcRnOversaturatedVisibleKindArg spec_arg)
1996
1997 -- The argument patterns, and RHS, are all boxed tau types
1998 -- E.g Reject type family F (a :: k1) :: k2
1999 -- type instance F (forall a. a->a) = ...
2000 -- type instance F Int# = ...
2001 -- type instance F Int = forall a. a->a
2002 -- type instance F Int = Int#
2003 -- See #9357
2004 ; checkValidMonoType rhs
2005
2006 -- We have a decidable instance unless otherwise permitted
2007 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
2008 ; traceTc "checkVTFE" (ppr fam_tc $$ ppr rhs $$ ppr (tcTyFamInsts rhs))
2009 ; unless undecidable_ok $
2010 mapM_ addErrTc (checkFamInstRhs fam_tc typats (tcTyFamInsts rhs)) }
2011
2012 -- | Checks that an associated type family default:
2013 --
2014 -- 1. Only consists of arguments that are bare type variables, and
2015 --
2016 -- 2. Has a distinct type variable in each argument.
2017 --
2018 -- See @Note [Type-checking default assoc decls]@ in "GHC.Tc.TyCl".
2019 checkValidAssocTyFamDeflt :: TyCon -- ^ of the type family
2020 -> [Type] -- ^ Type patterns
2021 -> TcM ()
2022 checkValidAssocTyFamDeflt fam_tc pats =
2023 do { cpt_tvs <- zipWithM extract_tv pats pats_vis
2024 ; check_all_distinct_tvs $ zip cpt_tvs pats_vis }
2025 where
2026 pats_vis :: [ArgFlag]
2027 pats_vis = tyConArgFlags fam_tc pats
2028
2029 -- Checks that a pattern on the LHS of a default is a type
2030 -- variable. If so, return the underlying type variable, and if
2031 -- not, throw an error.
2032 -- See Note [Type-checking default assoc decls]
2033 extract_tv :: Type -- The particular type pattern from which to extract
2034 -- its underlying type variable
2035 -> ArgFlag -- The visibility of the type pattern
2036 -- (only used for error message purposes)
2037 -> TcM TyVar
2038 extract_tv pat pat_vis =
2039 case getTyVar_maybe pat of
2040 Just tv -> pure tv
2041 Nothing -> failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
2042 pprWithExplicitKindsWhen (isInvisibleArgFlag pat_vis) $
2043 hang (text "Illegal argument" <+> quotes (ppr pat) <+> text "in:")
2044 2 (vcat [ppr_eqn, suggestion])
2045
2046 -- Checks that no type variables in an associated default declaration are
2047 -- duplicated. If that is the case, throw an error.
2048 -- See Note [Type-checking default assoc decls]
2049 check_all_distinct_tvs ::
2050 [(TyVar, ArgFlag)] -- The type variable arguments in the associated
2051 -- default declaration, along with their respective
2052 -- visibilities (the latter are only used for error
2053 -- message purposes)
2054 -> TcM ()
2055 check_all_distinct_tvs cpt_tvs_vis =
2056 let dups = findDupsEq ((==) `on` fst) cpt_tvs_vis in
2057 traverse_
2058 (\d -> let (pat_tv, pat_vis) = NE.head d in failWithTc $
2059 TcRnUnknownMessage $ mkPlainError noHints $
2060 pprWithExplicitKindsWhen (isInvisibleArgFlag pat_vis) $
2061 hang (text "Illegal duplicate variable"
2062 <+> quotes (ppr pat_tv) <+> text "in:")
2063 2 (vcat [ppr_eqn, suggestion]))
2064 dups
2065
2066 ppr_eqn :: SDoc
2067 ppr_eqn =
2068 quotes (text "type" <+> ppr (mkTyConApp fam_tc pats)
2069 <+> equals <+> text "...")
2070
2071 suggestion :: SDoc
2072 suggestion = text "The arguments to" <+> quotes (ppr fam_tc)
2073 <+> text "must all be distinct type variables"
2074
2075 -- Make sure that each type family application is
2076 -- (1) strictly smaller than the lhs,
2077 -- (2) mentions no type variable more often than the lhs, and
2078 -- (3) does not contain any further type family instances.
2079 --
2080 checkFamInstRhs :: TyCon -> [Type] -- LHS
2081 -> [(TyCon, [Type])] -- type family calls in RHS
2082 -> [TcRnMessage]
2083 checkFamInstRhs lhs_tc lhs_tys famInsts
2084 = map (TcRnUnknownMessage . mkPlainError noHints) $ mapMaybe check famInsts
2085 where
2086 lhs_size = sizeTyConAppArgs lhs_tc lhs_tys
2087 inst_head = pprType (TyConApp lhs_tc lhs_tys)
2088 lhs_fvs = fvTypes lhs_tys
2089 check (tc, tys)
2090 | not (all isTyFamFree tys) = Just (nestedMsg what)
2091 | not (null bad_tvs) = Just (noMoreMsg bad_tvs what inst_head)
2092 | lhs_size <= fam_app_size = Just (smallerMsg what inst_head)
2093 | otherwise = Nothing
2094 where
2095 what = text "type family application"
2096 <+> quotes (pprType (TyConApp tc tys))
2097 fam_app_size = sizeTyConAppArgs tc tys
2098 bad_tvs = fvTypes tys \\ lhs_fvs
2099 -- The (\\) is list difference; e.g.
2100 -- [a,b,a,a] \\ [a,a] = [b,a]
2101 -- So we are counting repetitions
2102
2103 -----------------
2104 checkFamPatBinders :: TyCon
2105 -> [TcTyVar] -- Bound on LHS of family instance
2106 -> [TcType] -- LHS patterns
2107 -> Type -- RHS
2108 -> TcM ()
2109 checkFamPatBinders fam_tc qtvs pats rhs
2110 = do { traceTc "checkFamPatBinders" $
2111 vcat [ debugPprType (mkTyConApp fam_tc pats)
2112 , ppr (mkTyConApp fam_tc pats)
2113 , text "qtvs:" <+> ppr qtvs
2114 , text "rhs_tvs:" <+> ppr (fvVarSet rhs_fvs)
2115 , text "cpt_tvs:" <+> ppr cpt_tvs
2116 , text "inj_cpt_tvs:" <+> ppr inj_cpt_tvs ]
2117
2118 -- Check for implicitly-bound tyvars, mentioned on the
2119 -- RHS but not bound on the LHS
2120 -- data T = MkT (forall (a::k). blah)
2121 -- data family D Int = MkD (forall (a::k). blah)
2122 -- In both cases, 'k' is not bound on the LHS, but is used on the RHS
2123 -- We catch the former in kcDeclHeader, and the latter right here
2124 -- See Note [Check type-family instance binders]
2125 ; check_tvs bad_rhs_tvs (text "mentioned in the RHS")
2126 (text "bound on the LHS of")
2127
2128 -- Check for explicitly forall'd variable that is not bound on LHS
2129 -- data instance forall a. T Int = MkT Int
2130 -- See Note [Unused explicitly bound variables in a family pattern]
2131 -- See Note [Check type-family instance binders]
2132 ; check_tvs bad_qtvs (text "bound by a forall")
2133 (text "used in")
2134 }
2135 where
2136 cpt_tvs = tyCoVarsOfTypes pats
2137 inj_cpt_tvs = fvVarSet $ injectiveVarsOfTypes False pats
2138 -- The type variables that are in injective positions.
2139 -- See Note [Dodgy binding sites in type family instances]
2140 -- NB: The False above is irrelevant, as we never have type families in
2141 -- patterns.
2142 --
2143 -- NB: It's OK to use the nondeterministic `fvVarSet` function here,
2144 -- since the order of `inj_cpt_tvs` is never revealed in an error
2145 -- message.
2146 rhs_fvs = tyCoFVsOfType rhs
2147 used_tvs = cpt_tvs `unionVarSet` fvVarSet rhs_fvs
2148 bad_qtvs = filterOut (`elemVarSet` used_tvs) qtvs
2149 -- Bound but not used at all
2150 bad_rhs_tvs = filterOut (`elemVarSet` inj_cpt_tvs) (fvVarList rhs_fvs)
2151 -- Used on RHS but not bound on LHS
2152 dodgy_tvs = cpt_tvs `minusVarSet` inj_cpt_tvs
2153
2154 check_tvs tvs what what2
2155 = unless (null tvs) $ addErrAt (getSrcSpan (head tvs)) $ TcRnUnknownMessage $ mkPlainError noHints $
2156 hang (text "Type variable" <> plural tvs <+> pprQuotedList tvs
2157 <+> isOrAre tvs <+> what <> comma)
2158 2 (vcat [ text "but not" <+> what2 <+> text "the family instance"
2159 , mk_extra tvs ])
2160
2161 -- mk_extra: #7536: give a decent error message for
2162 -- type T a = Int
2163 -- type instance F (T a) = a
2164 mk_extra tvs = ppWhen (any (`elemVarSet` dodgy_tvs) tvs) $
2165 hang (text "The real LHS (expanding synonyms) is:")
2166 2 (pprTypeApp fam_tc (map expandTypeSynonyms pats))
2167
2168
2169 -- | Checks that a list of type patterns is valid in a matching (LHS)
2170 -- position of a class instances or type/data family instance.
2171 --
2172 -- Specifically:
2173 -- * All monotypes
2174 -- * No type-family applications
2175 checkValidTypePats :: TyCon -> [Type] -> TcM ()
2176 checkValidTypePats tc pat_ty_args
2177 = do { -- Check that each of pat_ty_args is a monotype.
2178 -- One could imagine generalising to allow
2179 -- instance C (forall a. a->a)
2180 -- but we don't know what all the consequences might be.
2181 traverse_ checkValidMonoType pat_ty_args
2182
2183 -- Ensure that no type family applications occur a type pattern
2184 ; case tcTyConAppTyFamInstsAndVis tc pat_ty_args of
2185 [] -> pure ()
2186 ((tf_is_invis_arg, tf_tc, tf_args):_) -> failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
2187 ty_fam_inst_illegal_err tf_is_invis_arg
2188 (mkTyConApp tf_tc tf_args) }
2189 where
2190 inst_ty = mkTyConApp tc pat_ty_args
2191
2192 ty_fam_inst_illegal_err :: Bool -> Type -> SDoc
2193 ty_fam_inst_illegal_err invis_arg ty
2194 = pprWithExplicitKindsWhen invis_arg $
2195 hang (text "Illegal type synonym family application"
2196 <+> quotes (ppr ty) <+> text "in instance" <> colon)
2197 2 (ppr inst_ty)
2198
2199 -- Error messages
2200
2201 inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc
2202 inaccessibleCoAxBranch fam_tc cur_branch
2203 = text "Type family instance equation is overlapped:" $$
2204 nest 2 (pprCoAxBranchUser fam_tc cur_branch)
2205
2206 nestedMsg :: SDoc -> SDoc
2207 nestedMsg what
2208 = sep [ text "Illegal nested" <+> what
2209 , parens undecidableMsg ]
2210
2211 -------------------------
2212 checkConsistentFamInst :: AssocInstInfo
2213 -> TyCon -- ^ Family tycon
2214 -> CoAxBranch
2215 -> TcM ()
2216 -- See Note [Checking consistent instantiation]
2217
2218 checkConsistentFamInst NotAssociated _ _
2219 = return ()
2220
2221 checkConsistentFamInst (InClsInst { ai_class = clas
2222 , ai_tyvars = inst_tvs
2223 , ai_inst_env = mini_env })
2224 fam_tc branch
2225 = do { traceTc "checkConsistentFamInst" (vcat [ ppr inst_tvs
2226 , ppr arg_triples
2227 , ppr mini_env
2228 , ppr ax_tvs
2229 , ppr ax_arg_tys
2230 , ppr arg_triples ])
2231 -- Check that the associated type indeed comes from this class
2232 -- See [Mismatched class methods and associated type families]
2233 -- in TcInstDecls.
2234 ; checkTc (Just (classTyCon clas) == tyConAssoc_maybe fam_tc)
2235 (TcRnBadAssociatedType (className clas) (tyConName fam_tc))
2236
2237 ; check_match arg_triples
2238 }
2239 where
2240 (ax_tvs, ax_arg_tys, _) = etaExpandCoAxBranch branch
2241
2242 arg_triples :: [(Type,Type, ArgFlag)]
2243 arg_triples = [ (cls_arg_ty, at_arg_ty, vis)
2244 | (fam_tc_tv, vis, at_arg_ty)
2245 <- zip3 (tyConTyVars fam_tc)
2246 (tyConArgFlags fam_tc ax_arg_tys)
2247 ax_arg_tys
2248 , Just cls_arg_ty <- [lookupVarEnv mini_env fam_tc_tv] ]
2249
2250 pp_wrong_at_arg vis
2251 = pprWithExplicitKindsWhen (isInvisibleArgFlag vis) $
2252 vcat [ text "Type indexes must match class instance head"
2253 , text "Expected:" <+> pp_expected_ty
2254 , text " Actual:" <+> pp_actual_ty ]
2255
2256 -- Fiddling around to arrange that wildcards unconditionally print as "_"
2257 -- We only need to print the LHS, not the RHS at all
2258 -- See Note [Printing conflicts with class header]
2259 (tidy_env1, _) = tidyVarBndrs emptyTidyEnv inst_tvs
2260 (tidy_env2, _) = tidyCoAxBndrsForUser tidy_env1 (ax_tvs \\ inst_tvs)
2261
2262 pp_expected_ty = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc) $
2263 toIfaceTcArgs fam_tc $
2264 [ case lookupVarEnv mini_env at_tv of
2265 Just cls_arg_ty -> tidyType tidy_env2 cls_arg_ty
2266 Nothing -> mk_wildcard at_tv
2267 | at_tv <- tyConTyVars fam_tc ]
2268
2269 pp_actual_ty = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc) $
2270 toIfaceTcArgs fam_tc $
2271 tidyTypes tidy_env2 ax_arg_tys
2272
2273 mk_wildcard at_tv = mkTyVarTy (mkTyVar tv_name (tyVarKind at_tv))
2274 tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "_") noSrcSpan
2275
2276 -- For check_match, bind_me, see
2277 -- Note [Matching in the consistent-instantiation check]
2278 check_match :: [(Type,Type,ArgFlag)] -> TcM ()
2279 check_match triples = go emptyTCvSubst emptyTCvSubst triples
2280
2281 go _ _ [] = return ()
2282 go lr_subst rl_subst ((ty1,ty2,vis):triples)
2283 | Just lr_subst1 <- tcMatchTyX_BM bind_me lr_subst ty1 ty2
2284 , Just rl_subst1 <- tcMatchTyX_BM bind_me rl_subst ty2 ty1
2285 = go lr_subst1 rl_subst1 triples
2286 | otherwise
2287 = addErrTc (TcRnUnknownMessage $ mkPlainError noHints $ pp_wrong_at_arg vis)
2288
2289 -- The /scoped/ type variables from the class-instance header
2290 -- should not be alpha-renamed. Inferred ones can be.
2291 no_bind_set = mkVarSet inst_tvs
2292 bind_me tv _ty | tv `elemVarSet` no_bind_set = Apart
2293 | otherwise = BindMe
2294
2295
2296 {- Note [Check type-family instance binders]
2297 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2298 In a type family instance, we require (of course), type variables
2299 used on the RHS are matched on the LHS. This is checked by
2300 checkFamPatBinders. Here is an interesting example:
2301
2302 type family T :: k
2303 type instance T = (Nothing :: Maybe a)
2304
2305 Upon a cursory glance, it may appear that the kind variable `a` is unbound
2306 since there are no (visible) LHS patterns in `T`. However, there is an
2307 *invisible* pattern due to the return kind, so inside of GHC, the instance
2308 looks closer to this:
2309
2310 type family T @k :: k
2311 type instance T @(Maybe a) = (Nothing :: Maybe a)
2312
2313 Here, we can see that `a` really is bound by a LHS type pattern, so `a` is in
2314 fact not unbound. Contrast that with this example (#13985)
2315
2316 type instance T = Proxy (Nothing :: Maybe a)
2317
2318 This would looks like this inside of GHC:
2319
2320 type instance T @(*) = Proxy (Nothing :: Maybe a)
2321
2322 So this time, `a` is neither bound by a visible nor invisible type pattern on
2323 the LHS, so `a` would be reported as not in scope.
2324
2325 Finally, here's one more brain-teaser (from #9574). In the example below:
2326
2327 class Funct f where
2328 type Codomain f :: *
2329 instance Funct ('KProxy :: KProxy o) where
2330 type Codomain 'KProxy = NatTr (Proxy :: o -> *)
2331
2332 As it turns out, `o` is in scope in this example. That is because `o` is
2333 bound by the kind signature of the LHS type pattern 'KProxy. To make this more
2334 obvious, one can also write the instance like so:
2335
2336 instance Funct ('KProxy :: KProxy o) where
2337 type Codomain ('KProxy :: KProxy o) = NatTr (Proxy :: o -> *)
2338
2339 Note [Dodgy binding sites in type family instances]
2340 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2341 Consider the following example (from #7536):
2342
2343 type T a = Int
2344 type instance F (T a) = a
2345
2346 This `F` instance is extremely fishy, since the RHS, `a`, purports to be
2347 "bound" by the LHS pattern `T a`. "Bound" has scare quotes around it because
2348 `T a` expands to `Int`, which doesn't mention at all, so it's as if one had
2349 actually written:
2350
2351 type instance F Int = a
2352
2353 That is clearly bogus, so to reject this, we check that every type variable
2354 that is mentioned on the RHS is /actually/ bound on the LHS. In other words,
2355 we need to do something slightly more sophisticated that just compute the free
2356 variables of the LHS patterns.
2357
2358 It's tempting to just expand all type synonyms on the LHS and then compute
2359 their free variables, but even that isn't sophisticated enough. After all,
2360 an impish user could write the following (#17008):
2361
2362 type family ConstType (a :: Type) :: Type where
2363 ConstType _ = Type
2364
2365 type family F (x :: ConstType a) :: Type where
2366 F (x :: ConstType a) = a
2367
2368 Just like in the previous example, the `a` on the RHS isn't actually bound
2369 on the LHS, but this time a type family is responsible for the deception, not
2370 a type synonym.
2371
2372 We avoid both issues by requiring that all RHS type variables are mentioned
2373 in injective positions on the left-hand side (by way of
2374 `injectiveVarsOfTypes`). For instance, the `a` in `T a` is not in an injective
2375 position, as `T` is not an injective type constructor, so we do not count that.
2376 Similarly for the `a` in `ConstType a`.
2377
2378 Note [Matching in the consistent-instantiation check]
2379 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2380 Matching the class-instance header to family-instance tyvars is
2381 tricker than it sounds. Consider (#13972)
2382 class C (a :: k) where
2383 type T k :: Type
2384 instance C Left where
2385 type T (a -> Either a b) = Int
2386
2387 Here there are no lexically-scoped variables from (C Left).
2388 Yet the real class-instance header is C @(p -> Either @p @q)) (Left @p @q)
2389 while the type-family instance is T (a -> Either @a @b)
2390 So we allow alpha-renaming of variables that don't come
2391 from the class-instance header.
2392
2393 We track the lexically-scoped type variables from the
2394 class-instance header in ai_tyvars.
2395
2396 Here's another example (#14045a)
2397 class C (a :: k) where
2398 data S (a :: k)
2399 instance C (z :: Bool) where
2400 data S :: Bool -> Type where
2401
2402 Again, there is no lexical connection, but we will get
2403 class-instance header: C @Bool (z::Bool)
2404 family instance S @Bool (a::Bool)
2405
2406 When looking for mis-matches, we check left-to-right,
2407 kinds first. If we look at types first, we'll fail to
2408 suggest -fprint-explicit-kinds for a mis-match with
2409 T @k vs T @Type
2410 somewhere deep inside the type
2411
2412 Note [Checking consistent instantiation]
2413 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2414 See #11450 for background discussion on this check.
2415
2416 class C a b where
2417 type T a x b
2418
2419 With this class decl, if we have an instance decl
2420 instance C ty1 ty2 where ...
2421 then the type instance must look like
2422 type T ty1 v ty2 = ...
2423 with exactly 'ty1' for 'a', 'ty2' for 'b', and some type 'v' for 'x'.
2424 For example:
2425
2426 instance C [p] Int
2427 type T [p] y Int = (p,y,y)
2428
2429 Note that
2430
2431 * We used to allow completely different bound variables in the
2432 associated type instance; e.g.
2433 instance C [p] Int
2434 type T [q] y Int = ...
2435 But from GHC 8.2 onwards, we don't. It's much simpler this way.
2436 See #11450.
2437
2438 * When the class variable isn't used on the RHS of the type instance,
2439 it's tempting to allow wildcards, thus
2440 instance C [p] Int
2441 type T [_] y Int = (y,y)
2442 But it's awkward to do the test, and it doesn't work if the
2443 variable is repeated:
2444 instance C (p,p) Int
2445 type T (_,_) y Int = (y,y)
2446 Even though 'p' is not used on the RHS, we still need to use 'p'
2447 on the LHS to establish the repeated pattern. So to keep it simple
2448 we just require equality.
2449
2450 * For variables in associated type families that are not bound by the class
2451 itself, we do _not_ check if they are over-specific. In other words,
2452 it's perfectly acceptable to have an instance like this:
2453
2454 instance C [p] Int where
2455 type T [p] (Maybe x) Int = x
2456
2457 While the first and third arguments to T are required to be exactly [p] and
2458 Int, respectively, since they are bound by C, the second argument is allowed
2459 to be more specific than just a type variable. Furthermore, it is permissible
2460 to define multiple equations for T that differ only in the non-class-bound
2461 argument:
2462
2463 instance C [p] Int where
2464 type T [p] (Maybe x) Int = x
2465 type T [p] (Either x y) Int = x -> y
2466
2467 We once considered requiring that non-class-bound variables in associated
2468 type family instances be instantiated with distinct type variables. However,
2469 that requirement proved too restrictive in practice, as there were examples
2470 of extremely simple associated type family instances that this check would
2471 reject, and fixing them required tiresome boilerplate in the form of
2472 auxiliary type families. For instance, you would have to define the above
2473 example as:
2474
2475 instance C [p] Int where
2476 type T [p] x Int = CAux x
2477
2478 type family CAux x where
2479 CAux (Maybe x) = x
2480 CAux (Either x y) = x -> y
2481
2482 We decided that this restriction wasn't buying us much, so we opted not
2483 to pursue that design (see also GHC #13398).
2484
2485 Implementation
2486 * Form the mini-envt from the class type variables a,b
2487 to the instance decl types [p],Int: [a->[p], b->Int]
2488
2489 * Look at the tyvars a,x,b of the type family constructor T
2490 (it shares tyvars with the class C)
2491
2492 * Apply the mini-evnt to them, and check that the result is
2493 consistent with the instance types [p] y Int. (where y can be any type, as
2494 it is not scoped over the class type variables.
2495
2496 We make all the instance type variables scope over the
2497 type instances, of course, which picks up non-obvious kinds. Eg
2498 class Foo (a :: k) where
2499 type F a
2500 instance Foo (b :: k -> k) where
2501 type F b = Int
2502 Here the instance is kind-indexed and really looks like
2503 type F (k->k) (b::k->k) = Int
2504 But if the 'b' didn't scope, we would make F's instance too
2505 poly-kinded.
2506
2507 Note [Printing conflicts with class header]
2508 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2509 It's remarkably painful to give a decent error message for conflicts
2510 with the class header. Consider
2511 clase C b where
2512 type F a b c
2513 instance C [b] where
2514 type F x Int _ _ = ...
2515
2516 Here we want to report a conflict between
2517 Expected: F _ [b] _
2518 Actual: F x Int _ _
2519
2520 But if the type instance shadows the class variable like this
2521 (rename/should_fail/T15828):
2522 instance C [b] where
2523 type forall b. F x (Tree b) _ _ = ...
2524
2525 then we must use a fresh variable name
2526 Expected: F _ [b] _
2527 Actual: F x [b1] _ _
2528
2529 Notice that:
2530 - We want to print an underscore in the "Expected" type in
2531 positions where the class header has no influence over the
2532 parameter. Hence the fancy footwork in pp_expected_ty
2533
2534 - Although the binders in the axiom are already tidy, we must
2535 re-tidy them to get a fresh variable name when we shadow
2536
2537 - The (ax_tvs \\ inst_tvs) is to avoid tidying one of the
2538 class-instance variables a second time, from 'a' to 'a1' say.
2539 Remember, the ax_tvs of the axiom share identity with the
2540 class-instance variables, inst_tvs..
2541
2542 - We use tidyCoAxBndrsForUser to get underscores rather than
2543 _1, _2, etc in the axiom tyvars; see the definition of
2544 tidyCoAxBndrsForUser
2545
2546 This all seems absurdly complicated.
2547
2548 Note [Unused explicitly bound variables in a family pattern]
2549 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2550
2551 Why is 'unusedExplicitForAllErr' not just a warning?
2552
2553 Consider the following examples:
2554
2555 type instance F a = Maybe b
2556 type instance forall b. F a = Bool
2557 type instance forall b. F a = Maybe b
2558
2559 In every case, b is a type variable not determined by the LHS pattern. The
2560 first is caught by the renamer, but we catch the last two here. Perhaps one
2561 could argue that the second should be accepted, albeit with a warning, but
2562 consider the fact that in a type family instance, there is no way to interact
2563 with such a varable. At least with @x :: forall a. Int@ we can use visibile
2564 type application, like @x \@Bool 1@. (Of course it does nothing, but it is
2565 permissible.) In the type family case, the only sensible explanation is that
2566 the user has made a mistake -- thus we throw an error.
2567
2568 Note [Oversaturated type family equations]
2569 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2570 Type family tycons have very rigid arities. We want to reject something like
2571 this:
2572
2573 type family Foo :: Type -> Type where
2574 Foo x = ...
2575
2576 Because Foo has arity zero (i.e., it doesn't bind anything to the left of the
2577 double colon), we want to disallow any equation for Foo that has more than zero
2578 arguments, such as `Foo x = ...`. The algorithm here is pretty simple: if an
2579 equation has more arguments than the arity of the type family, reject.
2580
2581 Things get trickier when visible kind application enters the picture. Consider
2582 the following example:
2583
2584 type family Bar (x :: j) :: forall k. Either j k where
2585 Bar 5 @Symbol = ...
2586
2587 The arity of Bar is two, since it binds two variables, `j` and `x`. But even
2588 though Bar's equation has two arguments, it's still invalid. Imagine the same
2589 equation in Core:
2590
2591 Bar Nat 5 Symbol = ...
2592
2593 Here, it becomes apparent that Bar is actually taking /three/ arguments! So
2594 we can't just rely on a simple counting argument to reject
2595 `Bar 5 @Symbol = ...`, since it only has two user-written arguments.
2596 Moreover, there's one explicit argument (5) and one visible kind argument
2597 (@Symbol), which matches up perfectly with the fact that Bar has one required
2598 binder (x) and one specified binder (j), so that's not a valid way to detect
2599 oversaturation either.
2600
2601 To solve this problem in a robust way, we do the following:
2602
2603 1. When kind-checking, we count the number of user-written *required*
2604 arguments and check if there is an equal number of required tycon binders.
2605 If not, reject. (See `wrongNumberOfParmsErr` in GHC.Tc.TyCl.)
2606
2607 We perform this step during kind-checking, not during validity checking,
2608 since we can give better error messages if we catch it early.
2609 2. When validity checking, take all of the (Core) type patterns from on
2610 equation, drop the first n of them (where n is the arity of the type family
2611 tycon), and check if there are any types leftover. If so, reject.
2612
2613 Why does this work? We know that after dropping the first n type patterns,
2614 none of the leftover types can be required arguments, since step (1) would
2615 have already caught that. Moreover, the only places where visible kind
2616 applications should be allowed are in the first n types, since those are the
2617 only arguments that can correspond to binding forms. Therefore, the
2618 remaining arguments must correspond to oversaturated uses of visible kind
2619 applications, which are precisely what we want to reject.
2620
2621 Note that we only perform this check for type families, and not for data
2622 families. This is because it is perfectly acceptable to oversaturate data
2623 family instance equations: see Note [Arity of data families] in GHC.Core.FamInstEnv.
2624
2625 ************************************************************************
2626 * *
2627 Telescope checking
2628 * *
2629 ************************************************************************
2630
2631 Note [Bad TyCon telescopes]
2632 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
2633 Now that we can mix type and kind variables, there are an awful lot of
2634 ways to shoot yourself in the foot. Here are some.
2635
2636 data SameKind :: k -> k -> * -- just to force unification
2637
2638 1. data T1 a k (b :: k) (x :: SameKind a b)
2639
2640 The problem here is that we discover that a and b should have the same
2641 kind. But this kind mentions k, which is bound *after* a.
2642 (Testcase: dependent/should_fail/BadTelescope)
2643
2644 2. data T2 a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
2645
2646 Note that b is not bound. Yet its kind mentions a. Because we have
2647 a nice rule that all implicitly bound variables come before others,
2648 this is bogus.
2649
2650 To catch these errors, we call checkTyConTelescope during kind-checking
2651 datatype declarations. This checks for
2652
2653 * Ill-scoped binders. From (1) and (2) above we can get putative
2654 kinds like
2655 T1 :: forall (a:k) (k:*) (b:k). SameKind a b -> *
2656 where 'k' is mentioned a's kind before k is bound
2657
2658 This is easy to check for: just look for
2659 out-of-scope variables in the kind
2660
2661 * We should arguably also check for ambiguous binders
2662 but we don't. See Note [Ambiguous kind vars].
2663
2664 See also
2665 * Note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl.
2666 * Note [Checking telescopes] in GHC.Tc.Types.Constraint discusses how
2667 this check works for `forall x y z.` written in a type.
2668
2669 Note [Ambiguous kind vars]
2670 ~~~~~~~~~~~~~~~~~~~~~~~~~~
2671 We used to be concerned about ambiguous binders. Suppose we have the kind
2672 S1 :: forall k -> * -> *
2673 S2 :: forall k. * -> *
2674 Here S1 is OK, because k is Required, and at a use of S1 we will
2675 see (S1 *) or (S1 (*->*)) or whatever.
2676
2677 But S2 is /not/ OK because 'k' is Specfied (and hence invisible) and
2678 we have no way (ever) to figure out how 'k' should be instantiated.
2679 For example if we see (S2 Int), that tells us nothing about k's
2680 instantiation. (In this case we'll instantiate it to Any, but that
2681 seems wrong.) This is really the same test as we make for ambiguous
2682 type in term type signatures.
2683
2684 Now, it's impossible for a Specified variable not to occur
2685 at all in the kind -- after all, it is Specified so it must have
2686 occurred. (It /used/ to be possible; see tests T13983 and T7873. But
2687 with the advent of the forall-or-nothing rule for kind variables,
2688 those strange cases went away. See Note [forall-or-nothing rule] in
2689 GHC.Hs.Type.)
2690
2691 But one might worry about
2692 type v k = *
2693 S3 :: forall k. V k -> *
2694 which appears to mention 'k' but doesn't really. Or
2695 S4 :: forall k. F k -> *
2696 where F is a type function. But we simply don't check for
2697 those cases of ambiguity, yet anyway. The worst that can happen
2698 is ambiguity at the call sites.
2699
2700 Historical note: this test used to be called reportFloatingKvs.
2701 -}
2702
2703 -- | Check a list of binders to see if they make a valid telescope.
2704 -- See Note [Bad TyCon telescopes]
2705 type TelescopeAcc
2706 = ( TyVarSet -- Bound earlier in the telescope
2707 , Bool -- At least one binder occurred (in a kind) before
2708 -- it was bound in the telescope. E.g.
2709 ) -- T :: forall (a::k) k. blah
2710
2711 checkTyConTelescope :: TyCon -> TcM ()
2712 checkTyConTelescope tc
2713 | bad_scope
2714 = -- See "Ill-scoped binders" in Note [Bad TyCon telescopes]
2715 addErr $ TcRnUnknownMessage $ mkPlainError noHints $
2716 vcat [ hang (text "The kind of" <+> quotes (ppr tc) <+> text "is ill-scoped")
2717 2 pp_tc_kind
2718 , extra
2719 , hang (text "Perhaps try this order instead:")
2720 2 (pprTyVars sorted_tvs) ]
2721
2722 | otherwise
2723 = return ()
2724 where
2725 tcbs = tyConBinders tc
2726 tvs = binderVars tcbs
2727 sorted_tvs = scopedSort tvs
2728
2729 (_, bad_scope) = foldl add_one (emptyVarSet, False) tcbs
2730
2731 add_one :: TelescopeAcc -> TyConBinder -> TelescopeAcc
2732 add_one (bound, bad_scope) tcb
2733 = ( bound `extendVarSet` tv
2734 , bad_scope || not (isEmptyVarSet (fkvs `minusVarSet` bound)) )
2735 where
2736 tv = binderVar tcb
2737 fkvs = tyCoVarsOfType (tyVarKind tv)
2738
2739 inferred_tvs = [ binderVar tcb
2740 | tcb <- tcbs, Inferred == tyConBinderArgFlag tcb ]
2741 specified_tvs = [ binderVar tcb
2742 | tcb <- tcbs, Specified == tyConBinderArgFlag tcb ]
2743
2744 pp_inf = parens (text "namely:" <+> pprTyVars inferred_tvs)
2745 pp_spec = parens (text "namely:" <+> pprTyVars specified_tvs)
2746
2747 pp_tc_kind = text "Inferred kind:" <+> ppr tc <+> dcolon <+> ppr_untidy (tyConKind tc)
2748 ppr_untidy ty = pprIfaceType (toIfaceType ty)
2749 -- We need ppr_untidy here because pprType will tidy the type, which
2750 -- will turn the bogus kind we are trying to report
2751 -- T :: forall (a::k) k (b::k) -> blah
2752 -- into a misleadingly sanitised version
2753 -- T :: forall (a::k) k1 (b::k1) -> blah
2754
2755 extra
2756 | null inferred_tvs && null specified_tvs
2757 = empty
2758 | null inferred_tvs
2759 = hang (text "NB: Specified variables")
2760 2 (sep [pp_spec, text "always come first"])
2761 | null specified_tvs
2762 = hang (text "NB: Inferred variables")
2763 2 (sep [pp_inf, text "always come first"])
2764 | otherwise
2765 = hang (text "NB: Inferred variables")
2766 2 (vcat [ sep [ pp_inf, text "always come first"]
2767 , sep [text "then Specified variables", pp_spec]])
2768
2769 {-
2770 ************************************************************************
2771 * *
2772 \subsection{Auxiliary functions}
2773 * *
2774 ************************************************************************
2775 -}
2776
2777 -- Free variables of a type, retaining repetitions, and expanding synonyms
2778 -- This ignores coercions, as coercions aren't user-written
2779 fvType :: Type -> [TyCoVar]
2780 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
2781 fvType (TyVarTy tv) = [tv]
2782 fvType (TyConApp _ tys) = fvTypes tys
2783 fvType (LitTy {}) = []
2784 fvType (AppTy fun arg) = fvType fun ++ fvType arg
2785 fvType (FunTy _ w arg res) = fvType w ++ fvType arg ++ fvType res
2786 fvType (ForAllTy (Bndr tv _) ty)
2787 = fvType (tyVarKind tv) ++
2788 filter (/= tv) (fvType ty)
2789 fvType (CastTy ty _) = fvType ty
2790 fvType (CoercionTy {}) = []
2791
2792 fvTypes :: [Type] -> [TyVar]
2793 fvTypes tys = concatMap fvType tys
2794
2795 sizeType :: Type -> Int
2796 -- Size of a type: the number of variables and constructors
2797 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
2798 sizeType (TyVarTy {}) = 1
2799 sizeType (TyConApp tc tys) = 1 + sizeTyConAppArgs tc tys
2800 sizeType (LitTy {}) = 1
2801 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
2802 sizeType (FunTy _ w arg res) = sizeType w + sizeType arg + sizeType res + 1
2803 sizeType (ForAllTy _ ty) = sizeType ty
2804 sizeType (CastTy ty _) = sizeType ty
2805 sizeType (CoercionTy _) = 0
2806
2807 sizeTypes :: [Type] -> Int
2808 sizeTypes = foldr ((+) . sizeType) 0
2809
2810 sizeTyConAppArgs :: TyCon -> [Type] -> Int
2811 sizeTyConAppArgs _tc tys = sizeTypes tys -- (filterOutInvisibleTypes tc tys)
2812 -- See Note [Invisible arguments and termination]
2813
2814 -- Size of a predicate
2815 --
2816 -- We are considering whether class constraints terminate.
2817 -- Equality constraints and constraints for the implicit
2818 -- parameter class always terminate so it is safe to say "size 0".
2819 -- See #4200.
2820 sizePred :: PredType -> Int
2821 sizePred ty = goClass ty
2822 where
2823 goClass p = go (classifyPredType p)
2824
2825 go (ClassPred cls tys')
2826 | isTerminatingClass cls = 0
2827 | otherwise = sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys')
2828 -- The filtering looks bogus
2829 -- See Note [Invisible arguments and termination]
2830 go (EqPred {}) = 0
2831 go (SpecialPred {}) = 0
2832 go (IrredPred ty) = sizeType ty
2833 go (ForAllPred _ _ pred) = goClass pred
2834
2835 -- | When this says "True", ignore this class constraint during
2836 -- a termination check
2837 isTerminatingClass :: Class -> Bool
2838 isTerminatingClass cls
2839 = isIPClass cls -- Implicit parameter constraints always terminate because
2840 -- there are no instances for them --- they are only solved
2841 -- by "local instances" in expressions
2842 || isEqPredClass cls
2843 || cls `hasKey` typeableClassKey
2844 || cls `hasKey` coercibleTyConKey
2845
2846 allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool
2847 -- (allDistinctTyVars tvs tys) returns True if tys are
2848 -- a) all tyvars
2849 -- b) all distinct
2850 -- c) disjoint from tvs
2851 allDistinctTyVars _ [] = True
2852 allDistinctTyVars tkvs (ty : tys)
2853 = case getTyVar_maybe ty of
2854 Nothing -> False
2855 Just tv | tv `elemVarSet` tkvs -> False
2856 | otherwise -> allDistinctTyVars (tkvs `extendVarSet` tv) tys