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