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