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