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