Make validDerivPred ignore non-visible arguments to a class type constructor
[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 ContextKind(..), expectedKindInCtxt,
11 checkValidTheta, checkValidFamPats,
12 checkValidInstance, validDerivPred,
13 checkInstTermination,
14 ClsInstInfo, checkValidCoAxiom, checkValidCoAxBranch,
15 checkValidTyFamEqn,
16 arityErr, badATErr,
17 checkValidTelescope, checkZonkValidTelescope, checkValidInferredKinds,
18 allDistinctTyVars
19 ) where
20
21 #include "HsVersions.h"
22
23 import Maybes
24
25 -- friends:
26 import TcUnify ( tcSubType_NC )
27 import TcSimplify ( simplifyAmbiguityCheck )
28 import TyCoRep
29 import TcType hiding ( sizeType, sizeTypes )
30 import TcMType
31 import PrelNames
32 import Type
33 import Coercion
34 import Kind
35 import CoAxiom
36 import Class
37 import TyCon
38
39 -- others:
40 import HsSyn -- HsType
41 import TcRnMonad -- TcType, amongst others
42 import TcHsSyn ( checkForRepresentationPolymorphism )
43 import TcEnv ( tcGetInstEnvs )
44 import FunDeps
45 import InstEnv ( ClsInst, lookupInstEnv, isOverlappable )
46 import FamInstEnv ( isDominatedBy, injectiveBranches,
47 InjectivityCheckResult(..) )
48 import FamInst ( makeInjectivityErrors )
49 import Name
50 import VarEnv
51 import VarSet
52 import Var ( mkTyVar )
53 import ErrUtils
54 import DynFlags
55 import Util
56 import ListSetOps
57 import SrcLoc
58 import Outputable
59 import BasicTypes
60 import Module
61 import Unique ( mkAlphaTyVarUnique )
62 import qualified GHC.LanguageExtensions as LangExt
63
64 import Control.Monad
65 import Data.List ( (\\) )
66
67 {-
68 ************************************************************************
69 * *
70 Checking for ambiguity
71 * *
72 ************************************************************************
73
74 Note [The ambiguity check for type signatures]
75 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
76 checkAmbiguity is a check on *user-supplied type signatures*. It is
77 *purely* there to report functions that cannot possibly be called. So for
78 example we want to reject:
79 f :: C a => Int
80 The idea is there can be no legal calls to 'f' because every call will
81 give rise to an ambiguous constraint. We could soundly omit the
82 ambiguity check on type signatures entirely, at the expense of
83 delaying ambiguity errors to call sites. Indeed, the flag
84 -XAllowAmbiguousTypes switches off the ambiguity check.
85
86 What about things like this:
87 class D a b | a -> b where ..
88 h :: D Int b => Int
89 The Int may well fix 'b' at the call site, so that signature should
90 not be rejected. Moreover, using *visible* fundeps is too
91 conservative. Consider
92 class X a b where ...
93 class D a b | a -> b where ...
94 instance D a b => X [a] b where...
95 h :: X a b => a -> a
96 Here h's type looks ambiguous in 'b', but here's a legal call:
97 ...(h [True])...
98 That gives rise to a (X [Bool] beta) constraint, and using the
99 instance means we need (D Bool beta) and that fixes 'beta' via D's
100 fundep!
101
102 Behind all these special cases there is a simple guiding principle.
103 Consider
104
105 f :: <type>
106 f = ...blah...
107
108 g :: <type>
109 g = f
110
111 You would think that the definition of g would surely typecheck!
112 After all f has exactly the same type, and g=f. But in fact f's type
113 is instantiated and the instantiated constraints are solved against
114 the originals, so in the case an ambiguous type it won't work.
115 Consider our earlier example f :: C a => Int. Then in g's definition,
116 we'll instantiate to (C alpha) and try to deduce (C alpha) from (C a),
117 and fail.
118
119 So in fact we use this as our *definition* of ambiguity. We use a
120 very similar test for *inferred* types, to ensure that they are
121 unambiguous. See Note [Impedence matching] in TcBinds.
122
123 This test is very conveniently implemented by calling
124 tcSubType <type> <type>
125 This neatly takes account of the functional dependecy stuff above,
126 and implicit parameter (see Note [Implicit parameters and ambiguity]).
127 And this is what checkAmbiguity does.
128
129 What about this, though?
130 g :: C [a] => Int
131 Is every call to 'g' ambiguous? After all, we might have
132 intance C [a] where ...
133 at the call site. So maybe that type is ok! Indeed even f's
134 quintessentially ambiguous type might, just possibly be callable:
135 with -XFlexibleInstances we could have
136 instance C a where ...
137 and now a call could be legal after all! Well, we'll reject this
138 unless the instance is available *here*.
139
140 Note [When to call checkAmbiguity]
141 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
142 We call checkAmbiguity
143 (a) on user-specified type signatures
144 (b) in checkValidType
145
146 Conncerning (b), you might wonder about nested foralls. What about
147 f :: forall b. (forall a. Eq a => b) -> b
148 The nested forall is ambiguous. Originally we called checkAmbiguity
149 in the forall case of check_type, but that had two bad consequences:
150 * We got two error messages about (Eq b) in a nested forall like this:
151 g :: forall a. Eq a => forall b. Eq b => a -> a
152 * If we try to check for ambiguity of an nested forall like
153 (forall a. Eq a => b), the implication constraint doesn't bind
154 all the skolems, which results in "No skolem info" in error
155 messages (see Trac #10432).
156
157 To avoid this, we call checkAmbiguity once, at the top, in checkValidType.
158 (I'm still a bit worried about unbound skolems when the type mentions
159 in-scope type variables.)
160
161 In fact, because of the co/contra-variance implemented in tcSubType,
162 this *does* catch function f above. too.
163
164 Concerning (a) the ambiguity check is only used for *user* types, not
165 for types coming from inteface files. The latter can legitimately
166 have ambiguous types. Example
167
168 class S a where s :: a -> (Int,Int)
169 instance S Char where s _ = (1,1)
170 f:: S a => [a] -> Int -> (Int,Int)
171 f (_::[a]) x = (a*x,b)
172 where (a,b) = s (undefined::a)
173
174 Here the worker for f gets the type
175 fw :: forall a. S a => Int -> (# Int, Int #)
176
177
178 Note [Implicit parameters and ambiguity]
179 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
180 Only a *class* predicate can give rise to ambiguity
181 An *implicit parameter* cannot. For example:
182 foo :: (?x :: [a]) => Int
183 foo = length ?x
184 is fine. The call site will supply a particular 'x'
185
186 Furthermore, the type variables fixed by an implicit parameter
187 propagate to the others. E.g.
188 foo :: (Show a, ?x::[a]) => Int
189 foo = show (?x++?x)
190 The type of foo looks ambiguous. But it isn't, because at a call site
191 we might have
192 let ?x = 5::Int in foo
193 and all is well. In effect, implicit parameters are, well, parameters,
194 so we can take their type variables into account as part of the
195 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
196 -}
197
198 checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
199 checkAmbiguity ctxt ty
200 | wantAmbiguityCheck ctxt
201 = do { traceTc "Ambiguity check for" (ppr ty)
202 -- Solve the constraints eagerly because an ambiguous type
203 -- can cause a cascade of further errors. Since the free
204 -- tyvars are skolemised, we can safely use tcSimplifyTop
205 ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
206 ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
207 captureConstraints $
208 tcSubType_NC ctxt ty (mkCheckExpType ty)
209 ; simplifyAmbiguityCheck ty wanted
210
211 ; traceTc "Done ambiguity check for" (ppr ty) }
212
213 | otherwise
214 = return ()
215 where
216 mk_msg allow_ambiguous
217 = vcat [ text "In the ambiguity check for" <+> what
218 , ppUnless allow_ambiguous ambig_msg ]
219 ambig_msg = text "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes"
220 what | Just n <- isSigMaybe ctxt = quotes (ppr n)
221 | otherwise = pprUserTypeCtxt ctxt
222
223 wantAmbiguityCheck :: UserTypeCtxt -> Bool
224 wantAmbiguityCheck ctxt
225 = case ctxt of -- See Note [When we don't check for ambiguity]
226 GhciCtxt -> False
227 TySynCtxt {} -> False
228 _ -> True
229
230 checkUserTypeError :: Type -> TcM ()
231 -- Check to see if the type signature mentions "TypeError blah"
232 -- anywhere in it, and fail if so.
233 --
234 -- Very unsatisfactorily (Trac #11144) we need to tidy the type
235 -- because it may have come from an /inferred/ signature, not a
236 -- user-supplied one. This is really only a half-baked fix;
237 -- the other errors in checkValidType don't do tidying, and so
238 -- may give bad error messages when given an inferred type.
239 checkUserTypeError = check
240 where
241 check ty
242 | Just msg <- userTypeError_maybe ty = fail_with msg
243 | Just (_,ts) <- splitTyConApp_maybe ty = mapM_ check ts
244 | Just (t1,t2) <- splitAppTy_maybe ty = check t1 >> check t2
245 | Just (_,t1) <- splitForAllTy_maybe ty = check t1
246 | otherwise = return ()
247
248 fail_with msg = do { env0 <- tcInitTidyEnv
249 ; let (env1, tidy_msg) = tidyOpenType env0 msg
250 ; failWithTcM (env1, pprUserTypeErrorTy tidy_msg) }
251
252
253 {- Note [When we don't check for ambiguity]
254 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
255 In a few places we do not want to check a user-specified type for ambiguity
256
257 * GhciCtxt: Allow ambiguous types in GHCi's :kind command
258 E.g. type family T a :: * -- T :: forall k. k -> *
259 Then :k T should work in GHCi, not complain that
260 (T k) is ambiguous!
261
262 * TySynCtxt: type T a b = C a b => blah
263 It may be that when we /use/ T, we'll give an 'a' or 'b' that somehow
264 cure the ambiguity. So we defer the ambiguity check to the use site.
265
266 There is also an implementation reason (Trac #11608). In the RHS of
267 a type synonym we don't (currently) instantiate 'a' and 'b' with
268 TcTyVars before calling checkValidType, so we get asertion failures
269 from doing an ambiguity check on a type with TyVars in it. Fixing this
270 would not be hard, but let's wait till there's a reason.
271
272
273 ************************************************************************
274 * *
275 Checking validity of a user-defined type
276 * *
277 ************************************************************************
278
279 When dealing with a user-written type, we first translate it from an HsType
280 to a Type, performing kind checking, and then check various things that should
281 be true about it. We don't want to perform these checks at the same time
282 as the initial translation because (a) they are unnecessary for interface-file
283 types and (b) when checking a mutually recursive group of type and class decls,
284 we can't "look" at the tycons/classes yet. Also, the checks are rather
285 diverse, and used to really mess up the other code.
286
287 One thing we check for is 'rank'.
288
289 Rank 0: monotypes (no foralls)
290 Rank 1: foralls at the front only, Rank 0 inside
291 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
292
293 basic ::= tyvar | T basic ... basic
294
295 r2 ::= forall tvs. cxt => r2a
296 r2a ::= r1 -> r2a | basic
297 r1 ::= forall tvs. cxt => r0
298 r0 ::= r0 -> r0 | basic
299
300 Another thing is to check that type synonyms are saturated.
301 This might not necessarily show up in kind checking.
302 type A i = i
303 data T k = MkT (k Int)
304 f :: T A -- BAD!
305 -}
306
307 checkValidType :: UserTypeCtxt -> Type -> TcM ()
308 -- Checks that a user-written type is valid for the given context
309 -- Assumes arguemt is fully zonked
310 -- Not used for instance decls; checkValidInstance instead
311 checkValidType ctxt ty
312 = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
313 ; rankn_flag <- xoptM LangExt.RankNTypes
314 ; impred_flag <- xoptM LangExt.ImpredicativeTypes
315 ; let gen_rank :: Rank -> Rank
316 gen_rank r | rankn_flag = ArbitraryRank
317 | otherwise = r
318
319 rank1 = gen_rank r1
320 rank0 = gen_rank r0
321
322 r0 = rankZeroMonoType
323 r1 = LimitedRank True r0
324
325 rank
326 = case ctxt of
327 DefaultDeclCtxt-> MustBeMonoType
328 ResSigCtxt -> MustBeMonoType
329 PatSigCtxt -> rank0
330 RuleSigCtxt _ -> rank1
331 TySynCtxt _ -> rank0
332
333 ExprSigCtxt -> rank1
334 TypeAppCtxt | impred_flag -> ArbitraryRank
335 | otherwise -> tyConArgMonoType
336 -- Normally, ImpredicativeTypes is handled in check_arg_type,
337 -- but visible type applications don't go through there.
338 -- So we do this check here.
339
340 FunSigCtxt {} -> rank1
341 InfSigCtxt _ -> ArbitraryRank -- Inferred type
342 ConArgCtxt _ -> rank1 -- We are given the type of the entire
343 -- constructor, hence rank 1
344
345 ForSigCtxt _ -> rank1
346 SpecInstCtxt -> rank1
347 ThBrackCtxt -> rank1
348 GhciCtxt -> ArbitraryRank
349 _ -> panic "checkValidType"
350 -- Can't happen; not used for *user* sigs
351
352 ; env <- tcInitOpenTidyEnv (tyCoVarsOfType ty)
353
354 -- Check the internal validity of the type itself
355 ; check_type env ctxt rank ty
356
357 -- Check that the thing has kind Type, and is lifted if necessary.
358 -- Do this *after* check_type, because we can't usefully take
359 -- the kind of an ill-formed type such as (a~Int)
360 ; check_kind env ctxt ty
361
362 ; checkUserTypeError ty
363
364 -- Check for ambiguous types. See Note [When to call checkAmbiguity]
365 -- NB: this will happen even for monotypes, but that should be cheap;
366 -- and there may be nested foralls for the subtype test to examine
367 ; checkAmbiguity ctxt ty
368
369 ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }
370
371 checkValidMonoType :: Type -> TcM ()
372 -- Assumes arguemt is fully zonked
373 checkValidMonoType ty
374 = do { env <- tcInitOpenTidyEnv (tyCoVarsOfType ty)
375 ; check_type env SigmaCtxt MustBeMonoType ty }
376
377 check_kind :: TidyEnv -> UserTypeCtxt -> TcType -> TcM ()
378 -- Check that the type's kind is acceptable for the context
379 check_kind env ctxt ty
380 | TySynCtxt {} <- ctxt
381 , returnsConstraintKind actual_kind
382 = do { ck <- xoptM LangExt.ConstraintKinds
383 ; if ck
384 then when (isConstraintKind actual_kind)
385 (do { dflags <- getDynFlags
386 ; check_pred_ty env dflags ctxt ty })
387 else addErrTcM (constraintSynErr env actual_kind) }
388
389 | otherwise
390 = case expectedKindInCtxt ctxt of
391 TheKind k -> checkTcM (tcEqType actual_kind k) (kindErr env actual_kind)
392 OpenKind -> checkTcM (classifiesTypeWithValues actual_kind) (kindErr env actual_kind)
393 AnythingKind -> return ()
394 where
395 actual_kind = typeKind ty
396
397 -- | The kind expected in a certain context.
398 data ContextKind = TheKind Kind -- ^ a specific kind
399 | AnythingKind -- ^ any kind will do
400 | OpenKind -- ^ something of the form @TYPE _@
401
402 -- Depending on the context, we might accept any kind (for instance, in a TH
403 -- splice), or only certain kinds (like in type signatures).
404 expectedKindInCtxt :: UserTypeCtxt -> ContextKind
405 expectedKindInCtxt (TySynCtxt _) = AnythingKind
406 expectedKindInCtxt ThBrackCtxt = AnythingKind
407 expectedKindInCtxt GhciCtxt = AnythingKind
408 -- The types in a 'default' decl can have varying kinds
409 -- See Note [Extended defaults]" in TcEnv
410 expectedKindInCtxt DefaultDeclCtxt = AnythingKind
411 expectedKindInCtxt TypeAppCtxt = AnythingKind
412 expectedKindInCtxt (ForSigCtxt _) = TheKind liftedTypeKind
413 expectedKindInCtxt InstDeclCtxt = TheKind constraintKind
414 expectedKindInCtxt SpecInstCtxt = TheKind constraintKind
415 expectedKindInCtxt _ = OpenKind
416
417 {-
418 Note [Higher rank types]
419 ~~~~~~~~~~~~~~~~~~~~~~~~
420 Technically
421 Int -> forall a. a->a
422 is still a rank-1 type, but it's not Haskell 98 (Trac #5957). So the
423 validity checker allow a forall after an arrow only if we allow it
424 before -- that is, with Rank2Types or RankNTypes
425 -}
426
427 data Rank = ArbitraryRank -- Any rank ok
428
429 | LimitedRank -- Note [Higher rank types]
430 Bool -- Forall ok at top
431 Rank -- Use for function arguments
432
433 | MonoType SDoc -- Monotype, with a suggestion of how it could be a polytype
434
435 | MustBeMonoType -- Monotype regardless of flags
436
437
438 rankZeroMonoType, tyConArgMonoType, synArgMonoType, constraintMonoType :: Rank
439 rankZeroMonoType = MonoType (text "Perhaps you intended to use RankNTypes or Rank2Types")
440 tyConArgMonoType = MonoType (text "GHC doesn't yet support impredicative polymorphism")
441 synArgMonoType = MonoType (text "Perhaps you intended to use LiberalTypeSynonyms")
442 constraintMonoType = MonoType (text "A constraint must be a monotype")
443
444 funArgResRank :: Rank -> (Rank, Rank) -- Function argument and result
445 funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
446 funArgResRank other_rank = (other_rank, other_rank)
447
448 forAllAllowed :: Rank -> Bool
449 forAllAllowed ArbitraryRank = True
450 forAllAllowed (LimitedRank forall_ok _) = forall_ok
451 forAllAllowed _ = False
452
453 -- The zonker issues errors if it zonks a representation-polymorphic binder
454 -- But sometimes it's nice to check a little more eagerly, trying to report
455 -- errors earlier.
456 representationPolymorphismForbidden :: UserTypeCtxt -> Bool
457 representationPolymorphismForbidden = go
458 where
459 go (ConArgCtxt _) = True -- A rep-polymorphic datacon won't be useful
460 go (PatSynCtxt _) = True -- Similar to previous case
461 go _ = False -- Other cases are caught by zonker
462
463 ----------------------------------------
464 -- | Fail with error message if the type is unlifted
465 check_lifted :: Type -> TcM ()
466 check_lifted _ = return ()
467
468 {- ------ Legacy comment ---------
469 The check_unlifted function seems entirely redundant. The
470 kind system should check for uses of unlifted types. So I've
471 removed the check. See Trac #11120 comment:19.
472
473 check_lifted ty
474 = do { env <- tcInitOpenTidyEnv (tyCoVarsOfType ty)
475 ; checkTcM (not (isUnliftedType ty)) (unliftedArgErr env ty) }
476
477 unliftedArgErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
478 unliftedArgErr env ty = (env, sep [text "Illegal unlifted type:", ppr_tidy env ty])
479 ------ End of legacy comment --------- -}
480
481
482 check_type :: TidyEnv -> UserTypeCtxt -> Rank -> Type -> TcM ()
483 -- The args say what the *type context* requires, independent
484 -- of *flag* settings. You test the flag settings at usage sites.
485 --
486 -- Rank is allowed rank for function args
487 -- Rank 0 means no for-alls anywhere
488
489 check_type env ctxt rank ty
490 | not (null tvs && null theta)
491 = do { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
492 ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
493 -- Reject e.g. (Maybe (?x::Int => Int)),
494 -- with a decent error message
495
496 ; check_valid_theta env' SigmaCtxt theta
497 -- Allow type T = ?x::Int => Int -> Int
498 -- but not type T = ?x::Int
499
500 ; check_type env' ctxt rank tau -- Allow foralls to right of arrow
501 ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
502 (forAllEscapeErr env' ty tau_kind)
503 }
504 where
505 (tvs, theta, tau) = tcSplitSigmaTy ty
506 tau_kind = typeKind tau
507 (env', _) = tidyTyCoVarBndrs env tvs
508
509 phi_kind | null theta = tau_kind
510 | otherwise = liftedTypeKind
511 -- If there are any constraints, the kind is *. (#11405)
512
513 check_type _ _ _ (TyVarTy _) = return ()
514
515 check_type env ctxt rank (ForAllTy (Anon arg_ty) res_ty)
516 = do { check_type env ctxt arg_rank arg_ty
517 ; when (representationPolymorphismForbidden ctxt) $
518 checkForRepresentationPolymorphism empty arg_ty
519 ; check_type env ctxt res_rank res_ty }
520 where
521 (arg_rank, res_rank) = funArgResRank rank
522
523 check_type env ctxt rank (AppTy ty1 ty2)
524 = do { check_arg_type env ctxt rank ty1
525 ; check_arg_type env ctxt rank ty2 }
526
527 check_type env ctxt rank ty@(TyConApp tc tys)
528 | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
529 = check_syn_tc_app env ctxt rank ty tc tys
530 | isUnboxedTupleTyCon tc = check_ubx_tuple env ctxt ty tys
531 | otherwise = mapM_ (check_arg_type env ctxt rank) tys
532
533 check_type _ _ _ (LitTy {}) = return ()
534
535 check_type env ctxt rank (CastTy ty _) = check_type env ctxt rank ty
536
537 check_type _ _ _ ty = pprPanic "check_type" (ppr ty)
538
539 ----------------------------------------
540 check_syn_tc_app :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType
541 -> TyCon -> [KindOrType] -> TcM ()
542 -- Used for type synonyms and type synonym families,
543 -- which must be saturated,
544 -- but not data families, which need not be saturated
545 check_syn_tc_app env ctxt rank ty tc tys
546 | tc_arity <= length tys -- Saturated
547 -- Check that the synonym has enough args
548 -- This applies equally to open and closed synonyms
549 -- It's OK to have an *over-applied* type synonym
550 -- data Tree a b = ...
551 -- type Foo a = Tree [a]
552 -- f :: Foo a b -> ...
553 = do { -- See Note [Liberal type synonyms]
554 ; liberal <- xoptM LangExt.LiberalTypeSynonyms
555 ; if not liberal || isTypeFamilyTyCon tc then
556 -- For H98 and synonym families, do check the type args
557 mapM_ check_arg tys
558
559 else -- In the liberal case (only for closed syns), expand then check
560 case coreView ty of
561 Just ty' -> check_type env ctxt rank ty'
562 Nothing -> pprPanic "check_tau_type" (ppr ty) }
563
564 | GhciCtxt <- ctxt -- Accept under-saturated type synonyms in
565 -- GHCi :kind commands; see Trac #7586
566 = mapM_ check_arg tys
567
568 | otherwise
569 = failWithTc (tyConArityErr tc tys)
570 where
571 tc_arity = tyConArity tc
572 check_arg | isTypeFamilyTyCon tc = check_arg_type env ctxt rank
573 | otherwise = check_type env ctxt synArgMonoType
574
575 ----------------------------------------
576 check_ubx_tuple :: TidyEnv -> UserTypeCtxt -> KindOrType
577 -> [KindOrType] -> TcM ()
578 check_ubx_tuple env ctxt ty tys
579 = do { ub_tuples_allowed <- xoptM LangExt.UnboxedTuples
580 ; checkTcM ub_tuples_allowed (ubxArgTyErr env ty)
581
582 ; impred <- xoptM LangExt.ImpredicativeTypes
583 ; let rank' = if impred then ArbitraryRank else tyConArgMonoType
584 -- c.f. check_arg_type
585 -- However, args are allowed to be unlifted, or
586 -- more unboxed tuples, so can't use check_arg_ty
587 ; mapM_ (check_type env ctxt rank') tys }
588
589 ----------------------------------------
590 check_arg_type :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType -> TcM ()
591 -- The sort of type that can instantiate a type variable,
592 -- or be the argument of a type constructor.
593 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
594 -- Other unboxed types are very occasionally allowed as type
595 -- arguments depending on the kind of the type constructor
596 --
597 -- For example, we want to reject things like:
598 --
599 -- instance Ord a => Ord (forall s. T s a)
600 -- and
601 -- g :: T s (forall b.b)
602 --
603 -- NB: unboxed tuples can have polymorphic or unboxed args.
604 -- This happens in the workers for functions returning
605 -- product types with polymorphic components.
606 -- But not in user code.
607 -- Anyway, they are dealt with by a special case in check_tau_type
608
609 check_arg_type _ _ _ (CoercionTy {}) = return ()
610
611 check_arg_type env ctxt rank ty
612 = do { impred <- xoptM LangExt.ImpredicativeTypes
613 ; let rank' = case rank of -- Predictive => must be monotype
614 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
615 _other | impred -> ArbitraryRank
616 | otherwise -> tyConArgMonoType
617 -- Make sure that MustBeMonoType is propagated,
618 -- so that we don't suggest -XImpredicativeTypes in
619 -- (Ord (forall a.a)) => a -> a
620 -- and so that if it Must be a monotype, we check that it is!
621
622 ; check_type env ctxt rank' ty
623 ; check_lifted ty }
624 -- NB the isUnliftedType test also checks for
625 -- T State#
626 -- where there is an illegal partial application of State# (which has
627 -- kind * -> #); see Note [The kind invariant] in TyCoRep
628
629 ----------------------------------------
630 forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
631 forAllTyErr env rank ty
632 = ( env
633 , vcat [ hang herald 2 (ppr_tidy env ty)
634 , suggestion ] )
635 where
636 (tvs, _theta, _tau) = tcSplitSigmaTy ty
637 herald | null tvs = text "Illegal qualified type:"
638 | otherwise = text "Illegal polymorphic type:"
639 suggestion = case rank of
640 LimitedRank {} -> text "Perhaps you intended to use RankNTypes or Rank2Types"
641 MonoType d -> d
642 _ -> Outputable.empty -- Polytype is always illegal
643
644 forAllEscapeErr :: TidyEnv -> Type -> Kind -> (TidyEnv, SDoc)
645 forAllEscapeErr env ty tau_kind
646 = ( env
647 , hang (vcat [ text "Quantified type's kind mentions quantified type variable"
648 , text "(skolem escape)" ])
649 2 (vcat [ text " type:" <+> ppr_tidy env ty
650 , text "of kind:" <+> ppr_tidy env tau_kind ]) )
651
652 ubxArgTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
653 ubxArgTyErr env ty = (env, sep [text "Illegal unboxed tuple type as function argument:", ppr_tidy env ty])
654
655 kindErr :: TidyEnv -> Kind -> (TidyEnv, SDoc)
656 kindErr env kind = (env, sep [text "Expecting an ordinary type, but found a type of kind", ppr_tidy env kind])
657
658 {-
659 Note [Liberal type synonyms]
660 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
661 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
662 doing validity checking. This allows us to instantiate a synonym defn
663 with a for-all type, or with a partially-applied type synonym.
664 e.g. type T a b = a
665 type S m = m ()
666 f :: S (T Int)
667 Here, T is partially applied, so it's illegal in H98. But if you
668 expand S first, then T we get just
669 f :: Int
670 which is fine.
671
672 IMPORTANT: suppose T is a type synonym. Then we must do validity
673 checking on an appliation (T ty1 ty2)
674
675 *either* before expansion (i.e. check ty1, ty2)
676 *or* after expansion (i.e. expand T ty1 ty2, and then check)
677 BUT NOT BOTH
678
679 If we do both, we get exponential behaviour!!
680
681 data TIACons1 i r c = c i ::: r c
682 type TIACons2 t x = TIACons1 t (TIACons1 t x)
683 type TIACons3 t x = TIACons2 t (TIACons1 t x)
684 type TIACons4 t x = TIACons2 t (TIACons2 t x)
685 type TIACons7 t x = TIACons4 t (TIACons3 t x)
686
687
688 ************************************************************************
689 * *
690 \subsection{Checking a theta or source type}
691 * *
692 ************************************************************************
693
694 Note [Implicit parameters in instance decls]
695 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
696 Implicit parameters _only_ allowed in type signatures; not in instance
697 decls, superclasses etc. The reason for not allowing implicit params in
698 instances is a bit subtle. If we allowed
699 instance (?x::Int, Eq a) => Foo [a] where ...
700 then when we saw
701 (e :: (?x::Int) => t)
702 it would be unclear how to discharge all the potential uses of the ?x
703 in e. For example, a constraint Foo [Int] might come out of e, and
704 applying the instance decl would show up two uses of ?x. Trac #8912.
705 -}
706
707 checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
708 -- Assumes arguemt is fully zonked
709 checkValidTheta ctxt theta
710 = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypes theta)
711 ; addErrCtxtM (checkThetaCtxt ctxt theta) $
712 check_valid_theta env ctxt theta }
713
714 -------------------------
715 check_valid_theta :: TidyEnv -> UserTypeCtxt -> [PredType] -> TcM ()
716 check_valid_theta _ _ []
717 = return ()
718 check_valid_theta env ctxt theta
719 = do { dflags <- getDynFlags
720 ; warnTcM (Reason Opt_WarnDuplicateConstraints)
721 (wopt Opt_WarnDuplicateConstraints dflags && notNull dups)
722 (dupPredWarn env dups)
723 ; traceTc "check_valid_theta" (ppr theta)
724 ; mapM_ (check_pred_ty env dflags ctxt) theta }
725 where
726 (_,dups) = removeDups cmpType theta
727
728 -------------------------
729 {- Note [Validity checking for constraints]
730 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
731 We look through constraint synonyms so that we can see the underlying
732 constraint(s). For example
733 type Foo = ?x::Int
734 instance Foo => C T
735 We should reject the instance because it has an implicit parameter in
736 the context.
737
738 But we record, in 'under_syn', whether we have looked under a synonym
739 to avoid requiring language extensions at the use site. Main example
740 (Trac #9838):
741
742 {-# LANGUAGE ConstraintKinds #-}
743 module A where
744 type EqShow a = (Eq a, Show a)
745
746 module B where
747 import A
748 foo :: EqShow a => a -> String
749
750 We don't want to require ConstraintKinds in module B.
751 -}
752
753 check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
754 -- Check the validity of a predicate in a signature
755 -- See Note [Validity checking for constraints]
756 check_pred_ty env dflags ctxt pred
757 = do { check_type env SigmaCtxt constraintMonoType pred
758 ; check_pred_help False env dflags ctxt pred }
759
760 check_pred_help :: Bool -- True <=> under a type synonym
761 -> TidyEnv
762 -> DynFlags -> UserTypeCtxt
763 -> PredType -> TcM ()
764 check_pred_help under_syn env dflags ctxt pred
765 | Just pred' <- coreView pred -- Switch on under_syn when going under a
766 -- synonym (Trac #9838, yuk)
767 = check_pred_help True env dflags ctxt pred'
768 | otherwise
769 = case splitTyConApp_maybe pred of
770 Just (tc, tys)
771 | isTupleTyCon tc
772 -> check_tuple_pred under_syn env dflags ctxt pred tys
773 -- NB: this equality check must come first, because (~) is a class,
774 -- too.
775 | tc `hasKey` heqTyConKey ||
776 tc `hasKey` eqTyConKey ||
777 tc `hasKey` eqPrimTyConKey
778 -> check_eq_pred env dflags pred tc tys
779 | Just cls <- tyConClass_maybe tc
780 -> check_class_pred env dflags ctxt pred cls tys -- Includes Coercible
781 _ -> check_irred_pred under_syn env dflags ctxt pred
782
783 check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TyCon -> [TcType] -> TcM ()
784 check_eq_pred env dflags pred tc tys
785 = -- Equational constraints are valid in all contexts if type
786 -- families are permitted
787 do { checkTc (length tys == tyConArity tc) (tyConArityErr tc tys)
788 ; checkTcM (xopt LangExt.TypeFamilies dflags
789 || xopt LangExt.GADTs dflags)
790 (eqPredTyErr env pred) }
791
792 check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
793 check_tuple_pred under_syn env dflags ctxt pred ts
794 = do { -- See Note [ConstraintKinds in predicates]
795 checkTcM (under_syn || xopt LangExt.ConstraintKinds dflags)
796 (predTupleErr env pred)
797 ; mapM_ (check_pred_help under_syn env dflags ctxt) ts }
798 -- This case will not normally be executed because without
799 -- -XConstraintKinds tuple types are only kind-checked as *
800
801 check_irred_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
802 check_irred_pred under_syn env dflags ctxt pred
803 -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
804 -- where X is a type function
805 = do { -- If it looks like (x t1 t2), require ConstraintKinds
806 -- see Note [ConstraintKinds in predicates]
807 -- But (X t1 t2) is always ok because we just require ConstraintKinds
808 -- at the definition site (Trac #9838)
809 failIfTcM (not under_syn && not (xopt LangExt.ConstraintKinds dflags)
810 && hasTyVarHead pred)
811 (predIrredErr env pred)
812
813 -- Make sure it is OK to have an irred pred in this context
814 -- See Note [Irreducible predicates in superclasses]
815 ; failIfTcM (is_superclass ctxt
816 && not (xopt LangExt.UndecidableInstances dflags)
817 && has_tyfun_head pred)
818 (predSuperClassErr env pred) }
819 where
820 is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False }
821 has_tyfun_head ty
822 = case tcSplitTyConApp_maybe ty of
823 Just (tc, _) -> isTypeFamilyTyCon tc
824 Nothing -> False
825
826 {- Note [ConstraintKinds in predicates]
827 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
828 Don't check for -XConstraintKinds under a type synonym, because that
829 was done at the type synonym definition site; see Trac #9838
830 e.g. module A where
831 type C a = (Eq a, Ix a) -- Needs -XConstraintKinds
832 module B where
833 import A
834 f :: C a => a -> a -- Does *not* need -XConstraintKinds
835
836 Note [Irreducible predicates in superclasses]
837 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
838 Allowing type-family calls in class superclasses is somewhat dangerous
839 because we can write:
840
841 type family Fooish x :: * -> Constraint
842 type instance Fooish () = Foo
843 class Fooish () a => Foo a where
844
845 This will cause the constraint simplifier to loop because every time we canonicalise a
846 (Foo a) class constraint we add a (Fooish () a) constraint which will be immediately
847 solved to add+canonicalise another (Foo a) constraint. -}
848
849 -------------------------
850 check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
851 check_class_pred env dflags ctxt pred cls tys
852 | isIPClass cls
853 = do { check_arity
854 ; checkTcM (okIPCtxt ctxt) (badIPPred env pred) }
855
856 | otherwise
857 = do { check_arity
858 ; check_simplifiable_class_constraint
859 ; checkTcM arg_tys_ok (predTyVarErr env pred) }
860 where
861 check_arity = checkTc (classArity cls == length tys)
862 (tyConArityErr (classTyCon cls) tys)
863
864 -- Check the arguments of a class constraint
865 flexible_contexts = xopt LangExt.FlexibleContexts dflags
866 undecidable_ok = xopt LangExt.UndecidableInstances dflags
867 arg_tys_ok = case ctxt of
868 SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
869 InstDeclCtxt -> checkValidClsArgs (flexible_contexts || undecidable_ok) cls tys
870 -- Further checks on head and theta
871 -- in checkInstTermination
872 _ -> checkValidClsArgs flexible_contexts cls tys
873
874 -- See Note [Simplifiable given constraints]
875 check_simplifiable_class_constraint
876 | DataTyCtxt {} <- ctxt -- Don't do this check for the "stupid theta"
877 = return () -- of a data type declaration
878 | otherwise
879 = do { instEnvs <- tcGetInstEnvs
880 ; let (matches, _, _) = lookupInstEnv False instEnvs cls tys
881 bad_matches = [ inst | (inst,_) <- matches
882 , not (isOverlappable inst) ]
883 ; warnIf (Reason Opt_WarnSimplifiableClassConstraints)
884 (not (null bad_matches))
885 (simplifiable_constraint_warn bad_matches) }
886
887 simplifiable_constraint_warn :: [ClsInst] -> SDoc
888 simplifiable_constraint_warn (match : _)
889 = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred)))
890 2 (text "matches an instance declaration")
891 , ppr match
892 , hang (text "This makes type inference very fragile;")
893 2 (text "try simplifying it using the instance") ]
894 simplifiable_constraint_warn [] = pprPanic "check_class_pred" (ppr pred)
895
896 {- Note [Simplifiable given constraints]
897 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
898 A type signature like
899 f :: Eq [(a,b)] => a -> b
900 is very fragile, for reasons described at length in TcInteract
901
902 Note [Instance and Given overlap]. So this warning discourages uses
903 from writing simplifiable class constraints, at least unless the
904 top-level instance is explicitly declared as OVERLAPPABLE.
905 Trac #11948 provoked me to do this.
906 -}
907
908 -------------------------
909 okIPCtxt :: UserTypeCtxt -> Bool
910 -- See Note [Implicit parameters in instance decls]
911 okIPCtxt (FunSigCtxt {}) = True
912 okIPCtxt (InfSigCtxt {}) = True
913 okIPCtxt ExprSigCtxt = True
914 okIPCtxt TypeAppCtxt = True
915 okIPCtxt PatSigCtxt = True
916 okIPCtxt ResSigCtxt = True
917 okIPCtxt GenSigCtxt = True
918 okIPCtxt (ConArgCtxt {}) = True
919 okIPCtxt (ForSigCtxt {}) = True -- ??
920 okIPCtxt ThBrackCtxt = True
921 okIPCtxt GhciCtxt = True
922 okIPCtxt SigmaCtxt = True
923 okIPCtxt (DataTyCtxt {}) = True
924 okIPCtxt (PatSynCtxt {}) = True
925 okIPCtxt (TySynCtxt {}) = True -- e.g. type Blah = ?x::Int
926 -- Trac #11466
927
928 okIPCtxt (ClassSCCtxt {}) = False
929 okIPCtxt (InstDeclCtxt {}) = False
930 okIPCtxt (SpecInstCtxt {}) = False
931 okIPCtxt (RuleSigCtxt {}) = False
932 okIPCtxt DefaultDeclCtxt = False
933
934 {-
935 Note [Kind polymorphic type classes]
936 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
937 MultiParam check:
938
939 class C f where... -- C :: forall k. k -> Constraint
940 instance C Maybe where...
941
942 The dictionary gets type [C * Maybe] even if it's not a MultiParam
943 type class.
944
945 Flexibility check:
946
947 class C f where... -- C :: forall k. k -> Constraint
948 data D a = D a
949 instance C D where
950
951 The dictionary gets type [C * (D *)]. IA0_TODO it should be
952 generalized actually.
953 -}
954
955 checkThetaCtxt :: UserTypeCtxt -> ThetaType -> TidyEnv -> TcM (TidyEnv, SDoc)
956 checkThetaCtxt ctxt theta env
957 = return ( env
958 , vcat [ text "In the context:" <+> pprTheta (tidyTypes env theta)
959 , text "While checking" <+> pprUserTypeCtxt ctxt ] )
960
961 eqPredTyErr, predTupleErr, predIrredErr, predSuperClassErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
962 eqPredTyErr env pred
963 = ( env
964 , text "Illegal equational constraint" <+> ppr_tidy env pred $$
965 parens (text "Use GADTs or TypeFamilies to permit this") )
966 predTupleErr env pred
967 = ( env
968 , hang (text "Illegal tuple constraint:" <+> ppr_tidy env pred)
969 2 (parens constraintKindsMsg) )
970 predIrredErr env pred
971 = ( env
972 , hang (text "Illegal constraint:" <+> ppr_tidy env pred)
973 2 (parens constraintKindsMsg) )
974 predSuperClassErr env pred
975 = ( env
976 , hang (text "Illegal constraint" <+> quotes (ppr_tidy env pred)
977 <+> text "in a superclass context")
978 2 (parens undecidableMsg) )
979
980 predTyVarErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
981 predTyVarErr env pred
982 = (env
983 , vcat [ hang (text "Non type-variable argument")
984 2 (text "in the constraint:" <+> ppr_tidy env pred)
985 , parens (text "Use FlexibleContexts to permit this") ])
986
987 badIPPred :: TidyEnv -> PredType -> (TidyEnv, SDoc)
988 badIPPred env pred
989 = ( env
990 , text "Illegal implicit parameter" <+> quotes (ppr_tidy env pred) )
991
992 constraintSynErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
993 constraintSynErr env kind
994 = ( env
995 , hang (text "Illegal constraint synonym of kind:" <+> quotes (ppr_tidy env kind))
996 2 (parens constraintKindsMsg) )
997
998 dupPredWarn :: TidyEnv -> [[PredType]] -> (TidyEnv, SDoc)
999 dupPredWarn env dups
1000 = ( env
1001 , text "Duplicate constraint" <> plural primaryDups <> text ":"
1002 <+> pprWithCommas (ppr_tidy env) primaryDups )
1003 where
1004 primaryDups = map head dups
1005
1006 tyConArityErr :: TyCon -> [TcType] -> SDoc
1007 -- For type-constructor arity errors, be careful to report
1008 -- the number of /visible/ arguments required and supplied,
1009 -- ignoring the /invisible/ arguments, which the user does not see.
1010 -- (e.g. Trac #10516)
1011 tyConArityErr tc tks
1012 = arityErr (tyConFlavour tc) (tyConName tc)
1013 tc_type_arity tc_type_args
1014 where
1015 vis_tks = filterOutInvisibleTypes tc tks
1016
1017 -- tc_type_arity = number of *type* args expected
1018 -- tc_type_args = number of *type* args encountered
1019 tc_type_arity = count isVisibleBinder $ tyConBinders tc
1020 tc_type_args = length vis_tks
1021
1022 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
1023 arityErr what name n m
1024 = hsep [ text "The" <+> text what, quotes (ppr name), text "should have",
1025 n_arguments <> comma, text "but has been given",
1026 if m==0 then text "none" else int m]
1027 where
1028 n_arguments | n == 0 = text "no arguments"
1029 | n == 1 = text "1 argument"
1030 | True = hsep [int n, text "arguments"]
1031
1032 {-
1033 ************************************************************************
1034 * *
1035 \subsection{Checking for a decent instance head type}
1036 * *
1037 ************************************************************************
1038
1039 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1040 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1041
1042 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1043 flag is on, or (2)~the instance is imported (they must have been
1044 compiled elsewhere). In these cases, we let them go through anyway.
1045
1046 We can also have instances for functions: @instance Foo (a -> b) ...@.
1047 -}
1048
1049 checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
1050 checkValidInstHead ctxt clas cls_args
1051 = do { dflags <- getDynFlags
1052
1053 ; mod <- getModule
1054 ; checkTc (getUnique clas `notElem` abstractClassKeys ||
1055 nameModule (getName clas) == mod)
1056 (instTypeErr clas cls_args abstract_class_msg)
1057
1058 -- Check language restrictions;
1059 -- but not for SPECIALISE instance pragmas
1060 ; let ty_args = filterOutInvisibleTypes (classTyCon clas) cls_args
1061 ; unless spec_inst_prag $
1062 do { checkTc (xopt LangExt.TypeSynonymInstances dflags ||
1063 all tcInstHeadTyNotSynonym ty_args)
1064 (instTypeErr clas cls_args head_type_synonym_msg)
1065 ; checkTc (xopt LangExt.FlexibleInstances dflags ||
1066 all tcInstHeadTyAppAllTyVars ty_args)
1067 (instTypeErr clas cls_args head_type_args_tyvars_msg)
1068 ; checkTc (xopt LangExt.MultiParamTypeClasses dflags ||
1069 length ty_args == 1 || -- Only count type arguments
1070 (xopt LangExt.NullaryTypeClasses dflags &&
1071 null ty_args))
1072 (instTypeErr clas cls_args head_one_type_msg) }
1073
1074 ; mapM_ checkValidTypePat ty_args }
1075 where
1076 spec_inst_prag = case ctxt of { SpecInstCtxt -> True; _ -> False }
1077
1078 head_type_synonym_msg = parens (
1079 text "All instance types must be of the form (T t1 ... tn)" $$
1080 text "where T is not a synonym." $$
1081 text "Use TypeSynonymInstances if you want to disable this.")
1082
1083 head_type_args_tyvars_msg = parens (vcat [
1084 text "All instance types must be of the form (T a1 ... an)",
1085 text "where a1 ... an are *distinct type variables*,",
1086 text "and each type variable appears at most once in the instance head.",
1087 text "Use FlexibleInstances if you want to disable this."])
1088
1089 head_one_type_msg = parens (
1090 text "Only one type can be given in an instance head." $$
1091 text "Use MultiParamTypeClasses if you want to allow more, or zero.")
1092
1093 abstract_class_msg =
1094 text "Manual instances of this class are not permitted."
1095
1096 tcInstHeadTyNotSynonym :: Type -> Bool
1097 -- Used in Haskell-98 mode, for the argument types of an instance head
1098 -- These must not be type synonyms, but everywhere else type synonyms
1099 -- are transparent, so we need a special function here
1100 tcInstHeadTyNotSynonym ty
1101 = case ty of -- Do not use splitTyConApp,
1102 -- because that expands synonyms!
1103 TyConApp tc _ -> not (isTypeSynonymTyCon tc)
1104 _ -> True
1105
1106 tcInstHeadTyAppAllTyVars :: Type -> Bool
1107 -- Used in Haskell-98 mode, for the argument types of an instance head
1108 -- These must be a constructor applied to type variable arguments.
1109 -- But we allow kind instantiations.
1110 tcInstHeadTyAppAllTyVars ty
1111 | Just (tc, tys) <- tcSplitTyConApp_maybe (dropCasts ty)
1112 = ok (filterOutInvisibleTypes tc tys) -- avoid kinds
1113
1114 | otherwise
1115 = False
1116 where
1117 -- Check that all the types are type variables,
1118 -- and that each is distinct
1119 ok tys = equalLength tvs tys && hasNoDups tvs
1120 where
1121 tvs = mapMaybe tcGetTyVar_maybe tys
1122
1123 dropCasts :: Type -> Type
1124 -- See Note [Casts during validity checking]
1125 -- This function can turn a well-kinded type into an ill-kinded
1126 -- one, so I've kept it local to this module
1127 -- To consider: drop only UnivCo(HoleProv) casts
1128 dropCasts (CastTy ty _) = dropCasts ty
1129 dropCasts (AppTy t1 t2) = mkAppTy (dropCasts t1) (dropCasts t2)
1130 dropCasts (TyConApp tc tys) = mkTyConApp tc (map dropCasts tys)
1131 dropCasts (ForAllTy b ty) = ForAllTy (dropCastsB b) (dropCasts ty)
1132 dropCasts ty = ty -- LitTy, TyVarTy, CoercionTy
1133
1134 dropCastsB :: TyBinder -> TyBinder
1135 dropCastsB (Anon ty) = Anon (dropCasts ty)
1136 dropCastsB b = b -- Don't bother in the kind of a forall
1137
1138 abstractClassKeys :: [Unique]
1139 abstractClassKeys = [ heqTyConKey
1140 , eqTyConKey
1141 , coercibleTyConKey
1142 ] -- See Note [Equality class instances]
1143
1144 instTypeErr :: Class -> [Type] -> SDoc -> SDoc
1145 instTypeErr cls tys msg
1146 = hang (hang (text "Illegal instance declaration for")
1147 2 (quotes (pprClassPred cls tys)))
1148 2 msg
1149
1150 {- Note [Casts during validity checking]
1151 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1152 Consider the (bogus)
1153 instance Eq Char#
1154 We elaborate to 'Eq (Char# |> UnivCo(hole))' where the hole is an
1155 insoluble equality constraint for * ~ #. We'll report the insoluble
1156 constraint separately, but we don't want to *also* complain that Eq is
1157 not applied to a type constructor. So we look gaily look through
1158 CastTys here.
1159
1160 Another example: Eq (Either a). Then we actually get a cast in
1161 the middle:
1162 Eq ((Either |> g) a)
1163
1164
1165 Note [Valid 'deriving' predicate]
1166 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1167 validDerivPred checks for OK 'deriving' context. See Note [Exotic
1168 derived instance contexts] in TcDeriv. However the predicate is
1169 here because it uses sizeTypes, fvTypes.
1170
1171 It checks for three things
1172
1173 * No repeated variables (hasNoDups fvs)
1174
1175 * No type constructors. This is done by comparing
1176 sizeTypes tys == length (fvTypes tys)
1177 sizeTypes counts variables and constructors; fvTypes returns variables.
1178 So if they are the same, there must be no constructors. But there
1179 might be applications thus (f (g x)).
1180
1181 Note that tys only includes the visible arguments of the class type
1182 constructor. Including the non-vivisble arguments can cause the following,
1183 perfectly valid instance to be rejected:
1184 class Category (cat :: k -> k -> *) where ...
1185 newtype T (c :: * -> * -> *) a b = MkT (c a b)
1186 instance Category c => Category (T c) where ...
1187 since the first argument to Category is a non-visible *, which sizeTypes
1188 would count as a constructor! See Trac #11833.
1189
1190 * Also check for a bizarre corner case, when the derived instance decl
1191 would look like
1192 instance C a b => D (T a) where ...
1193 Note that 'b' isn't a parameter of T. This gives rise to all sorts of
1194 problems; in particular, it's hard to compare solutions for equality
1195 when finding the fixpoint, and that means the inferContext loop does
1196 not converge. See Trac #5287.
1197
1198 Note [Equality class instances]
1199 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1200 We can't have users writing instances for the equality classes. But we
1201 still need to be able to write instances for them ourselves. So we allow
1202 instances only in the defining module.
1203
1204 -}
1205
1206 validDerivPred :: TyVarSet -> PredType -> Bool
1207 -- See Note [Valid 'deriving' predicate]
1208 validDerivPred tv_set pred
1209 = case classifyPredType pred of
1210 ClassPred cls tys -> cls `hasKey` typeableClassKey
1211 -- Typeable constraints are bigger than they appear due
1212 -- to kind polymorphism, but that's OK
1213 || check_tys cls tys
1214 EqPred {} -> False -- reject equality constraints
1215 _ -> True -- Non-class predicates are ok
1216 where
1217 check_tys cls tys
1218 = hasNoDups fvs
1219 -- use sizePred to ignore implicit args
1220 && sizePred pred == fromIntegral (length fvs)
1221 && all (`elemVarSet` tv_set) fvs
1222 where tys' = filterOutInvisibleTypes (classTyCon cls) tys
1223 fvs = fvTypes tys'
1224
1225 {-
1226 ************************************************************************
1227 * *
1228 \subsection{Checking instance for termination}
1229 * *
1230 ************************************************************************
1231 -}
1232
1233 checkValidInstance :: UserTypeCtxt -> LHsSigType Name -> Type
1234 -> TcM ([TyVar], ThetaType, Class, [Type])
1235 checkValidInstance ctxt hs_type ty
1236 | Just (clas,inst_tys) <- getClassPredTys_maybe tau
1237 , inst_tys `lengthIs` classArity clas
1238 = do { setSrcSpan head_loc (checkValidInstHead ctxt clas inst_tys)
1239 ; traceTc "checkValidInstance {" (ppr ty)
1240 ; checkValidTheta ctxt theta
1241
1242 -- The Termination and Coverate Conditions
1243 -- Check that instance inference will terminate (if we care)
1244 -- For Haskell 98 this will already have been done by checkValidTheta,
1245 -- but as we may be using other extensions we need to check.
1246 --
1247 -- Note that the Termination Condition is *more conservative* than
1248 -- the checkAmbiguity test we do on other type signatures
1249 -- e.g. Bar a => Bar Int is ambiguous, but it also fails
1250 -- the termination condition, because 'a' appears more often
1251 -- in the constraint than in the head
1252 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
1253 ; if undecidable_ok
1254 then checkAmbiguity ctxt ty
1255 else checkInstTermination inst_tys theta
1256
1257 ; traceTc "cvi 2" (ppr ty)
1258
1259 ; case (checkInstCoverage undecidable_ok clas theta inst_tys) of
1260 IsValid -> return () -- Check succeeded
1261 NotValid msg -> addErrTc (instTypeErr clas inst_tys msg)
1262
1263 ; traceTc "End checkValidInstance }" empty
1264
1265 ; return (tvs, theta, clas, inst_tys) }
1266
1267 | otherwise
1268 = failWithTc (text "Malformed instance head:" <+> ppr tau)
1269 where
1270 (tvs, theta, tau) = tcSplitSigmaTy ty
1271
1272 -- The location of the "head" of the instance
1273 head_loc = getLoc (getLHsInstDeclHead hs_type)
1274
1275 {-
1276 Note [Paterson conditions]
1277 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1278 Termination test: the so-called "Paterson conditions" (see Section 5 of
1279 "Understanding functional dependencies via Constraint Handling Rules,
1280 JFP Jan 2007).
1281
1282 We check that each assertion in the context satisfies:
1283 (1) no variable has more occurrences in the assertion than in the head, and
1284 (2) the assertion has fewer constructors and variables (taken together
1285 and counting repetitions) than the head.
1286 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1287 (which have already been checked) guarantee termination.
1288
1289 The underlying idea is that
1290
1291 for any ground substitution, each assertion in the
1292 context has fewer type constructors than the head.
1293 -}
1294
1295 checkInstTermination :: [TcType] -> ThetaType -> TcM ()
1296 -- See Note [Paterson conditions]
1297 checkInstTermination tys theta
1298 = check_preds theta
1299 where
1300 head_fvs = fvTypes tys
1301 head_size = sizeTypes tys
1302
1303 check_preds :: [PredType] -> TcM ()
1304 check_preds preds = mapM_ check preds
1305
1306 check :: PredType -> TcM ()
1307 check pred
1308 = case classifyPredType pred of
1309 EqPred {} -> return () -- See Trac #4200.
1310 IrredPred {} -> check2 pred (sizeType pred)
1311 ClassPred cls tys
1312 | isTerminatingClass cls
1313 -> return ()
1314
1315 | isCTupleClass cls -- Look inside tuple predicates; Trac #8359
1316 -> check_preds tys
1317
1318 | otherwise
1319 -> check2 pred (sizeTypes $ filterOutInvisibleTypes (classTyCon cls) tys)
1320 -- Other ClassPreds
1321
1322 check2 pred pred_size
1323 | not (null bad_tvs) = addErrTc (noMoreMsg bad_tvs what)
1324 | pred_size >= head_size = addErrTc (smallerMsg what)
1325 | otherwise = return ()
1326 where
1327 what = text "constraint" <+> quotes (ppr pred)
1328 bad_tvs = fvType pred \\ head_fvs
1329
1330 smallerMsg :: SDoc -> SDoc
1331 smallerMsg what
1332 = vcat [ hang (text "The" <+> what)
1333 2 (text "is no smaller than the instance head")
1334 , parens undecidableMsg ]
1335
1336 noMoreMsg :: [TcTyVar] -> SDoc -> SDoc
1337 noMoreMsg tvs what
1338 = vcat [ hang (text "Variable" <> plural tvs <+> quotes (pprWithCommas ppr tvs)
1339 <+> occurs <+> text "more often")
1340 2 (sep [ text "in the" <+> what
1341 , text "than in the instance head" ])
1342 , parens undecidableMsg ]
1343 where
1344 occurs = if isSingleton tvs then text "occurs"
1345 else text "occur"
1346
1347 undecidableMsg, constraintKindsMsg :: SDoc
1348 undecidableMsg = text "Use UndecidableInstances to permit this"
1349 constraintKindsMsg = text "Use ConstraintKinds to permit this"
1350
1351 {-
1352 Note [Associated type instances]
1353 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1354 We allow this:
1355 class C a where
1356 type T x a
1357 instance C Int where
1358 type T (S y) Int = y
1359 type T Z Int = Char
1360
1361 Note that
1362 a) The variable 'x' is not bound by the class decl
1363 b) 'x' is instantiated to a non-type-variable in the instance
1364 c) There are several type instance decls for T in the instance
1365
1366 All this is fine. Of course, you can't give any *more* instances
1367 for (T ty Int) elsewhere, because it's an *associated* type.
1368
1369 Note [Checking consistent instantiation]
1370 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1371 See Trac #11450 for background discussion on this check.
1372
1373 class C a b where
1374 type T a x b
1375
1376 With this class decl, if we have an instance decl
1377 instance C ty1 ty2 where ...
1378 then the type instance must look like
1379 type T ty1 v ty2 = ...
1380 with exactly 'ty1' for 'a', 'ty2' for 'b', and a variable for 'x'.
1381 For example:
1382
1383 instance C [p] Int
1384 type T [p] y Int = (p,y,y)
1385
1386 Note that
1387
1388 * We used to allow completely different bound variables in the
1389 associated type instance; e.g.
1390 instance C [p] Int
1391 type T [q] y Int = ...
1392 But from GHC 8.2 onwards, we don't. It's much simpler this way.
1393 See Trac #11450.
1394
1395 * When the class variable isn't used on the RHS of the type instance,
1396 it's tempting to allow wildcards, thus
1397 instance C [p] Int
1398 type T [_] y Int = (y,y)
1399 But it's awkward to do the test, and it doesn't work if the
1400 variable is repeated:
1401 instance C (p,p) Int
1402 type T (_,_) y Int = (y,y)
1403 Even though 'p' is not used on the RHS, we still need to use 'p'
1404 on the LHS to establish the repeated pattern. So to keep it simple
1405 we just require equality.
1406
1407 * We also check that any non-class-tyvars are instantiated with
1408 distinct tyvars. That rules out
1409 instance C [p] Int where
1410 type T [p] Bool Int = p -- Note Bool
1411 type T [p] Char Int = p -- Note Char
1412
1413 and
1414 instance C [p] Int where
1415 type T [p] p Int = p -- Note repeated 'p' on LHS
1416 It's consistent to do this because we don't allow this kind of
1417 instantiation for the class-tyvar arguments of the family.
1418
1419 Overall, we can have exactly one type instance for each
1420 associated type. If you wantmore, use an auxiliary family.
1421
1422 Implementation
1423 * Form the mini-envt from the class type variables a,b
1424 to the instance decl types [p],Int: [a->[p], b->Int]
1425
1426 * Look at the tyvars a,x,b of the type family constructor T
1427 (it shares tyvars with the class C)
1428
1429 * Apply the mini-evnt to them, and check that the result is
1430 consistent with the instance types [p] y Int
1431
1432 We make all the instance type variables scope over the
1433 type instances, of course, which picks up non-obvious kinds. Eg
1434 class Foo (a :: k) where
1435 type F a
1436 instance Foo (b :: k -> k) where
1437 type F b = Int
1438 Here the instance is kind-indexed and really looks like
1439 type F (k->k) (b::k->k) = Int
1440 But if the 'b' didn't scope, we would make F's instance too
1441 poly-kinded.
1442 -}
1443
1444 -- | Extra information about the parent instance declaration, needed
1445 -- when type-checking associated types. The 'Class' is the enclosing
1446 -- class, the [TyVar] are the type variable of the instance decl,
1447 -- and and the @VarEnv Type@ maps class variables to their instance
1448 -- types.
1449 type ClsInstInfo = (Class, [TyVar], VarEnv Type)
1450
1451 type AssocInstArgShape = (Maybe Type, Type)
1452 -- AssocInstArgShape is used only for associated family instances
1453 -- (mb_exp, actual)
1454 -- mb_exp = Just ty => this arg corresponds to a class variable
1455 -- = Nothing => it doesn't correspond to a class variable
1456 -- e.g. class C b where
1457 -- type F a b c
1458 -- instance C [x] where
1459 -- type F p [x] q
1460 -- We get [AssocInstArgShape] = [ (Nothing, p)
1461 -- , (Just [x], [x])
1462 -- , (Nothing, q)]
1463
1464 checkConsistentFamInst
1465 :: Maybe ClsInstInfo
1466 -> TyCon -- ^ Family tycon
1467 -> [TyVar] -- ^ Type variables of the family instance
1468 -> [Type] -- ^ Type patterns from instance
1469 -> TcM ()
1470 -- See Note [Checking consistent instantiation]
1471
1472 checkConsistentFamInst Nothing _ _ _ = return ()
1473 checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc _at_tvs at_tys
1474 = do { -- Check that the associated type indeed comes from this class
1475 checkTc (Just clas == tyConAssoc_maybe fam_tc)
1476 (badATErr (className clas) (tyConName fam_tc))
1477
1478 -- Check type args first (more comprehensible)
1479 ; checkTc (all check_arg type_shapes) pp_wrong_at_arg
1480 ; checkTc (check_poly_args type_shapes) pp_wrong_at_tyvars
1481
1482 -- And now kind args
1483 ; checkTc (all check_arg kind_shapes)
1484 (pp_wrong_at_arg $$ ppSuggestExplicitKinds)
1485 ; checkTc (check_poly_args kind_shapes)
1486 (pp_wrong_at_tyvars $$ ppSuggestExplicitKinds)
1487
1488 ; traceTc "cfi" (vcat [ ppr inst_tvs
1489 , ppr arg_shapes
1490 , ppr mini_env ]) }
1491 where
1492 arg_shapes :: [AssocInstArgShape]
1493 arg_shapes = [ (lookupVarEnv mini_env fam_tc_tv, at_ty)
1494 | (fam_tc_tv, at_ty) <- tyConTyVars fam_tc `zip` at_tys ]
1495
1496 (kind_shapes, type_shapes) = partitionInvisibles fam_tc snd arg_shapes
1497
1498 check_arg :: AssocInstArgShape -> Bool
1499 check_arg (Just exp_ty, at_ty) = exp_ty `tcEqType` at_ty
1500 check_arg (Nothing, _ ) = True -- Arg position does not correspond
1501 -- to a class variable
1502 check_poly_args :: [(Maybe Type,Type)] -> Bool
1503 check_poly_args arg_shapes
1504 = allDistinctTyVars (mkVarSet inst_tvs)
1505 [ at_ty | (Nothing, at_ty) <- arg_shapes ]
1506
1507 pp_wrong_at_arg
1508 = vcat [ text "Type indexes must match class instance head"
1509 , pp_exp_act ]
1510
1511 pp_wrong_at_tyvars
1512 = vcat [ text "Polymorphic type indexes of associated type" <+> quotes (ppr fam_tc)
1513 , nest 2 $ vcat [ text "(i.e. ones independent of the class type variables)"
1514 , text "must be distinct type variables" ]
1515 , pp_exp_act ]
1516
1517 pp_exp_act
1518 = vcat [ text "Expected:" <+> ppr (mkTyConApp fam_tc expected_args)
1519 , text " Actual:" <+> ppr (mkTyConApp fam_tc at_tys)
1520 , sdocWithDynFlags $ \dflags ->
1521 ppWhen (has_poly_args dflags) $
1522 vcat [ text "where the `<tv>' arguments are type variables,"
1523 , text "distinct from each other and from the instance variables" ] ]
1524
1525 expected_args = [ exp_ty `orElse` mk_tv at_ty | (exp_ty, at_ty) <- arg_shapes ]
1526 mk_tv at_ty = mkTyVarTy (mkTyVar tv_name (typeKind at_ty))
1527 tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "<tv>") noSrcSpan
1528
1529 has_poly_args dflags = any (isNothing . fst) shapes
1530 where
1531 shapes | gopt Opt_PrintExplicitKinds dflags = arg_shapes
1532 | otherwise = type_shapes
1533
1534 badATErr :: Name -> Name -> SDoc
1535 badATErr clas op
1536 = hsep [text "Class", quotes (ppr clas),
1537 text "does not have an associated type", quotes (ppr op)]
1538
1539
1540 {-
1541 ************************************************************************
1542 * *
1543 Checking type instance well-formedness and termination
1544 * *
1545 ************************************************************************
1546 -}
1547
1548 checkValidCoAxiom :: CoAxiom Branched -> TcM ()
1549 checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
1550 = do { mapM_ (checkValidCoAxBranch Nothing fam_tc) branch_list
1551 ; foldlM_ check_branch_compat [] branch_list }
1552 where
1553 branch_list = fromBranches branches
1554 injectivity = familyTyConInjectivityInfo fam_tc
1555
1556 check_branch_compat :: [CoAxBranch] -- previous branches in reverse order
1557 -> CoAxBranch -- current branch
1558 -> TcM [CoAxBranch]-- current branch : previous branches
1559 -- Check for
1560 -- (a) this branch is dominated by previous ones
1561 -- (b) failure of injectivity
1562 check_branch_compat prev_branches cur_branch
1563 | cur_branch `isDominatedBy` prev_branches
1564 = do { addWarnAt NoReason (coAxBranchSpan cur_branch) $
1565 inaccessibleCoAxBranch ax cur_branch
1566 ; return prev_branches }
1567 | otherwise
1568 = do { check_injectivity prev_branches cur_branch
1569 ; return (cur_branch : prev_branches) }
1570
1571 -- Injectivity check: check whether a new (CoAxBranch) can extend
1572 -- already checked equations without violating injectivity
1573 -- annotation supplied by the user.
1574 -- See Note [Verifying injectivity annotation] in FamInstEnv
1575 check_injectivity prev_branches cur_branch
1576 | Injective inj <- injectivity
1577 = do { let conflicts =
1578 fst $ foldl (gather_conflicts inj prev_branches cur_branch)
1579 ([], 0) prev_branches
1580 ; mapM_ (\(err, span) -> setSrcSpan span $ addErr err)
1581 (makeInjectivityErrors ax cur_branch inj conflicts) }
1582 | otherwise
1583 = return ()
1584
1585 gather_conflicts inj prev_branches cur_branch (acc, n) branch
1586 -- n is 0-based index of branch in prev_branches
1587 = case injectiveBranches inj cur_branch branch of
1588 InjectivityUnified ax1 ax2
1589 | ax1 `isDominatedBy` (replace_br prev_branches n ax2)
1590 -> (acc, n + 1)
1591 | otherwise
1592 -> (branch : acc, n + 1)
1593 InjectivityAccepted -> (acc, n + 1)
1594
1595 -- Replace n-th element in the list. Assumes 0-based indexing.
1596 replace_br :: [CoAxBranch] -> Int -> CoAxBranch -> [CoAxBranch]
1597 replace_br brs n br = take n brs ++ [br] ++ drop (n+1) brs
1598
1599
1600 -- Check that a "type instance" is well-formed (which includes decidability
1601 -- unless -XUndecidableInstances is given).
1602 --
1603 checkValidCoAxBranch :: Maybe ClsInstInfo
1604 -> TyCon -> CoAxBranch -> TcM ()
1605 checkValidCoAxBranch mb_clsinfo fam_tc
1606 (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
1607 , cab_lhs = typats
1608 , cab_rhs = rhs, cab_loc = loc })
1609 = checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs loc
1610
1611 -- | Do validity checks on a type family equation, including consistency
1612 -- with any enclosing class instance head, termination, and lack of
1613 -- polytypes.
1614 checkValidTyFamEqn :: Maybe ClsInstInfo
1615 -> TyCon -- ^ of the type family
1616 -> [TyVar] -- ^ bound tyvars in the equation
1617 -> [CoVar] -- ^ bound covars in the equation
1618 -> [Type] -- ^ type patterns
1619 -> Type -- ^ rhs
1620 -> SrcSpan
1621 -> TcM ()
1622 checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs loc
1623 = setSrcSpan loc $
1624 do { checkValidFamPats mb_clsinfo fam_tc tvs cvs typats
1625
1626 -- The argument patterns, and RHS, are all boxed tau types
1627 -- E.g Reject type family F (a :: k1) :: k2
1628 -- type instance F (forall a. a->a) = ...
1629 -- type instance F Int# = ...
1630 -- type instance F Int = forall a. a->a
1631 -- type instance F Int = Int#
1632 -- See Trac #9357
1633 ; checkValidMonoType rhs
1634 ; check_lifted rhs
1635
1636 -- We have a decidable instance unless otherwise permitted
1637 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
1638 ; unless undecidable_ok $
1639 mapM_ addErrTc (checkFamInstRhs typats (tcTyFamInsts rhs)) }
1640
1641 -- Make sure that each type family application is
1642 -- (1) strictly smaller than the lhs,
1643 -- (2) mentions no type variable more often than the lhs, and
1644 -- (3) does not contain any further type family instances.
1645 --
1646 checkFamInstRhs :: [Type] -- lhs
1647 -> [(TyCon, [Type])] -- type family instances
1648 -> [MsgDoc]
1649 checkFamInstRhs lhsTys famInsts
1650 = mapMaybe check famInsts
1651 where
1652 size = sizeTypes lhsTys
1653 fvs = fvTypes lhsTys
1654 check (tc, tys)
1655 | not (all isTyFamFree tys) = Just (nestedMsg what)
1656 | not (null bad_tvs) = Just (noMoreMsg bad_tvs what)
1657 | size <= sizeTypes tys = Just (smallerMsg what)
1658 | otherwise = Nothing
1659 where
1660 what = text "type family application" <+> quotes (pprType (TyConApp tc tys))
1661 bad_tvs = fvTypes tys \\ fvs
1662
1663 checkValidFamPats :: Maybe ClsInstInfo -> TyCon -> [TyVar] -> [CoVar] -> [Type] -> TcM ()
1664 -- Patterns in a 'type instance' or 'data instance' decl should
1665 -- a) contain no type family applications
1666 -- (vanilla synonyms are fine, though)
1667 -- b) properly bind all their free type variables
1668 -- e.g. we disallow (Trac #7536)
1669 -- type T a = Int
1670 -- type instance F (T a) = a
1671 -- c) Have the right number of patterns
1672 -- d) For associated types, are consistently instantiated
1673 checkValidFamPats mb_clsinfo fam_tc tvs cvs ty_pats
1674 = do { -- A family instance must have exactly the same number of type
1675 -- parameters as the family declaration. You can't write
1676 -- type family F a :: * -> *
1677 -- type instance F Int y = y
1678 -- because then the type (F Int) would be like (\y.y)
1679 checkTc (length ty_pats == fam_arity) $
1680 wrongNumberOfParmsErr (fam_arity - count isInvisibleBinder fam_bndrs)
1681 -- report only explicit arguments
1682
1683 ; mapM_ checkValidTypePat ty_pats
1684
1685 ; let unbound_tcvs = filterOut (`elemVarSet` exactTyCoVarsOfTypes ty_pats) (tvs ++ cvs)
1686 ; checkTc (null unbound_tcvs) (famPatErr fam_tc unbound_tcvs ty_pats)
1687
1688 -- Check that type patterns match the class instance head
1689 ; checkConsistentFamInst mb_clsinfo fam_tc tvs ty_pats }
1690 where
1691 fam_arity = tyConArity fam_tc
1692 fam_bndrs = tyConBinders fam_tc
1693
1694
1695 checkValidTypePat :: Type -> TcM ()
1696 -- Used for type patterns in class instances,
1697 -- and in type/data family instances
1698 checkValidTypePat pat_ty
1699 = do { -- Check that pat_ty is a monotype
1700 checkValidMonoType pat_ty
1701 -- One could imagine generalising to allow
1702 -- instance C (forall a. a->a)
1703 -- but we don't know what all the consequences might be
1704
1705 -- Ensure that no type family instances occur a type pattern
1706 ; checkTc (isTyFamFree pat_ty) $
1707 tyFamInstIllegalErr pat_ty
1708
1709 ; check_lifted pat_ty }
1710
1711 isTyFamFree :: Type -> Bool
1712 -- ^ Check that a type does not contain any type family applications.
1713 isTyFamFree = null . tcTyFamInsts
1714
1715 -- Error messages
1716
1717 wrongNumberOfParmsErr :: Arity -> SDoc
1718 wrongNumberOfParmsErr exp_arity
1719 = text "Number of parameters must match family declaration; expected"
1720 <+> ppr exp_arity
1721
1722 inaccessibleCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
1723 inaccessibleCoAxBranch fi_ax cur_branch
1724 = text "Type family instance equation is overlapped:" $$
1725 nest 2 (pprCoAxBranch fi_ax cur_branch)
1726
1727 tyFamInstIllegalErr :: Type -> SDoc
1728 tyFamInstIllegalErr ty
1729 = hang (text "Illegal type synonym family application in instance" <>
1730 colon) 2 $
1731 ppr ty
1732
1733 nestedMsg :: SDoc -> SDoc
1734 nestedMsg what
1735 = sep [ text "Illegal nested" <+> what
1736 , parens undecidableMsg ]
1737
1738 famPatErr :: TyCon -> [TyVar] -> [Type] -> SDoc
1739 famPatErr fam_tc tvs pats
1740 = hang (text "Family instance purports to bind type variable" <> plural tvs
1741 <+> pprQuotedList tvs)
1742 2 (hang (text "but the real LHS (expanding synonyms) is:")
1743 2 (pprTypeApp fam_tc (map expandTypeSynonyms pats) <+>
1744 text "= ..."))
1745
1746 {-
1747 ************************************************************************
1748 * *
1749 Telescope checking
1750 * *
1751 ************************************************************************
1752
1753 Note [Bad telescopes]
1754 ~~~~~~~~~~~~~~~~~~~~~
1755 Now that we can mix type and kind variables, there are an awful lot of
1756 ways to shoot yourself in the foot. Here are some.
1757
1758 data SameKind :: k -> k -> * -- just to force unification
1759
1760 1. data T1 a k (b :: k) (x :: SameKind a b)
1761
1762 The problem here is that we discover that a and b should have the same
1763 kind. But this kind mentions k, which is bound *after* a.
1764 (Testcase: dependent/should_fail/BadTelescope)
1765
1766 2. data T2 a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
1767
1768 Note that b is not bound. Yet its kind mentions a. Because we have
1769 a nice rule that all implicitly bound variables come before others,
1770 this is bogus. (We could probably figure out to put b between a and c.
1771 But I think this is doing users a disservice, in the long run.)
1772 (Testcase: dependent/should_fail/BadTelescope4)
1773
1774 3. t3 :: forall a. (forall k (b :: k). SameKind a b) -> ()
1775
1776 This is a straightforward skolem escape. Note that a and b need to have
1777 the same kind.
1778 (Testcase: polykinds/T11142)
1779
1780 How do we deal with all of this? For TyCons, we have checkValidTyConTyVars.
1781 That function looks to see if any of the tyConTyVars are repeated, but
1782 it's really a telescope check. It works because all tycons are kind-generalized.
1783 If there is a bad telescope, the kind-generalization will end up generalizing
1784 over a variable bound later in the telescope.
1785
1786 For non-tycons, we do scope checking when we bring tyvars into scope,
1787 in tcImplicitTKBndrs and tcExplicitTKBndrs. Note that we also have to
1788 sort implicit binders into a well-scoped order whenever we have implicit
1789 binders to worry about. This is done in quantifyTyVars and in
1790 tcImplicitTKBndrs.
1791 -}
1792
1793 -- | Check a list of binders to see if they make a valid telescope.
1794 -- The key property we're checking for is scoping. For example:
1795 -- > data SameKind :: k -> k -> *
1796 -- > data X a k (b :: k) (c :: SameKind a b)
1797 -- Kind inference says that a's kind should be k. But that's impossible,
1798 -- because k isn't in scope when a is bound. This check has to come before
1799 -- general validity checking, because once we kind-generalise, this sort
1800 -- of problem is harder to spot (as we'll generalise over the unbound
1801 -- k in a's type.) See also Note [Bad telescopes].
1802 checkValidTelescope :: SDoc -- the original user-written telescope
1803 -> [TyVar] -- explicit vars (not necessarily zonked)
1804 -> SDoc -- note to put at bottom of message
1805 -> TcM ()
1806 checkValidTelescope hs_tvs orig_tvs extra
1807 = discardResult $ checkZonkValidTelescope hs_tvs orig_tvs extra
1808
1809 -- | Like 'checkZonkValidTelescope', but returns the zonked tyvars
1810 checkZonkValidTelescope :: SDoc
1811 -> [TyVar]
1812 -> SDoc
1813 -> TcM [TyVar]
1814 checkZonkValidTelescope hs_tvs orig_tvs extra
1815 = do { orig_tvs <- mapM zonkTyCoVarKind orig_tvs
1816 ; let (_, sorted_tidied_tvs) = tidyTyCoVarBndrs emptyTidyEnv $
1817 toposortTyVars orig_tvs
1818 ; unless (go [] emptyVarSet orig_tvs) $
1819 addErr $
1820 vcat [ hang (text "These kind and type variables:" <+> hs_tvs $$
1821 text "are out of dependency order. Perhaps try this ordering:")
1822 2 (sep (map pprTvBndr sorted_tidied_tvs))
1823 , extra ]
1824 ; return orig_tvs }
1825
1826 where
1827 go :: [TyVar] -- misplaced variables
1828 -> TyVarSet -> [TyVar] -> Bool
1829 go errs in_scope [] = null (filter (`elemVarSet` in_scope) errs)
1830 -- report an error only when the variable in the kind is brought
1831 -- into scope later in the telescope. Otherwise, we'll just quantify
1832 -- over it in kindGeneralize, as we should.
1833
1834 go errs in_scope (tv:tvs)
1835 = let bad_tvs = filterOut (`elemVarSet` in_scope) $
1836 tyCoVarsOfTypeList (tyVarKind tv)
1837 in go (bad_tvs ++ errs) (in_scope `extendVarSet` tv) tvs
1838
1839 -- | After inferring kinds of type variables, check to make sure that the
1840 -- inferred kinds any of the type variables bound in a smaller scope.
1841 -- This is a skolem escape check. See also Note [Bad telescopes].
1842 checkValidInferredKinds :: [TyVar] -- ^ vars to check (zonked)
1843 -> TyVarSet -- ^ vars out of scope
1844 -> SDoc -- ^ suffix to error message
1845 -> TcM ()
1846 checkValidInferredKinds orig_kvs out_of_scope extra
1847 = do { let bad_pairs = [ (tv, kv)
1848 | kv <- orig_kvs
1849 , Just tv <- map (lookupVarSet out_of_scope)
1850 (tyCoVarsOfTypeList (tyVarKind kv)) ]
1851 report (tidyTyVarOcc env -> tv, tidyTyVarOcc env -> kv)
1852 = addErr $
1853 text "The kind of variable" <+>
1854 quotes (ppr kv) <> text ", namely" <+>
1855 quotes (ppr (tyVarKind kv)) <> comma $$
1856 text "depends on variable" <+>
1857 quotes (ppr tv) <+> text "from an inner scope" $$
1858 text "Perhaps bind" <+> quotes (ppr kv) <+>
1859 text "sometime after binding" <+>
1860 quotes (ppr tv) $$
1861 extra
1862 ; mapM_ report bad_pairs }
1863
1864 where
1865 (env1, _) = tidyTyCoVarBndrs emptyTidyEnv orig_kvs
1866 (env, _) = tidyTyCoVarBndrs env1 (varSetElems out_of_scope)
1867
1868 {-
1869 ************************************************************************
1870 * *
1871 \subsection{Auxiliary functions}
1872 * *
1873 ************************************************************************
1874 -}
1875
1876 -- Free variables of a type, retaining repetitions, and expanding synonyms
1877 fvType :: Type -> [TyCoVar]
1878 fvType ty | Just exp_ty <- coreView ty = fvType exp_ty
1879 fvType (TyVarTy tv) = [tv]
1880 fvType (TyConApp _ tys) = fvTypes tys
1881 fvType (LitTy {}) = []
1882 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1883 fvType (ForAllTy bndr ty)
1884 = fvType (binderType bndr) ++
1885 caseBinder bndr (\tv -> filter (/= tv)) (const id) (fvType ty)
1886 fvType (CastTy ty co) = fvType ty ++ fvCo co
1887 fvType (CoercionTy co) = fvCo co
1888
1889 fvTypes :: [Type] -> [TyVar]
1890 fvTypes tys = concat (map fvType tys)
1891
1892 fvCo :: Coercion -> [TyCoVar]
1893 fvCo (Refl _ ty) = fvType ty
1894 fvCo (TyConAppCo _ _ args) = concatMap fvCo args
1895 fvCo (AppCo co arg) = fvCo co ++ fvCo arg
1896 fvCo (ForAllCo tv h co) = filter (/= tv) (fvCo co) ++ fvCo h
1897 fvCo (CoVarCo v) = [v]
1898 fvCo (AxiomInstCo _ _ args) = concatMap fvCo args
1899 fvCo (UnivCo p _ t1 t2) = fvProv p ++ fvType t1 ++ fvType t2
1900 fvCo (SymCo co) = fvCo co
1901 fvCo (TransCo co1 co2) = fvCo co1 ++ fvCo co2
1902 fvCo (NthCo _ co) = fvCo co
1903 fvCo (LRCo _ co) = fvCo co
1904 fvCo (InstCo co arg) = fvCo co ++ fvCo arg
1905 fvCo (CoherenceCo co1 co2) = fvCo co1 ++ fvCo co2
1906 fvCo (KindCo co) = fvCo co
1907 fvCo (SubCo co) = fvCo co
1908 fvCo (AxiomRuleCo _ cs) = concatMap fvCo cs
1909
1910 fvProv :: UnivCoProvenance -> [TyCoVar]
1911 fvProv UnsafeCoerceProv = []
1912 fvProv (PhantomProv co) = fvCo co
1913 fvProv (ProofIrrelProv co) = fvCo co
1914 fvProv (PluginProv _) = []
1915 fvProv (HoleProv h) = pprPanic "fvProv falls into a hole" (ppr h)
1916
1917 sizeType :: Type -> Int
1918 -- Size of a type: the number of variables and constructors
1919 sizeType ty | Just exp_ty <- coreView ty = sizeType exp_ty
1920 sizeType (TyVarTy {}) = 1
1921 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1922 sizeType (LitTy {}) = 1
1923 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1924 sizeType (ForAllTy (Anon arg) res)
1925 = sizeType arg + sizeType res + 1
1926 sizeType (ForAllTy (Named {}) ty)
1927 = sizeType ty
1928 sizeType (CastTy ty _) = sizeType ty
1929 sizeType (CoercionTy _) = 1
1930
1931 sizeTypes :: [Type] -> Int
1932 sizeTypes = sum . map sizeType
1933
1934 -- Size of a predicate
1935 --
1936 -- We are considering whether class constraints terminate.
1937 -- Equality constraints and constraints for the implicit
1938 -- parameter class always termiante so it is safe to say "size 0".
1939 -- (Implicit parameter constraints always terminate because
1940 -- there are no instances for them---they are only solved by
1941 -- "local instances" in expressions).
1942 -- See Trac #4200.
1943 sizePred :: PredType -> Int
1944 sizePred ty = goClass ty
1945 where
1946 goClass p = go (classifyPredType p)
1947
1948 go (ClassPred cls tys')
1949 | isTerminatingClass cls = 0
1950 | otherwise = sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys')
1951 go (EqPred {}) = 0
1952 go (IrredPred ty) = sizeType ty
1953
1954 -- | When this says "True", ignore this class constraint during
1955 -- a termination check
1956 isTerminatingClass :: Class -> Bool
1957 isTerminatingClass cls
1958 = isIPClass cls
1959 || cls `hasKey` typeableClassKey
1960 || cls `hasKey` coercibleTyConKey
1961 || cls `hasKey` eqTyConKey
1962 || cls `hasKey` heqTyConKey
1963
1964 -- | Tidy before printing a type
1965 ppr_tidy :: TidyEnv -> Type -> SDoc
1966 ppr_tidy env ty = pprType (tidyType env ty)
1967
1968 allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool
1969 -- (allDistinctTyVars tvs tys) returns True if tys are
1970 -- a) all tyvars
1971 -- b) all distinct
1972 -- c) disjoint from tvs
1973 allDistinctTyVars _ [] = True
1974 allDistinctTyVars tkvs (ty : tys)
1975 = case getTyVar_maybe ty of
1976 Nothing -> False
1977 Just tv | tv `elemVarSet` tkvs -> False
1978 | otherwise -> allDistinctTyVars (tkvs `extendVarSet` tv) tys