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