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